Trestle.Data.LitVar.Basic

Basic theorems about literals and variables.

source

def Trestle.LitVar.toPropForm {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

Model.PropForm ν

Equations

Trestle.LitVar.toPropForm l = if Trestle.LitVar.polarity l = true then Trestle.Model.PropForm.var (Trestle.LitVar.toVar l) else (Trestle.Model.PropForm.var (Trestle.LitVar.toVar l)).neg

Instances For

source

instance Trestle.LitVar.instCoeHeadPropForm {L : Type u} {ν : Type v} [LitVar L ν] :

CoeHead L (Model.PropForm ν)

Equations

Trestle.LitVar.instCoeHeadPropForm = { coe := Trestle.LitVar.toPropForm }

source

def Trestle.LitVar.toPropFun {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

Model.PropFun ν

Equations

Trestle.LitVar.toPropFun l = if Trestle.LitVar.polarity l = true then Trestle.Model.PropFun.var (Trestle.LitVar.toVar l) else (Trestle.Model.PropFun.var (Trestle.LitVar.toVar l))ᶜ

Instances For

source

instance Trestle.LitVar.instCoeHeadPropFun {L : Type u} {ν : Type v} [LitVar L ν] :

CoeHead L (Model.PropFun ν)

Equations

Trestle.LitVar.instCoeHeadPropFun = { coe := Trestle.LitVar.toPropFun }

source

theorem Trestle.LitVar.satisfies_iff {L : Type u} {ν : Type v} [LitVar L ν] {τ : Model.PropAssignment ν} {l : L} :

τ ⊨ toPropFun l ↔ τ (toVar l) = polarity l

source

@[simp]

theorem Trestle.LitVar.toPropFun_lit_ne_bot {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

toPropFun l ≠ ⊥

source

@[simp]

theorem Trestle.LitVar.bot_ne_toPropFun_lit {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

⊥ ≠ toPropFun l

source

@[simp]

theorem Trestle.LitVar.toPropFun_lit_ne_top {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

toPropFun l ≠ ⊤

source

@[simp]

theorem Trestle.LitVar.top_ne_toPropFun_lit {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

⊤ ≠ toPropFun l

source

@[simp]

theorem Trestle.LitVar.mk_toPropForm {L : Type u} {ν : Type v} [LitVar L ν] (l : L) :

⟦toPropForm l⟧ = toPropFun l

source

@[simp]

theorem Trestle.LitVar.vars_toPropForm {L : Type u} {ν : Type v} [LitVar L ν] [DecidableEq ν] (l : L) :

(toPropForm l).vars = {toVar l}

source

@[simp]

theorem Trestle.LitVar.semVars_toPropFun {L : Type u} {ν : Type v} [LitVar L ν] [DecidableEq ν] (l : L) :

(toPropFun l).semVars = {toVar l}

source

@[simp]

theorem Trestle.LitVar.var_mkLit {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) (p : Bool) :

toVar (mkLit L x p) = x

source

@[simp]

theorem Trestle.LitVar.polarity_mkLit {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) (p : Bool) :

polarity (mkLit L x p) = p

source

@[simp]

theorem Trestle.LitVar.eta {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l : L) :

mkLit L (toVar l) (polarity l) = l

source

@[simp]

theorem Trestle.LitVar.eta_neg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l : L) :

(mkLit L (toVar l) !polarity l) = -l

source

theorem Trestle.LitVar.mkPos_or_mkNeg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l : L) :

l = mkPos (toVar l) ∨ l = mkNeg (toVar l)

source

theorem Trestle.LitVar.exists_mkPos_or_mkNeg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l : L) :

∃ (v : ν), l = mkPos v ∨ l = mkNeg v

source

@[simp]

theorem Trestle.LitVar.mkPos_ne_mkNeg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {v₁ v₂ : ν} :

mkPos v₁ ≠ mkNeg v₂

source

@[simp]

theorem Trestle.LitVar.mkNeg_ne_mkPos {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {v₁ v₂ : ν} :

mkNeg v₁ ≠ mkPos v₂

source

@[simp]

theorem Trestle.LitVar.mkPos_inj {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {x y : ν} :

mkPos x = mkPos y ↔ x = y

source

@[simp]

theorem Trestle.LitVar.mkNeg_inj {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {x y : ν} :

mkNeg x = mkNeg y ↔ x = y

source

@[simp]

theorem Trestle.LitVar.toPropForm_mkPos {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) :

toPropForm (mkPos x) = Model.PropForm.var x

source

@[simp]

theorem Trestle.LitVar.toPropForm_mkNeg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) :

toPropForm (mkNeg x) = (Model.PropForm.var x).neg

source

@[simp]

theorem Trestle.LitVar.toPropFun_mkPos {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) :

toPropFun (mkPos x) = Model.PropFun.var x

source

@[simp]

theorem Trestle.LitVar.toPropFun_mkNeg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) :

toPropFun (mkNeg x) = (Model.PropFun.var x)ᶜ

source

@[simp]

theorem Trestle.LitVar.toPropFun_mkLit_true {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {v : ν} :

toPropFun (mkLit L v true) = Model.PropFun.var v

source

@[simp]

theorem Trestle.LitVar.toPropFun_mkLit_false {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {v : ν} :

toPropFun (mkLit L v false) = (Model.PropFun.var v)ᶜ

source

@[simp]

theorem Trestle.LitVar.toPropFun_neg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l : L) :

toPropFun (-l) = (toPropFun l)ᶜ

source

theorem Trestle.LitVar.ext_iff {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l1 l2 : L) :

l1 = l2 ↔ toVar l1 = toVar l2 ∧ polarity l1 = polarity l2

source

@[simp]

theorem Trestle.LitVar.neg_eq_neg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l1 l2 : L) :

-l1 = -l2 ↔ l1 = l2

source

@[simp]

theorem Trestle.LitVar.neg_neg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (l : L) :

- -l = l

source

@[simp]

theorem Trestle.LitVar.neg_mkPos {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) :

-mkPos x = mkNeg x

source

@[simp]

theorem Trestle.LitVar.neg_mkNeg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] (x : ν) :

-mkNeg x = mkPos x

source

theorem Trestle.LitVar.neg_eq_iff_eq_neg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {x y : L} :

-x = y ↔ x = -y

source

theorem Trestle.LitVar.toVar_eq_iff {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {l₁ l₂ : L} :

toVar l₁ = toVar l₂ ↔ l₁ = l₂ ∨ l₁ = -l₂

source

theorem Trestle.LitVar.toVar_eq_iff' {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {l₁ l₂ : L} :

toVar l₁ = toVar l₂ ↔ l₁ = l₂ ∨ -l₁ = l₂

source

theorem Trestle.LitVar.satisfies_neg {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] {τ : Model.PropAssignment ν} {l : L} :

τ ⊨ toPropFun (-l) ↔ (fun (M : Model.PropAssignment ν) (φ : Model.PropFun ν) => ¬M ⊨ φ) τ (toPropFun l)

source

theorem Trestle.LitVar.satisfies_set {L : Type u} {ν : Type v} [LitVar L ν] [DecidableEq ν] (τ : Model.PropAssignment ν) (l : L) :

τ.set (toVar l) (polarity l) ⊨ toPropFun l

source

theorem Trestle.LitVar.eq_of_flip {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] [DecidableEq ν] {τ : Model.PropAssignment ν} {l : L} {x : ν} {p : Bool} :

(fun (M : Model.PropAssignment ν) (φ : Model.PropFun ν) => ¬M ⊨ φ) τ (toPropFun l) → τ.set x p ⊨ toPropFun l → l = mkLit L x p

source

theorem Trestle.LitVar.eq_of_flip' {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] [DecidableEq ν] {τ : Model.PropAssignment ν} {l : L} {x : ν} {p : Bool} :

τ ⊨ toPropFun l → (fun (M : Model.PropAssignment ν) (φ : Model.PropFun ν) => ¬M ⊨ φ) (τ.set x p) (toPropFun l) → l = mkLit L x !p

source

theorem Trestle.LitVar.toPropFun.inj {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] [DecidableEq ν] :

Function.Injective toPropFun

source

@[simp]

theorem Trestle.LitVar.toPropFun_lit_eq_lit_iff {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] [DecidableEq ν] {l₁ l₂ : L} :

toPropFun l₁ = toPropFun l₂ ↔ l₁ = l₂

source

@[simp]

theorem Trestle.LitVar.toPropFun_lit_eq_var_iff {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] [DecidableEq ν] (l : L) (v : ν) :

toPropFun l = Model.PropFun.var v ↔ l = mkPos v

source

@[simp]

theorem Trestle.LitVar.var_eq_toPropFun_iff {L : Type u} {ν : Type v} [LitVar L ν] [LawfulLitVar L ν] [DecidableEq ν] (l : L) (v : ν) :

Model.PropFun.var v = toPropFun l ↔ l = mkPos v

map #

source

@[simp]

theorem Trestle.LitVar.satisfies_map {L : Type u} {V : Type u_1} {L' : Type u_2} {V' : Type u_3} [LitVar L V] [LitVar L' V'] [LawfulLitVar L' V'] (f : V → V') (l : L) (τ : Model.PropAssignment V') :

τ ⊨ toPropFun (map f l) ↔ Model.PropAssignment.map f τ ⊨ toPropFun l

source

@[simp]

theorem Trestle.LitVar.toPropFun_map {L : Type u} {V : Type u_1} {L' : Type u_2} {V' : Type u_3} [LitVar L V] [LitVar L' V'] [LawfulLitVar L' V'] (f : V → V') (l : L) :

toPropFun (map f l) = Model.PropFun.map f (toPropFun l)

Sums as valid literals #

source

instance Trestle.LitVar.instLawfulLitVarSum {L1 : Type u_1} {V1 : Type u_2} {L2 : Type u_3} {V2 : Type u_4} [LitVar L1 V1] [LitVar L2 V2] [LawfulLitVar L1 V1] [LawfulLitVar L2 V2] :

LawfulLitVar (L1 ⊕ L2) (V1 ⊕ V2)

source

@[simp]

theorem Trestle.LitVar.polarity_inl {L1 : Type u_2} {V1 : Type u_4} {L2 : Type u_1} {V2 : Type u_3} [LitVar L1 V1] [LitVar L2 V2] (l : L1) :

polarity (Sum.inl l) = polarity l

source

@[simp]

theorem Trestle.LitVar.polarity_inr {L1 : Type u_2} {V1 : Type u_4} {L2 : Type u_1} {V2 : Type u_3} [LitVar L1 V1] [LitVar L2 V2] (l : L2) :

polarity (Sum.inr l) = polarity l

source

@[simp]

theorem Trestle.LitVar.toVar_inl {L1 : Type u_4} {V1 : Type u_1} {L2 : Type u_3} {V2 : Type u_2} [LitVar L1 V1] [LitVar L2 V2] (l : L1) :

toVar (Sum.inl l) = Sum.inl (toVar l)

source

@[simp]

theorem Trestle.LitVar.toVar_inr {L1 : Type u_4} {V1 : Type u_1} {L2 : Type u_3} {V2 : Type u_2} [LitVar L1 V1] [LitVar L2 V2] (l : L2) :

toVar (Sum.inr l) = Sum.inr (toVar l)