From 5dff892df5aa24ab5cc16948faa6163813cf3571 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Sat, 2 Aug 2025 09:35:51 +0800 Subject: [PATCH 1/4] chore: `AssocArray` -> `DefaultDict` --- Algorithm.lean | 2 +- .../{AssocArray.lean => DefaultDict.lean} | 20 ++-- Algorithm/Data/Classes/Dict.lean | 20 ++-- Algorithm/Data/Classes/IndexedMinHeap.lean | 98 +++++++++---------- Algorithm/Data/Graph/AdjList.lean | 12 +-- Algorithm/Data/Graph/IsDFSForest.lean | 2 +- Algorithm/Data/UnionFind.lean | 4 +- Algorithm/Graph/DFS.lean | 34 +++---- Algorithm/Graph/Dijkstra.lean | 26 ++--- scripts/nolints.json | 30 +++--- 10 files changed, 124 insertions(+), 124 deletions(-) rename Algorithm/Data/Classes/{AssocArray.lean => DefaultDict.lean} (92%) diff --git a/Algorithm.lean b/Algorithm.lean index af64b54..0e230c9 100644 --- a/Algorithm.lean +++ b/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 diff --git a/Algorithm/Data/Classes/AssocArray.lean b/Algorithm/Data/Classes/DefaultDict.lean similarity index 92% rename from Algorithm/Data/Classes/AssocArray.lean rename to Algorithm/Data/Classes/DefaultDict.lean index 33f0122..4b8be6b 100644 --- a/Algorithm/Data/Classes/AssocArray.lean +++ b/Algorithm/Data/Classes/DefaultDict.lean @@ -40,13 +40,13 @@ class AssocDArray (C : Type*) [Inhabited C] (ι : outParam Type*) AssocDArray.ReadOnly C ι α d, GetSetElemAllValid C ι α where getElem_default i : (default : C)[i] = d i -abbrev AssocArray.ReadOnly (C : Type*) (ι : outParam Type*) +abbrev DefaultDict.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 +/-- `DefaultDict 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*) +abbrev DefaultDict (C : Type*) [Inhabited C] (ι : outParam Type*) (α : outParam Type*) (d : outParam α) := AssocDArray C ι α (fun _ ↦ d) @@ -90,24 +90,24 @@ instance : AssocDArray (Vector.WithDefault α n f) (Fin n) α f where end Vector.WithDefault -namespace AssocArray +namespace DefaultDict export AssocDArray (getElem_default) class Ext (C : Type*) [Inhabited C] (ι : outParam Type*) (α : outParam Type*) - (d : outParam α) [AssocArray C ι α d] : Prop where + (d : outParam α) [DefaultDict C ι α 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 ι α 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) ι α 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 +120,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,7 +171,7 @@ 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) diff --git a/Algorithm/Data/Classes/Dict.lean b/Algorithm/Data/Classes/Dict.lean index c52b872..47b4b94 100644 --- a/Algorithm/Data/Classes/Dict.lean +++ b/Algorithm/Data/Classes/Dict.lean @@ -3,7 +3,7 @@ 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.DefaultDict import Algorithm.Data.Classes.Bag import Algorithm.Data.Classes.GetElem @@ -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.asDefaultDict : C ≃ Dict.DefaultDict C := Equiv.refl _ -instance : Inhabited (Dict.AssocArray C) where - default := Dict.toAssocArray ∅ +instance : Inhabited (Dict.DefaultDict C) where + default := Dict.asDefaultDict ∅ -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 α) none where + getElem a i _ := (Dict.asDefaultDict.symm a)[i]? + toDFinsupp' a := .mk' ((Dict.asDefaultDict.symm a)[·]?) + (.mk ⟨toMultiset (Dict.asDefaultDict.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.asDefaultDict <| alterElem (Dict.asDefaultDict.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 _) diff --git a/Algorithm/Data/Classes/IndexedMinHeap.lean b/Algorithm/Data/Classes/IndexedMinHeap.lean index f8f482a..c16f31b 100644 --- a/Algorithm/Data/Classes/IndexedMinHeap.lean +++ b/Algorithm/Data/Classes/IndexedMinHeap.lean @@ -3,7 +3,7 @@ Copyright (c) 2023 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.DefaultDict import Algorithm.Data.Classes.MinHeap import Algorithm.Data.Classes.ToList import Mathlib.Data.Finset.Lattice.Fold @@ -107,17 +107,17 @@ instance (α) (x : WithTop α) : Decidable (x = ⊤) := end WithTop -structure AssocArrayWithHeap.WithIdx (α ι : Type*) where +structure DefaultDictWithHeap.WithIdx (α ι : Type*) where val : α idx : ι -namespace AssocArrayWithHeap.WithIdx +namespace DefaultDictWithHeap.WithIdx variable {α ι : Type*} -instance [LE α] : LE (AssocArrayWithHeap.WithIdx α ι) where +instance [LE α] : LE (DefaultDictWithHeap.WithIdx α ι) where le x y := x.val ≤ y.val -lemma le_def [LE α] {x y : AssocArrayWithHeap.WithIdx α ι} : +lemma le_def [LE α] {x y : DefaultDictWithHeap.WithIdx α ι} : x ≤ y ↔ x.val ≤ y.val := Iff.rfl @@ -126,7 +126,7 @@ lemma mk_le_mk [LE α] {x y : α} {xi yi : ι} : mk x xi ≤ mk y yi ↔ x ≤ y := Iff.rfl -instance [LT α] : LT (AssocArrayWithHeap.WithIdx α ι) where +instance [LT α] : LT (DefaultDictWithHeap.WithIdx α ι) where lt x y := x.val < y.val @[simp] @@ -134,65 +134,65 @@ lemma mk_lt_mk [LT α] {x y : α} {xi yi : ι} : mk x xi < mk y yi ↔ x < y := Iff.rfl -instance [Preorder α] : Preorder (AssocArrayWithHeap.WithIdx α ι) where +instance [Preorder α] : Preorder (DefaultDictWithHeap.WithIdx α ι) where le_refl _ := le_refl _ le_trans _ _ _ := le_trans lt_iff_le_not_ge _ _ := lt_iff_le_not_ge instance [Preorder α] [IsTotal α (· ≤ ·)] : - IsTotal (AssocArrayWithHeap.WithIdx α ι) (· ≤ ·) where + IsTotal (DefaultDictWithHeap.WithIdx α ι) (· ≤ ·) where total _ _ := total_of (α := α) (· ≤ ·) _ _ -end AssocArrayWithHeap.WithIdx +end DefaultDictWithHeap.WithIdx -structure AssocArrayWithHeap (C C' : Type*) {ι α : Type*} [Preorder α] [IsTotal α (· ≤ ·)] - [Inhabited C] [AssocArray C ι (WithTop α) ⊤] - [MinHeap C' (AssocArrayWithHeap.WithIdx α ι)] where mk' :: - assocArray : C +structure DefaultDictWithHeap (C C' : Type*) {ι α : Type*} [Preorder α] [IsTotal α (· ≤ ·)] + [Inhabited C] [DefaultDict C ι (WithTop α) ⊤] + [MinHeap C' (DefaultDictWithHeap.WithIdx α ι)] where mk' :: + defaultDict : C minHeap : C' - mem_minHeap' : ∀ i : ι, (hi : assocArray[i] ≠ ⊤) → ⟨assocArray[i].untop hi, i⟩ ∈ minHeap + mem_minHeap' : ∀ i : ι, (hi : defaultDict[i] ≠ ⊤) → ⟨defaultDict[i].untop hi, i⟩ ∈ minHeap getElem_minIdx' : (h : ¬isEmpty minHeap) → - assocArray[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val + defaultDict[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val -namespace AssocArrayWithHeap +namespace DefaultDictWithHeap variable {C C' : Type*} {ι α : Type*} [Preorder α] [IsTotal α (· ≤ ·)] - [Inhabited C] [AssocArray C ι (WithTop α) ⊤] - [MinHeap C' (AssocArrayWithHeap.WithIdx α ι)] + [Inhabited C] [DefaultDict C ι (WithTop α) ⊤] + [MinHeap C' (DefaultDictWithHeap.WithIdx α ι)] -instance : AssocArray.ReadOnly (AssocArrayWithHeap C C') ι (WithTop α) ⊤ where - getElem c i _ := c.assocArray[i] - toDFinsupp' c := toDFinsupp' c.assocArray - coe_toDFinsupp'_eq_getElem c := coe_toDFinsupp'_eq_getElem c.assocArray +instance : DefaultDict.ReadOnly (DefaultDictWithHeap C C') ι (WithTop α) ⊤ where + getElem c i _ := c.defaultDict[i] + toDFinsupp' c := toDFinsupp' c.defaultDict + coe_toDFinsupp'_eq_getElem c := coe_toDFinsupp'_eq_getElem c.defaultDict @[simp] -lemma assocArray_getElem (c : AssocArrayWithHeap C C') (i : ι) : - c.assocArray[i] = c[i] := +lemma defaultDict_getElem (c : DefaultDictWithHeap C C') (i : ι) : + c.defaultDict[i] = c[i] := rfl -lemma mem_minHeap (c : AssocArrayWithHeap C C') : +lemma mem_minHeap (c : DefaultDictWithHeap C C') : ∀ i : ι, (hi : c[i] ≠ ⊤) → ⟨c[i].untop hi, i⟩ ∈ c.minHeap := c.mem_minHeap' -lemma getElem_minIdx (c : AssocArrayWithHeap C C') (h : ¬isEmpty c.minHeap) : +lemma getElem_minIdx (c : DefaultDictWithHeap C C') (h : ¬isEmpty c.minHeap) : c[(MinHeap.head c.minHeap h).idx] = (MinHeap.head c.minHeap h).val := c.getElem_minIdx' h -instance : Inhabited (AssocArrayWithHeap C C') where +instance : Inhabited (DefaultDictWithHeap C C') where default := ⟨default, ∅, by simp, by simp [size_eq_card_toMultiset]⟩ -def mk [DecidableEq α] (assocArray : C) (minHeap : C') - (mem_minHeap : ∀ i : ι, (hi : assocArray[i] ≠ ⊤) → ⟨(assocArray[i]).untop hi, i⟩ ∈ minHeap) : - AssocArrayWithHeap C C' := +def mk [DecidableEq α] (defaultDict : C) (minHeap : C') + (mem_minHeap : ∀ i : ι, (hi : defaultDict[i] ≠ ⊤) → ⟨(defaultDict[i]).untop hi, i⟩ ∈ minHeap) : + DefaultDictWithHeap C C' := if h : isEmpty minHeap then - ⟨assocArray, minHeap, mem_minHeap, (False.elim <| · h)⟩ - else if h' : assocArray[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val then - ⟨assocArray, minHeap, mem_minHeap, fun _ ↦ h'⟩ + ⟨defaultDict, minHeap, mem_minHeap, (False.elim <| · h)⟩ + else if h' : defaultDict[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val then + ⟨defaultDict, minHeap, mem_minHeap, fun _ ↦ h'⟩ else haveI : DecidableEq (WithIdx α ι) := by classical infer_instance have : size (MinHeap.tail minHeap) < size minHeap := by simpa [h, size_eq_card_toMultiset, Multiset.card_erase_lt_of_mem] using Multiset.card_erase_lt_of_mem (MinHeap.head_mem_toMultiset _ _) - mk assocArray (MinHeap.tail minHeap) fun i hi ↦ by + mk defaultDict (MinHeap.tail minHeap) fun i hi ↦ by simp only [← mem_toMultiset, MinHeap.toMultiset_tail, h, Bool.false_eq_true, ↓reduceDIte, MinHeap.head_def] rw [Multiset.mem_erase_of_ne, mem_toMultiset] @@ -203,33 +203,33 @@ def mk [DecidableEq α] (assocArray : C) (minHeap : C') termination_by size minHeap @[simp, nolint unusedHavesSuffices] -- false positive -lemma mk_assocArray [DecidableEq α] (assocArray : C) (minHeap : C') - (mem_minHeap : ∀ i : ι, (hi : assocArray[i] ≠ ⊤) → ⟨(assocArray[i]).untop hi, i⟩ ∈ minHeap) : - (mk assocArray minHeap mem_minHeap).assocArray = assocArray := by +lemma mk_defaultDict [DecidableEq α] (defaultDict : C) (minHeap : C') + (mem_minHeap : ∀ i : ι, (hi : defaultDict[i] ≠ ⊤) → ⟨(defaultDict[i]).untop hi, i⟩ ∈ minHeap) : + (mk defaultDict minHeap mem_minHeap).defaultDict = defaultDict := by induction minHeap, mem_minHeap using mk.induct all_goals unfold mk; simp [*] @[simp] -lemma default_assocArray : - (default : AssocArrayWithHeap C C').assocArray = default := +lemma default_defaultDict : + (default : DefaultDictWithHeap C C').defaultDict = default := rfl @[simp] lemma default_minHeap : - (default : AssocArrayWithHeap C C').minHeap = ∅ := + (default : DefaultDictWithHeap C C').minHeap = ∅ := rfl instance [DecidableEq α] : - AssocArray (AssocArrayWithHeap C C') ι (WithTop α) ⊤ where + DefaultDict (DefaultDictWithHeap C C') ι (WithTop α) ⊤ where setElem c i x := mk - c.assocArray[i ↦ x] + c.defaultDict[i ↦ x] (if hx : x = ⊤ then c.minHeap else insert ⟨x.untop hx, i⟩ c.minHeap) fun j hj ↦ by haveI : DecidableEq ι := by classical infer_instance split_ifs with hx <;> simp? [Function.update_apply] at hj ⊢ says - simp only [all_valid, getElem_setElem, assocArray_getElem, ne_eq] at hj ⊢ + simp only [all_valid, getElem_setElem, defaultDict_getElem, ne_eq] at hj ⊢ · subst hx rw [ite_eq_left_iff, Classical.not_imp] at hj simp only [hj.1, ↓reduceIte] @@ -244,12 +244,12 @@ instance [DecidableEq α] : getElem_default := by simp [getElem] @[simp] -lemma set_assocArray [DecidableEq α] (c : AssocArrayWithHeap C C') (i : ι) (x) : - c[i ↦ x].assocArray = c.assocArray[i ↦ x] := by +lemma set_defaultDict [DecidableEq α] (c : DefaultDictWithHeap C C') (i : ι) (x) : + c[i ↦ x].defaultDict = c.defaultDict[i ↦ x] := by unfold_projs; simp instance [Inhabited ι] [DecidableEq α] : - IndexedMinHeap (AssocArrayWithHeap C C') ι (WithTop α) where + IndexedMinHeap (DefaultDictWithHeap C C') ι (WithTop α) where minIdx c := if h : isEmpty c.minHeap then default else (MinHeap.head c.minHeap h).idx getElem_minIdx_le c i := by split_ifs with h @@ -267,17 +267,17 @@ instance [Inhabited ι] [DecidableEq α] : -- 堆中按顺序为 `(x', 1)` `(x, 0)` `(x + 1, 0)` -- 将 `0` 处更新为 `x'`，堆可以变为 `(x, 0)` `(x', 0)` `(x', 1)` `(x + 1, 0)` -- 此时必须操作堆弹出 `(x, 0)` - -- decreaseKey c i x hx := ⟨AssocArray.set c.assocArray i x, + -- decreaseKey c i x hx := ⟨DefaultDict.set c.defaultDict i x, -- insert ⟨x.untop (hx.trans_le le_top).ne, i⟩ c.minHeap, -- by -- haveI : DecidableEq ι := by classical infer_instance -- intro j hj -- simp? [Function.update_apply] at hj ⊢ says -- simp only [AssocDArray.getElem_set, Function.update_apply, AssocDArray.get_eq_getElem, - -- assocArray_getElem, ne_eq] at hj ⊢ + -- defaultDict_getElem, ne_eq] at hj ⊢ -- rw [ToMultiset.mem_iff, toMultiset_insert, Multiset.mem_cons] -- split_ifs at hj ⊢ with hji -- · simp [hji] -- · exact .inr <| c.mem_minHeap j hj, -end AssocArrayWithHeap +end DefaultDictWithHeap diff --git a/Algorithm/Data/Graph/AdjList.lean b/Algorithm/Data/Graph/AdjList.lean index 8695837..f1871a5 100644 --- a/Algorithm/Data/Graph/AdjList.lean +++ b/Algorithm/Data/Graph/AdjList.lean @@ -3,7 +3,7 @@ Copyright (c) 2023 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.DefaultDict import Algorithm.Data.Classes.ToList -- import Mathlib.Data.List.Nodup import Mathlib.Combinatorics.Quiver.Path @@ -12,7 +12,7 @@ structure AdjList (V : Type*) (Info : Type*) (EColl : Type*) [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - (StarColl : Type*) [AssocArray.ReadOnly StarColl V EColl ∅] where + (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl ∅] where protected snd : Info → V protected star : StarColl @@ -20,7 +20,7 @@ structure AdjList₂ (V : Type*) (Info : Type*) (EColl : Type*) [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - (StarColl : Type*) [AssocArray.ReadOnly StarColl V EColl ∅] extends + (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl ∅] extends AdjList V Info EColl StarColl where fst : Info → V costar : StarColl @@ -36,7 +36,7 @@ class AdjListClass (G : Type*) (V : outParam <| Type*) (Info : outParam <| Type*) (EColl : outParam <| Type*) [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - (StarColl : outParam <| Type*) [AssocArray.ReadOnly StarColl V EColl ∅] where + (StarColl : outParam <| Type*) [DefaultDict.ReadOnly StarColl V EColl ∅] where snd : G → Info → V star : G → StarColl @@ -56,7 +56,7 @@ variable {V : Type*} {Info : Type*} {EColl : Type*} [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] instance : AdjListClass (AdjList V Info EColl StarColl) V Info EColl StarColl where snd := AdjList.snd @@ -365,7 +365,7 @@ variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] (g : G) def succList (v : V) : List V := (toList g[v]).map g..snd diff --git a/Algorithm/Data/Graph/IsDFSForest.lean b/Algorithm/Data/Graph/IsDFSForest.lean index 9f2be51..ccd98a0 100644 --- a/Algorithm/Data/Graph/IsDFSForest.lean +++ b/Algorithm/Data/Graph/IsDFSForest.lean @@ -14,7 +14,7 @@ variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] {g : G} variable (g) in diff --git a/Algorithm/Data/UnionFind.lean b/Algorithm/Data/UnionFind.lean index b84fed5..a1f1e04 100644 --- a/Algorithm/Data/UnionFind.lean +++ b/Algorithm/Data/UnionFind.lean @@ -172,7 +172,7 @@ lemma find_snd_root (self : UnionFind ι P S) (i : ι) : (self.find i).snd.root = self.root := rootCore_findAux_snd self.parent self.wf i _ -lemma wellFounded_assocArraySet (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) +lemma wellFounded_defaultDictSet (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i r : ι) (hr : parent[r] = r) : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[i ↦ r][k] := by refine ⟨fun x ↦ ?_⟩ @@ -191,7 +191,7 @@ set_option linter.unusedVariables false in -- easier to `rw` and `simp` def setParent (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦ i ≠ j ∧ i = parent[j]) (i j : ι) (hi : parent[i] = i) (hj : parent[j] = j) (s : ℕ) : UnionFind ι P S := - ⟨parent[i ↦ j], size[j ↦ s], wellFounded_assocArraySet parent wf i j hj⟩ + ⟨parent[i ↦ j], size[j ↦ s], wellFounded_defaultDictSet parent wf i j hj⟩ @[simp] lemma setParent_parent_eq_parent (parent : P) (size : S) diff --git a/Algorithm/Graph/DFS.lean b/Algorithm/Graph/DFS.lean index 9adb2b1..9271320 100644 --- a/Algorithm/Graph/DFS.lean +++ b/Algorithm/Graph/DFS.lean @@ -12,7 +12,7 @@ namespace AdjListClass variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] -- 也许在以后可以改成存迭代器 @@ -20,7 +20,7 @@ variable {V : Type*} {Info : Type*} def dfsForest' (g : G) [Fintype V] {BoolArray : Type*} - [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : Forest V × { b : BoolArray // [DecidableEq V] → (toDFinsupp' visited).support ⊆ (toDFinsupp' b).support } := @@ -55,7 +55,7 @@ decreasing_by lemma roots_dfsForest'_fst_subset (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] + [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : (g..dfsForest' vs visited).1.roots ⊆ {v | v ∈ vs} := by match vs with @@ -72,7 +72,7 @@ lemma roots_dfsForest'_fst_subset (g : G) lemma subset_support_toDFinsupp'_dfsForest'_snd (g : G) [DecidableEq V] [Fintype V] {BoolArray : Type*} - [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : {v | v ∈ vs} ⊆ (toDFinsupp' (g..dfsForest' vs visited).2.val).support := by match vs with @@ -93,7 +93,7 @@ lemma subset_support_toDFinsupp'_dfsForest'_snd (g : G) lemma isDFSForest_dfsForest' (g : G) [DecidableEq V] [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] + [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : g..IsDFSForest (toDFinsupp' visited).support @@ -116,14 +116,14 @@ lemma isDFSForest_dfsForest' (g : G) def dfsForest (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] + [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : Forest V × BoolArray := (g..dfsForest' vs visited).map id Subtype.val lemma dfsForest_spec' (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] (vs : List V) : + [DefaultDict BoolArray V Bool false] (vs : List V) : let (f, vis) := (g..dfsForest vs (default : BoolArray)) ([DecidableEq V] → f.support = (toDFinsupp' vis).support) ∧ ∀ v, v ∈ f.support ↔ ∃ r ∈ vs, g..Reachable r v := by @@ -139,7 +139,7 @@ lemma dfsForest_spec' (g : G) lemma dfsForest_spec (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] (vs : List V) : + [DefaultDict BoolArray V Bool false] (vs : List V) : let (f, vis) := (g..dfsForest vs (default : BoolArray)) f.support = {v : V | vis[v]} ∧ ∀ v : V, vis[v] ↔ ∃ r ∈ vs, g..Reachable r v := by letI : Unique (DecidableEq V) := uniqueOfSubsingleton <| by classical infer_instance @@ -151,7 +151,7 @@ lemma dfsForest_spec (g : G) · simp [H.1] def dfs' (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : { b : BoolArray // ([DecidableEq V] → (toDFinsupp' visited).support ⊆ (toDFinsupp' b).support) ∧ @@ -187,7 +187,7 @@ decreasing_by simpa [Prod.lex_iff, ← le_iff_lt_or_eq] using this def dfs (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : BoolArray := (g..dfs' vs visited).val @@ -195,20 +195,20 @@ def dfs (g : G) @[simp] lemma dfsForest_snd (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] + [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : (g..dfsForest vs visited).snd = g..dfs vs visited := (g..dfs' vs visited).prop.2.symm lemma dfs_spec (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] (vs : List V) : + [DefaultDict BoolArray V Bool false] (vs : List V) : ∀ v : V, (g..dfs vs (default : BoolArray))[v] ↔ ∃ r ∈ vs, g..Reachable r v := g..dfsForest_snd vs (default : BoolArray) ▸ (g..dfsForest_spec BoolArray vs).2 def dfsForestTR (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] + [DefaultDict BoolArray V Bool false] (vs : List (Forest V × List V)) (visited : BoolArray) : Forest V × BoolArray := match vs with @@ -238,7 +238,7 @@ decreasing_by simp [*, Function.update] def dfs'TR (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List (List V)) (visited : BoolArray) : BoolArray := match vs with @@ -265,7 +265,7 @@ decreasing_by simp [*, Function.update] def dfsTR (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : BoolArray := match vs with @@ -290,7 +290,7 @@ decreasing_by lemma dfsTR_spec' (g : G) [Fintype V] [DecidableEq V] - {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false] + {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] (vs : List V) (visited : BoolArray) : g..traversal (toDFinsupp' visited).support {v | v ∈ vs ∧ v ∉ (toDFinsupp' visited).support} = g..traversal (toDFinsupp' (g..dfsTR vs visited)).support ∅ := by @@ -316,7 +316,7 @@ lemma dfsTR_spec' (g : G) lemma dfsTR_spec (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [AssocArray BoolArray V Bool false] + [DefaultDict BoolArray V Bool false] (vs : List V) : g..traversal ∅ {v | v ∈ vs} = {v : V | (g..dfsTR vs (default : BoolArray))[v]} := by letI : DecidableEq V := by classical infer_instance diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean index c0c6423..bed479f 100644 --- a/Algorithm/Graph/Dijkstra.lean +++ b/Algorithm/Graph/Dijkstra.lean @@ -103,7 +103,7 @@ namespace AdjListClass variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] {CostType : Type*} @@ -372,7 +372,7 @@ lemma isDist_union {g : G} def dijkstraStep (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) : @@ -387,7 +387,7 @@ def dijkstraStep (g : G) (c : Info → CostType) structure dijkstraStep.Spec (g : G) (c : Info → CostType) [AddMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) (heap : DistHeap) (res : DistArray) : Prop where h₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤ @@ -401,7 +401,7 @@ structure dijkstraStep.Spec (g : G) (c : Info → CostType) lemma dijkstraStep_snd_getElem (g : G) (c : Info → CostType) [DecidableEq V] [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) : (dijkstraStep g c heap res hMinIdx).2[v] = @@ -410,7 +410,7 @@ lemma dijkstraStep_snd_getElem (g : G) (c : Info → CostType) lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) : (dijkstraStep g c heap res hMinIdx).2[v] = ⊤ ↔ @@ -423,7 +423,7 @@ lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType) lemma dijkstraStep_snd_support (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) : {v : V | (dijkstraStep g c heap res hMinIdx).2[v] ≠ ⊤} = @@ -434,7 +434,7 @@ lemma dijkstraStep_snd_support (g : G) (c : Info → CostType) lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType) [DecidableEq V] [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : @@ -472,7 +472,7 @@ lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType) lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType) [DecidableEq V] [DecidableEq Info] [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : @@ -498,7 +498,7 @@ lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType) lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : @@ -521,7 +521,7 @@ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType) lemma dijkstraStep_fst_support (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) : @@ -536,7 +536,7 @@ lemma dijkstraStep_fst_support (g : G) (c : Info → CostType) lemma dijkstraStep_spec (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] - {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) (heap : DistHeap) (res : DistArray) (h : dijkstraStep.Spec g c init heap res) (hMinIdx : heap[minIdx heap] ≠ ⊤) : @@ -678,7 +678,7 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) def dijkstra (g : G) (c : Info → CostType) [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] - (DistArray : Type*) [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) : DistArray := @@ -713,7 +713,7 @@ termination_by Fintype.card {v : V | res[v] = ⊤} lemma dijkstra_spec (g : G) (c : Info → CostType) [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] - (DistArray : Type*) [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤] + (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) (v : V) : g..IsDist c {s | init[s] ≠ ⊤} (fun s hs ↦ init[s].untop hs) v diff --git a/scripts/nolints.json b/scripts/nolints.json index 62e8238..84158d4 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -1,11 +1,11 @@ [["docBlame", "AdjList"], ["docBlame", "AdjListClass"], ["docBlame", "AdjList₂"], - ["docBlame", "AssocArrayWithHeap"], ["docBlame", "Back"], ["docBlame", "Bag"], ["docBlame", "DecidableMem"], ["docBlame", "DefaultAssocDArray"], + ["docBlame", "DefaultDictWithHeap"], ["docBlame", "Dict"], ["docBlame", "Erase"], ["docBlame", "Forest"], @@ -75,24 +75,24 @@ ["docBlame", "AdjListClass.traversal"], ["docBlame", "AdjList₂.costar"], ["docBlame", "AdjList₂.fst"], - ["docBlame", "AssocArray.Ext"], - ["docBlame", "AssocArray.Quotient"], - ["docBlame", "AssocArray.ReadOnly"], - ["docBlame", "AssocArray.indicator"], - ["docBlame", "AssocArray.listIndicator"], - ["docBlame", "AssocArray.toOfFn"], - ["docBlame", "AssocArrayWithHeap.WithIdx"], - ["docBlame", "AssocArrayWithHeap.assocArray"], - ["docBlame", "AssocArrayWithHeap.minHeap"], - ["docBlame", "AssocArrayWithHeap.mk"], ["docBlame", "AssocDArray.ReadOnly"], ["docBlame", "Back.back"], ["docBlame", "Back.back?"], ["docBlame", "Back.backD"], ["docBlame", "Bag.ReadOnly"], - ["docBlame", "Dict.AssocArray"], + ["docBlame", "DefaultDict.Ext"], + ["docBlame", "DefaultDict.Quotient"], + ["docBlame", "DefaultDict.ReadOnly"], + ["docBlame", "DefaultDict.indicator"], + ["docBlame", "DefaultDict.listIndicator"], + ["docBlame", "DefaultDict.toOfFn"], + ["docBlame", "DefaultDictWithHeap.WithIdx"], + ["docBlame", "DefaultDictWithHeap.defaultDict"], + ["docBlame", "DefaultDictWithHeap.minHeap"], + ["docBlame", "DefaultDictWithHeap.mk"], + ["docBlame", "Dict.DefaultDict"], ["docBlame", "Dict.ReadOnly"], - ["docBlame", "Dict.toAssocArray"], + ["docBlame", "Dict.asDefaultDict"], ["docBlame", "Erase.erase"], ["docBlame", "Forest.append"], ["docBlame", "Forest.post"], @@ -149,10 +149,10 @@ ["docBlame", "AdjListClass.Quiver.val"], ["docBlame", "AdjListClass.dijkstra.go"], ["docBlame", "AdjListClass.dijkstraStep.Spec"], - ["docBlame", "AssocArrayWithHeap.WithIdx.idx"], - ["docBlame", "AssocArrayWithHeap.WithIdx.val"], ["docBlame", "AssocDArray.ReadOnly.toDFinsupp'"], ["docBlame", "Bag.ReadOnly.decidableMem"], + ["docBlame", "DefaultDictWithHeap.WithIdx.idx"], + ["docBlame", "DefaultDictWithHeap.WithIdx.val"], ["docBlame", "MultiBag.ReadOnly.count"], ["docBlame", "Quiver.Path.cost"], ["docBlame", "UnionFindImpl.UnionFind.WF"], From 4c030b38447960b64f0897011e882fcb2eb6af18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Sat, 2 Aug 2025 10:11:59 +0800 Subject: [PATCH 2/4] Update Dict.lean --- Algorithm/Data/Classes/Dict.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Algorithm/Data/Classes/Dict.lean b/Algorithm/Data/Classes/Dict.lean index 47b4b94..c75a107 100644 --- a/Algorithm/Data/Classes/Dict.lean +++ b/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.DefaultDict import Algorithm.Data.Classes.Bag +import Algorithm.Data.Classes.DefaultDict import Algorithm.Data.Classes.GetElem variable {C ι α : Type*} From a4a38a477b7c09f2e7147b5ac2b461ec67813ae3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 19:19:49 +0800 Subject: [PATCH 3/4] fix --- Algorithm/Data/Classes/DefaultDict.lean | 57 ++++++++-------------- Algorithm/Data/Classes/Dict.lean | 14 +++--- Algorithm/Data/Classes/IndexedMinHeap.lean | 4 +- Algorithm/Data/Graph/AdjList.lean | 10 ++-- Algorithm/Data/Graph/IsDFSForest.lean | 2 +- Algorithm/Graph/DFS.lean | 42 ++++++++-------- Algorithm/Graph/Dijkstra.lean | 28 +++++------ 7 files changed, 71 insertions(+), 86 deletions(-) diff --git a/Algorithm/Data/Classes/DefaultDict.lean b/Algorithm/Data/Classes/DefaultDict.lean index f50ed86..36bb943 100644 --- a/Algorithm/Data/Classes/DefaultDict.lean +++ b/Algorithm/Data/Classes/DefaultDict.lean @@ -7,14 +7,12 @@ 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 +protected abbrev WithDefault (α : Type*) (n : Nat) (f : Fin n → α) := Vector α n instance {α n f} : Inhabited (Vector.WithDefault α n f) where default := .ofFn f @@ -26,41 +24,31 @@ lemma get_default {f} : (default : Vector.WithDefault α n f).get = f := by 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 DefaultDict.ReadOnly (C : Type*) (ι : outParam Type*) - (α : outParam Type*) (d : outParam α) := - AssocDArray.ReadOnly C ι α (fun _ ↦ d) - -/-- `DefaultDict C ι α d` is a data structure that acts like a finitely supported function - `ι →₀' [α, d]` with single point update operation. -/ -abbrev DefaultDict (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 +67,7 @@ end AssocDArray namespace Vector.WithDefault variable {α : Type*} {n : ℕ} {f : Fin n → α} -instance : AssocDArray (Vector.WithDefault α n f) (Fin n) α f where +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 @@ -92,13 +80,11 @@ end Vector.WithDefault namespace DefaultDict -export AssocDArray (getElem_default) - class Ext (C : Type*) [Inhabited C] (ι : outParam Type*) (α : outParam Type*) - (d : outParam α) [DefaultDict 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 : α} [DefaultDict C ι α d] +variable {C : Type*} [Inhabited C] {ι : Type*} {α : Type*} {d : α} [DefaultDict C ι α fun _ ↦ d] variable (C) @@ -107,7 +93,7 @@ protected def Quotient := @Quotient C (Setoid.ker (fun (a : C) (i : ι) ↦ a[i] instance : Inhabited (DefaultDict.Quotient C) := inferInstanceAs <| Inhabited (@Quotient C (Setoid.ker _)) -instance : DefaultDict (DefaultDict.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] @@ -173,16 +159,15 @@ abbrev toOfFn [Fintype ι] (f : ι → α) : OfFn C ι α f where 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 diff --git a/Algorithm/Data/Classes/Dict.lean b/Algorithm/Data/Classes/Dict.lean index c75a107..6bf07cb 100644 --- a/Algorithm/Data/Classes/Dict.lean +++ b/Algorithm/Data/Classes/Dict.lean @@ -31,18 +31,18 @@ instance : LawfulErase C ι := lawfulErase_iff_toFinset.mpr fun c i ↦ by def Dict.DefaultDict (C : Type*) := C -def Dict.asDefaultDict : C ≃ Dict.DefaultDict C := Equiv.refl _ +def Dict.toDefaultDict : C ≃ Dict.DefaultDict C := Equiv.refl _ instance : Inhabited (Dict.DefaultDict C) where - default := Dict.asDefaultDict ∅ + default := Dict.toDefaultDict ∅ -instance [Dict C ι α] : DefaultDict (Dict.DefaultDict C) ι (Option α) none where - getElem a i _ := (Dict.asDefaultDict.symm a)[i]? - toDFinsupp' a := .mk' ((Dict.asDefaultDict.symm a)[·]?) - (.mk ⟨toMultiset (Dict.asDefaultDict.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.asDefaultDict <| alterElem (Dict.asDefaultDict.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 _) diff --git a/Algorithm/Data/Classes/IndexedMinHeap.lean b/Algorithm/Data/Classes/IndexedMinHeap.lean index 94be03c..85b327f 100644 --- a/Algorithm/Data/Classes/IndexedMinHeap.lean +++ b/Algorithm/Data/Classes/IndexedMinHeap.lean @@ -11,7 +11,7 @@ import Mathlib.Data.Prod.Lex class IndexedMinHeap (C : Type*) [Inhabited C] (ι : outParam Type*) (α : outParam Type*) [Preorder α] [IsTotal α (· ≤ ·)] [OrderTop α] extends - AssocDArray C ι α fun _ ↦ ⊤ where + DefaultDict C ι α fun _ ↦ ⊤ where minIdx : C → ι getElem_minIdx_le c (i : ι) : c[minIdx c] ≤ c[i] decreaseKey (c : C) (i : ι) : ∀ v < c[i], C := fun v _ ↦ c[i ↦ v] @@ -63,7 +63,7 @@ variable {α : Type*} [LinearOrder α] {n : ℕ} [NeZero n] {d : Fin n → α} section ReadOnly -variable [AssocDArray.ReadOnly (Vector α n) (Fin n) α d] +variable [DefaultDict.ReadOnly (Vector α n) (Fin n) α d] abbrev minAux (a : Vector α n) : Lex (α × Fin n) := (⊤ : Finset (Fin n)).inf' ⟨0, Finset.mem_univ 0⟩ (fun i ↦ toLex (a[i], i)) diff --git a/Algorithm/Data/Graph/AdjList.lean b/Algorithm/Data/Graph/AdjList.lean index f347f26..3e12e6f 100644 --- a/Algorithm/Data/Graph/AdjList.lean +++ b/Algorithm/Data/Graph/AdjList.lean @@ -12,7 +12,7 @@ structure AdjList (V : Type*) (Info : Type*) (EColl : Type*) [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl ∅] where + (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] where protected snd : Info → V protected star : StarColl @@ -20,7 +20,7 @@ structure AdjList₂ (V : Type*) (Info : Type*) (EColl : Type*) [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl ∅] extends + (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] extends AdjList V Info EColl StarColl where fst : Info → V costar : StarColl @@ -36,7 +36,7 @@ class AdjListClass (G : Type*) (V : outParam <| Type*) (Info : outParam <| Type*) (EColl : outParam <| Type*) [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - (StarColl : outParam <| Type*) [DefaultDict.ReadOnly StarColl V EColl ∅] where + (StarColl : outParam <| Type*) [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] where snd : G → Info → V star : G → StarColl @@ -56,7 +56,7 @@ variable {V : Type*} {Info : Type*} {EColl : Type*} [ToMultiset EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] instance : AdjListClass (AdjList V Info EColl StarColl) V Info EColl StarColl where snd := AdjList.snd @@ -365,7 +365,7 @@ variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] (g : G) def succList (v : V) : List V := (toList g[v]).map g..snd diff --git a/Algorithm/Data/Graph/IsDFSForest.lean b/Algorithm/Data/Graph/IsDFSForest.lean index ccd98a0..ae471f3 100644 --- a/Algorithm/Data/Graph/IsDFSForest.lean +++ b/Algorithm/Data/Graph/IsDFSForest.lean @@ -14,7 +14,7 @@ variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] {g : G} variable (g) in diff --git a/Algorithm/Graph/DFS.lean b/Algorithm/Graph/DFS.lean index ce5bf11..734deb2 100644 --- a/Algorithm/Graph/DFS.lean +++ b/Algorithm/Graph/DFS.lean @@ -12,7 +12,7 @@ namespace AdjListClass variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] -- 也许在以后可以改成存迭代器 @@ -20,7 +20,7 @@ variable {V : Type*} {Info : Type*} def dfsForest' (g : G) [Fintype V] {BoolArray : Type*} - [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] + [Inhabited BoolArray] [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : Forest V × { b : BoolArray // [DecidableEq V] → (toDFinsupp' visited).support ⊆ (toDFinsupp' b).support } := @@ -55,7 +55,7 @@ decreasing_by lemma roots_dfsForest'_fst_subset (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : (g..dfsForest' vs visited).1.roots ⊆ {v | v ∈ vs} := by match vs with @@ -72,7 +72,7 @@ lemma roots_dfsForest'_fst_subset (g : G) lemma subset_support_toDFinsupp'_dfsForest'_snd (g : G) [DecidableEq V] [Fintype V] {BoolArray : Type*} - [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] + [Inhabited BoolArray] [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : {v | v ∈ vs} ⊆ (toDFinsupp' (g..dfsForest' vs visited).2.val).support := by match vs with @@ -93,7 +93,7 @@ lemma subset_support_toDFinsupp'_dfsForest'_snd (g : G) lemma isDFSForest_dfsForest' (g : G) [DecidableEq V] [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : g..IsDFSForest (toDFinsupp' visited).support @@ -116,14 +116,14 @@ lemma isDFSForest_dfsForest' (g : G) def dfsForest (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : Forest V × BoolArray := (g..dfsForest' vs visited).map id Subtype.val lemma dfsForest_spec' (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] (vs : List V) : + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) : let (f, vis) := (g..dfsForest vs (default : BoolArray)) ([DecidableEq V] → f.support = (toDFinsupp' vis).support) ∧ ∀ v, v ∈ f.support ↔ ∃ r ∈ vs, g..Reachable r v := by @@ -139,7 +139,7 @@ lemma dfsForest_spec' (g : G) lemma dfsForest_spec (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] (vs : List V) : + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) : let (f, vis) := (g..dfsForest vs (default : BoolArray)) f.support = {v : V | vis[v]} ∧ ∀ v : V, vis[v] ↔ ∃ r ∈ vs, g..Reachable r v := by letI : Unique (DecidableEq V) := uniqueOfSubsingleton <| by classical infer_instance @@ -150,8 +150,8 @@ lemma dfsForest_spec (g : G) · ext; simp · simp [H.1] -def dfs' (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] +def dfs' (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : { b : BoolArray // ([DecidableEq V] → (toDFinsupp' visited).support ⊆ (toDFinsupp' b).support) ∧ @@ -186,8 +186,8 @@ decreasing_by simpa using h.trans h₁ simpa [Prod.lex_iff, ← le_iff_lt_or_eq] using this -def dfs (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] +def dfs (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : BoolArray := (g..dfs' vs visited).val @@ -195,20 +195,20 @@ def dfs (g : G) @[simp] lemma dfsForest_snd (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : (g..dfsForest vs visited).snd = g..dfs vs visited := (g..dfs' vs visited).prop.2.symm lemma dfs_spec (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] (vs : List V) : + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) : ∀ v : V, (g..dfs vs (default : BoolArray))[v] ↔ ∃ r ∈ vs, g..Reachable r v := g..dfsForest_snd vs (default : BoolArray) ▸ (g..dfsForest_spec BoolArray vs).2 def dfsForestTR (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List (Forest V × List V)) (visited : BoolArray) : Forest V × BoolArray := match vs with @@ -237,8 +237,8 @@ decreasing_by rw [Finset.subset_iff] simp [*, Function.update] -def dfs'TR (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] +def dfs'TR (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List (List V)) (visited : BoolArray) : BoolArray := match vs with @@ -264,8 +264,8 @@ decreasing_by rw [Finset.subset_iff] simp [*, Function.update] -def dfsTR (g : G) - [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] +def dfsTR (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : BoolArray := match vs with @@ -290,7 +290,7 @@ decreasing_by lemma dfsTR_spec' (g : G) [Fintype V] [DecidableEq V] - {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool false] + {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) (visited : BoolArray) : g..traversal (toDFinsupp' visited).support {v | v ∈ vs ∧ v ∉ (toDFinsupp' visited).support} = g..traversal (toDFinsupp' (g..dfsTR vs visited)).support ∅ := by @@ -316,7 +316,7 @@ lemma dfsTR_spec' (g : G) lemma dfsTR_spec (g : G) [Fintype V] (BoolArray : Type*) [Inhabited BoolArray] - [DefaultDict BoolArray V Bool false] + [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) : g..traversal ∅ {v | v ∈ vs} = {v : V | (g..dfsTR vs (default : BoolArray))[v]} := by letI : DecidableEq V := by classical infer_instance diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean index 3308b92..a07065c 100644 --- a/Algorithm/Graph/Dijkstra.lean +++ b/Algorithm/Graph/Dijkstra.lean @@ -104,7 +104,7 @@ namespace AdjListClass variable {V : Type*} {Info : Type*} {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl] [LawfulEmptyCollection EColl Info] - {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl ∅] + {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] {G : Type*} [AdjListClass G V Info EColl StarColl] {CostType : Type*} @@ -373,7 +373,7 @@ lemma isDist_union {g : G} def dijkstraStep (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) : @@ -388,7 +388,7 @@ def dijkstraStep (g : G) (c : Info → CostType) structure dijkstraStep.Spec (g : G) (c : Info → CostType) [AddMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) (heap : DistHeap) (res : DistArray) : Prop where h₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤ @@ -402,7 +402,7 @@ structure dijkstraStep.Spec (g : G) (c : Info → CostType) lemma dijkstraStep_snd_getElem (g : G) (c : Info → CostType) [DecidableEq V] [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) : (dijkstraStep g c heap res hMinIdx).2[v] = @@ -411,7 +411,7 @@ lemma dijkstraStep_snd_getElem (g : G) (c : Info → CostType) lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) : (dijkstraStep g c heap res hMinIdx).2[v] = ⊤ ↔ @@ -424,7 +424,7 @@ lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType) lemma dijkstraStep_snd_support (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) : {v : V | (dijkstraStep g c heap res hMinIdx).2[v] ≠ ⊤} = @@ -435,7 +435,7 @@ lemma dijkstraStep_snd_support (g : G) (c : Info → CostType) lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType) [DecidableEq V] [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : @@ -473,7 +473,7 @@ lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType) lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType) [DecidableEq V] [DecidableEq Info] [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : @@ -499,7 +499,7 @@ lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType) lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : @@ -522,7 +522,7 @@ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType) lemma dijkstraStep_fst_support (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) : @@ -537,7 +537,7 @@ lemma dijkstraStep_fst_support (g : G) (c : Info → CostType) lemma dijkstraStep_spec (g : G) (c : Info → CostType) [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] - {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) (heap : DistHeap) (res : DistArray) (h : dijkstraStep.Spec g c init heap res) (hMinIdx : heap[minIdx heap] ≠ ⊤) : @@ -680,7 +680,7 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) def dijkstra (g : G) (c : Info → CostType) [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] - (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) : DistArray := @@ -704,7 +704,7 @@ termination_by Fintype.card {v : V | res[v] = ⊤} spec_init : dijkstraStep.Spec g c init init default := by constructor · simp - · simp only [AssocDArray.getElem_default, ne_eq, + · simp only [DefaultDict.getElem_default, ne_eq, not_true_eq_false, IsEmpty.forall_iff, implies_true, and_true, Set.mem_setOf_eq, forall_true_left] intro h @@ -715,7 +715,7 @@ termination_by Fintype.card {v : V | res[v] = ⊤} lemma dijkstra_spec (g : G) (c : Info → CostType) [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] - (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) ⊤] + (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤] {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)] (init : DistHeap) (v : V) : g..IsDist c {s | init[s] ≠ ⊤} (fun s hs ↦ init[s].untop hs) v From 0e7fd65b0e3c80ec49522dd79efc1eadb5106c40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 2 Jan 2026 09:26:10 +0800 Subject: [PATCH 4/4] fix --- Algorithm/Data/Classes/DefaultDict.lean | 16 ++++++++-------- scripts/nolints.json | 11 +++++------ test/UnionFind.lean | 1 - 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/Algorithm/Data/Classes/DefaultDict.lean b/Algorithm/Data/Classes/DefaultDict.lean index 36bb943..dbfecf8 100644 --- a/Algorithm/Data/Classes/DefaultDict.lean +++ b/Algorithm/Data/Classes/DefaultDict.lean @@ -14,14 +14,6 @@ set_option linter.unusedVariables false in -- TODO: generalize @[nolint unusedArguments] protected abbrev WithDefault (α : Type*) (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 - end Vector class DefaultDict.ReadOnly (C : Type*) (ι : outParam Type*) @@ -67,6 +59,14 @@ end AssocDArray namespace Vector.WithDefault variable {α : Type*} {n : ℕ} {f : Fin 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 + instance : DefaultDict (Vector.WithDefault α n f) (Fin n) α f where getElem a i _ := a.get i setElem a i := a.set i diff --git a/scripts/nolints.json b/scripts/nolints.json index 85220c6..22297a4 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -4,7 +4,6 @@ ["docBlame", "Back"], ["docBlame", "Bag"], ["docBlame", "DecidableMem"], - ["docBlame", "DefaultAssocDArray"], ["docBlame", "DefaultDictWithHeap"], ["docBlame", "Dict"], ["docBlame", "Erase"], @@ -15,7 +14,7 @@ ["docBlame", "GetSetElemAllValid"], ["docBlame", "GetSetEraseElem"], ["docBlame", "GetSetEraseElem?"], - ["docBlame", "HasDefaultAssocDArray"], + ["docBlame", "HasDefaultDict"], ["docBlame", "HasValid"], ["docBlame", "IndexedMinHeap"], ["docBlame", "LawfulAppend"], @@ -39,6 +38,7 @@ ["docBlame", "alterElem"], ["docBlame", "decreaseKeyD"], ["docBlame", "decreaseKeysD"], + ["docBlame", "mkDefaultDict"], ["docBlame", "modifyElem"], ["docBlame", "«term__[_=>_]»"], ["docBlame", "«term__[_↦_]»"], @@ -75,7 +75,6 @@ ["docBlame", "AdjListClass.traversal"], ["docBlame", "AdjList₂.costar"], ["docBlame", "AdjList₂.fst"], - ["docBlame", "AssocDArray.ReadOnly"], ["docBlame", "Back.back"], ["docBlame", "Back.back?"], ["docBlame", "Back.backD"], @@ -92,7 +91,7 @@ ["docBlame", "DefaultDictWithHeap.mk"], ["docBlame", "Dict.DefaultDict"], ["docBlame", "Dict.ReadOnly"], - ["docBlame", "Dict.asDefaultDict"], + ["docBlame", "Dict.toDefaultDict"], ["docBlame", "Erase.erase"], ["docBlame", "Forest.append"], ["docBlame", "Forest.post"], @@ -102,7 +101,7 @@ ["docBlame", "Front.front"], ["docBlame", "Front.front?"], ["docBlame", "Front.frontD"], - ["docBlame", "HasDefaultAssocDArray.toAssocDArray"], + ["docBlame", "HasDefaultDict.toDefaultDict"], ["docBlame", "HasValid.Valid"], ["docBlame", "IndexedMinHeap.decreaseKey"], ["docBlame", "IndexedMinHeap.minIdx"], @@ -149,8 +148,8 @@ ["docBlame", "AdjListClass.Quiver.val"], ["docBlame", "AdjListClass.dijkstra.go"], ["docBlame", "AdjListClass.dijkstraStep.Spec"], - ["docBlame", "AssocDArray.ReadOnly.toDFinsupp'"], ["docBlame", "Bag.ReadOnly.decidableMem"], + ["docBlame", "DefaultDict.ReadOnly.toDFinsupp'"], ["docBlame", "DefaultDictWithHeap.WithIdx.idx"], ["docBlame", "DefaultDictWithHeap.WithIdx.val"], ["docBlame", "Membership.IsEmpty.isEmpty"], diff --git a/test/UnionFind.lean b/test/UnionFind.lean index a23f4ca..0b9b047 100644 --- a/test/UnionFind.lean +++ b/test/UnionFind.lean @@ -1,6 +1,5 @@ import Algorithm.Data.UnionFind -abbrev Vector := Batteries.Vector abbrev UF := UnionFind (Fin 10) (Vector (Fin 10) 10) (Vector Nat 10) /--