Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case neg
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
      ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
        ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
          (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧
              ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
              assignments0[↑i] = unassigned ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Tactic:
. next h3 =>
  by_cases i.1 = l.1.1
  . next i_eq_l =>
    apply Or.inr ∘ Or.inl
    have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by
      simp only [insertUnit, Prod.mk.eta]
      split
      . contradiction
      . simp only [Array.size_push, Nat.lt_succ_self]
    let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size :=
      ⟨units.size, units_size_lt_updatedUnits_size⟩
    have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
    refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
    simp only [insertUnit, h3, Prod.mk.eta, ite_false, Array.get_push_eq, i_eq_l]
    constructor
    . rfl
    . constructor
      . rw [Array.get_modify_at_idx l_in_bounds]
        simp only [← i_eq_l, h1]
      . constructor
        . simp only [getElem!, l_in_bounds, ↓reduceDite, Array.get_eq_getElem,
          Bool.not_eq_true] at h3
          simp only [← i_eq_l, ← h1]
          simp only [i_eq_l, h3]
        . intro k hk
          have k_in_bounds : k.1 < units.size := by
            apply Nat.lt_of_le_of_ne
            . apply Nat.le_of_lt_succ
              have k_property := k.2
              simp only [insertUnit, h3, Prod.mk.eta, ite_false, Array.size_push] at k_property
              exact k_property
            . intro h
              simp only [← h, not_true, mostRecentUnitIdx] at hk
              exact hk rfl
          rw [Array.get_push_lt _ _ _ k_in_bounds]
          rw [i_eq_l] at h2
          exact h2 ⟨k.1, k_in_bounds⟩
  . next i_ne_l =>
    apply Or.inl
    simp only [insertUnit, h3, Prod.mk.eta, ite_false]
    rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)]
    constructor
    . exact h1
    . intro j
      rw [Array.get_push]
      by_cases h : j.val < Array.size units
      . simp only [h, dite_true]
        exact h2 ⟨j.1, h⟩
      . simp only [h, dite_false]
        exact Ne.symm i_ne_l
Proof state after:
no goals