Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
    false
⊢ p ⊨ (i, b)
Tactic:
have i_in_bounds :
  i.1 < (rupHints.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) 0 rupHints.size).1.size := by
  let in_bounds_motive (_idx : Nat) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) := acc.1.size = n
  have in_bounds_base : in_bounds_motive 0 (f.assignments, [], false, false) := by
    simp only [f_assignments_invariant.1, in_bounds_motive]
  have in_bounds_inductive (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool)
    (ih : in_bounds_motive idx.1 acc) : in_bounds_motive (idx.1 + 1) (confirmRupHint f.clauses acc rupHints[idx]) := by
    have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 rupHints[idx]
    simp at *
    omega
  rw [Array.foldl_induction in_bounds_motive in_bounds_base in_bounds_inductive]
  exact i.2.2
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
    false
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
⊢ p ⊨ (i, b)