Shared scaffolding of the clausal discharges

The clausal fragments of existential second-order logic – SO-Horn (DescriptiveComplexity.SecondOrderHorn) and SO-Krom (DescriptiveComplexity.SecondOrderKrom) – have discharges of the same shape: a program is translated, inside an ordered input structure, into a CNF instance whose propositional variables are the second-order atoms and whose clauses are the instances of the program's clauses whose guard holds (DescriptiveComplexity.Problems.HornSat.Hardness, DescriptiveComplexity.Problems.TwoSat.Hardness). Only the literals differ: a head and a body list on the Horn side, two signed slots on the Krom side.

Everything that does not depend on that difference is here:

• DescriptiveComplexity.clauseDim: the dimension of the interpretation, wide enough for the k universally quantified variables of the program and for every argument tuple of a relation variable of the block;
• DescriptiveComplexity.ClauseTag: the tags – one per clause of the program, one per relation variable of the block, plus a junk tag keeping the tag type nonempty;
• DescriptiveComplexity.guardF, DescriptiveComplexity.atomOccF: the defining formula of a clause's guard, and the formula saying that a coordinate tuple holds the canonically padded (DescriptiveComplexity.Padding) argument tuple of a second-order atom – the two building blocks of every defining formula of such a discharge, with their realization lemmas.

Dimension and tags

noncomputable def DescriptiveComplexity.clauseDim (B : SOBlock) (k : ℕ) : ℕ

The dimension of a clausal discharge: large enough for the k universally quantified first-order variables of the program and for every argument tuple of a relation variable of the block.

Equations

• DescriptiveComplexity.clauseDim B k = max k (DescriptiveComplexity.blockArityBound B)

theorem DescriptiveComplexity.le_clauseDim {B : SOBlock} {k : ℕ} : k ≤ clauseDim B k

theorem DescriptiveComplexity.arity_le_clauseDim {B : SOBlock} {k : ℕ} (i : B.ι) : B.arity i ≤ clauseDim B k

@[reducible, inline]

abbrev DescriptiveComplexity.ClauseTag (m : ℕ) (B : SOBlock) : Type

The tags of a clausal discharge of a program with m clauses: one per clause, one per relation variable of the block, plus a junk tag keeping the tag type nonempty when the program has no clause and the block no variable (its elements are neither clauses nor literals).

Equations

• DescriptiveComplexity.ClauseTag m B = ((Fin m ⊕ B.ι) ⊕ Unit)

@[reducible, inline]

abbrev DescriptiveComplexity.clTag {m : ℕ} {B : SOBlock} (c : Fin m) : ClauseTag m B

The tag of the clauses coming from the c-th clause of the program.

Equations

• DescriptiveComplexity.clTag c = Sum.inl (Sum.inl c)

@[reducible, inline]

abbrev DescriptiveComplexity.varTag {m : ℕ} {B : SOBlock} (i : B.ι) : ClauseTag m B

The tag of the propositional variables standing for the atoms of the relation variable i.

Equations

• DescriptiveComplexity.varTag i = Sum.inl (Sum.inr i)

noncomputable def DescriptiveComplexity.atomIdx {B : SOBlock} {k : ℕ} (a : SOAtom B k) : Fin (B.arity a.idx) → Fin (clauseDim B k)

The arguments of a second-order atom, as coordinates of the clause tuple.

Equations

• DescriptiveComplexity.atomIdx a j = Fin.castLE ⋯ (a.args j)

The two defining formulas

noncomputable def DescriptiveComplexity.guardF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (φ : (L.sum FirstOrder.Language.order).Formula (Fin k)) (u : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The guard of a clause, reading its variables off the coordinates selected by u.

Equations

• DescriptiveComplexity.guardF φ u = FirstOrder.Language.Formula.relabel (fun (j : Fin k) => u (Fin.castLE ⋯ j)) φ

noncomputable def DescriptiveComplexity.atomOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (a : SOAtom B k) (u x : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The occurrence formula of a second-order atom: the coordinates selected by x hold the canonically padded tuple of the atom's arguments, read off the coordinates selected by u.

Equations

• DescriptiveComplexity.atomOccF a u x = DescriptiveComplexity.padTupF (DescriptiveComplexity.atomIdx a) u x

theorem DescriptiveComplexity.realize_guardF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {φ : (L.sum FirstOrder.Language.order).Formula (Fin k)} {u : Fin (clauseDim B k) → γ} : (guardF φ u).Realize v ↔ φ.Realize fun (j : Fin k) => v (u (Fin.castLE ⋯ j))

theorem DescriptiveComplexity.realize_atomOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {a : SOAtom B k} {u x : Fin (clauseDim B k) → γ} : (atomOccF a u x).Realize v ↔ PadTup (atomIdx a) (fun (j : Fin (clauseDim B k)) => v (u j)) fun (j : Fin (clauseDim B k)) => v (x j)