The implication graph of a Krom program

A Krom program, instantiated in a structure, is a 2-CNF: its propositional variables are the atoms of the block at tuples of elements (DescriptiveComplexity.KromImpl.KromAtom), and each clause of the program contributes one propositional clause per valuation of its universally quantified variables satisfying its guard (DescriptiveComplexity.KromImpl.clauseRel).

So the criterion of DescriptiveComplexity.TwoCnf applies, and gives the fact this file exists for:

(∃ ρ, prog.Holds ρ) ↔ no goal clause fires ∧ no literal reaches its own negation and back

(DescriptiveComplexity.KromImpl.exists_holds_iff). The first conjunct is the empty clause of the 2-CNF, which has no place in the abstract criterion and is therefore carried separately: a clause of the program with neither literal slot filled is guard → ⊥, and its firing makes the program unsatisfiable outright.

This is the Lean-level half of the converse translation from the Krom fragment to FO(TC): what remains after it is to express the implication graph as a DescriptiveComplexity.TCSpec, i.e. to build the transition formulas that walk it. The half proved here is where the mathematics is; the other half is formula plumbing.

The propositional variables

def DescriptiveComplexity.KromImpl.KromAtom (B : SOBlock) (A : Type) : Type

A propositional variable of the instantiated program: a relation variable of the block together with a tuple of elements.

Equations

• DescriptiveComplexity.KromImpl.KromAtom B A = ((i : B.ι) × (Fin (B.arity i) → A))

instance DescriptiveComplexity.KromImpl.instFiniteKromAtom {B : SOBlock} (A : Type) [Finite A] : Finite (KromAtom B A)

def DescriptiveComplexity.KromImpl.toAssign {B : SOBlock} {A : Type} (ν : KromAtom B A → Prop) : B.Assignment A

The block assignment described by a truth assignment of the propositional variables.

Equations

• DescriptiveComplexity.KromImpl.toAssign ν i x = ν ⟨i, x⟩

def DescriptiveComplexity.KromImpl.ofAssign {B : SOBlock} {A : Type} (ρ : B.Assignment A) : KromAtom B A → Prop

The truth assignment of the propositional variables described by a block assignment.

Equations

• DescriptiveComplexity.KromImpl.ofAssign ρ a = ρ a.fst a.snd

@[simp]

theorem DescriptiveComplexity.KromImpl.toAssign_ofAssign {B : SOBlock} {A : Type} (ρ : B.Assignment A) : toAssign (ofAssign ρ) = ρ

@[simp]

theorem DescriptiveComplexity.KromImpl.ofAssign_toAssign {B : SOBlock} {A : Type} (ν : KromAtom B A → Prop) : ofAssign (toAssign ν) = ν

theorem DescriptiveComplexity.KromImpl.eq_of_mem_option {α : Type} {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b

def DescriptiveComplexity.KromImpl.atomVar {B : SOBlock} {k : ℕ} {A : Type} (a : SOAtom B k) (v : Fin k → A) : KromAtom B A

The propositional variable an atom denotes at a valuation.

Equations

• DescriptiveComplexity.KromImpl.atomVar a v = ⟨a.idx, fun (j : Fin (B.arity a.idx)) => v (a.args j)⟩

def DescriptiveComplexity.KromImpl.litOf {B : SOBlock} {k : ℕ} {A : Type} (l : KromLit B k) (v : Fin k → A) : TwoCnf.Lit (KromAtom B A)

The literal a Krom literal denotes at a valuation.

Equations

• DescriptiveComplexity.KromImpl.litOf l v = (DescriptiveComplexity.KromImpl.atomVar l.atom v, l.positive)

theorem DescriptiveComplexity.KromImpl.holds_iff_litTrue {B : SOBlock} {k : ℕ} {A : Type} (l : KromLit B k) (ν : KromAtom B A → Prop) (v : Fin k → A) : l.Holds (toAssign ν) v ↔ TwoCnf.LitTrue ν (litOf l v)

The 2-CNF of a program

def DescriptiveComplexity.KromImpl.clauseRel {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (prog : KromProgram L B k) (p q : TwoCnf.Lit (KromAtom B A)) : Prop

The clauses of the instantiated program, as a 2-CNF in the sense of DescriptiveComplexity.TwoCnf: a clause of the program whose guard holds at some valuation contributes the disjunction of its two literals, read at that valuation. A unit clause contributes the disjunction of its literal with itself, which is what DescriptiveComplexity.TwoCnf expects.

Equations

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

def DescriptiveComplexity.KromImpl.edgePairs {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (c : KromClause L B k) : List (KromLit B k × KromLit B k)

The ordered pairs of literals a clause contributes to the implication graph: the clause ℓ₁ ∨ ℓ₂ gives the edges ¬ℓ₁ → ℓ₂ and ¬ℓ₂ → ℓ₁, and a unit clause ℓ the edge ¬ℓ → ℓ. The pair records the two clause literals, the edge running from the negation of the first to the second.

Equations

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

theorem DescriptiveComplexity.KromImpl.step_iff_edgePairs {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (prog : KromProgram L B k) (p q : TwoCnf.Lit (KromAtom B A)) : TwoCnf.Step (clauseRel prog) p q ↔ ∃ c ∈ prog, ∃ (v : Fin k → A), c.guard.Realize v ∧ ∃ pr ∈ edgePairs c, TwoCnf.neg p = litOf pr.1 v ∧ q = litOf pr.2 v

The implication graph, clause by clause: there is an edge from p to q exactly when some clause of the program, at some valuation satisfying its guard, contributes the pair whose first literal is the negation of p and whose second is q. The DescriptiveComplexity.TwoCnf.Step on the left is symmetric in the two literals of a clause, which is why the ordered pairs of DescriptiveComplexity.KromImpl.edgePairs suffice.

def DescriptiveComplexity.KromImpl.GoalFires {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram L B k) (A : Type) [L.Structure A] : Prop

Some goal clause of the program fires: a clause with neither literal slot filled whose guard holds. Such a clause is guard → ⊥, so the program is then unsatisfiable, a case the abstract criterion does not cover.

Equations

• DescriptiveComplexity.KromImpl.GoalFires prog A = ∃ c ∈ prog, ∃ (v : Fin k → A), c.guard.Realize v ∧ c.lit₁ = none ∧ c.lit₂ = none

theorem DescriptiveComplexity.KromImpl.holds_iff_satisfies {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (prog : KromProgram L B k) (ν : KromAtom B A → Prop) : prog.Holds (toAssign ν) ↔ TwoCnf.Satisfies (clauseRel prog) ν ∧ ¬GoalFires prog A

An assignment satisfies the program iff it satisfies the 2-CNF and no goal clause fires.

theorem DescriptiveComplexity.KromImpl.exists_holds_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (prog : KromProgram L B k) : (∃ (ρ : B.Assignment A), prog.Holds ρ) ↔ ¬GoalFires prog A ∧ ∀ (p : TwoCnf.Lit (KromAtom B A)), ¬(TwoCnf.Reach (clauseRel prog) p (TwoCnf.neg p) ∧ TwoCnf.Reach (clauseRel prog) (TwoCnf.neg p) p)

The criterion for a Krom program: it is satisfiable exactly when no goal clause fires and no literal of its implication graph reaches its own negation and back.