From 7632cefa8791817df6c27e0b04ee39cd45330eaf Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 14 Oct 2025 17:10:01 +0200 Subject: [PATCH] feat: hash map iterators (#10761) This PR provides iterators on hash maps. --- src/Std/Data/DHashMap.lean | 4 +- .../DHashMap/Internal/AssocList/Iterator.lean | 80 ++++++++ src/Std/Data/DHashMap/Iterator.lean | 80 ++++++++ src/Std/Data/DHashMap/IteratorLemmas.lean | 186 ++++++++++++++++++ src/Std/Data/HashMap.lean | 4 +- src/Std/Data/HashMap/Iterator.lean | 78 ++++++++ src/Std/Data/HashMap/IteratorLemmas.lean | 175 ++++++++++++++++ src/Std/Data/HashSet.lean | 2 + src/Std/Data/HashSet/Iterator.lean | 40 ++++ src/Std/Data/HashSet/IteratorLemmas.lean | 63 ++++++ src/Std/Data/Iterators/Producers/List.lean | 11 ++ .../Iterators/Producers/Monadic/List.lean | 7 + tests/lean/run/hashmap.lean | 57 ++++++ 13 files changed, 785 insertions(+), 2 deletions(-) create mode 100644 src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean create mode 100644 src/Std/Data/DHashMap/Iterator.lean create mode 100644 src/Std/Data/DHashMap/IteratorLemmas.lean create mode 100644 src/Std/Data/HashMap/Iterator.lean create mode 100644 src/Std/Data/HashMap/IteratorLemmas.lean create mode 100644 src/Std/Data/HashSet/Iterator.lean create mode 100644 src/Std/Data/HashSet/IteratorLemmas.lean diff --git a/src/Std/Data/DHashMap.lean b/src/Std/Data/DHashMap.lean index 937ca58850..03860f7588 100644 --- a/src/Std/Data/DHashMap.lean +++ b/src/Std/Data/DHashMap.lean @@ -7,5 +7,7 @@ module prelude public import Std.Data.DHashMap.Basic -public import Std.Data.DHashMap.Lemmas public import Std.Data.DHashMap.AdditionalOperations +public import Std.Data.DHashMap.Iterator +public import Std.Data.DHashMap.Lemmas +public import Std.Data.DHashMap.IteratorLemmas diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean new file mode 100644 index 0000000000..37228e85a5 --- /dev/null +++ b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +import Init.Data.Nat.Lemmas + +public import Init.Data.Iterators.Consumers +import Init.Data.Iterators.Internal.Termination + +public import Std.Data.DHashMap.Internal.AssocList.Basic + +/-! +# Iterators on associative lists +-/ + +namespace Std.DHashMap.Internal.AssocList + +open Std.Iterators + +/-- Internal implementation detail of the hash map -/ +@[ext, unbox] +public structure AssocListIterator (α : Type u) (β : α → Type v) where + l : AssocList α β + +public instance : Iterator (α := AssocListIterator α β) Id ((a : α) × β a) where + IsPlausibleStep it + | .yield it' out => it.internalState.l = .cons out.1 out.2 it'.internalState.l + | .skip _ => False + | .done => it.internalState.l = .nil + step it := pure (match it with + | ⟨⟨.nil⟩⟩ => .deflate ⟨.done, rfl⟩ + | ⟨⟨.cons k v l⟩⟩ => .deflate ⟨.yield (toIterM ⟨l⟩ Id _) ⟨k, v⟩, rfl⟩) + +def AssocListIterator.finitenessRelation : + FinitenessRelation (AssocListIterator α β) Id where + rel := InvImage WellFoundedRelation.rel (AssocListIterator.l ∘ IterM.internalState) + wf := InvImage.wf _ WellFoundedRelation.wf + subrelation {it it'} h := by + simp_wf + obtain ⟨step, h, h'⟩ := h + cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] + +public instance : Finite (AssocListIterator α β) Id := + Finite.of_finitenessRelation AssocListIterator.finitenessRelation + +public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] : + IteratorCollect (AssocListIterator α β) Id m := + .defaultImplementation + +public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] : + IteratorCollectPartial (AssocListIterator α β) Id m := + .defaultImplementation + +public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] : + IteratorLoop (AssocListIterator α β) Id m := + .defaultImplementation + +public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] : + IteratorLoopPartial (AssocListIterator α β) Id m := + .defaultImplementation + +public instance : IteratorSize (AssocListIterator α β) Id := + .defaultImplementation + +public instance : IteratorSizePartial (AssocListIterator α β) Id := + .defaultImplementation + +/-- +Internal implementation detail of the hash map. Returns a finite iterator on an associative list. +-/ +@[expose] +public def iter {α : Type u} {β : α → Type v} (l : AssocList α β) : + Iter (α := AssocListIterator α β) ((a : α) × β a) := + ⟨⟨l⟩⟩ + +end Std.DHashMap.Internal.AssocList diff --git a/src/Std/Data/DHashMap/Iterator.lean b/src/Std/Data/DHashMap/Iterator.lean new file mode 100644 index 0000000000..3e2266a0ec --- /dev/null +++ b/src/Std/Data/DHashMap/Iterator.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Std.Data.Iterators.Producers.Array +public import Init.Data.Iterators.Combinators.FlatMap +public import Std.Data.DHashMap.Basic +public import Std.Data.DHashMap.Internal.AssocList.Iterator + +/-! +# Iterators on `DHashMap` and `DHashMap.Raw` +-/ + +namespace Std.DHashMap.Raw + +/-- +Returns a finite iterator over the entries of a dependent hash map. +The iterator yields the elements of the map in order and then terminates. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def iter {α : Type u} {β : α → Type v} (m : Raw α β) := + (m.buckets.iter.flatMap fun b => b.iter : Iter ((a : α) × β a)) + +/-- +Returns a finite iterator over the keys of a dependent hash map. +The iterator yields the keys in order and then terminates. + +The key and value types must live in the same universe. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def keysIter {α : Type u} {β : α → Type u} (m : Raw α β) := + (m.iter.map fun e => e.1 : Iter α) + +/-- +Returns a finite iterator over the values of a hash map. +The iterator yields the values in order and then terminates. + +The key and value types must live in the same universe. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def valuesIter {α : Type u} {β : Type u} (m : Raw α (fun _ => β)) := + (m.iter.map fun e => e.2 : Iter β) + +end Std.DHashMap.Raw + +namespace Std.DHashMap + +@[inline, inherit_doc Raw.iter] +public def iter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : DHashMap α β) := + (m.1.iter : Iter ((a : α) × β a)) + +@[inline, inherit_doc Raw.keysIter] +public def keysIter {α : Type u} {β : α → Type u} [BEq α] [Hashable α] (m : DHashMap α β) := + (m.1.keysIter : Iter α) + +@[inline, inherit_doc Raw.valuesIter] +public def valuesIter {α : Type u} {β : Type u} [BEq α] [Hashable α] + (m : DHashMap α (fun _ => β)) := + (m.iter.map fun e => e.2 : Iter β) + +end Std.DHashMap diff --git a/src/Std/Data/DHashMap/IteratorLemmas.lean b/src/Std/Data/DHashMap/IteratorLemmas.lean new file mode 100644 index 0000000000..eee4717fad --- /dev/null +++ b/src/Std/Data/DHashMap/IteratorLemmas.lean @@ -0,0 +1,186 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Std.Data.Iterators +public import Std.Data.DHashMap.Iterator +import all Std.Data.DHashMap.Basic +import all Std.Data.DHashMap.Raw +import all Std.Data.DHashMap.Iterator +import Init.Data.Iterators.Lemmas.Combinators +import Std.Data.DHashMap.Internal.WF +import all Std.Data.DHashMap.Internal.Defs +import Std.Data.DHashMap.RawLemmas +import Std.Data.DHashMap.Lemmas + +namespace Std.DHashMap.Internal.AssocList +open Std.Iterators + +@[simp] +public theorem step_iter_nil {α : Type u} {β : α → Type v} : + ((.nil : AssocList α β).iter).step = ⟨.done, rfl⟩ := by + simp [Iter.step, IterM.step, Iterator.step, Iter.toIterM, iter] + +@[simp] +public theorem step_iter_cons {α : Type u} {β : α → Type v} {k v} {l : AssocList α β} : + ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ := by + simp [Iter.step, IterM.step, Iterator.step, Iter.toIterM, iter, toIterM, IterM.toIter] + +@[simp] +public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} : + l.iter.toList = l.toList := by + induction l + · simp [Iter.toList_eq_match_step, step_iter_nil] + · rw [Iter.toList_eq_match_step, step_iter_cons] + simp [*] + +end Std.DHashMap.Internal.AssocList + +namespace Std.DHashMap.Raw +open Std.Iterators + +section EntriesIter + +variable {α : Type u} {β : α → Type v} {m : Raw α β} + +@[simp] +public theorem toList_iter : + m.iter.toList = m.toList := by + simp [Raw.iter, Iter.toList_flatMap, Iter.toList_map, Internal.toListModel, List.flatMap, + Internal.Raw.toList_eq_toListModel] + +@[simp] +public theorem toListRev_iter : + m.iter.toListRev = m.toList.reverse := by + simp [Iter.toListRev_eq, toList_iter] + +@[simp] +public theorem toArray_iter [BEq α] [Hashable α] (h : m.WF) : + m.iter.toArray = m.toArray := by + simp [← Iter.toArray_toList, ← Raw.toArray_toList h, toList_iter] + +end EntriesIter + +section KeysIter + +variable {α : Type u} {β : α → Type u} {m : Raw α β} + +@[simp] +public theorem toList_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.keysIter.toList = m.keys := by + simp [keysIter, ← map_fst_toList_eq_keys h, toList_iter] + +@[simp] +public theorem toListRev_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.keysIter.toListRev = m.keys.reverse := by + simp [Iter.toListRev_eq, toList_keysIter h] + +@[simp] +public theorem toArray_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.keysIter.toArray = m.keysArray := by + simp [← Iter.toArray_toList, ← Raw.toArray_keys h, toList_keysIter h] + +end KeysIter + +section ValuesIter + +variable {α β : Type u} {m : Raw α (fun _ => β)} + +@[simp] +public theorem toList_valuesIter_eq_toList_map_snd : + m.valuesIter.toList = m.toList.map Sigma.snd := by + simp [valuesIter, toList_iter] + +@[simp] +public theorem toListRev_valuesIter : + m.valuesIter.toListRev = (m.toList.map Sigma.snd).reverse := by + simp [Iter.toListRev_eq, toList_valuesIter_eq_toList_map_snd] + +@[simp] +public theorem toArray_valuesIter : + m.valuesIter.toArray = (m.toList.map Sigma.snd).toArray := by + simp [← Iter.toArray_toList, toList_valuesIter_eq_toList_map_snd] + +end ValuesIter + +end Std.DHashMap.Raw + +namespace Std.DHashMap +open Std.Iterators + +section EntriesIter + +variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : DHashMap α β} + +theorem toList_inner : + m.inner.toList = m.toList := + rfl + +@[simp] +public theorem toList_iter : + m.iter.toList = m.toList := by + simp [iter, Raw.toList_iter, toList_inner] + +@[simp] +public theorem toListRev_iter : + m.iter.toListRev = m.toList.reverse := by + simp [Iter.toListRev_eq, toList_iter] + +@[simp] +public theorem toArray_iter : + m.iter.toArray = m.toArray := by + simp [← Iter.toArray_toList, ← toArray_toList, toList_iter] + +end EntriesIter + +section KeysIter + +variable {α : Type u} {β : α → Type u} [BEq α] [Hashable α] {m : DHashMap α β} + +theorem keys_inner : + m.inner.keys = m.keys := + rfl + +@[simp] +public theorem toList_keysIter [EquivBEq α] [LawfulHashable α] : + m.keysIter.toList = m.keys := by + simp [keysIter, Raw.toList_keysIter m.wf, keys_inner] + +@[simp] +public theorem toListRev_keysIter [EquivBEq α] [LawfulHashable α] : + m.keysIter.toListRev = m.keys.reverse := by + simp [Iter.toListRev_eq, toList_keysIter] + +@[simp] +public theorem toArray_keysIter [EquivBEq α] [LawfulHashable α] : + m.keysIter.toArray = m.keysArray := by + simp [← Iter.toArray_toList, ← toArray_keys, toList_keysIter] + +end KeysIter + +section ValuesIter + +variable {α : Type u} {β : Type u} [BEq α] [Hashable α] {m : DHashMap α (fun _ => β)} + +@[simp] +public theorem toList_valuesIter_eq_toList_map_snd : + m.valuesIter.toList = m.toList.map Sigma.snd := by + simp [valuesIter, toList_iter] + +@[simp] +public theorem toListRev_valuesIter : + m.valuesIter.toListRev = (m.toList.map Sigma.snd).reverse := by + simp [Iter.toListRev_eq, toList_valuesIter_eq_toList_map_snd] + +@[simp] +public theorem toArray_valuesIter : + m.valuesIter.toArray = (m.toList.map Sigma.snd).toArray := by + simp [← Iter.toArray_toList, toList_valuesIter_eq_toList_map_snd] + +end ValuesIter + +end Std.DHashMap diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index f86b6bfe18..02b56e2ec6 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -7,5 +7,7 @@ module prelude public import Std.Data.HashMap.Basic -public import Std.Data.HashMap.Lemmas public import Std.Data.HashMap.AdditionalOperations +public import Std.Data.HashMap.Iterator +public import Std.Data.HashMap.Lemmas +public import Std.Data.HashMap.IteratorLemmas diff --git a/src/Std/Data/HashMap/Iterator.lean b/src/Std/Data/HashMap/Iterator.lean new file mode 100644 index 0000000000..7222732e72 --- /dev/null +++ b/src/Std/Data/HashMap/Iterator.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Std.Data.DHashMap.Iterator +public import Std.Data.HashMap.Basic +public import Std.Data.HashMap.Raw + +/-! +# Iterators on `HashMap` and `HashMap.Raw` +-/ + +namespace Std.HashMap.Raw + +/-- +Returns a finite iterator over the entries of a hash map. +The iterator yields the elements of the map in order and then terminates. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def iter {α : Type u} {β : Type v} (m : Raw α β) := + (m.inner.iter.map fun e => (e.1, e.2) : Iter (α × β)) + +/-- +Returns a finite iterator over the keys of a hash map. +The iterator yields the keys in order and then terminates. + +The key and value types must live in the same universe. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def keysIter {α : Type u} {β : Type u} (m : Raw α β) := + (m.inner.keysIter : Iter α) + +/-- +Returns a finite iterator over the values of a hash map. +The iterator yields the values in order and then terminates. + +The key and value types must live in the same universe. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def valuesIter {α : Type u} {β : Type u} (m : Raw α β) := + (m.inner.valuesIter : Iter β) + +end Std.HashMap.Raw + +namespace Std.HashMap + +@[inline, inherit_doc Raw.iter] +public def iter {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : HashMap α β) := + (m.inner.iter.map fun e => (e.1, e.2) : Iter (α × β)) + +@[inline, inherit_doc Raw.iter] +public def keysIter {α : Type u} {β : Type u} [BEq α] [Hashable α] (m : HashMap α β) := + (m.1.keysIter : Iter α) + +@[inline, inherit_doc Raw.iter] +public def valuesIter {α : Type u} {β : Type u} [BEq α] [Hashable α] (m : HashMap α β) := + (m.inner.valuesIter : Iter β) + +end Std.HashMap diff --git a/src/Std/Data/HashMap/IteratorLemmas.lean b/src/Std/Data/HashMap/IteratorLemmas.lean new file mode 100644 index 0000000000..ca2296d84c --- /dev/null +++ b/src/Std/Data/HashMap/IteratorLemmas.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +import Init.Data.Iterators.Lemmas.Combinators + +import Std.Data.DHashMap.IteratorLemmas +public import Std.Data.HashMap.Iterator +import all Std.Data.HashMap.Iterator +import Std.Data.HashMap.RawLemmas +import Std.Data.HashMap.Lemmas +import Std.Data.DHashMap.Internal.WF +import all Std.Data.DHashMap.Basic + +namespace Std.HashMap.Raw +open Std.Iterators + +section EntriesIter + +variable {α : Type u} {β : Type v} {m : Raw α β} + +theorem toList_inner : + m.inner.toList = m.toList.map fun e => ⟨e.1, e.2⟩ := by + simp [toList, DHashMap.Internal.Raw.Const.toList_eq_toListModel_map, + ← DHashMap.Internal.Raw.toList_eq_toListModel, Function.comp_def] + +@[simp] +public theorem toList_iter : + m.iter.toList = m.toList := by + simp [Raw.iter, Iter.toList_map, DHashMap.Raw.toList_iter, toList_inner, + Function.comp_def] + +@[simp] +public theorem toListRev_iter : + m.iter.toListRev = m.toList.reverse := by + simp [Iter.toListRev_eq, toList_iter] + +@[simp] +public theorem toArray_iter [BEq α] [Hashable α] (h : m.WF) : + m.iter.toArray = m.toArray := by + simp [← Iter.toArray_toList, ← Raw.toArray_toList h, toList_iter] + +end EntriesIter + +section KeysIter + +variable {α β : Type u} {m : Raw α β} + +theorem keys_inner : + m.inner.keys = m.keys := + rfl + +@[simp] +public theorem toList_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.keysIter.toList = m.keys := by + simp only [keysIter, ← map_fst_toList_eq_keys h, DHashMap.Raw.toList_keysIter h.out] + simp [HashMap.Raw.map_fst_toList_eq_keys h, keys_inner] + +@[simp] +public theorem toListRev_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.keysIter.toListRev = m.keys.reverse := by + simp [Iter.toListRev_eq, toList_keysIter h] + +@[simp] +public theorem toArray_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.keysIter.toArray = m.keysArray := by + simp [← Iter.toArray_toList, ← Raw.toArray_keys h, toList_keysIter h] + +end KeysIter + +section ValuesIter + +variable {α β : Type u} {m : Raw α β} + +@[simp] +public theorem toList_valuesIter_eq_toList_map_snd : + m.valuesIter.toList = m.toList.map Prod.snd := by + simp [valuesIter, DHashMap.Raw.toList_valuesIter_eq_toList_map_snd, + DHashMap.Internal.Raw.toList_eq_toListModel, toList, + DHashMap.Internal.Raw.Const.toList_eq_toListModel_map] + +@[simp] +public theorem toListRev_valuesIter : + m.valuesIter.toListRev = (m.toList.map Prod.snd).reverse := by + simp [Iter.toListRev_eq, toList_valuesIter_eq_toList_map_snd] + +@[simp] +public theorem toArray_valuesIter : + m.valuesIter.toArray = (m.toList.map Prod.snd).toArray := by + simp [← Iter.toArray_toList, toList_valuesIter_eq_toList_map_snd] + +end ValuesIter + +end Std.HashMap.Raw + +namespace Std.HashMap +open Std.Iterators + +section EntriesIter + +variable {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : HashMap α β} + +theorem toList_inner : + m.inner.toList = m.toList.map fun e => ⟨e.1, e.2⟩ := by + simp [toList, DHashMap.Const.toList, DHashMap.Internal.Raw.Const.toList_eq_toListModel_map, + Function.comp_def, DHashMap.toList, DHashMap.Internal.Raw.toList_eq_toListModel] + +@[simp] +public theorem toList_iter : + m.iter.toList = m.toList := by + simp [iter, DHashMap.toList_iter, toList_inner, Function.comp_def] + +@[simp] +public theorem toListRev_iter : + m.iter.toListRev = m.toList.reverse := by + simp [Iter.toListRev_eq, toList_iter] + +@[simp] +public theorem toArray_iter : + m.iter.toArray = m.toArray := by + simp [← Iter.toArray_toList, toList_iter] + +end EntriesIter + +section KeysIter + +theorem keys_inner {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : HashMap α β} : + m.inner.keys = m.keys := + rfl + +variable {α : Type u} {β : Type u} [BEq α] [Hashable α] {m : HashMap α β} + +@[simp] +public theorem toList_keysIter [EquivBEq α] [LawfulHashable α] : + m.keysIter.toList = m.keys := by + simp [keysIter, DHashMap.toList_keysIter, keys_inner] + +@[simp] +public theorem toListRev_keysIter [EquivBEq α] [LawfulHashable α] : + m.keysIter.toListRev = m.keys.reverse := by + simp [keysIter, DHashMap.toListRev_keysIter, keys_inner] + +@[simp] +public theorem toArray_keysIter [EquivBEq α] [LawfulHashable α] : + m.keysIter.toArray = m.keysArray := by + simp [← Iter.toArray_toList, keysIter, keysArray, DHashMap.toList_keysIter] + +end KeysIter + +section ValuesIter + +variable {α : Type u} {β : Type u} [BEq α] [Hashable α] {m : HashMap α β} + +@[simp] +public theorem toList_valuesIter_eq_toList_map_snd : + m.valuesIter.toList = m.toList.map Prod.snd := by + simp [valuesIter, DHashMap.toList_valuesIter_eq_toList_map_snd, toList_inner] + +@[simp] +public theorem toListRev_valuesIter : + m.valuesIter.toListRev = (m.toList.map Prod.snd).reverse := by + simp [Iter.toListRev_eq, toList_valuesIter_eq_toList_map_snd] + +@[simp] +public theorem toArray_valuesIter : + m.valuesIter.toArray = (m.toList.map Prod.snd).toArray := by + simp [← Iter.toArray_toList, toList_valuesIter_eq_toList_map_snd] + +end ValuesIter + +end Std.HashMap diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index 0e404fbc3d..c81d347fee 100644 --- a/src/Std/Data/HashSet.lean +++ b/src/Std/Data/HashSet.lean @@ -7,4 +7,6 @@ module prelude public import Std.Data.HashSet.Basic +public import Std.Data.HashSet.Iterator public import Std.Data.HashSet.Lemmas +public import Std.Data.HashSet.IteratorLemmas diff --git a/src/Std/Data/HashSet/Iterator.lean b/src/Std/Data/HashSet/Iterator.lean new file mode 100644 index 0000000000..86686492c0 --- /dev/null +++ b/src/Std/Data/HashSet/Iterator.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Std.Data.HashMap.Iterator +public import Std.Data.HashSet.Basic +public import Std.Data.HashSet.Raw + +/-! +# Iterators on `HashSet` and `HashSet.Raw` +-/ + +namespace Std.HashSet.Raw + +/-- +Returns a finite iterator over the elements of a hash set. +The iterator yields the elements of the set in order and then terminates. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ +@[inline] +public def iter {α : Type u} (m : Raw α) := + (m.inner.inner.iter.map fun e => e.1 : Iter α) + +end Std.HashSet.Raw + +namespace Std.HashSet + +@[inline, inherit_doc Raw.iter] +public def iter {α : Type u} [BEq α] [Hashable α] (m : HashSet α) := + (m.inner.inner.iter.map fun e => e.1 : Iter α) + +end Std.HashSet diff --git a/src/Std/Data/HashSet/IteratorLemmas.lean b/src/Std/Data/HashSet/IteratorLemmas.lean new file mode 100644 index 0000000000..988601c448 --- /dev/null +++ b/src/Std/Data/HashSet/IteratorLemmas.lean @@ -0,0 +1,63 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +import Init.Data.Iterators.Lemmas.Combinators + +import Std.Data.DHashMap.IteratorLemmas +import all Std.Data.HashMap.IteratorLemmas +public import Std.Data.HashSet.Iterator +import all Std.Data.HashSet.Iterator +import Std.Data.HashSet.RawLemmas +import Std.Data.HashSet.Lemmas +import Std.Data.DHashMap.Internal.WF +import all Std.Data.DHashMap.Basic + +namespace Std.HashSet.Raw +open Std.Iterators + +variable {α : Type u} {m : Raw α} + +@[simp] +public theorem toList_iter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.iter.toList = m.toList := by + simp [toList, iter, DHashMap.Raw.toList_iter, + ← HashMap.Raw.map_fst_toList_eq_keys h.out, HashMap.Raw.toList_inner] + +@[simp] +public theorem toListRev_iter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.iter.toListRev = m.toList.reverse := by + simp [Iter.toListRev_eq, toList_iter h] + +@[simp] +public theorem toArray_iter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.iter.toArray = m.toArray := by + simp [← Iter.toArray_toList, ← Raw.toArray_toList h, toList_iter h] + +end Std.HashSet.Raw + +namespace Std.HashSet +open Std.Iterators + +variable {α : Type u} [BEq α] [Hashable α] {m : HashSet α} + +@[simp] +public theorem toList_iter [EquivBEq α] [LawfulHashable α] : + m.iter.toList = m.toList := by + simp [iter, DHashMap.toList_iter, toList, HashMap.keys_inner] + +@[simp] +public theorem toListRev_iter [EquivBEq α] [LawfulHashable α] : + m.iter.toListRev = m.toList.reverse := by + simp [iter, DHashMap.toListRev_iter, toList, HashMap.keys_inner] + +@[simp] +public theorem toArray_iter [EquivBEq α] [LawfulHashable α] : + m.iter.toArray = m.toArray := by + simp [iter, DHashMap.toArray_iter, toArray, HashMap.keysArray] + +end Std.HashSet diff --git a/src/Std/Data/Iterators/Producers/List.lean b/src/Std/Data/Iterators/Producers/List.lean index c3c69e86b8..ca53fcafad 100644 --- a/src/Std/Data/Iterators/Producers/List.lean +++ b/src/Std/Data/Iterators/Producers/List.lean @@ -18,6 +18,17 @@ This module provides an iterator for lists that is accessible via `List.iter`. namespace Std.Iterators +/-- +Returns a finite iterator for the given list. +The iterator yields the elements of the list in order and then terminates. + +The monadic version of this iterator is `List.iterM`. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always +-/ @[always_inline, inline] def _root_.List.iter {α : Type w} (l : List α) : Iter (α := ListIterator α) α := diff --git a/src/Std/Data/Iterators/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Producers/Monadic/List.lean index c2d1733249..5ee9ff2b43 100644 --- a/src/Std/Data/Iterators/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Producers/Monadic/List.lean @@ -34,6 +34,13 @@ structure ListIterator (α : Type w) where /-- Returns a finite iterator for the given list. The iterator yields the elements of the list in order and then terminates. + +The non-monadic version of this iterator is `List.iter`. + +**Termination properties:** + +* `Finite` instance: always +* `Productive` instance: always -/ @[always_inline, inline] def _root_.List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] : diff --git a/tests/lean/run/hashmap.lean b/tests/lean/run/hashmap.lean index b0eefff15c..1b2890f351 100644 --- a/tests/lean/run/hashmap.lean +++ b/tests/lean/run/hashmap.lean @@ -1,6 +1,7 @@ import Std.Data.HashSet.Basic import Std.Data.HashSet.Raw import Std.Data.HashMap.AdditionalOperations +import Std.Data.HashSet.Iterator open Std @@ -58,6 +59,10 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray +/-- info: #[⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ +#guard_msgs in +#eval m.iter.toArray + /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DHashMap.Raw.Const.toList m @@ -74,10 +79,18 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray +/-- info: #[1, 2, 3] -/ +#guard_msgs in +#eval m.keysIter.toArray + /-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values +/-- info: #[2, 4, 6] -/ +#guard_msgs in +#eval m.valuesIter.toArray + /-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (m.insertMany [⟨16, 8⟩, ⟨16, 9⟩]).toList @@ -148,6 +161,10 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray +/-- info: #[⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ +#guard_msgs in +#eval m.iter.toArray + /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DHashMap.Const.toList m @@ -164,10 +181,18 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray +/-- info: #[1, 2, 3] -/ +#guard_msgs in +#eval m.keysIter.toArray + /-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values +/-- info: #[2, 4, 6] -/ +#guard_msgs in +#eval m.valuesIter.toArray + /-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (m.insertMany [⟨16, 8⟩, ⟨16, 9⟩]).toList @@ -238,6 +263,10 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray +/-- info: #[(1, 2), (2, 4), (3, 6)] -/ +#guard_msgs in +#eval m.iter.toArray + /-- info: [1, 2, 3] -/ #guard_msgs in #eval m.keys @@ -246,10 +275,18 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray +/-- info: #[1, 2, 3] -/ +#guard_msgs in +#eval m.keysIter.toArray + /-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values +/-- info: #[2, 4, 6] -/ +#guard_msgs in +#eval m.valuesIter.toArray + /-- info: [(16, 9), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval (m.insertMany [(16, 8), (16, 9)]).toList @@ -312,6 +349,10 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray +/-- info: #[(1, 2), (2, 4), (3, 6)] -/ +#guard_msgs in +#eval m.iter.toArray + /-- info: [1, 2, 3] -/ #guard_msgs in #eval m.keys @@ -320,10 +361,18 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray +/-- info: #[1, 2, 3] -/ +#guard_msgs in +#eval m.keysIter.toArray + /-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values +/-- info: #[2, 4, 6] -/ +#guard_msgs in +#eval m.valuesIter.toArray + /-- info: [(16, 9), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval (m.insertMany [(16, 8), (16, 9)]).toList @@ -426,6 +475,10 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray +/-- info: #[1, 2, 1000000000] -/ +#guard_msgs in +#eval m.iter.toArray + /-- info: Std.HashSet.Raw.ofList [16, 1, 2, 1000000000] -/ #guard_msgs in #eval m ∪ {16, 16} @@ -500,6 +553,10 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray +/-- info: #[1, 2, 1000000000] -/ +#guard_msgs in +#eval m.iter.toArray + /-- info: Std.HashSet.ofList [16, 1, 2, 1000000000] -/ #guard_msgs in #eval m ∪ {16, 16}