-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
    (assignment : Array Assignment) :
    reduce c assignment = encounteredBoth → Unsatisfiable (PosFin n) assignment

Proof state:
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

Result:
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

Proof state:
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

Result:
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

Proof state:
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

Result:
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

Proof state:
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 at h

Result:
no goals

Proof state:
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
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 [heq, has_both] at hp

Result:
no goals

Proof state:
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 [heq, has_both] at hp

Result:
no goals

Proof state:
case h_2.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)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToUnit l = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
simp at h

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
assignment : Array Assignment
⊢ reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment

Tactic:
simp

Result:
no goals

Proof state:
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 at h

Result:
no goals