Reading the encoded sentence off the image

DescriptiveComplexity.Problems.FinSat.Interp builds the sentence σ_A and proves it well formed (DescriptiveComplexity.FinSat.image_isWF); this file reads it back as a sentence – what its nodes are, and which of them are children, binders and literals of which – which is what the correctness of the reduction is then stated and proved against.

The elements are points

Every relation of the image but the order demands canonically padded tuples (DescriptiveComplexity.FinSat.canonG), and a canonical tuple is the padding of its own prefix (DescriptiveComplexity.pad_pref_of_canon). So the elements the sentence actually reads are exactly the DescriptiveComplexity.FinSat.ptOf a₀ t w: a tag together with a tuple of the tag's own length, padded with the least element. Elements that are not of that form are junk – variables of the encoded sentence that no node binds and no literal reads – and DescriptiveComplexity.FinSat.eq_ptOf says they are the only ones, so every case analysis may assume a point.

This is the idiom the library uses wherever tagged tuples are compared: a def for the element, an iff lemma for each relation it takes part in, and an inversion lemma putting an arbitrary element in that form. Matching on a pair literal at the type FOInterpretation.Map is ill-typed at the transparency rw and simp work at, so the named constructor is not a convenience but a requirement.

The points of the image

def DescriptiveComplexity.FinSat.ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : (finsatInterp B φ).Map A

An element of the encoded sentence: a tag, and a tuple of the tag's own length padded with the least element a₀.

Equations

• DescriptiveComplexity.FinSat.ptOf B φ a₀ t w = (t, DescriptiveComplexity.pad a₀ w)

@[simp]

theorem DescriptiveComplexity.FinSat.ptOf_fst {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : (ptOf B φ a₀ t w).1 = t

@[simp]

theorem DescriptiveComplexity.FinSat.ptOf_snd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : (ptOf B φ a₀ t w).2 = pad a₀ w

theorem DescriptiveComplexity.FinSat.canon_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : Canon (tagDim B φ (ptOf B φ a₀ t w).1) (ptOf B φ a₀ t w).2

theorem DescriptiveComplexity.FinSat.eq_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {x : (finsatInterp B φ).Map A} (h : Canon (tagDim B φ x.1) x.2) : x = ptOf B φ a₀ x.1 (pref ⋯ x.2)

Junk is the only thing that is not a point: an element whose tuple is canonically padded for its tag is the point of its own prefix.

theorem DescriptiveComplexity.FinSat.ptOf_inj {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {t : FTag B φ} {w w' : Fin (tagDim B φ t) → A} (h : ptOf B φ a₀ t w = ptOf B φ a₀ t w') : w = w'

The kinds of a node, at a point

The four kinds are decided by the tag alone (DescriptiveComplexity.FinSat.andTag and its companions), so at a point they are read off the tag and nothing else.

The nodes of the encoded sentence, by name

One definition per tag, so that a statement about the sentence never mentions a tuple that has to be reduced to be typed. Each is a DescriptiveComplexity.FinSat.ptOf, definitionally, which is how the lemmas below are proved: the work is done at ptOf – where the tags are literal constructors, so simp can reduce the body of a defining formula – and transported to the named node by exact, which unfolds at the transparency the matching tactics do not.

def DescriptiveComplexity.FinSat.pvarPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ a : A) : (finsatInterp B φ).Map A

The variable that existential binds.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.FinSat.dbvarPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (l : Fin (Tseitin.maxCtx φ)) : (finsatInterp B φ).Map A

The variable naming a de Bruijn level of the kernel.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.FinSat.symPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (i : B.ι) : (finsatInterp B φ).Map A

The relation symbol of a relation variable of the block.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.FinSat.aposPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (j : Fin (finsatDim B φ)) : (finsatInterp B φ).Map A

An argument position of the relation symbols.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.FinSat.ndPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (p : Pos B φ) (pol : Bool) : (finsatInterp B φ).Map A

The translation of the subformula at a position, at a polarity.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.FinSat.atupPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) : (finsatInterp B φ).Map A

One tuple of the translation of an atom the sentence may not mention.

Equations

• DescriptiveComplexity.FinSat.atupPt B φ a₀ p pol w = DescriptiveComplexity.FinSat.ptOf B φ a₀ (DescriptiveComplexity.FinSat.Tag.atup p pol) w

The relations that read the tuples

child, bind and the two equality literals are not decided by the tags alone: their bodies compare the elements the tuples hold. Each is bridged to its named body (DescriptiveComplexity.FinSat.childBodyF and its companions) read at the valuation the interpretation supplies, and then computed at the tags it is defined for.

The bridge is stated at points, not at two arbitrary elements projected with .1: a projection out of FOInterpretation.Map is ill-typed at the transparency simp matches at, so childBodyF B φ g.1 c.1 would never reduce even with both tags known. At a point the tag is syntactically there.

The child relation, node by node

The binders, the literals and the root

theorem DescriptiveComplexity.FinSat.bindG_nd_dbvar {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (l : Fin (Tseitin.maxCtx φ)) : BindG (ndPt B φ a₀ p pol) (dbvarPt B φ a₀ l) ↔ qLevel B φ p = some ↑l

A quantifier of the kernel binds the variable of the de Bruijn level it introduces.

Inversion: these are the only children

The truth definition quantifies over all the children of a node, so reading σ_A needs the converse of the lemmas above: which elements of the image are children of a given node, and no others. Everything rests on canonicity – a relation of the image holds only of canonically padded tuples, and those are the points – so an arbitrary element can always be replaced by a point, after which the tag alone decides.

The tuples of the tags of dimension zero, one and two, read out: what the inversion lemmas put an arbitrary tuple back into.

theorem DescriptiveComplexity.FinSat.tup_zero_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {t : FTag B φ} (h : tagDim B φ t = 0) (w w' : Fin (tagDim B φ t) → A) : w = w'

theorem DescriptiveComplexity.FinSat.tup_one_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {t : FTag B φ} (h : tagDim B φ t = 1) (w : Fin (tagDim B φ t) → A) (h0 : 0 < tagDim B φ t) : w = fun (x : Fin (tagDim B φ t)) => w ⟨0, h0⟩

theorem DescriptiveComplexity.FinSat.tup_two_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {t : FTag B φ} (h : tagDim B φ t = 2) (w : Fin (tagDim B φ t) → A) (h0 : 0 < tagDim B φ t) (h1 : 1 < tagDim B φ t) : w = fun (j : Fin (tagDim B φ t)) => if ↑j = 0 then w ⟨0, h0⟩ else w ⟨1, h1⟩

The literals and the atoms, node by node

The remaining clauses of the truth definition: the equality literals of the kernel and of the translated atoms, and the atoms of the relation variables – the only genuine atoms of the encoded sentence – with their symbols, their argument positions and their signature. All but the literals of a translated atom are decided by the tags.

The atoms of the relation variables, which the encoded sentence does name: all four relations are decided by the tags.

The children of the translated kernel

Inside the kernel a node takes the nodes of its children positions – the polarity flipping exactly at the premise of an implication – and, where the kernel carries an atom the sentence may not mention, the tuple nodes of that atom, each of which takes one equality literal per argument. A tuple node of another position is never a child, which is what makes the translation of two atoms independent.

theorem DescriptiveComplexity.FinSat.childG_nd_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (c : (finsatInterp B φ).Map A) : ChildG (ndPt B φ a₀ p pol) c ↔ (∃ (q : Pos B φ) (pol' : Bool), kidOf φ p.snd q.snd = some (pol ^^ pol') ∧ c = ndPt B φ a₀ q pol') ∨ ∃ (w : Fin (tagDim B φ (Tag.atup p pol)) → A), ChildG (ndPt B φ a₀ p pol) (atupPt B φ a₀ p pol w) ∧ c = atupPt B φ a₀ p pol w

The children of a node of the translated kernel.

The binders of a quantifier node

The quantifier clauses of the truth definition quantify over the variables a node binds, so they need the converse of DescriptiveComplexity.FinSat.bindG_nd_dbvar: a quantifier of the kernel binds the variable of the de Bruijn level it introduces, and nothing else.

The environment, as a de Bruijn context

An environment of the encoded sentence assigns a model element to every element of the image; what the kernel's own recursion reads is only its restriction to the variables of the de Bruijn levels. Passing under a quantifier updates the environment at one variable, and that is exactly Fin.snoc on the context tuple – the one calculation the quantifier case of the kernel recursion needs.

def DescriptiveComplexity.FinSat.envOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (v : (finsatInterp B φ).Map A → M) : Fin (Tseitin.maxCtx φ) → M

The de Bruijn context an environment carries.

Equations

• DescriptiveComplexity.FinSat.envOf B φ a₀ v l = v (DescriptiveComplexity.FinSat.dbvarPt B φ a₀ l)

The equality literals of the kernel, inverted

The truth definition's literal clauses quantify over the two elements an equality relates, so, as with the children, an arbitrary pair has to be put back into points and the tags then decide.

The existential prefix, evaluated

The prefix is the one chain of the encoded sentence, and the one place the proof walks the input order. Its evaluation needs nothing about the kernel: given that the top conjunction holds under the environment sending each variable x_b to its intended value, every node of the prefix holds – by downward induction, from the greatest element of the input order, where the child is the top conjunction, to the least, which is the root of the sentence.

The diagram, evaluated

What is left of the ⟹ direction, once the prefix is walked: the top conjunction. Its children are the distinctness literals and the root of the translated kernel, so it holds as soon as the environment separates the variables of distinct elements – which the intended assignment does, being injective – and the kernel holds.

theorem DescriptiveComplexity.FinSat.gval_of_kernel {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (ι : A → M) (hinj : Function.Injective ι) (hker : ∀ (v : (finsatInterp B φ).Map A → M), (∀ (b : A), v (pvarPt B φ a₀ b) = ι b) → Gval I v (ndPt B φ a₀ (rootPos B φ) true)) (v : (finsatInterp B φ).Map A → M) (g : (finsatInterp B φ).Map A) (hg : RootG g) : Gval I v g

The encoded sentence holds, modulo its kernel: the whole of the ⟹ direction that does not depend on φ. An injective intended assignment ι of the prefix variables satisfies the diagram, the prefix chain carries it to the root, and what is left to prove of σ_A is that the root of the translated kernel holds under every environment giving the prefix variables their intended values.

The model side: an interpretation from an assignment of the block

DescriptiveComplexity.FinSat.FinSatOn asks for a model together with a local interpretation – one that reads a symbol only at the argument positions of its own signature. The relation variables of the block give one: the symbol of a variable is interpreted by that variable's relation, read at the argument positions. Locality is what makes it a relation of the symbol's own arity rather than of the whole universe, and it is the condition the truth definition's atom clauses are stated against.

noncomputable def DescriptiveComplexity.FinSat.argTup {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (i : B.ι) (w : (finsatInterp B φ).Map A → M) : Fin (B.arity i) → M

The arguments an assignment of the argument positions gives to a relation variable. A variable of the block whose arity exceeds the dimension cannot occur in the kernel, so the sentence never reads it; the value taken there is immaterial, and reading it at the first position keeps the whole tuple inside the symbol's signature, which is what locality asks.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.FinSat.blockI {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (μ : B.Assignment M) : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop

The interpretation determined by an assignment of the block.

Equations

• DescriptiveComplexity.FinSat.blockI B φ a₀ μ s w = ∃ (i : B.ι), s = DescriptiveComplexity.FinSat.symPt B φ a₀ i ∧ μ i (DescriptiveComplexity.FinSat.argTup B φ a₀ i w)

The atom clause does not depend on the assignment it is read at

The truth definition reads an atom at some assignment of the argument positions matching the environment on the atom's arguments. Two such assignments agree on every position of the symbol's signature – that is what DescriptiveComplexity.FinSat.IsWF.arg_tot gives – so a local interpretation cannot tell them apart, and the clause may always be read at the canonical assignment below. This is the one place the shape conditions of well-formedness are used for something other than being proved.

The atoms of the relation variables, evaluated

Putting the last three pieces together: at a node of the kernel carrying an atom of a relation variable, the atom clause of the truth definition says exactly that the variable's relation holds of the values its arguments take. This is the one clause of the kernel recursion that mentions the model at all.

The nodes of a translated atom

An atom the sentence may not mention becomes a disjunction over the tuples where it holds, each tuple a conjunction of equality literals pinning one argument to a prefix variable. Those two node kinds need the same treatment as the kernel's: which clause of the truth definition fires, and which elements it relates.

The one place the input structure is read

The tuple nodes of a translated atom are selected by a defining formula, so reading them off the image means realizing that formula: for an atom of the input vocabulary it is the atom itself, at the tuple the node holds; for the marker old it is ⊤, since every original element is old. The kernelNode equation is a hypothesis to rewrite with – its arity is an implicit argument, so destructing it would land in HEq.

The truth definition at a node of the kernel

What the kernel says at a position decides which clause of the truth definition can fire there, and the other seven are then vacuous. These two lemmas do that bookkeeping once: at a node translating an n-ary connective – falsity, an implication or an atom the sentence may not mention – the value is the disjunction of the children's at polarity true and their conjunction at polarity false.

At a quantifier node the value is the conjunction (respectively the disjunction) over the model of the child's, the bound variable of the level the quantifier introduces taking each value in turn.

At a node translating an equality of the kernel the value is that equality, read at the variables of the two de Bruijn levels.

At a node translating an atom of a relation variable – the only genuine atoms of the encoded sentence – the value is that relation, read at the values of the atom's arguments.

The kernel, position by position

The cases of the induction, each stated for a subformula of the kernel embedded by a DescriptiveComplexity.FinSat.SubEmb: the shape facts come from SubEmb.node, the children from SubEmb.kid and SubEmb.kid_range through DescriptiveComplexity.FinSat.childG_nd_iff.

The truth definition at the two node kinds of a translated atom: a tuple node is the conjunction of its literals (the disjunction, at a negatively translated atom), and a literal is the equality it carries.

The kernel, by induction on the formula

The node lemmas above are stated about a position; tying them together is an induction on the kernel itself, carried by a DescriptiveComplexity.FinSat.SubEmb – a subformula together with an embedding of its positions into the kernel's – so that the clause of a node, which quantifies over all the children it has in the kernel, collapses to the subformula (SubEmb.no_children, SubEmb.imp_children, SubEmb.all_children).

Two things fall out of the same induction rather than being assumed: negation normal form, as the second half of each statement, and the quantifier step, where updating the environment at the variable of the level bound there is Fin.snoc on the context tuple (pref_envOf_upd).

The model is any structure over DescriptiveComplexity.newLang L whose relations are read through an injection ι of the instance – the shape an extended universe A ⊕ Fin m has (DescriptiveComplexity.relMap_ext_iff), and the only thing about it the translation uses.

theorem DescriptiveComplexity.FinSat.gval_kernel {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) [(newLang L).Structure M] [Nonempty M] (μ : B.Assignment M) (ι : A → M) (hrel : ∀ {k : ℕ} (r : L.Relations k) (u : Fin k → M), FirstOrder.Language.Structure.RelMap (Sum.inl r) u ↔ ∃ (y : Fin k → A), FirstOrder.Language.Structure.RelMap r y ∧ ∀ (j : Fin k), u j = ι (y j)) (hold : ∀ (u : Fin 1 → M), FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) u ↔ ∃ (a : A), u 0 = ι a) {n : ℕ} (f : ((newLang L).sum B.lang).BoundedFormula Empty n) (x✝ : SubEmb φ f) (hn : n ≤ Tseitin.maxCtx φ) (v : (finsatInterp B φ).Map A → M) : (∀ (b : A), v (pvarPt B φ a₀ b) = ι b) → (Gval (blockI B φ a₀ μ) v (ndPt B φ a₀ ⟨n, x✝.emb (Tseitin.rootAt f)⟩ true) ↔ Tseitin.RealizeWith μ f (pref hn (envOf B φ a₀ v))) ∧ (Gval (blockI B φ a₀ μ) v (ndPt B φ a₀ ⟨n, x✝.emb (Tseitin.rootAt f)⟩ false) ↔ ¬Tseitin.RealizeWith μ f (pref hn (envOf B φ a₀ v)))

The translated kernel computes the kernel: at every position of the kernel the node of the encoded sentence at polarity true holds exactly when the subformula there does, and the node at polarity false exactly when it does not.

The environment gives the prefix variables their intended values ι and the variables of the de Bruijn levels the context tuple; the model reads the relations of the instance through ι, which is what an extended universe does.