chore: AssocDArray -> DefaultDict

Algorithm.lean

@@ -1,6 +1,6 @@
 import Algorithm.Algebra.BigOperators.DFinsupp'
-import Algorithm.Data.Classes.AssocArray
 import Algorithm.Data.Classes.Bag
+import Algorithm.Data.Classes.DefaultDict
 import Algorithm.Data.Classes.Dict
 import Algorithm.Data.Classes.Erase
 import Algorithm.Data.Classes.GetElem

Algorithm/Data/Classes/AssocArray.lean → Algorithm/Data/Classes/DefaultDict.lean

@@ -7,60 +7,40 @@ import Algorithm.Data.Classes.GetElem
 import Algorithm.Data.DFinsupp'.Defs
 import Mathlib.Data.Setoid.Basic
 
-universe u v
-
 namespace Vector
 variable {α : Type*} {n : ℕ}
 
 set_option linter.unusedVariables false in -- TODO: generalize
 @[nolint unusedArguments]
-protected abbrev WithDefault (α : Type u) (n : Nat) (f : Fin n → α) := Vector α n
-
-instance {α n f} : Inhabited (Vector.WithDefault α n f) where
-  default := .ofFn f
-
-@[simp]
-lemma get_default {f} : (default : Vector.WithDefault α n f).get = f := by
-  ext i
-  exact getElem_ofFn i.2
+protected abbrev WithDefault (α : Type*) (n : Nat) (f : Fin n → α) := Vector α n
 
 end Vector
 
-class AssocDArray.ReadOnly (C : Type*) (ι : outParam Type*)
+class DefaultDict.ReadOnly (C : Type*) (ι : outParam Type*)
     (α : outParam Type*) (d : outParam <| ι → α) extends
     GetElemAllValid C ι α where
   toDFinsupp' : C → Π₀' i, [α, d i]
   coe_toDFinsupp'_eq_getElem : ∀ a, ⇑(toDFinsupp' a) = (a[·])
-export AssocDArray.ReadOnly (toDFinsupp' coe_toDFinsupp'_eq_getElem)
+export DefaultDict.ReadOnly (toDFinsupp' coe_toDFinsupp'_eq_getElem)
 
-/-- `AssocDArray C ι α d` is a data structure that acts like a finitely supported function
+/-- `DefaultDict C ι α d` is a data structure that acts like a finitely supported function
   `Π₀' i, [α, d i]` with single point update operation. -/
-class AssocDArray (C : Type*) [Inhabited C] (ι : outParam Type*)
+class DefaultDict (C : Type*) [Inhabited C] (ι : outParam Type*)
     (α : outParam Type*) (d : outParam <| ι → α) extends
-    AssocDArray.ReadOnly C ι α d, GetSetElemAllValid C ι α where
+    DefaultDict.ReadOnly C ι α d, GetSetElemAllValid C ι α where
   getElem_default i : (default : C)[i] = d i
 
-abbrev AssocArray.ReadOnly (C : Type*) (ι : outParam Type*)
-    (α : outParam Type*) (d : outParam α) :=
-  AssocDArray.ReadOnly C ι α (fun _ ↦ d)
-
-/-- `AssocArray C ι α d` is a data structure that acts like a finitely supported function
-  `ι →₀' [α, d]` with single point update operation. -/
-abbrev AssocArray (C : Type*) [Inhabited C] (ι : outParam Type*)
-    (α : outParam Type*) (d : outParam α) :=
-  AssocDArray C ι α (fun _ ↦ d)
-
-attribute [simp] AssocDArray.getElem_default coe_toDFinsupp'_eq_getElem
+attribute [simp] DefaultDict.getElem_default coe_toDFinsupp'_eq_getElem
 
 section AssocDArray
 
 variable {C ι α : Type*} {d : ι → α}
 
-variable [Inhabited C] [AssocDArray C ι α d]
+variable [Inhabited C] [DefaultDict C ι α d]
 
 instance : OfFn C ι α d where
   ofFn := default
-  getElem_ofFn i := AssocDArray.getElem_default i
+  getElem_ofFn i := DefaultDict.getElem_default i
 
 lemma toDFinsupp'_apply_eq_getElem (a : C) (i : ι) : toDFinsupp' a i = a[i] := by simp
 
@@ -79,7 +59,15 @@ end AssocDArray
 namespace Vector.WithDefault
 variable {α : Type*} {n : ℕ} {f : Fin n → α}
 
-instance : AssocDArray (Vector.WithDefault α n f) (Fin n) α f where
+instance {α n f} : Inhabited (Vector.WithDefault α n f) where
+  default := .ofFn f
+
+@[simp]
+lemma get_default {f} : (default : Vector.WithDefault α n f).get = f := by
+  ext i
+  exact getElem_ofFn i.2
+
+instance : DefaultDict (Vector.WithDefault α n f) (Fin n) α f where
   getElem a i _ := a.get i
   setElem a i := a.set i
   getElem_setElem_self a i v := a.getElem_set_self i.2
@@ -90,24 +78,22 @@ instance : AssocDArray (Vector.WithDefault α n f) (Fin n) α f where
 
 end Vector.WithDefault
 
-namespace AssocArray
-
-export AssocDArray (getElem_default)
+namespace DefaultDict
 
 class Ext (C : Type*) [Inhabited C] (ι : outParam Type*) (α : outParam Type*)
-    (d : outParam α) [AssocArray C ι α d] : Prop where
+    (d : outParam α) [DefaultDict C ι α fun _ ↦ d] : Prop where
   ext : ∀ {m₁ m₂ : C}, (∀ i : ι, m₁[i] = m₂[i]) → m₁ = m₂
 
-variable {C : Type*} [Inhabited C] {ι : Type*} {α : Type*} {d : α} [AssocArray C ι α d]
+variable {C : Type*} [Inhabited C] {ι : Type*} {α : Type*} {d : α} [DefaultDict C ι α fun _ ↦ d]
 
 variable (C)
 
 protected def Quotient := @Quotient C (Setoid.ker (fun (a : C) (i : ι) ↦ a[i]))
 
-instance : Inhabited (AssocArray.Quotient C) :=
+instance : Inhabited (DefaultDict.Quotient C) :=
   inferInstanceAs <| Inhabited (@Quotient C (Setoid.ker _))
 
-instance : AssocArray (AssocArray.Quotient C) ι α d where
+instance : DefaultDict (DefaultDict.Quotient C) ι α fun _ ↦ d where
   getElem c i _ := Quotient.lift (·[·] : C → ι → α) (fun _ _ ↦ id) c i
   setElem q i v := q.map' (·[i ↦ v]) fun _ _ hm ↦ funext fun j ↦ by
     classical simp [congrFun hm j]
@@ -120,7 +106,7 @@ instance : AssocArray (AssocArray.Quotient C) ι α d where
     induction a using Quotient.ind
     exact coe_toDFinsupp'_eq_getElem _
 
-instance : Ext (AssocArray.Quotient C) ι α d where
+instance : Ext (DefaultDict.Quotient C) ι α d where
   ext {m₁ m₂} := m₂.inductionOn <| m₁.inductionOn (fun _ _ ha ↦ Quotient.sound <| funext ha)
 export Ext (ext)
 
@@ -171,18 +157,17 @@ abbrev toOfFn [Fintype ι] (f : ι → α) : OfFn C ι α f where
     convert (getElem_indicator _ _ _).trans <| dif_pos <| Finset.mem_univ _
     classical infer_instance
 
-end AssocArray
+end DefaultDict
 
-class HasDefaultAssocDArray (ι : Type u) (α : Type v) (f : ι → α)
-    (DefaultAssocDArray : outParam <| Type max u v)
-    [Inhabited DefaultAssocDArray] where
-  [toAssocDArray : AssocDArray DefaultAssocDArray ι α f]
+class HasDefaultDict (ι : Type*) (α : Type*) (f : ι → α) (C : outParam <| Type*)
+    [Inhabited C] where
+  [toDefaultDict : DefaultDict C ι α f]
 
 @[nolint unusedArguments]
-def DefaultAssocDArray (ι : Type u) (α : Type v) (f : ι → α) {D : Type _} [Inhabited D]
-    [HasDefaultAssocDArray ι α f D] :=
-  D
+def mkDefaultDict (ι : Type*) (α : Type*) (f : ι → α) {D : Type*} [Inhabited D]
+    [HasDefaultDict ι α f D] : D :=
+  default
 
-instance {n α f} : HasDefaultAssocDArray (Fin n) α f (Vector.WithDefault α n f) where
+instance {n α f} : HasDefaultDict (Fin n) α f (Vector.WithDefault α n f) where
 
-example {n α f} := DefaultAssocDArray (Fin n) α f
+example {n α f} := mkDefaultDict (Fin n) α f

Algorithm/Data/Classes/Dict.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-import Algorithm.Data.Classes.AssocArray
 import Algorithm.Data.Classes.Bag
+import Algorithm.Data.Classes.DefaultDict
 import Algorithm.Data.Classes.GetElem
 
 variable {C ι α : Type*}
@@ -29,20 +29,20 @@ instance : Inhabited C where
 instance : LawfulErase C ι := lawfulErase_iff_toFinset.mpr fun c i ↦ by
   ext; simp [valid_erase, eq_comm]
 
-def Dict.AssocArray (C : Type*) := C
+def Dict.DefaultDict (C : Type*) := C
 
-def Dict.toAssocArray : C ≃ Dict.AssocArray C := Equiv.refl _
+def Dict.toDefaultDict : C ≃ Dict.DefaultDict C := Equiv.refl _
 
-instance : Inhabited (Dict.AssocArray C) where
-  default := Dict.toAssocArray ∅
+instance : Inhabited (Dict.DefaultDict C) where
+  default := Dict.toDefaultDict ∅
 
-instance [Dict C ι α] : AssocArray (Dict.AssocArray C) ι (Option α) none where
-  getElem a i _ := (Dict.toAssocArray.symm a)[i]?
-  toDFinsupp' a := .mk' ((Dict.toAssocArray.symm a)[·]?)
-    (.mk ⟨toMultiset (Dict.toAssocArray.symm a), fun i ↦ by
+instance [Dict C ι α] : DefaultDict (Dict.DefaultDict C) ι (Option α) fun _ ↦ none where
+  getElem a i _ := (Dict.toDefaultDict.symm a)[i]?
+  toDFinsupp' a := .mk' ((Dict.toDefaultDict.symm a)[·]?)
+    (.mk ⟨toMultiset (Dict.toDefaultDict.symm a), fun i ↦ by
       simp [mem_toMultiset, or_iff_not_imp_left] ⟩)
   coe_toDFinsupp'_eq_getElem := by simp
-  setElem c i x := Dict.toAssocArray <| alterElem (Dict.toAssocArray.symm c) i (fun _ ↦ x)
+  setElem c i x := Dict.toDefaultDict <| alterElem (Dict.toDefaultDict.symm c) i (fun _ ↦ x)
   getElem_setElem_self := by simp
   getElem_setElem_of_ne _ _ _ _ hij := by simp [hij]
   getElem_default _ := by simpa [default] using getElem?_neg (cont := C) _ _ (not_mem_empty _)