Theorem: LRAT.Clause.limplies_iff_mem (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ limplies α l c ↔ l ∈ toList c
Tactic:
simp only [limplies, sat_iff_exists, Prod.exists, Bool.exists_bool]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) ↔
    l ∈ toList c

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) ↔
    l ∈ toList c
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) →
    l ∈ toList c

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList c →
    ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))

State before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList c →
    ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
Tactic:
. intro h p pl
  apply Exists.intro l.1
  by_cases hl : l.2
  . apply Or.inr
    rw [← hl]
    exact ⟨h, pl⟩
  . apply Or.inl
    simp only [Bool.not_eq_true] at hl
    rw [← hl]
    exact ⟨h, pl⟩
State after:
no goals

State before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) →
    l ∈ toList c
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c

State before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c
Tactic:
let p := fun x : α => if x = l.1 then l.2 else (x, false) ∈ toList c
State after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
⊢ l ∈ toList c

State before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
⊢ l ∈ toList c
Tactic:
specialize h p pl
State after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
h : ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c

State before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
h : ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c
Tactic:
rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
State after:
case mp.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h2 : p ⊨ (v, false)
⊢ l ∈ toList c

case mp.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h2 : p ⊨ (v, true)
⊢ l ∈ toList c

State before:
case mp.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h2 : (if v = l.fst then l.snd else decide ((v, false) ∈ toList c)) = false
⊢ l ∈ toList c
Tactic:
split at h2
State after:
case mp.intro.inl.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = false
⊢ l ∈ toList c

case mp.intro.inl.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c

State before:
case mp.intro.inl.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = false
⊢ l ∈ toList c

case mp.intro.inl.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c
Tactic:
. next v_eq_l =>
  rw [← @Prod.mk.eta α Bool l, ← v_eq_l, h2]
  exact h1
State after:
case mp.intro.inl.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c

State before:
case mp.intro.inl.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c
Tactic:
. next v_ne_l =>
  simp only [decide_eq_false_iff_not] at h2
  exfalso
  exact h2 h1
State after:
no goals

State before:
case mp.intro.inl.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = false
⊢ l ∈ toList c
Tactic:
next v_eq_l =>
rw [← @Prod.mk.eta α Bool l, ← v_eq_l, h2]
exact h1
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = false
⊢ l ∈ toList c
Tactic:
rw [← @Prod.mk.eta α Bool l, ← v_eq_l, h2]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = false
⊢ (v, false) ∈ toList c

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = false
⊢ (v, false) ∈ toList c
Tactic:
exact h1
State after:
no goals

State before:
case mp.intro.inl.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c
Tactic:
next v_ne_l =>
simp only [decide_eq_false_iff_not] at h2
exfalso
exact h2 h1
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c
Tactic:
simp only [decide_eq_false_iff_not] at h2
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : ¬(v, false) ∈ toList c
⊢ l ∈ toList c

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : ¬(v, false) ∈ toList c
⊢ l ∈ toList c
Tactic:
exfalso
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : ¬(v, false) ∈ toList c
⊢ False

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : ¬(v, false) ∈ toList c
⊢ False
Tactic:
exact h2 h1
State after:
no goals

State before:
case mp.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h2 : (if v = l.fst then l.snd else decide ((v, false) ∈ toList c)) = true
⊢ l ∈ toList c
Tactic:
split at h2
State after:
case mp.intro.inr.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = true
⊢ l ∈ toList c

case mp.intro.inr.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c

State before:
case mp.intro.inr.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = true
⊢ l ∈ toList c

case mp.intro.inr.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c
Tactic:
. next v_eq_l =>
  rw [← @Prod.mk.eta α Bool l, ← v_eq_l, h2]
  exact h1
State after:
case mp.intro.inr.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c

State before:
case mp.intro.inr.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c
Tactic:
. next v_ne_l =>
  simp only [decide_eq_true_eq] at h2
  exfalso
  rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
  . exact v_not_in_c h1
  . simp only [negateLiteral, Bool.not_true] at negv_not_in_c
    exact negv_not_in_c h2
State after:
no goals

State before:
case mp.intro.inr.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = true
⊢ l ∈ toList c
Tactic:
next v_eq_l =>
rw [← @Prod.mk.eta α Bool l, ← v_eq_l, h2]
exact h1
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = true
⊢ l ∈ toList c
Tactic:
rw [← @Prod.mk.eta α Bool l, ← v_eq_l, h2]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = true
⊢ (v, true) ∈ toList c

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = true
⊢ (v, true) ∈ toList c
Tactic:
exact h1
State after:
no goals

State before:
case mp.intro.inr.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c
Tactic:
next v_ne_l =>
simp only [decide_eq_true_eq] at h2
exfalso
rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
. exact v_not_in_c h1
. simp only [negateLiteral, Bool.not_true] at negv_not_in_c
  exact negv_not_in_c h2
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c
Tactic:
simp only [decide_eq_true_eq] at h2
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
⊢ l ∈ toList c

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
⊢ l ∈ toList c
Tactic:
exfalso
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
⊢ False

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
⊢ False
Tactic:
rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
State after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
v_not_in_c : ¬(v, true) ∈ toList c
⊢ False

case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬negateLiteral (v, true) ∈ toList c
⊢ False

State before:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
v_not_in_c : ¬(v, true) ∈ toList c
⊢ False

case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬negateLiteral (v, true) ∈ toList c
⊢ False
Tactic:
. exact v_not_in_c h1
State after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬negateLiteral (v, true) ∈ toList c
⊢ False

State before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬negateLiteral (v, true) ∈ toList c
⊢ False
Tactic:
. simp only [negateLiteral, Bool.not_true] at negv_not_in_c
  exact negv_not_in_c h2
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
v_not_in_c : ¬(v, true) ∈ toList c
⊢ False
Tactic:
exact v_not_in_c h1
State after:
no goals

State before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬negateLiteral (v, true) ∈ toList c
⊢ False
Tactic:
simp only [negateLiteral, Bool.not_true] at negv_not_in_c
State after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬(v, false) ∈ toList c
⊢ False

State before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬(v, false) ∈ toList c
⊢ False
Tactic:
exact negv_not_in_c h2
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList c →
    ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
Tactic:
intro h p pl
State after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
⊢ ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))

State before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
⊢ ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
Tactic:
apply Exists.intro l.1
State after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

State before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
Tactic:
by_cases hl : l.2
State after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

State before:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
Tactic:
. apply Or.inr
  rw [← hl]
  exact ⟨h, pl⟩
State after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

State before:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
Tactic:
. apply Or.inl
  simp only [Bool.not_eq_true] at hl
  rw [← hl]
  exact ⟨h, pl⟩
State after:
no goals

State before:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
Tactic:
apply Or.inr
State after:
case pos.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

State before:
case pos.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
Tactic:
rw [← hl]
State after:
case pos.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))

State before:
case pos.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))
Tactic:
exact ⟨h, pl⟩
State after:
no goals

State before:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
Tactic:
apply Or.inl
State after:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))

State before:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))
Tactic:
simp only [Bool.not_eq_true] at hl
State after:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = false
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))

State before:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = false
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))
Tactic:
rw [← hl]
State after:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = false
⊢ (l.fst, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))

State before:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = false
⊢ (l.fst, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))
Tactic:
exact ⟨h, pl⟩
State after:
no goals