finish

Author: kim-em

src/Init/Data/List/Nat/Erase.lean

@@ -14,6 +14,7 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace List
 
+@[grind =]
 theorem getElem?_eraseIdx {l : List α} {i : Nat} {j : Nat} :
     (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]? := by
   rw [eraseIdx_eq_take_drop_succ, getElem?_append]
@@ -49,6 +50,7 @@ theorem getElem?_eraseIdx_of_ge {l : List α} {i : Nat} {j : Nat} (h : i ≤ j)
   intro h'
   omega
 
+@[grind =]
 theorem getElem_eraseIdx {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) :
     (l.eraseIdx i)[j] = if h' : j < i then
         l[j]'(by have := length_eraseIdx_le l i; omega)
@@ -123,6 +125,48 @@ theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
       · have t : i ≠ n := by omega
         simp [t]
 
+@[grind =]
+theorem eraseIdx_set {xs : List α} {i : Nat} {a : α} {j : Nat} :
+    (xs.set i a).eraseIdx j =
+      if j < i then
+        (xs.eraseIdx j).set (i - 1) a
+      else if j = i then
+        xs.eraseIdx i
+      else
+        (xs.eraseIdx j).set i a := by
+  split <;> rename_i h'
+  · rw [eraseIdx_set_lt]
+    omega
+  · split <;> rename_i h''
+    · subst h''
+      rw [eraseIdx_set_eq]
+    · rw [eraseIdx_set_gt]
+      omega
+
+theorem set_eraseIdx_le {xs : List α} {i : Nat} {j : Nat} {a : α} (h : i ≤ j) :
+    (xs.eraseIdx i).set j a = (xs.set (j + 1) a).eraseIdx i := by
+  rw [eraseIdx_set_lt]
+  · simp
+  · omega
+
+theorem set_eraseIdx_gt {xs : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
+    (xs.eraseIdx i).set j a = (xs.set j a).eraseIdx i := by
+  rw [eraseIdx_set_gt]
+  omega
+
+@[grind =]
+theorem set_eraseIdx {xs : List α} {i : Nat} {j : Nat} {a : α} :
+    (xs.eraseIdx i).set j a =
+      if i ≤ j then
+        (xs.set (j + 1) a).eraseIdx i
+      else
+        (xs.set j a).eraseIdx i := by
+  split <;> rename_i h'
+  · rw [set_eraseIdx_le]
+    omega
+  · rw [set_eraseIdx_gt]
+    omega
+
 @[simp] theorem set_getElem_succ_eraseIdx_succ
     {l : List α} {i : Nat} (h : i + 1 < l.length) :
     (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by

tests/lean/run/grind_list_erase.lean

@@ -28,4 +28,4 @@ theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).
 theorem set_getElem_succ_eraseIdx_succ
     {xs : Array α} {i : Nat} (h : i + 1 < xs.size) :
     (xs.eraseIdx (i + 1)).set i xs[i + 1] (by grind) = xs.eraseIdx i := by
-  grind
+  grind (splits := 9)