From a750da5a7f7448aa49a330c7e9dbc606ab11a586 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Fri, 20 Jun 2025 18:16:46 +1000 Subject: [PATCH] chore: convert `DHashMap` to a structure (#8761) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes the definition of `DHashMap` to a structure. This makes it more consistent with the other map types, which are generally defined as structures. It also ensures that the type `DHashMap α β` is already in weak head normal form, making it easier for `grind` to successfully generate patterns for `DHashMap` lemmas. --- src/Std/Data/DHashMap/Basic.lean | 6 ++- src/Std/Data/DHashMap/Lemmas.lean | 63 +++++++++++++++---------------- 2 files changed, 36 insertions(+), 33 deletions(-) diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index e10e1468b2..cbce4beaa5 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -61,7 +61,11 @@ be used in nested inductive types. For these use cases, `Std.DHashMap.Raw` and For a variant that is more convenient for use in proofs because of extensionalities, see `Std.ExtDHashMap` which is defined in the module `Std.Data.ExtDHashMap`. -/ -def DHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] := { m : DHashMap.Raw α β // m.WF } +structure DHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] where + /-- Internal implementation detail of the hash map. -/ + inner : DHashMap.Raw α β + /-- Internal implementation detail of the hash map. -/ + wf : inner.WF namespace DHashMap diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 20497e6274..54f4533cc2 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -29,6 +29,9 @@ namespace Std.DHashMap variable {m : DHashMap α β} +private theorem ext {t t' : DHashMap α β} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl + @[simp, grind =] theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).isEmpty := Raw₀.isEmpty_emptyWithCapacity @@ -51,14 +54,10 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a := -- While setting up the API, often use this in the reverse direction, -- but prefer this direction for users. -@[simp, grind =] +@[simp, grind _=_] theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m := Iff.rfl --- We need to specify the pattern for the reverse direction manually, --- as the default heuristic leaves the `DHashMap α β` argument as a wildcard. -grind_pattern contains_iff_mem => @Membership.mem α (DHashMap α β) _ m a - theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b := Raw₀.contains_congr _ m.2 hab @@ -169,7 +168,7 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @[simp, grind =] theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : DHashMap α β).erase k = emptyWithCapacity c := - Subtype.eq (congrArg Subtype.val (Raw₀.erase_emptyWithCapacity (k := k)) :) + ext <| congrArg Subtype.val (Raw₀.erase_emptyWithCapacity (k := k)) @[simp, grind =] theorem erase_empty {k : α} : (∅ : DHashMap α β).erase k = ∅ := @@ -218,7 +217,7 @@ theorem containsThenInsert_fst {k : α} {v : β k} : (m.containsThenInsert k v). @[simp, grind =] theorem containsThenInsert_snd {k : α} {v : β k} : (m.containsThenInsert k v).2 = m.insert k v := - Subtype.eq <| (congrArg Subtype.val (Raw₀.containsThenInsert_snd _ (k := k)) :) + ext <| congrArg Subtype.val (Raw₀.containsThenInsert_snd _ (k := k)) @[simp, grind =] theorem containsThenInsertIfNew_fst {k : α} {v : β k} : @@ -228,7 +227,7 @@ theorem containsThenInsertIfNew_fst {k : α} {v : β k} : @[simp, grind =] theorem containsThenInsertIfNew_snd {k : α} {v : β k} : (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v := - Subtype.eq <| (congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _ (k := k)) :) + ext <| congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _ (k := k)) @[simp, grind =] theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : DHashMap α β).get? a = none := @@ -1116,7 +1115,7 @@ theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} : @[simp, grind =] theorem getThenInsertIfNew?_snd [LawfulBEq α] {k : α} {v : β k} : (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v := - Subtype.eq <| (congrArg Subtype.val (Raw₀.getThenInsertIfNew?_snd _ (k := k)) :) + ext <| congrArg Subtype.val (Raw₀.getThenInsertIfNew?_snd _ (k := k)) namespace Const @@ -1129,7 +1128,7 @@ theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v). @[simp, grind =] theorem getThenInsertIfNew?_snd {k : α} {v : β} : (getThenInsertIfNew? m k v).2 = m.insertIfNew k v := - Subtype.eq <| (congrArg Subtype.val (Raw₀.Const.getThenInsertIfNew?_snd _ (k := k)) :) + ext <| congrArg Subtype.val (Raw₀.Const.getThenInsertIfNew?_snd _ (k := k)) end Const @@ -1402,16 +1401,16 @@ variable {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] @[simp, grind =] theorem insertMany_nil : m.insertMany [] = m := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_nil ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val (Raw₀.insertMany_nil ⟨m.1, m.2.size_buckets_pos⟩) @[simp, grind =] theorem insertMany_list_singleton {k : α} {v : β k} : m.insertMany [⟨k, v⟩] = m.insert k v := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val (Raw₀.insertMany_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) @[grind _=_] theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} : m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_cons ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val (Raw₀.insertMany_cons ⟨m.1, m.2.size_buckets_pos⟩) @[grind _=_] theorem insertMany_append {l₁ l₂ : List ((a : α) × β a)} : @@ -1607,17 +1606,17 @@ variable {ρ : Type w} [ForIn Id ρ (α × β)] @[simp, grind =] theorem insertMany_nil : insertMany m [] = m := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_nil ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertMany_nil ⟨m.1, m.2.size_buckets_pos⟩) @[simp, grind =] theorem insertMany_list_singleton {k : α} {v : β} : insertMany m [⟨k, v⟩] = m.insert k v := - Subtype.eq (congrArg Subtype.val - (Raw₀.Const.insertMany_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val + (Raw₀.Const.insertMany_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) @[grind _=_] theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} : insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_cons ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertMany_cons ⟨m.1, m.2.size_buckets_pos⟩) @[grind _=_] theorem insertMany_append {l₁ l₂ : List (α × β)} : @@ -1819,19 +1818,19 @@ variable {ρ : Type w} [ForIn Id ρ α] @[simp] theorem insertManyIfNewUnit_nil : insertManyIfNewUnit m [] = m := - Subtype.eq (congrArg Subtype.val - (Raw₀.Const.insertManyIfNewUnit_nil ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val + (Raw₀.Const.insertManyIfNewUnit_nil ⟨m.1, m.2.size_buckets_pos⟩) @[simp] theorem insertManyIfNewUnit_list_singleton {k : α} : insertManyIfNewUnit m [k] = m.insertIfNew k () := - Subtype.eq (congrArg Subtype.val - (Raw₀.Const.insertManyIfNewUnit_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val + (Raw₀.Const.insertManyIfNewUnit_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) theorem insertManyIfNewUnit_cons {l : List α} {k : α} : insertManyIfNewUnit m (k :: l) = insertManyIfNewUnit (m.insertIfNew k ()) l := - Subtype.eq (congrArg Subtype.val - (Raw₀.Const.insertManyIfNewUnit_cons ⟨m.1, m.2.size_buckets_pos⟩) :) + ext <| congrArg Subtype.val + (Raw₀.Const.insertManyIfNewUnit_cons ⟨m.1, m.2.size_buckets_pos⟩) @[elab_as_elim] theorem insertManyIfNewUnit_ind {motive : DHashMap α (fun _ => Unit) → Prop} @@ -2005,16 +2004,16 @@ namespace DHashMap @[simp, grind =] theorem ofList_nil : ofList ([] : List ((a : α) × (β a))) = ∅ := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_nil (α := α)) :) + ext <| congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_nil (α := α)) @[simp, grind =] theorem ofList_singleton {k : α} {v : β k} : ofList [⟨k, v⟩] = (∅: DHashMap α β).insert k v := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_singleton (α := α)) :) + ext <| congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_singleton (α := α)) @[grind _=_] theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} : ofList (⟨k, v⟩ :: tl) = ((∅ : DHashMap α β).insert k v).insertMany tl := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_cons (α := α)) :) + ext <| congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_cons (α := α)) theorem ofList_eq_insertMany_empty {l : List ((a : α) × β a)} : ofList l = insertMany (∅ : DHashMap α β) l := rfl @@ -2154,16 +2153,16 @@ variable {β : Type v} @[simp, grind =] theorem ofList_nil : ofList ([] : List (α × β)) = ∅ := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_nil (α:= α)) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_nil (α:= α)) @[simp, grind =] theorem ofList_singleton {k : α} {v : β} : ofList [⟨k, v⟩] = (∅ : DHashMap α (fun _ => β)).insert k v := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_singleton (α:= α)) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_singleton (α:= α)) @[grind _=_] theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} : ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : DHashMap α (fun _ => β)).insert k v) tl := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_cons (α:= α)) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_cons (α:= α)) theorem ofList_eq_insertMany_empty {l : List (α × β)} : ofList l = insertMany (∅ : DHashMap α (fun _ => β)) l := rfl @@ -2299,17 +2298,17 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α] @[simp] theorem unitOfList_nil : unitOfList ([] : List α) = ∅ := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_nil (α := α)) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_nil (α := α)) @[simp] theorem unitOfList_singleton {k : α} : unitOfList [k] = (∅ : DHashMap α (fun _ => Unit)).insertIfNew k () := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton (α := α)) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton (α := α)) theorem unitOfList_cons {hd : α} {tl : List α} : unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : DHashMap α (fun _ => Unit)).insertIfNew hd ()) tl := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (α := α)) :) + ext <| congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (α := α)) @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]