Canonically padded tuples

Shared machinery for interpretations whose tags need tuples of different lengths. The universe of a DescriptiveComplexity.FOInterpretation is Tag × A^dim for a single dimension dim, so an element meant to carry an m-tuple with m < dim must fix its remaining coordinates; otherwise the same intended element would have several representatives, which for the SAT-family reductions would mean several distinct propositional variables standing for the same atom.

The convention here is to pad with a minimum of the input order: a tuple is DescriptiveComplexity.Canon m when every coordinate from m on is a minimum. This is the one place where the reductions of the library need their input structure to be ordered. The file provides

• the semantic side: DescriptiveComplexity.Canon, DescriptiveComplexity.Agree, the padding DescriptiveComplexity.pad and prefix DescriptiveComplexity.pref operations, and the fact that a canonical tuple is the padding of its prefix (DescriptiveComplexity.pad_pref_of_canon, DescriptiveComplexity.eq_pad_of_canon_agree);
• the first-order side: formulas DescriptiveComplexity.canonF, DescriptiveComplexity.eqTupF, DescriptiveComplexity.agreeF over the ordered expansion L.sum Language.order expressing these conditions of the coordinates held by selected free variables, with their realization lemmas;
• the special case of a tuple read from a context through an index map (DescriptiveComplexity.PadTup, DescriptiveComplexity.padTupF), which is how an element encoding a second-order atom R (x_{f 0}, …) is pinned down.

Formula builders are parameterized by maps Fin D → γ selecting the free variables holding each tuple, so that they can be instantiated at the variable types of the defining formulas of an interpretation (Fin 1 × Fin D, Fin 2 × Fin D).

Clients: the Tseitin encoding of DescriptiveComplexity.Problems.Sat.Tseitin and the Horn discharge of DescriptiveComplexity.Problems.HornSat.Hardness.

Finite conjunctions and disjunctions of formulas

def DescriptiveComplexity.listInf {L' : FirstOrder.Language} {γ : Type} : List (L'.Formula γ) → L'.Formula γ

Finite conjunction of a list of formulas.

Equations

• DescriptiveComplexity.listInf [] = ⊤
• DescriptiveComplexity.listInf (φ :: l) = φ ⊓ DescriptiveComplexity.listInf l

def DescriptiveComplexity.listSup {L' : FirstOrder.Language} {γ : Type} : List (L'.Formula γ) → L'.Formula γ

Finite disjunction of a list of formulas.

Equations

• DescriptiveComplexity.listSup [] = ⊥
• DescriptiveComplexity.listSup (φ :: l) = φ ⊔ DescriptiveComplexity.listSup l

theorem DescriptiveComplexity.realize_listInf {L' : FirstOrder.Language} {γ A : Type} [L'.Structure A] {v : γ → A} (l : List (L'.Formula γ)) : (listInf l).Realize v ↔ ∀ φ ∈ l, φ.Realize v

theorem DescriptiveComplexity.realize_listSup {L' : FirstOrder.Language} {γ A : Type} [L'.Structure A] {v : γ → A} (l : List (L'.Formula γ)) : (listSup l).Realize v ↔ ∃ φ ∈ l, φ.Realize v

Padded tuples

def DescriptiveComplexity.Canon {A : Type} {D : ℕ} [LE A] (m : ℕ) (u : Fin D → A) : Prop

A D-tuple is canonical at context length m: every coordinate from m on is a minimum of the order.

Equations

• DescriptiveComplexity.Canon m u = ∀ (j : Fin D), m ≤ ↑j → IsBot (u j)

def DescriptiveComplexity.Agree {A : Type} {D : ℕ} (m : ℕ) (u x : Fin D → A) : Prop

Two D-tuples agree below m.

Equations

• DescriptiveComplexity.Agree m u x = ∀ (j : Fin D), ↑j < m → x j = u j

def DescriptiveComplexity.pad {A : Type} {D : ℕ} (a₀ : A) {m : ℕ} (w : Fin m → A) : Fin D → A

Pad a context tuple to a D-tuple with a (minimal) element.

Equations

• DescriptiveComplexity.pad a₀ w j = if hj : ↑j < m then w ⟨↑j, hj⟩ else a₀

def DescriptiveComplexity.pref {A : Type} {D m : ℕ} (h : m ≤ D) (u : Fin D → A) : Fin m → A

The prefix of a D-tuple.

Equations

• DescriptiveComplexity.pref h u j = u (Fin.castLE h j)

theorem DescriptiveComplexity.pref_pad {A : Type} {D : ℕ} (a₀ : A) {m : ℕ} (h : m ≤ D) (w : Fin m → A) : pref h (pad a₀ w) = w

theorem DescriptiveComplexity.canon_pad {A : Type} {D : ℕ} [LE A] {a₀ : A} (h₀ : IsBot a₀) (m : ℕ) (w : Fin m → A) : Canon m (pad a₀ w)

theorem DescriptiveComplexity.agree_pad_pad {A : Type} {D : ℕ} (a₀ : A) {m : ℕ} (w : Fin m → A) (a : A) : Agree m (pad a₀ (Fin.snoc w a)) (pad a₀ w)

theorem DescriptiveComplexity.pad_pref_of_canon {A : Type} {D : ℕ} [PartialOrder A] {a₀ : A} (h₀ : IsBot a₀) {m : ℕ} (h : m ≤ D) {u : Fin D → A} (hc : Canon m u) : pad a₀ (pref h u) = u

A canonical tuple is the padding of its prefix.

theorem DescriptiveComplexity.eq_pad_of_canon_agree {A : Type} {D : ℕ} [PartialOrder A] {a₀ : A} (h₀ : IsBot a₀) {m : ℕ} (h : m ≤ D) {u x : Fin D → A} (hcx : Canon m x) (ha : Agree m u x) : x = pad a₀ (pref h u)

A tuple canonical at m agreeing with u below m is the padding of u's prefix.

theorem DescriptiveComplexity.pref_pad_snoc {A : Type} {D : ℕ} (a₀ : A) {m : ℕ} (h : m ≤ D) (w : Fin m → A) (a : A) : pref h (pad a₀ (Fin.snoc w a)) = w

theorem DescriptiveComplexity.agree_pad_snoc_pref {A : Type} {D : ℕ} (a₀ a : A) {m : ℕ} (h : m ≤ D) (u : Fin D → A) : Agree m u (pad a₀ (Fin.snoc (pref h u) a))

Tuples read through an index map

An interpretation encoding second-order atoms as elements needs one element per atom R (x_{f 0}, …, x_{f (m-1)}), whose coordinates are read from a context tuple u through an index map f. Canonical padding makes that element unique.

def DescriptiveComplexity.PadTup {A : Type} {D : ℕ} [LE A] {m : ℕ} (f : Fin m → Fin D) (u x : Fin D → A) : Prop

x is the canonically padded, length-m tuple read from u through the index map f.

Equations

• DescriptiveComplexity.PadTup f u x = (DescriptiveComplexity.Canon m x ∧ ∀ (j : Fin D) (hj : ↑j < m), x j = u (f ⟨↑j, hj⟩))

theorem DescriptiveComplexity.padTup_pad {A : Type} {D : ℕ} [LE A] {a₀ : A} (h₀ : IsBot a₀) {m : ℕ} (f : Fin m → Fin D) (u : Fin D → A) : PadTup f u (pad a₀ fun (j : Fin m) => u (f j))

The canonical padding of the tuple read through f does satisfy DescriptiveComplexity.PadTup.

theorem DescriptiveComplexity.eq_pad_of_padTup {A : Type} {D : ℕ} [PartialOrder A] {a₀ : A} (h₀ : IsBot a₀) {m : ℕ} {f : Fin m → Fin D} {u x : Fin D → A} (h : PadTup f u x) : x = pad a₀ fun (j : Fin m) => u (f j)

Conversely, a tuple satisfying DescriptiveComplexity.PadTup is that canonical padding: the element encoding an atom is unique.

theorem DescriptiveComplexity.eq_pad_snoc_of_canon_agree {A : Type} {D : ℕ} [PartialOrder A] {a₀ : A} (h₀ : IsBot a₀) {m : ℕ} (h : m < D) {u x : Fin D → A} (hcx : Canon (m + 1) x) (ha : Agree m u x) : x = pad a₀ (Fin.snoc (pref ⋯ u) (x ⟨m, h⟩))

A tuple canonical at m + 1 agreeing below m with u is the padding of the prefix of u extended by its own coordinate m.

noncomputable def DescriptiveComplexity.botF {L : FirstOrder.Language} {γ : Type} (x : γ) : (L.sum FirstOrder.Language.order).Formula γ

x is a minimum of the order, as a formula.

Equations

• DescriptiveComplexity.botF x = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.leSymb.formula₂ (FirstOrder.Language.var (Sum.inl x)) (FirstOrder.Language.var (Sum.inr 0)))

noncomputable def DescriptiveComplexity.canonF {L : FirstOrder.Language} {γ : Type} {D : ℕ} (m : ℕ) (c : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The coordinates of c from m on are minima, as a formula: c holds a canonically padded context tuple of length m.

Equations

• DescriptiveComplexity.canonF m c = DescriptiveComplexity.listInf (List.map (fun (j : Fin D) => if m ≤ ↑j then DescriptiveComplexity.botF (c j) else ⊤) (List.finRange D))

def DescriptiveComplexity.eqTupF {L : FirstOrder.Language} {γ : Type} {D : ℕ} (u x : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The tuples held by u and x are equal, as a formula.

Equations

• DescriptiveComplexity.eqTupF u x = DescriptiveComplexity.listInf (List.map (fun (j : Fin D) => (FirstOrder.Language.var (x j)).equal (FirstOrder.Language.var (u j))) (List.finRange D))

def DescriptiveComplexity.agreeF {L : FirstOrder.Language} {γ : Type} {D : ℕ} (m : ℕ) (u x : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The tuples held by u and x agree below m, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.padTupF {L : FirstOrder.Language} {γ : Type} {D m : ℕ} (f : Fin m → Fin D) (u x : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The tuple held by x is the canonically padded, length-m tuple read from u through the index map f, as a formula.

Equations

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

Realization of the builders

@[simp]

theorem DescriptiveComplexity.realize_botF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {x : γ} : (botF x).Realize v ↔ IsBot (v x)

@[simp]

theorem DescriptiveComplexity.realize_canonF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {m : ℕ} {c : Fin D → γ} : (canonF m c).Realize v ↔ Canon m fun (j : Fin D) => v (c j)

@[simp]

theorem DescriptiveComplexity.realize_eqTupF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {u x : Fin D → γ} : (eqTupF u x).Realize v ↔ (fun (j : Fin D) => v (x j)) = fun (j : Fin D) => v (u j)

@[simp]

theorem DescriptiveComplexity.realize_agreeF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {m : ℕ} {u x : Fin D → γ} : (agreeF m u x).Realize v ↔ Agree m (fun (j : Fin D) => v (u j)) fun (j : Fin D) => v (x j)

@[simp]

theorem DescriptiveComplexity.realize_padTupF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {m : ℕ} {f : Fin m → Fin D} {u x : Fin D → γ} : (padTupF f u x).Realize v ↔ PadTup f (fun (j : Fin D) => v (u j)) fun (j : Fin D) => v (x j)