chore: fix Array.modify lemmas

src/Init/Data/Array/Lemmas.lean

@@ -847,26 +847,26 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
   unfold modify modifyM Id.run
   split <;> simp
 
-theorem getElem_modify {as : Array α} {x i} (h : i < as.size) :
-    (as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by
+theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
+    (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
   simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
   split
-  · simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
+  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
+  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
-theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) :
-    (as.modify i f)[i]'(by simp [h]) = f as[i] := by
+theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
+    (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
   simp [getElem_modify h]
 
-theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size)
-    (f : α → α) (h : i ≠ j) :
-    (as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by
+theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
+    (f : α → α) (hj : j < (as.modify i f).size) :
+    (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
 @[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
-    (arr.modify x f).get ⟨i, by simp [h]⟩ =
-    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
   simp [getElem_modify h]
 
 /-! ### filter -/

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -136,12 +136,10 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
           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.getElem_modify_self l_in_bounds] at h
+            simp only [i_eq_l, Array.getElem_modify_self] at h
             by_cases b
             · next b_eq_true =>
               rw [isUnit_iff, DefaultClause.toList] at heq
@@ -160,16 +158,14 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               rw [b_eq_false, Subtype.ext i_eq_l]
               exact ih h
           · next i_ne_l =>
-            simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
+            simp only [Array.getElem_modify_of_ne (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.getElem_modify_self l_in_bounds] at h
+            simp only [i_eq_l, Array.getElem_modify_self] at h
             by_cases b
             · next b_eq_true =>
               simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h
@@ -187,7 +183,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               rw [c_def] at cOpt_in_arr
               exact cOpt_in_arr
           · next i_ne_l =>
-            simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
+            simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
             exact ih i b h
     rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
@@ -281,7 +277,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b
     have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
-    have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
     simp only at hb
     by_cases (i, b) = (l, true)
     · next ib_eq_c =>
@@ -292,7 +287,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
       apply DefaultClause.ext
       simp only [unit, hc]
     · next ib_ne_c =>
-      have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
+      have hb' : hasAssignment b f.assignments[i.1] := by
         by_cases l.1 = i.1
         · next l_eq_i =>
           have b_eq_false : b = false := by
@@ -302,10 +297,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
             · next b_eq_false =>
               simp only [Bool.not_eq_true] at b_eq_false
               exact b_eq_false
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb
           simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
         · next l_ne_i =>
-          simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+          simp only [Array.getElem_modify_of_ne l_ne_i] at hb
           exact hb
       specialize hf hb'
       simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -322,7 +317,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b
     have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
-    have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
     simp only at hb
     by_cases (i, b) = (l, false)
     · next ib_eq_c =>
@@ -333,7 +327,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
       apply DefaultClause.ext
       simp only [unit, hc]
     · next ib_ne_c =>
-      have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
+      have hb' : hasAssignment b f.assignments[i.1] := by
         by_cases l.1 = i.1
         · next l_eq_i =>
           have b_eq_false : b = true := by
@@ -341,10 +335,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
             · assumption
             · next b_eq_false =>
               simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_true, hasPos_addNeg] at hb
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb
           simp only [hasAssignment, b_eq_false, ite_true, hb]
         · next l_ne_i =>
-          simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+          simp only [Array.getElem_modify_of_ne l_ne_i] at hb
           exact hb
       specialize hf hb'
       simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -471,14 +465,14 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
       simp only [deleteOne, heq, hl] at hb
       by_cases l.1.1 = i.1
       · next l_eq_i =>
-        simp only [l_eq_i, Array.getElem_modify_self i_in_bounds] at hb
+        simp only [l_eq_i, Array.getElem_modify_self] at hb
         have l_ne_b : l.2 ≠ b := by
           intro l_eq_b
           rw [← l_eq_b] at hb
           have hb' := not_has_remove f.assignments[i.1] l.2
           simp [hb] at hb'
         replace l_ne_b := Bool.eq_not_of_ne l_ne_b
-        rw [l_ne_b] at hb
+        simp only [l_ne_b] at hb
         have hb := has_remove_irrelevant f.assignments[i.1] b hb
         specialize hf i b hb
         simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -512,7 +506,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           · exact hf
         · exact Or.inr hf
       · next l_ne_i =>
-        simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+        simp only [Array.getElem_modify_of_ne l_ne_i] at hb
         specialize hf i b hb
         simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -115,7 +115,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         constructor
         · rfl
         · constructor
-          · rw [Array.getElem_modify_self l_in_bounds]
+          · rw [Array.getElem_modify_self]
             simp only [← i_eq_l, h1]
           · constructor
             · simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@@ -138,7 +138,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
       · next i_ne_l =>
         apply Or.inl
         simp only [insertUnit, h3, ite_false, reduceCtorEq]
-        rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
+        rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l)]
         constructor
         · exact h1
         · intro j
@@ -197,7 +197,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
               rfl
             · constructor
               · simp only [i_eq_l]
-                rw [Array.getElem_modify_self l_in_bounds]
+                rw [Array.getElem_modify_self]
                 simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
                 apply addNeg_addPos_eq_both
               · constructor
@@ -234,7 +234,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
             · rw [Array.get_push_lt units l j.1 j.2, h1]
             · constructor
               · simp only [i_eq_l]
-                rw [Array.getElem_modify_self l_in_bounds]
+                rw [Array.getElem_modify_self]
                 simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
                 apply addPos_addNeg_eq_both
               · constructor
@@ -277,7 +277,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         constructor
         · rw [Array.get_push_lt units l j.1 j.2, h1]
         · constructor
-          · rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h2]
+          · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
           · constructor
             · exact h3
             · intro k k_ne_j
@@ -319,9 +319,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
             by_cases i.1 = l.1.1
             · next i_eq_l =>
               simp only [i_eq_l]
-              rw [Array.getElem_modify_self l_in_bounds]
+              rw [Array.getElem_modify_self]
               simp only [← i_eq_l, h3, add_both_eq_both]
-            · next i_ne_l => rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h3]
+            · next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3]
         · constructor
           · exact h4
           · intro k k_ne_j1 k_ne_j2
@@ -535,7 +535,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
       have i_in_bounds : i.1 < assignments.size := by
         rw [hsize]
         exact i.2
-      have h := Array.getElem_modify_of_ne i_in_bounds (removeAssignment units[idx.val].2) ih2
+      have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds)
       simp only [Fin.getElem_fin] at h
       rw [h]
       exact ih1
@@ -546,8 +546,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
       apply Or.inl
       constructor
       · simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1]
-        have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
-        rw [Array.getElem_modify_self i_in_bounds, ih2, remove_add_cancel]
+        rw [Array.getElem_modify_self, ih2, remove_add_cancel]
         exact ih3
       · intro k k_ge_idx_add_one
         have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one
@@ -568,8 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
         · constructor
           · simp only [clearUnit, Array.get_eq_getElem]
             specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
-            have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
-            rw [Array.getElem_modify_of_ne i_in_bounds _ ih4]
+            rw [Array.getElem_modify_of_ne ih4]
             exact ih2
           · constructor
             · exact ih3
@@ -593,8 +591,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
           exact ih2
         · constructor
           · simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1]
-            have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-            rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
+            rw [Array.getElem_modify_self, ih3, ih4]
             decide
           · constructor
             · simp [hasAssignment, hasNegAssignment, ih4]
@@ -630,8 +627,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
             exact ih1
           · constructor
             · simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2]
-              have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-              rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
+              rw [Array.getElem_modify_self, ih3, ih4]
               decide
             · constructor
               · simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
@@ -687,10 +683,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
                       simp only [Bool.not_eq_true] at h2
                       simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
                       exact h3 rfl
-                  have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
-                    rw [hsize]; exact units[idx.1].1.2.2
-                  have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-                  rw [Array.getElem_modify_of_ne i_in_bounds _ idx_res_ne_i]
+                  rw [Array.getElem_modify_of_ne idx_res_ne_i]
                   exact ih3
                 · constructor
                   · exact ih4
@@ -796,7 +789,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       constructor
       · simp only [List.get, l_eq_i]
       · constructor
-        · simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, List.get, h1]
+        · simp only [l_eq_i, Array.getElem_modify_self, List.get, h1]
         · constructor
           · simp only [List.get, Bool.not_eq_true]
             simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@@ -826,7 +819,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
     · next l_ne_i =>
       apply Or.inl
       constructor
-      · rw [Array.getElem_modify_of_ne i_in_bounds (addAssignment l.2) l_ne_i]
+      · rw [Array.getElem_modify_of_ne l_ne_i]
         exact h1
       · intro l' l'_in_list
         simp only [List.find?, List.mem_cons] at l'_in_list
@@ -865,7 +858,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             apply And.intro l_eq_true ∘ And.intro l'_eq_false
             constructor
             · simp only [l'] at l'_eq_false
-              simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
+              simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self, h1,
                 l'_eq_false, ite_false]
               apply addPos_addNeg_eq_both
             · constructor
@@ -914,7 +907,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             apply And.intro l'_eq_true ∘ And.intro l_eq_false
             constructor
             · simp only [l'] at l'_eq_true
-              simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
+              simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self, h1,
                 l_eq_false, ite_false]
               apply addNeg_addPos_eq_both
             · constructor
@@ -950,7 +943,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       constructor
       · exact j_eq_i
       · constructor
-        · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        · rw [Array.getElem_modify_of_ne l_ne_i]
           exact h1
         · apply And.intro h2
           intro k k_ne_j_succ
@@ -1002,7 +995,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       all_goals
         simp (config := {decide := true}) [getElem!, l_eq_i, i_in_bounds, h1, decidableGetElem?] at h
     constructor
-    · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+    · rw [Array.getElem_modify_of_ne l_ne_i]
       exact h1
     · constructor
       · exact h2

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -39,27 +39,26 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
     rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
     · simp only [insertUnit, hl, ite_false]
       rcases h foundContradiction_eq_true with ⟨i, h⟩
-      have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
       apply Exists.intro i
       by_cases l.1.1 = i.1
       · next l_eq_i =>
-        simp [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
+        simp [l_eq_i, Array.getElem_modify_self, h]
         exact add_both_eq_both l.2
       · next l_ne_i =>
-        simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        simp [Array.getElem_modify_of_ne l_ne_i]
         exact h
     · apply Exists.intro l.1
-      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq]
+      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]
       simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
       by_cases l.2
       · next l_eq_true =>
-        rw [l_eq_true]
+        simp only [l_eq_true]
         simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
           Bool.not_eq_true, decidableGetElem?] at hl
         split at hl <;> simp_all (config := { decide := true })
       · next l_eq_false =>
         simp only [Bool.not_eq_true] at l_eq_false
-        rw [l_eq_false]
+        simp only [l_eq_false]
         simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl
         split at hl <;> simp_all (config := { decide := true })
 
@@ -681,7 +680,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
           by_cases l.1 = i.1
           · next l_eq_i =>
             simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte,
-              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self i_in_bounds (addAssignment b), decidableGetElem?]
+              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?]
             simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc
             by_cases pi : p i
             · simp only [pi, decide_False]
@@ -705,7 +704,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
                 exact pacc
           · next l_ne_i =>
             simp only [getElem!, Array.size_modify, i_in_bounds,
-              Array.getElem_modify_of_ne i_in_bounds _ l_ne_i, dite_true,
+              Array.getElem_modify_of_ne l_ne_i, dite_true,
               Array.get_eq_getElem, decidableGetElem?]
             simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
             exact pacc