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

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ¬∃ a,
      (a, false) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = false ∨
        (a, true) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp only [not_exists, not_or, not_and] at p'_not_entails_c
State after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
⊢ l.negateLiteral ∈ Clause.toList c

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
rcases p_entails_c with ⟨v, ⟨v_in_c, pv⟩ | ⟨v_in_c, pv⟩⟩
State after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
specialize p'_not_entails_c v
State after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
have h := p'_not_entails_c.1 v_in_c
State after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = false
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = false
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp only [HSat.eval, Bool.not_eq_false] at h
State after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : (if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : (if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
split at h
State after:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
. next heq => simp [negateLiteral, ← heq, h, v_in_c]
State after:
case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
next heq => simp [negateLiteral, ← heq, h, v_in_c]
State after:
no goals

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
heq : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp [negateLiteral, ← heq, h, v_in_c]
State after:
no goals

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
exfalso
State after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : p v = true
⊢ False

State before:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
specialize p'_not_entails_c v
State after:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
have h := p'_not_entails_c.2 v_in_c
State after:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
split at h
State after:
case intro.inr.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inr.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
. next heq => simp [negateLiteral, ← heq, h, v_in_c]
State after:
case intro.inr.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c

State before:
case intro.inr.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
next heq => simp [negateLiteral, ← heq, h, v_in_c]
State after:
no goals

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
heq : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp [negateLiteral, ← heq, h, v_in_c]
State after:
no goals

State before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
exfalso
State after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : ¬p v = true
⊢ False