Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_assignments_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRupUnits units).fst.rupUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRupUnits units).fst.rupUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRupUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    k ≠ j → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
h✝ : b = b'
⊢ p ⊨ (i, b)
Tactic:
next b_eq_b' =>
let j_unit := unit (insertRupUnits f units).1.rupUnits[j]
have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := rfl
have j_unit_in_insertRupUnits_res :
  ∃ i : PosFin n,
    (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j_unit ∨
    (i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j_unit := by
  apply Exists.intro i
  rw [j_unit_def, h1]
  by_cases hb' : b'
  . rw [hb']
    apply Or.inr
    constructor
    . have h1 : (insertRupUnits f units).fst.rupUnits[j] = (i, true) := by
        rw [hb'] at h1
        rw [h1]
        simp only [Prod.mk.injEq, and_true]
        apply Subtype.ext
        rfl
      rw [← h1]
      apply Array.getElem_mem_data
    . rfl
  . simp only [Bool.not_eq_true] at hb'
    rw [hb']
    apply Or.inl
    constructor
    . have h1 : (insertRupUnits f units).fst.rupUnits[j] = (i, false) := by
        rw [hb'] at h1
        rw [h1]
        simp only [Prod.mk.injEq, and_true]
        apply Subtype.ext
        rfl
      rw [← h1]
      apply Array.getElem_mem_data
    . rfl
specialize hp j_unit ((Or.inr ∘ Or.inl) j_unit_in_insertRupUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
simp only [Fin.getElem_fin] at h1
rcases hp with ⟨i', hp⟩
simp only [h1, Clause.toList, unit_eq, List.mem_singleton,
  Prod.mk.injEq] at hp
rcases hp with ⟨hp1, hp2⟩ | ⟨hp1, hp2⟩
. simp only [b_eq_b', ← hp1.2, HSat.eval]
  rw [hp1.1] at hp2
  exact of_decide_eq_true hp2
. simp only [b_eq_b', ← hp1.2, HSat.eval]
  rw [hp1.1] at hp2
  exact hp2
Proof state after:
no goals