Theorem: LRAT.DefaultFormula.insertRupUnits_postcondition (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = n
Tactic:
rw [← f_readyForRupAdd.2.1]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = f.assignments.size
Tactic:
exact insertRupUnits_preserves_assignments_size f units
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant f.assignments ⋯ rupUnits assignments hsize
Tactic:
simp only [insertRupUnits]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯
Tactic:
have hsize : f.assignments.size = n := by rw [f_readyForRupAdd.2.1]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯
Tactic:
have h0 : insertUnit_invariant f.assignments hsize f.rupUnits f.assignments hsize := by
  intro i
  simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
  apply Or.inl
  intro j
  simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
  exact Fin.elim0 j
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
h0 : insertUnit_invariant f.assignments hsize f.rupUnits f.assignments hsize
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
h0 : insertUnit_invariant f.assignments hsize f.rupUnits f.assignments hsize
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯
Tactic:
exact insertUnit_fold_preserves_invariant f.assignments hsize f.rupUnits f.assignments hsize false units h0
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ f.assignments.size = n
Tactic:
rw [f_readyForRupAdd.2.1]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments hsize f.rupUnits f.assignments hsize
Tactic:
intro i
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i
Tactic:
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i
Tactic:
apply Or.inl
State after:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i

State before:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i
Tactic:
intro j
State after:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j : Fin f.rupUnits.size
⊢ ¬f.rupUnits[↑j].fst.val = ↑i

State before:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j : Fin f.rupUnits.size
⊢ ¬f.rupUnits[↑j].fst.val = ↑i
Tactic:
simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
State after:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j✝ : Fin f.rupUnits.size
j : Fin 0
⊢ ¬f.rupUnits[↑j✝].fst.val = ↑i

State before:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j✝ : Fin f.rupUnits.size
j : Fin 0
⊢ ¬f.rupUnits[↑j✝].fst.val = ↑i
Tactic:
exact Fin.elim0 j
State after:
no goals