From 7e3e7cf5d9dbbe272ff2e244df0e36ad7f36231d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Fri, 20 Mar 2026 11:39:40 +0000 Subject: [PATCH] feat: add `cbv` annotations to iterators and strings (#12961) This PR adds `cbv` annotations to some iterator and string operations. --------- Co-authored-by: Claude Opus 4.6 --- src/Init/Data/Array/Sort/Lemmas.lean | 1 + .../Data/Iterators/Combinators/Append.lean | 2 +- .../Data/Iterators/Combinators/Attach.lean | 2 +- .../Data/Iterators/Combinators/FilterMap.lean | 6 +- .../Data/Iterators/Combinators/FlatMap.lean | 2 +- src/Init/Data/Iterators/Combinators/Take.lean | 2 +- .../Data/Iterators/Combinators/ULift.lean | 2 +- .../Data/Iterators/Consumers/Collect.lean | 4 +- .../Iterators/Lemmas/Combinators/Append.lean | 4 +- .../Iterators/Lemmas/Combinators/Attach.lean | 4 +- .../Lemmas/Combinators/FilterMap.lean | 14 +- .../Iterators/Lemmas/Combinators/FlatMap.lean | 2 + .../Iterators/Lemmas/Combinators/Take.lean | 4 +- .../Iterators/Lemmas/Combinators/ULift.lean | 4 +- .../Iterators/Lemmas/Consumers/Collect.lean | 2 +- .../Data/Iterators/Lemmas/Consumers/Loop.lean | 2 +- .../Data/Iterators/Lemmas/Producers/List.lean | 4 +- src/Init/Data/Iterators/Producers/List.lean | 2 +- .../Iterators/Producers/Monadic/List.lean | 2 +- src/Init/Data/List/Basic.lean | 18 + src/Init/Data/List/Sublist.lean | 25 ++ src/Init/Data/Range/Polymorphic/Lemmas.lean | 21 ++ src/Init/Data/Slice/Array/Lemmas.lean | 3 +- src/Init/Data/String/Iterate.lean | 11 +- src/Init/Data/String/Lemmas/Iterate.lean | 15 +- src/Init/Data/String/Lemmas/Modify.lean | 8 + .../Data/String/Lemmas/Pattern/Find/Char.lean | 2 +- .../Data/String/Lemmas/Pattern/Find/Pred.lean | 2 +- .../String/Lemmas/Pattern/Find/String.lean | 8 + .../String/Lemmas/Pattern/Split/Basic.lean | 2 + .../String/Lemmas/Pattern/Split/Char.lean | 1 + .../String/Lemmas/Pattern/Split/Pred.lean | 21 ++ src/Init/Data/String/Slice.lean | 2 +- src/Init/WFExtrinsicFix.lean | 6 +- .../Data/DHashMap/AdditionalOperations.lean | 4 +- src/Std/Data/DHashMap/Basic.lean | 8 +- src/Std/Data/DHashMap/Lemmas.lean | 92 ++--- .../Data/HashMap/AdditionalOperations.lean | 4 +- src/Std/Data/HashMap/Basic.lean | 8 +- src/Std/Data/HashMap/Lemmas.lean | 88 +++-- src/Std/Data/HashSet/Basic.lean | 8 +- src/Std/Data/HashSet/Lemmas.lean | 14 +- src/Std/Data/Iterators/Combinators/Drop.lean | 2 +- .../Data/Iterators/Combinators/DropWhile.lean | 2 +- .../Data/Iterators/Combinators/TakeWhile.lean | 2 +- src/Std/Data/Iterators/Combinators/Zip.lean | 2 +- .../Iterators/Lemmas/Combinators/Drop.lean | 4 +- .../Lemmas/Combinators/DropWhile.lean | 4 +- .../Lemmas/Combinators/TakeWhile.lean | 4 +- .../Iterators/Lemmas/Combinators/Zip.lean | 4 +- .../Iterators/Lemmas/Producers/Array.lean | 4 +- src/Std/Data/Iterators/Producers/Array.lean | 4 +- tests/elab/cbv3.lean | 2 - tests/elab/cbv_classical.lean | 2 - tests/elab/cbv_eval_erase.lean | 15 +- tests/elab/cbv_eval_erase.lean.out.expected | 5 - tests/elab/cbv_hashmap_annotations.lean | 218 +++++++++++ tests/elab/cbv_iter.lean | 349 ++++++++++++++++++ tests/elab/cbv_opaque_guard.lean | 2 - tests/elab/cbv_opaque_inline.lean | 2 - tests/elab/cbv_string_split.lean | 29 ++ 61 files changed, 915 insertions(+), 177 deletions(-) delete mode 100644 tests/elab/cbv_eval_erase.lean.out.expected create mode 100644 tests/elab/cbv_hashmap_annotations.lean create mode 100644 tests/elab/cbv_iter.lean create mode 100644 tests/elab/cbv_string_split.lean diff --git a/src/Init/Data/Array/Sort/Lemmas.lean b/src/Init/Data/Array/Sort/Lemmas.lean index 956b28d4e4..6ce642e97b 100644 --- a/src/Init/Data/Array/Sort/Lemmas.lean +++ b/src/Init/Data/Array/Sort/Lemmas.lean @@ -134,6 +134,7 @@ theorem Array.toList_mergeSort {xs : Array α} {le : α → α → Bool} : (xs.mergeSort le).toList = xs.toList.mergeSort le := by rw [Array.mergeSort, Subarray.toList_mergeSort, Array.toList_mkSlice_rii] +@[cbv_eval] theorem Array.mergeSort_eq_toArray_mergeSort_toList {xs : Array α} {le : α → α → Bool} : xs.mergeSort le = (xs.toList.mergeSort le).toArray := by simp [← toList_mergeSort] diff --git a/src/Init/Data/Iterators/Combinators/Append.lean b/src/Init/Data/Iterators/Combinators/Append.lean index 6d918af239..3600477772 100644 --- a/src/Init/Data/Iterators/Combinators/Append.lean +++ b/src/Init/Data/Iterators/Combinators/Append.lean @@ -37,7 +37,7 @@ The standard library does not provide a `Productive` instance for this case. This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`. -/ -@[inline, expose] +@[cbv_opaque, inline, expose] def Iter.append {α₁ : Type w} {α₂ : Type w} {β : Type w} [Iterator α₁ Id β] [Iterator α₂ Id β] (it₁ : Iter (α := α₁) β) (it₂ : Iter (α := α₂) β) : diff --git a/src/Init/Data/Iterators/Combinators/Attach.lean b/src/Init/Data/Iterators/Combinators/Attach.lean index a39083fd13..e88677abda 100644 --- a/src/Init/Data/Iterators/Combinators/Attach.lean +++ b/src/Init/Data/Iterators/Combinators/Attach.lean @@ -13,7 +13,7 @@ public section namespace Std open Std.Iterators -@[always_inline, inline, expose, inherit_doc IterM.attachWith] +@[cbv_opaque, always_inline, inline, expose, inherit_doc IterM.attachWith] def Iter.attachWith {α β : Type w} [Iterator α Id β] (it : Iter (α := α) β) (P : β → Prop) (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) : diff --git a/src/Init/Data/Iterators/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Combinators/FilterMap.lean index 989a1cfd9f..46ea3b13a0 100644 --- a/src/Init/Data/Iterators/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Combinators/FilterMap.lean @@ -282,17 +282,17 @@ def Iter.mapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] [MonadAttach m] (f : β → m γ) (it : Iter (α := α) β) := (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.mapM f : IterM m γ) -@[always_inline, inline, inherit_doc IterM.filterMap, expose] +@[cbv_opaque, always_inline, inline, inherit_doc IterM.filterMap, expose] def Iter.filterMap {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] (f : β → Option γ) (it : Iter (α := α) β) := ((it.toIterM.filterMap f).toIter : Iter γ) -@[always_inline, inline, inherit_doc IterM.filter, expose] +@[cbv_opaque, always_inline, inline, inherit_doc IterM.filter, expose] def Iter.filter {α : Type w} {β : Type w} [Iterator α Id β] (f : β → Bool) (it : Iter (α := α) β) := ((it.toIterM.filter f).toIter : Iter β) -@[always_inline, inline, inherit_doc IterM.map, expose] +@[cbv_opaque, always_inline, inline, inherit_doc IterM.map, expose] def Iter.map {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] (f : β → γ) (it : Iter (α := α) β) := ((it.toIterM.map f).toIter : Iter γ) diff --git a/src/Init/Data/Iterators/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Combinators/FlatMap.lean index 51deaec245..5ef274d9d8 100644 --- a/src/Init/Data/Iterators/Combinators/FlatMap.lean +++ b/src/Init/Data/Iterators/Combinators/FlatMap.lean @@ -44,7 +44,7 @@ public def Iter.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w} (f : β → Iter (α := α₂) γ) (it₁ : Iter (α := α) β) (it₂ : Option (Iter (α := α₂) γ)) := ((it₁.toIterM.flatMapAfter (fun b => (f b).toIterM) (Iter.toIterM <$> it₂)).toIter : Iter γ) -@[always_inline, expose, inherit_doc IterM.flatMap] +@[cbv_opaque, always_inline, expose, inherit_doc IterM.flatMap] public def Iter.flatMap {α : Type w} {β : Type w} {α₂ : Type w} {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] (f : β → Iter (α := α₂) γ) (it : Iter (α := α) β) := diff --git a/src/Init/Data/Iterators/Combinators/Take.lean b/src/Init/Data/Iterators/Combinators/Take.lean index 29b37f0ed2..f28a0c2b9a 100644 --- a/src/Init/Data/Iterators/Combinators/Take.lean +++ b/src/Init/Data/Iterators/Combinators/Take.lean @@ -36,7 +36,7 @@ it.take 3 ---a--⊥ This combinator incurs an additional O(1) cost with each output of `it`. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.take {α : Type w} {β : Type w} [Iterator α Id β] (n : Nat) (it : Iter (α := α) β) : Iter (α := Take α Id) β := it.toIterM.take n |>.toIter diff --git a/src/Init/Data/Iterators/Combinators/ULift.lean b/src/Init/Data/Iterators/Combinators/ULift.lean index da337b21e3..34c115eaad 100644 --- a/src/Init/Data/Iterators/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/ULift.lean @@ -44,7 +44,7 @@ it.uLift n ---.up a----.up b---.up c--.up d---⊥ * `Finite`: only if the original iterator is finite * `Productive`: only if the original iterator is productive -/ -@[always_inline, inline, expose] +@[cbv_opaque, always_inline, inline, expose] def Iter.uLift (it : Iter (α := α) β) : Iter (α := Types.ULiftIterator.{v} α Id Id β (fun _ => monadLift)) (ULift β) := (it.toIterM.uLift Id).toIter diff --git a/src/Init/Data/Iterators/Consumers/Collect.lean b/src/Init/Data/Iterators/Consumers/Collect.lean index c1b1309908..cecd907a78 100644 --- a/src/Init/Data/Iterators/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Consumers/Collect.lean @@ -32,7 +32,7 @@ Traverses the given iterator and stores the emitted values in an array. If the iterator is not finite, this function might run forever. The variant `it.ensureTermination.toArray` always terminates after finitely many steps. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.toArray {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) : Array β := it.toIterM.toArray.run @@ -101,7 +101,7 @@ lists are prepend-only, `toListRev` is usually more efficient that `toList`. If the iterator is not finite, this function might run forever. The variant `it.ensureTermination.toList` always terminates after finitely many steps. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.toList {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) : List β := it.toIterM.toList.run diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean index e73fbdea5d..9a1b9e5362 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean @@ -56,7 +56,7 @@ theorem Iter.Intermediate.step_appendSnd {α₁ α₂ β : Type w} simp only [Iter.step, appendSnd, toIterM_toIter, IterM.Intermediate.step_appendSnd, Id.run_bind] cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp -@[simp] +@[cbv_eval, simp] theorem Iter.toList_append {α₁ α₂ β : Type w} [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : @@ -70,7 +70,7 @@ theorem Iter.toListRev_append {α₁ α₂ β : Type w} (it₁.append it₂).toListRev = it₂.toListRev ++ it₁.toListRev := by simp [append_eq_toIter_append_toIterM, toListRev_eq_toListRev_toIterM] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_append {α₁ α₂ β : Type w} [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean index 44c67fb79b..543836f971 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean @@ -34,7 +34,7 @@ theorem Iter.unattach_toList_attachWith [Iterator α Id β] ← Id.run_map (f := List.unattach), IterM.map_unattach_toList_attachWith, Iter.toList_eq_toList_toIterM] -@[simp] +@[cbv_eval, simp] theorem Iter.toList_attachWith [Iterator α Id β] {it : Iter (α := α) β} {hP} [Finite α Id] : @@ -68,7 +68,7 @@ theorem Iter.unattach_toArray_attachWith [Iterator α Id β] (it.attachWith P hP).toListRev.unattach = it.toListRev := by simp [toListRev_eq] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_attachWith [Iterator α Id β] {it : Iter (α := α) β} {hP} [Finite α Id] : diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean index 94cbac585b..2d486ce3a4 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean @@ -297,7 +297,7 @@ def Iter.val_step_filter {f : β → Bool} : · simp · simp -@[simp] +@[cbv_eval, simp] theorem Iter.toList_filterMap [Finite α Id] {f : β → Option γ} : (it.filterMap f).toList = it.toList.filterMap f := by @@ -315,12 +315,12 @@ theorem Iter.toList_mapM [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawful (it.mapM f).toList = it.toList.mapM f := by simp [Iter.mapM_eq_toIter_mapM_toIterM, IterM.toList_mapM, Iter.toList_eq_toList_toIterM] -@[simp] +@[cbv_eval, simp] theorem Iter.toList_map [Finite α Id] {f : β → γ} : (it.map f).toList = it.toList.map f := by simp [map_eq_toIter_map_toIterM, IterM.toList_map, Iter.toList_eq_toList_toIterM] -@[simp] +@[cbv_eval, simp] theorem Iter.toList_filter [Finite α Id] {f : β → Bool} : (it.filter f).toList = it.toList.filter f := by simp [filter_eq_toIter_filter_toIterM, IterM.toList_filter, Iter.toList_eq_toList_toIterM] @@ -369,7 +369,7 @@ theorem Iter.toListRev_filter [Finite α Id] (it.filter f).toListRev = it.toListRev.filter f := by simp [filter_eq_toIter_filter_toIterM, IterM.toListRev_filter, Iter.toListRev_eq_toListRev_toIterM] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_filterMap [Finite α Id] {f : β → Option γ} : (it.filterMap f).toArray = it.toArray.filterMap f := by @@ -387,13 +387,13 @@ theorem Iter.toArray_mapM [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfu (it.mapM f).toArray = it.toArray.mapM f := by simp [Iter.mapM_eq_toIter_mapM_toIterM, IterM.toArray_mapM, Iter.toArray_eq_toArray_toIterM] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_map [Finite α Id] {f : β → γ} : (it.map f).toArray = it.toArray.map f := by simp [map_eq_toIter_map_toIterM, IterM.toArray_map, Iter.toArray_eq_toArray_toIterM] -@[simp] -theorem Iter.toArray_filter[Finite α Id] {f : β → Bool} : +@[cbv_eval, simp] +theorem Iter.toArray_filter [Finite α Id] {f : β → Bool} : (it.filter f).toArray = it.toArray.filter f := by simp [filter_eq_toIter_filter_toIterM, IterM.toArray_filter, Iter.toArray_eq_toArray_toIterM] diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean index 50a6ab460e..85beae749f 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean @@ -254,6 +254,7 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α unfold Iter.toArray cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map] +@[cbv_eval] public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id] [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id] @@ -261,6 +262,7 @@ public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] (it₁.flatMap f).toList = (it₁.map fun b => (f b).toList).toList.flatten := by simp [flatMap, toList_flatMapAfter] +@[cbv_eval] public theorem Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id] [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id] diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean index 85fb8060c0..d2f9a602f7 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean @@ -67,7 +67,7 @@ theorem Iter.atIdxSlow?_take {α β} simp only [atIdxSlow?_eq_match (it := it.take k), step_take, h'] cases k <;> cases l <;> simp -@[simp] +@[cbv_eval, simp] theorem Iter.toList_take_of_finite {α β} [Iterator α Id β] {n : Nat} [Finite α Id] {it : Iter (α := α) β} : (it.take n).toList = it.toList.take n := by @@ -89,7 +89,7 @@ theorem Iter.toListRev_take_of_finite {α β} [Iterator α Id β] {n : Nat} (it.take n).toListRev = it.toListRev.drop (it.toList.length - n) := by rw [toListRev_eq, toList_take_of_finite, List.reverse_take, toListRev_eq] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_take_of_finite {α β} [Iterator α Id β] {n : Nat} [Finite α Id] {it : Iter (α := α) β} : (it.take n).toArray = it.toArray.take n := by diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean index b2f0969491..cbd1be95c5 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean @@ -38,7 +38,7 @@ theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} : PlausibleIterStep.done, pure_bind] cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp -@[simp] +@[cbv_eval, simp] theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β} [Finite α Id] : it.uLift.toList = it.toList.map ULift.up := by @@ -52,7 +52,7 @@ theorem Iter.toListRev_uLift [Iterator α Id β] {it : Iter (α := α) β} it.uLift.toListRev = it.toListRev.map ULift.up := by rw [toListRev_eq, toListRev_eq, toList_uLift, List.map_reverse] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β} [Finite α Id] : it.uLift.toArray = it.toArray.map ULift.up := by diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean index ca40328bec..a5ac30aa8c 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -88,7 +88,7 @@ theorem Iter.toList_toArray_ensureTermination {α β} [Iterator α Id β] [Finit it.ensureTermination.toArray.toList = it.toList := by simp -@[simp] +@[cbv_eval ←, simp] theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} : it.toList.toArray = it.toArray := by diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index fa9e077bff..43fe66f310 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -449,7 +449,7 @@ theorem Iter.toArray_eq_fold {α β : Type w} [Iterator α Id β] rw [← fold_hom (List.toArray)] simp -@[simp] +@[cbv_eval ←, simp] theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} : diff --git a/src/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean index 32a61c1306..cc01d62636 100644 --- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean +++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean @@ -33,12 +33,12 @@ theorem List.step_iter_cons {x : β} {xs : List β} : ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq] -@[simp, grind =] +@[cbv_eval, simp, grind =] theorem List.toArray_iter {l : List β} : l.iter.toArray = l.toArray := by simp [List.iter, List.toArray_iterM, Iter.toArray_eq_toArray_toIterM] -@[simp, grind =] +@[cbv_eval, simp, grind =] theorem List.toList_iter {l : List β} : l.iter.toList = l := by simp [List.iter, List.toList_iterM] diff --git a/src/Init/Data/Iterators/Producers/List.lean b/src/Init/Data/Iterators/Producers/List.lean index 23c6e3d8d9..9802918cd2 100644 --- a/src/Init/Data/Iterators/Producers/List.lean +++ b/src/Init/Data/Iterators/Producers/List.lean @@ -29,7 +29,7 @@ The monadic version of this iterator is `List.iterM`. * `Finite` instance: always * `Productive` instance: always -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def List.iter {α : Type w} (l : List α) : Iter (α := ListIterator α) α := ((l.iterM Id).toIter : Iter α) diff --git a/src/Init/Data/Iterators/Producers/Monadic/List.lean b/src/Init/Data/Iterators/Producers/Monadic/List.lean index 851db9b088..a0e9f34304 100644 --- a/src/Init/Data/Iterators/Producers/Monadic/List.lean +++ b/src/Init/Data/Iterators/Producers/Monadic/List.lean @@ -46,7 +46,7 @@ The non-monadic version of this iterator is `List.iter`. * `Finite` instance: always * `Productive` instance: always -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def _root_.List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] : IterM (α := ListIterator α) m α := ⟨{ list := l }⟩ diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index d4deb9493e..cd81857504 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -1246,6 +1246,24 @@ def IsInfix (l₁ : List α) (l₂ : List α) : Prop := Exists fun s => Exists f /-- not `isInfix` -/ recommended_spelling "infix" for "<:+:" in [IsInfix, «term_<:+:_»] +/-- +Checks whether the first list is a contiguous sub-list of the second. + +The relation `List.IsInfixOf` expresses this property with respect to logical equality. + +Examples: + * `[2, 3].isInfixOf_internal [1, 2, 3, 4] = true` + * `[2, 3].isInfixOf_internal [1, 3, 2, 4] = false` + * `[2, 3].isInfixOf_internal [2, 3] = true` + * `[2, 3].isInfixOf_internal [1] = false` + + Used internally by the `cbv` tactic. +-/ +def isInfixOf_internal [BEq α] (l₁ l₂ : List α) : Bool := + l₁.isPrefixOf l₂ || match l₂ with + | [] => false + | _ :: l₂ => isInfixOf_internal l₁ l₂ + /-! ### splitAt -/ /-- diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 0ed0f6f1bb..fd6e375153 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -1297,6 +1297,31 @@ instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂) := instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂) := decidable_of_iff (l₁.isSuffixOf l₂) isSuffixOf_iff_suffix +/- + Used internally by the `cbv` tactic. +-/ +theorem isInfixOf_internal_iff_isInfix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : + l₁.isInfixOf_internal l₂ ↔ l₁ <:+: l₂ := by + induction l₂ with + | nil => simp [isInfixOf_internal, IsInfix] + | cons a l₂ ih => + simp only [isInfixOf_internal, Bool.or_eq_true] + constructor + · rintro (h | h) + · exact (isPrefixOf_iff_prefix.mp h).isInfix + · exact infix_cons <| ih.mp h + · intro ⟨s, t, h⟩ + match s with + | [] => left; exact isPrefixOf_iff_prefix.mpr ⟨t, h⟩ + | a' :: s' => + right; exact ih.mpr ⟨s', t, List.cons.inj h |>.2⟩ + +/- + Used internally by the `cbv` tactic. +-/ +instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+: l₂) := + decidable_of_iff (l₁.isInfixOf_internal l₂) isInfixOf_internal_iff_isInfix + theorem prefix_iff_eq_append : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ := ⟨by rintro ⟨r, rfl⟩; rw [drop_left], fun e => ⟨_, e⟩⟩ diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index 7507236d0e..f2bc8e2321 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -411,6 +411,7 @@ private theorem Rii.Internal.toArray_eq_toArray_iter [Least? α] r.toArray = (Internal.iter r).toArray := by rfl +@[cbv_eval] public theorem Rxc.Iterator.toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] @@ -428,6 +429,7 @@ public theorem Rxc.Iterator.toList_eq_match [LE α] [DecidableLE α] · simp [*] · split <;> rename_i heq' <;> simp [*] +@[cbv_eval] public theorem Rxc.Iterator.toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] @@ -443,6 +445,7 @@ public theorem Rxc.Iterator.toArray_eq_match [LE α] [DecidableLE α] · rfl · split <;> simp +@[cbv_eval] public theorem Rxo.Iterator.toList_eq_match [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] @@ -459,6 +462,7 @@ public theorem Rxo.Iterator.toList_eq_match [LT α] [DecidableLT α] · simp [*] · split <;> rename_i heq' <;> simp [*] +@[cbv_eval] public theorem Rxo.Iterator.toArray_eq_match [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] @@ -491,6 +495,7 @@ public theorem Rxc.Iterator.toList_eq_toList_rxoIterator [LE α] [DecidableLE α · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h +@[cbv_eval] public theorem Rxi.Iterator.toList_eq_match [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {it : Iter (α := Rxi.Iterator α) α} : @@ -502,6 +507,7 @@ public theorem Rxi.Iterator.toList_eq_match simp only [Iter.toList_eq_match_step (it := it), Rxi.Iterator.step_eq_step, Rxi.Iterator.step] split <;> rename_i heq <;> simp [*] +@[cbv_eval] public theorem Rxi.Iterator.toArray_eq_match [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {it : Iter (α := Rxi.Iterator α) α} : @@ -608,6 +614,7 @@ namespace Rcc variable {r : Rcc α} +@[cbv_eval] public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = if r.lower ≤ r.upper then @@ -755,6 +762,7 @@ public theorem ClosedOpen.toList_succ_succ_eq_map [LE α] [DecidableLE α] [Upwa (lo...=hi).toList.map succ := Rcc.toList_succ_succ_eq_map +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] @@ -844,6 +852,7 @@ namespace Rco variable {r : Rco α} +@[cbv_eval] public theorem toList_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : r.toList = if r.lower < r.upper then @@ -1011,6 +1020,7 @@ public theorem toArray_succ_succ_eq_map [LE α] [DecidableLE α] [LT α] [Decida (lo...hi).toArray.map succ := by simp [← toArray_toList, toList_succ_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -1224,6 +1234,7 @@ public theorem toArray_succ_succ_eq_map [LE α] [DecidableLE α] ((succ lo)...*).toArray = (lo...*).toArray.map succ := by simp [← toArray_toList, toList_succ_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -1330,6 +1341,7 @@ public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match (it := Internal.iter r)] simp [Internal.iter, Internal.toArray_eq_toArray_iter] +@[cbv_eval] public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = match UpwardEnumerable.succ? r.lower with @@ -1473,6 +1485,7 @@ public theorem toArray_succ_succ_eq_map [LE α] [DecidableLE α] [LT α] [Decida (lo<...=hi).toArray.map succ := by simp [← toArray_toList, toList_succ_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} @@ -1572,6 +1585,7 @@ public theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerab #[] := by rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl +@[cbv_eval] public theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toList = match UpwardEnumerable.succ? r.lower with @@ -1705,6 +1719,7 @@ public theorem toArray_succ_succ_eq_map [LT α] [DecidableLT α] (lo<...hi).toArray.map succ := by simp [← toArray_toList, toList_succ_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -1939,6 +1954,7 @@ public theorem toArray_succ_succ_eq_map [LT α] [DecidableLT α] ((succ lo)<...*).toArray = (lo<...*).toArray.map succ := by simp [← toArray_toList, toList_succ_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -2039,6 +2055,7 @@ public theorem toList_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumer r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] +@[cbv_eval] public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : @@ -2231,6 +2248,7 @@ public theorem toArray_succ_eq_map [LE α] [DecidableLE α] [Least? α] #[UpwardEnumerable.least (hn := ⟨r.upper⟩)] ++ (*...=hi).toArray.map succ := by simp [← toArray_toList, toList_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} @@ -2340,6 +2358,7 @@ public theorem toList_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumer r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] +@[cbv_eval] public theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : @@ -2550,6 +2569,7 @@ public theorem toArray_succ_eq_map [LT α] [DecidableLT α] [Least? α] #[UpwardEnumerable.least (hn := ⟨r.upper⟩)] ++ (*...hi).toArray.map succ := by simp [← toArray_toList, toList_succ_eq_map] +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} @@ -2788,6 +2808,7 @@ public theorem pairwise_toList_le [LE α] [Least? α] |> List.Pairwise.imp UpwardEnumerable.le_of_lt |> List.Pairwise.imp (fun hle => (UpwardEnumerable.le_iff ..).mpr hle) +@[cbv_eval] public theorem forIn'_eq_forIn'_toList [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 7497049302..5cc4c2174c 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -126,7 +126,7 @@ public theorem forIn_toList {α : Type u} {s : Subarray α} ForIn.forIn s.toList init f = ForIn.forIn s init f := Slice.forIn_toList -@[grind =] +@[cbv_eval, grind =] public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : @@ -243,6 +243,7 @@ private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start sto List.length_take, ge_iff_le, h₁] omega +@[cbv_eval] public theorem Subarray.toList_eq_drop_take {xs : Subarray α} : xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take'] diff --git a/src/Init/Data/String/Iterate.lean b/src/Init/Data/String/Iterate.lean index 27157f8e03..9d0a7f6df5 100644 --- a/src/Init/Data/String/Iterate.lean +++ b/src/Init/Data/String/Iterate.lean @@ -27,6 +27,7 @@ deriving Inhabited /-- Creates an iterator over the valid positions within {name}`s`, starting at {name}`p`. -/ +@[cbv_opaque] def positionsFrom {s : Slice} (p : s.Pos) : Std.Iter (α := PosIterator s) { p : s.Pos // p ≠ s.endPos } := { internalState := { currPos := p } } @@ -99,7 +100,7 @@ Examples: * {lean}`"abc".toSlice.chars.toList = ['a', 'b', 'c']` * {lean}`"ab∀c".toSlice.chars.toList = ['a', 'b', '∀', 'c']` -/ -@[expose, inline] +@[cbv_opaque, expose, inline] def chars (s : Slice) := Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (positions s) @@ -188,7 +189,7 @@ Example: * {lean}`"abc".toSlice.revChars.toList = ['c', 'b', 'a']` * {lean}`"ab∀c".toSlice.revChars.toList = ['c', '∀', 'b', 'a']` -/ -@[expose, inline] +@[cbv_opaque, expose, inline] def revChars (s : Slice) := Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (revPositions s) @@ -347,7 +348,7 @@ Examples: * {lean}`"coffee tea and water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3` * {lean}`"coffee tea water".toSlice.foldl (·.push ·) "" = "coffee tea water"` -/ -@[inline] +@[cbv_opaque, inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Slice) : α := Std.Iter.fold f init (chars s) @@ -398,7 +399,7 @@ Examples: * {lean}`"abc".chars.toList = ['a', 'b', 'c']` * {lean}`"ab∀c".chars.toList = ['a', 'b', '∀', 'c']` -/ -@[inline] +@[cbv_opaque, inline] def chars (s : String) := (s.toSlice.chars : Std.Iter Char) @@ -432,7 +433,7 @@ Example: * {lean}`"abc".revChars.toList = ['c', 'b', 'a']` * {lean}`"ab∀c".revChars.toList = ['c', '∀', 'b', 'a']` -/ -@[inline] +@[cbv_opaque, inline] def revChars (s : String) := (s.toSlice.revChars : Std.Iter Char) diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean index 51fca51f4b..d436445458 100644 --- a/src/Init/Data/String/Lemmas/Iterate.lean +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -76,7 +76,7 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} : (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList := Model.map_get_positionsFrom_of_splits (splits_startPos s) -@[simp] +@[cbv_eval, simp] theorem toList_positionsFrom {s : Slice} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p := by rw [positionsFrom] @@ -91,7 +91,7 @@ theorem toList_positionsFrom {s : Slice} {p : s.Pos} : theorem toList_positions {s : Slice} : s.positions.toList = Model.positionsFrom s.startPos := by simp [positions] -@[simp] +@[cbv_eval, simp] theorem toList_chars {s : Slice} : s.chars.toList = s.copy.toList := by simp [chars, Model.map_get_positionsFrom_startPos] @@ -177,20 +177,20 @@ theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} : theorem toList_revPositions {s : Slice} : s.revPositions.toList = Model.revPositionsFrom s.endPos := by simp [revPositions] -@[simp] +@[cbv_eval, simp] theorem toList_revChars {s : Slice} : s.revChars.toList = s.copy.toList.reverse := by simp [revChars, Model.map_get_revPositionsFrom_endPos] theorem forIn_eq_forIn_chars {m : Type u → Type v} [Monad m] {s : Slice} {b} {f : Char → β → m (ForInStep β)} : ForIn.forIn s b f = ForIn.forIn s.chars b f := rfl -@[simp] +@[cbv_eval, simp] theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : Slice} {b} {f : Char → β → m (ForInStep β)} : ForIn.forIn s b f = ForIn.forIn s.copy.toList b f := by rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars] -@[simp] +@[cbv_eval, simp] theorem foldl_eq_foldl_toList {α : Type u} {f : α → Char → α} {init : α} {s : Slice} : s.foldl f init = s.copy.toList.foldl f init := by rw [foldl, ← Std.Iter.foldl_toList, toList_chars] @@ -262,10 +262,11 @@ theorem toList_positionsFrom {s : String} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p := by simp [positionsFrom, Internal.ofToSliceWithProof, Model.positionsFrom_eq_map] +@[cbv_eval] theorem toList_positions {s : String} : s.positions.toList = Model.positionsFrom s.startPos := by simp [positions] -@[simp] +@[cbv_eval, simp] theorem toList_chars {s : String} : s.chars.toList = s.toList := by simp [chars] @@ -353,7 +354,7 @@ theorem toList_revPositions {s : String} : s.revPositions.toList = Model.revPositionsFrom s.endPos := by simp [revPositions] -@[simp] +@[cbv_eval, simp] theorem toList_revChars {s : String} : s.revChars.toList = s.toList.reverse := by simp [revChars] diff --git a/src/Init/Data/String/Lemmas/Modify.lean b/src/Init/Data/String/Lemmas/Modify.lean index 028d57b0ac..5818a191d4 100644 --- a/src/Init/Data/String/Lemmas/Modify.lean +++ b/src/Init/Data/String/Lemmas/Modify.lean @@ -49,6 +49,14 @@ theorem toList_mapAux {f : Char → Char} {s : String} {p : s.Pos} theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by simp [map, toList_mapAux s.splits_startPos] +/- + Used internally by the `cbv` tactic. +-/ +@[cbv_eval] +theorem map_eq_internal {f : Char → Char} {s : String} : s.map f = .ofList (s.toList.map f) := by + apply String.toList_injective + simp only [toList_map, toList_ofList] + @[simp] theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by simp [← length_toList] diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean index c32d3e1a01..fb55bb6f4f 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean @@ -183,7 +183,7 @@ theorem find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} : · rintro ⟨t, u, hsplit, hnotin⟩ exact ⟨pos.toSlice, ⟨t, u, Pos.splits_toSlice_iff.mpr hsplit, hnotin⟩, by simp⟩ -@[simp] +@[cbv_eval, simp] theorem contains_char_eq {c : Char} {s : String} : s.contains c = decide (c ∈ s.toList) := by simp [contains_eq_contains_toSlice, Slice.contains_char_eq, copy_toSlice] diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean index f9ac4bb832..40c3009bec 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean @@ -58,7 +58,7 @@ theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff_splits, decide_eq_true_eq, decide_eq_false_iff_not] -@[simp] +@[cbv_eval, simp] theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy.toList.any p := by rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff] simp only [Pattern.Model.CharPred.matchesAt_iff, ne_eq, List.any_eq_true, diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/String.lean b/src/Init/Data/String/Lemmas/Pattern/Find/String.lean index b966ffed15..268259e688 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Find/String.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Find/String.lean @@ -90,4 +90,12 @@ theorem contains_string_eq_false_iff {t s : String} : s.contains t = false ↔ ¬(t.toList <:+: s.toList) := Bool.eq_false_iff.trans (not_congr contains_string_iff) +/- + Used internally by the `cbv` tactic. +-/ +@[cbv_eval] +theorem contains_string_eq_internal {t s : String} : + s.contains t = t.toList.isInfixOf_internal s.toList := by + rw [Bool.eq_iff_iff, contains_string_iff, List.isInfixOf_internal_iff_isInfix] + end String diff --git a/src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean index adaf31c970..b6a585449b 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean @@ -35,6 +35,7 @@ This gives a low-level correctness proof from which higher-level API lemmas can namespace String.Slice.Pattern.Model +@[cbv_opaque] public protected noncomputable def split {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {s : Slice} (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr) : List s.Subslice := if h : curr = s.endPos then @@ -153,6 +154,7 @@ end Model open Model +@[cbv_eval] public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type} [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)] [∀ s, Std.Iterators.Finite (σ s) Id] [LawfulToForwardSearcherModel pat] (s : Slice) : diff --git a/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean index 3e6da1cafb..5c8735bb65 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean @@ -30,6 +30,7 @@ namespace String.Slice open Pattern.Model Pattern.Model.Char +@[cbv_eval] theorem Pattern.Model.split_char_eq_split_beq {c : Char} {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) : Model.split c f curr hle = Model.split (· == c) f curr hle := by diff --git a/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean index da26eb0099..85148465f9 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean @@ -58,12 +58,33 @@ theorem toList_split_bool {s : Slice} {p : Char → Bool} : (s.split p).toList.map Slice.copy = (s.copy.toList.splitOnP p).map String.ofList := by simp [toList_split_eq_splitToSubslice, ← toList_splitToSubslice_bool] +/- + Used internally by the `cbv` tactic. +-/ +@[cbv_eval] +theorem Pattern.Model.split_bool_eq_internal {p : Char → Bool} {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) : + Model.split p f curr hle = + if h : curr = s.endPos then [s.subslice _ _ hle] + else if p (curr.get h) then + s.subslice _ _ hle :: Model.split p (curr.next h) (curr.next h) (by simp [Std.le_refl]) + else Model.split p f (curr.next h) (by simp [Std.le_trans hle _]) := by + by_cases h : curr = s.endPos + · simp only [h, split_endPos, subslice_endPos, ↓reduceDIte] + · simp only [h, ↓reduceDIte] + by_cases hp : p (curr.get h) + · simp only [hp, ↓reduceIte] + exact split_eq_of_isLongestMatchAt (isLongestMatchAt_of_get hp) + · rw [Bool.not_eq_true] at hp + simp only [hp, Bool.false_eq_true, ↓reduceIte] + exact split_eq_next_of_not_matchesAt h (not_matchesAt_of_get hp) + end section open Pattern.Model Pattern.Model.CharPred.Decidable +@[cbv_eval] theorem Pattern.Model.split_eq_split_decide {p : Char → Prop} [DecidablePred p] {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) : Model.split p f curr hle = Model.split (decide <| p ·) f curr hle := by diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index 4cdbaa9880..087f5f765f 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -213,7 +213,7 @@ Examples: * {lean}`("ababababa".toSlice.splitToSubslice "aba").toStringList == ["coffee", "water"]` * {lean}`("baaab".toSlice.splitToSubslice "aa").toStringList == ["b", "ab"]` -/ -@[specialize pat] +@[specialize pat, cbv_opaque] def splitToSubslice (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] : Std.Iter (α := SplitIterator pat s) s.Subslice := { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) } diff --git a/src/Init/WFExtrinsicFix.lean b/src/Init/WFExtrinsicFix.lean index f9767eba7e..5459c98e78 100644 --- a/src/Init/WFExtrinsicFix.lean +++ b/src/Init/WFExtrinsicFix.lean @@ -63,7 +63,7 @@ nothing interesting can be proved about the recursive function; it is opaque. If {name}`R` _is_ well-founded, {lean}`extrinsicFix R F` is equivalent to {lean}`WellFounded.fix _ F`, logically and regarding its termination behavior. -/ -@[implemented_by opaqueFix] +@[cbv_opaque, implemented_by opaqueFix] public def extrinsicFix [∀ a, Nonempty (C a)] (R : α → α → Prop) (F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a := open scoped Classical in @@ -150,7 +150,7 @@ nothing interesting can be proved about the recursive function; it is opaque. If {name}`R` _is_ well-founded, {lean}`extrinsicFix₂ R F` is equivalent to a well-founded recursive function, logically and regarding its termination behavior. -/ -@[implemented_by opaqueFix₂] +@[cbv_opaque, implemented_by opaqueFix₂] public def extrinsicFix₂ [∀ a b, Nonempty (C₂ a b)] (R : (a : α) ×' β a → (a : α) ×' β a → Prop) (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) @@ -222,7 +222,7 @@ nothing interesting can be proved about the recursive function; it is opaque. If {name}`R` _is_ well-founded, {lean}`extrinsicFix₃ R F` is equivalent to a well-founded recursive function, logically and regarding its termination behavior. -/ -@[implemented_by opaqueFix₃] +@[cbv_opaque, implemented_by opaqueFix₃] public def extrinsicFix₃ [∀ a b c, Nonempty (C₃ a b c)] (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop) (F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c) diff --git a/src/Std/Data/DHashMap/AdditionalOperations.lean b/src/Std/Data/DHashMap/AdditionalOperations.lean index 28eb563cc1..d8e4115292 100644 --- a/src/Std/Data/DHashMap/AdditionalOperations.lean +++ b/src/Std/Data/DHashMap/AdditionalOperations.lean @@ -43,11 +43,11 @@ theorem WF.map [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) end Raw -@[inline, inherit_doc Raw.filterMap] def filterMap [BEq α] [Hashable α] +@[cbv_opaque, inline, inherit_doc Raw.filterMap] def filterMap [BEq α] [Hashable α] (f : (a : α) → β a → Option (δ a)) (m : DHashMap α β) : DHashMap α δ := ⟨Raw₀.filterMap f ⟨m.1, m.2.size_buckets_pos⟩, Raw₀.wf_filterMap₀ m.2⟩ -@[inline, inherit_doc Raw.map] def map [BEq α] [Hashable α] (f : (a : α) → β a → δ a) +@[cbv_opaque, inline, inherit_doc Raw.map] def map [BEq α] [Hashable α] (f : (a : α) → β a → δ a) (m : DHashMap α β) : DHashMap α δ := ⟨Raw₀.map f ⟨m.1, m.2.size_buckets_pos⟩, Raw₀.wf_map₀ m.2⟩ diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index a96418fada..82630a31fe 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -74,7 +74,7 @@ structure DHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] whe namespace DHashMap -@[inline, inherit_doc Raw.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : DHashMap α β := +@[cbv_opaque, inline, inherit_doc Raw.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : DHashMap α β := ⟨Raw.emptyWithCapacity capacity, .emptyWithCapacity₀⟩ instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where @@ -90,7 +90,7 @@ structure Equiv (m₁ m₂ : DHashMap α β) where @[inherit_doc] scoped infixl:50 " ~m " => Equiv -@[inline, inherit_doc Raw.insert] def insert (m : DHashMap α β) (a : α) +@[cbv_opaque, inline, inherit_doc Raw.insert] def insert (m : DHashMap α β) (a : α) (b : β a) : DHashMap α β := ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩ @@ -146,7 +146,7 @@ instance [BEq α] [Hashable α] {m : DHashMap α β} {a : α} : Decidable (a ∈ (a : α) (fallback : β a) : β a := Raw₀.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback -@[inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) : +@[cbv_opaque, inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) : DHashMap α β := ⟨Raw₀.erase ⟨m.1, m.2.size_buckets_pos⟩ a, .erase₀ m.2⟩ @@ -261,7 +261,7 @@ define the `ForM` and `ForIn` instances for `HashMap`. end Const -@[inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool) +@[cbv_opaque, inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool) (m : DHashMap α β) : DHashMap α β := ⟨Raw₀.filter f ⟨m.1, m.2.size_buckets_pos⟩, .filter₀ m.2⟩ diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 77eb65ed83..76e19906de 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -76,7 +76,7 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := by simp [← contains_iff_mem, contains_congr hab] -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).contains a = false := Raw₀.contains_emptyWithCapacity @@ -119,7 +119,7 @@ theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] : Singleton.singleton p = (∅ : DHashMap α β).insert p.1 p.2 := rfl -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} : (m.insert k v).contains a = (k == a || m.contains a) := Raw₀.contains_insert ⟨m.1, _⟩ m.2 @@ -197,7 +197,7 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : (m.insert k v).size ≤ m.size + 1 := Raw₀.size_insert_le ⟨m.1, _⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : DHashMap α β).erase k = emptyWithCapacity c := ext <| congrArg Subtype.val (Raw₀.erase_emptyWithCapacity (k := k)) @@ -210,7 +210,7 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) := Raw₀.isEmpty_erase _ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = (!(k == a) && m.contains a) := Raw₀.contains_erase ⟨m.1, _⟩ m.2 @@ -256,7 +256,7 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β k} : (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v := ext <| congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _ (k := k)) -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : DHashMap α β).get? a = none := Raw₀.get?_emptyWithCapacity @@ -267,7 +267,7 @@ theorem get?_empty [LawfulBEq α] {a : α} : (∅ : DHashMap α β).get? a = non theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a = none := Raw₀.get?_of_isEmpty ⟨m.1, _⟩ m.2 -@[grind =] theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a = +@[grind =, cbv_eval] theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a = if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := Raw₀.get?_insert ⟨m.1, _⟩ m.2 @@ -300,7 +300,7 @@ theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} : theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := by simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false -@[grind =] theorem get?_erase [LawfulBEq α] {k a : α} : +@[grind =, cbv_eval] theorem get?_erase [LawfulBEq α] {k a : α} : (m.erase k).get? a = if k == a then none else m.get? a := Raw₀.get?_erase ⟨m.1, _⟩ m.2 @@ -312,7 +312,7 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_emptyWithCapacity {a : α} {c} : get? (emptyWithCapacity c : DHashMap α (fun _ => β)) a = none := Raw₀.Const.get?_emptyWithCapacity @@ -324,7 +324,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → get? m a = none := Raw₀.Const.get?_of_isEmpty ⟨m.1, _⟩ m.2 -@[grind =] theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : +@[grind =, cbv_eval] theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : get? (m.insert k v) a = if k == a then some v else get? m a := Raw₀.Const.get?_insert ⟨m.1, _⟩ m.2 @@ -360,7 +360,7 @@ theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → get? m a = none := by simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false -@[grind =] theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : +@[grind =, cbv_eval] theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : Const.get? (m.erase k) a = if k == a then none else get? m a := Raw₀.Const.get?_erase ⟨m.1, _⟩ m.2 @@ -457,7 +457,7 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h end Const -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get!_emptyWithCapacity [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : (emptyWithCapacity c : DHashMap α β).get! a = default := Raw₀.get!_emptyWithCapacity @@ -471,7 +471,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] : m.isEmpty = true → m.get! a = default := Raw₀.get!_of_isEmpty ⟨m.1, _⟩ m.2 -@[grind =] theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} : +@[grind =, cbv_eval] theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} : (m.insert k v).get! a = if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := Raw₀.get!_insert ⟨m.1, _⟩ m.2 @@ -489,7 +489,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] : ¬a ∈ m → m.get! a = default := by simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false -@[grind =] theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] : +@[grind =, cbv_eval] theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] : (m.erase k).get! a = if k == a then default else m.get! a := Raw₀.get!_erase ⟨m.1, _⟩ m.2 @@ -518,7 +518,7 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} : get! (emptyWithCapacity c : DHashMap α (fun _ => β)) a = default := Raw₀.Const.get!_emptyWithCapacity @@ -531,7 +531,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α m.isEmpty = true → get! m a = default := Raw₀.Const.get!_of_isEmpty ⟨m.1, _⟩ m.2 -@[grind =] theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : +@[grind =, cbv_eval] theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : get! (m.insert k v) a = if k == a then v else get! m a := Raw₀.Const.get!_insert ⟨m.1, _⟩ m.2 @@ -548,7 +548,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α ¬a ∈ m → get! m a = default := by simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false -@[grind =] theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : +@[grind =, cbv_eval] theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : get! (m.erase k) a = if k == a then default else get! m a := Raw₀.Const.get!_erase ⟨m.1, _⟩ m.2 @@ -583,7 +583,7 @@ theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} ( end Const -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getD_emptyWithCapacity [LawfulBEq α] {a : α} {fallback : β a} {c} : (emptyWithCapacity c : DHashMap α β).getD a fallback = fallback := Raw₀.getD_emptyWithCapacity @@ -597,7 +597,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} : m.isEmpty = true → m.getD a fallback = fallback := Raw₀.getD_of_isEmpty ⟨m.1, _⟩ m.2 -@[grind =] theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} : +@[grind =, cbv_eval] theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} : (m.insert k v).getD a fallback = if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := Raw₀.getD_insert ⟨m.1, _⟩ m.2 @@ -615,7 +615,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} : ¬a ∈ m → m.getD a fallback = fallback := by simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false -@[grind =] theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} : +@[grind =, cbv_eval] theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} : (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := Raw₀.getD_erase ⟨m.1, _⟩ m.2 @@ -648,7 +648,7 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : getD (emptyWithCapacity c : DHashMap α (fun _ => β)) a fallback = fallback := Raw₀.Const.getD_emptyWithCapacity @@ -662,7 +662,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : m.isEmpty = true → getD m a fallback = fallback := Raw₀.Const.getD_of_isEmpty ⟨m.1, _⟩ m.2 -@[grind =] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : +@[grind =, cbv_eval] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := Raw₀.Const.getD_insert ⟨m.1, _⟩ m.2 @@ -679,7 +679,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : ¬a ∈ m → getD m a fallback = fallback := by simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false -@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : +@[grind =, cbv_eval] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := Raw₀.Const.getD_erase ⟨m.1, _⟩ m.2 @@ -4654,7 +4654,7 @@ theorem isEmpty_filterMap_eq_false_iff [LawfulBEq α] ∃ (k : α) (h : k ∈ m), (f k (m.get k h)).isSome := Raw₀.isEmpty_filterMap_eq_false_iff ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem contains_filterMap [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} : (m.filterMap f).contains k = (m.get? k).any (f k · |>.isSome) := @@ -4689,7 +4689,7 @@ theorem size_filterMap_eq_size_iff [LawfulBEq α] (m.filterMap f).size = m.size ↔ ∀ (a : α) (h : a ∈ m), (f a (m.get a h)).isSome := Raw₀.size_filterMap_eq_size_iff ⟨m.1, _⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_filterMap [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} : (m.filterMap f).get? k = (m.get? k).bind (f k) := @@ -4709,13 +4709,13 @@ theorem get_filterMap [LawfulBEq α] (isSome_apply_of_mem_filterMap h') := Raw₀.get_filterMap ⟨m.1, _⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get!_filterMap [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} [Inhabited (γ k)] : (m.filterMap f).get! k = ((m.get? k).bind (f k)).get! := Raw₀.get!_filterMap ⟨m.1, _⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getD_filterMap [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} : (m.filterMap f).getD k fallback = ((m.get? k).bind (f k)).getD fallback := @@ -4789,7 +4789,7 @@ theorem get?_filterMap [EquivBEq α] [LawfulHashable α] Raw₀.Const.get?_filterMap ⟨m.1, _⟩ m.2 /-- Simpler variant of `get?_filterMap` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem get?_filterMap' [LawfulBEq α] {f : α → β → Option γ} {k : α} : Const.get? (m.filterMap f) k = (Const.get? m k).bind fun x => f k x := by @@ -4832,10 +4832,10 @@ theorem get!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited γ] Raw₀.Const.get!_filterMap ⟨m.1, _⟩ m.2 /-- Simpler variant of `get!_filterMap` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem get!_filterMap' [LawfulBEq α] [Inhabited γ] {f : α → β → Option γ} {k : α} : - Const.get! (m.filterMap f) k = ((Const.get? m k).bind (f k) ).get!:= by + Const.get! (m.filterMap f) k = ((Const.get? m k).bind (f k)).get! := by simp [get!_filterMap] theorem get!_filterMap_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhabited γ] @@ -4851,7 +4851,7 @@ theorem getD_filterMap [EquivBEq α] [LawfulHashable α] Raw₀.Const.getD_filterMap ⟨m.1, _⟩ m.2 /-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getD_filterMap' [LawfulBEq α] {f : α → β → Option γ} {k : α} {fallback : γ} : Const.getD (m.filterMap f) k fallback = ((Const.get? m k).bind (f k)).getD fallback := by @@ -4935,7 +4935,7 @@ theorem isEmpty_filter_key_eq_false_iff [EquivBEq α] [LawfulHashable α] ∃ (k : α) (h : k ∈ m), f (m.getKey k h) := Raw₀.isEmpty_filter_key_eq_false_iff ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem contains_filter [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} : (m.filter f).contains k = (m.get? k).any (f k) := @@ -4992,7 +4992,7 @@ theorem size_filter_key_eq_size_iff [EquivBEq α] [LawfulHashable α] (m.filter fun k _ => f k).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) := Raw₀.size_filter_key_eq_size_iff ⟨m.1, _⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_filter [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} : (m.filter f).get? k = (m.get? k).filter (f k) := @@ -5004,13 +5004,13 @@ theorem get_filter [LawfulBEq α] (m.filter f).get k h' = m.get k (mem_of_mem_filter h') := Raw₀.get_filter ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem get!_filter [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} [Inhabited (β k)] : (m.filter f).get! k = ((m.get? k).filter (f k)).get! := Raw₀.get!_filter ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem getD_filter [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k} : (m.filter f).getD k fallback = ((m.get? k).filter (f k)).getD fallback := @@ -5118,7 +5118,7 @@ theorem get?_filter [EquivBEq α] [LawfulHashable α] Raw₀.Const.get?_filter ⟨m.1, _⟩ m.2 /-- Simpler variant of `get?_filter` when `LawfulBEq` is available. -/ -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_filter' [LawfulBEq α] {f : α → β → Bool} {k : α} : Const.get? (m.filter f) k = (Const.get? m k).filter (f k) := by @@ -5144,7 +5144,7 @@ theorem get!_filter [EquivBEq α] [LawfulHashable α] [Inhabited β] Raw₀.Const.get!_filter ⟨m.1, _⟩ m.2 /-- Simpler variant of `get!_filter` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem get!_filter' [LawfulBEq α] [Inhabited β] {f : α → β → Bool} {k : α} : Const.get! (m.filter f) k = ((Const.get? m k).filter (f k)).get! := by @@ -5163,7 +5163,7 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α] Raw₀.Const.getD_filter ⟨m.1, _⟩ m.2 /-- Simpler variant of `getD_filter` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getD_filter' [LawfulBEq α] {f : α → β → Bool} {k : α} {fallback : β} : Const.getD (m.filter f) k fallback = ((Const.get? m k).filter (f k)).getD fallback := by @@ -5237,13 +5237,13 @@ theorem filterMap_equiv_map [EquivBEq α] [LawfulHashable α] (m.filterMap (fun k v => some (f k v))) ~m m.map f := ⟨Raw₀.filterMap_equiv_map ⟨m.1, m.2.size_buckets_pos⟩ m.2⟩ -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem isEmpty_map [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} : (m.map f).isEmpty = m.isEmpty := Raw₀.isEmpty_map ⟨m.1, m.2.size_buckets_pos⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem contains_map [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} : (m.map f).contains k = m.contains k := @@ -5265,13 +5265,13 @@ theorem mem_of_mem_map [EquivBEq α] [LawfulHashable α] k ∈ m.map f → k ∈ m := Raw₀.contains_of_contains_map ⟨m.1, _⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem size_map [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} : (m.map f).size = m.size := Raw₀.size_map ⟨m.1, m.2.size_buckets_pos⟩ m.2 -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_map [LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} : (m.map f).get? k = (m.get? k).map (f k) := @@ -5283,13 +5283,13 @@ theorem get_map [LawfulBEq α] (m.map f).get k h' = f k (m.get k (mem_of_mem_map h')) := Raw₀.get_map ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem get!_map [LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} [Inhabited (γ k)] : (m.map f).get! k = ((m.get? k).map (f k)).get! := Raw₀.get!_map ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem getD_map [LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k} : (m.map f).getD k fallback = ((m.get? k).map (f k)).getD fallback := @@ -5323,7 +5323,7 @@ namespace Const variable {β : Type v} {γ : Type w} {m : DHashMap α fun _ => β} -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem get?_map [LawfulBEq α] {f : α → β → γ} {k : α} : Const.get? (m.map f) k = (Const.get? m k).map (f k) := @@ -5356,7 +5356,7 @@ theorem get_map' [EquivBEq α] [LawfulHashable α] f (m.getKey k (mem_of_mem_map h')) (Const.get m k (mem_of_mem_map h')) := Raw₀.Const.get_map' ⟨m.1, _⟩ m.2 -@[grind =] +@[grind =, cbv_eval] theorem get!_map [LawfulBEq α] [Inhabited γ] {f : α → β → γ} {k : α} : Const.get! (m.map f) k = ((Const.get? m k).map (f k)).get! := @@ -5375,7 +5375,7 @@ theorem get!_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhabited Const.get! (m.map f) k = ((Const.get? m k).map (f k')).get! := Raw₀.Const.get!_map_of_getKey?_eq_some ⟨m.1, _⟩ m.2 h -@[grind =] +@[grind =, cbv_eval] theorem getD_map [LawfulBEq α] {f : α → β → γ} {k : α} {fallback : γ} : Const.getD (m.map f) k fallback = ((Const.get? m k).map (f k)).getD fallback := diff --git a/src/Std/Data/HashMap/AdditionalOperations.lean b/src/Std/Data/HashMap/AdditionalOperations.lean index eb52bfb86d..d4462ae837 100644 --- a/src/Std/Data/HashMap/AdditionalOperations.lean +++ b/src/Std/Data/HashMap/AdditionalOperations.lean @@ -41,11 +41,11 @@ theorem WF.map [BEq α] [Hashable α] {m : Raw α β} {f : α → β → γ} (h end Raw -@[inline, inherit_doc DHashMap.filterMap] def filterMap [BEq α] [Hashable α] (f : α → β → Option γ) +@[cbv_opaque, inline, inherit_doc DHashMap.filterMap] def filterMap [BEq α] [Hashable α] (f : α → β → Option γ) (m : HashMap α β) : HashMap α γ := ⟨m.inner.filterMap f⟩ -@[inline, inherit_doc DHashMap.map] def map [BEq α] [Hashable α] (f : α → β → γ) (m : HashMap α β) : +@[cbv_opaque, inline, inherit_doc DHashMap.map] def map [BEq α] [Hashable α] (f : α → β → γ) (m : HashMap α β) : HashMap α γ := ⟨m.inner.map f⟩ diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index 0c0d5eb42b..4b83503ca0 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -67,7 +67,7 @@ structure HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where namespace HashMap -@[inline, inherit_doc DHashMap.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : +@[cbv_opaque, inline, inherit_doc DHashMap.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : HashMap α β := ⟨DHashMap.emptyWithCapacity capacity⟩ @@ -84,7 +84,7 @@ structure Equiv (m₁ m₂ : HashMap α β) where @[inherit_doc] scoped infixl:50 " ~m " => Equiv -@[inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α) +@[cbv_opaque, inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β := ⟨m.inner.insert a b⟩ @@ -178,7 +178,7 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a @[inline, inherit_doc DHashMap.getKey!] def getKey! [Inhabited α] (m : HashMap α β) (a : α) : α := DHashMap.getKey! m.inner a -@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) : +@[cbv_opaque, inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) : HashMap α β := ⟨m.inner.erase a⟩ @@ -229,7 +229,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w'} [Monad m] : ForM m (Has instance [BEq α] [Hashable α] {m : Type w → Type w'} [Monad m] : ForIn m (HashMap α β) (α × β) where forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init -@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool) +@[cbv_opaque, inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool) (m : HashMap α β) : HashMap α β := ⟨m.inner.filter f⟩ diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index a16c6dfbea..e5cf75a887 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -69,7 +69,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := DHashMap.mem_congr hab -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).contains a = false := DHashMap.contains_emptyWithCapacity @@ -113,7 +113,7 @@ theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] : Singleton.singleton p = (∅ : HashMap α β).insert p.1 p.2 := rfl -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insert k v).contains a = (k == a || m.contains a) := DHashMap.contains_insert @@ -184,7 +184,7 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).size ≤ m.size + 1 := DHashMap.size_insert_le -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashMap α β).erase a = emptyWithCapacity c := ext DHashMap.erase_emptyWithCapacity @@ -197,7 +197,7 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) := DHashMap.isEmpty_erase -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = (!(k == a) && m.contains a) := DHashMap.contains_erase @@ -247,7 +247,7 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β} : @[simp, grind =] theorem get?_eq_getElem? {a : α} : get? m a = m[a]? := rfl @[simp, grind =] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getElem?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β)[a]? = none := DHashMap.Const.get?_emptyWithCapacity @@ -260,7 +260,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m[a]? = none := DHashMap.Const.get?_of_isEmpty -@[grind =] theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : +@[grind =, cbv_eval] theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insert k v)[a]? = if k == a then some v else m[a]? := DHashMap.Const.get?_insert @@ -269,6 +269,15 @@ theorem getElem?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} (m.insert k v)[k]? = some v := DHashMap.Const.get?_insert_self +@[cbv_eval] +theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).get? a = none := + getElem?_emptyWithCapacity + +@[cbv_eval] +theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : + (m.insert k v).get? a = if k == a then some v else m.get? a := + getElem?_insert + -- TODO: request this is reversed, and made `@[simp, grind]` theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = m[a]?.isSome := @@ -299,7 +308,7 @@ theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m[a]? = none := DHashMap.Const.get?_eq_none -@[grind =] theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : +@[grind =, cbv_eval] theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k)[a]? = if k == a then none else m[a]? := DHashMap.Const.get?_erase @@ -307,6 +316,11 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m theorem getElem?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k)[k]? = none := DHashMap.Const.get?_erase_self +@[cbv_eval] +theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : + (m.erase k).get? a = if k == a then none else m.get? a := + getElem?_erase + theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m[a]? = m[b]? := DHashMap.Const.get?_congr hab @@ -349,7 +363,7 @@ theorem getElem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b m[a]'h' = m[b]'((mem_congr hab).1 h') := DHashMap.Const.get_congr hab (h' := h') -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getElem!_emptyWithCapacity [Inhabited β] {a : α} {c} : (emptyWithCapacity c : HashMap α β)[a]! = default := DHashMap.Const.get!_emptyWithCapacity @@ -361,10 +375,20 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a m.isEmpty = true → m[a]! = default := DHashMap.Const.get!_of_isEmpty -@[grind =] theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : +@[grind =, cbv_eval] theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : (m.insert k v)[a]! = if k == a then v else m[a]! := DHashMap.Const.get!_insert +@[cbv_eval] +theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} : + (emptyWithCapacity c : HashMap α β).get! a = default := + getElem!_emptyWithCapacity + +@[cbv_eval] +theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : + (m.insert k v).get! a = if k == a then v else m.get! a := + getElem!_insert + @[simp] theorem getElem!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} : (m.insert k v)[k]! = v := @@ -378,7 +402,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a ¬a ∈ m → m[a]! = default := DHashMap.Const.get!_eq_default -@[grind =] theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : +@[grind =, cbv_eval] theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : (m.erase k)[a]! = if k == a then default else m[a]! := DHashMap.Const.get!_erase @@ -387,6 +411,11 @@ theorem getElem!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k (m.erase k)[k]! = default := DHashMap.Const.get!_erase_self +@[cbv_eval] +theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : + (m.erase k).get! a = if k == a then default else m.get! a := + getElem!_erase + theorem getElem?_eq_some_getElem!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.contains a = true → m[a]? = some m[a]! := DHashMap.Const.get?_eq_some_get!_of_contains @@ -407,7 +436,7 @@ theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : m[a]! = m[b]! := DHashMap.Const.get!_congr hab -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : (emptyWithCapacity c : HashMap α β).getD a fallback = fallback := DHashMap.Const.getD_emptyWithCapacity @@ -420,7 +449,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : m.isEmpty = true → m.getD a fallback = fallback := DHashMap.Const.getD_of_isEmpty -@[grind =] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : +@[grind =, cbv_eval] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : (m.insert k v).getD a fallback = if k == a then v else m.getD a fallback := DHashMap.Const.getD_insert @@ -437,7 +466,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : ¬a ∈ m → m.getD a fallback = fallback := DHashMap.Const.getD_eq_fallback -@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : +@[grind =, cbv_eval] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := DHashMap.Const.getD_erase @@ -3255,7 +3284,7 @@ theorem getElem?_filterMap [EquivBEq α] [LawfulHashable α] DHashMap.Const.get?_filterMap /-- Simpler variant of `getElem?_filterMap` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getElem?_filterMap' [LawfulBEq α] {f : α → β → Option γ} {k : α} : (m.filterMap f)[k]? = m[k]?.bind fun x => f k x := by @@ -3298,7 +3327,7 @@ theorem getElem!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited γ] DHashMap.Const.get!_filterMap /-- Simpler variant of `getElem!_filterMap` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getElem!_filterMap' [LawfulBEq α] [Inhabited γ] {f : α → β → Option γ} {k : α} : (m.filterMap f)[k]! = (m[k]?.bind (f k)).get! := by @@ -3317,7 +3346,7 @@ theorem getD_filterMap [EquivBEq α] [LawfulHashable α] DHashMap.Const.getD_filterMap /-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getD_filterMap' [LawfulBEq α] {f : α → β → Option γ} {k : α} {fallback : γ} : (m.filterMap f).getD k fallback = (m[k]?.bind (f k)).getD fallback := by @@ -3433,7 +3462,7 @@ theorem getElem?_filter [EquivBEq α] [LawfulHashable α] DHashMap.Const.get?_filter /-- Simpler variant of `getElem?_filter` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getElem?_filter' [LawfulBEq α] {f : α → β → Bool} {k : α} : (m.filter f)[k]? = m[k]?.filter (f k) := by @@ -3459,7 +3488,7 @@ theorem getElem!_filter [EquivBEq α] [LawfulHashable α] [Inhabited β] DHashMap.Const.get!_filter /-- Simpler variant of `getElem!_filter` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getElem!_filter' [LawfulBEq α] [Inhabited β] {f : α → β → Bool} {k : α} : (m.filter f)[k]! = (m[k]?.filter (f k)).get! := by @@ -3478,7 +3507,7 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α] DHashMap.Const.getD_filter /-- Simpler variant of `getD_filter` when `LawfulBEq` is available. -/ -@[grind =] +@[grind =, cbv_eval] theorem getD_filter' [LawfulBEq α] {f : α → β → Bool} {k : α} {fallback : β} : (m.filter f).getD k fallback = (m[k]?.filter (f k)).getD fallback := by @@ -3504,6 +3533,7 @@ theorem getKey?_filter [EquivBEq α] [LawfulHashable α] (f x (m[x]'(mem_of_getKey?_eq_some h')))) := DHashMap.Const.getKey?_filter +@[cbv_eval] theorem getKey?_filter_key [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} : (m.filter fun k _ => f k).getKey? k = (m.getKey? k).filter f := @@ -3523,6 +3553,7 @@ theorem getKey!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α] (f x (m[x]'(mem_of_getKey?_eq_some h'))))).get! := DHashMap.Const.getKey!_filter +@[cbv_eval] theorem getKey!_filter_key [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → Bool} {k : α} : (m.filter fun k _ => f k).getKey! k = ((m.getKey? k).filter f).get! := @@ -3536,6 +3567,7 @@ theorem getKeyD_filter [EquivBEq α] [LawfulHashable α] (f x (m[x]'(mem_of_getKey?_eq_some h'))))).getD fallback := DHashMap.Const.getKeyD_filter +@[cbv_eval] theorem getKeyD_filter_key [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} : (m.filter fun k _ => f k).getKeyD k fallback = ((m.getKey? k).filter f).getD fallback := @@ -3566,13 +3598,13 @@ theorem filterMap_equiv_map [EquivBEq α] [LawfulHashable α] (m.filterMap (fun k v => some (f k v))) ~m m.map f := ⟨DHashMap.filterMap_equiv_map⟩ -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem isEmpty_map [EquivBEq α] [LawfulHashable α] {f : α → β → γ} : (m.map f).isEmpty = m.isEmpty := DHashMap.isEmpty_map -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_map [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} : (m.map f).contains k = m.contains k := @@ -3594,13 +3626,13 @@ theorem mem_of_mem_map [EquivBEq α] [LawfulHashable α] k ∈ m.map f → k ∈ m := DHashMap.contains_of_contains_map -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem size_map [EquivBEq α] [LawfulHashable α] {f : α → β → γ} : (m.map f).size = m.size := DHashMap.size_map -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getElem?_map [LawfulBEq α] {f : α → β → γ} {k : α} : (m.map f)[k]? = m[k]?.map (f k) := @@ -3634,7 +3666,7 @@ theorem getElem_map' [EquivBEq α] [LawfulHashable α] f (m.getKey k (mem_of_mem_map h')) (m[k]'(mem_of_mem_map h')) := DHashMap.Const.get_map' -@[grind =] +@[grind =, cbv_eval] theorem getElem!_map [LawfulBEq α] [Inhabited γ] {f : α → β → γ} {k : α} : (m.map f)[k]! = @@ -3654,7 +3686,7 @@ theorem getElem!_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhab (m.map f)[k]! = (m[k]?.map (f k')).get! := DHashMap.Const.get!_map_of_getKey?_eq_some h -@[grind =] +@[grind =, cbv_eval] theorem getD_map [LawfulBEq α] {f : α → β → γ} {k : α} {fallback : γ} : (m.map f).getD k fallback = @@ -3674,7 +3706,7 @@ theorem getD_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhabited (m.map f).getD k fallback = (m[k]?.map (f k')).getD fallback := DHashMap.Const.getD_map_of_getKey?_eq_some h -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getKey?_map [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} : (m.map f).getKey? k = m.getKey? k := @@ -3686,13 +3718,13 @@ theorem getKey_map [EquivBEq α] [LawfulHashable α] (m.map f).getKey k h' = m.getKey k (mem_of_mem_map h') := DHashMap.getKey_map -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getKey!_map [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → β → γ} {k : α} : (m.map f).getKey! k = m.getKey! k := DHashMap.getKey!_map -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem getKeyD_map [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k fallback : α} : (m.map f).getKeyD k fallback = m.getKeyD k fallback := diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 5ee9a33425..64d670f04d 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -65,7 +65,7 @@ set so that it can hold the given number of elements without reallocating. It is use the empty collection notations `∅` and `{}` to create an empty hash set with the default capacity. -/ -@[inline] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : HashSet α := +@[cbv_opaque, inline] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : HashSet α := ⟨HashMap.emptyWithCapacity capacity⟩ instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) where @@ -91,7 +91,7 @@ Note: this non-replacement behavior is true for `HashSet` and `HashSet.Raw`. The `insert` function on `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves differently: it will overwrite an existing mapping. -/ -@[inline] def insert (m : HashSet α) (a : α) : HashSet α := +@[cbv_opaque, inline] def insert (m : HashSet α) (a : α) : HashSet α := ⟨m.inner.insertIfNew a ()⟩ instance : Singleton α (HashSet α) := ⟨fun a => (∅ : HashSet α).insert a⟩ @@ -126,7 +126,7 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m) inferInstanceAs (Decidable (a ∈ m.inner)) /-- Removes the element if it exists. -/ -@[inline] def erase (m : HashSet α) (a : α) : HashSet α := +@[cbv_opaque, inline] def erase (m : HashSet α) (a : α) : HashSet α := ⟨m.inner.erase a⟩ /-- The number of elements present in the set -/ @@ -213,7 +213,7 @@ instance [BEq α] [Hashable α] {m : Type v → Type w} [Monad m] : ForIn m (Has forIn m init f := m.forIn f init /-- Removes all elements from the hash set for which the given function returns `false`. -/ -@[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α := +@[cbv_opaque, inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α := ⟨m.inner.filter fun a _ => f a⟩ /-- diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index c81707b1fc..56f3cdd6c8 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -65,7 +65,7 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := HashMap.mem_congr hab -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).contains a = false := HashMap.contains_emptyWithCapacity @@ -106,7 +106,7 @@ theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] : @[simp] theorem singleton_eq_insert {a : α} : Singleton.singleton a = (∅ : HashSet α).insert a := rfl -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} : (m.insert k).contains a = (k == a || m.contains a) := HashMap.contains_insertIfNew @@ -172,7 +172,7 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).size ≤ m.size + 1 := HashMap.size_insertIfNew_le -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashSet α).erase a = emptyWithCapacity c := ext HashMap.erase_emptyWithCapacity @@ -185,7 +185,7 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) := HashMap.isEmpty_erase -@[simp, grind =] +@[simp, grind =, cbv_eval] theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = (!(k == a) && m.contains a) := HashMap.contains_erase @@ -262,7 +262,7 @@ theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.get? a = none := HashMap.getKey?_eq_none -@[grind =] theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : +@[grind =, cbv_eval] theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).get? a = if k == a then none else m.get? a := HashMap.getKey?_erase @@ -344,7 +344,7 @@ theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α ¬a ∈ m → m.get! a = default := HashMap.getKey!_eq_default -@[grind =] theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} : +@[grind =, cbv_eval] theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).get! a = if k == a then default else m.get! a := HashMap.getKey!_erase @@ -404,7 +404,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} : ¬a ∈ m → m.getD a fallback = fallback := HashMap.getKeyD_eq_fallback -@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} : +@[grind =, cbv_eval] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} : (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := HashMap.getKeyD_erase diff --git a/src/Std/Data/Iterators/Combinators/Drop.lean b/src/Std/Data/Iterators/Combinators/Drop.lean index b952136879..27b1a33714 100644 --- a/src/Std/Data/Iterators/Combinators/Drop.lean +++ b/src/Std/Data/Iterators/Combinators/Drop.lean @@ -37,7 +37,7 @@ it.drop 3 ------⊥ Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator does not drop any elements anymore. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.drop {α : Type w} {β : Type w} (n : Nat) (it : Iter (α := α) β) : Iter (α := Drop α Id β) β := it.toIterM.drop n |>.toIter diff --git a/src/Std/Data/Iterators/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Combinators/DropWhile.lean index 180cd8ea02..38d89d5072 100644 --- a/src/Std/Data/Iterators/Combinators/DropWhile.lean +++ b/src/Std/Data/Iterators/Combinators/DropWhile.lean @@ -56,7 +56,7 @@ Depending on `P`, it is possible that `it.dropWhileM P` is productive although This combinator calls `P` on each output of `it` until the predicate evaluates to false. After that, the combinator incurs an additional O(1) cost for each value emitted by `it`. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.dropWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) := (it.toIterM.dropWhile P |>.toIter : Iter β) diff --git a/src/Std/Data/Iterators/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/TakeWhile.lean index 5d767e1afe..cafcd4487c 100644 --- a/src/Std/Data/Iterators/Combinators/TakeWhile.lean +++ b/src/Std/Data/Iterators/Combinators/TakeWhile.lean @@ -42,7 +42,7 @@ In this case, the `Finite` (or `Productive`) instance needs to be proved manuall This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then it terminates. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.takeWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) := (it.toIterM.takeWhile P |>.toIter : Iter β) diff --git a/src/Std/Data/Iterators/Combinators/Zip.lean b/src/Std/Data/Iterators/Combinators/Zip.lean index 4e83ddc909..b90bf8bf6c 100644 --- a/src/Std/Data/Iterators/Combinators/Zip.lean +++ b/src/Std/Data/Iterators/Combinators/Zip.lean @@ -42,7 +42,7 @@ This combinator incurs an additional O(1) cost with each step taken by `left` or Right now, the compiler does not unbox the internal state, leading to worse performance than theoretically possible. -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Iter.zip {α₁ : Type w} {β₁: Type w} {α₂ : Type w} {β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] (left : Iter (α := α₁) β₁) (right : Iter (α := α₂) β₂) := diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean index 2ed254118d..9c030f916e 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean @@ -50,7 +50,7 @@ theorem Iter.atIdxSlow?_drop {α β} rw [atIdxSlow?_eq_match, atIdxSlow?_eq_match, step_drop] cases it.step using PlausibleIterStep.casesOn <;> simp [*] -@[simp] +@[cbv_eval, simp] theorem Iter.toList_drop {α β} [Iterator α Id β] {n : Nat} [Finite α Id] {it : Iter (α := α) β} : (it.drop n).toList = it.toList.drop n := by @@ -64,7 +64,7 @@ theorem Iter.toListRev_drop {α β} [Iterator α Id β] {n : Nat} (it.drop n).toListRev = (it.toList.reverse.take (it.toList.length - n)) := by rw [toListRev_eq, toList_drop, List.reverse_drop] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_drop {α β} [Iterator α Id β] {n : Nat} [Finite α Id] {it : Iter (α := α) β} : (it.drop n).toArray = it.toArray.extract n := by diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean index 3237de9b97..4fbc5e4b0f 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean @@ -136,14 +136,14 @@ theorem Iter.toList_intermediateDropWhile_of_finite {α β} [Iterator α Id β] simp [ihs hp] · simp -@[simp] +@[cbv_eval, simp] theorem Iter.toList_dropWhile_of_finite {α β} [Iterator α Id β] {P} [Finite α Id] {it : Iter (α := α) β} : (it.dropWhile P).toList = it.toList.dropWhile P := by simp [dropWhile_eq_intermediateDropWhile, toList_intermediateDropWhile_of_finite] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_dropWhile_of_finite {α β} [Iterator α Id β] {P} [Finite α Id] {it : Iter (α := α) β} : diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean index 44bf9c44a1..19a969ad43 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean @@ -135,7 +135,7 @@ private theorem List.getElem?_takeWhile {l : List α} {P : α → Bool} {k} : specialize h 0 simp_all -@[simp] +@[cbv_eval, simp] theorem Iter.toList_takeWhile_of_finite {α β} [Iterator α Id β] {P} [Finite α Id] {it : Iter (α := α) β} : @@ -150,7 +150,7 @@ theorem Iter.toListRev_takeWhile_of_finite {α β} [Iterator α Id β] {P} (it.takeWhile P).toListRev = (it.toList.takeWhile P).reverse := by rw [toListRev_eq, toList_takeWhile_of_finite] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_takeWhile_of_finite {α β} [Iterator α Id β] {P} [Finite α Id] {it : Iter (α := α) β} : diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean index e810699be5..1bc94d7663 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean @@ -262,7 +262,7 @@ theorem Iter.atIdxSlow?_zip {α₁ α₂ β₁ β₂} [Iterator α₁ Id β₁] (it₁.zip it₂).atIdxSlow? n = do return (← it₁.atIdxSlow? n, ← it₂.atIdxSlow? n) := by rw [zip_eq_intermediateZip, atIdxSlow?_intermediateZip] -@[simp] +@[cbv_eval, simp] theorem Iter.toList_zip_of_finite {α₁ α₂ β₁ β₂} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter (α := α₁) β₁} {it₂ : Iter (α := α₂) β₂} [Finite α₁ Id] [Finite α₂ Id] : @@ -328,7 +328,7 @@ theorem Iter.toListRev_zip_of_finite_right {α₁ α₂ β₁ β₂} [Iterator (it₁.zip it₂).toListRev = ((it₁.take it₂.toList.length).toList.zip it₂.toList).reverse := by simp [toListRev_eq, toList_zip_of_finite_right] -@[simp] +@[cbv_eval, simp] theorem Iter.toArray_zip_of_finite {α₁ α₂ β₁ β₂} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter (α := α₁) β₁} {it₂ : Iter (α := α₂) β₂} [Finite α₁ Id] [Finite α₂ Id] : diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean index 7e2061c31d..ba7e641bf0 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean @@ -67,7 +67,7 @@ theorem Array.toList_iterFromIdx {array : Array β} simp [Iter.toList, Array.iterFromIdx_eq_toIter_iterFromIdxM, Iter.toIterM_toIter, Array.toList_iterFromIdxM] -@[simp, grind =] +@[cbv_eval, simp, grind =] theorem Array.toList_iter {array : Array β} : array.iter.toList = array.toList := by simp [Array.iter_eq_iterFromIdx, Array.toList_iterFromIdx] @@ -77,7 +77,7 @@ theorem Array.toArray_iterFromIdx {array : Array β} {pos : Nat} : (array.iterFromIdx pos).toArray = array.extract pos := by simp [iterFromIdx_eq_toIter_iterFromIdxM, Iter.toArray] -@[simp, grind =] +@[cbv_eval, simp, grind =] theorem Array.toArray_iter {array : Array β} : array.iter.toArray = array := by simp [Array.iter_eq_iterFromIdx] diff --git a/src/Std/Data/Iterators/Producers/Array.lean b/src/Std/Data/Iterators/Producers/Array.lean index b12ce8b848..8c3c292366 100644 --- a/src/Std/Data/Iterators/Producers/Array.lean +++ b/src/Std/Data/Iterators/Producers/Array.lean @@ -29,7 +29,7 @@ The monadic version of this iterator is `Array.iterFromIdxM`. * `Finite` instance: always * `Productive` instance: always -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Array.iterFromIdx {α : Type w} (l : Array α) (pos : Nat) : Iter (α := ArrayIterator α) α := ((l.iterFromIdxM Id pos).toIter : Iter α) @@ -45,7 +45,7 @@ The monadic version of this iterator is `Array.iterM`. * `Finite` instance: always * `Productive` instance: always -/ -@[always_inline, inline] +@[cbv_opaque, always_inline, inline] def Array.iter {α : Type w} (l : Array α) : Iter (α := ArrayIterator α) α := ((l.iterM Id).toIter : Iter α) diff --git a/tests/elab/cbv3.lean b/tests/elab/cbv3.lean index 81363a3456..4bdc8874fa 100644 --- a/tests/elab/cbv3.lean +++ b/tests/elab/cbv3.lean @@ -1,5 +1,3 @@ -set_option cbv.warning false - def f (n : Nat) : Nat := match n with | 0 => 0 | (n + 1) => (f n) + 1 diff --git a/tests/elab/cbv_classical.lean b/tests/elab/cbv_classical.lean index c36b185716..10c32f1ae7 100644 --- a/tests/elab/cbv_classical.lean +++ b/tests/elab/cbv_classical.lean @@ -1,5 +1,3 @@ -set_option cbv.warning false - /-! # A regression test against `cbv` picking up `Classical.propDecidable`, when re-synthesizing instances. diff --git a/tests/elab/cbv_eval_erase.lean b/tests/elab/cbv_eval_erase.lean index 283fa11a55..75c2381196 100644 --- a/tests/elab/cbv_eval_erase.lean +++ b/tests/elab/cbv_eval_erase.lean @@ -1,9 +1,11 @@ import Std -set_option cbv.warning false -- Use opaque constants so that cbv_eval is the ONLY way cbv can reduce them. -- After erasure, cbv makes no progress and the goal must be closed manually. opaque myConst : Nat + +/-- warning: declaration uses `sorry` -/ +#guard_msgs in @[cbv_eval] theorem myConst_eq : myConst = 42 := sorry -- Before erasure: cbv reduces myConst to 42 via cbv_eval @@ -26,6 +28,9 @@ example : myConst = 42 := by -- Scoping: erasure inside a section is reverted opaque myConst2 : Nat + +/-- warning: declaration uses `sorry` -/ +#guard_msgs in @[cbv_eval] theorem myConst2_eq : myConst2 = 100 := sorry section @@ -49,6 +54,9 @@ example : myConst2 = 100 := by cbv -- Erasure of inverted theorem opaque myConst3 : Nat + +/-- warning: declaration uses `sorry` -/ +#guard_msgs in @[cbv_eval ←] theorem myConst3_eq : 7 = myConst3 := sorry example : myConst3 = 7 := by cbv @@ -73,7 +81,12 @@ example : myConst3 = 7 := by cbv -- Erasure with multiple cbv_eval rules: erase only one opaque myFn : Nat → Nat +/-- warning: declaration uses `sorry` -/ +#guard_msgs in @[cbv_eval] theorem myFn_zero : myFn 0 = 1 := sorry + +/-- warning: declaration uses `sorry` -/ +#guard_msgs in @[cbv_eval] theorem myFn_one : myFn 1 = 0 := sorry example : myFn 0 = 1 := by cbv diff --git a/tests/elab/cbv_eval_erase.lean.out.expected b/tests/elab/cbv_eval_erase.lean.out.expected deleted file mode 100644 index 9a2ea47c92..0000000000 --- a/tests/elab/cbv_eval_erase.lean.out.expected +++ /dev/null @@ -1,5 +0,0 @@ -cbv_eval_erase.lean:7:20-7:30: warning: declaration uses `sorry` -cbv_eval_erase.lean:29:20-29:31: warning: declaration uses `sorry` -cbv_eval_erase.lean:52:22-52:33: warning: declaration uses `sorry` -cbv_eval_erase.lean:76:20-76:29: warning: declaration uses `sorry` -cbv_eval_erase.lean:77:20-77:28: warning: declaration uses `sorry` diff --git a/tests/elab/cbv_hashmap_annotations.lean b/tests/elab/cbv_hashmap_annotations.lean new file mode 100644 index 0000000000..d9f105e3f4 --- /dev/null +++ b/tests/elab/cbv_hashmap_annotations.lean @@ -0,0 +1,218 @@ +import Std +open Std + +/-! ### HashSet.contains -/ + +example : (HashSet.emptyWithCapacity.insert 3).contains 3 = true := by cbv +example : (HashSet.emptyWithCapacity.insert 3).contains 4 = false := by cbv +example : (HashSet.emptyWithCapacity : HashSet Nat).contains 1 = false := by cbv +example : (HashSet.emptyWithCapacity.insert 1 |>.insert 2 |>.insert 3).contains 2 = true := by cbv +example : (HashSet.emptyWithCapacity.insert 1 |>.insert 2 |>.insert 3).contains 5 = false := by cbv +example : (HashSet.emptyWithCapacity.insert 10 |>.insert 20).contains 10 = true := by cbv +example : (HashSet.emptyWithCapacity.insert 10 |>.insert 20).contains 20 = true := by cbv +example : (HashSet.emptyWithCapacity.insert 10 |>.insert 20).contains 30 = false := by cbv + +/-! ### HashMap.contains -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10).contains 1 = true := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10).contains 2 = false := by cbv +example : (HashMap.emptyWithCapacity : HashMap Nat Nat).contains 1 = false := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 30).contains 2 = true := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 30).contains 4 = false := by cbv + +/-! ### HashMap.get? -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 2).get? 1 = .some 2 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 2).get? 3 = .none := by cbv +example : (HashMap.emptyWithCapacity : HashMap Nat Nat).get? 1 = .none := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 1 = .some 10 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 2 = .some 20 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 3 = .some 30 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 4 = .none := by cbv +-- overwrite +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 1 99).get? 1 = .some 99 := by cbv + +/-! ### HashMap.get! -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 42).get! 1 = 42 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 42).get! 2 = 0 := by cbv +example : (HashMap.emptyWithCapacity : HashMap Nat Nat).get! 1 = 0 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20).get! 2 = 20 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20).get! 3 = 0 := by cbv + +/-! ### HashMap.getD -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 42).getD 1 999 = 42 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 42).getD 2 999 = 999 := by cbv +example : (HashMap.emptyWithCapacity : HashMap Nat Nat).getD 1 999 = 999 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20).getD 2 0 = 20 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20).getD 3 0 = 0 := by cbv + +/-! ### DHashMap.contains -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10).contains 1 = true := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10).contains 2 = false := by cbv +example : (DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).contains 1 = false := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 30).contains 2 = true := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 30).contains 4 = false := by cbv + +/-! ### DHashMap.get? -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 2).get? 1 = .some 2 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 2).get? 3 = .none := by cbv +example : (DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).get? 1 = .none := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 1 = .some 10 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 2 = .some 20 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 30).get? 4 = .none := by cbv +-- overwrite +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 1 99).get? 1 = .some 99 := by cbv + +/-! ### DHashMap.get! -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 42).get! 1 = 42 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 42).get! 2 = 0 := by cbv +example : (DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).get! 1 = 0 := by cbv + +/-! ### DHashMap.getD -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 42).getD 1 999 = 42 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 42).getD 2 999 = 999 := by cbv +example : (DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).getD 1 999 = 999 := by cbv + +/-! ### HashSet.erase -/ + +-- erase from empty +example : ((HashSet.emptyWithCapacity : HashSet Nat).erase 1).contains 1 = false := by cbv +-- erase existing element +example : ((HashSet.emptyWithCapacity.insert 1 |>.insert 2 |>.insert 3).erase 2).contains 2 = false := by cbv +-- erase does not affect other elements +example : ((HashSet.emptyWithCapacity.insert 1 |>.insert 2 |>.insert 3).erase 2).contains 1 = true := by cbv +example : ((HashSet.emptyWithCapacity.insert 1 |>.insert 2 |>.insert 3).erase 2).contains 3 = true := by cbv +-- erase non-existing element +example : ((HashSet.emptyWithCapacity.insert 1 |>.insert 2).erase 5).contains 1 = true := by cbv +example : ((HashSet.emptyWithCapacity.insert 1 |>.insert 2).erase 5).contains 5 = false := by cbv + +/-! ### HashMap.erase + contains -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).erase 1).contains 1 = false := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).contains 1 = false := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).contains 2 = true := by cbv + +/-! ### HashMap.erase + get? -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).get? 1 = .none := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).get? 2 = .some 20 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).erase 1).get? 1 = .none := by cbv + +/-! ### HashMap.erase + get! -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).get! 1 = 0 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).get! 2 = 20 := by cbv + +/-! ### HashMap.erase + getD -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).getD 1 999 = 999 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.erase 1).getD 2 999 = 20 := by cbv + +/-! ### DHashMap.erase + contains -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).erase 1).contains 1 = false := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).contains 1 = false := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).contains 2 = true := by cbv + +/-! ### DHashMap.erase + get? -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).get? 1 = .none := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).get? 2 = .some 20 := by cbv + +/-! ### DHashMap.erase + get! -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).get! 1 = 0 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).get! 2 = 20 := by cbv + +/-! ### DHashMap.erase + getD -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).getD 1 999 = 999 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.erase 1).getD 2 999 = 20 := by cbv + +/-! ### HashMap.map + getD -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).getD 1 999 = 20 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).getD 2 999 = 40 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).getD 3 999 = 999 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).map (fun _ v => v + 1)).getD 1 999 = 999 := by cbv + +/-! ### HashMap.map + contains -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).contains 1 = true := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).contains 3 = false := by cbv + +/-! ### HashMap.filter + getD -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 5 |>.filter (fun _ v => v > 8)).getD 1 999 = 10 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 5 |>.filter (fun _ v => v > 8)).getD 3 999 = 999 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.insert 3 5 |>.filter (fun _ v => v > 8)).getD 4 999 = 999 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).getD 2 999 = 20 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).getD 1 999 = 999 := by cbv + +/-! ### HashMap.filterMap + getD -/ + +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).getD 2 999 = 40 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).getD 1 999 = 999 := by cbv +example : ((HashMap.emptyWithCapacity : HashMap Nat Nat).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).getD 3 999 = 999 := by cbv + +/-! ### DHashMap.map + get? -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).get? 1 = .some 20 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).get? 2 = .some 40 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).get? 3 = .none := by cbv + +/-! ### DHashMap.map + get! -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v + 1)).get! 1 = 11 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v + 1)).get! 3 = 0 := by cbv + +/-! ### DHashMap.map + getD -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.map (fun _ v => v + 5)).getD 1 999 = 15 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.map (fun _ v => v + 5)).getD 2 999 = 999 := by cbv + +/-! ### DHashMap.map + contains -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).contains 1 = true := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.map (fun _ v => v * 2)).contains 3 = false := by cbv + +/-! ### DHashMap.filter + contains -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).contains 2 = true := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).contains 1 = false := by cbv + +/-! ### DHashMap.filter + get? -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 5 |>.filter (fun _ v => v > 8)).get? 1 = .some 10 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.insert 3 5 |>.filter (fun _ v => v > 8)).get? 3 = .none := by cbv + +/-! ### DHashMap.filter + get! -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).get! 2 = 20 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).get! 1 = 0 := by cbv + +/-! ### DHashMap.filter + getD -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).getD 2 999 = 20 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filter (fun _ v => v > 15)).getD 1 999 = 999 := by cbv + +/-! ### DHashMap.filterMap + get? -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).get? 2 = .some 40 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).get? 1 = .none := by cbv + +/-! ### DHashMap.filterMap + get! -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).get! 2 = 40 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).get! 1 = 0 := by cbv + +/-! ### DHashMap.filterMap + getD -/ + +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).getD 2 999 = 40 := by cbv +example : ((DHashMap.emptyWithCapacity : DHashMap Nat (fun _ => Nat)).insert 1 10 |>.insert 2 20 |>.filterMap (fun _ v => if v > 15 then some (v * 2) else none)).getD 1 999 = 999 := by cbv diff --git a/tests/elab/cbv_iter.lean b/tests/elab/cbv_iter.lean new file mode 100644 index 0000000000..a188043eff --- /dev/null +++ b/tests/elab/cbv_iter.lean @@ -0,0 +1,349 @@ +import Std + +/-! ### Basic producer tests -/ + +example : [1, 2, 3].iter.toList = [1, 2, 3] := by cbv +example : [1, 2, 3].iter.toArray = #[1, 2, 3] := by cbv +example : ([] : List Nat).iter.toList = [] := by cbv +example : ([] : List Nat).iter.toArray = #[] := by cbv + +/-! ### Map tests -/ + +example : ([1, 2, 3].iter.map (· + 1)).toList = [2, 3, 4] := by cbv +example : ([1, 2, 3].iter.map (· + 1)).toArray = #[2, 3, 4] := by cbv +example : ([1, 2, 3].iter.map (· * 2)).toList = [2, 4, 6] := by cbv +example : (([] : List Nat).iter.map (· + 1)).toList = [] := by cbv + +/-! ### Filter tests -/ + +example : ([1, 2, 3, 4].iter.filter (· % 2 == 0)).toList = [2, 4] := by cbv +example : ([1, 2, 3, 4].iter.filter (· % 2 == 0)).toArray = #[2, 4] := by cbv + +/-! ### FilterMap tests -/ + +example : ([1, 2, 3, 4].iter.filterMap (fun x => if x % 2 == 0 then some (x * 10) else none)).toList + = [20, 40] := by cbv + +/-! ### Fold tests -/ + +example : [1, 2, 3].iter.fold (· + ·) 0 = 6 := by cbv +example : [1, 2, 3, 4].iter.fold (· * ·) 1 = 24 := by cbv +example : ([] : List Nat).iter.fold (· + ·) 0 = 0 := by cbv + +/-! ### Composed combinator tests -/ + +example : ([1, 2, 3, 4].iter.filter (· % 2 == 0) |>.map (· * 10)).toList = [20, 40] := by cbv +example : ([1, 2, 3].iter.map (· + 1) |>.filter (· % 2 == 0)).toList = [2, 4] := by cbv +example : ([1, 2, 3].iter.map (· * 2) |>.map (· + 1)).toList = [3, 5, 7] := by cbv + +/-! ### String operations using iterators internally -/ + +example : "abc".contains 'b' = true := by cbv +example : "abc".contains 'd' = false := by cbv +example : "hello".contains (· == 'l') = true := by cbv +example : String.toNat? "192" = some 192 := by cbv +example : String.toNat? "0" = some 0 := by cbv +example : String.toNat? "" = none := by cbv +example : "hello".foldl (fun n _ => n + 1) 0 = 5 := by cbv + +-- Tests requiring `String.contains_string_eq` (not yet available): +def filterBySubstring (strings : Array String) (substring : String) : Array String := + strings.filter (·.contains substring) + +example : filterBySubstring #[] "john" = #[] := by cbv +example : filterBySubstring #["xxx", "asd", "xxy", "john doe", "xxxAAA", "xxx"] "xxx" = #["xxx", "xxxAAA", "xxx"] := by cbv +example : filterBySubstring #["xxx", "asd", "aaaxxy", "john doe", "xxxAAA", "xxx"] "xx" = #["xxx", "aaaxxy", "xxxAAA", "xxx"] := by cbv +example : filterBySubstring #["grunt", "trumpet", "prune", "gruesome"] "run" = #["grunt", "prune"] := by cbv + + +def allPrefixes (string : String) : Array String.Slice := + if string = "" then + #[] + else + ((string.positions.drop 1).map (string.sliceTo ·.1) |>.toArray).push string + +example : allPrefixes "" = #[] := by cbv +example : allPrefixes "asdfgh" == #["a".toSlice, "as", "asd", "asdf", "asdfg", "asdfgh"] := by cbv +example : allPrefixes "WWW" == #["W".toSlice, "WW", "WWW"] := by cbv + +def sumSquares (xs : List Rat) : Int := + xs.map (·.ceil ^ (2 : Nat)) |>.sum + +/-! ### Rational arithmetic tests -/ + +example : sumSquares [1, 2, 3] = 14 := by cbv +example : sumSquares [1.0, 2, 3] = 14 := by cbv +example : sumSquares [1, 3, 5, 7] = 84 := by cbv +example : sumSquares [1.4, 4.2, 0] = 29 := by cbv +example : sumSquares [-2.4, 1, 1] = 6 := by cbv +example : sumSquares [100, 1, 15, 2] = 10230 := by cbv +example : sumSquares [10000, 10000] = 200000000 := by cbv +example : sumSquares [-1.4, 4.6, 6.3] = 75 := by cbv +example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by cbv +example : sumSquares [0] = 0 := by cbv +example : sumSquares [-1] = 1 := by cbv +example : sumSquares [-1, 1, 0] = 2 := by cbv + +/-! ### String case swapping and reversal tests -/ + +def reverseString (s : String) : String := + s.revChars.fold (init := "") fun sofar c => sofar.push c + +def swapCase (c : Char) : Char := + if c.isUpper then + c.toLower + else if c.isLower then + c.toUpper + else + c + +def solve (s : String) : String := + if s.contains Char.isAlpha then + s.map swapCase + else + reverseString s + +example : solve "AsDf" = "aSdF" := by cbv +example : solve "1234" = "4321" := by cbv +example : solve "ab" = "AB" := by cbv +example : solve "#a@C" = "#A@c" := by cbv +example : solve "#AsdfW^45" = "#aSDFw^45" := by cbv +example : solve "#6@2" = "2@6#" := by cbv +example : solve "#$a^D" = "#$A^d" := by cbv +example : solve "#ccc" = "#CCC" := by cbv + + +/-! ### Subarray iteration tests -/ + +def isSorted (xs : Array Nat) : Bool := Id.run do + if h : xs.size > 0 then + let mut last := xs[0] + let mut repeated := false + for x in xs[1...*] do + match compare last x with + | .lt => + last := x + repeated := false + | .eq => + if repeated then + return false + else + repeated := true + | .gt => + return false + return true + +example : isSorted #[5] = true := by cbv +example : isSorted #[1, 2, 3, 4, 5] = true := by cbv +example : isSorted #[1, 3, 2, 4, 5] = false := by cbv +example : isSorted #[1, 2, 3, 4, 5, 6] = true := by cbv +example : isSorted #[1, 2, 3, 4, 5, 6, 7] = true := by cbv +example : isSorted #[1, 3, 2, 4, 5, 6, 7] = false := by cbv +example : isSorted #[] = true := by cbv +example : isSorted #[1] = true := by cbv +example : isSorted #[3, 2, 1] = false := by cbv +example : isSorted #[1, 2, 2, 2, 3, 4] = false := by cbv +example : isSorted #[1, 2, 3, 3, 3, 4] = false := by cbv +example : isSorted #[1, 2, 2, 3, 3, 4] = true := by cbv +example : isSorted #[1, 2, 3, 4] = true := by cbv + +/-! ### Inclusive range iteration tests -/ + +def f (n : Nat) : List Nat := Id.run do + let mut ret : List Nat := [] + for i in 1...=n do + if i % 2 = 0 then + let mut x := 1 + for j in 1...=i do x := x * j + ret := x :: ret + else + let mut x := 0 + for j in 1...=i do x := x + j + ret := x :: ret + return ret.reverse + +example : f 5 = [1, 2, 6, 24, 15] := by cbv +example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by cbv +example : f 1 = [1] := by cbv +example : f 3 = [1, 2, 6] := by cbv + + +def hasCloseElements (xs : Array Rat) (threshold : Rat) : Bool := Id.run do + let sorted := xs.mergeSort + for h : i in *...(sorted.size - 1) do + if (sorted[i + 1] - sorted[i]).abs < threshold then + return true + return false + +example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by cbv +example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by cbv +example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by cbv +example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by cbv +example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by cbv +example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by cbv +example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by cbv + +/-! ### Array.iter producer tests -/ + +example : #[1, 2, 3].iter.toList = [1, 2, 3] := by cbv +example : #[1, 2, 3].iter.toArray = #[1, 2, 3] := by cbv +example : (#[] : Array Nat).iter.toList = [] := by cbv +example : (#[1, 2, 3].iter.map (· + 10)).toList = [11, 12, 13] := by cbv +example : (#[1, 2, 3, 4].iter.filter (· % 2 == 0)).toArray = #[2, 4] := by cbv + +/-! ### FlatMap tests -/ + +example : ([1, 2, 3].iter.flatMap (fun n => List.replicate n n |>.iter)).toList + = [1, 2, 2, 3, 3, 3] := by cbv +example : ([1, 2].iter.flatMap (fun n => [n, n * 10].iter)).toList + = [1, 10, 2, 20] := by cbv +example : (([] : List Nat).iter.flatMap (fun n => [n].iter)).toList = [] := by cbv + +/-! ### TakeWhile tests -/ + +example : ([1, 2, 3, 4, 5].iter.takeWhile (· < 4)).toList = [1, 2, 3] := by cbv +example : ([1, 2, 3, 4, 5].iter.takeWhile (· < 1)).toList = [] := by cbv +example : ([1, 2, 3].iter.takeWhile (· < 10)).toList = [1, 2, 3] := by cbv + +/-! ### DropWhile tests -/ + +example : ([1, 2, 3, 4, 5].iter.dropWhile (· < 4)).toList = [4, 5] := by cbv +example : ([1, 2, 3, 4, 5].iter.dropWhile (· < 1)).toList = [1, 2, 3, 4, 5] := by cbv +example : ([1, 2, 3].iter.dropWhile (· < 10)).toList = [] := by cbv + +/-! ### Zip tests -/ + +example : ([1, 2, 3].iter.zip [10, 20, 30].iter).toList = [(1, 10), (2, 20), (3, 30)] := by cbv +example : ([1, 2].iter.zip [10, 20, 30].iter).toList = [(1, 10), (2, 20)] := by cbv +example : ([1, 2, 3].iter.zip ([] : List Nat).iter).toList = [] := by cbv + +/-! ### Composed new combinator tests -/ + +def dotProduct (xs ys : List Int) : Int := + (xs.iter.zip ys.iter |>.map (fun (a, b) => a * b) |>.fold (· + ·) 0) + +example : dotProduct [1, 2, 3] [4, 5, 6] = 32 := by cbv +example : dotProduct [1, 0, -1] [1, 1, 1] = 0 := by cbv +example : dotProduct [] [] = 0 := by cbv + +def runLengthEncode (xs : List Nat) : List (Nat × Nat) := Id.run do + let mut result : List (Nat × Nat) := [] + let mut current := 0 + let mut count := 0 + for x in xs do + if count == 0 then + current := x + count := 1 + else if x == current then + count := count + 1 + else + result := (current, count) :: result + current := x + count := 1 + if count > 0 then + result := (current, count) :: result + return result.reverse + +example : runLengthEncode [1, 1, 2, 3, 3, 3, 2, 2] = [(1, 2), (2, 1), (3, 3), (2, 2)] := by cbv +example : runLengthEncode [] = [] := by cbv +example : runLengthEncode [5] = [(5, 1)] := by cbv + +/-! ### Range iteration tests for all interval types -/ + +-- Rco (closed-open): a...b +def sumRco (a b : Nat) : Nat := Id.run do + let mut s := 0 + for i in a...b do s := s + i + return s + +example : sumRco 0 5 = 10 := by cbv +example : sumRco 1 4 = 6 := by cbv +example : sumRco 3 3 = 0 := by cbv +example : sumRco 0 0 = 0 := by cbv +example : sumRco 0 1 = 0 := by cbv + +-- Rcc (closed-closed): a...=b (already tested via `f`, adding direct tests) +def sumRcc (a b : Nat) : Nat := Id.run do + let mut s := 0 + for i in a...=b do s := s + i + return s + +example : sumRcc 0 4 = 10 := by cbv +example : sumRcc 1 3 = 6 := by cbv +example : sumRcc 3 3 = 3 := by cbv +example : sumRcc 5 3 = 0 := by cbv + +-- Rio (inclusive-open): *...b (already tested via hasCloseElements, adding direct tests) +def sumRio (b : Nat) : Nat := Id.run do + let mut s := 0 + for i in *...b do s := s + i + return s + +example : sumRio 5 = 10 := by cbv +example : sumRio 1 = 0 := by cbv +example : sumRio 0 = 0 := by cbv + +-- Ric (inclusive-closed): *...=b +def sumRic (b : Nat) : Nat := Id.run do + let mut s := 0 + for i in *...=b do s := s + i + return s + +example : sumRic 4 = 10 := by cbv +example : sumRic 0 = 0 := by cbv +example : sumRic 1 = 1 := by cbv + +-- Roc (open-closed): a<...=b +def sumRoc (a b : Nat) : Nat := Id.run do + let mut s := 0 + for i in a<...=b do s := s + i + return s + +example : sumRoc 0 4 = 10 := by cbv +example : sumRoc 0 1 = 1 := by cbv +example : sumRoc 3 3 = 0 := by cbv +example : sumRoc 1 5 = 14 := by cbv + +-- Roo (open-open): a<...b +def sumRoo (a b : Nat) : Nat := Id.run do + let mut s := 0 + for i in a<...b do s := s + i + return s + +example : sumRoo 0 5 = 10 := by cbv +example : sumRoo 0 1 = 0 := by cbv +example : sumRoo 3 3 = 0 := by cbv +example : sumRoo 1 5 = 9 := by cbv + +-- Rco (closed-open): a...b +example : (1...3).iter.toList = [1, 2] := by cbv +example : (1...3).iter.toArray = #[1, 2] := by cbv +example : (0...5).iter.toList = [0, 1, 2, 3, 4] := by cbv +example : (3...3).iter.toList = [] := by cbv + +-- Rcc (closed-closed): a...=b +example : (1...=3).iter.toList = [1, 2, 3] := by cbv +example : (1...=3).iter.toArray = #[1, 2, 3] := by cbv +example : (0...=4).iter.toList = [0, 1, 2, 3, 4] := by cbv +example : (3...=3).iter.toList = [3] := by cbv +example : (5...=3).iter.toList = [] := by cbv + +-- Rio (inclusive-open): *...b +example : ((*...5 : Std.Rio Nat)).iter.toList = [0, 1, 2, 3, 4] := by cbv +example : ((*...0 : Std.Rio Nat)).iter.toList = [] := by cbv + +-- Ric (inclusive-closed): *...=b +example : ((*...=4 : Std.Ric Nat)).iter.toList = [0, 1, 2, 3, 4] := by cbv +example : ((*...=0 : Std.Ric Nat)).iter.toList = [0] := by cbv + +-- Roc (open-closed): a<...=b +example : (1<...=4).iter.toList = [2, 3, 4] := by cbv +example : (1<...=4).iter.toArray = #[2, 3, 4] := by cbv +example : (3<...=3).iter.toList = [] := by cbv +example : (0<...=5).iter.toList = [1, 2, 3, 4, 5] := by cbv + +-- Roo (open-open): a<...b +example : (1<...5).iter.toList = [2, 3, 4] := by cbv +example : (1<...5).iter.toArray = #[2, 3, 4] := by cbv +example : (3<...3).iter.toList = [] := by cbv +example : (0<...5).iter.toList = [1, 2, 3, 4] := by cbv diff --git a/tests/elab/cbv_opaque_guard.lean b/tests/elab/cbv_opaque_guard.lean index 5e0019ed94..c8ae56cabe 100644 --- a/tests/elab/cbv_opaque_guard.lean +++ b/tests/elab/cbv_opaque_guard.lean @@ -1,5 +1,3 @@ -set_option cbv.warning false - /-! Test that `@[cbv_opaque]` is respected by `reduceRecMatcher` and `reduceProj`. -/ /-! `@[cbv_opaque]` constants are not unfolded. -/ diff --git a/tests/elab/cbv_opaque_inline.lean b/tests/elab/cbv_opaque_inline.lean index d8a9249055..6e1cf5e1cb 100644 --- a/tests/elab/cbv_opaque_inline.lean +++ b/tests/elab/cbv_opaque_inline.lean @@ -1,5 +1,3 @@ -set_option cbv.warning false - /-! Test that `@[cbv_opaque]` is respected for `@[inline]` and `@[always_inline]` definitions. These are reducible, so the preprocessing stage must skip them when they are also `@[cbv_opaque]`. -/ diff --git a/tests/elab/cbv_string_split.lean b/tests/elab/cbv_string_split.lean new file mode 100644 index 0000000000..0446e9f765 --- /dev/null +++ b/tests/elab/cbv_string_split.lean @@ -0,0 +1,29 @@ +import Std + +example : ("hello world".split (· == ' ')).toList.map (·.toString) = ["hello", "world"] := by cbv + +example : ("hello world".split (· = ' ')).toList.map (·.toString) = ["hello", "world"] := by cbv + +example : ("hello world".split (' ')).toList.map (·.toString) = ["hello", "world"] := by cbv + +def numbers : List String := + ["zero", "one", "two", "three", "four", "five", "six", "seven", "eight", "nine"] + +def numberToNumber : Std.HashMap String Nat := + (0...=9).iter.fold (init := ∅) (fun sofar num => sofar.insert numbers[num]! num) + +def sortNumbers (str : String) : String := + str.split ' ' + |>.filter (!·.isEmpty) + |>.map (numberToNumber[·.copy]!) + |>.toList + |>.mergeSort + |>.map (numbers[·]!) + |> String.intercalate " " + +example : sortNumbers "" = "" := by cbv +example : sortNumbers "three" = "three" := by cbv +example : sortNumbers "three five" = "three five" := by cbv +example : sortNumbers "five three" = "three five" := by cbv +example : sortNumbers "one one" = "one one" := by cbv +example : sortNumbers "six one two" = "one two six" := by cbv