From b39ee8a84b07b9ead8e2d7ed3fb2b7854976d755 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Wed, 12 Nov 2025 16:56:28 +0000 Subject: [PATCH] feat: add minimal support for `getEntry`/`getEntry?`/`getEntry!`/`getEntryD` for DHashMap (#11076) This PR adds `getEntry`/`getEntry?`/`getEntry!`/`getEntryD` operation on DHashMap. --- src/Std/Data/DHashMap/Basic.lean | 12 ++ .../DHashMap/Internal/AssocList/Basic.lean | 21 +++ .../DHashMap/Internal/AssocList/Lemmas.lean | 32 +++++ src/Std/Data/DHashMap/Internal/Defs.lean | 28 ++++ src/Std/Data/DHashMap/Internal/Model.lean | 28 ++++ src/Std/Data/DHashMap/Internal/RawLemmas.lean | 12 +- src/Std/Data/DHashMap/Internal/WF.lean | 40 ++++++ src/Std/Data/DHashMap/Raw.lean | 35 +++++ src/Std/Data/Internal/List/Associative.lean | 127 ++++++++++++++++++ 9 files changed, 331 insertions(+), 4 deletions(-) diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index d2773860ca..ae1e26b0dd 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -190,6 +190,18 @@ end @[inline, inherit_doc Raw.getKeyD] def getKeyD (m : DHashMap α β) (a : α) (fallback : α) : α := Raw₀.getKeyD ⟨m.1, m.2.size_buckets_pos⟩ a fallback +@[inline, inherit_doc Raw.getEntry?] def getEntry? (m : DHashMap α β) (a : α) : Option ((a : α) × β a) := + Raw₀.getEntry? ⟨m.1, m.2.size_buckets_pos⟩ a + +@[inline, inherit_doc Raw.getEntry] def getEntry (m : DHashMap α β) (a : α) (h : a ∈ m) : (a : α) × β a := + Raw₀.getEntry ⟨m.1, m.2.size_buckets_pos⟩ a h + +@[inline, inherit_doc Raw.getEntry!] def getEntry! [Inhabited ((a : α) × β a)] (m : DHashMap α β) (a : α) : (a : α) × β a := + Raw₀.getEntry! ⟨m.1, m.2.size_buckets_pos⟩ a + +@[inline, inherit_doc Raw.getEntryD] def getEntryD (m : DHashMap α β) (a : α) (fallback : (a : α) × β a) : (a : α) × β a := + Raw₀.getEntryD ⟨m.1, m.2.size_buckets_pos⟩ a fallback + @[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat := m.1.size diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean index 5f400d6794..8bc28c0deb 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean @@ -107,6 +107,12 @@ def getCast? [BEq α] [LawfulBEq α] (a : α) : AssocList α β → Option (β a | cons k v es => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else es.getCast? a +/-- Internal implementation detail of the hash map -/ +def getEntry? [BEq α] (a : α) : (l : AssocList α β) → Option ((a : α) × β a) + | nil => none + | cons k v es => if k == a then some ⟨k, v⟩ + else es.getEntry? a + /-- Internal implementation detail of the hash map -/ def contains [BEq α] (a : α) : AssocList α β → Bool | nil => false @@ -122,6 +128,21 @@ def getCast [BEq α] [LawfulBEq α] (a : α) : (l : AssocList α β) → l.conta | cons k v es, h => if hka : k == a then cast (congrArg β (eq_of_beq hka)) v else es.getCast a (by rw [← h, contains, Bool.of_not_eq_true hka, Bool.false_or]) +/-- Internal implementation detail of the hash map -/ +def getEntry [BEq α] (a : α) : (l : AssocList α β) → l.contains a → (a : α) × β a + | cons k v es, h => if hka : k == a then ⟨k, v⟩ + else es.getEntry a (by rw [← h, contains, Bool.of_not_eq_true hka, Bool.false_or]) + +/-- Internal implementation detail of the hash map -/ +def getEntryD [BEq α] (a : α) (fallback : (a : α) × β a) : AssocList α β → (a : α) × β a + | nil => fallback + | cons k v es => if k == a then ⟨k, v⟩ else es.getEntryD a fallback + +/-- Internal implementation detail of the hash map -/ +def getEntry! [BEq α] (a : α) [Inhabited ((a : α) × β a)] : AssocList α β → (a : α) × β a + | nil => default + | cons k v es => if k == a then ⟨k, v⟩ else es.getEntry! a + /-- Internal implementation detail of the hash map -/ def getKey [BEq α] (a : α) : (l : AssocList α β) → l.contains a → α | cons k _ es, h => if hka : k == a then k diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index ec5a160fb1..e9c08935cd 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -82,6 +82,38 @@ theorem get_eq {β : Type v} [BEq α] {l : AssocList α (fun _ => β)} {a : α} · simp [contains] at h next k v t ih => simp only [get, toList_cons, List.getValue_cons, ih] +@[simp] +theorem getEntry_eq [BEq α] {l : AssocList α β} {a : α} {h} : + l.getEntry a h = List.getEntry a l.toList (contains_eq.symm.trans h) := by + induction l + · simp [contains] at h + next k v t ih => + simp only [getEntry, toList_cons, List.getEntry_cons, ih] + +@[simp] +theorem getEntry?_eq [BEq α] {l : AssocList α β} {a : α} : + l.getEntry? a = List.getEntry? a l.toList := by + induction l + · simp only [getEntry?, toList_nil, getEntry?_nil] + next k v t ih => + simp only [getEntry?, ih, toList_cons, getEntry?_cons, Bool.ite_eq_cond_iff] + +@[simp] +theorem getEntryD_eq [BEq α] {l : AssocList α β} {a : α} {fallback : (a : α) × β a} : + l.getEntryD a fallback = List.getEntryD a fallback l.toList := by + induction l + · simp only [getEntryD, toList_nil, getEntryD_nil] + next k v t ih => + simp only [getEntryD, ih, toList_cons, getEntryD_cons, Bool.ite_eq_cond_iff] + +@[simp] +theorem getEntry!_eq [BEq α] {l : AssocList α β} {a : α} [Inhabited ((a : α) × β a)] : + l.getEntry! a = List.getEntry! a l.toList := by + induction l + · simp only [getEntry!, toList_nil, getEntry!_nil] + next k v t ih => + simp only [getEntry!, ih, toList_cons, List.getEntry!_cons, Bool.ite_eq_cond_iff] + @[simp] theorem getCastD_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {fallback : β a} : l.getCastD a fallback = getValueCastD a l.toList fallback := by diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index 4b197702ce..b776bfc730 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -368,6 +368,34 @@ def get [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (hma : let idx := mkIdx buckets.size h (hash a) buckets[idx.1].getCast a hma +/-- Internal implementation detail of the hash map -/ +def getEntry [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (hma : m.contains a) : + (a : α) × β a := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getEntry a hma + +/-- Internal implementation detail of the hash map -/ +def getEntry? [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : + Option ((a : α) × β a) := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getEntry? a + +/-- Internal implementation detail of the hash map -/ +def getEntryD [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : (a : α) × β a) : + (a : α) × β a := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getEntryD a fallback + +/-- Internal implementation detail of the hash map -/ +def getEntry! [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) [Inhabited ((a : α) × β a)] : + (a : α) × β a := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getEntry! a + /-- Internal implementation detail of the hash map -/ def getD [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : β a) : β a := diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index de50c3d65a..5237e19a4d 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -294,6 +294,22 @@ def containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Bool := def getₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.containsₘ a) : β a := (bucket m.1.buckets m.2 a).getCast a h +/-- Internal implementation detail of the hash map -/ +def getEntryₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.containsₘ a) : (a : α) × β a := + (bucket m.1.buckets m.2 a).getEntry a h + +/-- Internal implementation detail of the hash map -/ +def getEntry?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option ((a : α) × β a) := + (bucket m.1.buckets m.2 a).getEntry? a + +/-- Internal implementation detail of the hash map -/ +def getEntryDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : (a : α) × β a) : (a : α) × β a := + (bucket m.1.buckets m.2 a).getEntryD a fallback + +/-- Internal implementation detail of the hash map -/ +def getEntry!ₘ [BEq α] [Hashable α] [Inhabited ((a : α) × β a)] (m : Raw₀ α β) (a : α) : (a : α) × β a := + (bucket m.1.buckets m.2 a).getEntry! a + /-- Internal implementation detail of the hash map -/ def getDₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : β a) : β a := (m.get?ₘ a).getD fallback @@ -452,6 +468,18 @@ theorem get?_eq_get?ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) theorem get_eq_getₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.contains a) : get m a h = getₘ m a (by exact h) := (rfl) +theorem getEntry_eq_getEntryₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.contains a) : + getEntry m a h = getEntryₘ m a (by exact h) := (rfl) + +theorem getEntry?_eq_getEntry?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : + getEntry? m a = getEntry?ₘ m a := (rfl) + +theorem getEntryD_eq_getEntryDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : (a : α) × β a) : + getEntryD m a fallback = getEntryDₘ m a fallback := (rfl) + +theorem getEntry!_eq_getEntry!ₘ [BEq α] [Hashable α] [Inhabited ((a : α) × β a)] (m : Raw₀ α β) (a : α) : + getEntry! m a = getEntry!ₘ m a := (rfl) + theorem getD_eq_getDₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : β a) : getD m a fallback = getDₘ m a fallback := by simp [getD, getDₘ, get?ₘ, List.getValueCastD_eq_getValueCast?, bucket] diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 91ff297a9a..0e1dca4ca2 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -140,6 +140,10 @@ private meta def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (T ⟨`getKey, (``getKey_eq_getKey, #[`(getKey_of_perm _)])⟩, ⟨`getKeyD, (``getKeyD_eq_getKeyD, #[`(getKeyD_of_perm _)])⟩, ⟨`getKey!, (``getKey!_eq_getKey!, #[`(getKey!_of_perm _)])⟩, + ⟨`getEntry, (``getEntry_eq_getEntry, #[`(getEntry_of_perm _)])⟩, + ⟨`getEntry?, (``getEntry?_eq_getEntry?, #[`(getEntry?_of_perm _)])⟩, + ⟨`getEntryD, (``getEntryD_eq_getEntryD, #[`(getEntryD_of_perm _)])⟩, + ⟨`getEntry!, (``getEntry!_eq_getEntry!, #[`(getEntry!_of_perm _)])⟩, ⟨`toList, (``Raw.toList_eq_toListModel, #[])⟩, ⟨`keys, (``Raw.keys_eq_keys_toListModel, #[`(perm_keys_congr_left)])⟩, ⟨`Const.toList, (``Raw.Const.toList_eq_toListModel_map, #[`(perm_map_congr_left)])⟩, @@ -2424,7 +2428,7 @@ theorem union_equiv_congr_left {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashab (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₁.1.Equiv m₂.1) : (m₁.union m₃).1.Equiv (m₂.union m₃).1 := by revert equiv - simp_to_model [union] + simp_to_model [Equiv, union] intro equiv apply List.insertList_perm_of_perm_first equiv wf_trivial @@ -2433,7 +2437,7 @@ theorem union_equiv_congr_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHasha (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₂.1.Equiv m₃.1) : (m₁.union m₂).1.Equiv (m₁.union m₃).1 := by revert equiv - simp_to_model [union] + simp_to_model [Equiv, union] intro equiv apply @List.insertList_perm_of_perm_second _ _ _ _ (toListModel m₂.val.buckets) (toListModel m₃.val.buckets) (toListModel m₁.val.buckets) equiv all_goals wf_trivial @@ -2441,10 +2445,10 @@ theorem union_equiv_congr_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHasha theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : (m₁.union (m₂.insert p.fst p.snd)).1.Equiv ((m₁.union m₂).insert p.fst p.snd).1 := by - simp_to_model [union, insert] + simp_to_model [Equiv, union, insert] apply List.Perm.trans . apply insertList_perm_of_perm_second - simp_to_model [insert] + simp_to_model [Equiv, insert] . apply insertEntry_of_perm . wf_trivial . apply List.Perm.refl diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index eefc861de9..57b8293e9a 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -405,11 +405,51 @@ theorem getₘ_eq_getValue [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α apply_bucket_with_proof hm a AssocList.getCast List.getValueCast AssocList.getCast_eq List.getValueCast_of_perm List.getValueCast_append_of_containsKey_eq_false +theorem getEntryₘ_eq_getEntry [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} {h : m.containsₘ a} : + m.getEntryₘ a h = List.getEntry a (toListModel m.1.buckets) (containsₘ_eq_containsKey hm ▸ h) := + apply_bucket_with_proof hm a AssocList.getEntry List.getEntry AssocList.getEntry_eq getEntry_of_perm getEntry_append_of_containsKey_eq_false + +theorem getEntry?ₘ_eq_getEntry? [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} : + m.getEntry?ₘ a = List.getEntry? a (toListModel m.1.buckets) := + apply_bucket hm AssocList.getEntry?_eq getEntry?_of_perm getEntry?_append_of_containsKey_eq_false + theorem get_eq_getValueCast [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} : m.get a h = getValueCast a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by rw [get_eq_getₘ, getₘ_eq_getValue hm] +theorem getEntry_eq_getEntry [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} {h : m.contains a} : + m.getEntry a h = List.getEntry a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by + rw [getEntry_eq_getEntryₘ, getEntryₘ_eq_getEntry hm] + +theorem getEntry?_eq_getEntry? [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} : + m.getEntry? a = List.getEntry? a (toListModel m.1.buckets) := by + rw [getEntry?_eq_getEntry?ₘ, getEntry?ₘ_eq_getEntry? hm] + +theorem getEntryDₘ_eq_getEntryD [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} {fallback : (a : α) × β a} : + m.getEntryDₘ a fallback = List.getEntryD a fallback (toListModel m.1.buckets) := + apply_bucket hm AssocList.getEntryD_eq getEntryD_of_perm getEntryD_append_of_containsKey_eq_false + +theorem getEntryD_eq_getEntryD [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} {fallback : (a : α) × β a} : + m.getEntryD a fallback = List.getEntryD a fallback (toListModel m.1.buckets) := by + rw [getEntryD_eq_getEntryDₘ, getEntryDₘ_eq_getEntryD hm] + +theorem getEntry!ₘ_eq_getEntry! [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} [Inhabited ((a : α) × β a)] : + m.getEntry!ₘ a = List.getEntry! a (toListModel m.1.buckets) := + apply_bucket hm AssocList.getEntry!_eq getEntry!_of_perm getEntry!_append_of_containsKey_eq_false + +theorem getEntry!_eq_getEntry! [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) + {a : α} [Inhabited ((a : α) × β a)] : + m.getEntry! a = List.getEntry! a (toListModel m.1.buckets) := by + rw [getEntry!_eq_getEntry!ₘ, getEntry!ₘ_eq_getEntry! hm] + theorem get!ₘ_eq_getValueCast! [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} [Inhabited (β a)] : m.get!ₘ a = getValueCast! a (toListModel m.1.buckets) := by diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 61dbea8ba5..31fa346d8a 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -300,6 +300,41 @@ If no panic occurs the result is guaranteed to be pointer equal to the key in th Raw₀.getKey! ⟨m, h⟩ a else default -- will never happen for well-formed inputs +/-- +Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `none`. +The key in the returned pair will be `BEq` to the input `a`. +-/ +@[inline] def getEntry? [BEq α] [Hashable α] (m : Raw α β) (a : α) : Option ((a : α) × β a) := + if h : 0 < m.buckets.size then + Raw₀.getEntry? ⟨m, h⟩ a + else none -- will never happen for well-formed inputs + +/-- +Retrieves the key-value pair, whose key matches `a`. Ensures that such a mapping exists by +requiring a proof of `a ∈ m`. The key in the returned pair will be `BEq` to the input `a`. +-/ +@[inline] def getEntry [BEq α] [Hashable α] (m : Raw α β) (a : α) (h : a ∈ m) : (a : α) × β a := + Raw₀.getEntry ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a + (by change dite .. = true at h; split at h <;> simp_all) + +/-- +Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `fallback`. +The key in the returned pair will be `BEq` to the input `a`. +-/ +@[inline] def getEntryD [BEq α] [Hashable α] (m : Raw α β) (a : α) (fallback : (a : α) × β a) : (a : α) × β a := + if h : 0 < m.buckets.size then + Raw₀.getEntryD ⟨m, h⟩ a fallback + else fallback -- will never happen for well-formed inputs + +/-- +Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise panics. +The key in the returned pair will be `BEq` to the input `a`. +-/ +@[inline] def getEntry! [BEq α] [Hashable α] [Inhabited ((a : α) × β a)] (m : Raw α β) (a : α) : (a : α) × β a := + if h : 0 < m.buckets.size then + Raw₀.getEntry! ⟨m, h⟩ a + else default -- will never happen for well-formed inputs + /-- Returns `true` if the hash map contains no mappings. diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 549a8eecb9..c0e3e75aba 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -49,8 +49,25 @@ def getEntry? [BEq α] (a : α) : List ((a : α) × β a) → Option ((a : α) | [] => none | ⟨k, v⟩ :: l => bif k == a then some ⟨k, v⟩ else getEntry? a l +/-- Internal implementation detail of the hash map -/ +def getEntryD [BEq α] (a : α) (fallback : (a : α) × β a) : List ((a : α) × β a) → (a : α) × β a + | [] => fallback + | ⟨k, v⟩ :: l => bif k == a then ⟨k, v⟩ else getEntryD a fallback l + +/-- Internal implementation detail of the hash map -/ +def getEntry! [BEq α] (a : α) [Inhabited ((a : α) × β a)] : List ((a : α) × β a) → (a : α) × β a + | [] => panic! "key is not present in associative list" + | ⟨k, v⟩ :: l => bif k == a then ⟨k, v⟩ else getEntry! a l + @[simp] theorem getEntry?_nil [BEq α] {a : α} : getEntry? a ([] : List ((a : α) × β a)) = none := (rfl) + +@[simp] theorem getEntryD_nil [BEq α] {a : α} (fallback : (a : α) × β a) : + getEntryD a fallback ([] : List ((a : α) × β a)) = fallback := (rfl) + +@[simp] theorem getEntry!_nil [BEq α] {a : α} [Inhabited ((a : α) × β a)] : + getEntry! a ([] : List ((a : α) × β a)) = default := (rfl) + theorem getEntry?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := (rfl) @@ -73,6 +90,38 @@ theorem getEntry?_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} getEntry? k (⟨k, v⟩ :: l) = some ⟨k, v⟩ := getEntry?_cons_of_true BEq.rfl +theorem getEntryD_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {fallback : (a : α) × β a} : + getEntryD a fallback (⟨k, v⟩ :: l) = bif k == a then ⟨k, v⟩ else getEntryD a fallback l := (rfl) + +theorem getEntryD_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {fallback : (a : α) × β a} + (h : k == a) : getEntryD a fallback (⟨k, v⟩ :: l) = ⟨k, v⟩ := by + simp [getEntryD, h] + +theorem getEntryD_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {fallback : (a : α) × β a} + (h : (k == a) = false) : getEntryD a fallback (⟨k, v⟩ :: l) = getEntryD a fallback l := by + simp [getEntryD, h] + +@[simp] +theorem getEntryD_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} {fallback : (a : α) × β a} : + getEntryD k fallback (⟨k, v⟩ :: l) = ⟨k, v⟩ := + getEntryD_cons_of_true BEq.rfl + +theorem getEntry!_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} [Inhabited ((a : α) × β a)] : + getEntry! a (⟨k, v⟩ :: l) = bif k == a then ⟨k, v⟩ else getEntry! a l := (rfl) + +theorem getEntry!_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} [Inhabited ((a : α) × β a)] + (h : k == a) : getEntry! a (⟨k, v⟩ :: l) = ⟨k, v⟩ := by + simp [getEntry!, h] + +theorem getEntry!_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} [Inhabited ((a : α) × β a)] + (h : (k == a) = false) : getEntry! a (⟨k, v⟩ :: l) = getEntry! a l := by + simp [getEntry!, h] + +@[simp] +theorem getEntry!_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} [Inhabited ((a : α) × β a)] : + getEntry! k (⟨k, v⟩ :: l) = ⟨k, v⟩ := + getEntry!_cons_of_true BEq.rfl + theorem beq_of_getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a} (h : getEntry? a l = some p) : p.1 == a := by induction l using assoc_induction @@ -95,6 +144,18 @@ theorem getEntry?_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β rw [getEntry?_cons_of_false h', getEntry?_cons_of_false h₂, ih] · rw [getEntry?_cons_of_true h', getEntry?_cons_of_true (BEq.trans h' h)] +theorem getEntryD_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a} : + getEntryD a fallback l = (getEntry? a l).getD fallback := by + induction l using assoc_induction with + | nil => simp [getEntryD, getEntry?] + | cons k v t ih => cases h : k == a <;> simp_all [getEntryD, getEntry?] + +theorem getEntry!_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited ((a : α) × β a)] : + getEntry! a l = (getEntry? a l).get! := by + induction l using assoc_induction with + | nil => rfl + | cons k v t ih => cases h : k == a <;> simp_all [getEntry!, getEntry?] + theorem keys_eq_map {l : List ((a : α) × β a)} : keys l = l.map (·.1) := by induction l with @@ -484,6 +545,30 @@ theorem getEntry_eq_of_getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} (h : getEntry? a l = some ⟨k, v⟩) {h'} : getEntry a l h' = ⟨k, v⟩ := by simp [getEntry, h] +theorem getEntry_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} + (h : containsKey a (⟨k, v⟩ :: l)) : + getEntry a (⟨k, v⟩ :: l) h = + if h' : k == a then + ⟨k, v⟩ + else + getEntry a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by + rw [getEntry, Option.get_congr getEntry?_cons] + split + case _ => + rename_i h + simp [h] + case _ => + rename_i h + simp [h] + rw [getEntry] + +theorem getEntry_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} + (h : a == b) {h₁ h₂} : getEntry a l h₁ = getEntry b l h₂ := by + suffices some (getEntry a l h₁) = some (getEntry b l h₂) by + injections + simp only [← getEntry?_eq_some_getEntry] + apply getEntry?_congr h + theorem getEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) : getEntry a (⟨k, v⟩ :: l) (containsKey_cons_of_beq (v := v) h) = ⟨k, v⟩ := by simp [getEntry, getEntry?_cons_of_true h] @@ -1622,6 +1707,20 @@ theorem getValueCast_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × getValueCast?_insertEntry] simp only [← getValueCast?_eq_some_getValueCast] +theorem getEntry_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} + {v : β k} {h} : + getEntry a (insertEntry k v l) h = if h' : k == a then ⟨k, v⟩ else getEntry a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by + suffices some (getEntry a (insertEntry k v l) h) = if h' : (k == a) = true then some ⟨k, v⟩ else some (getEntry a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h'))) by + split <;> (rename_i h; simpa [h] using this) + simp only [← getEntry?_eq_some_getEntry] + apply getEntry?_insertEntry + +theorem beq_of_getEntry_eq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {p : ((a : α) × β a)} + {k : α} {h₁} (h : getEntry k l h₁ = p) : p.fst == k := by + have heq1 : some (getEntry k l h₁) = some p := by simp only [h] + rw [← getEntry?_eq_some_getEntry] at heq1 + exact @beq_of_getEntry?_eq_some α β _ l k p heq1 + theorem getValueCast_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : getValueCast k (insertEntry k v l) containsKey_insertEntry_self = v := by simp [getValueCast_insertEntry] @@ -2133,6 +2232,14 @@ theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))).elim next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm))) +theorem getEntryD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a} + (hl : DistinctKeys l) (h : Perm l l') : getEntryD a fallback l = getEntryD a fallback l' := by + rw [getEntryD_eq_getEntry?, getEntryD_eq_getEntry?, getEntry?_of_perm hl h] + +theorem getEntry!_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} [Inhabited ((a : α) × β a)] + (hl : DistinctKeys l) (h : Perm l l') : getEntry! a l = getEntry! a l' := by + rw [getEntry!_eq_getEntry?, getEntry!_eq_getEntry?, getEntry?_of_perm hl h] + theorem containsKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α} (h : Perm l l') : containsKey k l = containsKey k l' := by induction h @@ -2153,6 +2260,12 @@ theorem getValueCast_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast, getValueCast?_of_perm hl h] +theorem getEntry_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {h'} (hl : DistinctKeys l) (h : Perm l l') : getEntry a l h' = getEntry a l' ((containsKey_of_perm h).symm.trans h') := by + suffices some (getEntry a l h') = some (getEntry a l' ((containsKey_of_perm h).symm.trans h')) by injections + rw [← getEntry?_eq_some_getEntry, ← getEntry?_eq_some_getEntry] + apply getEntry?_of_perm hl h + + theorem getValueCast!_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (hl : DistinctKeys l) (h : Perm l l') : getValueCast! a l = getValueCast! a l' := by @@ -2328,6 +2441,14 @@ theorem getEntry?_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) (h : containsKey a l' = false) : getEntry? a (l ++ l') = getEntry? a l := by rw [getEntry?_append, getEntry?_eq_none.2 h, Option.or_none] +theorem getEntryD_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a} + (h : containsKey a l' = false) : getEntryD a fallback (l ++ l') = getEntryD a fallback l := by + simp [getEntryD_eq_getEntry?, getEntry?_append_of_containsKey_eq_false h] + +theorem getEntry!_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α} [Inhabited ((a : α) × β a)] + (h : containsKey a l' = false) : getEntry! a (l ++ l') = getEntry! a l := by + simp [getEntry!_eq_getEntry?, getEntry?_append_of_containsKey_eq_false h] + @[simp] theorem containsKey_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} : containsKey a (l ++ l') = (containsKey a l || containsKey a l') := by @@ -2377,6 +2498,12 @@ theorem getValueCast_append_of_containsKey_eq_false [BEq α] [LawfulBEq α] rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast, getValueCast?_append_of_containsKey_eq_false hl'] +theorem getEntry_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α} {h} (hl' : containsKey a l' = false) : getEntry a (l ++ l') h = getEntry a l ((containsKey_append_of_not_contains_right hl').symm.trans h) := by + suffices some (getEntry a (l ++ l') h) = some (getEntry a l ((containsKey_append_of_not_contains_right hl').symm.trans h)) by + injections + simp only [← getEntry?_eq_some_getEntry] + apply getEntry?_append_of_containsKey_eq_false hl' + theorem getKey?_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) : getKey? a (l ++ l') = getKey? a l := by