Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant
Tactic:
. have hsize : (ofArray arr).assignments.size = n := by
    simp only [ofArray, Array.foldl_eq_foldl_data]
    have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
    have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
      (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
    exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
  apply Exists.intro hsize
  let modified_assignments_invariant (assignments : Array Assignment) : Prop :=
    ∃ hsize : assignments.size = n,
      ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
      (unit (i, b)) ∈ toList (ofArray arr)
  have hb : modified_assignments_invariant (mkArray n unassigned) := by
    have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
    apply Exists.intro hsize
    intro i b h
    by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
  have hl (acc : Array Assignment) (ih : modified_assignments_invariant acc) (cOpt : Option (DefaultClause n))
    (cOpt_in_arr : cOpt ∈ arr.data) : modified_assignments_invariant (ofArray_fold_fn acc cOpt) := by
    have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size, ih.1]
    apply Exists.intro hsize
    intro i b h
    simp only [ofArray_fold_fn] at h
    split at h
    . exact ih.2 i b h
    . next cOpt c =>
      match heq : isUnit c with
      | none =>
        simp only [heq] at h
        exact ih.2 i b h
      | some (l, true) =>
        simp only [heq] at h
        have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
        have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
        rcases ih with ⟨hsize, ih⟩
        by_cases i = l.1
        . next i_eq_l =>
          simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
          by_cases b
          . next b_eq_true =>
            rw [isUnit_iff, DefaultClause.toList] at heq
            simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
            have i_eq_l : i = l := Subtype.ext i_eq_l
            simp only [unit, b_eq_true, i_eq_l]
            have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
            simp only [heq] at c_def
            rw [c_def] at cOpt_in_arr
            exact cOpt_in_arr
          . next b_eq_false =>
            simp only [Bool.not_eq_true] at b_eq_false
            simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
            specialize ih l false
            simp only [hasAssignment, ite_false] at ih
            rw [b_eq_false, Subtype.ext i_eq_l]
            exact ih h
        . next i_ne_l =>
          simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
          exact ih i b h
      | some (l, false) =>
        simp only [heq] at h
        have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
        have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
        rcases ih with ⟨hsize, ih⟩
        by_cases i = l.1
        . next i_eq_l =>
          simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
          by_cases b
          . next b_eq_true =>
            simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
            specialize ih l true
            simp only [hasAssignment, ite_false] at ih
            rw [b_eq_true, Subtype.ext i_eq_l]
            exact ih h
          . next b_eq_false =>
            rw [isUnit_iff, DefaultClause.toList] at heq
            simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
            have i_eq_l : i = l := Subtype.ext i_eq_l
            simp only [unit, b_eq_false, i_eq_l]
            have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
            simp only [heq] at c_def
            rw [c_def] at cOpt_in_arr
            exact cOpt_in_arr
        . next i_ne_l =>
          simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
          exact ih i b h
  rcases List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
  intro i b h
  simp only [ofArray, Array.foldl_eq_foldl_data] at h
  exact h' i b h
Proof state after:
no goals