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
⊢ τ ⊨ toPropFun l → (fun M φ => ¬M ⊨ φ) (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
  have : (!p) = polarity l := by
    simp [Bool.bnot_eq, hSet]
  simp [hEq, this]
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 hSet (τ.set_get_of_ne p hEq ▸ h)
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:
have : (!p) = polarity l := by
  simp [Bool.bnot_eq, 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
this : (!p) = polarity 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
this : (!p) = polarity l
⊢ l = mkLit L x !p
Tactic:
simp [hEq, this]
State after:
no goals

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]
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 hSet (τ.set_get_of_ne p hEq ▸ h)
State after:
no goals