diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 3a790fcdeb..1b10320836 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -135,6 +135,9 @@ theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b := by simp [getElem?_def] +theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a := + getElem?_eq_some_iff.mp + theorem some_eq_getElem?_iff {xs : Array α} : some b = xs[i]? ↔ ∃ h : i < xs.size, xs[i] = b := by rw [eq_comm, getElem?_eq_some_iff] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 10ae9534a3..f5265db1f0 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -68,6 +68,9 @@ theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, · simp_all · simp; omega +theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a := + getElem?_eq_some_iff.mp + set_option linter.missingDocs false in @[deprecated getElem?_eq_some_iff (since := "2025-02-17")] abbrev getElem?_eq_some := @getElem?_eq_some_iff diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index c7244cfa4d..3f7bff3dde 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -259,6 +259,9 @@ theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.le · match i, h with | i + 1, h => simp [getElem?_eq_some_iff, Nat.succ_lt_succ_iff] +theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.length, l[i] = a := + getElem?_eq_some_iff.mp + theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a := by rw [eq_comm, getElem?_eq_some_iff] @@ -711,8 +714,8 @@ theorem set_set (a : α) {b : α} : ∀ {l : List α} {i : Nat}, (l.set i a).set theorem mem_set {l : List α} {i : Nat} (h : i < l.length) (a : α) : a ∈ l.set i a := by - simp [mem_iff_getElem] - exact ⟨i, (by simpa using h), by simp⟩ + simp only [mem_iff_getElem] + exact ⟨i, by simpa using h, by simp⟩ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.set i b → a ∈ l ∨ a = b | _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _) @@ -827,9 +830,15 @@ theorem getElem_length_sub_one_eq_getLast {l : List α} (h : l.length - 1 < l.le l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by rw [← getLast_eq_getElem] +@[simp] theorem getLast_cons_cons {a : α} {l : List α} : + getLast (a :: b :: l) (by simp) = getLast (b :: l) (by simp) := by + rfl + theorem getLast_cons {a : α} {l : List α} : ∀ (h : l ≠ nil), getLast (a :: l) (cons_ne_nil a l) = getLast l h := by - induction l <;> intros; {contradiction}; rfl + induction l <;> intros + · contradiction + · rfl theorem getLast_eq_getLastD {a l} (h) : @getLast α (a::l) h = getLastD l a := by cases l <;> rfl @@ -1296,7 +1305,7 @@ abbrev filter_length_eq_length := @length_filter_eq_length_iff @[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by induction as with - | nil => simp [filter] + | nil => simp | cons a as ih => by_cases h : p a · simp_all [or_and_left] @@ -1362,12 +1371,9 @@ theorem filter_eq_cons_iff {l} {a} {as} : split at h <;> rename_i w · simp only [cons.injEq] at h obtain ⟨rfl, rfl⟩ := h - refine ⟨[], l, ?_⟩ - simp [w] - · specialize ih h - obtain ⟨l₁, l₂, rfl, w₁, w₂, w₃⟩ := ih - refine ⟨x :: l₁, l₂, ?_⟩ - simp_all + exact ⟨[], l, by simp [w]⟩ + · obtain ⟨l₁, l₂, rfl, w₁, w₂, w₃⟩ := ih h + exact ⟨x :: l₁, l₂, by simp_all⟩ · rintro ⟨l₁, l₂, rfl, h₁, h, h₂⟩ simp [h₂, filter_cons, filter_eq_nil_iff.mpr h₁, h] @@ -2046,7 +2052,7 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)}, | _, [] => by simp_all | [], _ :: _ => by simp_all | _ :: _, _ :: _ => by - simp + simp only [cons.injEq, flatten_cons, map_cons] rw [eq_iff_flatten_eq] constructor · rintro ⟨rfl, h₁, h₂⟩ @@ -2709,12 +2715,12 @@ theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] : -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification. theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁} (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by - induction l generalizing init <;> simp [*, H] + induction l generalizing init <;> simp [*] -- The argument `f : β₁ → β₂` is intentionally explicit, as it is sometimes not found by unification. theorem foldr_hom (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ : α → β₂ → β₂} {l : List α} {init : β₁} (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by - induction l <;> simp [*, H] + induction l <;> simp [*] /-- A reasoning principle for proving propositions about the result of `List.foldl` by establishing an @@ -3260,6 +3266,10 @@ theorem eq_or_mem_of_mem_insert {l : List α} (h : a ∈ l.insert b) : a = b ∨ @[simp] theorem length_insert_of_not_mem {l : List α} (h : a ∉ l) : length (l.insert a) = length l + 1 := by rw [insert_of_not_mem h]; rfl +theorem length_insert {l : List α} : + (l.insert a).length = l.length + if a ∈ l then 0 else 1 := by + split <;> simp_all + theorem length_le_length_insert {l : List α} {a : α} : l.length ≤ (l.insert a).length := by by_cases h : a ∈ l · rw [length_insert_of_mem h] diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 283841a427..875b040f8f 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -824,6 +824,9 @@ theorem getElem?_eq_none {xs : Vector α n} (h : n ≤ i) : xs[i]? = none := by theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b ↔ ∃ h : i < n, xs[i] = b := by simp [getElem?_def] +theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a → ∃ h : i < n, xs[i] = a := + getElem?_eq_some_iff.mp + theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? ↔ ∃ h : i < n, xs[i] = b := by rw [eq_comm, getElem?_eq_some_iff]