From cf3b257ccd2599e0bee2116f046a3a9f52f35e76 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 10 Apr 2025 20:53:30 +0200 Subject: [PATCH] chore: `Option` cleanup (#7897) This PR cleans up the `Option` development, upstreaming some results from mathlib in the process. Notable changes: - the name `_eq_some_iff` is preferred over `_eq_some` - the `simp` normal form for `<$>` is `Option.map`, for `>>=` is `Option.bind` and for `<|>` is `Option.orElse` (for the former two, this was already true before this PR). All further lemmas about these operations are now stated only in terms of `Option.map`/`Option.bind`/`Option.orElse`. Previously, in some cases both versions were available, with a prime used to disambiguate (the primed version was usually the "non-ascii-art" version). Now, there are no lemmas about the ascii-art versions besides the ones turning them into the non-ascii-art operations, and there is only one version of every lemma, about the non-ascii-art operation, and named without a prime. --- src/Init/Data/List/Attach.lean | 2 +- src/Init/Data/List/Find.lean | 8 +- src/Init/Data/List/MapIdx.lean | 2 +- src/Init/Data/Option/Attach.lean | 6 +- src/Init/Data/Option/Basic.lean | 5 +- src/Init/Data/Option/Instances.lean | 24 ++- src/Init/Data/Option/Lemmas.lean | 174 ++++++++++++++---- src/Init/Data/Vector/Lemmas.lean | 2 +- .../DHashMap/Internal/AssocList/Lemmas.lean | 4 +- src/Std/Data/DHashMap/Internal/Model.lean | 2 +- src/Std/Data/DHashMap/Internal/WF.lean | 2 +- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 2 +- src/Std/Data/Internal/List/Associative.lean | 48 ++--- tests/lean/run/grind_list.lean | 2 +- tests/lean/run/grind_t1.lean | 8 +- tests/lean/run/grind_trace.lean | 6 +- 16 files changed, 199 insertions(+), 98 deletions(-) diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index e55ed96544..c16c94231d 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -477,7 +477,7 @@ theorem attach_filterMap {l : List α} {f : α → Option β} : · simp only [h] rfl rw [ih] - simp only [map_filterMap, Option.map_pbind, Option.map_some'] + simp only [map_filterMap, Option.map_pbind, Option.map_some] rfl · simp only [Option.pbind_eq_some_iff] at h obtain ⟨a, h, w⟩ := h diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 9524e62bff..931ec0c456 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -95,10 +95,10 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} : | cons x xs ih => simp [guard, findSome?, find?] split <;> rename_i h - · simp only [Option.guard_eq_some] at h + · simp only [Option.guard_eq_some_iff] at h obtain ⟨rfl, h⟩ := h simp [h] - · simp only [Option.guard_eq_none] at h + · simp only [Option.guard_eq_none_iff] at h simp [ih, h] theorem find?_eq_findSome?_guard {l : List α} : find? p l = findSome? (Option.guard fun x => p x) l := @@ -768,7 +768,7 @@ theorem findIdx?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {i : Nat} not_and, Classical.not_forall, Bool.not_eq_false] intros refine ⟨0, zero_lt_succ i, ‹_›⟩ - · simp only [Option.map_eq_some', ih, Bool.not_eq_true, length_cons] + · simp only [Option.map_eq_some_iff, ih, Bool.not_eq_true, length_cons] constructor · rintro ⟨a, ⟨⟨h, h₁, h₂⟩, rfl⟩⟩ refine ⟨Nat.succ_lt_succ_iff.mpr h, by simpa, fun j hj => ?_⟩ @@ -824,7 +824,7 @@ abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none (xs ++ ys : List α).findIdx? p = (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.length) := by induction xs with simp - | cons _ _ _ => split <;> simp_all [Option.map_or', Option.map_map]; rfl + | cons _ _ _ => split <;> simp_all [Option.map_or, Option.map_map]; rfl theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} : l.flatten.findIdx? p = diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index 318f63237c..687b1771f2 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -339,7 +339,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat}, if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]? | [], acc, i => by simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList, - ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none'] + ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none] | a :: l, acc, i => by rw [mapIdx.go, getElem?_mapIdx_go] simp only [Array.size_push] diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index 5ac2034a52..215c8c49f2 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -141,11 +141,11 @@ theorem toList_attach (o : Option α) : cases o <;> simp theorem attach_map {o : Option α} (f : α → β) : - (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some.2 ⟨_, h, rfl⟩⟩) := by + (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by cases o <;> simp theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} : - (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some.2 ⟨_, h, rfl⟩))).map + (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some_iff.2 ⟨_, h, rfl⟩))).map fun ⟨x, h⟩ => ⟨f x, h⟩ := by cases o <;> simp @@ -174,7 +174,7 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o theorem attach_bind {o : Option α} {f : α → Option β} : (o.bind f).attach = - o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some.2 ⟨_, h, h'⟩⟩ := by + o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by cases o <;> simp theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} : diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index a9c2d697e2..d1eb928b0e 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -231,13 +231,12 @@ def merge (fn : α → α → α) : Option α → Option α → Option α @[simp] theorem getD_none : getD none a = a := rfl @[simp] theorem getD_some : getD (some a) b = a := rfl -@[simp] theorem map_none' (f : α → β) : none.map f = none := rfl -@[simp] theorem map_some' (a) (f : α → β) : (some a).map f = some (f a) := rfl +@[simp] theorem map_none (f : α → β) : none.map f = none := rfl +@[simp] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl @[simp] theorem none_bind (f : α → Option β) : none.bind f = none := rfl @[simp] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl - /-- A case analysis function for `Option`. diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index b4d50bfb48..88bdbc4779 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -39,18 +39,24 @@ This is not an instance because it is not definitionally equal to the standard i Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead. -/ -@[inline] def decidable_eq_none {o : Option α} : Decidable (o = none) := +@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) := decidable_of_decidable_of_iff isNone_iff_eq_none -instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∀ a, a ∈ o → p a) -| none => isTrue nofun -| some a => - if h : p a then isTrue fun _ e => some_inj.1 e ▸ h - else isFalse <| mt (· _ rfl) h +@[deprecated decidableEqNone (since := "2025-04-10"), inline] +def decidable_eq_none {o : Option α} : Decidable (o = none) := + decidableEqNone -instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (Exists fun a => a ∈ o ∧ p a) -| none => isFalse nofun -| some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn +instance decidableForallMem {p : α → Prop} [DecidablePred p] : + ∀ o : Option α, Decidable (∀ a, a ∈ o → p a) + | none => isTrue nofun + | some a => + if h : p a then isTrue fun _ e => some_inj.1 e ▸ h + else isFalse <| mt (· _ rfl) h + +instance decidableExistsMem {p : α → Prop} [DecidablePred p] : + ∀ o : Option α, Decidable (Exists fun a => a ∈ o ∧ p a) + | none => isFalse nofun + | some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn /-- Given an optional value and a function that can be applied when the value is `some`, returns the diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 982de8b42c..ef74fd4f83 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -17,6 +17,8 @@ theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl theorem mem_some {a b : α} : a ∈ some b ↔ b = a := by simp +theorem mem_some_iff {a b : α} : a ∈ some b ↔ b = a := mem_some + theorem mem_some_self (a : α) : a ∈ some a := rfl theorem some_ne_none (x : α) : some x ≠ none := nofun @@ -29,6 +31,9 @@ protected theorem «exists» {p : Option α → Prop} : ⟨fun | ⟨none, hx⟩ => .inl hx | ⟨some x, hx⟩ => .inr ⟨x, hx⟩, fun | .inl h => ⟨_, h⟩ | .inr ⟨_, hx⟩ => ⟨_, hx⟩⟩ +theorem eq_none_or_eq_some (a : Option α) : a = none ∨ ∃ x, a = some x := + Option.exists.mp exists_eq' + theorem get_mem : ∀ {o : Option α} (h : isSome o), o.get h ∈ o | some _, _ => rfl @@ -88,6 +93,9 @@ set_option Elab.async false theorem eq_none_iff_forall_ne_some : o = none ↔ ∀ a, o ≠ some a := by cases o <;> simp +theorem eq_none_iff_forall_some_ne : o = none ↔ ∀ a, some a ≠ o := by + cases o <;> simp + theorem eq_none_iff_forall_not_mem : o = none ↔ ∀ a, a ∉ o := eq_none_iff_forall_ne_some @@ -102,9 +110,30 @@ theorem isSome_of_mem {x : Option α} {y : α} (h : y ∈ x) : x.isSome := by theorem isSome_of_eq_some {x : Option α} {y : α} (h : x = some y) : x.isSome := by cases x <;> trivial -@[simp] theorem not_isSome : isSome a = false ↔ a.isNone = true := by +@[simp] theorem isSome_eq_false_iff : isSome a = false ↔ a.isNone = true := by cases a <;> simp +@[simp] theorem isNone_eq_false_iff : isNone a = false ↔ a.isSome = true := by + cases a <;> simp + +@[simp] +theorem not_isSome (a : Option α) : (!a.isSome) = a.isNone := by + cases a <;> simp + +@[simp] +theorem not_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone := by + funext + simp + +@[simp] +theorem not_isNone (a : Option α) : (!a.isNone) = a.isSome := by + cases a <;> simp + +@[simp] +theorem not_comp_isNone : (!·) ∘ @Option.isNone α = Option.isSome := by + funext x + simp + theorem eq_some_iff_get_eq : o = some a ↔ ∃ h : o.isSome, o.get h = a := by cases o <;> simp @@ -146,17 +175,25 @@ abbrev ball_ne_none := @forall_ne_none @[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl +@[simp] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl + @[simp] theorem bind_some (x : Option α) : x.bind some = x := by cases x <;> rfl @[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by cases x <;> rfl -theorem bind_eq_some : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by +theorem bind_eq_some_iff : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by cases x <;> simp -@[simp] theorem bind_eq_none {o : Option α} {f : α → Option β} : +@[deprecated bind_eq_some_iff (since := "2025-04-10")] +abbrev bind_eq_some := @bind_eq_some_iff + +@[simp] theorem bind_eq_none_iff {o : Option α} {f : α → Option β} : o.bind f = none ↔ ∀ a, o = some a → f a = none := by cases o <;> simp +@[deprecated bind_eq_none_iff (since := "2025-04-10")] +abbrev bind_eq_none := @bind_eq_none_iff + theorem bind_eq_none' {o : Option α} {f : α → Option β} : o.bind f = none ↔ ∀ b a, o = some a → f a ≠ some b := by cases o <;> simp [eq_none_iff_forall_ne_some] @@ -193,50 +230,67 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α → (isSome_apply_of_isSome_bind h) := by cases x <;> trivial -theorem join_eq_some : x.join = some a ↔ x = some (some a) := by - simp [bind_eq_some] +theorem join_eq_some_iff : x.join = some a ↔ x = some (some a) := by + simp [bind_eq_some_iff] + +@[deprecated join_eq_some_iff (since := "2025-04-10")] +abbrev join_eq_some := @join_eq_some_iff theorem join_ne_none : x.join ≠ none ↔ ∃ z, x = some (some z) := by - simp only [ne_none_iff_exists', join_eq_some, iff_self] + simp only [ne_none_iff_exists', join_eq_some_iff, iff_self] theorem join_ne_none' : ¬x.join = none ↔ ∃ z, x = some (some z) := join_ne_none -theorem join_eq_none : o.join = none ↔ o = none ∨ o = some none := +theorem join_eq_none_iff : o.join = none ↔ o = none ∨ o = some none := match o with | none | some none | some (some _) => by simp +@[deprecated join_eq_none_iff (since := "2025-04-10")] +abbrev join_eq_none := @join_eq_none_iff + theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl @[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl -theorem map_none : f <$> none = none := rfl +@[deprecated map_none (since := "2025-04-10")] +abbrev map_none' := @map_none -theorem map_some : f <$> some a = some (f a) := rfl +@[deprecated map_some (since := "2025-04-10")] +abbrev map_some' := @map_some -@[simp] theorem map_eq_some' : x.map f = some b ↔ ∃ a, x = some a ∧ f a = b := by cases x <;> simp - -theorem map_eq_some : f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_eq_some' - -@[simp] theorem map_eq_none' : x.map f = none ↔ x = none := by - cases x <;> simp [map_none', map_some', eq_self_iff_true] - -theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by +@[simp] theorem map_eq_some_iff : x.map f = some b ↔ ∃ a, x = some a ∧ f a = b := by cases x <;> simp -@[simp] theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome := by +@[deprecated map_eq_some_iff (since := "2025-04-10")] +abbrev map_eq_some := @map_eq_some_iff + +@[deprecated map_eq_some_iff (since := "2025-04-10")] +abbrev map_eq_some' := @map_eq_some_iff + +@[simp] theorem map_eq_none_iff : x.map f = none ↔ x = none := by + cases x <;> simp [map_none, map_some, eq_self_iff_true] + +@[deprecated map_eq_none_iff (since := "2025-04-10")] +abbrev map_eq_none := @map_eq_none_iff + +@[deprecated map_eq_none_iff (since := "2025-04-10")] +abbrev map_eq_none' := @map_eq_none_iff + +@[simp] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by cases x <;> simp -@[simp] theorem isNone_map' {x : Option α} : (x.map f).isNone = x.isNone := by - cases x <;> simp +@[deprecated isSome_map (since := "2025-04-10")] +abbrev isSome_map' := @isSome_map -theorem map_eq_none : f <$> x = none ↔ x = none := map_eq_none' +@[simp] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by + cases x <;> simp theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f) := by cases x <;> simp [Option.bind] theorem map_congr {x : Option α} (h : ∀ a, x = some a → f a = g a) : x.map f = x.map g := by - cases x <;> simp only [map_none', map_some', h] + cases x <;> simp only [map_none, map_some, h] @[simp] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by funext; simp [map_id] @@ -254,7 +308,7 @@ theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} : @[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) : (x.map g).map h = x.map (h ∘ g) := by - cases x <;> simp only [map_none', map_some', ·∘·] + cases x <;> simp only [map_none, map_some, ·∘·] theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ g) = (x.map g).map h := (map_map ..).symm @@ -262,7 +316,7 @@ theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ @[simp] theorem map_comp_map (f : α → β) (g : β → γ) : Option.map g ∘ Option.map f = Option.map (g ∘ f) := by funext x; simp -theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some' .. +theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some .. theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y → x = y) : o.map f = o'.map f ↔ o = o' := by @@ -292,11 +346,14 @@ theorem isSome_of_isSome_filter (p : α → Bool) (o : Option α) (h : (o.filter @[deprecated isSome_of_isSome_filter (since := "2025-03-18")] abbrev isSome_filter_of_isSome := @isSome_of_isSome_filter -@[simp] theorem filter_eq_none {o : Option α} {p : α → Bool} : +@[simp] theorem filter_eq_none_iff {o : Option α} {p : α → Bool} : o.filter p = none ↔ ∀ a, o = some a → ¬ p a := by cases o <;> simp [filter_some] -@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} : +@[deprecated filter_eq_none_iff (since := "2025-04-10")] +abbrev filter_eq_none := @filter_eq_none_iff + +@[simp] theorem filter_eq_some_iff {o : Option α} {p : α → Bool} : o.filter p = some a ↔ o = some a ∧ p a := by cases o with | none => simp @@ -310,6 +367,9 @@ abbrev isSome_filter_of_isSome := @isSome_of_isSome_filter rintro rfl simpa using h +@[deprecated filter_eq_some_iff (since := "2025-04-10")] +abbrev filter_eq_some := @filter_eq_some_iff + theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} : a ∈ o.filter p ↔ a ∈ o ∧ p a := by simp @@ -383,29 +443,43 @@ theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join) cases x <;> simp theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x := - h.symm ▸ join_eq_some.1 h + h.symm ▸ join_eq_some_iff.1 h -@[simp] theorem some_orElse (a : α) (x : Option α) : (some a <|> x) = some a := rfl +@[simp] theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl -@[simp] theorem none_orElse (x : Option α) : (none <|> x) = x := rfl +@[simp] theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl -@[simp] theorem orElse_none (x : Option α) : (x <|> none) = x := by cases x <;> rfl +@[simp] theorem orElse_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl -theorem map_orElse {x y : Option α} : (x <|> y).map f = (x.map f <|> y.map f) := by +theorem orElse_eq_some_iff (o : Option α) (f) (x : α) : + (o.orElse f) = some x ↔ o = some x ∨ o = none ∧ f () = some x := by + cases o <;> simp + +theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none ↔ o = none ∧ f () = none := by + cases o <;> simp + +theorem map_orElse {x : Option α} {y} : + (x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by cases x <;> simp -@[simp] theorem guard_eq_some [DecidablePred p] : guard p a = some b ↔ a = b ∧ p a := +@[simp] theorem guard_eq_some_iff [DecidablePred p] : guard p a = some b ↔ a = b ∧ p a := if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h] +@[deprecated guard_eq_some_iff (since := "2025-04-10")] +abbrev guard_eq_some := @guard_eq_some_iff + @[simp] theorem isSome_guard [DecidablePred p] : (Option.guard p a).isSome ↔ p a := if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h] @[deprecated isSome_guard (since := "2025-03-18")] abbrev guard_isSome := @isSome_guard -@[simp] theorem guard_eq_none [DecidablePred p] : Option.guard p a = none ↔ ¬ p a := +@[simp] theorem guard_eq_none_iff [DecidablePred p] : Option.guard p a = none ↔ ¬ p a := if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h] +@[deprecated guard_eq_none_iff (since := "2025-04-10")] +abbrev guard_eq_none := @guard_eq_none_iff + @[simp] theorem guard_pos [DecidablePred p] (h : p a) : Option.guard p a = some a := by simp [Option.guard, h] @@ -475,6 +549,22 @@ theorem liftOrGet_none_right {f} {a : Option α} : merge f a none = a := theorem liftOrGet_some_some {f} {a b : α} : merge f (some a) (some b) = f a b := merge_some_some +instance commutative_merge (f : α → α → α) [Std.Commutative f] : + Std.Commutative (merge f) := + ⟨fun a b ↦ by cases a <;> cases b <;> simp [merge, Std.Commutative.comm]⟩ + +instance associative_merge (f : α → α → α) [Std.Associative f] : + Std.Associative (merge f) := + ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [merge, Std.Associative.assoc]⟩ + +instance idempotentOp_merge (f : α → α → α) [Std.IdempotentOp f] : + Std.IdempotentOp (merge f) := + ⟨fun a ↦ by cases a <;> simp [merge, Std.IdempotentOp.idempotent]⟩ + +instance lawfulIdentity_merge (f : α → α → α) : Std.LawfulIdentity (merge f) none where + left_id a := by cases a <;> simp [merge] + right_id a := by cases a <;> simp [merge] + @[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl @[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl @@ -535,12 +625,18 @@ theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by @[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by cases o <;> rfl -@[simp] theorem or_eq_none : or o o' = none ↔ o = none ∧ o' = none := by +@[simp] theorem or_eq_none_iff : or o o' = none ↔ o = none ∧ o' = none := by cases o <;> simp -@[simp] theorem or_eq_some : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by +@[deprecated or_eq_none_iff (since := "2025-04-10")] +abbrev or_eq_none := @or_eq_none_iff + +@[simp] theorem or_eq_some_iff : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by cases o <;> simp +@[deprecated or_eq_some_iff (since := "2025-04-10")] +abbrev or_eq_some := @or_eq_some_iff + theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by cases o₁ <;> cases o₂ <;> rfl instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩ @@ -564,11 +660,11 @@ instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩ theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by cases o <;> rfl -theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by +theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by cases o <;> rfl -theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by - cases o <;> rfl +@[deprecated map_or (since := "2025-04-10")] +abbrev map_or' := @map_or theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o := by match o, h with @@ -804,7 +900,7 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) : pmap g (o.map f) H = - pmap (fun a h => g (f a) h) o (fun a m => H (f a) (map_eq_some.2 ⟨_, m, rfl⟩)) := by + pmap (fun a h => g (f a) h) o (fun a m => H (f a) (map_eq_some_iff.2 ⟨_, m, rfl⟩)) := by cases o <;> simp theorem pmap_pred_congr {α : Type u} diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 3171a9aebf..2573a27009 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -1511,7 +1511,7 @@ theorem map_eq_iff {f : α → β} {as : Vector α n} {bs : Vector β n} : if h : i < as.size then simpa [h, h'] using w i h else - rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega + rw [getElem?_neg, getElem?_neg, Option.map_none] <;> omega @[simp] theorem map_set {f : α → β} {xs : Vector α n} {i : Nat} {h : i < n} {a : α} : (xs.set i a).map f = (xs.map f).set i (f a) (by simpa using h) := by diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index c70b1f38a7..0e14c5d1ac 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -215,7 +215,7 @@ theorem modify_eq_alter [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l modify a f l = alter a (·.map f) l := by induction l · rfl - · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih] + · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some, ih] namespace Const @@ -235,7 +235,7 @@ theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : Ass modify a f l = alter a (·.map f) l := by induction l · rfl - · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih] + · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some, ih] end Const diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 16039b3f25..4b306c6556 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -630,7 +630,7 @@ theorem Const.getThenInsertIfNew?_eq_insertIfNewₘ [BEq α] [Hashable α] (m : (a : α) (b : β) : (Const.getThenInsertIfNew? m a b).2 = m.insertIfNewₘ a b := by rw [getThenInsertIfNew?, insertIfNewₘ, containsₘ, bucket] dsimp only [Array.ugetElem_eq_getElem, Array.uset] - split <;> simp_all [consₘ, updateBucket, List.containsKey_eq_isSome_getValue?, -Option.not_isSome] + split <;> simp_all [consₘ, updateBucket, List.containsKey_eq_isSome_getValue?, -Option.isSome_eq_false_iff] theorem Const.getThenInsertIfNew?_eq_get?ₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) (b : β) : (Const.getThenInsertIfNew? m a b).1 = Const.get?ₘ m a := by diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 3911346cdd..f224d04ef7 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -964,7 +964,7 @@ theorem isHashSelf_filterMapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHasha IsHashSelf (m.filterMapₘ f).1.buckets := by refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_) have hp := AssocList.toList_filterMap.mem_iff.1 hp - simp only [mem_filterMap, Option.map_eq_some'] at hp + simp only [mem_filterMap, Option.map_eq_some_iff] at hp obtain ⟨p, ⟨hkv, ⟨d, ⟨-, rfl⟩⟩⟩⟩ := hp exact containsKey_of_mem hkv diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 4da5d73be8..29276038b5 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1031,7 +1031,7 @@ theorem ordered_filterMap [Ord α] {t : Impl α β} {h} {f : (a : α) → β a simp only [Ordered, toListModel_filterMap] apply ho.filterMap intro e f hef e' he' f' hf' - simp only [Option.map_eq_some'] at he' hf' + simp only [Option.map_eq_some_iff] at he' hf' obtain ⟨_, _, rfl⟩ := he' obtain ⟨_, _, rfl⟩ := hf' exact hef diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 3eae10f342..ceda220148 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -169,7 +169,7 @@ theorem getValue?_eq_getEntry? [BEq α] {l : List ((_ : α) × β)} {a : α} : · next k v l ih => cases h : k == a · rw [getEntry?_cons_of_false h, getValue?_cons_of_false h, ih] - · rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some'] + · rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some] theorem getValue?_congr [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} (h : a == b) : getValue? a l = getValue? b l := by @@ -338,7 +338,7 @@ theorem getEntry?_eq_none [BEq α] {l : List ((a : α) × β a)} {a : α} : @[simp] theorem getValue?_eq_none {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} : getValue? a l = none ↔ containsKey a l = false := by - rw [getValue?_eq_getEntry?, Option.map_eq_none', getEntry?_eq_none] + rw [getValue?_eq_getEntry?, Option.map_eq_none_iff, getEntry?_eq_none] theorem containsKey_eq_isSome_getValue? {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} : containsKey a l = (getValue? a l).isSome := by @@ -613,7 +613,7 @@ theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} : · next k v l ih => cases h : k == a · rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih] - · rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some'] + · rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some] theorem fst_mem_keys_of_mem [BEq α] [EquivBEq α] {a : (a : α) × β a} {l : List ((a : α) × β a)} (hm : a ∈ l) : a.1 ∈ keys l := @@ -1515,7 +1515,7 @@ theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a cases h : k == a · simp · rw [containsKey_eq_isSome_getEntry?, getEntry?_congr h] - simp + simp [-Option.not_isSome] theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : containsKey k (insertEntryIfNew k v l) := by @@ -2098,7 +2098,7 @@ theorem containsKey_append_of_not_contains_right [BEq α] {l l' : List ((a : α) @[simp] theorem getValue?_append {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} : getValue? a (l ++ l') = (getValue? a l).or (getValue? a l') := by - simp [getValue?_eq_getEntry?, Option.map_or'] + simp [getValue?_eq_getEntry?, Option.map_or] theorem getValue?_append_of_containsKey_eq_false {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} (h : containsKey a l' = false) : getValue? a (l ++ l') = getValue? a l := by @@ -2233,7 +2233,7 @@ theorem mem_map_toProd_iff_mem {β : Type v} {k : α} {v : β} {l : List ((_ : theorem mem_iff_getValue?_eq_some [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) : ⟨k, v⟩ ∈ l ↔ getValue? k l = some v := by - simp only [mem_iff_getEntry?_eq_some h, getValue?_eq_getEntry?, Option.map_eq_some'] + simp only [mem_iff_getEntry?_eq_some h, getValue?_eq_getEntry?, Option.map_eq_some_iff] constructor · intro h exists ⟨k, v⟩ @@ -2256,7 +2256,7 @@ theorem find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some [BEq | nil => simp | cons hd tl ih => simp only [List.map_cons, List.find?_cons_eq_some, Prod.mk.injEq, Bool.not_eq_eq_eq_not, - Bool.not_true, Option.map_eq_some', getKey?, cond_eq_if, getValue?] + Bool.not_true, Option.map_eq_some_iff, getKey?, cond_eq_if, getValue?] by_cases hdfst_k: hd.fst == k · simp only [hdfst_k, true_and, Bool.true_eq_false, false_and, or_false, ↓reduceIte, Option.some.injEq] @@ -2271,7 +2271,7 @@ theorem mem_iff_getKey?_eq_some_and_getValue?_eq_some [BEq α] [EquivBEq α] theorem getValue?_eq_some_iff_exists_beq_and_mem_toList {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k: α} {v : β} (h : DistinctKeys l) : getValue? k l = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ l.map (fun x => (x.fst, x.snd)) := by - simp only [getValue?_eq_getEntry?, Option.map_eq_some', ← mem_map_toProd_iff_mem, + simp only [getValue?_eq_getEntry?, Option.map_eq_some_iff, ← mem_map_toProd_iff_mem, mem_iff_getEntry?_eq_some h] constructor · intro h' @@ -2635,7 +2635,7 @@ theorem getKey?_insertList_of_mem [BEq α] [EquivBEq α] rcases List.mem_map.1 mem with ⟨⟨k, v⟩, pair_mem, rfl⟩ rw [getKey?_eq_getEntry?, getEntry?_insertList distinct_l distinct_toInsert, getEntry?_of_mem (DistinctKeys.def.2 distinct_toInsert) k_beq pair_mem, Option.some_or, - Option.map_some'] + Option.map_some] theorem getKey_insertList_of_contains_eq_false [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} @@ -3074,7 +3074,7 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [B (h': containsKey k l = false) (h : toInsert.contains k = false) : getKey? k (insertListIfNewUnit l toInsert) = none := by rw [getKey?_eq_getEntry?, - getEntry?_insertListIfNewUnit_of_contains_eq_false h, Option.map_eq_none', getEntry?_eq_none] + getEntry?_insertListIfNewUnit_of_contains_eq_false h, Option.map_eq_none_iff, getEntry?_eq_none] exact h' theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α] @@ -3083,8 +3083,8 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivB (mem' : containsKey k l = false) (distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) : getKey? k' (insertListIfNewUnit l toInsert) = some k := by - simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some', - Option.or_eq_some, getEntry?_eq_none] + simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some_iff, + Option.or_eq_some_iff, getEntry?_eq_none] exists ⟨k, ()⟩ simp only [and_true] right @@ -4301,8 +4301,8 @@ theorem minEntry?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : minKey? l = some k ↔ getKey? k l = some k ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by - simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd] - simp only [getKey?_eq_getEntry?, Option.map_eq_some', getEntry?_eq_some_iff hd] + simp only [minKey?, Option.map_eq_some_iff, minEntry?_eq_some_iff _ hd] + simp only [getKey?_eq_getEntry?, Option.map_eq_some_iff, getEntry?_eq_some_iff hd] apply Iff.intro · rintro ⟨_, ⟨hm, hcmp⟩, rfl⟩ exact ⟨⟨_, ⟨BEq.refl, hm⟩, rfl⟩, hcmp⟩ @@ -4312,7 +4312,7 @@ theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [B theorem minKey?_eq_some_iff_mem_and_forall [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : minKey? l = some k ↔ containsKey k l ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by - simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd] + simp only [minKey?, Option.map_eq_some_iff, minEntry?_eq_some_iff _ hd] apply Iff.intro · rintro ⟨_, ⟨hm, hcmp⟩, rfl⟩ exact ⟨containsKey_of_mem hm, hcmp⟩ @@ -4361,7 +4361,7 @@ theorem isNone_minKey?_eq_isEmpty [Ord α] {l : List ((a : α) × β a)} : theorem isSome_minEntry?_eq_not_isEmpty [Ord α] {l : List ((a : α) × β a)} : (minEntry? l).isSome = !l.isEmpty := by - rw [← Bool.not_inj_iff, Bool.not_not, Bool.eq_iff_iff, Bool.not_eq_true', Option.not_isSome, + rw [← Bool.not_inj_iff, Bool.not_not, Bool.eq_iff_iff, Bool.not_eq_true', Option.isSome_eq_false_iff, Option.isNone_iff_eq_none] apply minEntry?_eq_none_iff_isEmpty @@ -4384,7 +4384,7 @@ theorem minEntry?_map [Ord α] (l : List ((a : α) × β a)) (f : (a : α) × β simp only [minEntry?, List.min?] cases l <;> try rfl rename_i e es - simp only [List.map_cons, Option.map_some', Option.some.injEq] + simp only [List.map_cons, Option.map_some, Option.some.injEq] rw [← List.foldr_reverse, ← List.foldr_reverse, ← List.map_reverse] induction es.reverse with | nil => rfl @@ -4442,7 +4442,7 @@ theorem minEntry?_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] cases h : containsKey k l · simp only [cond_false, minEntry?_cons, Option.some.injEq] rfl - · rw [cond_true, minEntry?_replaceEntry hl, Option.map_eq_some'] + · rw [cond_true, minEntry?_replaceEntry hl, Option.map_eq_some_iff] have := isSome_minEntry?_of_contains ‹_› simp only [Option.isSome_iff_exists] at this obtain ⟨a, ha⟩ := this @@ -4538,7 +4538,7 @@ theorem minKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] theorem containsKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} (hkm : minKey? l = some km) : containsKey km l := by - simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd] at hkm + simp only [minKey?, Option.map_eq_some_iff, minEntry?_eq_some_iff _ hd] at hkm obtain ⟨e, ⟨hm, _⟩, rfl⟩ := hkm exact containsKey_of_mem hm @@ -4710,7 +4710,7 @@ theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd minKey? (alterKey k f l) = some k ↔ (f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.alterKey, getKey?_alterKey _ hd, - beq_self_eq_true, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, Option.not_isSome, + beq_self_eq_true, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, Option.isSome_eq_false_iff, Option.isNone_iff_eq_none, reduceCtorEq, imp_false, ← Option.isSome_iff_ne_none, containsKey_alterKey hd, beq_iff_eq, Bool.ite_eq_true_distrib, and_congr_right_iff] intro hf @@ -4753,18 +4753,18 @@ theorem minKey?_modifyKey_eq_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqO simp only [minKey?_modifyKey hd] cases minKey? l · rfl - · simp only [beq_iff_eq, Option.map_some', Option.some.injEq, ite_eq_right_iff] + · simp only [beq_iff_eq, Option.map_some, Option.some.injEq, ite_eq_right_iff] exact Eq.symm theorem isSome_minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f} {l : List ((_ : α) × β)} : (modifyKey k f l |> minKey?).isSome = !l.isEmpty := by - simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey] + simp [Option.isSome_map, isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey] theorem isSome_minKey?_modifyKey_eq_isSome [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f} {l : List ((_ : α) × β)} : (modifyKey k f l |> minKey?).isSome = (minKey? l).isSome := by - simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey] + simp [Option.isSome_map, isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey] theorem minKey?_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f km kmm} {l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : minKey? l = some km) @@ -4784,7 +4784,7 @@ theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd (f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.constAlterKey, getKey?_alterKey _ hd, ← compare_eq_iff_beq, compare_self, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, - Option.not_isSome, Option.isNone_iff_eq_none, reduceCtorEq, imp_false, + Option.isSome_eq_false_iff, Option.isNone_iff_eq_none, reduceCtorEq, imp_false, ← Option.isSome_iff_ne_none, containsKey_alterKey hd, Bool.ite_eq_true_distrib, and_congr_right_iff] intro hf diff --git a/tests/lean/run/grind_list.lean b/tests/lean/run/grind_list.lean index 0f7f8503f0..3d0e9d4ab2 100644 --- a/tests/lean/run/grind_list.lean +++ b/tests/lean/run/grind_list.lean @@ -18,7 +18,7 @@ theorem getElem!_of_getElem?' [Inhabited α] : ∀ {l : List α} {i : Nat}, l[i]? = some b → l[i]! = b := by grind -attribute [local grind =] Option.map_some' Option.map_none' in +attribute [local grind =] Option.map_some Option.map_none in attribute [local grind =] getElem?_map in attribute [local grind =] getElem?_replicate in theorem map_replicate' : (replicate n a).map f = replicate n (f a) := by diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean index def1f152fd..62ca75d6c9 100644 --- a/tests/lean/run/grind_t1.lean +++ b/tests/lean/run/grind_t1.lean @@ -318,20 +318,20 @@ example {α β} (f : α → β) (a : α) : ∃ a', f a' = f a := by open List in example : (replicate n a).map f = replicate n (f a) := by - grind +splitIndPred only [Option.map_some', Option.map_none', getElem?_map, getElem?_replicate] + grind +splitIndPred only [Option.map_some, Option.map_none, getElem?_map, getElem?_replicate] open List in example : (replicate n a).map f = replicate n (f a) := by - grind only [cases Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate] + grind only [cases Exists, Option.map_some, Option.map_none, getElem?_map, getElem?_replicate] open List in example : (replicate n a).map f = replicate n (f a) := by - grind only [cases Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate] + grind only [cases Exists, Option.map_some, Option.map_none, getElem?_map, getElem?_replicate] open List in example : (replicate n a).map f = replicate n (f a) := by -- Should fail since extensionality is disabled - fail_if_success grind -ext only [Option.map_some', Option.map_none', getElem?_map, getElem?_replicate] + fail_if_success grind -ext only [Option.map_some, Option.map_none, getElem?_map, getElem?_replicate] sorry @[ext] structure S where diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean index 0c684e2d8c..1b30e0d070 100644 --- a/tests/lean/run/grind_trace.lean +++ b/tests/lean/run/grind_trace.lean @@ -8,7 +8,7 @@ attribute [grind =] List.getElem?_eq_none attribute [grind =] List.getElem?_eq_some_iff attribute [grind =] getElem!_pos -attribute [grind =] Option.map_some' Option.map_none' +attribute [grind =] Option.map_some Option.map_none attribute [grind =] List.getElem?_map attribute [grind =] List.getElem?_replicate @@ -33,8 +33,8 @@ example : 0 < (x :: t).length := by grind? /-- -info: Try this: grind only [= List.getElem?_replicate, = List.getElem?_eq_some_iff, = List.getElem?_map, = - List.getElem_replicate, = List.getElem?_eq_none, = Option.map_some', = Option.map_none', = List.length_replicate, → +info: Try this: grind only [= Option.map_some, = Option.map_none, = List.getElem?_replicate, = List.getElem?_eq_some_iff, = + List.getElem?_map, = List.getElem_replicate, = List.getElem?_eq_none, = List.length_replicate, → List.getElem?_eq_getElem, cases Or] -/ #guard_msgs (info) in