internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))
Tactic:
apply Or.inr
Proof state after:
case false.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
case false.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))
Tactic:
simp [mkLit]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Tactic:
apply Or.inl
Proof state after:
case true.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true))
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
case true.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true))
Tactic:
simp [mkLit]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropForm_mkPos
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
⊢ toPropForm (mkPos x) = PropForm.var x
Tactic:
simp [toPropForm]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropForm_mkNeg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
⊢ toPropForm (mkNeg x) = PropForm.neg (PropForm.var x)
Tactic:
simp [toPropForm]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.mk_toPropForm
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦toPropForm l⟧ = toPropFun l
Tactic:
dsimp [toPropForm, toPropFun]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))⟧ =
    if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ
Theorem: LeanSAT.LitVar.mk_toPropForm
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))⟧ =
    if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ
Tactic:
cases polarity l <;> simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun_mkPos
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
⊢ toPropFun (mkPos x) = PropFun.var x
Tactic:
simp [toPropFun]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun_mkNeg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
⊢ toPropFun (mkNeg x) = (PropFun.var x)ᶜ
Tactic:
simp [toPropFun]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun_mkLit_true
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
v : ν
⊢ toPropFun (mkLit L v true) = PropFun.var v
Tactic:
simp [toPropFun]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun_mkLit_false
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
v : ν
⊢ toPropFun (mkLit L v false) = (PropFun.var v)ᶜ
Tactic:
simp [toPropFun]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun_neg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ toPropFun (-l) = (toPropFun l)ᶜ
Tactic:
dsimp [toPropFun]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ (if polarity (-l) = true then PropFun.var (toVar (-l)) else (PropFun.var (toVar (-l)))ᶜ) =
    (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ)ᶜ
Theorem: LeanSAT.LitVar.toPropFun_neg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ (if polarity (-l) = true then PropFun.var (toVar (-l)) else (PropFun.var (toVar (-l)))ᶜ) =
    (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ)ᶜ
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.LitVar.ext_iff
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 ↔ toVar l1 = toVar l2 ∧ polarity l1 = polarity l2
Tactic:
constructor
Proof state after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2

case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar l1 = toVar l2 ∧ polarity l1 = polarity l2 → l1 = l2
Theorem: LeanSAT.LitVar.ext_iff
Proof state before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2
Tactic:
rintro rfl
Proof state after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ toVar l1 = toVar l1 ∧ polarity l1 = polarity l1
Theorem: LeanSAT.LitVar.ext_iff
Proof state before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ toVar l1 = toVar l1 ∧ polarity l1 = polarity l1
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.ext_iff
Proof state before:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar l1 = toVar l2 ∧ polarity l1 = polarity l2 → l1 = l2
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.LitVar.neg_eq_neg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 ↔ l1 = l2
Tactic:
constructor
Proof state after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 → l1 = l2

case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → -l1 = -l2
Theorem: LeanSAT.LitVar.neg_eq_neg
Proof state before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 → l1 = l2
Tactic:
rw [ext_iff, ext_iff (L := L)]
Proof state after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar (-l1) = toVar (-l2) ∧ polarity (-l1) = polarity (-l2) → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2
Theorem: LeanSAT.LitVar.neg_eq_neg
Proof state before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar (-l1) = toVar (-l2) ∧ polarity (-l1) = polarity (-l2) → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.neg_eq_neg
Proof state before:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → -l1 = -l2
Tactic:
rintro rfl
Proof state after:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ -l1 = -l1
Theorem: LeanSAT.LitVar.neg_eq_neg
Proof state before:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ -l1 = -l1
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.LitVar.neg_neg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ - -l = l
Tactic:
rw [ext_iff]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ toVar (- -l) = toVar l ∧ polarity (- -l) = polarity l
Theorem: LeanSAT.LitVar.neg_neg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ toVar (- -l) = toVar l ∧ polarity (- -l) = polarity l
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.vars_toPropForm
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropForm.vars (toPropForm l) = {toVar l}
Tactic:
dsimp [toPropForm]
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropForm.vars (if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))) =
    {toVar l}
Theorem: LeanSAT.LitVar.vars_toPropForm
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropForm.vars (if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))) =
    {toVar l}
Tactic:
cases polarity l <;> simp [PropForm.vars]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropFun.semVars (toPropFun l) = {toVar l}
Tactic:
dsimp [toPropFun]
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropFun.semVars (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ) = {toVar l}
Theorem: LeanSAT.LitVar.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropFun.semVars (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ) = {toVar l}
Tactic:
cases polarity l <;> simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.satisfies_neg
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
⊢ τ ⊨ toPropFun (-l) ↔ (fun M φ => ¬M ⊨ φ) τ (toPropFun l)
Tactic:
simp [satisfies_iff]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.satisfies_set
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
⊢ PropAssignment.set τ (toVar l) (polarity l) ⊨ toPropFun l
Tactic:
simp [satisfies_iff, τ.set_get]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ (fun M φ => ¬M ⊨ φ) τ (toPropFun l) → PropAssignment.set τ x p ⊨ toPropFun l → l = mkLit L x p
Tactic:
simp only [satisfies_iff]
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ ¬τ (toVar l) = polarity l → PropAssignment.set τ x p (toVar l) = polarity l → l = mkLit L x p
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ ¬τ (toVar l) = polarity l → PropAssignment.set τ x p (toVar l) = polarity l → l = mkLit L x p
Tactic:
intro h hSet
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
⊢ l = mkLit L x p
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
⊢ l = mkLit L x p
Tactic:
by_cases hEq : x = toVar l
Proof state after:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : x = toVar l
⊢ l = mkLit L x p

case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x p
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : x = toVar l
⊢ l = mkLit L x p

case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x p
Tactic:
. rw [hEq, τ.set_get] at hSet
  simp [hSet, hEq]
Proof state after:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x p
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x p
Tactic:
. exfalso; exact h (τ.set_get_of_ne p hEq ▸ hSet)
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : x = toVar l
⊢ l = mkLit L x p
Tactic:
rw [hEq, τ.set_get] at hSet
Proof state after:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : p = polarity l
hEq : x = toVar l
⊢ l = mkLit L x p
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : p = polarity l
hEq : x = toVar l
⊢ l = mkLit L x p
Tactic:
simp [hSet, hEq]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x p
Tactic:
exfalso
Proof state after:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ False
Theorem: LeanSAT.LitVar.eq_of_flip
Proof state before:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : ¬τ (toVar l) = polarity l
hSet : PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ False
Tactic:
exact h (τ.set_get_of_ne p hEq ▸ hSet)
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ τ ⊨ toPropFun l → (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x p) (toPropFun l) → l = mkLit L x !p
Tactic:
simp only [satisfies_iff]
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ τ (toVar l) = polarity l → ¬PropAssignment.set τ x p (toVar l) = polarity l → l = mkLit L x !p
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ τ (toVar l) = polarity l → ¬PropAssignment.set τ x p (toVar l) = polarity l → l = mkLit L x !p
Tactic:
intro h hSet
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
⊢ l = mkLit L x !p
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
⊢ l = mkLit L x !p
Tactic:
by_cases hEq : x = toVar l
Proof state after:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : x = toVar l
⊢ l = mkLit L x !p

case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x !p
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : x = toVar l
⊢ l = mkLit L x !p

case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x !p
Tactic:
. rw [hEq, τ.set_get] at hSet
  have : (!p) = polarity l := by
    simp [Bool.bnot_eq, hSet]
  simp [hEq, this]
Proof state after:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x !p
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x !p
Tactic:
. exfalso; exact hSet (τ.set_get_of_ne p hEq ▸ h)
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : x = toVar l
⊢ l = mkLit L x !p
Tactic:
rw [hEq, τ.set_get] at hSet
Proof state after:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬p = polarity l
hEq : x = toVar l
⊢ l = mkLit L x !p
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬p = polarity l
hEq : x = toVar l
⊢ l = mkLit L x !p
Tactic:
have : (!p) = polarity l := by
  simp [Bool.bnot_eq, hSet]
Proof state after:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬p = polarity l
hEq : x = toVar l
this : (!p) = polarity l
⊢ l = mkLit L x !p
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case pos
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬p = polarity l
hEq : x = toVar l
this : (!p) = polarity l
⊢ l = mkLit L x !p
Tactic:
simp [hEq, this]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬p = polarity l
hEq : x = toVar l
⊢ (!p) = polarity l
Tactic:
simp [Bool.bnot_eq, hSet]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ l = mkLit L x !p
Tactic:
exfalso
Proof state after:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ False
Theorem: LeanSAT.LitVar.eq_of_flip'
Proof state before:
case neg
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
h : τ (toVar l) = polarity l
hSet : ¬PropAssignment.set τ x p (toVar l) = polarity l
hEq : ¬x = toVar l
⊢ False
Tactic:
exact hSet (τ.set_get_of_ne p hEq ▸ h)
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun.inj
Proof state before:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
⊢ Function.Injective toPropFun
Tactic:
intro l1 l2 h
Proof state after:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h : toPropFun l1 = toPropFun l2
⊢ l1 = l2
Theorem: LeanSAT.LitVar.toPropFun.inj
Proof state before:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h : toPropFun l1 = toPropFun l2
⊢ l1 = l2
Tactic:
simp [toPropFun] at h
Proof state after:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h :
  (if polarity l1 = true then var (toVar l1) else (var (toVar l1))ᶜ) =
    if polarity l2 = true then var (toVar l2) else (var (toVar l2))ᶜ
⊢ l1 = l2
Theorem: LeanSAT.LitVar.toPropFun.inj
Proof state before:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h :
  (if polarity l1 = true then var (toVar l1) else (var (toVar l1))ᶜ) =
    if polarity l2 = true then var (toVar l2) else (var (toVar l2))ᶜ
⊢ l1 = l2
Tactic:
apply LawfulLitVar.ext <;> aesop
Proof state after:
no goals
Theorem: LeanSAT.LitVar.satisfies_map
Proof state before:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ τ ⊨ toPropFun (map f l) ↔ PropAssignment.map f τ ⊨ toPropFun l
Tactic:
simp [map, toPropFun]
Proof state after:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ (τ ⊨ if polarity l = true then var (f (toVar l)) else (var (f (toVar l)))ᶜ) ↔
    PropAssignment.map f τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ