Theorem: LRAT.DefaultFormula.encounteredBoth_entails_unsat (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
⊢ c.reduce assignment = encounteredBoth → unsatisfiable (PosFin n) assignment
Tactic:
have hb : (reducedToEmpty : ReduceResult (PosFin n)) = encounteredBoth → unsatisfiable (PosFin n) assignment := by
  simp only [false_implies]
State after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
⊢ c.reduce assignment = encounteredBoth → unsatisfiable (PosFin n) assignment

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
hl :
  ∀ (res : ReduceResult (PosFin n)),
    (res = encounteredBoth → unsatisfiable (PosFin n) assignment) →
      ∀ (l : Literal (PosFin n)),
        l ∈ c.clause → reduce_fold_fn assignment res l = encounteredBoth → unsatisfiable (PosFin n) assignment
⊢ c.reduce assignment = encounteredBoth → unsatisfiable (PosFin n) assignment
Tactic:
exact List.foldlRecOn c.clause (reduce_fold_fn assignment) reducedToEmpty hb hl
State after:
no goals

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
⊢ reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
Tactic:
simp only [false_implies]
State after:
no goals

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
⊢ reduce_fold_fn assignment res l = encounteredBoth → unsatisfiable (PosFin n) assignment
Tactic:
intro h
State after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h : reduce_fold_fn assignment res l = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h : reduce_fold_fn assignment res l = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
rw [reduce_fold_fn] at h
State after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
      | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit l
    | reducedToUnit l' =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
      | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit l
    | reducedToUnit l' =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
split at h <;>
  [
    exact ih rfl;
    skip;
    skip;
    simp only at h
  ]
State after:
case h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
h :
  (match assignment[l.fst.val]! with
    | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
    | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit l) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
h :
  (match assignment[l.fst.val]! with
    | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

State before:
case h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
h :
  (match assignment[l.fst.val]! with
    | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
split at h
State after:
case h_3.h_1
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = pos
h : (if l.snd = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

State before:
case h_3.h_1
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = pos
h : (if l.snd = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
. split at h <;> simp only at h
State after:
case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

State before:
case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
. split at h <;> simp only at h
State after:
case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

State before:
case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
. simp only at h
State after:
no goals

State before:
case h_3.h_1
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = pos
h : (if l.snd = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
split at h <;> simp only at h
State after:
no goals

State before:
case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
split at h <;> simp only at h
State after:
no goals

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
intro p hp
State after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
p : PosFin n → Bool
hp : p ⊨ assignment
⊢ False

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
p : PosFin n → Bool
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ False
Tactic:
specialize hp l.1
State after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
p : PosFin n → Bool
hp : hasAssignment (decide (p l.fst = false)) assignment[l.fst.val]! = false
⊢ False

State before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
p : PosFin n → Bool
hp : hasAssignment (decide (p l.fst = false)) assignment[l.fst.val]! = false
⊢ False
Tactic:
simp only [heq, has_of_both] at hp
State after:
no goals

State before:
case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
simp only at h
State after:
no goals