Theorem: LeanSAT.LitVar.eq_of_flip (LeanSAT/Data/Cnf.lean)

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]
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

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
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

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
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

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]
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

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)
State after:
no goals

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
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

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]
State after:
no goals

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
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

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)
State after:
no goals