Documentation

DescriptiveComplexity.Problems.Cvp.Hardness.Wiring

The drawn circuit, gate by gate #

What the interpretation of DescriptiveComplexity.Problems.Cvp.Hardness.Interp marks and wires, read back as statements about named points – bdPt, hdPt … – rather than about raw tagged tuples. Two kinds of lemma are needed downstream and both are proved here once:

the marks: which points are gates of which kind, and which point is the output;
the wires: for each gate, an iff naming its left and right inputs, so that a derivation can be built (the mpr direction, used to evaluate the circuit) and inverted (the mp direction, used to prove that nothing else evaluates to 1).

Everything is stated relative to a minimum m and a maximum M of the universe, which a finite nonempty linear order supplies; the coordinates a tag does not use are pinned to m.

The points #

def DescriptiveComplexity.CvpDraw.ttPt {A : Type} (m : A) :

cvpInterp.Map A

The constant 1 gate.

Equations

DescriptiveComplexity.CvpDraw.ttPt m = (DescriptiveComplexity.CvpTag.tt , fun (x : Fin 3) => m)

Instances For

Dependency graph

def DescriptiveComplexity.CvpDraw.ffPt {A : Type} (m : A) :

cvpInterp.Map A

The constant 0 gate.

Equations

DescriptiveComplexity.CvpDraw.ffPt m = (DescriptiveComplexity.CvpTag.ff , fun (x : Fin 3) => m)

Instances For

Dependency graph

def DescriptiveComplexity.CvpDraw.bdPt {A : Type} (c y s : A) :

cvpInterp.Map A

The conjunction chain of the clause c up to the literal y, at stage s.

Equations

DescriptiveComplexity.CvpDraw.bdPt c y s = (DescriptiveComplexity.CvpTag.bd , ![c, y, s])

Instances For

Dependency graph

def DescriptiveComplexity.CvpDraw.bdTopPt {A : Type} (m c y : A) :

cvpInterp.Map A

The conjunction chain of the clause c up to y, read at the last stage.

Equations

DescriptiveComplexity.CvpDraw.bdTopPt m c y = (DescriptiveComplexity.CvpTag.bdTop , ![c, y, m])

Instances For

Dependency graph

def DescriptiveComplexity.CvpDraw.hdPt {A : Type} (x c s : A) :

cvpInterp.Map A

The propagation chain forcing x from the clauses up to c, at stage s.

Equations

DescriptiveComplexity.CvpDraw.hdPt x c s = (DescriptiveComplexity.CvpTag.hd , ![x, c, s])

Instances For

Dependency graph

def DescriptiveComplexity.CvpDraw.glPt {A : Type} (m c : A) :

cvpInterp.Map A

The goal chain over the clauses up to c.

Equations

DescriptiveComplexity.CvpDraw.glPt m c = (DescriptiveComplexity.CvpTag.gl , ![c, m, m])

Instances For

Dependency graph

The marks #

theorem DescriptiveComplexity.CvpDraw.isTrue_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : CvpTag) (w : Fin 3 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circIsTrue ![(t, w)] ↔ t = CvpTag.tt ∧ (∀ (a : A), w 0 ≤ a) ∧ (∀ (a : A), w 1 ≤ a) ∧ ∀ (a : A), w 2 ≤ a

Only the canonical tt point is a constant 1.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.isAnd_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : CvpTag) (w : Fin 3 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circIsAnd ![(t, w)] ↔ t = CvpTag.bd ∨ t = CvpTag.bdTop ∧ ∀ (a : A), w 2 ≤ a

The conjunction gates are the two conjunction chains.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.isOr_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : CvpTag) (w : Fin 3 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circIsOr ![(t, w)] ↔ t = CvpTag.hd ∨ t = CvpTag.gl ∧ (∀ (a : A), w 1 ≤ a) ∧ ∀ (a : A), w 2 ≤ a

The disjunction gates are the propagation chain and the goal chain.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.not_isNot {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : CvpTag) (w : Fin 3 → A) :

¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.circIsNot ![(t, w)]

The circuit is monotone: it has no negation gate.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.out_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : CvpTag) (w : Fin 3 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circOut ![(t, w)] ↔ t = CvpTag.gl ∧ (∀ (a : A), a ≤ w 0) ∧ (∀ (a : A), w 1 ≤ a) ∧ ∀ (a : A), w 2 ≤ a

The output is the top of the goal chain.

Dependency graph

The wires #

Each gate names its left and its right input. The mpr direction builds a derivation, the mp direction inverts one; the constants have no input at all.

theorem DescriptiveComplexity.CvpDraw.eq_pad {A : Type} [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) {w : Fin 3 → A} (h0 : ∀ (a : A), w 0 ≤ a) (h1 : ∀ (a : A), w 1 ≤ a) (h2 : ∀ (a : A), w 2 ≤ a) :

w = fun (x : Fin 3) => m

Being pinned to the minimum at every coordinate identifies a padded point.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.isBot_iff_eq {A : Type} [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) (x : A) :

(∀ (a : A), x ≤ a) ↔ x = m

In a linear order with a minimum m, being below everything is being m: the rewrite that turns the padding conditions into equations.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.left_bd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) (w : Fin 3 → A) (q : cvpInterp.Map A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circLeft ![(CvpTag.bd , w), q] ↔ (∀ (a : A), w 1 ≤ a) ∧ q = ttPt m ∨ ∃ (y' : A), y' ⋖ w 1 ∧ q = bdPt (w 0) y' (w 2)

The left input of a conjunction chain: the constant 1 at the bottom of the walk, the previous link otherwise.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.isTop_iff_eq {A : Type} [LinearOrder A] {M : A} (hM : ∀ (a : A), a ≤ M) (x : A) :

(∀ (a : A), a ≤ x) ↔ x = M

Dually, being above everything is being the maximum.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.left_bdTop {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) (w : Fin 3 → A) (q : cvpInterp.Map A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circLeft ![(CvpTag.bdTop , w), q] ↔ (∀ (a : A), w 2 ≤ a) ∧ (∀ (a : A), w 1 ≤ a) ∧ q = ttPt m ∨ (∀ (a : A), w 2 ≤ a) ∧ ∃ (y' : A), y' ⋖ w 1 ∧ q = bdTopPt m (w 0) y'

The left input of the top-stage conjunction chain.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.left_hd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) (w : Fin 3 → A) (q : cvpInterp.Map A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circLeft ![(CvpTag.hd , w), q] ↔ (∀ (a : A), w 1 ≤ a) ∧ q = ffPt m ∨ ∃ (c' : A), c' ⋖ w 1 ∧ q = hdPt (w 0) c' (w 2)

The left input of the propagation chain: the constant 0 at the bottom of the walk over clauses, the previous link otherwise.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.left_gl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) (w : Fin 3 → A) (q : cvpInterp.Map A) (h1 : ∀ (a : A), w 1 ≤ a) (h2 : ∀ (a : A), w 2 ≤ a) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circLeft ![(CvpTag.gl , w), q] ↔ (∀ (a : A), w 0 ≤ a) ∧ AtMostOnePositive A ∧ q = ffPt m ∨ (∀ (a : A), w 0 ≤ a) ∧ ¬AtMostOnePositive A ∧ q = ttPt m ∨ ∃ (c' : A), c' ⋖ w 0 ∧ q = glPt m c'

The left input of the goal chain. At the bottom of the walk it is the constant 1 exactly when the instance is not Horn, which is what makes a non-Horn instance a yes-instance outright.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.right_bd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) {M : A} (hM : ∀ (a : A), a ≤ M) (w : Fin 3 → A) (q : cvpInterp.Map A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circRight ![(CvpTag.bd , w), q] ↔ ¬SatOcc.NegIn (w 0) (w 1) ∧ q = ttPt m ∨ SatOcc.NegIn (w 0) (w 1) ∧ (∀ (a : A), w 2 ≤ a) ∧ q = ffPt m ∨ SatOcc.NegIn (w 0) (w 1) ∧ ∃ (s' : A), s' ⋖ w 2 ∧ q = hdPt (w 1) M s'

The right input of a conjunction chain: the constant 1 when the literal is not a negative literal of the clause, the constant 0 at the bottom stage, and the propagation gate of the previous stage otherwise.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.right_bdTop {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) {M : A} (hM : ∀ (a : A), a ≤ M) (w : Fin 3 → A) (q : cvpInterp.Map A) (h2 : ∀ (a : A), w 2 ≤ a) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circRight ![(CvpTag.bdTop , w), q] ↔ ¬SatOcc.NegIn (w 0) (w 1) ∧ q = ttPt m ∨ SatOcc.NegIn (w 0) (w 1) ∧ q = hdPt (w 1) M M

The right input of the top-stage conjunction chain reads the propagation gate at the last stage.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.right_hd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) {M : A} (hM : ∀ (a : A), a ≤ M) (w : Fin 3 → A) (q : cvpInterp.Map A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circRight ![(CvpTag.hd , w), q] ↔ (SatOcc.IsCl (w 1) ∧ SatOcc.PosIn (w 1) (w 0)) ∧ q = bdPt (w 1) M (w 2) ∨ ¬(SatOcc.IsCl (w 1) ∧ SatOcc.PosIn (w 1) (w 0)) ∧ q = ffPt m

The right input of the propagation chain: the body of the clause at hand when that clause has the right positive literal, the constant 0 otherwise.

Dependency graph

theorem DescriptiveComplexity.CvpDraw.right_gl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) {M : A} (hM : ∀ (a : A), a ≤ M) (w : Fin 3 → A) (q : cvpInterp.Map A) (h1 : ∀ (a : A), w 1 ≤ a) (h2 : ∀ (a : A), w 2 ≤ a) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.circRight ![(CvpTag.gl , w), q] ↔ (SatOcc.IsCl (w 0) ∧ ∀ (x : A), ¬SatOcc.PosIn (w 0) x) ∧ q = bdTopPt m (w 0) M ∨ ¬(SatOcc.IsCl (w 0) ∧ ∀ (x : A), ¬SatOcc.PosIn (w 0) x) ∧ q = ffPt m

The right input of the goal chain: the top-stage body of the clause at hand when it is a goal clause, the constant 0 otherwise.

Dependency graph