chore: convert ExtDHashMap into a one-field structure (#8770)

Author: Rob23oba

src/Std/Data/ExtDHashMap/Basic.lean

@@ -56,15 +56,47 @@ be used in nested inductive types. For these use cases, `Std.DHashMap.Raw` and
 `Std.DHashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer
 `DHashMap` over `DHashMap.Raw`.
 -/
-def ExtDHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] :=
-  Quotient (DHashMap.isSetoid α β)
+structure ExtDHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] where
+  /-- Internal implementation detail of the hash map. -/
+  mk' ::
+  /-- Internal implementation detail of the hash map. -/
+  inner : Quotient (DHashMap.isSetoid α β)
 
 namespace ExtDHashMap
 
+/-- Internal implementation detail of the hash map. -/
+abbrev mk (m : DHashMap α β) : ExtDHashMap α β :=
+  mk' (.mk _ m)
+
+/-- Internal implementation detail of the hash map. -/
+abbrev lift {γ : Sort w} (f : DHashMap α β → γ) (h : ∀ a b, a ~m b → f a = f b) (m : ExtDHashMap α β) : γ :=
+  m.1.lift f h
+
+/-- Internal implementation detail of the hash map. -/
+abbrev pliftOn {γ : Sort w} (m : ExtDHashMap α β) (f : (a : DHashMap α β) → m = mk a → γ)
+    (h : ∀ a b h₁ h₂, a ~m b → f a h₁ = f b h₂) : γ :=
+  m.1.pliftOn (fun a ha => f a (by cases m; cases ha; rfl)) (fun _ _ _ _ h' => h _ _ _ _ h')
+
+@[induction_eliminator, cases_eliminator, elab_as_elim]
+theorem inductionOn {motive : ExtDHashMap α β → Prop} (m : ExtDHashMap α β)
+    (mk : (a : DHashMap α β) → motive (mk a)) : motive m :=
+  (m.1.inductionOn fun _ => mk _ : motive ⟨m.1⟩)
+
+@[elab_as_elim]
+theorem inductionOn₂ {motive : ExtDHashMap α β → ExtDHashMap α β → Prop}
+    (m₁ m₂ : ExtDHashMap α β) (mk : (a b : DHashMap α β) → motive (mk a) (mk b)) : motive m₁ m₂ :=
+  m₁.inductionOn fun _ => m₂.inductionOn fun _ => mk _ _
+
+theorem sound {m₁ m₂ : DHashMap α β} (h : m₁ ~m m₂) : mk m₁ = mk m₂ :=
+  congrArg mk' (Quotient.sound h)
+
+theorem exact {m₁ m₂ : DHashMap α β} (h : mk m₁ = mk m₂) : m₁ ~m m₂ :=
+  Quotient.exact (congrArg inner h)
+
 @[inline, inherit_doc DHashMap.emptyWithCapacity]
 def emptyWithCapacity [BEq α] [Hashable α]
     (capacity := 8) : ExtDHashMap α β :=
-  Quotient.mk' (DHashMap.emptyWithCapacity capacity)
+  mk (DHashMap.emptyWithCapacity capacity)
 
 instance [BEq α] [Hashable α] : EmptyCollection (ExtDHashMap α β) where
   emptyCollection := emptyWithCapacity
@@ -75,8 +107,8 @@ instance [BEq α] [Hashable α] : Inhabited (ExtDHashMap α β) where
 @[inline, inherit_doc DHashMap.insert]
 def insert [EquivBEq α] [LawfulHashable α] (m : ExtDHashMap α β) (a : α)
     (b : β a) : ExtDHashMap α β :=
-  m.lift (fun m => Quotient.mk' (m.insert a b))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.insert a b))
+  m.lift (fun m => mk (m.insert a b))
+    (fun m m' (h : m ~m m') => sound (h.insert a b))
 
 instance [EquivBEq α] [LawfulHashable α] : Singleton ((a : α) × β a) (ExtDHashMap α β) where
   singleton | ⟨a, b⟩ => (∅ : ExtDHashMap α β).insert a b
@@ -90,37 +122,37 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulSingleton ((a : α) × β a)
 @[inline, inherit_doc DHashMap.insertIfNew]
 def insertIfNew [EquivBEq α] [LawfulHashable α] (m : ExtDHashMap α β)
     (a : α) (b : β a) : ExtDHashMap α β :=
-  m.lift (fun m => Quotient.mk' (m.insertIfNew a b))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.insertIfNew a b))
+  m.lift (fun m => mk (m.insertIfNew a b))
+    (fun m m' (h : m ~m m') => sound (h.insertIfNew a b))
 
 @[inline, inherit_doc DHashMap.containsThenInsert]
 def containsThenInsert [EquivBEq α] [LawfulHashable α]
     (m : ExtDHashMap α β) (a : α) (b : β a) : Bool × ExtDHashMap α β :=
-  m.lift (fun m => let m' := m.containsThenInsert a b; ⟨m'.1, Quotient.mk' m'.2⟩)
+  m.lift (fun m => let m' := m.containsThenInsert a b; ⟨m'.1, mk m'.2⟩)
     (fun m m' (h : m ~m m') =>
       Prod.ext
         (m.containsThenInsert_fst.symm ▸ m'.containsThenInsert_fst.symm ▸ h.contains_eq)
-        (Quotient.sound <|
+        (sound <|
           m.containsThenInsert_snd.symm ▸ m'.containsThenInsert_snd.symm ▸ h.insert a b))
 
 @[inline, inherit_doc DHashMap.containsThenInsertIfNew]
 def containsThenInsertIfNew [EquivBEq α] [LawfulHashable α]
     (m : ExtDHashMap α β) (a : α) (b : β a) : Bool × ExtDHashMap α β :=
-  m.lift (fun m => let m' := m.containsThenInsertIfNew a b; ⟨m'.1, Quotient.mk' m'.2⟩)
+  m.lift (fun m => let m' := m.containsThenInsertIfNew a b; ⟨m'.1, mk m'.2⟩)
     (fun m m' (h : m ~m m') =>
       Prod.ext
         (m.containsThenInsertIfNew_fst.symm ▸ m'.containsThenInsertIfNew_fst.symm ▸ h.contains_eq)
-        (Quotient.sound <|
+        (sound <|
           m.containsThenInsertIfNew_snd.symm ▸ m'.containsThenInsertIfNew_snd.symm ▸ h.insertIfNew a b))
 
 @[inline, inherit_doc DHashMap.getThenInsertIfNew?]
 def getThenInsertIfNew? [LawfulBEq α]
     (m : ExtDHashMap α β) (a : α) (b : β a) : Option (β a) × ExtDHashMap α β :=
-  m.lift (fun m => let m' := m.getThenInsertIfNew? a b; ⟨m'.1, Quotient.mk' m'.2⟩)
+  m.lift (fun m => let m' := m.getThenInsertIfNew? a b; ⟨m'.1, mk m'.2⟩)
     (fun m m' (h : m ~m m') =>
       Prod.ext
         (m.getThenInsertIfNew?_fst.symm ▸ m'.getThenInsertIfNew?_fst.symm ▸ h.get?_eq)
-        (Quotient.sound <|
+        (sound <|
           m.getThenInsertIfNew?_snd.symm ▸ m'.getThenInsertIfNew?_snd.symm ▸ h.insertIfNew a b))
 
 @[inline, inherit_doc DHashMap.get?]
@@ -158,8 +190,8 @@ def getD [LawfulBEq α] (m : ExtDHashMap α β)
 @[inline, inherit_doc DHashMap.erase]
 def erase [EquivBEq α] [LawfulHashable α] (m : ExtDHashMap α β) (a : α) :
     ExtDHashMap α β :=
-  m.lift (fun m => Quotient.mk' (m.erase a))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.erase a))
+  m.lift (fun m => mk (m.erase a))
+    (fun m m' (h : m ~m m') => sound (h.erase a))
 
 namespace Const
 
@@ -195,12 +227,12 @@ def getThenInsertIfNew? [EquivBEq α] [LawfulHashable α]
     Option β × ExtDHashMap α (fun _ => β) :=
   m.lift (fun m =>
       let m' := DHashMap.Const.getThenInsertIfNew? m a b
-      ⟨m'.1, Quotient.mk' m'.2⟩)
+      ⟨m'.1, mk m'.2⟩)
     (fun m m' (h : m ~m m') =>
       Prod.ext
         (DHashMap.Const.getThenInsertIfNew?_fst.symm ▸
           DHashMap.Const.getThenInsertIfNew?_fst.symm ▸ h.constGet?_eq)
-        (Quotient.sound <|
+        (sound <|
           DHashMap.Const.getThenInsertIfNew?_snd.symm ▸
           DHashMap.Const.getThenInsertIfNew?_snd.symm ▸ h.insertIfNew a b))
 
@@ -237,44 +269,44 @@ def isEmpty [EquivBEq α] [LawfulHashable α] (m : ExtDHashMap α β) : Bool :=
 @[inline, inherit_doc DHashMap.filter]
 def filter [EquivBEq α] [LawfulHashable α] (f : (a : α) → β a → Bool)
     (m : ExtDHashMap α β) : ExtDHashMap α β :=
-  m.lift (fun m => Quotient.mk' (m.filter f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.filter f))
+  m.lift (fun m => mk (m.filter f))
+    (fun m m' (h : m ~m m') => sound (h.filter f))
 
 @[inline, inherit_doc DHashMap.map]
 def map [EquivBEq α] [LawfulHashable α] (f : (a : α) → β a → γ a)
     (m : ExtDHashMap α β) : ExtDHashMap α γ :=
-  m.lift (fun m => Quotient.mk' (m.map f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.map f))
+  m.lift (fun m => mk (m.map f))
+    (fun m m' (h : m ~m m') => sound (h.map f))
 
 @[inline, inherit_doc DHashMap.filterMap]
 def filterMap [EquivBEq α] [LawfulHashable α] (f : (a : α) → β a → Option (γ a))
     (m : ExtDHashMap α β) : ExtDHashMap α γ :=
-  m.lift (fun m => Quotient.mk' (m.filterMap f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.filterMap f))
+  m.lift (fun m => mk (m.filterMap f))
+    (fun m m' (h : m ~m m') => sound (h.filterMap f))
 
 @[inline, inherit_doc DHashMap.modify]
 def modify [LawfulBEq α] (m : ExtDHashMap α β)
     (a : α) (f : β a → β a) : ExtDHashMap α β :=
-  m.lift (fun m => Quotient.mk' (m.modify a f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.modify a f))
+  m.lift (fun m => mk (m.modify a f))
+    (fun m m' (h : m ~m m') => sound (h.modify a f))
 
 @[inline, inherit_doc DHashMap.Const.modify]
 def Const.modify [EquivBEq α] [LawfulHashable α] {β : Type v} (m : ExtDHashMap α (fun _ => β))
     (a : α) (f : β → β) : ExtDHashMap α (fun _ => β) :=
-  m.lift (fun m => Quotient.mk' (DHashMap.Const.modify m a f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.constModify a f))
+  m.lift (fun m => mk (DHashMap.Const.modify m a f))
+    (fun m m' (h : m ~m m') => sound (h.constModify a f))
 
 @[inline, inherit_doc DHashMap.alter]
 def alter [LawfulBEq α] (m : ExtDHashMap α β)
     (a : α) (f : Option (β a) → Option (β a)) : ExtDHashMap α β :=
-  m.lift (fun m => Quotient.mk' (m.alter a f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.alter a f))
+  m.lift (fun m => mk (m.alter a f))
+    (fun m m' (h : m ~m m') => sound (h.alter a f))
 
 @[inline, inherit_doc DHashMap.Const.alter]
 def Const.alter [EquivBEq α] [LawfulHashable α] {β : Type v} (m : ExtDHashMap α (fun _ => β))
     (a : α) (f : Option β → Option β) : ExtDHashMap α (fun _ => β) :=
-  m.lift (fun m => Quotient.mk' (DHashMap.Const.alter m a f))
-    (fun m m' (h : m ~m m') => Quotient.sound (h.constAlter a f))
+  m.lift (fun m => mk (DHashMap.Const.alter m a f))
+    (fun m m' (h : m ~m m') => sound (h.constAlter a f))
 
 /-
 Note: We can't use the existing functions because weird (noncomputable) `ForIn` instances
@@ -315,22 +347,22 @@ def Const.insertManyIfNewUnit [EquivBEq α] [LawfulHashable α] {ρ : Type w}
 @[inline, inherit_doc DHashMap.Const.unitOfArray]
 def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
     ExtDHashMap α (fun _ => Unit) :=
-  Quotient.mk' (DHashMap.Const.unitOfArray l)
+  mk (DHashMap.Const.unitOfArray l)
 
 @[inline, inherit_doc DHashMap.ofList]
 def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) :
     ExtDHashMap α β :=
-  Quotient.mk' (DHashMap.ofList l)
+  mk (DHashMap.ofList l)
 
 @[inline, inherit_doc DHashMap.Const.ofList]
 def Const.ofList {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :
     ExtDHashMap α (fun _ => β) :=
-  Quotient.mk' (DHashMap.Const.ofList l)
+  mk (DHashMap.Const.ofList l)
 
 @[inline, inherit_doc DHashMap.Const.unitOfList]
 def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
     ExtDHashMap α (fun _ => Unit) :=
-  Quotient.mk' (DHashMap.Const.unitOfList l)
+  mk (DHashMap.Const.unitOfList l)
 
 end ExtDHashMap