From ae1ab94992ea12766ea3dc28862539e476d843d2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 22 May 2025 22:45:35 +0000 Subject: [PATCH] fix: replace bad simp lemmas for `Id` (#7352) This PR reworks the `simp` set around the `Id` monad, to not elide or unfold `pure` and `Id.run` In particular, it stops encoding the "defeq abuse" of `Id X = X` in the statements of theorems, instead using `Id.run` and `pure` to pass back and forth between these two spellings. Often when writing these with `pure`, they generalize to other lawful monads; though such changes were split off to other PRs. This fixes the problem with the current simp set where `Id.run (pure x)` is simplified to `Id.run x`, instead of the desirable `x`. This is particularly bad because the` x` is sometimes inferred with type `Id X` instead of `X`, which prevents other `simp` lemmas about `X` from firing. Making `Id` reducible instead is not an option, as then the `Monad` instances would have nothing to key on. --------- Co-authored-by: Sebastian Graf Co-authored-by: Kim Morrison Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> --- src/Init/Control/Lawful/Basic.lean | 17 ++++- src/Init/Data/Array/Basic.lean | 24 +++---- src/Init/Data/Array/BasicAux.lean | 2 +- src/Init/Data/Array/BinSearch.lean | 2 +- src/Init/Data/Array/Lemmas.lean | 71 +++++++++---------- src/Init/Data/Array/Lex/Lemmas.lean | 10 +-- src/Init/Data/Array/MapIdx.lean | 2 +- src/Init/Data/Array/Monadic.lean | 34 ++++++--- src/Init/Data/Array/OfFn.lean | 1 - src/Init/Data/Array/Subarray.lean | 10 +-- src/Init/Data/ByteArray/Basic.lean | 2 +- src/Init/Data/Fin/Fold.lean | 4 +- src/Init/Data/FloatArray/Basic.lean | 2 +- src/Init/Data/List/BasicAux.lean | 2 +- src/Init/Data/List/Control.lean | 17 ++++- src/Init/Data/List/Lemmas.lean | 27 ++++--- src/Init/Data/List/Monadic.lean | 34 ++++++--- src/Init/Data/List/OfFn.lean | 1 - src/Init/Data/List/ToArray.lean | 6 +- src/Init/Data/Option/Monadic.lean | 26 +++++-- src/Init/Data/Vector/Lemmas.lean | 27 ++++--- src/Init/Data/Vector/Lex.lean | 2 +- src/Init/Data/Vector/Monadic.lean | 28 +++++--- src/Init/Data/Vector/OfFn.lean | 1 - src/Init/Meta.lean | 4 +- src/Lean/Compiler/LCNF/FVarUtil.lean | 4 +- src/Lean/Data/AssocList.lean | 2 +- src/Lean/Data/NameTrie.lean | 4 +- src/Lean/Data/PersistentArray.lean | 12 ++-- src/Lean/Data/PersistentHashMap.lean | 4 +- src/Lean/Data/PersistentHashSet.lean | 2 +- src/Lean/Language/Basic.lean | 2 +- src/Lean/LocalContext.lean | 12 ++-- src/Lean/Meta/DiscrTree.lean | 4 +- src/Lean/Parser/Basic.lean | 2 +- src/Lean/Parser/Module.lean | 2 +- .../Completion/EligibleHeaderDecls.lean | 4 +- .../Completion/SyntheticCompletion.lean | 2 +- src/Lean/Server/InfoUtils.lean | 8 +-- src/Lean/SubExpr.lean | 2 +- src/Lean/Syntax.lean | 2 +- .../DHashMap/Internal/AssocList/Basic.lean | 4 +- .../DHashMap/Internal/AssocList/Lemmas.lean | 6 +- src/Std/Data/DHashMap/Internal/Model.lean | 8 +-- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 12 ++-- src/Std/Data/DHashMap/Internal/WF.lean | 9 +-- src/Std/Data/DHashMap/Raw.lean | 6 +- src/Std/Data/DTreeMap/Internal/Queries.lean | 4 +- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 25 ++++--- src/Std/Data/ExtDHashMap/Lemmas.lean | 6 +- src/Std/Data/Iterators/Consumers/Collect.lean | 12 ++-- .../Iterators/Lemmas/Consumers/Collect.lean | 26 +++---- src/lake/Lake/Reservoir.lean | 4 +- tests/lean/autoBoundImplicits1.lean | 2 +- tests/lean/run/1293.lean | 2 +- tests/lean/run/array_simp.lean | 2 - tests/lean/run/fib_correct.lean | 2 +- tests/lean/run/list_simp.lean | 4 +- tests/lean/run/treeNode.lean | 2 +- tests/lean/run/treemap.lean | 6 +- tests/lean/run/wfOverapplicationIssue.lean | 2 +- 61 files changed, 324 insertions(+), 244 deletions(-) diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index 79c1471960..d7db61e015 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -6,6 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro module prelude +import Init.Ext import Init.SimpLemmas import Init.Meta @@ -241,13 +242,23 @@ theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m] namespace Id -@[simp] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl -@[simp] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl -@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl +@[ext] theorem ext {x y : Id α} (h : x.run = y.run) : x = y := h instance : LawfulMonad Id := by refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl +@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl +@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl +@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl +@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl +@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl +@[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl + +-- These lemmas are bad as they abuse the defeq of `Id α` and `α` +@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl +@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl +@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl + end Id /-! # Option -/ diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 38a721356f..512abd7d30 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -544,7 +544,7 @@ Examples: -/ @[inline] def modify (xs : Array α) (i : Nat) (f : α → α) : Array α := - Id.run <| modifyM xs i f + Id.run <| modifyM xs i (pure <| f ·) set_option linter.indexVariables false in -- Changing `idx` causes bootstrapping issues, haven't investigated. /-- @@ -1059,7 +1059,7 @@ Examples: -/ @[inline] def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β := - Id.run <| as.foldlM f init start stop + Id.run <| as.foldlM (pure <| f · ·) init start stop /-- Folds a function over an array from the right, accumulating a value starting with `init`. The @@ -1076,7 +1076,7 @@ Examples: -/ @[inline] def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β := - Id.run <| as.foldrM f init start stop + Id.run <| as.foldrM (pure <| f · ·) init start stop /-- Computes the sum of the elements of an array. @@ -1124,7 +1124,7 @@ Examples: -/ @[inline] def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β := - Id.run <| as.mapM f + Id.run <| as.mapM (pure <| f ·) instance : Functor Array where map := map @@ -1139,7 +1139,7 @@ valid. -/ @[inline] def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β := - Id.run <| as.mapFinIdxM f + Id.run <| as.mapFinIdxM (pure <| f · · ·) /-- Applies a function to each element of the array along with the index at which that element is found, @@ -1150,7 +1150,7 @@ is valid. -/ @[inline] def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β := - Id.run <| as.mapIdxM f + Id.run <| as.mapIdxM (pure <| f · ·) /-- Pairs each element of an array with its index, optionally starting from an index other than `0`. @@ -1198,7 +1198,7 @@ some 10 -/ @[inline] def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β := - Id.run <| as.findSomeM? f + Id.run <| as.findSomeM? (pure <| f ·) /-- Returns the first non-`none` result of applying the function `f` to each element of the @@ -1232,7 +1232,7 @@ Examples: -/ @[inline] def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β := - Id.run <| as.findSomeRevM? f + Id.run <| as.findSomeRevM? (pure <| f ·) /-- Returns the last element of the array for which the predicate `p` returns `true`, or `none` if no @@ -1244,7 +1244,7 @@ Examples: -/ @[inline] def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α := - Id.run <| as.findRevM? p + Id.run <| as.findRevM? (pure <| p ·) /-- Returns the index of the first element for which `p` returns `true`, or `none` if there is no such @@ -1383,7 +1383,7 @@ Examples: -/ @[inline] def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool := - Id.run <| as.anyM p start stop + Id.run <| as.anyM (pure <| p ·) start stop /-- Returns `true` if `p` returns `true` for every element of `as`. @@ -1401,7 +1401,7 @@ Examples: -/ @[inline] def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool := - Id.run <| as.allM p start stop + Id.run <| as.allM (pure <| p ·) start stop /-- Checks whether `a` is an element of `as`, using `==` to compare elements. @@ -1670,7 +1670,7 @@ Example: -/ @[inline] def filterMap (f : α → Option β) (as : Array α) (start := 0) (stop := as.size) : Array β := - Id.run <| as.filterMapM f (start := start) (stop := stop) + Id.run <| as.filterMapM (pure <| f ·) (start := start) (stop := stop) /-- Returns the largest element of the array, as determined by the comparison `lt`, or `none` if diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index 73559d4b93..9f24e79ee5 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -88,4 +88,4 @@ pointer equality, and does not allocate a new array if the result of each functi pointer-equal to its argument. -/ @[inline] def Array.mapMono (as : Array α) (f : α → α) : Array α := - Id.run <| as.mapMonoM f + Id.run <| as.mapMonoM (pure <| f ·) diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean index a900e6ba15..ed96e55932 100644 --- a/src/Init/Data/Array/BinSearch.lean +++ b/src/Init/Data/Array/BinSearch.lean @@ -129,6 +129,6 @@ Examples: * `#[].binInsert (· < ·) 1 = #[1]` -/ @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α := - Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k + Id.run <| binInsertM lt (fun _ => pure k) (fun _ => pure k) as k end Array diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 7de8b1b825..427beec0f2 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -613,13 +613,13 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st -- Auxiliary for `any_iff_exists`. theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) : - anyM.loop (m := Id) p as stop h start = true ↔ + (anyM.loop (m := Id) (pure <| p ·) as stop h start).run = true ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by unfold anyM.loop split <;> rename_i h₁ · dsimp split <;> rename_i h₂ - · simp only [true_iff] + · simp only [true_iff, Id.run_pure] refine ⟨start, by omega, by omega, by omega, h₂⟩ · rw [anyM_loop_iff_exists] constructor @@ -636,9 +636,9 @@ termination_by stop - start -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic` theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} : as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] := by - dsimp [any, anyM, Id.run] + dsimp [any, anyM] split - · rw [anyM_loop_iff_exists] + · rw [anyM_loop_iff_exists (p := p)] · rw [anyM_loop_iff_exists] constructor · rintro ⟨i, hi, ge, _, h⟩ @@ -1370,17 +1370,17 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar @[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")] theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} : - mapM.map (m := Id) f as i b = as.foldl (start := i) (fun acc a => acc.push (f a)) b := by + mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by unfold mapM.map split <;> rename_i h - · simp only [Id.bind_eq] - dsimp [foldl, Id.run, foldlM] + · ext : 1 + dsimp [foldl, foldlM] rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h] -- Calling `split` here gives a bad goal. have : size as - i = Nat.succ (size as - i - 1) := by omega rw [this] - simp [foldl, foldlM, Id.run, Nat.sub_add_eq] - · dsimp [foldl, Id.run, foldlM] + simp [foldl, foldlM, Nat.sub_add_eq] + · dsimp [foldl, foldlM] rw [dif_pos (by omega), foldlM.loop, dif_neg h] rfl termination_by as.size - i @@ -1602,8 +1602,8 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs) as.toList ++ List.filterMap f xs := ?_ exact this #[] induction xs - · simp_all [Id.run] - · simp_all [Id.run, List.filterMap_cons] + · simp_all + · simp_all [List.filterMap_cons] split <;> simp_all @[grind] theorem toList_filterMap {f : α → Option β} {xs : Array α} : @@ -3215,18 +3215,16 @@ theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Array α} {a : α} {f : β rw [foldr, foldrM_start_stop, ← foldrM_toList, List.foldrM_pure, foldr_toList, foldr, ← foldrM_start_stop] theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop : Nat} : - xs.foldl f b start stop = xs.foldlM (m := Id) f b start stop := by - simp [foldl, Id.run] + xs.foldl f b start stop = (xs.foldlM (m := Id) (pure <| f · ·) b start stop).run := rfl theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} : - xs.foldr f b start stop = xs.foldrM (m := Id) f b start stop := by - simp [foldr, Id.run] + xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl @[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Array α} {start stop : Nat} : - Id.run (xs.foldlM f b start stop) = xs.foldl f b start stop := foldl_eq_foldlM.symm + Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl @[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Array α} {start stop : Nat} : - Id.run (xs.foldrM f b start stop) = xs.foldr f b start stop := foldr_eq_foldrM.symm + Id.run (xs.foldrM f b start stop) = xs.foldr (f · · |>.run) b start stop := rfl /-- Variant of `foldlM_reverse` with a side condition for the `stop` argument. -/ @[simp] theorem foldlM_reverse' [Monad m] {xs : Array α} {f : β → α → m β} {b} {stop : Nat} @@ -3526,17 +3524,16 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs @[simp] theorem foldr_append' {f : α → β → β} {b} {xs ys : Array α} {start : Nat} (w : start = xs.size + ys.size) : - (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := by - subst w - simp [foldr_eq_foldrM] + (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := + foldrM_append' w @[grind _=_]theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} : - (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by - simp [foldl_eq_foldlM] + (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := + foldlM_append @[grind _=_] theorem foldr_append {f : α → β → β} {b} {xs ys : Array α} : - (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by - simp [foldr_eq_foldrM] + (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := + foldrM_append @[simp] theorem foldl_flatten' {f : β → α → β} {b} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) : @@ -3565,21 +3562,22 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs /-- Variant of `foldl_reverse` with a side condition for the `stop` argument. -/ @[simp] theorem foldl_reverse' {xs : Array α} {f : β → α → β} {b} {stop : Nat} (w : stop = xs.size) : - xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b := by - simp [w, foldl_eq_foldlM, foldr_eq_foldrM] + xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b := + foldlM_reverse' w /-- Variant of `foldr_reverse` with a side condition for the `start` argument. -/ @[simp] theorem foldr_reverse' {xs : Array α} {f : α → β → β} {b} {start : Nat} (w : start = xs.size) : - xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b := by - simp [w, foldl_eq_foldlM, foldr_eq_foldrM] + xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b := + foldrM_reverse' w @[grind] theorem foldl_reverse {xs : Array α} {f : β → α → β} {b} : - xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM] + xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := + foldlM_reverse @[grind] theorem foldr_reverse {xs : Array α} {f : α → β → β} {b} : xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b := - (foldl_reverse ..).symm.trans <| by simp + foldrM_reverse theorem foldl_eq_foldr_reverse {xs : Array α} {f : β → α → β} {b} : xs.foldl f b = xs.reverse.foldr (fun x y => f y x) b := by simp @@ -4094,15 +4092,16 @@ abbrev all_mkArray := @all_replicate /-! ### modify -/ @[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by - unfold modify modifyM Id.run + unfold modify modifyM split <;> simp theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) : (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by - simp only [modify, modifyM, Id.run, Id.pure_eq] + simp only [modify, modifyM] split - · simp only [Id.bind_eq, getElem_set]; split <;> simp [*] - · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))] + · simp only [getElem_set, Id.run_pure, Id.run_bind]; split <;> simp [*] + · simp only [Id.run_pure] + rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))] @[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} : (xs.modify i f).toList = xs.toList.modify i f := by @@ -4643,12 +4642,12 @@ namespace Array @[simp] theorem findSomeRev?_eq_findSome?_reverse {f : α → Option β} {xs : Array α} : xs.findSomeRev? f = xs.reverse.findSome? f := by cases xs - simp [findSomeRev?, Id.run] + simp [findSomeRev?] @[simp] theorem findRev?_eq_find?_reverse {f : α → Bool} {xs : Array α} : xs.findRev? f = xs.reverse.find? f := by cases xs - simp [findRev?, Id.run] + simp [findRev?] /-! ### unzip -/ diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index 44f2540511..a7fa0f8525 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -29,16 +29,16 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys Decidable.not_not @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by - simp [lex, Id.run] + simp [lex] @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by simp only [lex, List.getElem_toArray, List.getElem_singleton] - cases lt a b <;> cases a != b <;> simp [Id.run] + cases lt a b <;> cases a != b <;> simp private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} : (#[a] ++ xs).lex (#[b] ++ ys) lt = (lt a b || a == b && xs.lex ys lt) := by - simp only [lex, Id.run] + simp only [lex] simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton, Nat.add_comm 1] simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left, @@ -51,10 +51,10 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs @[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} : l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by induction l₁ generalizing l₂ with - | nil => cases l₂ <;> simp [lex, Id.run] + | nil => cases l₂ <;> simp [lex] | cons x l₁ ih => cases l₂ with - | nil => simp [lex, Id.run] + | nil => simp [lex] | cons y l₂ => rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih] diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index 316045e6a3..943e58a9b9 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -27,7 +27,7 @@ theorem mapFinIdx_induction (xs : Array α) (f : (i : Nat) → α → (h : i < x motive xs.size ∧ ∃ eq : (Array.mapFinIdx xs f).size = xs.size, ∀ i h, p i ((Array.mapFinIdx xs f)[i]) h := by let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) : - let as : Array β := Array.mapFinIdxM.map (m := Id) xs f i j h bs + let as : Array β := Id.run <| Array.mapFinIdxM.map xs (pure <| f · · ·) i j h bs motive xs.size ∧ ∃ eq : as.size = xs.size, ∀ i h, p i as[i] h := by induction i generalizing j bs with simp [mapFinIdxM.map] | zero => diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index 345ce1a64c..ae040d4d6d 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -36,7 +36,11 @@ open Nat xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by induction xs; simp_all -@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f := +@[simp] theorem idRun_mapM {xs : Array α} {f : α → Id β} : (xs.mapM f).run = xs.map (f · |>.run) := + mapM_pure + +@[deprecated idRun_mapM (since := "2025-05-21")] +theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f := mapM_pure @[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {xs : Array α} : @@ -191,12 +195,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs⟩ simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map] -@[simp] theorem forIn'_yield_eq_foldl +@[simp] theorem idRun_forIn'_yield_eq_foldl + {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : + (forIn' xs init (fun a m b => .yield <$> f a m b)).run = + xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := + forIn'_pure_yield_eq_foldl _ _ + +@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")] +theorem forIn'_yield_eq_foldl {xs : Array α} (f : (a : α) → a ∈ xs → β → β) (init : β) : forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) = - xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by - rcases xs with ⟨xs⟩ - simp [List.foldl_map] + xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := + forIn'_pure_yield_eq_foldl _ _ @[simp] theorem forIn'_map [Monad m] [LawfulMonad m] {xs : Array α} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) : @@ -233,12 +243,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs⟩ simp [List.forIn_pure_yield_eq_foldl, List.foldl_map] -@[simp] theorem forIn_yield_eq_foldl +@[simp] theorem idRun_forIn_yield_eq_foldl + {xs : Array α} (f : α → β → Id β) (init : β) : + (forIn xs init (fun a b => .yield <$> f a b)).run = + xs.foldl (fun b a => f a b |>.run) init := + forIn_pure_yield_eq_foldl _ _ + +@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")] +theorem forIn_yield_eq_foldl {xs : Array α} (f : α → β → β) (init : β) : forIn (m := Id) xs init (fun a b => .yield (f a b)) = - xs.foldl (fun b a => f a b) init := by - rcases xs with ⟨xs⟩ - simp [List.foldl_map] + xs.foldl (fun b a => f a b) init := + forIn_pure_yield_eq_foldl _ _ @[simp] theorem forIn_map [Monad m] [LawfulMonad m] {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} : diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean index c43fbc4907..fc097db333 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -129,7 +129,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} : @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} : Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by - unfold Id.run induction n with | zero => simp | succ n ih => simp [ofFnM_succ', ofFn_succ', ih] diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 04b7af62bd..8324678e25 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -290,7 +290,7 @@ Examples: -/ @[inline] def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β := - Id.run <| as.foldlM f (init := init) + Id.run <| as.foldlM (pure <| f · ·) (init := init) /-- Folds an operation from right to left over the elements in a subarray. @@ -304,7 +304,7 @@ Examples: -/ @[inline] def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β := - Id.run <| as.foldrM f (init := init) + Id.run <| as.foldrM (pure <| f · ·) (init := init) /-- Checks whether any of the elements in a subarray satisfy a Boolean predicate. @@ -314,7 +314,7 @@ an element that satisfies the predicate is found. -/ @[inline] def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool := - Id.run <| as.anyM p + Id.run <| as.anyM (pure <| p ·) /-- Checks whether all of the elements in a subarray satisfy a Boolean predicate. @@ -324,7 +324,7 @@ an element that does not satisfy the predicate is found. -/ @[inline] def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool := - Id.run <| as.allM p + Id.run <| as.allM (pure <| p ·) /-- Applies a monadic function to each element in a subarray in reverse order, stopping at the first @@ -394,7 +394,7 @@ Examples: -/ @[inline] def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α := - Id.run <| as.findRevM? p + Id.run <| as.findRevM? (pure <| p ·) end Subarray diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 75a387d5eb..ffa5fa53ed 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -205,7 +205,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → @[inline] def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β := - Id.run <| as.foldlM f init start stop + Id.run <| as.foldlM (pure <| f · ·) init start stop /-- Iterator over the bytes (`UInt8`) of a `ByteArray`. diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index 1e6d3b4a11..c80346ebfc 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -266,7 +266,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) : | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc] theorem foldl_eq_foldlM (f : α → Fin n → α) (x) : - foldl n f x = foldlM (m:=Id) n f x := by + foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *] -- This is not marked `@[simp]` as it would match on every occurrence of `foldlM`. @@ -319,7 +319,7 @@ theorem foldr_add (f : Fin (n + m) → α → α) (x) : | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc] theorem foldr_eq_foldrM (f : Fin n → α → α) (x) : - foldr n f x = foldrM (m:=Id) n f x := by + foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by induction n <;> simp [foldr_succ, foldrM_succ, *] theorem foldl_rev (f : Fin n → α → α) (x) : diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index fb416d0f94..faf7174876 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -165,7 +165,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float → @[inline] def foldl {β : Type v} (f : β → Float → β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : β := - Id.run <| as.foldlM f init start stop + Id.run <| as.foldlM (pure <| f · ·) init start stop end FloatArray diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index da44feb2d7..263ae46b64 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -254,7 +254,7 @@ pointer-equal to its argument. For verification purposes, `List.mapMono = List.map`. -/ def mapMono (as : List α) (f : α → α) : List α := - Id.run <| as.mapMonoM f + Id.run <| as.mapMonoM (pure <| f ·) /-! ## Additional lemmas required for bootstrapping `Array`. -/ diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index c94a059bda..99a00a7bd9 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -348,9 +348,16 @@ theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List | false => simp [ih] @[simp] -theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p := +theorem idRun_findM? (p : α → Id Bool) (as : List α) : + (findM? p as).run = as.find? (p · |>.run) := findM?_pure _ _ +@[deprecated idRun_findM? (since := "2025-05-21")] +theorem findM?_id (p : α → Id Bool) (as : List α) : + findM? (m := Id) p as = as.find? p := + findM?_pure _ _ + + /-- Returns the first non-`none` result of applying the monadic function `f` to each element of the list, in order. Returns `none` if `f` returns `none` for all elements. @@ -394,7 +401,13 @@ theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : L | none => simp [ih] @[simp] -theorem findSomeM?_id {f : α → Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f := +theorem idRun_findSomeM? (f : α → Id (Option β)) (as : List α) : + (findSomeM? f as).run = as.findSome? (f · |>.run) := + findSomeM?_pure + +@[deprecated idRun_findSomeM? (since := "2025-05-21")] +theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) : + findSomeM? (m := Id) f as = as.findSome? f := findSomeM?_pure theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} : diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index cbdc03ea5b..2ac7eedaa3 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -2541,17 +2541,25 @@ theorem flatten_reverse {L : List (List α)} : induction l generalizing b <;> simp [*] theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} : - l.foldl f b = l.foldlM (m := Id) f b := by - induction l generalizing b <;> simp [*, foldl] + l.foldl f b = (l.foldlM (m := Id) (pure <| f · ·) b).run := by + simp theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} : - l.foldr f b = l.foldrM (m := Id) f b := by - induction l <;> simp [*, foldr] + l.foldr f b = (l.foldrM (m := Id) (pure <| f · ·) b).run := by + simp -@[simp] theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} : +theorem idRun_foldlM {f : β → α → Id β} {b : β} {l : List α} : + Id.run (l.foldlM f b) = l.foldl (f · · |>.run) b := foldl_eq_foldlM.symm + +@[deprecated idRun_foldlM (since := "2025-05-21")] +theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} : Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm -@[simp] theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} : +theorem idRun_foldrM {f : α → β → Id β} {b : β} {l : List α} : + Id.run (l.foldrM f b) = l.foldr (f · · |>.run) b := foldr_eq_foldrM.symm + +@[deprecated idRun_foldrM (since := "2025-05-21")] +theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} : Id.run (l.foldrM f b) = l.foldr f b := foldr_eq_foldrM.symm @[simp] theorem foldlM_reverse [Monad m] {l : List α} {f : β → α → m β} {b : β} : @@ -2646,10 +2654,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β → induction l <;> simp [*] @[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} : - (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM] + (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM, -foldlM_pure] @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} : - (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM] + (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, -foldrM_pure] @[grind] theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} : (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by @@ -2660,7 +2668,8 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β → induction L <;> simp_all @[simp, grind] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} : - l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM] + l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by + simp [foldl_eq_foldlM, foldr_eq_foldrM, -foldrM_pure] @[simp, grind] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} : l.reverse.foldr f b = l.foldl (fun x y => f y x) b := diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean index 376dd4f176..80f02629a1 100644 --- a/src/Init/Data/List/Monadic.lean +++ b/src/Init/Data/List/Monadic.lean @@ -68,7 +68,11 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by induction l <;> simp_all -@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f := +@[simp] theorem idRun_mapM {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) := + mapM_pure + +@[deprecated idRun_mapM (since := "2025-05-21")] +theorem mapM_id {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) := mapM_pure @[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {l : List α} : @@ -345,12 +349,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m] simp only [forIn'_eq_foldlM] induction l.attach generalizing init <;> simp_all -@[simp] theorem forIn'_yield_eq_foldl +@[simp] theorem idRun_forIn'_yield_eq_foldl + (l : List α) (f : (a : α) → a ∈ l → β → Id β) (init : β) : + (forIn' l init (fun a m b => .yield <$> f a m b)).run = + l.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := + forIn'_pure_yield_eq_foldl _ _ + +@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")] +theorem forIn'_yield_eq_foldl {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) : forIn' (m := Id) l init (fun a m b => .yield (f a m b)) = - l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by - simp only [forIn'_eq_foldlM] - induction l.attach generalizing init <;> simp_all + l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := + forIn'_pure_yield_eq_foldl _ _ @[simp] theorem forIn'_map [Monad m] [LawfulMonad m] {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) : @@ -398,12 +408,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m] simp only [forIn_eq_foldlM] induction l generalizing init <;> simp_all -@[simp] theorem forIn_yield_eq_foldl +@[simp] theorem idRun_forIn_yield_eq_foldl + (l : List α) (f : α → β → Id β) (init : β) : + (forIn l init (fun a b => .yield <$> f a b)).run = + l.foldl (fun b a => f a b |>.run) init := + forIn_pure_yield_eq_foldl _ _ + +@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")] +theorem forIn_yield_eq_foldl {l : List α} (f : α → β → β) (init : β) : forIn (m := Id) l init (fun a b => .yield (f a b)) = - l.foldl (fun b a => f a b) init := by - simp only [forIn_eq_foldlM] - induction l generalizing init <;> simp_all + l.foldl (fun b a => f a b) init := + forIn_pure_yield_eq_foldl _ _ @[simp] theorem forIn_map [Monad m] [LawfulMonad m] {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} : diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean index 460730cc4b..53367f2367 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -173,7 +173,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} : @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} : Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by - unfold Id.run induction n with | zero => simp | succ n ih => simp [-ofFn_succ, ofFnM_succ_last, ofFn_succ_last, ih] diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index f558f3b025..3bb1175d20 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -256,16 +256,16 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis @[simp, grind =] theorem findSome?_toArray (f : α → Option β) (l : List α) : l.toArray.findSome? f = l.findSome? f := by - rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run] + rw [Array.findSome?, findSomeM?_toArray, findSomeM?_pure, Id.run_pure] @[simp, grind =] theorem find?_toArray (f : α → Bool) (l : List α) : l.toArray.find? f = l.find? f := by rw [Array.find?] - simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray] + simp only [forIn_toArray] induction l with | nil => simp | cons a l ih => - simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?] + simp only [forIn_cons, find?] by_cases f a <;> simp_all private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) : diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean index 244ef754d1..894a74fddf 100644 --- a/src/Init/Data/Option/Monadic.lean +++ b/src/Init/Data/Option/Monadic.lean @@ -90,11 +90,18 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m] pure (f := m) (o.pelim b (fun a h => f a h b)) := by cases o <;> simp -@[simp] theorem forIn'_id_yield_eq_pelim +@[simp] theorem idRun_forIn'_yield_eq_pelim + (o : Option α) (f : (a : α) → a ∈ o → β → Id β) (b : β) : + (forIn' o b (fun a m b => .yield <$> f a m b)).run = + o.pelim b (fun a h => f a h b |>.run) := + forIn'_pure_yield_eq_pelim _ _ _ + +@[deprecated idRun_forIn'_yield_eq_pelim (since := "2025-05-21")] +theorem forIn'_id_yield_eq_pelim (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) : forIn' (m := Id) o b (fun a m b => .yield (f a m b)) = - o.pelim b (fun a h => f a h b) := by - cases o <;> simp + o.pelim b (fun a h => f a h b) := + forIn'_pure_yield_eq_pelim _ _ _ @[simp, grind] theorem forIn'_map [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) : @@ -126,11 +133,18 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m] pure (f := m) (o.elim b (fun a => f a b)) := by cases o <;> simp -@[simp] theorem forIn_id_yield_eq_elim +@[simp] theorem idRun_forIn_yield_eq_elim + (o : Option α) (f : (a : α) → β → Id β) (b : β) : + (forIn o b (fun a b => .yield <$> f a b)).run = + o.elim b (fun a => f a b |>.run) := + forIn_pure_yield_eq_elim _ _ _ + +@[deprecated idRun_forIn_yield_eq_elim (since := "2025-05-21")] +theorem forIn_id_yield_eq_elim (o : Option α) (f : (a : α) → β → β) (b : β) : forIn (m := Id) o b (fun a b => .yield (f a b)) = - o.elim b (fun a => f a b) := by - cases o <;> simp + o.elim b (fun a => f a b) := + forIn_pure_yield_eq_elim _ _ _ @[simp, grind] theorem forIn_map [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) : diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 11e61a8385..a10a3813f7 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -2385,19 +2385,23 @@ theorem foldrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {b} {xs : V Array.foldrM_pure theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Vector α n} : - xs.foldl f b = xs.foldlM (m := Id) f b := by - rcases xs with ⟨xs, rfl⟩ - simp [Array.foldl_eq_foldlM] + xs.foldl f b = (xs.foldlM (m := Id) (pure <| f · ·) b).run := rfl theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Vector α n} : - xs.foldr f b = xs.foldrM (m := Id) f b := by - rcases xs with ⟨xs, rfl⟩ - simp [Array.foldr_eq_foldrM] + xs.foldr f b = (xs.foldrM (m := Id) (pure <| f · ·) b).run := rfl -@[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Vector α n} : +@[simp] theorem idRun_foldlM {f : β → α → Id β} {b} {xs : Vector α n} : + Id.run (xs.foldlM f b) = xs.foldl (f · · |>.run) b := foldl_eq_foldlM.symm + +@[deprecated idRun_foldlM (since := "2025-05-21")] +theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Vector α n} : Id.run (xs.foldlM f b) = xs.foldl f b := foldl_eq_foldlM.symm -@[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} : +@[simp] theorem idRun_foldrM {f : α → β → Id β} {b} {xs : Vector α n} : + Id.run (xs.foldrM f b) = xs.foldr (f · · |>.run) b := foldr_eq_foldrM.symm + +@[deprecated idRun_foldrM (since := "2025-05-21")] +theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} : Id.run (xs.foldrM f b) = xs.foldr f b := foldr_eq_foldrM.symm @[simp] theorem foldlM_reverse [Monad m] {xs : Vector α n} {f : β → α → m β} {b} : @@ -2485,10 +2489,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β → simp @[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs : Vector α n} {ys : Vector α k} : - (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by simp [foldl_eq_foldlM] + (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := foldlM_append @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b} {xs : Vector α n} {ys : Vector α k} : - (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by simp [foldr_eq_foldrM] + (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := foldrM_append @[simp, grind] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} : (flatten xss).foldl f b = xss.foldl (fun b xs => xs.foldl f b) b := by @@ -2501,7 +2505,8 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β → simp [Array.foldr_flatten', Array.foldr_map'] @[simp, grind] theorem foldl_reverse {xs : Vector α n} {f : β → α → β} {b} : - xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM] + xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := + foldlM_reverse @[simp, grind] theorem foldr_reverse {xs : Vector α n} {f : α → β → β} {b} : xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b := diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index c89a50b3d0..f02ea2cae5 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -60,7 +60,7 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton] - cases lt a b <;> cases a != b <;> simp [Id.run] + cases lt a b <;> cases a != b <;> simp protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (xs : Vector α n) : ¬ xs < xs := Array.lt_irrefl xs.toArray diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index cf30e5149c..b86c2cbd6b 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -148,12 +148,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs, rfl⟩ simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map] -@[simp] theorem forIn'_yield_eq_foldl +@[simp] theorem idRun_forIn'_yield_eq_foldl + {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : + (forIn' xs init (fun a m b => .yield <$> f a m b)).run = + xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := + forIn'_pure_yield_eq_foldl _ _ + +@[deprecated forIn'_yield_eq_foldl (since := "2025-05-21")] +theorem forIn'_yield_eq_foldl {xs : Vector α n} (f : (a : α) → a ∈ xs → β → β) (init : β) : forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) = - xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by - rcases xs with ⟨xs, rfl⟩ - simp [List.foldl_map] + xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := + forIn'_pure_yield_eq_foldl _ _ @[simp] theorem forIn'_map [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) : @@ -190,12 +196,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs, rfl⟩ simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map] -@[simp] theorem forIn_yield_eq_foldl +@[simp] theorem idRun_forIn_yield_eq_foldl + {xs : Vector α n} (f : α → β → Id β) (init : β) : + (forIn xs init (fun a b => .yield <$> f a b)).run = + xs.foldl (fun b a => f a b |>.run) init := + forIn_pure_yield_eq_foldl _ _ + +@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")] +theorem forIn_yield_eq_foldl {xs : Vector α n} (f : α → β → β) (init : β) : forIn (m := Id) xs init (fun a b => .yield (f a b)) = - xs.foldl (fun b a => f a b) init := by - rcases xs with ⟨xs, rfl⟩ - simp + xs.foldl (fun b a => f a b) init := + forIn_pure_yield_eq_foldl _ _ @[simp] theorem forIn_map [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)) : diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index 87002994b5..ee87ead869 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -154,7 +154,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} : @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} : Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by - unfold Id.run induction n with | zero => simp | succ n ih => simp [ofFnM_succ', ofFn_succ', ih] diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 9149369274..3d2aa43944 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1317,7 +1317,7 @@ test with the predicate `p`. The resulting array contains the tested elements fo `true`, separated by the corresponding separator elements. -/ def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax := - Id.run <| a.filterSepElemsM p + Id.run <| a.filterSepElemsM (pure <| p ·) private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do if h : i < a.size then @@ -1334,7 +1334,7 @@ def mapSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax mapSepElemsMAux a f 0 #[] def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax := - Id.run <| a.mapSepElemsM f + Id.run <| a.mapSepElemsM (pure <| f ·) end Array diff --git a/src/Lean/Compiler/LCNF/FVarUtil.lean b/src/Lean/Compiler/LCNF/FVarUtil.lean index 0bab20cac0..8e8380df1b 100644 --- a/src/Lean/Compiler/LCNF/FVarUtil.lean +++ b/src/Lean/Compiler/LCNF/FVarUtil.lean @@ -205,9 +205,9 @@ where if !(← f fvar) then failure def anyFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool := - Id.run <| anyFVarM f x + Id.run <| anyFVarM (pure <| f ·) x def allFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool := - Id.run <| allFVarM f x + Id.run <| allFVarM (pure <| f ·) x end Lean.Compiler.LCNF diff --git a/src/Lean/Data/AssocList.lean b/src/Lean/Data/AssocList.lean index 4ad955e28c..b7dae70c38 100644 --- a/src/Lean/Data/AssocList.lean +++ b/src/Lean/Data/AssocList.lean @@ -38,7 +38,7 @@ def isEmpty : AssocList α β → Bool foldlM f d es @[inline] def foldl (f : δ → α → β → δ) (init : δ) (as : AssocList α β) : δ := - Id.run (foldlM f init as) + Id.run (foldlM (pure <| f · · ·) init as) def toList (as : AssocList α β) : List (α × β) := as.foldl (init := []) (fun r a b => (a, b)::r) |>.reverse diff --git a/src/Lean/Data/NameTrie.lean b/src/Lean/Data/NameTrie.lean index 699bc98bd6..d08d4c7faa 100644 --- a/src/Lean/Data/NameTrie.lean +++ b/src/Lean/Data/NameTrie.lean @@ -75,9 +75,9 @@ def NameTrie.forM [Monad m] (t : NameTrie β) (f : β → m Unit) : m Unit := t.forMatchingM Name.anonymous f def NameTrie.matchingToArray (t : NameTrie β) (k : Name) : Array β := - Id.run <| t.foldMatchingM k #[] fun v acc => acc.push v + Id.run <| t.foldMatchingM k #[] fun v acc => return acc.push v def NameTrie.toArray (t : NameTrie β) : Array β := - Id.run <| t.foldM #[] fun v acc => acc.push v + Id.run <| t.foldM #[] fun v acc => return acc.push v end Lean diff --git a/src/Lean/Data/PersistentArray.lean b/src/Lean/Data/PersistentArray.lean index 7621caa344..c2b809f361 100644 --- a/src/Lean/Data/PersistentArray.lean +++ b/src/Lean/Data/PersistentArray.lean @@ -281,10 +281,10 @@ instance : ForIn m (PersistentArray α) α where end @[inline] def foldl (t : PersistentArray α) (f : β → α → β) (init : β) (start : Nat := 0) : β := - Id.run <| t.foldlM f init start + Id.run <| t.foldlM (pure <| f · ·) init start @[inline] def foldr (t : PersistentArray α) (f : α → β → β) (init : β) : β := - Id.run <| t.foldrM f init + Id.run <| t.foldrM (pure <| f · ·) init @[inline] def filter (as : PersistentArray α) (p : α → Bool) : PersistentArray α := as.foldl (init := {}) fun asNew a => if p a then asNew.push a else asNew @@ -301,10 +301,10 @@ def append (t₁ t₂ : PersistentArray α) : PersistentArray α := instance : Append (PersistentArray α) := ⟨append⟩ @[inline] def findSome? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β := - Id.run $ t.findSomeM? f + Id.run $ t.findSomeM? (pure <| f ·) @[inline] def findSomeRev? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β := - Id.run $ t.findSomeRevM? f + Id.run $ t.findSomeRevM? (pure <| f ·) def toList (t : PersistentArray α) : List α := (t.foldl (init := []) fun xs x => x :: xs).reverse @@ -325,7 +325,7 @@ variable {m : Type → Type w} [Monad m] end @[inline] def any (a : PersistentArray α) (p : α → Bool) : Bool := - Id.run $ anyM a p + Id.run $ anyM a (pure <| p ·) @[inline] def all (a : PersistentArray α) (p : α → Bool) : Bool := !any a fun v => !p v @@ -346,7 +346,7 @@ variable {β : Type u} end @[inline] def map {β} (f : α → β) (t : PersistentArray α) : PersistentArray β := - Id.run $ t.mapM f + Id.run $ t.mapM (pure <| f ·) structure Stats where numNodes : Nat diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean index 90df37be75..fdc0baf88c 100644 --- a/src/Lean/Data/PersistentHashMap.lean +++ b/src/Lean/Data/PersistentHashMap.lean @@ -288,7 +288,7 @@ def forM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : α map.foldlM (fun _ => f) ⟨⟩ def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ := - Id.run <| map.foldlM f init + Id.run <| map.foldlM (pure <| f · · ·) init protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m] (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do @@ -322,7 +322,7 @@ def mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Mona return { root } def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β → σ) : PersistentHashMap α σ := - Id.run <| pm.mapM f + Id.run <| pm.mapM (pure <| f ·) def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) := m.foldl (init := []) fun ps k v => (k, v) :: ps diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean index 1ead5c97f0..fe6de94171 100644 --- a/src/Lean/Data/PersistentHashSet.lean +++ b/src/Lean/Data/PersistentHashSet.lean @@ -48,7 +48,7 @@ variable {_ : BEq α} {_ : Hashable α} s.set.foldlM (init := init) fun d a _ => f d a @[inline] def fold {β : Type v} (f : β → α → β) (init : β) (s : PersistentHashSet α) : β := - Id.run $ s.foldM f init + Id.run $ s.foldM (pure <| f · ·) init def toList (s : PersistentHashSet α) : List α := s.set.toList.map (·.1) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index acb33a448b..434d9343be 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -315,7 +315,7 @@ def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) /-- Waits on and returns all snapshots in the tree. -/ def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot := - Id.run <| s.foldM (·.push ·) #[] + Id.run <| s.foldM (pure <| ·.push ·) #[] /-- Returns a task that waits on all snapshots in the tree. -/ def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit) diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index f946726d33..a47d50ea82 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -397,19 +397,19 @@ instance : ForIn m LocalContext LocalDecl where | some d => f d b @[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β := - Id.run <| lctx.foldlM f init start + Id.run <| lctx.foldlM (pure <| f · ·) init start @[inline] def foldr (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) : β := - Id.run <| lctx.foldrM f init + Id.run <| lctx.foldrM (pure <| f · ·) init def size (lctx : LocalContext) : Nat := lctx.foldl (fun n _ => n+1) 0 @[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β := - Id.run <| lctx.findDeclM? f + Id.run <| lctx.findDeclM? (pure <| f ·) @[inline] def findDeclRev? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β := - Id.run <| lctx.findDeclRevM? f + Id.run <| lctx.findDeclRevM? (pure <| f ·) partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool := if h : i < a₁.size then @@ -473,11 +473,11 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr := /-- Return `true` if `lctx` contains a local declaration satisfying `p`. -/ @[inline] def any (lctx : LocalContext) (p : LocalDecl → Bool) : Bool := - Id.run <| lctx.anyM p + Id.run <| lctx.anyM (pure <| p ·) /-- Return `true` if all declarations in `lctx` satisfy `p`. -/ @[inline] def all (lctx : LocalContext) (p : LocalDecl → Bool) : Bool := - Id.run <| lctx.allM p + Id.run <| lctx.allM (pure <| p ·) /-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones contains macroscopes. -/ def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext := do diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index 57b229b4b3..a95b43ca8c 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -795,7 +795,7 @@ Fold the values stored in a `Trie`. -/ @[inline] def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ := - Id.run <| t.foldValuesM (init := init) f + Id.run <| t.foldValuesM (init := init) (pure <| f · ·) /-- The number of values stored in a `Trie`. @@ -835,7 +835,7 @@ Fold over the values stored in a `DiscrTree`. -/ @[inline] def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ := - Id.run <| t.foldValuesM (init := init) f + Id.run <| t.foldValuesM (init := init) (pure <| f · ·) /-- Check for the presence of a value satisfying a predicate. diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index d4451d14e3..eb08abab23 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1975,7 +1975,7 @@ def foldArgsM (s : Syntax) (f : Syntax → β → m β) (b : β) : m β := s.getArgs.foldlM (flip f) b def foldArgs (s : Syntax) (f : Syntax → β → β) (b : β) : β := - Id.run (s.foldArgsM f b) + Id.run (s.foldArgsM (pure <| f · ·) b) def forArgsM (s : Syntax) (f : Syntax → m Unit) : m Unit := s.foldArgsM (fun s _ => f s) () diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index 0b694a8326..306bcc1821 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -67,7 +67,7 @@ private partial def mkErrorMessage (c : InputContext) (pos : String.Pos) (stk : where -- Error recovery might lead to there being some "junk" on the stack lastTrailing (s : SyntaxStack) : Option Substring := - s.toSubarray.findSomeRevM? (m := Id) fun stx => + Id.run <| s.toSubarray.findSomeRevM? fun stx => if let .original (trailing := trailing) .. := stx.getTailInfo then pure (some trailing) else none diff --git a/src/Lean/Server/Completion/EligibleHeaderDecls.lean b/src/Lean/Server/Completion/EligibleHeaderDecls.lean index 56eed2f16c..ef2ec82b4a 100644 --- a/src/Lean/Server/Completion/EligibleHeaderDecls.lean +++ b/src/Lean/Server/Completion/EligibleHeaderDecls.lean @@ -23,8 +23,8 @@ def getEligibleHeaderDecls (env : Environment) : IO EligibleHeaderDecls := do eligibleHeaderDeclsRef.modifyGet fun | some eligibleHeaderDecls => (eligibleHeaderDecls, some eligibleHeaderDecls) | none => - let (_, eligibleHeaderDecls) := - StateT.run (m := Id) (s := {}) do + let (_, eligibleHeaderDecls) := Id.run <| + StateT.run (s := {}) do -- `map₁` are the header decls env.constants.map₁.forM fun declName c => do modify fun eligibleHeaderDecls => diff --git a/src/Lean/Server/Completion/SyntheticCompletion.lean b/src/Lean/Server/Completion/SyntheticCompletion.lean index f855522e9e..0473271f7c 100644 --- a/src/Lean/Server/Completion/SyntheticCompletion.lean +++ b/src/Lean/Server/Completion/SyntheticCompletion.lean @@ -15,7 +15,7 @@ private def findBest? (gt : α → α → Bool) (f : ContextInfo → Info → PersistentArray InfoTree → Option α) : Option α := - infoTree.visitM (m := Id) (postNode := choose) |>.join + (Id.run <| infoTree.visitM (postNode := choose)).join where choose (ctx : ContextInfo) diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 636d576c22..b27a7b54f2 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -77,7 +77,7 @@ def InfoTree.collectNodesBottomUpM [Monad m] (p : ContextInfo → Info → Persi /-- Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/ def InfoTree.collectNodesBottomUp (p : ContextInfo → Info → PersistentArray InfoTree → List α → List α) (i : InfoTree) : List α := - i.collectNodesBottomUpM (m := Id) p + Id.run <| i.collectNodesBottomUpM (pure <| p · · · ·) /-- For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns @@ -97,7 +97,7 @@ partial def InfoTree.deepestNodesM [Monad m] (p : ContextInfo → Info → Persi `some _` and return the union of all such nodes. The visitor `p` is given a node together with its innermost surrounding `ContextInfo`. -/ partial def InfoTree.deepestNodes (p : ContextInfo → Info → PersistentArray InfoTree → Option α) (infoTree : InfoTree) : List α := - infoTree.deepestNodesM (m := Id) p + Id.run <| infoTree.deepestNodesM (pure <| p · · ·) partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α := go none init @@ -237,7 +237,7 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) (omitIdentApps := false) : Option InfoWithCtx := Id.run do - let results := t.visitM (m := Id) (postNode := fun ctx info children results => do + let results := (← t.visitM (postNode := fun ctx info children results => do let mut results := results.flatMap (·.getD []) if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then results := results.filter (·.2.info.stx != info.stx[0]) @@ -267,7 +267,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in Int.negOfNat (r.stop - r.start).byteIdx, -- prefer results for constants over variables (which overlap at declaration names) if info matches .ofTermInfo { expr := .fvar .., .. } then 0 else 1) - [(priority, {ctx, info, children})]) |>.getD [] + [(priority, {ctx, info, children})])) |>.getD [] -- sort results by lexicographical priority let maxPrio? := let _ := @lexOrd diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 309eda5857..2b6bbd4668 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -76,7 +76,7 @@ def depth (p : Pos) := /-- Returns true if `pred` is true for each coordinate in `p`.-/ def all (pred : Nat → Bool) (p : Pos) : Bool := - OptionT.run (m := Id) (foldrM (fun n a => if pred n then pure a else failure) p ()) |>.isSome + (Id.run <| OptionT.run (foldrM (fun n a => if pred n then pure a else failure) p ())) |>.isSome def append : Pos → Pos → Pos := foldl push diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 61fa9fc7b3..38b7d99eb9 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -235,7 +235,7 @@ partial def hasIdent (id : Name) : Syntax → Bool | stx => fn stx @[inline] def rewriteBottomUp (fn : Syntax → Syntax) (stx : Syntax) : Syntax := - Id.run <| stx.rewriteBottomUpM fn + Id.run <| stx.rewriteBottomUpM (pure <| fn ·) private def updateInfo : SourceInfo → String.Pos → String.Pos → SourceInfo | SourceInfo.original lead pos trail endPos, leadStart, trailStop => diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean index 84bb11bac4..9ed98fbbae 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean @@ -49,7 +49,7 @@ namespace AssocList /-- Internal implementation detail of the hash map -/ @[inline] def foldl (f : δ → (α : α) → β α → δ) (init : δ) (as : AssocList α β) : δ := - Id.run (foldlM f init as) + Id.run (foldlM (pure <| f · · ·) init as) /-- Internal implementation detail of the hash map -/ @[specialize] def foldrM (f : (a : α) → β a → δ → m δ) : (init : δ) → AssocList α β → m δ @@ -60,7 +60,7 @@ namespace AssocList /-- Internal implementation detail of the hash map -/ @[inline] def foldr (f : (a : α) → β a → δ → δ) (init : δ) (as : AssocList α β) : δ := - Id.run (foldrM f init as) + Id.run (foldrM (pure <| f · · ·) init as) /-- Internal implementation detail of the hash map -/ @[inline] def forM (f : (a : α) → β a → m PUnit) (as : AssocList α β) : m PUnit := diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index 223fe41794..283e7da693 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -36,7 +36,7 @@ open Std.Internal @[simp] theorem foldl_eq {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocList α β} : l.foldl f init = l.toList.foldl (fun d p => f d p.1 p.2) init := by - induction l generalizing init <;> simp_all [foldl, Id.run, foldlM] + induction l generalizing init <;> simp_all [foldl, foldlM] @[simp] theorem length_eq {l : AssocList α β} : l.length = l.toList.length := by @@ -260,11 +260,11 @@ end Const theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) : l.foldl (fun acc k v => f k v :: acc) acc = (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by - induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run] + induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM] theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) : l.foldr (fun k v acc => f k v :: acc) acc = (l.toList.map (fun p => f p.1 p.2)) ++ acc := by - induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run] + induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM] end Std.DHashMap.Internal.AssocList diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index e2251ad8f2..b533097fdb 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -596,7 +596,7 @@ theorem filter_eq_filterₘ (m : Raw₀ α β) (f : (a : α) → β a → Bool) m.filter f = m.filterₘ f := rfl theorem insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α β) (l : List ((a : α) × β a)) : insertMany m l = insertListₘ m l := by - simp only [insertMany, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl] + simp only [insertMany, Id.run_pure, Id.run_bind, pure_bind, List.forIn_pure_yield_eq_foldl] suffices ∀ (t : { m' // ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) → P m → P m' }), (List.foldl (fun m' p => ⟨m'.val.insert p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val = @@ -639,9 +639,9 @@ theorem Const.getThenInsertIfNew?_eq_get?ₘ [BEq α] [Hashable α] (m : Raw₀ split <;> simp_all [-getValue?_eq_none] theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) - (l: List (α × β)): + (l : List (α × β)) : (Const.insertMany m l).1 = Const.insertListₘ m l := by - simp only [insertMany, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl] + simp only [insertMany, Id.run_pure, pure_bind, List.forIn_pure_yield_eq_foldl] suffices ∀ (t : { m' // ∀ (P : Raw₀ α (fun _ => β) → Prop), (∀ {m'' : Raw₀ α (fun _ => β)} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }), (List.foldl (fun m' p => ⟨m'.val.insert p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val = @@ -656,7 +656,7 @@ theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => Unit)) (l: List α): (Const.insertManyIfNewUnit m l).1 = Const.insertListIfNewUnitₘ m l := by - simp only [insertManyIfNewUnit, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl] + simp only [insertManyIfNewUnit, Id.run_pure, Id.run_bind, pure_bind, List.forIn_pure_yield_eq_foldl] suffices ∀ (t : { m' // ∀ (P : Raw₀ α (fun _ => Unit) → Prop), (∀ {m'' a b}, P m'' → P (m''.insertIfNew a b)) → P m → P m'}), (List.foldl (fun m' p => ⟨m'.val.insertIfNew p (), fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val = diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index c4c2a7bc00..b9baaf5431 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -1210,12 +1210,12 @@ theorem insertMany_ind {motive : Raw₀ α β → Prop} (m : Raw₀ α β) (l : @[simp] theorem insertMany_nil : m.insertMany [] = m := by - simp [insertMany, Id.run] + simp [insertMany] @[simp] theorem insertMany_list_singleton {k : α} {v : β k} : m.insertMany [⟨k, v⟩] = m.insert k v := by - simp [insertMany, Id.run] + simp [insertMany] theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} : (m.insertMany (⟨k, v⟩ :: l)).1 = ((m.insert k v).insertMany l).1 := by @@ -1412,12 +1412,12 @@ theorem insertMany_ind {motive : Raw₀ α (fun _ => β) → Prop} (m : Raw₀ @[simp] theorem insertMany_nil : insertMany m [] = m := by - simp [insertMany, Id.run] + simp [insertMany] @[simp] theorem insertMany_list_singleton {k : α} {v : β} : insertMany m [⟨k, v⟩] = m.insert k v := by - simp [insertMany, Id.run] + simp [insertMany] theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} : (insertMany m (⟨k, v⟩ :: l)).1 = (insertMany (m.insert k v) l).1 := by @@ -1613,12 +1613,12 @@ theorem insertManyIfNewUnit_ind {motive : Raw₀ α (fun _ => Unit) → Prop} @[simp] theorem insertManyIfNewUnit_nil : insertManyIfNewUnit m [] = m := by - simp [insertManyIfNewUnit, Id.run] + simp [insertManyIfNewUnit] @[simp] theorem insertManyIfNewUnit_list_singleton {k : α} : insertManyIfNewUnit m [k] = m.insertIfNew k () := by - simp [insertManyIfNewUnit, Id.run] + simp [insertManyIfNewUnit] theorem insertManyIfNewUnit_cons {l : List α} {k : α} : (insertManyIfNewUnit m (k :: l)).1 = (insertManyIfNewUnit (m.insertIfNew k ()) l).1 := by diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 37c899f254..64216b8cf8 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -69,9 +69,7 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp Nat.beq_eq_true_eq] theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} : - l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := by - simp only [Raw.fold, Raw.foldM, ← Array.foldlM_toList, Array.foldl_toList, - ← List.foldl_eq_foldlM, Id.run, AssocList.foldl] + l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := rfl theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) : l.fold (fun acc k v => f k v :: acc) acc = @@ -94,8 +92,7 @@ theorem fold_cons_key {l : Raw α β} {acc : List α} : theorem foldRev_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} : Raw.Internal.foldRev f init l = l.buckets.foldr (fun l acc => l.foldr (fun a b g => f g a b) acc) init := by - simp only [Raw.Internal.foldRev, Raw.Internal.foldRevM, ← Array.foldrM_toList, Array.foldr_toList, - ← List.foldr_eq_foldrM, Id.run, AssocList.foldr] + simp only [Raw.Internal.foldRev, Raw.Internal.foldRevM, Array.id_run_foldrM, AssocList.foldr] theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) : Raw.Internal.foldRev (fun acc k v => f k v :: acc) acc l = @@ -261,7 +258,7 @@ theorem isHashSelf_foldl_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [Lawfu IsHashSelf target.1 → IsHashSelf (l.foldl (fun acc p => reinsertAux hash acc p.1 p.2) target).1 := by induction l generalizing target - · simp [Id.run] + · simp · next k v _ ih => exact fun h => ih _ (isHashSelf_reinsertAux _ _ _ h) theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α] diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index e415eb1e8a..8176be6da8 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -357,7 +357,7 @@ map in some order. /-- Folds the given function over the mappings in the hash map in some order. -/ @[inline] def fold (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := - Id.run (b.foldM f init) + Id.run (b.foldM (pure <| f · · ·) init) namespace Internal @@ -376,7 +376,7 @@ Internal implementation detail of the hash map. Folds the given function over the mappings in the hash map in the reverse order used by `foldM`. -/ @[inline] def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := - Id.run (foldRevM f init b) + Id.run (foldRevM (pure <| f · · ·) init b) end Internal @@ -395,7 +395,7 @@ by `foldM`. -/ @[inline, deprecated "Deprecated without replacement. If the order does not matter, use fold." (since := "2025-03-07")] def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := - Id.run (Internal.foldRevM f init b) + Id.run (Internal.foldRevM (pure <| f · · ·) init b) /-- Carries out a monadic action on each mapping in the hash map in some order. -/ @[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit := diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean index e04ce2905c..b8b3709d5a 100644 --- a/src/Std/Data/DTreeMap/Internal/Queries.lean +++ b/src/Std/Data/DTreeMap/Internal/Queries.lean @@ -200,7 +200,7 @@ def foldlM {m} [Monad m] (f : δ → (a : α) → β a → m δ) (init : δ) : I /-- Folds the given function over the mappings in the tree in ascending order. -/ @[specialize] def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : Impl α β) : δ := - Id.run (t.foldlM f init) + Id.run (t.foldlM (pure <| f · · ·) init) /-- Folds the given function over the mappings in the tree in descending order. -/ @[specialize] @@ -214,7 +214,7 @@ def foldrM {m} [Monad m] (f : (a : α) → β a → δ → m δ) (init : δ) : I /-- Folds the given function over the mappings in the tree in descending order. -/ @[inline] def foldr (f : (a : α) → β a → δ → δ) (init : δ) (t : Impl α β) : δ := - Id.run (t.foldrM f init) + Id.run (t.foldrM (pure <| f · · ·) init) /-- Applies the given function to the mappings in the tree in ascending order. -/ @[inline] diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index d96e586172..990268b4a9 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1189,7 +1189,7 @@ theorem foldlM_toListModel_eq_foldlM {t : Impl α β} {m δ} [Monad m] [LawfulMo theorem foldl_eq_foldl {t : Impl α β} {δ} {f : δ → (a : α) → β a → δ} {init} : t.foldl (init := init) f = t.toListModel.foldl (init := init) fun acc p => f acc p.1 p.2 := by - rw [foldl, foldlM_eq_foldlM_toListModel, List.foldl_eq_foldlM, Id.run] + rw [foldl, foldlM_eq_foldlM_toListModel, List.foldl_eq_foldlM] /-! ### foldrM @@ -1210,7 +1210,7 @@ theorem foldrM_eq_foldrM {t : Impl α β} {m δ} [Monad m] [LawfulMonad m] theorem foldr_eq_foldr {t : Impl α β} {δ} {f : (a : α) → β a → δ → δ} {init} : t.foldr (init := init) f = t.toListModel.foldr (init := init) fun p acc => f p.1 p.2 acc := by - rw [foldr, foldrM_eq_foldrM, List.foldr_eq_foldrM, Id.run] + rw [foldr, foldrM_eq_foldrM, List.foldr_eq_foldrM] /-! ### toList @@ -1542,11 +1542,11 @@ theorem WF.eraseMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ α] {l : ρ} theorem insertMany!_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} : (t.insertMany! l).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by - simp [insertMany!, Id.run, ← List.foldl_hom Subtype.val] + simp [insertMany!, ← List.foldl_hom Subtype.val, List.forIn_pure_yield_eq_foldl] theorem insertMany_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertMany l h).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by - simp [insertMany, Id.run, insert_eq_insert!, ← List.foldl_hom Subtype.val] + simp [insertMany, insert_eq_insert!, ← List.foldl_hom Subtype.val, List.forIn_pure_yield_eq_foldl] theorem insertMany_eq_insertMany! {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : @@ -1592,15 +1592,14 @@ variable {β : Type v} theorem insertMany!_eq_foldl {_ : Ord α} {l : List (α × β)} {t : Impl α β} : (insertMany! t l).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by - simp only [insertMany!, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl] + simp only [insertMany!, Id.run_pure, pure_bind, List.forIn_pure_yield_eq_foldl] rw [← List.foldl_hom Subtype.val] simp only [implies_true] theorem insertMany_eq_foldl {_ : Ord α} {l : List (α × β)} {t : Impl α β} (h : t.Balanced) : (Const.insertMany t l h).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by - simp only [insertMany, Id.run, Id.pure_eq, insert_eq_insert!, Id.bind_eq, - List.forIn_yield_eq_foldl] + simp only [insertMany, Id.run_pure, insert_eq_insert!, pure_bind, List.forIn_pure_yield_eq_foldl] rw [← List.foldl_hom Subtype.val] simp only [implies_true] @@ -1627,13 +1626,13 @@ theorem toListModel_insertMany!_list {_ : Ord α} [BEq α] [LawfulBEqOrd α] [Tr theorem insertManyIfNewUnit_eq_foldl {_ : Ord α} {l : List α} {t : Impl α Unit} (h : t.Balanced) : (Const.insertManyIfNewUnit t l h).val = l.foldl (init := t) fun acc k => acc.insertIfNew! k () := by - simp only [insertManyIfNewUnit, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl] + simp only [insertManyIfNewUnit, Id.run_pure, pure_bind, List.forIn_pure_yield_eq_foldl] rw [← List.foldl_hom Subtype.val] simp only [insertIfNew_eq_insertIfNew!, implies_true] theorem insertManyIfNewUnit!_eq_foldl {_ : Ord α} {l : List α} {t : Impl α Unit} : (Const.insertManyIfNewUnit! t l).val = l.foldl (init := t) fun acc k => acc.insertIfNew! k () := by - simp only [insertManyIfNewUnit!, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl] + simp only [insertManyIfNewUnit!, Id.run_pure, pure_bind, List.forIn_pure_yield_eq_foldl] rw [← List.foldl_hom Subtype.val] simp only [implies_true] @@ -1687,8 +1686,8 @@ theorem mergeWith_eq_mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t induction t₂ generalizing t₁ with | leaf => rfl | inner sz k v l r ihl ihr => - simp only [foldl, foldlM, Id.run, bind] - simp only [foldl, Id.run, bind] at ihl ihr + simp only [foldl, foldlM, pure_bind, Id.run_bind] + simp only [foldl] at ihl ihr rw [ihr] congr simp only [SizedBalancedTree.toBalancedTree] @@ -1708,8 +1707,8 @@ theorem Const.mergeWith_eq_mergeWith! {β : Type v} {_ : Ord α} {mergeFn} {t₁ induction t₂ generalizing t₁ with | leaf => rfl | inner sz k v l r ihl ihr => - simp only [foldl, foldlM, Id.run, bind] - simp only [foldl, Id.run, bind] at ihl ihr + simp only [foldl, foldlM, Id.run_bind, pure_bind] + simp only [foldl] at ihl ihr rw [ihr] congr simp only [SizedBalancedTree.toBalancedTree] diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean index 985ff43924..46397af7fd 100644 --- a/src/Std/Data/ExtDHashMap/Lemmas.lean +++ b/src/Std/Data/ExtDHashMap/Lemmas.lean @@ -965,7 +965,7 @@ theorem insertMany_cons [EquivBEq α] [LawfulHashable α] m.insertMany (p :: l) = (m.insert p.1 p.2).insertMany l := by rcases p with ⟨k, v⟩ unfold insertMany - simp only [Id.pure_eq, Id.bind_eq, Id.run, List.forIn_yield_eq_foldl, List.foldl_cons] + simp only [bind_pure_comp, map_pure, List.forIn_pure_yield_eq_foldl, List.foldl_cons, Id.run_pure] refine Eq.trans ?_ (Eq.symm ?_ : l.foldl (fun b a => b.insert a.1 a.2) (m.insert k v) = _) exact (List.foldl_hom (f := Subtype.val) fun x y => rfl).symm exact (List.foldl_hom (f := Subtype.val) fun x y => rfl).symm @@ -1228,7 +1228,7 @@ theorem insertMany_cons [EquivBEq α] [LawfulHashable α] {l : List (α × β)} insertMany m (p :: l) = insertMany (m.insert p.1 p.2) l := by rcases p with ⟨k, v⟩ unfold insertMany - simp only [Id.pure_eq, Id.bind_eq, Id.run, List.forIn_yield_eq_foldl, List.foldl_cons] + simp only [bind_pure_comp, map_pure, List.forIn_pure_yield_eq_foldl, List.foldl_cons, Id.run_pure] refine Eq.trans ?_ (Eq.symm ?_ : l.foldl (fun b a => b.insert a.1 a.2) (m.insert k v) = _) exact (List.foldl_hom (f := Subtype.val) fun x y => rfl).symm exact (List.foldl_hom (f := Subtype.val) fun x y => rfl).symm @@ -1492,7 +1492,7 @@ theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] {k theorem insertManyIfNewUnit_cons [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : insertManyIfNewUnit m (k :: l) = insertManyIfNewUnit (m.insertIfNew k ()) l := by unfold insertManyIfNewUnit - simp only [Id.pure_eq, Id.bind_eq, Id.run, List.forIn_yield_eq_foldl, List.foldl_cons] + simp only [bind_pure_comp, map_pure, List.forIn_pure_yield_eq_foldl, List.foldl_cons, Id.run_pure] refine Eq.trans ?_ (Eq.symm ?_ : l.foldl (fun b a => b.insertIfNew a ()) (m.insertIfNew k ()) = _) exact (List.foldl_hom (f := Subtype.val) fun x y => rfl).symm exact (List.foldl_hom (f := Subtype.val) fun x y => rfl).symm diff --git a/src/Std/Data/Iterators/Consumers/Collect.lean b/src/Std/Data/Iterators/Consumers/Collect.lean index e4104c5625..6426153b34 100644 --- a/src/Std/Data/Iterators/Consumers/Collect.lean +++ b/src/Std/Data/Iterators/Consumers/Collect.lean @@ -27,31 +27,31 @@ namespace Std.Iterators @[always_inline, inline, inherit_doc IterM.toArray] def Iter.toArray {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] (it : Iter (α := α) β) : Array β := - it.toIterM.toArray + it.toIterM.toArray.run @[always_inline, inline, inherit_doc IterM.Partial.toArray] def Iter.Partial.toArray {α : Type w} {β : Type w} [Iterator α Id β] [IteratorCollectPartial α Id] (it : Iter.Partial (α := α) β) : Array β := - it.it.toIterM.allowNontermination.toArray + it.it.toIterM.allowNontermination.toArray.run @[always_inline, inline, inherit_doc IterM.toListRev] def Iter.toListRev {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β := - it.toIterM.toListRev + it.toIterM.toListRev.run @[always_inline, inline, inherit_doc IterM.Partial.toListRev] def Iter.Partial.toListRev {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter.Partial (α := α) β) : List β := - it.it.toIterM.allowNontermination.toListRev + it.it.toIterM.allowNontermination.toListRev.run @[always_inline, inline, inherit_doc IterM.toList] def Iter.toList {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] (it : Iter (α := α) β) : List β := - it.toIterM.toList + it.toIterM.toList.run @[always_inline, inline, inherit_doc IterM.Partial.toList] def Iter.Partial.toList {α : Type w} {β : Type w} [Iterator α Id β] [IteratorCollectPartial α Id] (it : Iter.Partial (α := α) β) : List β := - it.it.toIterM.allowNontermination.toList + it.it.toIterM.allowNontermination.toList.run end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean index 688572dcc2..d272c2a390 100644 --- a/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean +++ b/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -13,42 +13,40 @@ namespace Std.Iterators theorem Iter.toArray_eq_toArray_toIterM {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : - it.toArray = it.toIterM.toArray := + it.toArray = it.toIterM.toArray.run := rfl theorem Iter.toList_eq_toList_toIterM {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : - it.toList = it.toIterM.toList := + it.toList = it.toIterM.toList.run := rfl theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} : - it.toListRev = it.toIterM.toListRev := + it.toListRev = it.toIterM.toListRev.run := rfl @[simp] theorem IterM.toList_toIter {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] {it : IterM (α := α) Id β} : - it.toIter.toList = it.toList := + it.toIter.toList = it.toList.run := rfl @[simp] theorem IterM.toListRev_toIter {α β} [Iterator α Id β] [Finite α Id] {it : IterM (α := α) Id β} : - it.toIter.toListRev = it.toListRev := + it.toIter.toListRev = it.toListRev.run := rfl theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : it.toArray.toList = it.toList := by - simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray, - Id.map_eq] + simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray] theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : it.toList.toArray = it.toArray := by - simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList, - Id.map_eq] + simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList] theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : @@ -62,9 +60,8 @@ theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [I | .skip it' _ => it'.toArray | .done _ => #[] := by simp only [Iter.toArray_eq_toArray_toIterM, Iter.step] - rw [IterM.toArray_eq_match_step] - simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run] - generalize it.toIterM.step = step + rw [IterM.toArray_eq_match_step, Id.run_bind] + generalize it.toIterM.step.run = step cases step using PlausibleIterStep.casesOn <;> simp theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] @@ -81,9 +78,8 @@ theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] | .yield it' out _ => it'.toListRev ++ [out] | .skip it' _ => it'.toListRev | .done _ => [] := by - rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_eq_match_step, Iter.step] - simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run] - generalize it.toIterM.step = step + rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_eq_match_step, Iter.step, Id.run_bind] + generalize it.toIterM.step.run = step cases step using PlausibleIterStep.casesOn <;> simp theorem Iter.getElem?_toList_eq_atIdxSlow? {α β} diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean index 8ebfc93213..18f8f08a6d 100644 --- a/src/lake/Lake/Reservoir.lean +++ b/src/lake/Lake/Reservoir.lean @@ -145,10 +145,10 @@ def uriEscapeByte (b : UInt8) (s := "") : String := return s abbrev foldlUtf8 (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ := - Id.run <| foldlUtf8M c f init + Id.run <| foldlUtf8M c (pure <| f · ·) init example : foldlUtf8 c (fun l b => b::l) List.nil = (String.utf8EncodeChar c).reverse := by - simp only [foldlUtf8M, String.utf8EncodeChar, Id.run] + simp only [foldlUtf8, foldlUtf8M, String.utf8EncodeChar] if h1 : c.val ≤ 0x7f then simp [h1] else if h2 : c.val ≤ 0x7ff then simp [h1, h2] else if h3 : c.val ≤ 0xffff then simp [h1, h2, h3] diff --git a/tests/lean/autoBoundImplicits1.lean b/tests/lean/autoBoundImplicits1.lean index 1403b2a093..bd28954d15 100644 --- a/tests/lean/autoBoundImplicits1.lean +++ b/tests/lean/autoBoundImplicits1.lean @@ -62,7 +62,7 @@ def findSomeRevM? [Monad m] (as : Array α) (f : α → m (Option β)) : m (Opti pure none def findSomeRev? (as : Array α) (f : α → Option β) : Option β := - Id.run <| findSomeRevM? as f + Id.run <| findSomeRevM? as (pure <| f ·) end Ex1 diff --git a/tests/lean/run/1293.lean b/tests/lean/run/1293.lean index 6834e8df70..54805603ae 100644 --- a/tests/lean/run/1293.lean +++ b/tests/lean/run/1293.lean @@ -1,5 +1,5 @@ theorem modifySize {A : Type u} (as : Array A) (f : A → A) (n : Nat) : (as.modify n f).size = as.size := by - simp [Array.modify, Array.modifyM, Id.run]; split <;> simp [Id.run] + simp [Array.modify, Array.modifyM]; split <;> simp structure Idx (p : Array String) where n : Fin p.size diff --git a/tests/lean/run/array_simp.lean b/tests/lean/run/array_simp.lean index ad5c6da7df..fc95ebbc05 100644 --- a/tests/lean/run/array_simp.lean +++ b/tests/lean/run/array_simp.lean @@ -11,7 +11,6 @@ attribute [-simp] Nat.default_eq_zero -- undo changes to simp set after this tes variable {xs : Array α} in #check_simp xs.size = 0 ~> xs = #[] -attribute [local simp] Id.run in #check_simp (Id.run do let mut s := 0 @@ -19,7 +18,6 @@ attribute [local simp] Id.run in s := s + i pure s) ~> 10 -attribute [local simp] Id.run in #check_simp (Id.run do let mut s := 0 diff --git a/tests/lean/run/fib_correct.lean b/tests/lean/run/fib_correct.lean index 2e056923e5..afbb23f570 100644 --- a/tests/lean/run/fib_correct.lean +++ b/tests/lean/run/fib_correct.lean @@ -34,7 +34,7 @@ def fib_impl (n : Nat) := Id.run do theorem fib_correct {n} : fib_impl n = fib_spec n := by -- The default simp set eliminates the binds generated by `do` notation, -- and converts the `for` loop into a `List.foldl` over `List.range'`. - simp [fib_impl, Id.run] + simp [fib_impl] match n with | 0 => simp [fib_spec] | n+1 => diff --git a/tests/lean/run/list_simp.lean b/tests/lean/run/list_simp.lean index 4ecfaf657a..29f0caf3f6 100644 --- a/tests/lean/run/list_simp.lean +++ b/tests/lean/run/list_simp.lean @@ -467,7 +467,7 @@ example (f : Fin 3 → Nat) : List.ofFn f = [f 0, f 1, f 2] := rfl example (f : Fin 3 → Nat) : Fin.foldl 3 (fun acc i => f i :: acc) [] = [f 2, f 1, f 0] := rfl /-! ## Monadic operations -/ -attribute [local simp] Id.run in + #check_simp (Id.run do let mut s := 0 @@ -475,7 +475,6 @@ attribute [local simp] Id.run in s := s + i pure s) ~> 10 -attribute [local simp] Id.run in #check_simp (Id.run do let mut s := 0 @@ -483,7 +482,6 @@ attribute [local simp] Id.run in s := s + i pure s) ~> 10 -attribute [local simp] Id.run in variable (l : List α) (k m : Nat) in #check_simp (Id.run do diff --git a/tests/lean/run/treeNode.lean b/tests/lean/run/treeNode.lean index 0174a8a47d..dd8105b56b 100644 --- a/tests/lean/run/treeNode.lean +++ b/tests/lean/run/treeNode.lean @@ -14,7 +14,7 @@ def treeToList (t : TreeNode) : List String := return r @[simp] theorem treeToList_eq (name : String) (children : List TreeNode) : treeToList (.mkNode name children) = name :: List.flatten (children.map treeToList) := by - simp [treeToList, Id.run] + simp [treeToList] mutual def numNames : TreeNode → Nat diff --git a/tests/lean/run/treemap.lean b/tests/lean/run/treemap.lean index 5b54373db0..16d85cd043 100644 --- a/tests/lean/run/treemap.lean +++ b/tests/lean/run/treemap.lean @@ -36,13 +36,13 @@ example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := (mkTreeMapSingleton a b)[a]? example [TransOrd α] (a : α) (b : β) : (mkTreeMapSingleton a b).contains a := by - simp [mkTreeMapSingleton, Id.run] + simp [mkTreeMapSingleton] example [TransOrd α] (a : α) (b : β) : (mkDTreeMapSingleton a b).contains a := by - simp [mkDTreeMapSingleton, Id.run] + simp [mkDTreeMapSingleton] example [TransOrd α] (a : α) : (mkTreeSetSingleton a).contains a := by - simp [mkTreeSetSingleton, Id.run] + simp [mkTreeSetSingleton] namespace DTreeMap.Raw diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean index 55dda3ae00..3debaafff8 100644 --- a/tests/lean/run/wfOverapplicationIssue.lean +++ b/tests/lean/run/wfOverapplicationIssue.lean @@ -1,6 +1,6 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h - let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by + let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => pure <| decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by unfold anyM.loop intro h split at h