more

Author: kim-em

src/Init/Data/Array/Erase.lean

@@ -24,6 +24,7 @@ open Nat
 
 /-! ### eraseP -/
 
+@[grind =]
 theorem eraseP_empty : #[].eraseP p = #[] := by simp
 
 theorem eraseP_of_forall_mem_not {xs : Array α} (h : ∀ a, a ∈ xs → ¬p a) : xs.eraseP p = xs := by
@@ -64,6 +65,7 @@ theorem exists_or_eq_self_of_eraseP (p) (xs : Array α) :
   let ⟨_, ys, zs, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
   rw [e₂]; simp [size_append, e₁]
 
+@[grind =]
 theorem size_eraseP {xs : Array α} : (xs.eraseP p).size = if xs.any p then xs.size - 1 else xs.size := by
   split <;> rename_i h
   · simp only [any_eq_true] at h
@@ -81,27 +83,31 @@ theorem le_size_eraseP {xs : Array α} : xs.size - 1 ≤ (xs.eraseP p).size := b
   rcases xs with ⟨xs⟩
   simpa using List.le_length_eraseP
 
+@[grind →]
 theorem mem_of_mem_eraseP {xs : Array α} : a ∈ xs.eraseP p → a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_eraseP
 
-@[simp] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
+@[simp, grind] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_eraseP_of_neg pa
 
 @[simp] theorem eraseP_eq_self_iff {xs : Array α} : xs.eraseP p = xs ↔ ∀ a ∈ xs, ¬ p a := by
   rcases xs with ⟨xs⟩
   simp
 
+@[grind _=_]
 theorem eraseP_map {f : β → α} {xs : Array β} : (xs.map f).eraseP p = (xs.eraseP (p ∘ f)).map f := by
   rcases xs with ⟨xs⟩
   simpa using List.eraseP_map
 
+@[grind =]
 theorem eraseP_filterMap {f : α → Option β} {xs : Array α} :
     (filterMap f xs).eraseP p = filterMap f (xs.eraseP (fun x => match f x with | some y => p y | none => false)) := by
   rcases xs with ⟨xs⟩
   simpa using List.eraseP_filterMap
 
+@[grind =]
 theorem eraseP_filter {f : α → Bool} {xs : Array α} :
     (filter f xs).eraseP p = filter f (xs.eraseP (fun x => p x && f x)) := by
   rcases xs with ⟨xs⟩
@@ -119,13 +125,15 @@ theorem eraseP_append_right {xs : Array α} ys (h : ∀ b ∈ xs, ¬p b) :
   rcases ys with ⟨ys⟩
   simpa using List.eraseP_append_right ys (by simpa using h)
 
+@[grind =]
 theorem eraseP_append {xs : Array α} {ys : Array α} :
     (xs ++ ys).eraseP p = if xs.any p then xs.eraseP p ++ ys else xs ++ ys.eraseP p := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.eraseP_toArray, List.eraseP_append, List.any_toArray]
   split <;> simp
 
+@[grind =]
 theorem eraseP_replicate {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).eraseP p = if p a then replicate (n - 1) a else replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]
@@ -165,6 +173,7 @@ theorem eraseP_eq_iff {p} {xs : Array α} :
     · exact Or.inl h
     · exact Or.inr ⟨a, l₁, by simpa using h₁, h₂, ⟨l, by simp⟩⟩
 
+@[grind =]
 theorem eraseP_comm {xs : Array α} (h : ∀ a ∈ xs, ¬ p a ∨ ¬ q a) :
     (xs.eraseP p).eraseP q = (xs.eraseP q).eraseP p := by
   rcases xs with ⟨xs⟩
@@ -208,6 +217,7 @@ theorem exists_erase_eq [LawfulBEq α] {a : α} {xs : Array α} (h : a ∈ xs) :
     (xs.erase a).size = xs.size - 1 := by
   rw [erase_eq_eraseP]; exact size_eraseP_of_mem h (beq_self_eq_true a)
 
+@[grind =]
 theorem size_erase [LawfulBEq α] {a : α} {xs : Array α} :
     (xs.erase a).size = if a ∈ xs then xs.size - 1 else xs.size := by
   rw [erase_eq_eraseP, size_eraseP]
@@ -222,18 +232,20 @@ theorem le_size_erase [LawfulBEq α] {a : α} {xs : Array α} : xs.size - 1 ≤
   rcases xs with ⟨xs⟩
   simpa using List.le_length_erase
 
+@[grind →]
 theorem mem_of_mem_erase {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_erase (by simpa using h)
 
-@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
+@[simp, grind] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
     a ∈ xs.erase b ↔ a ∈ xs :=
   erase_eq_eraseP b xs ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
 @[simp] theorem erase_eq_self_iff [LawfulBEq α] {xs : Array α} : xs.erase a = xs ↔ a ∉ xs := by
   rw [erase_eq_eraseP', eraseP_eq_self_iff]
   simp [forall_mem_ne']
 
+@[grind _=_]
 theorem erase_filter [LawfulBEq α] {f : α → Bool} {xs : Array α} :
     (filter f xs).erase a = filter f (xs.erase a) := by
   rcases xs with ⟨xs⟩
@@ -251,13 +263,15 @@ theorem erase_append_right [LawfulBEq α] {a : α} {xs : Array α} (ys : Array 
   rcases ys with ⟨ys⟩
   simpa using List.erase_append_right ys (by simpa using h)
 
+@[grind =]
 theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
     (xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
   split <;> simp
 
+@[grind =]
 theorem erase_replicate [LawfulBEq α] {n : Nat} {a b : α} :
     (replicate n a).erase b = if b == a then replicate (n - 1) a else replicate n a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
@@ -269,6 +283,7 @@ abbrev erase_mkArray := @erase_replicate
 
 -- The arguments `a b` are explicit,
 -- so they can be specified to prevent `simp` repeatedly applying the lemma.
+@[grind =]
 theorem erase_comm [LawfulBEq α] (a b : α) {xs : Array α} :
     (xs.erase a).erase b = (xs.erase b).erase a := by
   rcases xs with ⟨xs⟩
@@ -312,6 +327,7 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.siz
     xs.eraseIdx i h = xs.eraseIdxIfInBounds i := by
   simp [eraseIdxIfInBounds, h]
 
+@[grind =]
 theorem eraseIdx_eq_take_drop_succ {xs : Array α} {i : Nat} (h) :
     xs.eraseIdx i h = xs.take i ++ xs.drop (i + 1) := by
   rcases xs with ⟨xs⟩
@@ -322,6 +338,7 @@ theorem eraseIdx_eq_take_drop_succ {xs : Array α} {i : Nat} (h) :
   rw [List.take_of_length_le]
   simp
 
+@[grind =]
 theorem getElem?_eraseIdx {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} :
     (xs.eraseIdx i)[j]? = if j < i then xs[j]? else xs[j + 1]? := by
   rcases xs with ⟨xs⟩
@@ -339,6 +356,7 @@ theorem getElem?_eraseIdx_of_ge {xs : Array α} {i : Nat} (h : i < xs.size) {j :
   intro h'
   omega
 
+@[grind =]
 theorem getElem_eraseIdx {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} (h' : j < (xs.eraseIdx i).size) :
     (xs.eraseIdx i)[j] = if h'' : j < i then
         xs[j]
@@ -362,6 +380,7 @@ theorem eraseIdx_ne_empty_iff {xs : Array α} {i : Nat} {h} : xs.eraseIdx i ≠
     simp [h]
   · simp
 
+@[grind →]
 theorem mem_of_mem_eraseIdx {xs : Array α} {i : Nat} {h} {a : α} (h : a ∈ xs.eraseIdx i) : a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_eraseIdx (by simpa using h)
@@ -373,13 +392,29 @@ theorem eraseIdx_append_of_lt_size {xs : Array α} {k : Nat} (hk : k < xs.size)
   simp at hk
   simp [List.eraseIdx_append_of_lt_length, *]
 
-theorem eraseIdx_append_of_length_le {xs : Array α} {k : Nat} (hk : xs.size ≤ k) (ys : Array α) (h) :
+theorem eraseIdx_append_of_size_le {xs : Array α} {k : Nat} (hk : xs.size ≤ k) (ys : Array α) (h) :
     eraseIdx (xs ++ ys) k = xs ++ eraseIdx ys (k - xs.size) (by simp at h; omega) := by
   rcases xs with ⟨l⟩
   rcases ys with ⟨l'⟩
   simp at hk
   simp [List.eraseIdx_append_of_length_le, *]
 
+@[deprecated eraseIdx_append_of_size_le (since := "2025-06-11")]
+abbrev eraseIdx_append_of_length_le := @eraseIdx_append_of_size_le
+
+@[grind =]
+theorem eraseIdx_append {xs ys : Array α} (h : k < (xs ++ ys).size) :
+    eraseIdx (xs ++ ys) k =
+      if h' : k < xs.size then
+        eraseIdx xs k ++ ys
+      else
+        xs ++ eraseIdx ys (k - xs.size) (by simp at h; omega) := by
+  split <;> rename_i h
+  · simp [eraseIdx_append_of_lt_size h]
+  · rw [eraseIdx_append_of_size_le]
+    omega
+
+@[grind =]
 theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
     (replicate n a).eraseIdx k = replicate (n - 1) a := by
   simp at h
@@ -428,6 +463,48 @@ theorem eraseIdx_set_gt {xs : Array α} {i : Nat} {j : Nat} {a : α} (h : i < j)
   rcases xs with ⟨xs⟩
   simp [List.eraseIdx_set_gt, *]
 
+@[grind =]
+theorem eraseIdx_set {xs : Array α} {i : Nat} {a : α} {hi : i < xs.size} {j : Nat} {hj : j < (xs.set i a).size} :
+    (xs.set i a).eraseIdx j =
+      if h' : j < i then
+        (xs.eraseIdx j).set (i - 1) a (by simp; omega)
+      else if h'' : j = i then
+        xs.eraseIdx i
+      else
+        (xs.eraseIdx j (by simp at hj; omega)).set i a (by simp at hj ⊢; omega) := 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 : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (h : i ≤ j) (hj : j < (xs.eraseIdx i).size) :
+    (xs.eraseIdx i).set j a = (xs.set (j + 1) a (by simp at hj; omega)).eraseIdx i (by simp at ⊢; omega) := by
+  rw [eraseIdx_set_lt]
+  · simp
+  · omega
+
+theorem set_eraseIdx_gt {xs : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (h : j < i) (hj : j < (xs.eraseIdx i).size) :
+    (xs.eraseIdx i).set j a = (xs.set j a).eraseIdx i (by simp at ⊢; omega) := by
+  rw [eraseIdx_set_gt]
+  omega
+
+@[grind =]
+theorem set_eraseIdx {xs : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (hj : j < (xs.eraseIdx i).size) :
+    (xs.eraseIdx i).set j a =
+      if h' : i ≤ j then
+        (xs.set (j + 1) a (by simp at hj; omega)).eraseIdx i (by simp at ⊢; omega)
+      else
+        (xs.set j a).eraseIdx i (by simp at ⊢; omega) := by
+  split <;> rename_i h'
+  · rw [set_eraseIdx_le]
+    omega
+  · rw [set_eraseIdx_gt]
+    omega
+
 @[simp] 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 simp; omega) = xs.eraseIdx i := by

src/Init/Data/Vector/Erase.lean

@@ -22,11 +22,13 @@ open Nat
 
 /-! ### eraseIdx -/
 
+@[grind =]
 theorem eraseIdx_eq_take_drop_succ {xs : Vector α n} {i : Nat} (h) :
     xs.eraseIdx i = (xs.take i ++ xs.drop (i + 1)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.eraseIdx_eq_take_drop_succ, *]
 
+@[grind =]
 theorem getElem?_eraseIdx {xs : Vector α n} {i : Nat} (h : i < n) {j : Nat} :
     (xs.eraseIdx i)[j]? = if j < i then xs[j]? else xs[j + 1]? := by
   rcases xs with ⟨xs, rfl⟩
@@ -44,12 +46,14 @@ theorem getElem?_eraseIdx_of_ge {xs : Vector α n} {i : Nat} (h : i < n) {j : Na
   intro h'
   omega
 
+@[grind =]
 theorem getElem_eraseIdx {xs : Vector α n} {i : Nat} (h : i < n) {j : Nat} (h' : j < n - 1) :
     (xs.eraseIdx i)[j] = if h'' : j < i then xs[j] else xs[j + 1] := by
   apply Option.some.inj
   rw [← getElem?_eq_getElem, getElem?_eraseIdx]
   split <;> simp
 
+@[grind →]
 theorem mem_of_mem_eraseIdx {xs : Vector α n} {i : Nat} {h} {a : α} (h : a ∈ xs.eraseIdx i) : a ∈ xs := by
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.mem_of_mem_eraseIdx (by simpa using h)
@@ -64,13 +68,23 @@ theorem eraseIdx_append_of_length_le {xs : Vector α n} {k : Nat} (hk : n ≤ k)
     eraseIdx (xs ++ xs') k = (xs ++ eraseIdx xs' (k - n)).cast (by omega) := by
   rcases xs with ⟨xs⟩
   rcases xs' with ⟨xs'⟩
-  simp [Array.eraseIdx_append_of_length_le, *]
+  simp [Array.eraseIdx_append_of_size_le, *]
 
+@[grind =]
+theorem eraseIdx_append {xs : Vector α n} {ys : Vector α m} {k : Nat} (h : k < n + m) :
+    eraseIdx (xs ++ ys) k = if h' : k < n then (eraseIdx xs k ++ ys).cast (by omega) else (xs ++ eraseIdx ys (k - n) (by omega)).cast (by omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp only [mk_append_mk, eraseIdx_mk, Array.eraseIdx_append]
+  split <;> simp
+
+@[grind = ]
 theorem eraseIdx_cast {xs : Vector α n} {k : Nat} (h : k < m) :
     eraseIdx (xs.cast w) k h = (eraseIdx xs k).cast (by omega) := by
   rcases xs with ⟨xs⟩
   simp
 
+@[grind =]
 theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
     (replicate n a).eraseIdx k = replicate (n - 1) a := by
   rw [replicate_eq_mk_replicate, eraseIdx_mk]
@@ -112,6 +126,45 @@ theorem eraseIdx_set_gt {xs : Vector α n} {i : Nat} {j : Nat} {a : α} (h : i <
   rcases xs with ⟨xs⟩
   simp [Array.eraseIdx_set_gt, *]
 
+@[grind =]
+theorem eraseIdx_set {xs : Vector α n} {i : Nat} {a : α} {hi : i < n} {j : Nat} {hj : j < n} :
+    (xs.set i a).eraseIdx j =
+      if h' : j < i then
+        (xs.eraseIdx j).set (i - 1) a
+      else if h'' : j = i then
+        xs.eraseIdx i
+      else
+        (xs.eraseIdx j).set i a := by
+  rcases xs with ⟨xs⟩
+  simp only [set_mk, eraseIdx_mk, Array.eraseIdx_set]
+  split
+  · simp
+  · split <;> simp
+
+theorem set_eraseIdx_le {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : i ≤ j) (hj : j < n - 1) :
+    (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 : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) (hj : j < n - 1) :
+    (xs.eraseIdx i).set j a = (xs.set j a).eraseIdx i := by
+  rw [eraseIdx_set_gt]
+  omega
+
+@[grind =]
+theorem set_eraseIdx {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (hj : j < n - 1) :
+    (xs.eraseIdx i).set j a =
+      if h' : 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
     {xs : Vector α n} {i : Nat} (h : i + 1 < n) :
     (xs.eraseIdx (i + 1)).set i xs[i + 1] = xs.eraseIdx i := by

tests/lean/run/grind_list_erase.lean

@@ -10,7 +10,6 @@ theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
     length (l.eraseP p) = length l - 1 := by
   grind
 
--- reverse direction of lemma from library
 theorem eraseP_filterMap' {f : α → Option β} {l : List α} :
     filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false)) = (filterMap f l).eraseP p := by
   grind
@@ -21,3 +20,12 @@ theorem eraseP_append_left {a : α} (pa : p a) {l₁ : List α} {l₂} : a ∈ l
 theorem eraseP_append_right {l₁ : List α} {l₂} (h : ∀ b ∈ l₁, ¬p b) :
     eraseP p (l₁ ++ l₂) = l₁ ++ l₂.eraseP p := by
   grind
+
+theorem head_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs := by grind
+
+theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs := by grind
+
+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