Skip to content

chore: convert DHashMap to a structure #8761

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kim-em merged 1 commit into from
Jun 20, 2025
Merged

chore: convert DHashMap to a structure #8761

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/Std/Data/DHashMap/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
63 changes: 31 additions & 32 deletions src/Std/Data/DHashMap/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 = ∅ :=
Expand Down Expand Up @@ -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} :
Expand All @@ -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 :=
Expand Down Expand Up @@ -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

Expand All @@ -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

Expand Down Expand Up @@ -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)} :
Expand Down Expand Up @@ -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 (α × β)} :
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 α]
Expand Down
Loading