Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
⊢ unit (i, b) ∈
    (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
match heq : f.clauses[id]! with
| none =>
  simp only
  simp only [deleteOne, heq] at hb
  exact hf i b hb
| some c =>
  by_cases hl : ∃ l : Literal (PosFin n), c = unit l
  . rcases hl with ⟨l, hl⟩
    simp only [unit] at hl
    simp only [hl]
    simp only [deleteOne, heq, hl] at hb
    by_cases l.1.1 = i.1
    . next l_eq_i =>
      simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
      have l_ne_b : l.2 ≠ b := by
        intro l_eq_b
        rw [← l_eq_b] at hb
        have hb' := not_has_of_remove f.assignments[i.1] l.2
        simp [hb] at hb'
      rw [← Bool.eq_not_iff] at l_ne_b
      rw [l_ne_b] at hb
      have hb := has_of_remove_irrelevant f.assignments[i.1] b hb
      specialize hf i b hb
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
      rcases hf with hf | hf
      . apply Or.inl
        simp only [Array.set!, Array.setD]
        split
        . rcases List.get_of_mem hf with ⟨idx, hidx⟩
          simp only [← hidx, Array.data_set]
          rw [List.mem_iff_get]
          have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
            simp only [List.length_set]
            exact idx.2
          apply Exists.intro ⟨idx.1, idx_in_bounds⟩
          by_cases id = idx
          . next id_eq_idx =>
            exfalso
            have idx_in_bounds2 : idx.1 < f.clauses.size := by
              have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
              conv => rhs; rw [f_clauses_rw, Array.size_mk]
              exact idx.2
            simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
              Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
            rw [hidx, hl] at heq
            simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
            simp only [← heq, not] at l_ne_b
            split at l_ne_b
            . simp only at l_ne_b
            . simp only at l_ne_b
          . next id_ne_idx =>
            simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
        . exact hf
      . exact Or.inr hf
    . next l_ne_i =>
      have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
      simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
      specialize hf i b hb
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
      rcases hf with hf | hf
      . apply Or.inl
        simp only [Array.set!, Array.setD]
        split
        . rcases List.get_of_mem hf with ⟨idx, hidx⟩
          simp only [← hidx, Array.data_set]
          rw [List.mem_iff_get]
          have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
            simp only [List.length_set]
            exact idx.2
          apply Exists.intro ⟨idx.1, idx_in_bounds⟩
          by_cases id = idx
          . next id_eq_idx =>
            exfalso
            have idx_in_bounds2 : idx.1 < f.clauses.size := by
              have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
              conv => rhs; rw [f_clauses_rw, Array.size_mk]
              exact idx.2
            simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
              Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
            rw [hidx, hl] at heq
            simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
            have i_eq_l : i = l.1 := by rw [← heq]
            simp only [i_eq_l, not_true] at l_ne_i
          . next id_ne_idx =>
            simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
        . exact hf
      . exact Or.inr hf
  . simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
    split
    . next some_eq_none =>
      simp only at some_eq_none
    . next l _ _ heq =>
      simp only [Option.some.injEq] at heq
      rw [heq] at hl
      specialize hl l.1
      simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
      by_cases hl2 : l.2
      . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
      . simp only [Bool.not_eq_true] at hl2
        simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
    . have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
        simp only [deleteOne]
        split
        . next heq2 =>
          simp only [heq] at heq2
        . next l _ _ heq2 =>
          simp only [heq, Option.some.injEq] at heq2
          rw [heq2] at hl
          specialize hl l.1
          simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
          by_cases hl2 : l.2
          . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
          . simp only [Bool.not_eq_true] at hl2
            simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
        . rfl
      simp only [deleteOne_f_rw] at hb
      specialize hf i b hb
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
      rcases hf with hf | hf
      . apply Or.inl
        simp only [Array.set!, Array.setD]
        split
        . rcases List.get_of_mem hf with ⟨idx, hidx⟩
          simp only [← hidx, Array.data_set]
          rw [List.mem_iff_get]
          have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
            simp only [List.length_set]
            exact idx.2
          apply Exists.intro ⟨idx.1, idx_in_bounds⟩
          by_cases id = idx
          . next id_eq_idx =>
            exfalso
            have idx_in_bounds2 : idx.1 < f.clauses.size := by
              have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
              conv => rhs; rw [f_clauses_rw, Array.size_mk]
              exact idx.2
            simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
              Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
            rw [hidx] at heq
            simp only [Option.some.injEq] at heq
            rw [← heq] at hl
            specialize hl i
            simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
              Bool.not_eq_false, Bool.not_eq_true] at hl
            by_cases b_val : b
            . simp only [b_val, and_false] at hl
            . simp only [b_val, false_and] at hl
          . next id_ne_idx =>
            simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
        . exact hf
      . exact Or.inr hf
Proof state after:
no goals