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

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
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
intro p hp

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)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
p : PosFin n → Bool
hp : p ⊨ assignment
⊢ False

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 : ∀ (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)
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

Proof state:
case 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 : reducedToNonunit = encounteredBoth → Unsatisfiable (PosFin n) assignment
h : reducedToNonunit = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
simp at h

Result:
no goals

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

Result:
case 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)
ih : encounteredBoth = encounteredBoth → Unsatisfiable (PosFin n) assignment
h : encounteredBoth = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

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

case 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 : reducedToNonunit = encounteredBoth → Unsatisfiable (PosFin n) assignment
h : reducedToNonunit = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Proof state:
case 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)
ih : encounteredBoth = encounteredBoth → Unsatisfiable (PosFin n) assignment
h : encounteredBoth = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
exact ih rfl

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
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
intro p hp

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 : p ⊨ assignment
⊢ False