max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add grind annotations for List/Array/Vector.eraseP/erase/eraseIdx (#8719)

Browse source 
This PR adds grind annotations for
List/Array/Vector.eraseP/erase/eraseIdx. It also adds some missing
lemmas.
This commit is contained in:
Kim Morrison 2025-06-11 19:44:47 +10:00 • committed by GitHub
parent ee5b652136
commit 082ca94d3b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 257 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

83
src/Init/Data/Array/Erase.lean
View file

@ -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,11 +83,12 @@ 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
@ -93,15 +96,18 @@ theorem mem_of_mem_eraseP {xs : Array α} : a ∈ xs.eraseP p → a ∈ xs := 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,6 +125,7 @@ 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⟩
@ -126,6 +133,7 @@ theorem eraseP_append {xs : Array α} {ys : Array α} :
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,11 +232,12 @@ 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)
@ -234,6 +245,7 @@ theorem mem_of_mem_erase {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a
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,6 +263,7 @@ 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⟩
@ -258,6 +271,7 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
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

55
src/Init/Data/List/Erase.lean
View file

@ -23,9 +23,9 @@ open Nat
/-! ### eraseP -/
@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
@[simp, grind =] theorem eraseP_nil : [].eraseP p = [] := rfl
theorem eraseP_cons {a : α} {l : List α} :
@[grind =] theorem eraseP_cons {a : α} {l : List α} :
(a :: l).eraseP p = bif p a then l else a :: l.eraseP p := rfl
@[simp] theorem eraseP_cons_of_pos {l : List α} {p} (h : p a) : (a :: l).eraseP p = l := by
@ -92,7 +92,7 @@ theorem exists_or_eq_self_of_eraseP (p) (l : List α) :
let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
rw [e₂]; simp [length_append, e₁]
theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by
@[grind =] theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by
split <;> rename_i h
· simp only [any_eq_true] at h
obtain ⟨x, m, h⟩ := h
@ -106,8 +106,13 @@ theorem eraseP_sublist {l : List α} : l.eraseP p <+ l := by
| .inl h => rw [h]; apply Sublist.refl
| .inr ⟨c, l₁, l₂, _, _, h₃, h₄⟩ => rw [h₄, h₃]; simp
grind_pattern eraseP_sublist => l.eraseP p, List.Sublist
theorem eraseP_subset {l : List α} : l.eraseP p ⊆ l := eraseP_sublist.subset
grind_pattern eraseP_subset => l.eraseP p, List.Subset
@[grind ←]
protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p
| .slnil => Sublist.refl _
| .cons a s => by
@ -147,10 +152,12 @@ theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (erase
· intro; obtain ⟨x, m, h⟩ := h; simp_all
· simp_all
@[grind _=_]
theorem eraseP_map {f : β → α} : ∀ {l : List β}, (map f l).eraseP p = map f (l.eraseP (p ∘ f))
| [] => rfl
| b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map, eraseP_cons_of_pos]
@[grind =]
theorem eraseP_filterMap {f : α → Option β} : ∀ {l : List α},
(filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))
| [] => rfl
@ -165,6 +172,7 @@ theorem eraseP_filterMap {f : α → Option β} : ∀ {l : List α},
· simp only [w, cond_false]
rw [filterMap_cons_some h, eraseP_filterMap]
@[grind =]
theorem eraseP_filter {f : α → Bool} {l : List α} :
(filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x)) := by
rw [← filterMap_eq_filter, eraseP_filterMap]
@ -174,18 +182,19 @@ theorem eraseP_filter {f : α → Bool} {l : List α} :
split <;> split at * <;> simp_all
theorem eraseP_append_left {a : α} (pa : p a) :
∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂
∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁ ++ l₂).eraseP p = l₁.eraseP p ++ l₂
| x :: xs, l₂, h => by
by_cases h' : p x <;> simp [h']
rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
intro | rfl => exact pa
theorem eraseP_append_right :
∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁ ++ l₂) = l₁ ++ l₂.eraseP p
| [], _, _ => rfl
| _ :: _, _, h => by
simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]
@[grind =]
theorem eraseP_append {l₁ l₂ : List α} :
(l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p := by
split <;> rename_i h
@ -196,6 +205,7 @@ theorem eraseP_append {l₁ l₂ : List α} :
rw [eraseP_append_right _]
simp_all
@[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
induction n with
@ -212,6 +222,7 @@ theorem eraseP_replicate {n : Nat} {a : α} {p : α → Bool} :
(replicate n a).eraseP p = replicate n a := by
rw [eraseP_of_forall_not (by simp_all)]
@[grind ←]
protected theorem IsPrefix.eraseP (h : l₁ <+: l₂) : l₁.eraseP p <+: l₂.eraseP p := by
rw [IsPrefix] at h
obtain ⟨t, rfl⟩ := h
@ -258,13 +269,15 @@ theorem eraseP_eq_iff {p} {l : List α} :
subst p
simp_all
@[grind ←]
theorem Pairwise.eraseP (q) : Pairwise p l → Pairwise p (l.eraseP q) :=
Pairwise.sublist <| eraseP_sublist
@[grind]
@[grind ←]
theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
Pairwise.eraseP p
@[grind =]
theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
(l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by
induction l with
@ -357,6 +370,7 @@ theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
length (l.erase a) = length l - 1 := by
rw [erase_eq_eraseP]; exact length_eraseP_of_mem h (beq_self_eq_true a)
@[grind =]
theorem length_erase [LawfulBEq α] {a : α} {l : List α} :
length (l.erase a) = if a ∈ l then length l - 1 else length l := by
rw [erase_eq_eraseP, length_eraseP]
@ -365,11 +379,17 @@ theorem length_erase [LawfulBEq α] {a : α} {l : List α} :
theorem erase_sublist {a : α} {l : List α} : l.erase a <+ l :=
erase_eq_eraseP' a l ▸ eraseP_sublist ..
grind_pattern length_erase => l.erase a, List.Sublist
theorem erase_subset {a : α} {l : List α} : l.erase a ⊆ l := erase_sublist.subset
grind_pattern erase_subset => l.erase a, List.Subset
@[grind ←]
theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by
simp only [erase_eq_eraseP']; exact h.eraseP
@[grind ←]
theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.erase a <+: l₂.erase a := by
simp only [erase_eq_eraseP']; exact h.eraseP
@ -391,6 +411,7 @@ theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈
rw [erase_eq_eraseP', eraseP_eq_self_iff]
simp [forall_mem_ne']
@[grind _=_]
theorem erase_filter [LawfulBEq α] {f : α → Bool} {l : List α} :
(filter f l).erase a = filter f (l.erase a) := by
induction l with
@ -418,10 +439,12 @@ theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List
rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]
intros b h' h''; rw [eq_of_beq h''] at h; exact h h'
@[grind =]
theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
(l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a := by
simp [erase_eq_eraseP, eraseP_append]
@[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
rw [erase_eq_eraseP]
@ -429,6 +452,7 @@ theorem erase_replicate [LawfulBEq α] {n : Nat} {a b : α} :
-- 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 : α) {l : List α} :
(l.erase a).erase b = (l.erase b).erase a := by
if ab : a == b then rw [eq_of_beq ab] else ?_
@ -468,6 +492,7 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
rw [erase_of_not_mem]
simp_all
@[grind ←]
theorem Pairwise.erase [LawfulBEq α] {l : List α} (a) : Pairwise p l → Pairwise p (l.erase a) :=
Pairwise.sublist <| erase_sublist
@ -520,6 +545,7 @@ end erase
/-! ### eraseIdx -/
@[grind =]
theorem length_eraseIdx {l : List α} {i : Nat} :
(l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length := by
induction l generalizing i with
@ -537,8 +563,9 @@ theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
(l.eraseIdx i).length = length l - 1 := by
simp [length_eraseIdx, h]
@[simp] theorem eraseIdx_zero {l : List α} : eraseIdx l 0 = l.tail := by cases l <;> rfl
@[simp, grind =] theorem eraseIdx_zero {l : List α} : eraseIdx l 0 = l.tail := by cases l <;> rfl
@[grind =]
theorem eraseIdx_eq_take_drop_succ :
∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)
| nil, _ => by simp
@ -565,6 +592,7 @@ theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2
@[deprecated eraseIdx_ne_nil_iff (since := "2025-01-30")]
abbrev eraseIdx_ne_nil := @eraseIdx_ne_nil_iff
@[grind]
theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
| [], _ => by simp
| a::l, 0 => by simp
@ -573,6 +601,7 @@ theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
theorem mem_of_mem_eraseIdx {l : List α} {i : Nat} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l :=
(eraseIdx_sublist _ _).mem h
@[grind]
theorem eraseIdx_subset {l : List α} {k : Nat} : eraseIdx l k ⊆ l :=
(eraseIdx_sublist _ _).subset
@ -612,6 +641,15 @@ theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤
| zero => simp_all
| succ k => simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]
@[grind =]
theorem eraseIdx_append :
eraseIdx (l ++ l') k = if k < length l then eraseIdx l k ++ l' else l ++ eraseIdx l' (k - length l) := by
split <;> rename_i h
· simp [eraseIdx_append_of_lt_length h]
· rw [eraseIdx_append_of_length_le]
omega
@[grind =]
theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
(replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a := by
split <;> rename_i h
@ -623,12 +661,15 @@ theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
exact m.2
· rw [eraseIdx_of_length_le (by simpa using h)]
@[grind ←]
theorem Pairwise.eraseIdx {l : List α} (k) : Pairwise p l → Pairwise p (l.eraseIdx k) :=
Pairwise.sublist <| eraseIdx_sublist _ _
@[grind ←]
theorem Nodup.eraseIdx {l : List α} (k) : Nodup l → Nodup (l.eraseIdx k) :=
Pairwise.eraseIdx k
@[grind ←]
protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
eraseIdx l k <+: eraseIdx l' k := by
rcases h with ⟨t, rfl⟩

44
src/Init/Data/List/Nat/Erase.lean
View file

@ -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

55
src/Init/Data/Vector/Erase.lean
View file

@ -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

31
tests/lean/run/grind_list_erase.lean Normal file
View file

@ -0,0 +1,31 @@
open List
theorem eraseP_eq_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by
induction xs with grind
theorem eraseP_ne_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by
induction xs with grind
theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
length (l.eraseP p) = length l - 1 := by
grind
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
theorem eraseP_append_left {a : α} (pa : p a) {l₁ : List α} {l₂} : a ∈ l₁ → (l₁ ++ l₂).eraseP p = l₁.eraseP p ++ l₂ := by
grind
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 (splits := 9)