internlm/Lean-Github huggingface dataset:
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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]
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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]
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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⟩
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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⟩
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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]
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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⟩
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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]
Proof 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))
Theorem: LRAT.Clause.limplies_iff_mem
Proof 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⟩
Proof state after:
no goals
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
⊢ p ⊨ delete c l → p ⊨ c
Tactic:
intro h
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
h : p ⊨ delete c l
⊢ p ⊨ c