Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro
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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
j1_lt_updatedUnits_size : ↑j1 < (insertUnit (units, assignments, foundContradiction) l).fst.size
j2_lt_updatedUnits_size : ↑j2 < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (insertUnit (units, assignments, foundContradiction) l).fst[↑⟨↑j1, j1_lt_updatedUnits_size⟩] = (⟨↑i, ⋯⟩, true) ∧
    (insertUnit (units, assignments, foundContradiction) l).fst[↑⟨↑j2, j2_lt_updatedUnits_size⟩] = (⟨↑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, j1_lt_updatedUnits_size⟩ →
              ¬k = ⟨↑j2, j2_lt_updatedUnits_size⟩ →
                ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Tactic:
simp only [insertUnit, Prod.mk.eta]
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro
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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
j1_lt_updatedUnits_size : ↑j1 < (insertUnit (units, assignments, foundContradiction) l).fst.size
j2_lt_updatedUnits_size : ↑j2 < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
          else
            (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
              foundContradiction || assignments[l.fst.val]! != unassigned)).fst[↑j1] =
      (⟨↑i, ⋯⟩, true) ∧
    (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
            else
              (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned)).fst[↑j2] =
        (⟨↑i, ⋯⟩, false) ∧
      (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
                else
                  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
                    foundContradiction || assignments[l.fst.val]! != unassigned)).snd.fst[↑i] =
          both ∧
        assignments0[↑i] = unassigned ∧
          ∀
            (k :
              Fin
                (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
                    else
                      (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                        foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
            ¬k = ⟨↑j1, j1_lt_updatedUnits_size⟩ →
              ¬k = ⟨↑j2, j2_lt_updatedUnits_size⟩ →
                ¬(if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
                            else
                              (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
                                foundContradiction || assignments[l.fst.val]! != unassigned)).fst[↑k].fst.val =
                    ↑i