Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment (LeanSAT/LRAT/Formula/RatAddSound.lean)

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_cl :
  ∃ a,
    ((a, false) ≠ l.negateLiteral ∧ (a, false) ∈ c.toList) ∧ p a = false ∨
      ((a, true) ≠ l.negateLiteral ∧ (a, true) ∈ c.toList) ∧ p a = true
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
Tactic:
rcases p_entails_cl with ⟨v, ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩ | ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩⟩
  <;> [
      (apply Exists.intro v; apply Or.inl);
      (apply Exists.intro v; apply Or.inr)
    ]
State after:
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false

case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true

State before:
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false

case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
all_goals
  constructor
  . simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
  . split
    . next heq =>
      simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
      split at negl_ne_v <;> simp_all
    . next hne =>
      exact pv
State after:
no goals

State before:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
Tactic:
apply Exists.intro v
State after:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true

State before:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
apply Or.inl
State after:
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false

State before:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
Tactic:
apply Exists.intro v
State after:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true

State before:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
apply Or.inr
State after:
case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true

State before:
case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
constructor
State after:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral)

case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true

State before:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral)

case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Tactic:
. simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
State after:
case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true

State before:
case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Tactic:
. split
  . next heq =>
    simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
    split at negl_ne_v <;> simp_all
  . next hne =>
    exact pv
State after:
no goals

State before:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral)
Tactic:
simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
State after:
no goals

State before:
case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Tactic:
split
State after:
case intro.inr.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = true

case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true

State before:
case intro.inr.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = true

case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Tactic:
. next heq =>
  simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
  split at negl_ne_v <;> simp_all
State after:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true

State before:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Tactic:
. next hne =>
  exact pv
State after:
no goals

State before:
case intro.inr.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = true
Tactic:
next heq =>
simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
split at negl_ne_v <;> simp_all
State after:
no goals

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
⊢ l.snd = true
Tactic:
simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
State after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
negl_ne_v :
  ¬true =
      match l.snd with
      | true => false
      | false => true
⊢ l.snd = true

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
negl_ne_v :
  ¬true =
      match l.snd with
      | true => false
      | false => true
⊢ l.snd = true
Tactic:
split at negl_ne_v <;> simp_all
State after:
no goals

State before:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Tactic:
next hne =>
exact pv
State after:
no goals

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
hne : ¬v = l.fst
⊢ p v = true
Tactic:
exact pv
State after:
no goals