Theorem: LRAT.DefaultClause.not_tautology (LeanSAT/LRAT/Clause.lean)

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.toList ∨ ¬l.negateLiteral ∈ c.toList
Tactic:
simp only [toList, negateLiteral]
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
have h := c.nodupkey l.1
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
by_cases hl : l.2
State after:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

State before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
. simp only [hl, Bool.not_true]
  rw [← hl] at h
  rcases h with h | h
  . exact Or.inl h
  . exact Or.inr h
State after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

State before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
. simp only [hl, Bool.not_false]
  simp only [Bool.not_eq_true] at hl
  rw [← hl] at h
  rcases h with h | h
  . exact Or.inr h
  . exact Or.inl h
State after:
no goals

State before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
simp only [hl, Bool.not_true]
State after:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

State before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
rw [← hl] at h
State after:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, l.snd) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

State before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, l.snd) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
rcases h with h | h
State after:
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

State before:
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
. exact Or.inl h
State after:
case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

State before:
case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
. exact Or.inr h
State after:
no goals

State before:
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
exact Or.inl h
State after:
no goals

State before:
case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
exact Or.inr h
State after:
no goals

State before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
simp only [hl, Bool.not_false]
State after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

State before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
simp only [Bool.not_eq_true] at hl
State after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

State before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
rw [← hl] at h
State after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, l.snd) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

State before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, l.snd) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
rcases h with h | h
State after:
case neg.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, true) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

State before:
case neg.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, true) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
. exact Or.inr h
State after:
case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

State before:
case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
. exact Or.inl h
State after:
no goals

State before:
case neg.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, true) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
exact Or.inr h
State after:
no goals

State before:
case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
exact Or.inl h
State after:
no goals