Verified Encodings

This file defines VEncCNF, the main type for building verified encodings to CNF. This augments the regular EncCNF with the ability to specify and verify what a particular EncCNF value actually encodes.

def Trestle.Encode.EncCNF.encodesProp {ν α : Type u_1} (e : EncCNF ν α) (P : Model.PropPred ν) : Prop

e encodes proposition P

Equations

• e.encodesProp P = Trestle.Encode.EncCNF.encodesProp.aux P ↑e

def Trestle.Encode.EncCNF.encodesProp.aux {ν α : Type u_1} (P : Model.PropPred ν) (e' : StateM (LawfulState ν) α) : Prop

Equations

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

theorem Trestle.Encode.EncCNF.encodesProp_equisatisfiable {ν α : Type u_1} [IndexType ν] [LawfulIndexType ν] (e : EncCNF ν α) (P : Model.PropPred ν) (h : e.encodesProp P) : (∃ (τ : Model.PropAssignment ν), τ ⊨ P) ↔ ∃ (τ : Model.PropAssignment IVar), τ ⊨ Cnf.toPropFun e.toICnf

If e encodes P, then P is satisfiable iff e.toICnf is satisfiable

theorem Trestle.Encode.EncCNF.bind_encodesProp {ν α β : Type u_1} {P Q : Model.PropPred ν} (e1 : EncCNF ν α) (f : α → EncCNF ν β) : e1.encodesProp P → (∀ (s : LawfulState ν), (f (↑e1 s).1).encodesProp Q) → (e1 >>= f).encodesProp (P ⊓ Q)

@[simp]

theorem Trestle.Encode.EncCNF.encodesProp_pure {α ν : Type u_1} (a : α) : (pure a).encodesProp ⊤

theorem Trestle.Encode.EncCNF.encodesProp_map {ν α β : Type u_1} {P : Model.PropPred ν} (e1 : EncCNF ν α) (f : α → β) : (f <$> e1).encodesProp P ↔ e1.encodesProp P

def Trestle.Encode.VEncCNF (ν α : Type u) (P : Model.PropPred ν) : Type u

The verified encoding monad.

Equations

• Trestle.Encode.VEncCNF ν α P = { e : Trestle.Encode.EncCNF ν α // e.encodesProp P }

instance Trestle.Encode.VEncCNF.instCoeHeadEncCNF {ν α : Type u_1} {P : Model.PropPred ν} : CoeHead (VEncCNF ν α P) (EncCNF ν α)

Equations

• Trestle.Encode.VEncCNF.instCoeHeadEncCNF = { coe := fun (x : Trestle.Encode.VEncCNF ν α P) => ↑x }

theorem Trestle.Encode.VEncCNF.toICnf_equisatisfiable {ν α : Type u_1} {P : Model.PropPred ν} [IndexType ν] [LawfulIndexType ν] (v : VEncCNF ν α P) : (∃ (τ : Model.PropAssignment IVar), τ ⊨ Cnf.toPropFun (↑v).toICnf) ↔ ∃ (τ : Model.PropAssignment ν), τ ⊨ P

def Trestle.Encode.VEncCNF.mapProp {ν α : Type u_1} {P P' : Model.PropPred ν} (h : P = P') : VEncCNF ν α P → VEncCNF ν α P'

Equations

• Trestle.Encode.VEncCNF.mapProp h ⟨e, he⟩ = ⟨e, ⋯⟩

def Trestle.Encode.VEncCNF.newCtx {ν α : Type} {P : Model.PropPred ν} (name : String) (inner : VEncCNF ν α P) : VEncCNF ν α P

Equations

• Trestle.Encode.VEncCNF.newCtx name inner = ⟨Trestle.Encode.EncCNF.newCtx name ↑inner, ⋯⟩

def Trestle.Encode.VEncCNF.pure {α ν : Type u_1} (a : α) : VEncCNF ν α ⊤

Equations

• Trestle.Encode.VEncCNF.pure a = ⟨pure a, ⋯⟩

def Trestle.Encode.VEncCNF.addClause {ν : Type} (C : Clause (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ C.toPropFun

Equations

• Trestle.Encode.VEncCNF.addClause C = ⟨Trestle.Encode.EncCNF.addClause C, ⋯⟩

def Trestle.Encode.VEncCNF.unit {ν : Type} (l : Literal ν) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ LitVar.toPropFun l

Equations

• Trestle.Encode.VEncCNF.unit l = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.addClause #[l])

@[inline]

def Trestle.Encode.VEncCNF.withTemps {ν α : Type (max u_1 u_2)} (ι : Type u_2) [IndexType ι] [LawfulIndexType ι] {P : Model.PropAssignment (ν ⊕ ι) → Prop} (ve : VEncCNF (ν ⊕ ι) α P) (names : Option (ι → String) := none) : VEncCNF ν α fun (τ : Model.PropAssignment ν) => ∃ (σ : Model.PropAssignment (ν ⊕ ι)), τ = Model.PropAssignment.map Sum.inl σ ∧ P σ

Equations

• Trestle.Encode.VEncCNF.withTemps ι ve names = ⟨Trestle.Encode.EncCNF.withTemps ι (↑ve) names, ⋯⟩

def Trestle.Encode.VEncCNF.bind {ν α : Type u_1} {P : Model.PropPred ν} {β : Type u_1} {Q : Model.PropPred ν} (e1 : VEncCNF ν α P) (e2 : α → VEncCNF ν β Q) : VEncCNF ν β (P ⊓ Q)

Equations

• e1.bind e2 = Trestle.Encode.VEncCNF.mapProp ⋯ ⟨do let a ← ↑e1 let __do_lift ← ↑(e2 a) pure __do_lift, ⋯⟩

def Trestle.Encode.VEncCNF.seq {ν : Type} {P : Model.PropPred ν} {β : Type} {Q : Model.PropPred ν} (e1 : VEncCNF ν Unit P) (e2 : VEncCNF ν β Q) : VEncCNF ν β fun (τ : Model.PropAssignment ν) => P τ ∧ Q τ

Sequences two encodings together, i.e. a conjunction of the encodings.

For sequencing many encodings together, see seq[ ... ] syntax

Equations

• e1.seq e2 = e1.bind fun (x : Unit) => e2

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

Equations

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

@[inline]

def Trestle.Encode.VEncCNF.for_all {α : Type u_1} {ν : Type} (arr : Array α) {P : α → Model.PropPred ν} (f : (a : α) → VEncCNF ν Unit (P a)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => ∀ a ∈ arr, P a τ

Equations

• Trestle.Encode.VEncCNF.for_all arr f = ⟨Array.foldlM (fun (x : Unit) (x : α) => ↑(f x)) () arr, ⋯⟩

def Trestle.Encode.VEncCNF.guard {ν : Type} (p : Prop) [Decidable p] {P : p → Model.PropPred ν} (f : (h : p) → VEncCNF ν Unit (P h)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => ∀ (h : p), P h τ

Equations

• Trestle.Encode.VEncCNF.guard p f = ⟨if h : p then ↑(f h) else pure PUnit.unit, ⋯⟩

def Trestle.Encode.VEncCNF.ite {ν : Type} (p : Prop) [Decidable p] {P : p → Model.PropPred ν} {Q : ¬p → Model.PropPred ν} (f : (h : p) → VEncCNF ν Unit (P h)) (g : (h : ¬p) → VEncCNF ν Unit (Q h)) : VEncCNF ν Unit (if h : p then P h else Q h)

Equations

• Trestle.Encode.VEncCNF.ite p f g = ⟨if h : p then ↑(f h) else ↑(g h), ⋯⟩

def Trestle.Encode.VEncCNF.andImplyOr {ν : Type} (hyps conc : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => (∀ h ∈ hyps, τ ⊨ LitVar.toPropFun h) → ∃ c ∈ conc, τ ⊨ LitVar.toPropFun c

Equations

• Trestle.Encode.VEncCNF.andImplyOr hyps conc = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.addClause (Array.map Trestle.LitVar.negate hyps ++ conc))

def Trestle.Encode.VEncCNF.andImply {ν : Type} (hyps : Array (Literal ν)) (conc : Literal ν) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => (∀ h ∈ hyps, τ ⊨ LitVar.toPropFun h) → τ ⊨ LitVar.toPropFun conc

Equations

• Trestle.Encode.VEncCNF.andImply hyps conc = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.andImplyOr hyps #[conc])

def Trestle.Encode.VEncCNF.implyOr {ν : Type} (hyp : Literal ν) (conc : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ LitVar.toPropFun hyp → ∃ c ∈ conc, τ ⊨ LitVar.toPropFun c

Equations

• Trestle.Encode.VEncCNF.implyOr hyp conc = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.andImplyOr #[hyp] conc)

def Trestle.Encode.VEncCNF.orImplyOr {ν : Type} (hyps conc : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => (∃ h ∈ hyps, τ ⊨ LitVar.toPropFun h) → ∃ c ∈ conc, τ ⊨ LitVar.toPropFun c

Equations

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

def Trestle.Encode.VEncCNF.orImply {ν : Type} (hyps : Array (Literal ν)) (conc : Literal ν) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => (∃ h ∈ hyps, τ ⊨ LitVar.toPropFun h) → τ ⊨ LitVar.toPropFun conc

Equations

• Trestle.Encode.VEncCNF.orImply hyps conc = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.orImplyOr hyps #[conc])

def Trestle.Encode.VEncCNF.andImplyAnd {ν : Type} (hyps concs : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => (∀ h ∈ hyps, τ ⊨ LitVar.toPropFun h) → ∀ c ∈ concs, τ ⊨ LitVar.toPropFun c

Equations

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

def Trestle.Encode.VEncCNF.implyAnd {ν : Type} (hyp : Literal ν) (concs : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ LitVar.toPropFun hyp → ∀ c ∈ concs, τ ⊨ LitVar.toPropFun c

Equations

• Trestle.Encode.VEncCNF.implyAnd hyp concs = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.andImplyAnd #[hyp] concs)

def Trestle.Encode.VEncCNF.orImplyAnd {ν : Type} (hyps concs : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => (∃ h ∈ hyps, τ ⊨ LitVar.toPropFun h) → ∀ c ∈ concs, τ ⊨ LitVar.toPropFun c

Equations

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

def Trestle.Encode.VEncCNF.imply {ν : Type} (v1 v2 : Literal ν) : VEncCNF ν Unit fun (x : Model.PropAssignment ν) => x ⊨ LitVar.toPropFun v1 ⇨ LitVar.toPropFun v2

Equations

• Trestle.Encode.VEncCNF.imply v1 v2 = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.andImplyOr #[v1] #[v2])

def Trestle.Encode.VEncCNF.biImpl {ν : Type} (v1 v2 : Literal ν) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ LitVar.toPropFun v1 ↔ τ ⊨ LitVar.toPropFun v2

Equations

• Trestle.Encode.VEncCNF.biImpl v1 v2 = Trestle.Encode.VEncCNF.mapProp ⋯ ((Trestle.Encode.VEncCNF.imply v1 v2).seq (Trestle.Encode.VEncCNF.imply v2 v1))

def Trestle.Encode.VEncCNF.defConj {ν : Type} (v : Literal ν) (vs : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ LitVar.toPropFun v ↔ ∀ v ∈ vs, τ ⊨ LitVar.toPropFun v

Equations

• Trestle.Encode.VEncCNF.defConj v vs = Trestle.Encode.VEncCNF.mapProp ⋯ ((Trestle.Encode.VEncCNF.implyAnd v vs).seq (Trestle.Encode.VEncCNF.andImply vs v))

def Trestle.Encode.VEncCNF.defDisj {ν : Type} (v : Literal ν) (vs : Array (Literal ν)) : VEncCNF ν Unit fun (τ : Model.PropAssignment ν) => τ ⊨ LitVar.toPropFun v ↔ ∃ v ∈ vs, τ ⊨ LitVar.toPropFun v

Equations

• Trestle.Encode.VEncCNF.defDisj v vs = Trestle.Encode.VEncCNF.mapProp ⋯ ((Trestle.Encode.VEncCNF.implyOr v vs).seq (Trestle.Encode.VEncCNF.orImply vs v))

def Trestle.Encode.VEncCNF.castVar {ν₁ ν₂ α : Type u_1} {P : Model.PropPred ν₁} (h : ν₁ = ν₂) (ve : VEncCNF ν₁ α P) : VEncCNF ν₂ α (h ▸ P)

Equations

• Trestle.Encode.VEncCNF.castVar h ⟨e, he⟩ = ⟨h ▸ e, ⋯⟩