Tseitin Transform

This file implements a lightly optimized Tseitin encoding of arbitrary PropForm formulas into CNF.

The formula is put into negation normal form first, and top-level ∧ / top-level ∨ are collected into one formula/clause respectively.

inductive Trestle.Encode.Tseitin.NegNormForm (ν : Type u) : Type u

• all {ν : Type u} (as : Array (NegNormForm ν)) : NegNormForm ν
• any {ν : Type u} (as : Array (NegNormForm ν)) : NegNormForm ν
• lit {ν : Type u} (l : Literal ν) : NegNormForm ν

instance Trestle.Encode.Tseitin.instReprNegNormForm {ν✝ : Type u_1} [Repr ν✝] : Repr (NegNormForm ν✝)

Equations

• Trestle.Encode.Tseitin.instReprNegNormForm = { reprPrec := Trestle.Encode.Tseitin.reprNegNormForm✝ }

@[irreducible]

def Trestle.Encode.Tseitin.NegNormForm.toPropForm {ν : Type u_1} (r : NegNormForm ν) : Model.PropForm ν

Equations

• One or more equations did not get rendered due to their size.
• (Trestle.Encode.Tseitin.NegNormForm.lit a).toPropForm = Trestle.LitVar.toPropForm a

@[irreducible]

def Trestle.Encode.Tseitin.NegNormForm.toPropFun {ν : Type u_1} (r : NegNormForm ν) : Model.PropFun ν

Equations

• One or more equations did not get rendered due to their size.
• (Trestle.Encode.Tseitin.NegNormForm.lit a).toPropFun = Trestle.LitVar.toPropFun a

def Trestle.Encode.Tseitin.NegNormForm.const {ν : Type u_1} (val : Bool) : NegNormForm ν

Equations

• Trestle.Encode.Tseitin.NegNormForm.const true = Trestle.Encode.Tseitin.NegNormForm.all #[]
• Trestle.Encode.Tseitin.NegNormForm.const false = Trestle.Encode.Tseitin.NegNormForm.any #[]

@[simp]

theorem Trestle.Encode.Tseitin.NegNormForm.const_toPropFun {ν : Type u_1} {b : Bool} : (const b).toPropFun = if b = true then ⊤ else ⊥

def Trestle.Encode.Tseitin.NegNormForm.ofPropForm {ν : Type u_1} (neg : Bool) : Model.PropForm ν → NegNormForm ν

Equations

• One or more equations did not get rendered due to their size.
• Trestle.Encode.Tseitin.NegNormForm.ofPropForm neg Trestle.Model.PropForm.tr = Trestle.Encode.Tseitin.NegNormForm.const !neg
• Trestle.Encode.Tseitin.NegNormForm.ofPropForm neg Trestle.Model.PropForm.fls = Trestle.Encode.Tseitin.NegNormForm.const neg
• Trestle.Encode.Tseitin.NegNormForm.ofPropForm neg (Trestle.Model.PropForm.var v) = Trestle.Encode.Tseitin.NegNormForm.lit (Trestle.LitVar.mkLit (Trestle.Literal ν) v !neg)
• Trestle.Encode.Tseitin.NegNormForm.ofPropForm neg f.neg = Trestle.Encode.Tseitin.NegNormForm.ofPropForm (!neg) f

theorem Trestle.Encode.Tseitin.NegNormForm.toPropFun_ofPropForm {ν : Type u_1} {neg : Bool} (f : Model.PropForm ν) : (ofPropForm neg f).toPropFun = if neg = true then ⟦f.neg⟧ else ⟦f⟧

@[irreducible]

def Trestle.Encode.Tseitin.NegNormForm.conjuncts {ν : Type u_1} : NegNormForm ν → Array (NegNormForm ν)

Equations

• One or more equations did not get rendered due to their size.
• (Trestle.Encode.Tseitin.NegNormForm.lit l).conjuncts = #[Trestle.Encode.Tseitin.NegNormForm.lit l]

@[irreducible]

def Trestle.Encode.Tseitin.NegNormForm.disjuncts {ν : Type u_1} : NegNormForm ν → Array (NegNormForm ν)

Equations

• One or more equations did not get rendered due to their size.
• (Trestle.Encode.Tseitin.NegNormForm.lit l).disjuncts = #[Trestle.Encode.Tseitin.NegNormForm.lit l]

@[irreducible]

def Trestle.Encode.Tseitin.NegNormForm.toPropFun_all_conjuncts {ν : Type u_1} (f : NegNormForm ν) : (all f.conjuncts).toPropFun = f.toPropFun

Equations

• ⋯ = ⋯

@[irreducible]

def Trestle.Encode.Tseitin.NegNormForm.toPropFun_any_disjuncts {ν : Type u_1} (f : NegNormForm ν) : (any f.disjuncts).toPropFun = f.toPropFun

Equations

• ⋯ = ⋯

Take a formula f into

def Trestle.Encode.Tseitin.NegNormForm.normalize {ν : Type u_1} (f : NegNormForm ν) : Array (Array (NegNormForm ν))

Equations

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

theorem Trestle.Encode.Tseitin.NegNormForm.satisfies_normalize {ν : Type u_1} (τ : Model.PropAssignment ν) (f : NegNormForm ν) : τ ⊨ f.toPropFun ↔ ∀ c ∈ f.normalize, ∃ d ∈ c, τ ⊨ d.toPropFun

@[irreducible]

def Trestle.Encode.Tseitin.encodeNNF_mkDefs {ν' : Type u_1} {ν : Type} (fs : Array (NegNormForm ν')) (emb : ν' ↪ ν) : VEncCNF (ν ⊕ Fin fs.size) Unit fun (τ : Model.PropAssignment (ν ⊕ Fin fs.size)) => ∀ (i : Fin fs.size), τ (Sum.inr i) = true → Model.PropAssignment.map (Sum.inl ∘ ⇑emb) τ ⊨ fs[i].toPropFun

Equations

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

@[irreducible]

def Trestle.Encode.Tseitin.encodeNNF {ν : Type} {ν' : Type u_1} (t : ν) (emb : ν' ↪ ν) (f : NegNormForm ν') : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ t = true → τ ⊨ Model.PropFun.map (⇑emb) f.toPropFun

Tseitin encoding in the general case creates temporaries for each clause

Equations

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

def Trestle.Encode.Tseitin.encodeNNF_top_clause {ν : Type} (clause : Array (NegNormForm ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => ∃ f ∈ clause, τ ⊨ f.toPropFun

Equations

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

def Trestle.Encode.Tseitin.encodeNNF_top {ν : Type} (f : NegNormForm ν) : VEncCNF ν Unit fun (x : Model.PropAssignment ν) => x ⊨ f.toPropFun

Equations

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

@[noinline]

def Trestle.Encode.Tseitin.encode {V : Type} [DecidableEq V] (f : Model.PropForm V) : VEncCNF V Unit fun (x : Model.PropAssignment V) => x ⊨ f

Equations

• Trestle.Encode.Tseitin.encode f = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.Tseitin.encodeNNF_top (Trestle.Encode.Tseitin.NegNormForm.ofPropForm false f))

def Trestle.Encode.«termTseitin[_]» : Lean.ParserDescr

Equations

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

inductive Trestle.Encode.Example.V : Type

• p : V
• q : V
• r : V
• s : V
• t : V

instance Trestle.Encode.Example.instReprV : Repr V

Equations

• Trestle.Encode.Example.instReprV = { reprPrec := Trestle.Encode.Example.reprV✝ }

instance Trestle.Encode.Example.instIndexTypeV : IndexType V

Equations

• Trestle.Encode.Example.instIndexTypeV = Trestle.IndexType.ofEquiv Trestle.Encode.Example.V.proxyTypeEquiv

instance Trestle.Encode.Example.instLawfulIndexTypeV : LawfulIndexType V

def Trestle.Encode.Example.ex : Model.PropForm V

Equations

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