diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean index 827ba902f9..ef277cb58d 100644 --- a/src/Init/Data/Array.lean +++ b/src/Init/Data/Array.lean @@ -23,4 +23,5 @@ import Init.Data.Array.FinRange import Init.Data.Array.Perm import Init.Data.Array.Find import Init.Data.Array.Lex +import Init.Data.Array.Erase import Init.Data.Array.Zip diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 52fa2889b5..3f7976ae45 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -720,6 +720,9 @@ def finIdxOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) := @[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")] abbrev indexOf? := @finIdxOf? +/-- Returns the index of the first element equal to `a`, or the length of the array otherwise. -/ +def idxOf [BEq α] (a : α) : Array α → Nat := findIdx (· == a) + def idxOf? [BEq α] (a : Array α) (v : α) : Option Nat := (a.finIdxOf? v).map (·.val) diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean new file mode 100644 index 0000000000..1e907584d7 --- /dev/null +++ b/src/Init/Data/Array/Erase.lean @@ -0,0 +1,400 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Data.Array.Lemmas +import Init.Data.List.Nat.Erase +import Init.Data.List.Nat.Basic + +/-! +# Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`. +-/ + +namespace Array + +open Nat + +/-! ### eraseP -/ + +@[simp] theorem eraseP_empty : #[].eraseP p = #[] := rfl + +theorem eraseP_of_forall_mem_not {l : Array α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l := by + cases l + simp_all [List.eraseP_of_forall_not] + +theorem eraseP_of_forall_getElem_not {l : Array α} (h : ∀ i, (h : i < l.size) → ¬p l[i]) : l.eraseP p = l := + eraseP_of_forall_mem_not fun a m => by + rw [mem_iff_getElem] at m + obtain ⟨i, w, rfl⟩ := m + exact h i w + +@[simp] theorem eraseP_eq_empty_iff {xs : Array α} {p : α → Bool} : xs.eraseP p = #[] ↔ xs = #[] ∨ ∃ x, p x ∧ xs = #[x] := by + cases xs + simp + +theorem eraseP_ne_empty_iff {xs : Array α} {p : α → Bool} : xs.eraseP p ≠ #[] ↔ xs ≠ #[] ∧ ∀ x, p x → xs ≠ #[x] := by + simp + +theorem exists_of_eraseP {l : Array α} {a} (hm : a ∈ l) (hp : p a) : + ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁.push a ++ l₂ ∧ l.eraseP p = l₁ ++ l₂ := by + rcases l with ⟨l⟩ + obtain ⟨a, l₁, l₂, h₁, h₂, rfl, h₃⟩ := List.exists_of_eraseP (by simpa using hm) (hp) + refine ⟨a, ⟨l₁⟩, ⟨l₂⟩, by simpa using h₁, h₂, by simp, by simpa using h₃⟩ + +theorem exists_or_eq_self_of_eraseP (p) (l : Array α) : + l.eraseP p = l ∨ + ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁.push a ++ l₂ ∧ l.eraseP p = l₁ ++ l₂ := + if h : ∃ a ∈ l, p a then + let ⟨_, ha, pa⟩ := h + .inr (exists_of_eraseP ha pa) + else + .inl (eraseP_of_forall_mem_not (h ⟨·, ·, ·⟩)) + +@[simp] theorem size_eraseP_of_mem {l : Array α} (al : a ∈ l) (pa : p a) : + (l.eraseP p).size = l.size - 1 := by + let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa + rw [e₂]; simp [size_append, e₁]; omega + +theorem size_eraseP {l : Array α} : (l.eraseP p).size = if l.any p then l.size - 1 else l.size := by + split <;> rename_i h + · simp only [any_eq_true] at h + obtain ⟨i, h, w⟩ := h + simp [size_eraseP_of_mem (l := l) (by simp) w] + · simp only [any_eq_true] at h + rw [eraseP_of_forall_getElem_not] + simp_all + +theorem size_eraseP_le (l : Array α) : (l.eraseP p).size ≤ l.size := by + rcases l with ⟨l⟩ + simpa using List.length_eraseP_le l + +theorem le_size_eraseP (l : Array α) : l.size - 1 ≤ (l.eraseP p).size := by + rcases l with ⟨l⟩ + simpa using List.le_length_eraseP l + +theorem mem_of_mem_eraseP {l : Array α} : a ∈ l.eraseP p → a ∈ l := by + rcases l with ⟨l⟩ + simpa using List.mem_of_mem_eraseP + +@[simp] theorem mem_eraseP_of_neg {l : Array α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by + rcases l with ⟨l⟩ + simpa using List.mem_eraseP_of_neg pa + +@[simp] theorem eraseP_eq_self_iff {p} {l : Array α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by + rcases l with ⟨l⟩ + simp + +theorem eraseP_map (f : β → α) (l : Array β) : (map f l).eraseP p = map f (l.eraseP (p ∘ f)) := by + rcases l with ⟨l⟩ + simpa using List.eraseP_map f l + +theorem eraseP_filterMap (f : α → Option β) (l : Array α) : + (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false)) := by + rcases l with ⟨l⟩ + simpa using List.eraseP_filterMap f l + +theorem eraseP_filter (f : α → Bool) (l : Array α) : + (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x)) := by + rcases l with ⟨l⟩ + simpa using List.eraseP_filter f l + +theorem eraseP_append_left {a : α} (pa : p a) {l₁ : Array α} l₂ (h : a ∈ l₁) : + (l₁ ++ l₂).eraseP p = l₁.eraseP p ++ l₂ := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simpa using List.eraseP_append_left pa l₂ (by simpa using h) + +theorem eraseP_append_right {l₁ : Array α} l₂ (h : ∀ b ∈ l₁, ¬p b) : + (l₁ ++ l₂).eraseP p = l₁ ++ l₂.eraseP p := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simpa using List.eraseP_append_right l₂ (by simpa using h) + +theorem eraseP_append (l₁ l₂ : Array α) : + (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simp only [List.append_toArray, List.eraseP_toArray, List.eraseP_append l₁ l₂, List.any_toArray'] + split <;> simp + +theorem eraseP_mkArray (n : Nat) (a : α) (p : α → Bool) : + (mkArray n a).eraseP p = if p a then mkArray (n - 1) a else mkArray n a := by + simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate] + split <;> simp + +@[simp] theorem eraseP_mkArray_of_pos {n : Nat} {a : α} (h : p a) : + (mkArray n a).eraseP p = mkArray (n - 1) a := by + simp only [← List.toArray_replicate, List.eraseP_toArray] + simp [h] + +@[simp] theorem eraseP_mkArray_of_neg {n : Nat} {a : α} (h : ¬p a) : + (mkArray n a).eraseP p = mkArray n a := by + simp only [← List.toArray_replicate, List.eraseP_toArray] + simp [h] + +theorem eraseP_eq_iff {p} {l : Array α} : + l.eraseP p = l' ↔ + ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨ + ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁.push a ++ l₂ ∧ l' = l₁ ++ l₂ := by + rcases l with ⟨l⟩ + rcases l' with ⟨l'⟩ + simp [List.eraseP_eq_iff] + constructor + · rintro (h | ⟨a, l₁, h₁, h₂, ⟨x, rfl, rfl⟩⟩) + · exact Or.inl h + · exact Or.inr ⟨a, ⟨l₁⟩, by simpa using h₁, h₂, ⟨⟨x⟩, by simp⟩⟩ + · rintro (h | ⟨a, ⟨l₁⟩, h₁, h₂, ⟨⟨x⟩, rfl, rfl⟩⟩) + · exact Or.inl h + · exact Or.inr ⟨a, l₁, by simpa using h₁, h₂, ⟨x, by simp⟩⟩ + +theorem eraseP_comm {l : Array α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) : + (l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by + rcases l with ⟨l⟩ + simpa using List.eraseP_comm (by simpa using h) + +/-! ### erase -/ + +section erase +variable [BEq α] + +theorem erase_of_not_mem [LawfulBEq α] {a : α} {l : Array α} (h : a ∉ l) : l.erase a = l := by + rcases l with ⟨l⟩ + simp [List.erase_of_not_mem (by simpa using h)] + +theorem erase_eq_eraseP' (a : α) (l : Array α) : l.erase a = l.eraseP (· == a) := by + rcases l with ⟨l⟩ + simp [List.erase_eq_eraseP'] + +theorem erase_eq_eraseP [LawfulBEq α] (a : α) (l : Array α) : l.erase a = l.eraseP (a == ·) := by + rcases l with ⟨l⟩ + simp [List.erase_eq_eraseP] + +@[simp] theorem erase_eq_empty_iff [LawfulBEq α] {xs : Array α} {a : α} : + xs.erase a = #[] ↔ xs = #[] ∨ xs = #[a] := by + rcases xs with ⟨xs⟩ + simp [List.erase_eq_nil_iff] + +theorem erase_ne_empty_iff [LawfulBEq α] {xs : Array α} {a : α} : + xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a] := by + rcases xs with ⟨xs⟩ + simp [List.erase_ne_nil_iff] + +theorem exists_erase_eq [LawfulBEq α] {a : α} {l : Array α} (h : a ∈ l) : + ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁.push a ++ l₂ ∧ l.erase a = l₁ ++ l₂ := by + let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _) + rw [erase_eq_eraseP]; exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩ + +@[simp] theorem size_erase_of_mem [LawfulBEq α] {a : α} {l : Array α} (h : a ∈ l) : + (l.erase a).size = l.size - 1 := by + rw [erase_eq_eraseP]; exact size_eraseP_of_mem h (beq_self_eq_true a) + +theorem size_erase [LawfulBEq α] (a : α) (l : Array α) : + (l.erase a).size = if a ∈ l then l.size - 1 else l.size := by + rw [erase_eq_eraseP, size_eraseP] + congr + simp [mem_iff_getElem, eq_comm (a := a)] + +theorem size_erase_le (a : α) (l : Array α) : (l.erase a).size ≤ l.size := by + rcases l with ⟨l⟩ + simpa using List.length_erase_le a l + +theorem le_size_erase [LawfulBEq α] (a : α) (l : Array α) : l.size - 1 ≤ (l.erase a).size := by + rcases l with ⟨l⟩ + simpa using List.le_length_erase a l + +theorem mem_of_mem_erase {a b : α} {l : Array α} (h : a ∈ l.erase b) : a ∈ l := by + rcases l with ⟨l⟩ + simpa using List.mem_of_mem_erase (by simpa using h) + +@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : Array α} (ab : a ≠ b) : + a ∈ l.erase b ↔ a ∈ l := + erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm) + +@[simp] theorem erase_eq_self_iff [LawfulBEq α] {l : Array α} : l.erase a = l ↔ a ∉ l := by + rw [erase_eq_eraseP', eraseP_eq_self_iff] + simp [forall_mem_ne'] + +theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : Array α) : + (filter f l).erase a = filter f (l.erase a) := by + rcases l with ⟨l⟩ + simpa using List.erase_filter f l + +theorem erase_append_left [LawfulBEq α] {l₁ : Array α} (l₂) (h : a ∈ l₁) : + (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simpa using List.erase_append_left l₂ (by simpa using h) + +theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∉ l₁) : + (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a) := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simpa using List.erase_append_right l₂ (by simpa using h) + +theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : Array α} : + (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray] + split <;> simp + +theorem erase_mkArray [LawfulBEq α] (n : Nat) (a b : α) : + (mkArray n a).erase b = if b == a then mkArray (n - 1) a else mkArray n a := by + simp only [← List.toArray_replicate, List.erase_toArray] + simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate] + split <;> simp + +theorem erase_comm [LawfulBEq α] (a b : α) (l : Array α) : + (l.erase a).erase b = (l.erase b).erase a := by + rcases l with ⟨l⟩ + simpa using List.erase_comm a b l + +theorem erase_eq_iff [LawfulBEq α] {a : α} {l : Array α} : + l.erase a = l' ↔ + (a ∉ l ∧ l = l') ∨ + ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁.push a ++ l₂ ∧ l' = l₁ ++ l₂ := by + rw [erase_eq_eraseP', eraseP_eq_iff] + simp only [beq_iff_eq, forall_mem_ne', exists_and_left] + constructor + · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, x, rfl, rfl⟩) + · left; simp_all + · right; refine ⟨l', h, x, by simp⟩ + · rintro (⟨h, rfl⟩ | ⟨l₁, h, x, rfl, rfl⟩) + · left; simp_all + · right; refine ⟨a, l₁, h, rfl, x, by simp⟩ + +@[simp] theorem erase_mkArray_self [LawfulBEq α] {a : α} : + (mkArray n a).erase a = mkArray (n - 1) a := by + simp only [← List.toArray_replicate, List.erase_toArray] + simp [List.erase_replicate] + +@[simp] theorem erase_mkArray_ne [LawfulBEq α] {a b : α} (h : !b == a) : + (mkArray n a).erase b = mkArray n a := by + rw [erase_of_not_mem] + simp_all + +end erase + +/-! ### eraseIdx -/ + +theorem eraseIdx_eq_take_drop_succ (l : Array α) (i : Nat) (h) : l.eraseIdx i = l.take i ++ l.drop (i + 1) := by + rcases l with ⟨l⟩ + simp only [size_toArray] at h + simp only [List.eraseIdx_toArray, List.eraseIdx_eq_take_drop_succ, take_eq_extract, + List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, drop_eq_extract, + size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq] + rw [List.take_of_length_le] + simp + +theorem getElem?_eraseIdx (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) : + (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]? := by + rcases l with ⟨l⟩ + simp [List.getElem?_eraseIdx] + +theorem getElem?_eraseIdx_of_lt (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h' : j < i) : + (l.eraseIdx i)[j]? = l[j]? := by + rw [getElem?_eraseIdx] + simp [h'] + +theorem getElem?_eraseIdx_of_ge (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h' : i ≤ j) : + (l.eraseIdx i)[j]? = l[j + 1]? := by + rw [getElem?_eraseIdx] + simp only [dite_eq_ite, ite_eq_right_iff] + intro h' + omega + +theorem getElem_eraseIdx (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h' : j < (l.eraseIdx i).size) : + (l.eraseIdx i)[j] = if h'' : j < i then + l[j] + else + l[j + 1]'(by rw [size_eraseIdx] at h'; omega) := by + apply Option.some.inj + rw [← getElem?_eq_getElem, getElem?_eraseIdx] + split <;> simp + +@[simp] theorem eraseIdx_eq_empty_iff {l : Array α} {i : Nat} {h} : eraseIdx l i = #[] ↔ l.size = 1 ∧ i = 0 := by + rcases l with ⟨l⟩ + simp only [List.eraseIdx_toArray, mk.injEq, List.eraseIdx_eq_nil_iff, size_toArray, + or_iff_right_iff_imp] + rintro rfl + simp_all + +theorem eraseIdx_ne_empty_iff {l : Array α} {i : Nat} {h} : eraseIdx l i ≠ #[] ↔ 2 ≤ l.size := by + rcases l with ⟨_ | ⟨a, (_ | ⟨b, l⟩)⟩⟩ + · simp + · simp at h + simp [h] + · simp + +theorem mem_of_mem_eraseIdx {l : Array α} {i : Nat} {h} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l := by + rcases l with ⟨l⟩ + simpa using List.mem_of_mem_eraseIdx (by simpa using h) + +theorem eraseIdx_append_of_lt_size {l : Array α} {k : Nat} (hk : k < l.size) (l' : Array α) (h) : + eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by + rcases l with ⟨l⟩ + rcases l' with ⟨l'⟩ + simp at hk + simp [List.eraseIdx_append_of_lt_length, *] + +theorem eraseIdx_append_of_length_le {l : Array α} {k : Nat} (hk : l.size ≤ k) (l' : Array α) (h) : + eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - l.size) (by simp at h; omega) := by + rcases l with ⟨l⟩ + rcases l' with ⟨l'⟩ + simp at hk + simp [List.eraseIdx_append_of_length_le, *] + +theorem eraseIdx_mkArray {n : Nat} {a : α} {k : Nat} {h} : + (mkArray n a).eraseIdx k = mkArray (n - 1) a := by + simp at h + simp only [← List.toArray_replicate, List.eraseIdx_toArray] + simp [List.eraseIdx_replicate, h] + +theorem mem_eraseIdx_iff_getElem {x : α} {l} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i w, i ≠ k ∧ l[i]'w = x := by + rcases l with ⟨l⟩ + simp [List.mem_eraseIdx_iff_getElem, *] + +theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i ≠ k, l[i]? = some x := by + rcases l with ⟨l⟩ + simp [List.mem_eraseIdx_iff_getElem?, *] + +theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α] (l : Array α) (a : α) (i : Nat) (w : l.idxOf a = i) (h : i < l.size) : + l.erase a = l.eraseIdx i := by + rcases l with ⟨l⟩ + simp at w + simp [List.erase_eq_eraseIdx_of_idxOf, *] + +theorem getElem_eraseIdx_of_lt (l : Array α) (i : Nat) (w : i < l.size) (j : Nat) (h : j < (l.eraseIdx i).size) (h' : j < i) : + (l.eraseIdx i)[j] = l[j] := by + rcases l with ⟨l⟩ + simp [List.getElem_eraseIdx_of_lt, *] + +theorem getElem_eraseIdx_of_ge (l : Array α) (i : Nat) (w : i < l.size) (j : Nat) (h : j < (l.eraseIdx i).size) (h' : i ≤ j) : + (l.eraseIdx i)[j] = l[j + 1]'(by simp at h; omega) := by + rcases l with ⟨l⟩ + simp [List.getElem_eraseIdx_of_ge, *] + +theorem eraseIdx_set_eq {l : Array α} {i : Nat} {a : α} {h : i < l.size} : + (l.set i a).eraseIdx i (by simp; omega) = l.eraseIdx i := by + rcases l with ⟨l⟩ + simp [List.eraseIdx_set_eq, *] + +theorem eraseIdx_set_lt {l : Array α} {i : Nat} {w : i < l.size} {j : Nat} {a : α} (h : j < i) : + (l.set i a).eraseIdx j (by simp; omega) = (l.eraseIdx j).set (i - 1) a (by simp; omega) := by + rcases l with ⟨l⟩ + simp [List.eraseIdx_set_lt, *] + +theorem eraseIdx_set_gt {l : Array α} {i : Nat} {j : Nat} {a : α} (h : i < j) {w : j < l.size} : + (l.set i a).eraseIdx j (by simp; omega) = (l.eraseIdx j).set i a (by simp; omega) := by + rcases l with ⟨l⟩ + simp [List.eraseIdx_set_gt, *] + +@[simp] theorem set_getElem_succ_eraseIdx_succ + {l : Array α} {i : Nat} (h : i + 1 < l.size) : + (l.eraseIdx (i + 1)).set i l[i + 1] (by simp; omega) = l.eraseIdx i := by + rcases l with ⟨l⟩ + simp [List.set_getElem_succ_eraseIdx_succ, *] + +end Array diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index ab59af0fa4..fbf25dea0a 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -1277,7 +1277,7 @@ theorem findSome?_cons {f : α → Option β} : @[simp] theorem findIdx_nil {α : Type _} (p : α → Bool) : [].findIdx p = 0 := rfl -/-! ### indexOf -/ +/-! ### idxOf -/ /-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/ def idxOf [BEq α] (a : α) : List α → Nat := findIdx (· == a) @@ -1300,7 +1300,7 @@ where | [], _ => none | a :: l, i => if p a then some i else go l (i + 1) -/-! ### indexOf? -/ +/-! ### idxOf? -/ /-- Return the index of the first occurrence of `a` in the list. -/ @[inline] def idxOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a) diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index 25cbf623a0..ccdd9ec667 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -9,7 +9,7 @@ import Init.Data.List.Pairwise import Init.Data.List.Find /-! -# Lemmas about `List.eraseP` and `List.erase`. +# Lemmas about `List.eraseP`, `List.erase`, and `List.eraseIdx`. -/ namespace List @@ -34,7 +34,7 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er | nil => rfl | cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2] -@[simp] theorem eraseP_eq_nil {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by +@[simp] theorem eraseP_eq_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by induction xs with | nil => simp | cons x xs ih => @@ -50,9 +50,15 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er rintro x h' rfl simp_all -theorem eraseP_ne_nil {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by +@[deprecated eraseP_eq_nil_iff (since := "2025-01-30")] +abbrev eraseP_eq_nil := @eraseP_eq_nil_iff + +theorem eraseP_ne_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by simp +@[deprecated eraseP_ne_nil_iff (since := "2025-01-30")] +abbrev eraseP_ne_nil := @eraseP_ne_nil_iff + theorem exists_of_eraseP : ∀ {l : List α} {a} (_ : a ∈ l) (_ : p a), ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂ | b :: l, _, al, pa => @@ -191,6 +197,14 @@ theorem eraseP_replicate (n : Nat) (a : α) (p : α → Bool) : simp only [replicate_succ, eraseP_cons] split <;> simp [*] +@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) : + (replicate n a).eraseP p = replicate (n - 1) a := by + cases n <;> simp [replicate_succ, h] + +@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) : + (replicate n a).eraseP p = replicate n a := by + rw [eraseP_of_forall_not (by simp_all)] + protected theorem IsPrefix.eraseP (h : l₁ <+: l₂) : l₁.eraseP p <+: l₂.eraseP p := by rw [IsPrefix] at h obtain ⟨t, rfl⟩ := h @@ -237,14 +251,6 @@ theorem eraseP_eq_iff {p} {l : List α} : subst p simp_all -@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) : - (replicate n a).eraseP p = replicate (n - 1) a := by - cases n <;> simp [replicate_succ, h] - -@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) : - (replicate n a).eraseP p = replicate n a := by - rw [eraseP_of_forall_not (by simp_all)] - theorem Pairwise.eraseP (q) : Pairwise p l → Pairwise p (l.eraseP q) := Pairwise.sublist <| eraseP_sublist _ @@ -286,6 +292,7 @@ theorem eraseP_eq_eraseIdx {xs : List α} {p : α → Bool} : split <;> simp [*] /-! ### erase -/ + section erase variable [BEq α] @@ -313,16 +320,22 @@ theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ l : List α, l.erase a = | b :: l => by if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l] -@[simp] theorem erase_eq_nil [LawfulBEq α] {xs : List α} {a : α} : +@[simp] theorem erase_eq_nil_iff [LawfulBEq α] {xs : List α} {a : α} : xs.erase a = [] ↔ xs = [] ∨ xs = [a] := by rw [erase_eq_eraseP] simp -theorem erase_ne_nil [LawfulBEq α] {xs : List α} {a : α} : +@[deprecated erase_eq_nil_iff (since := "2025-01-30")] +abbrev erase_eq_nil := @erase_eq_nil_iff + +theorem erase_ne_nil_iff [LawfulBEq α] {xs : List α} {a : α} : xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a] := by rw [erase_eq_eraseP] simp +@[deprecated erase_ne_nil_iff (since := "2025-01-30")] +abbrev erase_ne_nil := @erase_ne_nil_iff + theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ := by let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _) @@ -471,7 +484,7 @@ theorem head_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).head h ∈ xs theorem getLast_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).getLast h ∈ xs := (erase_sublist a xs).getLast_mem h -theorem erase_eq_eraseIdx [LawfulBEq α] (l : List α) (a : α) : +theorem erase_eq_eraseIdx (l : List α) (a : α) : l.erase a = match l.idxOf? a with | none => l | some i => l.eraseIdx i := by @@ -515,18 +528,24 @@ theorem eraseIdx_eq_take_drop_succ : -- See `Init.Data.List.Nat.Erase` for `getElem?_eraseIdx` and `getElem_eraseIdx`. -@[simp] theorem eraseIdx_eq_nil {l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0) := by +@[simp] theorem eraseIdx_eq_nil_iff {l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0) := by match l, i with | [], _ | a::l, 0 | a::l, i + 1 => simp [Nat.succ_inj'] -theorem eraseIdx_ne_nil {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2 ≤ l.length ∨ (l.length = 1 ∧ i ≠ 0) := by +@[deprecated eraseIdx_eq_nil_iff (since := "2025-01-30")] +abbrev eraseIdx_eq_nil := @eraseIdx_eq_nil_iff + +theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2 ≤ l.length ∨ (l.length = 1 ∧ i ≠ 0) := by match l with | [] | [a] | a::b::l => simp [Nat.succ_inj'] +@[deprecated eraseIdx_ne_nil_iff (since := "2025-01-30")] +abbrev eraseIdx_ne_nil := @eraseIdx_ne_nil_iff + theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l | [], _ => by simp | a::l, 0 => by simp diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 17d7ebfcd3..3f275c5360 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -886,6 +886,14 @@ theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l List.findIdx? p l₂ = none → List.findIdx? p l₁ = none := h.sublist.findIdx?_eq_none +theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} : + xs.findIdx p = (xs.findIdx? p).getD xs.length := by + induction xs with + | nil => simp + | cons x xs ih => + simp only [findIdx_cons, findIdx?_cons] + split <;> simp_all [ih] + /-! ### findFinIdx? -/ theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} : diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 3265ce85ce..aa689cf6a0 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -528,16 +528,24 @@ termination_by xs.length - i rw [findFinIdx?_go_beq_eq_idxOfAux_toArray] simp +@[simp] theorem findIdx_toArray [BEq α] {as : List α} {p : α → Bool} : + as.toArray.findIdx p = as.findIdx p := by + rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?] + @[simp] theorem idxOf?_toArray [BEq α] {as : List α} {a : α} : as.toArray.idxOf? a = as.idxOf? a := by rw [Array.idxOf?, finIdxOf?_toArray, idxOf?_eq_map_finIdxOf?_val] +@[simp] theorem idxOf_toArray [BEq α] {as : List α} {a : α} : + as.toArray.idxOf a = as.idxOf a := by + rw [Array.idxOf, findIdx_toArray, idxOf] + @[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} : as.toArray.eraseP p = (as.eraseP p).toArray := by rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray] split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] -@[simp] theorem erase_toArray [BEq α] [LawfulBEq α] {as : List α} {a : α} : +@[simp] theorem erase_toArray [BEq α] {as : List α} {a : α} : as.toArray.erase a = (as.erase a).toArray := by rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx] rw [idxOf?_eq_map_finIdxOf?_val] diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean index e6474dd81f..adbb9caf2e 100644 --- a/src/Init/Data/Vector.lean +++ b/src/Init/Data/Vector.lean @@ -12,3 +12,4 @@ import Init.Data.Vector.Count import Init.Data.Vector.DecidableEq import Init.Data.Vector.Zip import Init.Data.Vector.OfFn +import Init.Data.Vector.Erase diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index a68512ced9..23d1f04641 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -71,7 +71,7 @@ theorem countP_le_size {l : Vector α n} : countP p l ≤ n := by theorem countP_mkVector (p : α → Bool) (a : α) (n : Nat) : countP p (mkVector n a) = if p a then n else 0 := by - simp only [mkVector_eq_toVector_mkArray, countP_cast, countP_mk] + simp only [mkVector_eq_mk_mkArray, countP_cast, countP_mk] simp [Array.countP_mkArray] theorem boole_getElem_le_countP (p : α → Bool) (l : Vector α n) (i : Nat) (h : i < n) : @@ -213,11 +213,11 @@ theorem count_eq_size {l : Vector α n} : count a l = l.size ↔ ∀ b ∈ l, a simp [Array.count_eq_size] @[simp] theorem count_mkVector_self (a : α) (n : Nat) : count a (mkVector n a) = n := by - simp only [mkVector_eq_toVector_mkArray, count_cast, count_mk] + simp only [mkVector_eq_mk_mkArray, count_cast, count_mk] simp theorem count_mkVector (a b : α) (n : Nat) : count a (mkVector n b) = if b == a then n else 0 := by - simp only [mkVector_eq_toVector_mkArray, count_cast, count_mk] + simp only [mkVector_eq_mk_mkArray, count_cast, count_mk] simp [Array.count_mkArray] theorem count_le_count_map [DecidableEq β] (l : Vector α n) (f : α → β) (x : α) : diff --git a/src/Init/Data/Vector/Erase.lean b/src/Init/Data/Vector/Erase.lean new file mode 100644 index 0000000000..53b144c3fa --- /dev/null +++ b/src/Init/Data/Vector/Erase.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Data.Vector.Lemmas +import Init.Data.Array.Erase + +/-! +# Lemmas about `Vector.eraseIdx`. +-/ + +namespace Vector + +open Nat + +/-! ### eraseIdx -/ + +theorem eraseIdx_eq_take_drop_succ (l : Vector α n) (i : Nat) (h) : + l.eraseIdx i = (l.take i ++ l.drop (i + 1)).cast (by omega) := by + rcases l with ⟨l, rfl⟩ + simp [Array.eraseIdx_eq_take_drop_succ, *] + +theorem getElem?_eraseIdx (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) : + (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]? := by + rcases l with ⟨l, rfl⟩ + simp [Array.getElem?_eraseIdx] + +theorem getElem?_eraseIdx_of_lt (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < i) : + (l.eraseIdx i)[j]? = l[j]? := by + rw [getElem?_eraseIdx] + simp [h'] + +theorem getElem?_eraseIdx_of_ge (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : i ≤ j) : + (l.eraseIdx i)[j]? = l[j + 1]? := by + rw [getElem?_eraseIdx] + simp only [dite_eq_ite, ite_eq_right_iff] + intro h' + omega + +theorem getElem_eraseIdx (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < n - 1) : + (l.eraseIdx i)[j] = if h'' : j < i then l[j] else l[j + 1] := by + apply Option.some.inj + rw [← getElem?_eq_getElem, getElem?_eraseIdx] + split <;> simp + +theorem mem_of_mem_eraseIdx {l : Vector α n} {i : Nat} {h} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l := by + rcases l with ⟨l, rfl⟩ + simpa using Array.mem_of_mem_eraseIdx (by simpa using h) + +theorem eraseIdx_append_of_lt_size {l : Vector α n} {k : Nat} (hk : k < n) (l' : Vector α n) (h) : + eraseIdx (l ++ l') k = (eraseIdx l k ++ l').cast (by omega) := by + rcases l with ⟨l⟩ + rcases l' with ⟨l'⟩ + simp [Array.eraseIdx_append_of_lt_size, *] + +theorem eraseIdx_append_of_length_le {l : Vector α n} {k : Nat} (hk : n ≤ k) (l' : Vector α n) (h) : + eraseIdx (l ++ l') k = (l ++ eraseIdx l' (k - n)).cast (by omega) := by + rcases l with ⟨l⟩ + rcases l' with ⟨l'⟩ + simp [Array.eraseIdx_append_of_length_le, *] + +theorem eraseIdx_cast {l : Vector α n} {k : Nat} (h : k < m) : + eraseIdx (l.cast w) k h = (eraseIdx l k).cast (by omega) := by + rcases l with ⟨l, rfl⟩ + simp + +theorem eraseIdx_mkVector {n : Nat} {a : α} {k : Nat} {h} : + (mkVector n a).eraseIdx k = mkVector (n - 1) a := by + rw [mkVector_eq_mk_mkArray, eraseIdx_mk] + simp [Array.eraseIdx_mkArray, *] + +theorem mem_eraseIdx_iff_getElem {x : α} {l : Vector α n} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i w, i ≠ k ∧ l[i]'w = x := by + rcases l with ⟨l, rfl⟩ + simp [Array.mem_eraseIdx_iff_getElem, *] + +theorem mem_eraseIdx_iff_getElem? {x : α} {l : Vector α n} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i ≠ k, l[i]? = some x := by + rcases l with ⟨l, rfl⟩ + simp [Array.mem_eraseIdx_iff_getElem?, *] + +theorem getElem_eraseIdx_of_lt (l : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : j < i) : + (l.eraseIdx i)[j] = l[j] := by + rcases l with ⟨l, rfl⟩ + simp [Array.getElem_eraseIdx_of_lt, *] + +theorem getElem_eraseIdx_of_ge (l : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : i ≤ j) : + (l.eraseIdx i)[j] = l[j + 1] := by + rcases l with ⟨l, rfl⟩ + simp [Array.getElem_eraseIdx_of_ge, *] + +theorem eraseIdx_set_eq {l : Vector α n} {i : Nat} {a : α} {h : i < n} : + (l.set i a).eraseIdx i = l.eraseIdx i := by + rcases l with ⟨l, rfl⟩ + simp [Array.eraseIdx_set_eq, *] + +theorem eraseIdx_set_lt {l : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) : + (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by + rcases l with ⟨l, rfl⟩ + simp [Array.eraseIdx_set_lt, *] + +theorem eraseIdx_set_gt {l : Vector α n} {i : Nat} {j : Nat} {a : α} (h : i < j) {w : j < n} : + (l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by + rcases l with ⟨l, rfl⟩ + simp [Array.eraseIdx_set_gt, *] + +@[simp] theorem set_getElem_succ_eraseIdx_succ + {l : Vector α n} {i : Nat} (h : i + 1 < n) : + (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by + rcases l with ⟨l, rfl⟩ + simp [List.set_getElem_succ_eraseIdx_succ, *] + +end Vector diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 2505e2af91..af14d71af3 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -589,11 +589,11 @@ theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by @[simp] theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj] -@[simp] theorem _root_.Array.toVector_mkArray (a : α) (n : Nat) : - (Array.mkArray n a).toVector = (mkVector n a).cast (by simp) := rfl +@[simp] theorem _root_.Array.mk_mkArray (a : α) (n : Nat) (h : (mkArray n a).size = m) : + mk (Array.mkArray n a) h = (mkVector n a).cast (by simpa using h) := rfl -theorem mkVector_eq_toVector_mkArray (a : α) (n : Nat) : - mkVector n a = (Array.mkArray n a).toVector.cast (by simp) := by +theorem mkVector_eq_mk_mkArray (a : α) (n : Nat) : + mkVector n a = mk (mkArray n a) (by simp) := by simp /-! ## L[i] and L[i]? -/ @@ -1770,6 +1770,7 @@ theorem mkVector_succ' : mkVector (n + 1) a = (#v[a] ++ mkVector n a).cast (by o @[simp] theorem mem_mkVector {a b : α} {n} : b ∈ mkVector n a ↔ n ≠ 0 ∧ b = a := by unfold mkVector + simp only [mem_mk] simp theorem eq_of_mem_mkVector {a b : α} {n} (h : b ∈ mkVector n a) : b = a := (mem_mkVector.1 h).2 @@ -1779,7 +1780,8 @@ theorem forall_mem_mkVector {p : α → Prop} {a : α} {n} : cases n <;> simp [mem_mkVector] @[simp] theorem getElem_mkVector (a : α) (n i : Nat) (h : i < n) : (mkVector n a)[i] = a := by - simp [mkVector] + rw [mkVector_eq_mk_mkArray, getElem_mk] + simp theorem getElem?_mkVector (a : α) (n i : Nat) : (mkVector n a)[i]? = if i < n then some a else none := by simp [getElem?_def]