Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst

case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
. simp only [h, ite_true]
  exact ih
Proof state after:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst