diff --git a/src/Lean/Compiler/LCNF/FloatLetIn.lean b/src/Lean/Compiler/LCNF/FloatLetIn.lean index 0ef04b1896..b3e67d05cb 100644 --- a/src/Lean/Compiler/LCNF/FloatLetIn.lean +++ b/src/Lean/Compiler/LCNF/FloatLetIn.lean @@ -117,7 +117,7 @@ up to this point, with respect to `cs`. The initial decisions are: - `unknown` otherwise -/ def initialDecisions (cs : Cases) : BaseFloatM (Std.HashMap FVarId Decision) := do - let mut map := Std.HashMap.empty (← read).decls.length + let mut map := Std.HashMap.emptyWithCapacity (← read).decls.length let folder val acc := do if let .let decl := val then if (← ignore? decl) then @@ -148,7 +148,7 @@ Compute the initial new arms. This will just set up a map from all arms of `cs` to empty `Array`s, plus one additional entry for `dont`. -/ def initialNewArms (cs : Cases) : Std.HashMap Decision (List CodeDecl) := Id.run do - let mut map := Std.HashMap.empty (cs.alts.size + 1) + let mut map := Std.HashMap.emptyWithCapacity (cs.alts.size + 1) map := map.insert .dont [] cs.alts.foldr (init := map) fun val acc => acc.insert (.ofAlt val) [] diff --git a/src/Lean/Compiler/LCNF/Probing.lean b/src/Lean/Compiler/LCNF/Probing.lean index 68ee340d6c..659be13f63 100644 --- a/src/Lean/Compiler/LCNF/Probing.lean +++ b/src/Lean/Compiler/LCNF/Probing.lean @@ -30,7 +30,7 @@ def sortedBySize : Probe Decl (Nat × Decl) := fun decls => if sz₁ == sz₂ then Name.lt decl₁.name decl₂.name else sz₁ < sz₂ def countUnique [ToString α] [BEq α] [Hashable α] : Probe α (α × Nat) := fun data => do - let mut map := Std.HashMap.empty + let mut map := Std.HashMap.emptyWithCapacity data.size for d in data do if let some count := map[d]? then map := map.insert d (count + 1) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean index 34ea1b279a..25d7e52a65 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean @@ -116,7 +116,7 @@ def markUninterestingConst (n : Name) : PreProcessM Unit := do @[inline] def run (cfg : BVDecideConfig) (goal : MVarId) (x : PreProcessM α) : MetaM α := do let hyps ← goal.withContext do getPropHyps - ReaderT.run x cfg |>.run' { rewriteCache := Std.HashSet.empty hyps.size } + ReaderT.run x cfg |>.run' { rewriteCache := Std.HashSet.emptyWithCapacity hyps.size } end PreProcessM diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean index 31537fd25e..b3df223386 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean @@ -122,7 +122,7 @@ where let argTypes := relevantTerms.map (fun _ => (`x, argType)) let innerMotiveType ← withLocalDeclsDND argTypes fun args => do - let mut subst : Std.HashMap Expr Expr := Std.HashMap.empty (args.size + 1) + let mut subst : Std.HashMap Expr Expr := Std.HashMap.emptyWithCapacity (args.size + 1) subst := subst.insert (mkConst ``System.Platform.numBits) z for term in relevantTerms, arg in args do subst := subst.insert term arg diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index bcedcebf87..74e85650e5 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1767,8 +1767,8 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) ( (leakEnv := false) : IO Environment := do let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod => numConsts + mod.constants.size + mod.extraConstNames.size - let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts) - let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts) + let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numConsts) + let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numConsts) for h : modIdx in [0:s.moduleData.size] do let mod := s.moduleData[modIdx] for cname in mod.constNames, cinfo in mod.constants do diff --git a/src/Lean/Namespace.lean b/src/Lean/Namespace.lean index 8d8e466d31..fbb984d4a9 100644 --- a/src/Lean/Namespace.lean +++ b/src/Lean/Namespace.lean @@ -20,7 +20,7 @@ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet 6.18% of the runtime is here. It was 9.31% before the `HashMap` optimization. -/ let capacity := as.foldl (init := 0) fun r e => r + e.size - let map : Std.HashMap Name Unit := Std.HashMap.empty capacity + let map : Std.HashMap Name Unit := Std.HashMap.emptyWithCapacity capacity let map := mkStateFromImportedEntries (fun map name => map.insert name ()) map as SMap.fromHashMap map |>.switch addEntryFn := fun s n => s.insert n diff --git a/src/Lean/Util/PtrSet.lean b/src/Lean/Util/PtrSet.lean index 56e57aeb06..1a9e3bff55 100644 --- a/src/Lean/Util/PtrSet.lean +++ b/src/Lean/Util/PtrSet.lean @@ -28,7 +28,7 @@ unsafe def PtrSet (α : Type) := Std.HashSet (Ptr α) unsafe def mkPtrSet {α : Type} (capacity : Nat := 64) : PtrSet α := - Std.HashSet.empty capacity + Std.HashSet.emptyWithCapacity capacity unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α := Std.HashSet.insert s { value := a } @@ -43,7 +43,7 @@ unsafe def PtrMap (α : Type) (β : Type) := Std.HashMap (Ptr α) β unsafe def mkPtrMap {α β : Type} (capacity : Nat := 64) : PtrMap α β := - Std.HashMap.empty capacity + Std.HashMap.emptyWithCapacity capacity unsafe abbrev PtrMap.insert (s : PtrMap α β) (a : α) (b : β) : PtrMap α β := Std.HashMap.insert s { value := a } b diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean index 3a508533fd..34747a71f2 100644 --- a/src/Lean/Util/ShareCommon.lean +++ b/src/Lean/Util/ShareCommon.lean @@ -15,8 +15,8 @@ namespace Lean.ShareCommon def objectFactory := StateFactory.mk { - Map := Std.HashMap, mkMap := (Std.HashMap.empty ·), mapFind? := (·.get?), mapInsert := (·.insert) - Set := Std.HashSet, mkSet := (Std.HashSet.empty ·), setFind? := (·.get?), setInsert := (·.insert) + Map := Std.HashMap, mkMap := (Std.HashMap.emptyWithCapacity ·), mapFind? := (·.get?), mapInsert := (·.insert) + Set := Std.HashSet, mkSet := (Std.HashSet.emptyWithCapacity ·), setFind? := (·.get?), setInsert := (·.insert) } def persistentObjectFactory := diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 36cf5e427b..c63a1c9bc6 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -62,11 +62,14 @@ def DHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] := { m : namespace DHashMap -@[inline, inherit_doc Raw.empty] def empty [BEq α] [Hashable α] (capacity := 8) : DHashMap α β := - ⟨Raw.empty capacity, .empty₀⟩ +@[inline, inherit_doc Raw.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : DHashMap α β := + ⟨Raw.emptyWithCapacity capacity, .emptyWithCapacity₀⟩ + +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where - emptyCollection := empty + emptyCollection := emptyWithCapacity instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where default := ∅ @@ -82,7 +85,7 @@ structure Equiv (m₁ m₂ : DHashMap α β) where (b : β a) : DHashMap α β := ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩ -instance : Singleton ((a : α) × β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ => DHashMap.empty.insert a b⟩ +instance : Singleton ((a : α) × β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ => (∅ : DHashMap α β).insert a b⟩ instance : Insert ((a : α) × β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩ diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index a7f6f746b8..07212ed078 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -170,10 +170,13 @@ abbrev Raw₀ (α : Type u) (β : α → Type v) := namespace Raw₀ /-- Internal implementation detail of the hash map -/ -@[inline] def empty (capacity := 8) : Raw₀ α β := +@[inline] def emptyWithCapacity (capacity := 8) : Raw₀ α β := ⟨⟨0, mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil⟩, by simpa using Nat.pos_of_isPowerOfTwo (Nat.isPowerOfTwo_nextPowerOfTwo _)⟩ +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity + -- Take `hash` as a function instead of `Hashable α` as per -- https://github.com/leanprover/lean4/issues/4191 /-- Internal implementation detail of the hash map -/ diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index a1f5fb2466..80089cfdf6 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -24,9 +24,11 @@ namespace Std.DHashMap.Internal namespace Raw -theorem empty_eq [BEq α] [Hashable α] {c : Nat} : (Raw.empty c : Raw α β) = (Raw₀.empty c).1 := rfl +-- TODO: the next two lemmas need to be renamed, but there is a bootstrapping obstacle. -theorem emptyc_eq [BEq α] [Hashable α] : (∅ : Raw α β) = Raw₀.empty.1 := rfl +theorem empty_eq [BEq α] [Hashable α] {c : Nat} : (Raw.emptyWithCapacity c : Raw α β) = (Raw₀.emptyWithCapacity c).1 := rfl + +theorem emptyc_eq [BEq α] [Hashable α] : (∅ : Raw α β) = Raw₀.emptyWithCapacity.1 := rfl theorem insert_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : m.insert a b = (Raw₀.insert ⟨m, h.size_buckets_pos⟩ a b).1 := by @@ -122,7 +124,7 @@ theorem insertMany_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Ty simp [Raw.insertMany, h.size_buckets_pos] theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} : - Raw.ofList l = Raw₀.insertMany Raw₀.empty l := by + Raw.ofList l = Raw₀.insertMany Raw₀.emptyWithCapacity l := by simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte] congr @@ -143,7 +145,7 @@ theorem Const.insertMany_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h simp [Raw.Const.insertMany, h.size_buckets_pos] theorem Const.ofList_eq [BEq α] [Hashable α] {l : List (α × β)} : - Raw.Const.ofList l = Raw₀.Const.insertMany Raw₀.empty l := by + Raw.Const.ofList l = Raw₀.Const.insertMany Raw₀.emptyWithCapacity l := by simp only [Raw.Const.ofList, Raw.Const.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte] congr @@ -153,7 +155,7 @@ theorem Const.insertManyIfNewUnit_eq {ρ : Type w} [ForIn Id ρ α] [BEq α] [Ha simp [Raw.Const.insertManyIfNewUnit, h.size_buckets_pos] theorem Const.unitOfList_eq [BEq α] [Hashable α] {l : List α} : - Raw.Const.unitOfList l = Raw₀.Const.insertManyIfNewUnit Raw₀.empty l := by + Raw.Const.unitOfList l = Raw₀.Const.insertManyIfNewUnit Raw₀.emptyWithCapacity l := by simp only [Raw.Const.unitOfList, Raw.Const.insertManyIfNewUnit, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte] congr diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index a2912a2e32..a0bdc17759 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -28,31 +28,43 @@ namespace Std.DHashMap.Internal section empty @[simp] -theorem Raw₀.buckets_empty {c} {i : Nat} {h} : - (empty c : Raw₀ α β).1.buckets[i]'h = AssocList.nil := by - simp [empty] +theorem Raw₀.buckets_emptyWithCapacity {c} {i : Nat} {h} : + (emptyWithCapacity c : Raw₀ α β).1.buckets[i]'h = AssocList.nil := by + simp [emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated Raw₀.buckets_emptyWithCapacity (since := "2025-03-12")] +abbrev Raw₀.buckets_empty := @Raw₀.buckets_emptyWithCapacity @[simp] -theorem Raw.buckets_empty {c} {i : Nat} {h} : - (Raw.empty c : Raw α β).buckets[i]'h = AssocList.nil := by - simp [Raw.empty] +theorem Raw.buckets_emptyWithCapacity {c} {i : Nat} {h} : + (Raw.emptyWithCapacity c : Raw α β).buckets[i]'h = AssocList.nil := by + simp [Raw.emptyWithCapacity] @[simp] -theorem Raw.buckets_emptyc {i : Nat} {h} : +theorem Raw.buckets_empty {i : Nat} {h} : (∅ : Raw α β).buckets[i]'h = AssocList.nil := - buckets_empty + buckets_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated Raw.buckets_empty (since := "2025-03-12")] +abbrev Raw.buckets_emptyc := @Raw.buckets_empty variable [BEq α] [Hashable α] @[simp] -theorem buckets_empty {c} {i : Nat} {h} : - (empty c : DHashMap α β).1.buckets[i]'h = AssocList.nil := by - simp [empty] +theorem buckets_emptyWithCapacity {c} {i : Nat} {h} : + (emptyWithCapacity c : DHashMap α β).1.buckets[i]'h = AssocList.nil := by + simp [emptyWithCapacity] @[simp] -theorem buckets_emptyc {i : Nat} {h} : +theorem buckets_empty {i : Nat} {h} : (∅ : DHashMap α β).1.buckets[i]'h = AssocList.nil := - buckets_empty + buckets_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated buckets_empty (since := "2025-03-12")] +abbrev buckets_emptyc := @buckets_empty end empty @@ -61,7 +73,11 @@ namespace Raw₀ variable (m : Raw₀ α β) @[simp] -theorem size_empty {c} : (empty c : Raw₀ α β).1.size = 0 := rfl +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.size = 0 := rfl + +set_option linter.missingDocs false in +@[deprecated size_emptyWithCapacity (since := "2025-03-12")] +abbrev size_empty := @size_emptyWithCapacity theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by simp [Raw.isEmpty] @@ -83,7 +99,7 @@ macro_rules | apply Raw₀.Const.wf_insertManyIfNewUnit₀ | apply Raw.WF.filter₀ -- TODO: map₀ and filterMap₀ - | apply Raw.WF.empty₀) <;> wf_trivial) + | apply Raw.WF.emptyWithCapacity₀) <;> wf_trivial) /-- Internal implementation detail of the hash map -/ scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } ) @@ -166,8 +182,12 @@ macro_rules <;> with_reducible try wf_trivial) @[simp] -theorem isEmpty_empty {c} : (empty c : Raw₀ α β).1.isEmpty := by - rw [Raw.isEmpty_eq_isEmpty wfImp_empty, toListModel_buckets_empty, List.isEmpty_nil] +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.isEmpty := by + rw [Raw.isEmpty_eq_isEmpty wfImp_emptyWithCapacity, toListModel_buckets_emptyWithCapacity, List.isEmpty_nil] + +set_option linter.missingDocs false in +@[deprecated isEmpty_emptyWithCapacity (since := "2025-03-12")] +abbrev isEmpty_empty := @isEmpty_emptyWithCapacity @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} : @@ -179,9 +199,13 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} simp_to_model [contains] using List.containsKey_congr hab @[simp] -theorem contains_empty {a : α} {c : Nat} : (empty c : Raw₀ α β).contains a = false := by +theorem contains_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : Raw₀ α β).contains a = false := by simp [contains] +set_option linter.missingDocs false in +@[deprecated contains_emptyWithCapacity (since := "2025-03-12")] +abbrev contains_empty := @contains_emptyWithCapacity + theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} : m.1.isEmpty = true → m.contains a = false := by simp_to_model [isEmpty, contains]; empty @@ -219,8 +243,12 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} { simp_to_model [insert, size] using List.length_insertEntry_le @[simp] -theorem erase_empty {k : α} {c : Nat} : (empty c : Raw₀ α β).erase k = empty c := by - simp [erase, empty] +theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw₀ α β).erase k = emptyWithCapacity c := by + simp [erase, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated erase_emptyWithCapacity (since := "2025-03-12")] +abbrev erase_empty := @erase_emptyWithCapacity theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} : (m.erase k).1.isEmpty = (m.1.isEmpty || (m.1.size == 1 && m.contains k)) := by @@ -265,9 +293,13 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β k} : rw [containsThenInsertIfNew_eq_insertIfNewₘ, insertIfNew_eq_insertIfNewₘ] @[simp] -theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw₀ α β).get? a = none := by +theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : Raw₀ α β).get? a = none := by simp [get?] +set_option linter.missingDocs false in +@[deprecated get?_emptyWithCapacity (since := "2025-03-12")] +abbrev get?_empty := @get?_emptyWithCapacity + theorem get?_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} : m.1.isEmpty = true → m.get? a = none := by simp_to_model [isEmpty, get?]; empty @@ -300,9 +332,13 @@ namespace Const variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF) @[simp] -theorem get?_empty {a : α} {c} : get? (empty c : Raw₀ α (fun _ => β)) a = none := by +theorem get?_emptyWithCapacity {a : α} {c} : get? (emptyWithCapacity c : Raw₀ α (fun _ => β)) a = none := by simp [get?] +set_option linter.missingDocs false in +@[deprecated get?_emptyWithCapacity (since := "2025-03-12")] +abbrev get?_empty := @get?_emptyWithCapacity + theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} : m.1.isEmpty = true → get? m a = none := by simp_to_model [isEmpty, Const.get?]; empty @@ -392,9 +428,13 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab end Const -theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : - (empty c : Raw₀ α β).get! a = default := by - simp [get!, empty] +theorem get!_emptyWithCapacity [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : + (emptyWithCapacity c : Raw₀ α β).get! a = default := by + simp [get!, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated get!_emptyWithCapacity (since := "2025-03-12")] +abbrev get!_empty := @get!_emptyWithCapacity theorem get!_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] : m.1.isEmpty = true → m.get! a = default := by @@ -437,9 +477,13 @@ namespace Const variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF) -theorem get!_empty [Inhabited β] {a : α} {c} : - get! (empty c : Raw₀ α (fun _ => β)) a = default := by - simp [get!, empty] +theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} : + get! (emptyWithCapacity c : Raw₀ α (fun _ => β)) a = default := by + simp [get!, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated get!_emptyWithCapacity (since := "2025-03-12")] +abbrev get!_empty := @get!_emptyWithCapacity theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} : m.1.isEmpty = true → get! m a = default := by @@ -487,9 +531,13 @@ theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) end Const -theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} : - (empty c : Raw₀ α β).getD a fallback = fallback := by - simp [getD, empty] +theorem getD_emptyWithCapacity [LawfulBEq α] {a : α} {fallback : β a} {c} : + (emptyWithCapacity c : Raw₀ α β).getD a fallback = fallback := by + simp [getD, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated getD_emptyWithCapacity (since := "2025-03-12")] +abbrev getD_empty := @getD_emptyWithCapacity theorem getD_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} : m.1.isEmpty = true → m.getD a fallback = fallback := by @@ -536,9 +584,13 @@ namespace Const variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF) -theorem getD_empty {a : α} {fallback : β} {c} : - getD (empty c : Raw₀ α (fun _ => β)) a fallback = fallback := by - simp [getD, empty] +theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : + getD (emptyWithCapacity c : Raw₀ α (fun _ => β)) a fallback = fallback := by + simp [getD, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated getD_emptyWithCapacity (since := "2025-03-12")] +abbrev getD_empty := @getD_emptyWithCapacity theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} : m.1.isEmpty = true → getD m a fallback = fallback := by @@ -591,9 +643,13 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} {fa end Const @[simp] -theorem getKey?_empty {a : α} {c} : (empty c : Raw₀ α β).getKey? a = none := by +theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw₀ α β).getKey? a = none := by simp [getKey?] +set_option linter.missingDocs false in +@[deprecated getKey?_emptyWithCapacity (since := "2025-03-12")] +abbrev getKey?_empty := @getKey?_emptyWithCapacity + theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} : m.1.isEmpty = true → m.getKey? a = none := by simp_to_model [getKey?, isEmpty]; empty @@ -669,9 +725,13 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a m.getKey? a = some (m.getKey a h') := by simp_to_model [getKey?, getKey] using List.getKey?_eq_some_getKey -theorem getKey!_empty {a : α} [Inhabited α] {c} : - (empty c : Raw₀ α β).getKey! a = default := by - simp [getKey!, empty] +theorem getKey!_emptyWithCapacity {a : α} [Inhabited α] {c} : + (emptyWithCapacity c : Raw₀ α β).getKey! a = default := by + simp [getKey!, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated getKey!_emptyWithCapacity (since := "2025-03-12")] +abbrev getKey!_empty := @getKey!_emptyWithCapacity theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} : m.1.isEmpty = true → m.getKey! a = default := by @@ -718,9 +778,13 @@ theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.1.WF) {k : m.contains k → m.getKey! k = k := by simp_to_model [getKey!, contains] using List.getKey!_eq_of_containsKey -theorem getKeyD_empty {a : α} {fallback : α} {c} : - (empty c : Raw₀ α β).getKeyD a fallback = fallback := by - simp [getKeyD, empty] +theorem getKeyD_emptyWithCapacity {a : α} {fallback : α} {c} : + (emptyWithCapacity c : Raw₀ α β).getKeyD a fallback = fallback := by + simp [getKeyD, emptyWithCapacity] + +set_option linter.missingDocs false in +@[deprecated getKeyD_emptyWithCapacity (since := "2025-03-12")] +abbrev getKeyD_empty := @getKeyD_emptyWithCapacity theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} : m.1.isEmpty = true → m.getKeyD a fallback = fallback := by @@ -1603,405 +1667,645 @@ theorem getD_insertManyIfNewUnit_list end Const @[simp] -theorem insertMany_empty_list_nil : - (insertMany empty ([] : List ((a : α) × (β a)))).1 = empty := by +theorem insertMany_emptyWithCapacity_list_nil : + (insertMany emptyWithCapacity ([] : List ((a : α) × (β a)))).1 = emptyWithCapacity := by simp +set_option linter.missingDocs false in +@[deprecated insertMany_emptyWithCapacity_list_nil (since := "2025-03-12")] +abbrev insertMany_empty_list_nil := @insertMany_emptyWithCapacity_list_nil + @[simp] -theorem insertMany_empty_list_singleton {k : α} {v : β k} : - (insertMany empty [⟨k, v⟩]).1 = empty.insert k v := by +theorem insertMany_emptyWithCapacity_list_singleton {k : α} {v : β k} : + (insertMany emptyWithCapacity [⟨k, v⟩]).1 = emptyWithCapacity.insert k v := by simp -theorem insertMany_empty_list_cons {k : α} {v : β k} +set_option linter.missingDocs false in +@[deprecated insertMany_emptyWithCapacity_list_singleton (since := "2025-03-12")] +abbrev insertMany_empty_list_singleton := @insertMany_emptyWithCapacity_list_singleton + +theorem insertMany_emptyWithCapacity_list_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} : - (insertMany empty (⟨k, v⟩ :: tl)).1 = ((empty.insert k v).insertMany tl).1 := by + (insertMany emptyWithCapacity (⟨k, v⟩ :: tl)).1 = ((emptyWithCapacity.insert k v).insertMany tl).1 := by rw [insertMany_cons] -theorem contains_insertMany_empty_list [EquivBEq α] [LawfulHashable α] - {l : List ((a : α) × β a)} {k : α} : - (insertMany empty l).1.contains k = (l.map Sigma.fst).contains k := by - simp [contains_insertMany_list _ Raw.WF.empty₀] +set_option linter.missingDocs false in +@[deprecated insertMany_emptyWithCapacity_list_cons (since := "2025-03-12")] +abbrev insertMany_empty_list_cons := @insertMany_emptyWithCapacity_list_cons -theorem get?_insertMany_empty_list_of_contains_eq_false [LawfulBEq α] +theorem contains_insertMany_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] + {l : List ((a : α) × β a)} {k : α} : + (insertMany emptyWithCapacity l).1.contains k = (l.map Sigma.fst).contains k := by + simp [contains_insertMany_list _ Raw.WF.emptyWithCapacity₀] + +set_option linter.missingDocs false in +@[deprecated contains_insertMany_emptyWithCapacity_list (since := "2025-03-12")] +abbrev contains_insertMany_empty_list := @contains_insertMany_emptyWithCapacity_list + +theorem get?_insertMany_emptyWithCapacity_list_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (h : (l.map Sigma.fst).contains k = false) : - (insertMany empty l).1.get? k = none := by - simp [get?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] + (insertMany emptyWithCapacity l).1.get? k = none := by + simp [get?_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] -theorem get?_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev get?_insertMany_empty_list_of_contains_eq_false := @get?_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem get?_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : - (insertMany empty l).1.get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by - rw [get?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by + rw [get?_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem get_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev get?_insertMany_empty_list_of_mem := @get?_insertMany_emptyWithCapacity_list_of_mem + +theorem get_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) {h} : - (insertMany empty l).1.get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by - rw [get_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by + rw [get_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem get!_insertMany_empty_list_of_contains_eq_false [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev get_insertMany_empty_list_of_mem := @get_insertMany_emptyWithCapacity_list_of_mem + +theorem get!_insertMany_emptyWithCapacity_list_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h : (l.map Sigma.fst).contains k = false) : - (insertMany empty l).1.get! k = default := by - simp only [get!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply get!_empty + (insertMany emptyWithCapacity l).1.get! k = default := by + simp only [get!_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply get!_emptyWithCapacity -theorem get!_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev get!_insertMany_empty_list_of_contains_eq_false := @get!_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem get!_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : - (insertMany empty l).1.get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by - rw [get!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by + rw [get!_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getD_insertMany_empty_list_of_contains_eq_false [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev get!_insertMany_empty_list_of_mem := @get!_insertMany_emptyWithCapacity_list_of_mem + +theorem getD_insertMany_emptyWithCapacity_list_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (l.map Sigma.fst).contains k = false) : - (insertMany empty l).1.getD k fallback = fallback := by - rw [getD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ contains_eq_false] - apply getD_empty + (insertMany emptyWithCapacity l).1.getD k fallback = fallback := by + rw [getD_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ contains_eq_false] + apply getD_emptyWithCapacity -theorem getD_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated getD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getD_insertMany_empty_list_of_contains_eq_false := @getD_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getD_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : - (insertMany empty l).1.getD k' fallback = + (insertMany emptyWithCapacity l).1.getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by - rw [getD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + rw [getD_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKey?_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getD_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getD_insertMany_empty_list_of_mem := @getD_insertMany_emptyWithCapacity_list_of_mem + +theorem getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (h : (l.map Sigma.fst).contains k = false) : - (insertMany empty l).1.getKey? k = none := by - rw [getKey?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply getKey?_empty + (insertMany emptyWithCapacity l).1.getKey? k = none := by + rw [getKey?_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply getKey?_emptyWithCapacity -theorem getKey?_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKey?_insertMany_empty_list_of_contains_eq_false := @getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getKey?_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : - (insertMany empty l).1.getKey? k' = some k := by - rw [getKey?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.getKey? k' = some k := by + rw [getKey?_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKey_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey?_insertMany_empty_list_of_mem := @getKey?_insertMany_emptyWithCapacity_list_of_mem + +theorem getKey_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) {h'} : - (insertMany empty l).1.getKey k' h' = k := by - rw [getKey_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.getKey k' h' = k := by + rw [getKey_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKey!_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey_insertMany_empty_list_of_mem := @getKey_insertMany_emptyWithCapacity_list_of_mem + +theorem getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (h : (l.map Sigma.fst).contains k = false) : - (insertMany empty l).1.getKey! k = default := by - rw [getKey!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply getKey!_empty + (insertMany emptyWithCapacity l).1.getKey! k = default := by + rw [getKey!_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply getKey!_emptyWithCapacity -theorem getKey!_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] +set_option linter.missingDocs false in +@[deprecated getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKey!_insertMany_empty_list_of_contains_eq_false := @getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getKey!_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : - (insertMany empty l).1.getKey! k' = k := by - rw [getKey!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.getKey! k' = k := by + rw [getKey!_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKeyD_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey!_insertMany_empty_list_of_mem := @getKey!_insertMany_emptyWithCapacity_list_of_mem + +theorem getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (h : (l.map Sigma.fst).contains k = false) : - (insertMany empty l).1.getKeyD k fallback = fallback := by - rw [getKeyD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply getKeyD_empty + (insertMany emptyWithCapacity l).1.getKeyD k fallback = fallback := by + rw [getKeyD_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply getKeyD_emptyWithCapacity -theorem getKeyD_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKeyD_insertMany_empty_list_of_contains_eq_false := @getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getKeyD_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : - (insertMany empty l).1.getKeyD k' fallback = k := by - rw [getKeyD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany emptyWithCapacity l).1.getKeyD k' fallback = k := by + rw [getKeyD_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem size_insertMany_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKeyD_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKeyD_insertMany_empty_list_of_mem := @getKeyD_insertMany_emptyWithCapacity_list_of_mem + +theorem size_insertMany_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : - (insertMany empty l).1.1.size = l.length := by - rw [size_insertMany_list _ Raw.WF.empty₀ distinct] - · simp only [size_empty, Nat.zero_add] - · simp only [contains_empty, Bool.false_eq_true, false_implies, implies_true] + (insertMany emptyWithCapacity l).1.1.size = l.length := by + rw [size_insertMany_list _ Raw.WF.emptyWithCapacity₀ distinct] + · simp only [size_emptyWithCapacity, Nat.zero_add] + · simp only [contains_emptyWithCapacity, Bool.false_eq_true, false_implies, implies_true] -theorem size_insertMany_empty_list_le [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated size_insertMany_emptyWithCapacity_list (since := "2025-03-12")] +abbrev size_insertMany_empty_list := @size_insertMany_emptyWithCapacity_list + +theorem size_insertMany_emptyWithCapacity_list_le [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : - (insertMany empty l).1.1.size ≤ l.length := by + (insertMany emptyWithCapacity l).1.1.size ≤ l.length := by rw [← Nat.zero_add l.length] - apply (size_insertMany_list_le _ Raw.WF.empty₀) + apply (size_insertMany_list_le _ Raw.WF.emptyWithCapacity₀) -theorem isEmpty_insertMany_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated size_insertMany_emptyWithCapacity_list_le (since := "2025-03-12")] +abbrev size_insertMany_empty_list_le := @size_insertMany_emptyWithCapacity_list_le + +theorem isEmpty_insertMany_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : - (insertMany empty l).1.1.isEmpty = l.isEmpty := by - simp [isEmpty_insertMany_list _ Raw.WF.empty₀] + (insertMany emptyWithCapacity l).1.1.isEmpty = l.isEmpty := by + simp [isEmpty_insertMany_list _ Raw.WF.emptyWithCapacity₀] + +set_option linter.missingDocs false in +@[deprecated isEmpty_insertMany_emptyWithCapacity_list (since := "2025-03-12")] +abbrev isEmpty_insertMany_empty_list := @isEmpty_insertMany_emptyWithCapacity_list namespace Const variable {β : Type v} @[simp] -theorem insertMany_empty_list_nil : - (insertMany empty ([] : List (α × β))).1 = empty := by +theorem insertMany_emptyWithCapacity_list_nil : + (insertMany emptyWithCapacity ([] : List (α × β))).1 = emptyWithCapacity := by simp only [insertMany_nil] +set_option linter.missingDocs false in +@[deprecated insertMany_emptyWithCapacity_list_nil (since := "2025-03-12")] +abbrev insertMany_empty_list_nil := @insertMany_emptyWithCapacity_list_nil + @[simp] -theorem insertMany_empty_list_singleton {k : α} {v : β} : - (insertMany empty [⟨k, v⟩]).1 = empty.insert k v := by +theorem insertMany_emptyWithCapacity_list_singleton {k : α} {v : β} : + (insertMany emptyWithCapacity [⟨k, v⟩]).1 = emptyWithCapacity.insert k v := by simp only [insertMany_list_singleton] -theorem insertMany_empty_list_cons {k : α} {v : β} +set_option linter.missingDocs false in +@[deprecated insertMany_emptyWithCapacity_list_singleton (since := "2025-03-12")] +abbrev insertMany_empty_list_singleton := @insertMany_emptyWithCapacity_list_singleton + +theorem insertMany_emptyWithCapacity_list_cons {k : α} {v : β} {tl : List (α × β)} : - (insertMany empty (⟨k, v⟩ :: tl)) = (insertMany (empty.insert k v) tl).1 := by + (insertMany emptyWithCapacity (⟨k, v⟩ :: tl)) = (insertMany (emptyWithCapacity.insert k v) tl).1 := by rw [insertMany_cons] -theorem contains_insertMany_empty_list [EquivBEq α] [LawfulHashable α] - {l : List (α × β)} {k : α} : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.contains k = (l.map Prod.fst).contains k := by - simp [contains_insertMany_list _ Raw.WF.empty₀] +set_option linter.missingDocs false in +@[deprecated insertMany_emptyWithCapacity_list_cons (since := "2025-03-12")] +abbrev insertMany_empty_list_cons := @insertMany_emptyWithCapacity_list_cons -theorem get?_insertMany_empty_list_of_contains_eq_false [LawfulBEq α] +theorem contains_insertMany_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] + {l : List (α × β)} {k : α} : + (insertMany emptyWithCapacity l).1.contains k = (l.map Prod.fst).contains k := by + simp [contains_insertMany_list _ Raw.WF.emptyWithCapacity₀] + +set_option linter.missingDocs false in +@[deprecated contains_insertMany_emptyWithCapacity_list (since := "2025-03-12")] +abbrev contains_insertMany_empty_list := @contains_insertMany_emptyWithCapacity_list + +theorem get?_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (h : (l.map Prod.fst).contains k = false) : - get? (insertMany (empty : Raw₀ α (fun _ => β)) l).1 k = none := by - rw [get?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply get?_empty + get? (insertMany emptyWithCapacity l).1 k = none := by + rw [get?_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply get?_emptyWithCapacity -theorem get?_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev get?_insertMany_empty_list_of_contains_eq_false := @get?_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem get?_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : - get? (insertMany (empty : Raw₀ α (fun _ => β)) l) k' = some v := by - rw [get?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + get? (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l) k' = some v := by + rw [get?_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem get_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev get?_insertMany_empty_list_of_mem := @get?_insertMany_emptyWithCapacity_list_of_mem + +theorem get_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) {h} : - get (insertMany (empty : Raw₀ α (fun _ => β)) l) k' h = v := by - rw [get_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + get (insertMany emptyWithCapacity l) k' h = v := by + rw [get_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem get!_insertMany_empty_list_of_contains_eq_false [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev get_insertMany_empty_list_of_mem := @get_insertMany_emptyWithCapacity_list_of_mem + +theorem get!_insertMany_emptyWithCapacity_list_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} [Inhabited β] (h : (l.map Prod.fst).contains k = false) : - get! (insertMany (empty : Raw₀ α (fun _ => β)) l) k = (default : β) := by - rw [get!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply get!_empty + get! (insertMany emptyWithCapacity l) k = (default : β) := by + rw [get!_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply get!_emptyWithCapacity -theorem get!_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev get!_insertMany_empty_list_of_contains_eq_false := @get!_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem get!_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} [Inhabited β] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : - get! (insertMany (empty : Raw₀ α (fun _ => β)) l) k' = v := by - rw [get!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + get! (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l) k' = v := by + rw [get!_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getD_insertMany_empty_list_of_contains_eq_false [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated get!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev get!_insertMany_empty_list_of_mem := @get!_insertMany_emptyWithCapacity_list_of_mem + +theorem getD_insertMany_emptyWithCapacity_list_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (l.map Prod.fst).contains k = false) : - getD (insertMany (empty : Raw₀ α (fun _ => β)) l) k fallback = fallback := by - rw [getD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ contains_eq_false] - apply getD_empty + getD (insertMany emptyWithCapacity l) k fallback = fallback := by + rw [getD_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ contains_eq_false] + apply getD_emptyWithCapacity -theorem getD_insertMany_empty_list_of_mem [LawfulBEq α] +set_option linter.missingDocs false in +@[deprecated getD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getD_insertMany_empty_list_of_contains_eq_false := @getD_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getD_insertMany_emptyWithCapacity_list_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : - getD (insertMany (empty : Raw₀ α (fun _ => β)) l) k' fallback = v := by - rw [getD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + getD (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l) k' fallback = v := by + rw [getD_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKey?_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getD_insertMany_empty_list_of_mem (since := "2025-03-12")] +abbrev getD_insertMany_empty_list_of_mem := @getD_insertMany_emptyWithCapacity_list_of_mem + +theorem getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (h : (l.map Prod.fst).contains k = false) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey? k = none := by - rw [getKey?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply getKey?_empty + (insertMany emptyWithCapacity l).1.getKey? k = none := by + rw [getKey?_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply getKey?_emptyWithCapacity -theorem getKey?_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKey?_insertMany_empty_list_of_contains_eq_false := @getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getKey?_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey? k' = some k := by - rw [getKey?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.getKey? k' = some k := by + rw [getKey?_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKey_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey?_insertMany_empty_list_of_mem := @getKey?_insertMany_emptyWithCapacity_list_of_mem + +theorem getKey_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) {h'} : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey k' h' = k := by - rw [getKey_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.getKey k' h' = k := by + rw [getKey_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKey!_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey_insertMany_empty_list_of_mem := @getKey_insertMany_emptyWithCapacity_list_of_mem + +theorem getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (h : (l.map Prod.fst).contains k = false) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey! k = default := by - rw [getKey!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply getKey!_empty + (insertMany emptyWithCapacity l).1.getKey! k = default := by + rw [getKey!_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply getKey!_emptyWithCapacity -theorem getKey!_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] +set_option linter.missingDocs false in +@[deprecated getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKey!_insertMany_empty_list_of_contains_eq_false := @getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getKey!_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey! k' = k := by - rw [getKey!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.getKey! k' = k := by + rw [getKey!_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem getKeyD_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey!_insertMany_empty_list_of_mem := @getKey!_insertMany_emptyWithCapacity_list_of_mem + +theorem getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (h : (l.map Prod.fst).contains k = false) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKeyD k fallback = fallback := by - rw [getKeyD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h] - apply getKeyD_empty + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.getKeyD k fallback = fallback := by + rw [getKeyD_insertMany_list_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ h] + apply getKeyD_emptyWithCapacity -theorem getKeyD_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKeyD_insertMany_empty_list_of_contains_eq_false := @getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false + +theorem getKeyD_insertMany_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' fallback : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKeyD k' fallback = k := by - rw [getKeyD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem] + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.getKeyD k' fallback = k := by + rw [getKeyD_insertMany_list_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq distinct mem] -theorem size_insertMany_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKeyD_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKeyD_insertMany_empty_list_of_mem := @getKeyD_insertMany_emptyWithCapacity_list_of_mem + +theorem size_insertMany_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.1.size = l.length := by - rw [size_insertMany_list _ Raw.WF.empty₀ distinct] - · simp only [size_empty, Nat.zero_add] - · simp only [contains_empty, Bool.false_eq_true, false_implies, implies_true] + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.1.size = l.length := by + rw [size_insertMany_list _ Raw.WF.emptyWithCapacity₀ distinct] + · simp only [size_emptyWithCapacity, Nat.zero_add] + · simp only [contains_emptyWithCapacity, Bool.false_eq_true, false_implies, implies_true] -theorem size_insertMany_empty_list_le [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated size_insertMany_emptyWithCapacity_list (since := "2025-03-12")] +abbrev size_insertMany_empty_list := @size_insertMany_emptyWithCapacity_list + +theorem size_insertMany_emptyWithCapacity_list_le [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.1.size ≤ l.length := by + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.1.size ≤ l.length := by rw [← Nat.zero_add l.length] - apply (size_insertMany_list_le _ Raw.WF.empty₀) + apply (size_insertMany_list_le _ Raw.WF.emptyWithCapacity₀) -theorem isEmpty_insertMany_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated size_insertMany_emptyWithCapacity_list_le (since := "2025-03-12")] +abbrev size_insertMany_empty_list_le := @size_insertMany_emptyWithCapacity_list_le + +theorem isEmpty_insertMany_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : - (insertMany (empty : Raw₀ α (fun _ => β)) l).1.1.isEmpty = l.isEmpty := by - simp [isEmpty_insertMany_list _ Raw.WF.empty₀] + (insertMany (emptyWithCapacity : Raw₀ α (fun _ => β)) l).1.1.isEmpty = l.isEmpty := by + simp [isEmpty_insertMany_list _ Raw.WF.emptyWithCapacity₀] + +set_option linter.missingDocs false in +@[deprecated isEmpty_insertMany_emptyWithCapacity_list (since := "2025-03-12")] +abbrev isEmpty_insertMany_empty_list := @isEmpty_insertMany_emptyWithCapacity_list @[simp] -theorem insertManyIfNewUnit_empty_list_nil : - insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) ([] : List α) = - (empty : Raw₀ α (fun _ => Unit)) := by +theorem insertManyIfNewUnit_emptyWithCapacity_list_nil : + insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) ([] : List α) = + (emptyWithCapacity : Raw₀ α (fun _ => Unit)) := by simp +set_option linter.missingDocs false in +@[deprecated insertManyIfNewUnit_emptyWithCapacity_list_nil (since := "2025-03-12")] +abbrev insertManyIfNewUnit_empty_list_nil := @insertManyIfNewUnit_emptyWithCapacity_list_nil + @[simp] -theorem insertManyIfNewUnit_empty_list_singleton {k : α} : - (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) [k]).1 = empty.insertIfNew k () := by +theorem insertManyIfNewUnit_emptyWithCapacity_list_singleton {k : α} : + (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) [k]).1 = emptyWithCapacity.insertIfNew k () := by simp -theorem insertManyIfNewUnit_empty_list_cons {hd : α} {tl : List α} : - insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) (hd :: tl) = - (insertManyIfNewUnit (empty.insertIfNew hd ()) tl).1 := by +set_option linter.missingDocs false in +@[deprecated insertManyIfNewUnit_emptyWithCapacity_list_singleton (since := "2025-03-12")] +abbrev insertManyIfNewUnit_empty_list_singleton := @insertManyIfNewUnit_emptyWithCapacity_list_singleton + +theorem insertManyIfNewUnit_emptyWithCapacity_list_cons {hd : α} {tl : List α} : + insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) (hd :: tl) = + (insertManyIfNewUnit (emptyWithCapacity.insertIfNew hd ()) tl).1 := by rw [insertManyIfNewUnit_cons] -theorem contains_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated insertManyIfNewUnit_emptyWithCapacity_list_cons (since := "2025-03-12")] +abbrev insertManyIfNewUnit_empty_list_cons := @insertManyIfNewUnit_emptyWithCapacity_list_cons + +theorem contains_insertManyIfNewUnit_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : - (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.contains k = l.contains k := by - simp [contains_insertManyIfNewUnit_list _ Raw.WF.empty₀] + (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1.contains k = l.contains k := by + simp [contains_insertManyIfNewUnit_list _ Raw.WF.emptyWithCapacity₀] -theorem getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated contains_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev contains_insertManyIfNewUnit_empty_list := @contains_insertManyIfNewUnit_emptyWithCapacity_list + +theorem getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h' : l.contains k = false) : - getKey? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k = none := by - exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀ - contains_empty h' + getKey? (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k = none := by + exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ + contains_emptyWithCapacity h' -theorem getKey?_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false := @getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false + +theorem getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : - getKey? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' = some k := by - exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq - contains_empty distinct mem + getKey? (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k' = some k := by + exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq + contains_emptyWithCapacity distinct mem -theorem getKey_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey?_insertManyIfNewUnit_empty_list_of_mem := @getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem + +theorem getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h'} : - getKey (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' h' = k := by - exact getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq - contains_empty distinct mem + getKey (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k' h' = k := by + exact getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq + contains_emptyWithCapacity distinct mem -theorem getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey_insertManyIfNewUnit_empty_list_of_mem := @getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem + +theorem getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (h' : l.contains k = false) : - getKey! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k = default := by - exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀ - contains_empty h' + getKey! (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k = default := by + exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.emptyWithCapacity₀ + contains_emptyWithCapacity h' -theorem getKey!_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false := @getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false + +theorem getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : - getKey! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' = k := by - exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq - contains_empty distinct mem + getKey! (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k' = k := by + exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq + contains_emptyWithCapacity distinct mem -theorem getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKey!_insertManyIfNewUnit_empty_list_of_mem := @getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem + +theorem getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (h' : l.contains k = false) : - getKeyD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k fallback = fallback := by + getKeyD (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k fallback = fallback := by exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false - _ Raw.WF.empty₀ contains_empty h' + _ Raw.WF.emptyWithCapacity₀ contains_emptyWithCapacity h' -theorem getKeyD_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")] +abbrev getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false := @getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false + +theorem getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : - getKeyD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' fallback = k := by - exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq - contains_empty distinct mem + getKeyD (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1 k' fallback = k := by + exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.emptyWithCapacity₀ k_beq + contains_emptyWithCapacity distinct mem -theorem size_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")] +abbrev getKeyD_insertManyIfNewUnit_empty_list_of_mem := @getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem + +theorem size_insertManyIfNewUnit_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : l.Pairwise (fun a b => (a == b) = false)) : - (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.1.size = l.length := by - simp [size_insertManyIfNewUnit_list _ Raw.WF.empty₀ distinct] + (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1.1.size = l.length := by + simp [size_insertManyIfNewUnit_list _ Raw.WF.emptyWithCapacity₀ distinct] -theorem size_insertManyIfNewUnit_empty_list_le [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated size_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev size_insertManyIfNewUnit_empty_list := @size_insertManyIfNewUnit_emptyWithCapacity_list + +theorem size_insertManyIfNewUnit_emptyWithCapacity_list_le [EquivBEq α] [LawfulHashable α] {l : List α} : - (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.1.size ≤ l.length := by - apply Nat.le_trans (size_insertManyIfNewUnit_list_le _ Raw.WF.empty₀) + (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1.1.size ≤ l.length := by + apply Nat.le_trans (size_insertManyIfNewUnit_list_le _ Raw.WF.emptyWithCapacity₀) simp -theorem isEmpty_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated size_insertManyIfNewUnit_emptyWithCapacity_list_le (since := "2025-03-12")] +abbrev size_insertManyIfNewUnit_empty_list_le := @size_insertManyIfNewUnit_emptyWithCapacity_list_le + +theorem isEmpty_insertManyIfNewUnit_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List α} : - (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.1.isEmpty = l.isEmpty := by - rw [isEmpty_insertManyIfNewUnit_list _ Raw.WF.empty₀] + (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l).1.1.isEmpty = l.isEmpty := by + rw [isEmpty_insertManyIfNewUnit_list _ Raw.WF.emptyWithCapacity₀] simp -theorem get?_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α] +set_option linter.missingDocs false in +@[deprecated isEmpty_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev isEmpty_insertManyIfNewUnit_empty_list := @isEmpty_insertManyIfNewUnit_emptyWithCapacity_list + +theorem get?_insertManyIfNewUnit_emptyWithCapacity_list [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : - get? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k = + get? (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k = if l.contains k then some () else none := by - rw [get?_insertManyIfNewUnit_list _ Raw.WF.empty₀] + rw [get?_insertManyIfNewUnit_list _ Raw.WF.emptyWithCapacity₀] simp -theorem get_insertManyIfNewUnit_empty_list +set_option linter.missingDocs false in +@[deprecated get?_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev get?_insertManyIfNewUnit_empty_list := @get?_insertManyIfNewUnit_emptyWithCapacity_list + +theorem get_insertManyIfNewUnit_emptyWithCapacity_list {l : List α} {k : α} {h} : - get (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k h = () := by + get (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k h = () := by simp -theorem get!_insertManyIfNewUnit_empty_list +set_option linter.missingDocs false in +@[deprecated get_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev get_insertManyIfNewUnit_empty_list := @get_insertManyIfNewUnit_emptyWithCapacity_list + +theorem get!_insertManyIfNewUnit_emptyWithCapacity_list {l : List α} {k : α} : - get! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k = () := by + get! (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k = () := by simp -theorem getD_insertManyIfNewUnit_empty_list +set_option linter.missingDocs false in +@[deprecated get!_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev get!_insertManyIfNewUnit_empty_list := @get!_insertManyIfNewUnit_emptyWithCapacity_list + +theorem getD_insertManyIfNewUnit_emptyWithCapacity_list {l : List α} {k : α} {fallback : Unit} : - getD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k fallback = () := by + getD (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k fallback = () := by simp +set_option linter.missingDocs false in +@[deprecated getD_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")] +abbrev getD_insertManyIfNewUnit_empty_list := @getD_insertManyIfNewUnit_emptyWithCapacity_list + end Const section Alter @@ -2611,10 +2915,14 @@ end Raw variable (m₁ m₂ : Raw₀ α β) -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {c : Nat} : - m.1 ~m (empty c).1 ↔ m.1.isEmpty := by +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {c : Nat} : + m.1 ~m (emptyWithCapacity c).1 ↔ m.1.isEmpty := by simp_to_model [Equiv, isEmpty] - simp only [toListModel_buckets_empty, List.perm_nil, List.isEmpty_iff] + simp only [toListModel_buckets_emptyWithCapacity, List.perm_nil, List.isEmpty_iff] + +set_option linter.missingDocs false in +@[deprecated equiv_emptyWithCapacity_iff_isEmpty (since := "2025-03-12")] +abbrev equiv_empty_iff_isEmpty := @equiv_emptyWithCapacity_iff_isEmpty theorem isEmpty_eq_of_equiv [EquivBEq α] [LawfulHashable α] (h₁ : m₁.1.WF) (h₂ : m₂.1.WF) (h : m₁.1 ~m m₂.1) : diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 4f98850d7d..023c96a2a7 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -217,14 +217,22 @@ namespace Raw₀ /-! # Raw₀.empty -/ @[simp] -theorem toListModel_buckets_empty {c} : toListModel (empty c : Raw₀ α β).1.buckets = [] := +theorem toListModel_buckets_emptyWithCapacity {c} : toListModel (emptyWithCapacity c : Raw₀ α β).1.buckets = [] := toListModel_mkArray_nil -theorem wfImp_empty [BEq α] [Hashable α] {c} : Raw.WFImp (empty c : Raw₀ α β).1 where - buckets_hash_self := by simp [Raw.empty, Raw₀.empty] - size_eq := by simp [Raw.empty, Raw₀.empty] +set_option linter.missingDocs false in +@[deprecated toListModel_buckets_emptyWithCapacity (since := "2025-03-12")] +abbrev toListModel_buckets_empty := @toListModel_buckets_emptyWithCapacity + +theorem wfImp_emptyWithCapacity [BEq α] [Hashable α] {c} : Raw.WFImp (emptyWithCapacity c : Raw₀ α β).1 where + buckets_hash_self := by simp [Raw.emptyWithCapacity, Raw₀.emptyWithCapacity] + size_eq := by simp [Raw.emptyWithCapacity, Raw₀.emptyWithCapacity] distinct := by simp +set_option linter.missingDocs false in +@[deprecated wfImp_emptyWithCapacity (since := "2025-03-12")] +abbrev wfImp_empty := @wfImp_emptyWithCapacity + theorem isHashSelf_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (data : {d : Array (AssocList α β) // 0 < d.size}) (a : α) (b : β a) (h : IsHashSelf data.1) : IsHashSelf (reinsertAux hash data a b).1 := by @@ -1064,7 +1072,7 @@ theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashabl (h : m.WF) : Raw.WFImp m := by induction h generalizing i₁ i₂ · next h => apply h - · exact Raw₀.wfImp_empty + · exact Raw₀.wfImp_emptyWithCapacity · next h => exact Raw₀.wfImp_insert (by apply h) · next h => exact Raw₀.wfImp_containsThenInsert (by apply h) · next h => exact Raw₀.wfImp_containsThenInsertIfNew (by apply h) diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 54f7309a75..555993fe2e 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -30,12 +30,16 @@ namespace Std.DHashMap variable {m : DHashMap α β} @[simp] -theorem isEmpty_empty {c} : (empty c : DHashMap α β).isEmpty := - Raw₀.isEmpty_empty +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).isEmpty := + Raw₀.isEmpty_emptyWithCapacity @[simp] -theorem isEmpty_emptyc : (∅ : DHashMap α β).isEmpty := - isEmpty_empty +theorem isEmpty_empty : (∅ : DHashMap α β).isEmpty := + isEmpty_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated isEmpty_empty (since := "2025-03-12")] +abbrev isEmpty_emptyc := @isEmpty_empty @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -52,17 +56,26 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := by simp [mem_iff_contains, contains_congr hab] -@[simp] theorem contains_empty {a : α} {c} : (empty c : DHashMap α β).contains a = false := - Raw₀.contains_empty +@[simp] +theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).contains a = false := + Raw₀.contains_emptyWithCapacity -@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : DHashMap α β) := by +@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : DHashMap α β) := by simp [mem_iff_contains] -@[simp] theorem contains_emptyc {a : α} : (∅ : DHashMap α β).contains a = false := - contains_empty +@[simp] theorem contains_empty {a : α} : (∅ : DHashMap α β).contains a = false := + contains_emptyWithCapacity -@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : DHashMap α β) := - not_mem_empty +set_option linter.missingDocs false in +@[deprecated contains_empty (since := "2025-03-12")] +abbrev contains_emptyc := @contains_empty + +@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : DHashMap α β) := + not_mem_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated not_mem_empty (since := "2025-03-12")] +abbrev not_mem_emptyc := @not_mem_empty theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty → m.contains a = false := @@ -119,12 +132,16 @@ theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : k ∈ m.insert k v := by simp @[simp] -theorem size_empty {c} : (empty c : DHashMap α β).size = 0 := - Raw₀.size_empty +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).size = 0 := + Raw₀.size_emptyWithCapacity @[simp] -theorem size_emptyc : (∅ : DHashMap α β).size = 0 := - size_empty +theorem size_empty : (∅ : DHashMap α β).size = 0 := + size_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated size_empty (since := "2025-03-12")] +abbrev size_emptyc := @size_empty theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl @@ -141,12 +158,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : Raw₀.size_insert_le ⟨m.1, _⟩ m.2 @[simp] -theorem erase_empty {k : α} {c : Nat} : (empty c : DHashMap α β).erase k = empty c := - Subtype.eq (congrArg Subtype.val (Raw₀.erase_empty (k := k)) :) -- Lean code is happy +theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : DHashMap α β).erase k = emptyWithCapacity c := + Subtype.eq (congrArg Subtype.val (Raw₀.erase_emptyWithCapacity (k := k)) :) @[simp] -theorem erase_emptyc {k : α} : (∅ : DHashMap α β).erase k = ∅ := - erase_empty +theorem erase_empty {k : α} : (∅ : DHashMap α β).erase k = ∅ := + erase_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated erase_empty (since := "2025-03-12")] +abbrev erase_emptyc := @erase_empty @[simp] theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} : @@ -200,12 +221,16 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β k} : Subtype.eq <| (congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _ (k := k)) :) @[simp] -theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : DHashMap α β).get? a = none := - Raw₀.get?_empty +theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : DHashMap α β).get? a = none := + Raw₀.get?_emptyWithCapacity @[simp] -theorem get?_emptyc [LawfulBEq α] {a : α} : (∅ : DHashMap α β).get? a = none := - get?_empty +theorem get?_empty [LawfulBEq α] {a : α} : (∅ : DHashMap α β).get? a = none := + get?_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-12")] +abbrev get?_emptyc := @get?_empty theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a = none := Raw₀.get?_of_isEmpty ⟨m.1, _⟩ m.2 @@ -241,12 +266,16 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} @[simp] -theorem get?_empty {a : α} {c} : get? (empty c : DHashMap α (fun _ => β)) a = none := - Raw₀.Const.get?_empty +theorem get?_emptyWithCapacity {a : α} {c} : get? (emptyWithCapacity c : DHashMap α (fun _ => β)) a = none := + Raw₀.Const.get?_emptyWithCapacity @[simp] -theorem get?_emptyc {a : α} : get? (∅ : DHashMap α (fun _ => β)) a = none := - get?_empty +theorem get?_empty {a : α} : get? (∅ : DHashMap α (fun _ => β)) a = none := + get?_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-12")] +abbrev get?_emptyc := @get?_empty theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → get? m a = none := @@ -342,14 +371,18 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h end Const @[simp] -theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : - (empty c : DHashMap α β).get! a = default := - Raw₀.get!_empty +theorem get!_emptyWithCapacity [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : + (emptyWithCapacity c : DHashMap α β).get! a = default := + Raw₀.get!_emptyWithCapacity @[simp] -theorem get!_emptyc [LawfulBEq α] {a : α} [Inhabited (β a)] : +theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] : (∅ : DHashMap α β).get! a = default := - get!_empty + get!_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get!_empty (since := "2025-03-12")] +abbrev get!_emptyc := @get!_empty theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] : m.isEmpty = true → m.get! a = default := @@ -403,13 +436,17 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} @[simp] -theorem get!_empty [Inhabited β] {a : α} {c} : - get! (empty c : DHashMap α (fun _ => β)) a = default := - Raw₀.Const.get!_empty +theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} : + get! (emptyWithCapacity c : DHashMap α (fun _ => β)) a = default := + Raw₀.Const.get!_emptyWithCapacity @[simp] -theorem get!_emptyc [Inhabited β] {a : α} : get! (∅ : DHashMap α (fun _ => β)) a = default := - get!_empty +theorem get!_empty [Inhabited β] {a : α} : get! (∅ : DHashMap α (fun _ => β)) a = default := + get!_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get!_empty (since := "2025-03-12")] +abbrev get!_emptyc := @get!_empty theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.isEmpty = true → get! m a = default := @@ -468,14 +505,18 @@ theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} ( end Const @[simp] -theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} : - (empty c : DHashMap α β).getD a fallback = fallback := - Raw₀.getD_empty +theorem getD_emptyWithCapacity [LawfulBEq α] {a : α} {fallback : β a} {c} : + (emptyWithCapacity c : DHashMap α β).getD a fallback = fallback := + Raw₀.getD_emptyWithCapacity @[simp] -theorem getD_emptyc [LawfulBEq α] {a : α} {fallback : β a} : +theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} : (∅ : DHashMap α β).getD a fallback = fallback := - getD_empty + getD_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-12")] +abbrev getD_emptyc := @getD_empty theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} : m.isEmpty = true → m.getD a fallback = fallback := @@ -533,14 +574,18 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} @[simp] -theorem getD_empty {a : α} {fallback : β} {c} : - getD (empty c : DHashMap α (fun _ => β)) a fallback = fallback := - Raw₀.Const.getD_empty +theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : + getD (emptyWithCapacity c : DHashMap α (fun _ => β)) a fallback = fallback := + Raw₀.Const.getD_emptyWithCapacity @[simp] -theorem getD_emptyc {a : α} {fallback : β} : +theorem getD_empty {a : α} {fallback : β} : getD (∅ : DHashMap α (fun _ => β)) a fallback = fallback := - getD_empty + getD_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-12")] +abbrev getD_emptyc := @getD_empty theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.isEmpty = true → getD m a fallback = fallback := @@ -603,12 +648,16 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} end Const @[simp] -theorem getKey?_empty {a : α} {c} : (empty c : DHashMap α β).getKey? a = none := - Raw₀.getKey?_empty +theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).getKey? a = none := + Raw₀.getKey?_emptyWithCapacity @[simp] -theorem getKey?_emptyc {a : α} : (∅ : DHashMap α β).getKey? a = none := - Raw₀.getKey?_empty +theorem getKey?_empty {a : α} : (∅ : DHashMap α β).getKey? a = none := + getKey?_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getKey?_empty (since := "2025-03-12")] +abbrev getKey?_emptyc := @getKey?_empty theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.getKey? a = none := @@ -691,14 +740,18 @@ theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k := Raw₀.getKey_eq ⟨m.1, _⟩ m.2 h @[simp] -theorem getKey!_empty [Inhabited α] {a : α} {c} : - (empty c : DHashMap α β).getKey! a = default := - Raw₀.getKey!_empty +theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} : + (emptyWithCapacity c : DHashMap α β).getKey! a = default := + Raw₀.getKey!_emptyWithCapacity @[simp] -theorem getKey!_emptyc [Inhabited α] {a : α} : +theorem getKey!_empty [Inhabited α] {a : α} : (∅ : DHashMap α β).getKey! a = default := - getKey!_empty + getKey!_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getKey!_empty (since := "2025-03-12")] +abbrev getKey!_emptyc := @getKey!_empty theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.isEmpty = true → m.getKey! a = default := @@ -760,14 +813,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : getKey!_eq_of_contains h @[simp] -theorem getKeyD_empty {a fallback : α} {c} : - (empty c : DHashMap α β).getKeyD a fallback = fallback := - Raw₀.getKeyD_empty +theorem getKeyD_emptyWithCapacity {a fallback : α} {c} : + (emptyWithCapacity c : DHashMap α β).getKeyD a fallback = fallback := + Raw₀.getKeyD_emptyWithCapacity @[simp] -theorem getKeyD_emptyc {a fallback : α} : +theorem getKeyD_empty {a fallback : α} : (∅ : DHashMap α β).getKeyD a fallback = fallback := - getKeyD_empty + getKeyD_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getKeyD_empty (since := "2025-03-12")] +abbrev getKeyD_emptyc := @getKeyD_empty theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.isEmpty = true → m.getKeyD a fallback = fallback := @@ -1753,22 +1810,22 @@ namespace DHashMap @[simp] theorem ofList_nil : ofList ([] : List ((a : α) × (β a))) = ∅ := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_nil (α := α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_nil (α := α)) :) @[simp] theorem ofList_singleton {k : α} {v : β k} : ofList [⟨k, v⟩] = (∅: DHashMap α β).insert k v := - Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_singleton (α := α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_singleton (α := α)) :) 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_empty_list_cons (α := α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_cons (α := α)) :) @[simp] theorem contains_ofList [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} : (ofList l).contains k = (l.map Sigma.fst).contains k := - Raw₀.contains_insertMany_empty_list + Raw₀.contains_insertMany_emptyWithCapacity_list @[simp] theorem mem_ofList [EquivBEq α] [LawfulHashable α] @@ -1780,14 +1837,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).get? k = none := - Raw₀.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem get?_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : (ofList l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := - Raw₀.get?_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem get_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} @@ -1795,39 +1852,39 @@ theorem get_ofList_of_mem [LawfulBEq α] (mem : ⟨k, v⟩ ∈ l) {h} : (ofList l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := - Raw₀.get_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.get_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem get!_ofList_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).get! k = default := - Raw₀.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem get!_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : (ofList l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := - Raw₀.get!_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getD_ofList_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getD k fallback = fallback := - Raw₀.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getD_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : (ofList l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := - Raw₀.getD_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getKey? k = none := - Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} @@ -1835,7 +1892,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : (ofList l).getKey? k' = some k := - Raw₀.getKey?_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} @@ -1844,13 +1901,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] (mem : k ∈ l.map Sigma.fst) {h} : (ofList l).getKey k' h = k := - Raw₀.getKey_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getKey! k = default := - Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} @@ -1858,13 +1915,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : (ofList l).getKey! k' = k := - Raw₀.getKey!_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getKeyD k fallback = fallback := - Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} @@ -1872,23 +1929,23 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : (ofList l).getKeyD k' fallback = k := - Raw₀.getKeyD_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem size_ofList [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : (ofList l).size = l.length := - Raw₀.size_insertMany_empty_list distinct + Raw₀.size_insertMany_emptyWithCapacity_list distinct theorem size_ofList_le [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (ofList l).size ≤ l.length := - Raw₀.size_insertMany_empty_list_le + Raw₀.size_insertMany_emptyWithCapacity_list_le @[simp] theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (ofList l).isEmpty = l.isEmpty := - Raw₀.isEmpty_insertMany_empty_list + Raw₀.isEmpty_insertMany_emptyWithCapacity_list namespace Const @@ -1897,22 +1954,22 @@ variable {β : Type v} @[simp] theorem ofList_nil : ofList ([] : List (α × β)) = ∅ := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_nil (α:= α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_nil (α:= α)) :) @[simp] theorem ofList_singleton {k : α} {v : β} : ofList [⟨k, v⟩] = (∅ : DHashMap α (fun _ => β)).insert k v := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_singleton (α:= α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_singleton (α:= α)) :) 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_empty_list_cons (α:= α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_cons (α:= α)) :) @[simp] theorem contains_ofList [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : (ofList l).contains k = (l.map Prod.fst).contains k := - Raw₀.Const.contains_insertMany_empty_list + Raw₀.Const.contains_insertMany_emptyWithCapacity_list @[simp] theorem mem_ofList [EquivBEq α] [LawfulHashable α] @@ -1924,14 +1981,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : get? (ofList l) k = none := - Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem get?_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : get? (ofList l) k' = some v := - Raw₀.Const.get?_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem get_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} @@ -1939,39 +1996,39 @@ theorem get_ofList_of_mem [LawfulBEq α] (mem : ⟨k, v⟩ ∈ l) {h} : get (ofList l) k' h = v := - Raw₀.Const.get_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem get!_ofList_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (l.map Prod.fst).contains k = false) : get! (ofList l) k = (default : β) := - Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem get!_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} [Inhabited β] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : get! (ofList l) k' = v := - Raw₀.Const.get!_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getD_ofList_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (l.map Prod.fst).contains k = false) : getD (ofList l) k fallback = fallback := - Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getD_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : getD (ofList l) k' fallback = v := - Raw₀.Const.getD_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : (ofList l).getKey? k = none := - Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} @@ -1979,7 +2036,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : (ofList l).getKey? k' = some k := - Raw₀.Const.getKey?_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} @@ -1988,13 +2045,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] (mem : k ∈ l.map Prod.fst) {h} : (ofList l).getKey k' h = k := - Raw₀.Const.getKey_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : (ofList l).getKey! k = default := - Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} @@ -2002,13 +2059,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : (ofList l).getKey! k' = k := - Raw₀.Const.getKey!_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : (ofList l).getKeyD k fallback = fallback := - Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} @@ -2016,44 +2073,44 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : (ofList l).getKeyD k' fallback = k := - Raw₀.Const.getKeyD_insertMany_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem theorem size_ofList [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : (ofList l).size = l.length := - Raw₀.Const.size_insertMany_empty_list distinct + Raw₀.Const.size_insertMany_emptyWithCapacity_list distinct theorem size_ofList_le [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (ofList l).size ≤ l.length := - Raw₀.Const.size_insertMany_empty_list_le + Raw₀.Const.size_insertMany_emptyWithCapacity_list_le @[simp] theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (ofList l).isEmpty = l.isEmpty := - Raw₀.Const.isEmpty_insertMany_empty_list + Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list @[simp] theorem unitOfList_nil : unitOfList ([] : List α) = ∅ := - Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_nil (α := α)) :) + Subtype.eq (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_empty_list_singleton (α := α)) :) + Subtype.eq (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_empty_list_cons (α := α)) :) + Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (α := α)) :) @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (unitOfList l).contains k = l.contains k := - Raw₀.Const.contains_insertManyIfNewUnit_empty_list + Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem mem_unitOfList [EquivBEq α] [LawfulHashable α] @@ -2064,13 +2121,13 @@ theorem mem_unitOfList [EquivBEq α] [LawfulHashable α] theorem getKey?_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : getKey? (unitOfList l) k = none := - Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKey?_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : getKey? (unitOfList l) k' = some k := - Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} @@ -2078,69 +2135,69 @@ theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h} : getKey (unitOfList l) k' h = k := - Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKey!_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : getKey! (unitOfList l) k = default := - Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKey!_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : getKey! (unitOfList l) k' = k := - Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem theorem getKeyD_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) : getKeyD (unitOfList l) k fallback = fallback := - Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false + Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false contains_eq_false theorem getKeyD_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : getKeyD (unitOfList l) k' fallback = k := - Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem + Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem theorem size_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : l.Pairwise (fun a b => (a == b) = false)) : (unitOfList l).size = l.length := - Raw₀.Const.size_insertManyIfNewUnit_empty_list distinct + Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list distinct theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α] {l : List α} : (unitOfList l).size ≤ l.length := - Raw₀.Const.size_insertManyIfNewUnit_empty_list_le + Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le @[simp] theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} : (unitOfList l).isEmpty = l.isEmpty := - Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list + Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem get?_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : get? (unitOfList l) k = if l.contains k then some () else none := - Raw₀.Const.get?_insertManyIfNewUnit_empty_list + Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem get_unitOfList {l : List α} {k : α} {h} : get (unitOfList l) k h = () := - Raw₀.Const.get_insertManyIfNewUnit_empty_list + Raw₀.Const.get_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem get!_unitOfList {l : List α} {k : α} : get! (unitOfList l) k = () := - Raw₀.Const.get!_insertManyIfNewUnit_empty_list + Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem getD_unitOfList @@ -2991,23 +3048,30 @@ end Const end Equiv @[simp] -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : - m ~m empty c ↔ m.isEmpty := - ⟨fun ⟨h⟩ => (Raw₀.equiv_empty_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mp h, - fun h => ⟨(Raw₀.equiv_empty_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mpr h⟩⟩ +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : + m ~m emptyWithCapacity c ↔ m.isEmpty := + ⟨fun ⟨h⟩ => (Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mp h, + fun h => ⟨(Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mpr h⟩⟩ @[simp] -theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty := - equiv_empty_iff_isEmpty +theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty := + equiv_emptyWithCapacity_iff_isEmpty + +set_option linter.missingDocs false in +@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-11")] +abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty + +theorem empty_equivWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : + emptyWithCapacity c ~m m ↔ m.isEmpty := + Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty @[simp] -theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : - empty c ~m m ↔ m.isEmpty := - Equiv.comm.trans equiv_empty_iff_isEmpty +theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty := + empty_equivWithCapacity_iff_isEmpty -@[simp] -theorem emptyc_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty := - empty_equiv_iff_isEmpty +set_option linter.missingDocs false in +@[deprecated empty_equiv_iff_isEmpty (since := "2025-03-11")] +abbrev emptyc_equiv_iff_isEmpty := @empty_equiv_iff_isEmpty theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap α β} [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 8d92812863..9f513f71ea 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -48,11 +48,14 @@ map so that it can hold the given number of mappings without reallocating. It is use the empty collection notations `∅` and `{}` to create an empty hash map with the default capacity. -/ -@[inline] def empty (capacity := 8) : Raw α β := - (Raw₀.empty capacity).1 +@[inline] def emptyWithCapacity (capacity := 8) : Raw α β := + (Raw₀.emptyWithCapacity capacity).1 + +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity instance : EmptyCollection (Raw α β) where - emptyCollection := empty + emptyCollection := emptyWithCapacity instance : Inhabited (Raw α β) where default := ∅ @@ -81,7 +84,7 @@ unchanged if a matching key is already present. else m -- will never happen for well-formed inputs instance [BEq α] [Hashable α] : Singleton ((a : α) × β a) (Raw α β) := - ⟨fun ⟨a, b⟩ => Raw.empty.insert a b⟩ + ⟨fun ⟨a, b⟩ => (∅ : Raw α β).insert a b⟩ instance [BEq α] [Hashable α] : Insert ((a : α) × β a) (Raw α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩ @@ -581,7 +584,7 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable | wf {α β} [BEq α] [Hashable α] {m : Raw α β} : 0 < m.buckets.size → (∀ [EquivBEq α] [LawfulHashable α], Raw.WFImp m) → WF m /-- Internal implementation detail of the hash map -/ - | empty₀ {α β} [BEq α] [Hashable α] {c} : WF (Raw₀.empty c : Raw₀ α β).1 + | emptyWithCapacity₀ {α β} [BEq α] [Hashable α] {c} : WF (Raw₀.emptyWithCapacity c : Raw₀ α β).1 /-- Internal implementation detail of the hash map -/ | insert₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.insert ⟨m, h⟩ a b).1 /-- Internal implementation detail of the hash map -/ @@ -616,10 +619,15 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable | constAlter₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} {f : Option β → Option β} : WF m → WF (Raw₀.Const.alter ⟨m, h⟩ a f).1 +-- TODO: this needs to be deprecated, but there is a bootstrapping issue. +-- @[deprecated WF.emptyWithCapacity₀ (since := "2025-03-12")] +@[inherit_doc Raw.WF.emptyWithCapacity₀] +abbrev WF.empty₀ := @WF.emptyWithCapacity₀ + /-- Internal implementation detail of the hash map -/ theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0 < m.buckets.size | wf h₁ _ => h₁ - | empty₀ => (Raw₀.empty _).2 + | emptyWithCapacity₀ => (Raw₀.emptyWithCapacity _).2 | insert₀ _ => (Raw₀.insert ⟨_, _⟩ _ _).2 | containsThenInsert₀ _ => (Raw₀.containsThenInsert ⟨_, _⟩ _ _).2.2 | containsThenInsertIfNew₀ _ => (Raw₀.containsThenInsertIfNew ⟨_, _⟩ _ _).2.2 @@ -633,11 +641,15 @@ theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0 | alter₀ _ => (Raw₀.alter _ _ _).2 | constAlter₀ _ => (Raw₀.Const.alter _ _ _).2 -@[simp] theorem WF.empty [BEq α] [Hashable α] {c : Nat} : (Raw.empty c : Raw α β).WF := - .empty₀ +@[simp] theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c : Nat} : (Raw.emptyWithCapacity c : Raw α β).WF := + .emptyWithCapacity₀ -@[simp] theorem WF.emptyc [BEq α] [Hashable α] : (∅ : Raw α β).WF := - .empty +@[simp] theorem WF.empty [BEq α] [Hashable α] : (∅ : Raw α β).WF := + .emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated WF.empty (since := "2025-03-12")] +abbrev WF.emptyc := @WF.empty theorem WF.insert [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β a} (h : m.WF) : (m.insert a b).WF := by diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 23f170adaf..6ffffd9ef2 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -67,12 +67,16 @@ open Internal.Raw₀ Internal.Raw variable {m : Raw α β} @[simp] -theorem size_empty {c} : (empty c : Raw α β).size = 0 := by - simp_to_raw using Raw₀.size_empty +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).size = 0 := by + simp_to_raw using Raw₀.size_emptyWithCapacity @[simp] -theorem size_emptyc : (∅ : Raw α β).size = 0 := - size_empty +theorem size_empty : (∅ : Raw α β).size = 0 := + size_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated size_empty (since := "2025-03-11")] +abbrev size_emptyc := @size_empty theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by simp [isEmpty] @@ -80,12 +84,16 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by variable [BEq α] [Hashable α] @[simp] -theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty := by - simp_to_raw using Raw₀.isEmpty_empty +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).isEmpty := by + simp_to_raw using Raw₀.isEmpty_emptyWithCapacity @[simp] -theorem isEmpty_emptyc : (∅ : Raw α β).isEmpty := - isEmpty_empty +theorem isEmpty_empty : (∅ : Raw α β).isEmpty := + isEmpty_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated isEmpty_empty (since := "2025-03-11")] +abbrev isEmpty_emptyc := @isEmpty_empty @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : @@ -103,17 +111,25 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a ∈ m ↔ b ∈ m := by simp [mem_iff_contains, contains_congr h hab] -@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false := by - simp_to_raw using Raw₀.contains_empty +@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false := by + simp_to_raw using Raw₀.contains_emptyWithCapacity -@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α β) := by +@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) := by simp [mem_iff_contains] -@[simp] theorem contains_emptyc {a : α} : (∅ : Raw α β).contains a = false := - contains_empty +@[simp] theorem contains_empty {a : α} : (∅ : Raw α β).contains a = false := + contains_emptyWithCapacity -@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) := - not_mem_empty +set_option linter.missingDocs false in +@[deprecated contains_empty (since := "2025-03-11")] +abbrev contains_emptyc := @contains_empty + +@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : Raw α β) := + not_mem_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated not_mem_empty (since := "2025-03-11")] +abbrev not_mem_emptyc := @not_mem_empty theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty → m.contains a = false := by @@ -187,13 +203,17 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v simp_to_raw using Raw₀.size_insert_le ⟨m, _⟩ h @[simp] -theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c := by +theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α β).erase k = emptyWithCapacity c := by rw [erase_eq (by wf_trivial)] - exact congrArg Subtype.val Raw₀.erase_empty + exact congrArg Subtype.val Raw₀.erase_emptyWithCapacity @[simp] -theorem erase_emptyc {k : α} : (∅ : Raw α β).erase k = ∅ := - erase_empty +theorem erase_empty {k : α} : (∅ : Raw α β).erase k = ∅ := + erase_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated erase_empty (since := "2025-03-11")] +abbrev erase_emptyc := @erase_empty @[simp] theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : @@ -252,12 +272,16 @@ theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β k} : simp_to_raw using congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _) @[simp] -theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw α β).get? a = none := by - simp_to_raw using Raw₀.get?_empty +theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : Raw α β).get? a = none := by + simp_to_raw using Raw₀.get?_emptyWithCapacity @[simp] -theorem get?_emptyc [LawfulBEq α] {a : α} : (∅ : Raw α β).get? a = none := - get?_empty +theorem get?_empty [LawfulBEq α] {a : α} : (∅ : Raw α β).get? a = none := + get?_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-11")] +abbrev get?_emptyc := @get?_empty theorem get?_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} : m.isEmpty = true → m.get? a = none := by simp_to_raw using Raw₀.get?_of_isEmpty ⟨m, _⟩ @@ -295,12 +319,16 @@ namespace Const variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF) @[simp] -theorem get?_empty {a : α} {c} : get? (empty c : Raw α (fun _ => β)) a = none := by - simp_to_raw using Raw₀.Const.get?_empty +theorem get?_emptyWithCapacity {a : α} {c} : get? (emptyWithCapacity c : Raw α (fun _ => β)) a = none := by + simp_to_raw using Raw₀.Const.get?_emptyWithCapacity @[simp] -theorem get?_emptyc {a : α} : get? (∅ : Raw α (fun _ => β)) a = none := - get?_empty +theorem get?_empty {a : α} : get? (∅ : Raw α (fun _ => β)) a = none := + get?_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-11")] +abbrev get?_emptyc := @get?_empty theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → get? m a = none := by @@ -399,14 +427,18 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : end Const @[simp] -theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : - (empty c : Raw α β).get! a = default := by - simp_to_raw using Raw₀.get!_empty +theorem get!_emptyWithCapacity [LawfulBEq α] {a : α} [Inhabited (β a)] {c} : + (emptyWithCapacity c : Raw α β).get! a = default := by + simp_to_raw using Raw₀.get!_emptyWithCapacity @[simp] -theorem get!_emptyc [LawfulBEq α] {a : α} [Inhabited (β a)] : +theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] : (∅ : Raw α β).get! a = default := - get!_empty + get!_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get!_empty (since := "2025-03-11")] +abbrev get!_emptyc := @get!_empty theorem get!_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : m.isEmpty = true → m.get! a = default := by @@ -459,12 +491,16 @@ namespace Const variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF) @[simp] -theorem get!_empty [Inhabited β] {a : α} {c} : get! (empty c : Raw α (fun _ => β)) a = default := by - simp_to_raw using Raw₀.Const.get!_empty +theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} : get! (emptyWithCapacity c : Raw α (fun _ => β)) a = default := by + simp_to_raw using Raw₀.Const.get!_emptyWithCapacity @[simp] -theorem get!_emptyc [Inhabited β] {a : α} : get! (∅ : Raw α (fun _ => β)) a = default := - get!_empty +theorem get!_empty [Inhabited β] {a : α} : get! (∅ : Raw α (fun _ => β)) a = default := + get!_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated get!_empty (since := "2025-03-11")] +abbrev get!_emptyc := @get!_empty theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} : m.isEmpty = true → get! m a = default := by @@ -524,14 +560,18 @@ theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) { end Const @[simp] -theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} : - (empty c : Raw α β).getD a fallback = fallback := by - simp_to_raw using Raw₀.getD_empty +theorem getD_emptyWithCapacity [LawfulBEq α] {a : α} {fallback : β a} {c} : + (emptyWithCapacity c : Raw α β).getD a fallback = fallback := by + simp_to_raw using Raw₀.getD_emptyWithCapacity @[simp] -theorem getD_emptyc [LawfulBEq α] {a : α} {fallback : β a} : +theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} : (∅ : Raw α β).getD a fallback = fallback := - getD_empty + getD_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-11")] +abbrev getD_emptyc := @getD_empty theorem getD_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : m.isEmpty = true → m.getD a fallback = fallback := by @@ -589,13 +629,17 @@ namespace Const variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF) @[simp] -theorem getD_empty {a : α} {fallback : β} {c} : - getD (empty c : Raw α (fun _ => β)) a fallback = fallback := by - simp_to_raw using Raw₀.Const.getD_empty +theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : + getD (emptyWithCapacity c : Raw α (fun _ => β)) a fallback = fallback := by + simp_to_raw using Raw₀.Const.getD_emptyWithCapacity @[simp] -theorem getD_emptyc {a : α} {fallback : β} : getD (∅ : Raw α (fun _ => β)) a fallback = fallback := - getD_empty +theorem getD_empty {a : α} {fallback : β} : getD (∅ : Raw α (fun _ => β)) a fallback = fallback := + getD_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-11")] +abbrev getD_emptyc := @getD_empty theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} : m.isEmpty = true → getD m a fallback = fallback := by @@ -658,13 +702,17 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall end Const @[simp] -theorem getKey?_empty {a : α} {c} : - (empty c : Raw α β).getKey? a = none := by - simp_to_raw using Raw₀.getKey?_empty +theorem getKey?_emptyWithCapacity {a : α} {c} : + (emptyWithCapacity c : Raw α β).getKey? a = none := by + simp_to_raw using Raw₀.getKey?_emptyWithCapacity @[simp] -theorem getKey?_emptyc {a : α} : (∅ : Raw α β).getKey? a = none := - getKey?_empty +theorem getKey?_empty {a : α} : (∅ : Raw α β).getKey? a = none := + getKey?_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getKey?_empty (since := "2025-03-11")] +abbrev getKey?_emptyc := @getKey?_empty theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m.getKey? a = none := by @@ -752,14 +800,18 @@ theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h') : simp_to_raw using Raw₀.getKey_eq @[simp] -theorem getKey!_empty [Inhabited α] {a : α} {c} : - (empty c : Raw α β).getKey! a = default := by - simp_to_raw using Raw₀.getKey!_empty +theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} : + (emptyWithCapacity c : Raw α β).getKey! a = default := by + simp_to_raw using Raw₀.getKey!_emptyWithCapacity @[simp] -theorem getKey!_emptyc [Inhabited α] {a : α} : +theorem getKey!_empty [Inhabited α] {a : α} : (∅ : Raw α β).getKey! a = default := - getKey!_empty + getKey!_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getKey!_empty (since := "2025-03-11")] +abbrev getKey!_emptyc := @getKey!_empty theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : m.isEmpty = true → m.getKey! a = default := by @@ -823,14 +875,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} : simpa only [mem_iff_contains] using getKey!_eq_of_contains h @[simp] -theorem getKeyD_empty {a fallback : α} {c} : - (empty c : Raw α β).getKeyD a fallback = fallback := by - simp_to_raw using Raw₀.getKeyD_empty +theorem getKeyD_emptyWithCapacity {a fallback : α} {c} : + (emptyWithCapacity c : Raw α β).getKeyD a fallback = fallback := by + simp_to_raw using Raw₀.getKeyD_emptyWithCapacity @[simp] -theorem getKeyD_emptyc {a fallback : α} : +theorem getKeyD_empty {a fallback : α} : (∅ : Raw α β).getKeyD a fallback = fallback := - getKeyD_empty + getKeyD_emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated getKeyD_empty (since := "2025-03-11")] +abbrev getKeyD_emptyc := @getKeyD_empty theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : m.isEmpty = true → m.getKeyD a fallback = fallback := by @@ -1855,24 +1911,24 @@ open Internal.Raw Internal.Raw₀ theorem ofList_nil : ofList ([] : List ((a : α) × (β a))) = ∅ := by simp_to_raw - rw [Raw₀.insertMany_empty_list_nil] + rw [Raw₀.insertMany_emptyWithCapacity_list_nil] @[simp] theorem ofList_singleton {k : α} {v : β k} : ofList [⟨k, v⟩] = (∅ : Raw α β).insert k v := by simp_to_raw - rw [Raw₀.insertMany_empty_list_singleton] + rw [Raw₀.insertMany_emptyWithCapacity_list_singleton] theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl : List ((a : α) × (β a))} : ofList (⟨k, v⟩ :: tl) = ((∅ : Raw α β).insert k v).insertMany tl := by simp_to_raw - rw [Raw₀.insertMany_empty_list_cons] + rw [Raw₀.insertMany_emptyWithCapacity_list_cons] @[simp] theorem contains_ofList [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} : (ofList l).contains k = (l.map Sigma.fst).contains k := by - simp_to_raw using Raw₀.contains_insertMany_empty_list + simp_to_raw using Raw₀.contains_insertMany_emptyWithCapacity_list @[simp] theorem mem_ofList [EquivBEq α] [LawfulHashable α] @@ -1884,14 +1940,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).get? k = none := by - simp_to_raw using Raw₀.get?_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem get?_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : (ofList l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by - simp_to_raw using Raw₀.get?_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem theorem get_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} @@ -1899,39 +1955,39 @@ theorem get_ofList_of_mem [LawfulBEq α] (mem : ⟨k, v⟩ ∈ l) {h} : (ofList l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by - simp_to_raw using Raw₀.get_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.get_insertMany_emptyWithCapacity_list_of_mem theorem get!_ofList_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).get! k = default := by - simp_to_raw using get!_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem get!_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : (ofList l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by - simp_to_raw using Raw₀.get!_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem theorem getD_ofList_of_contains_eq_false [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getD k fallback = fallback := by - simp_to_raw using Raw₀.getD_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getD_ofList_of_mem [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : (ofList l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by - simp_to_raw using Raw₀.getD_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getKey? k = none := by - simp_to_raw using Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} @@ -1939,7 +1995,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : (ofList l).getKey? k' = some k := by - simp_to_raw using Raw₀.getKey?_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} @@ -1948,13 +2004,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] (mem : k ∈ l.map Sigma.fst) {h'} : (ofList l).getKey k' h' = k := by - simp_to_raw using Raw₀.getKey_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getKey! k = default := by - simp_to_raw using Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} @@ -1962,13 +2018,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : (ofList l).getKey! k' = k := by - simp_to_raw using Raw₀.getKey!_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (contains_eq_false : (l.map Sigma.fst).contains k = false) : (ofList l).getKeyD k fallback = fallback := by - simp_to_raw using Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} @@ -1976,23 +2032,23 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Sigma.fst) : (ofList l).getKeyD k' fallback = k := by - simp_to_raw using Raw₀.getKeyD_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem theorem size_ofList [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : (ofList l).size = l.length := by - simp_to_raw using Raw₀.size_insertMany_empty_list + simp_to_raw using Raw₀.size_insertMany_emptyWithCapacity_list theorem size_ofList_le [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (ofList l).size ≤ l.length := by - simp_to_raw using Raw₀.size_insertMany_empty_list_le + simp_to_raw using Raw₀.size_insertMany_emptyWithCapacity_list_le @[simp] theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (ofList l).isEmpty = l.isEmpty := by - simp_to_raw using Raw₀.isEmpty_insertMany_empty_list + simp_to_raw using Raw₀.isEmpty_insertMany_emptyWithCapacity_list namespace Const @@ -2013,13 +2069,13 @@ theorem ofList_singleton {k : α} {v : β} : theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} : ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : Raw α (fun _ => β)).insert k v) tl := by simp_to_raw - rw [Raw₀.Const.insertMany_empty_list_cons] + rw [Raw₀.Const.insertMany_emptyWithCapacity_list_cons] @[simp] theorem contains_ofList [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : (ofList l).contains k = (l.map Prod.fst).contains k := by - simp_to_raw using Raw₀.Const.contains_insertMany_empty_list + simp_to_raw using Raw₀.Const.contains_insertMany_emptyWithCapacity_list @[simp] theorem mem_ofList [EquivBEq α] [LawfulHashable α] @@ -2031,14 +2087,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : get? (ofList l) k = none := by - simp_to_raw using Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem get?_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : get? (ofList l) k' = some v := by - simp_to_raw using Raw₀.Const.get?_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem theorem get_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} @@ -2046,39 +2102,39 @@ theorem get_ofList_of_mem [LawfulBEq α] (mem : ⟨k, v⟩ ∈ l) {h} : get (ofList l) k' h = v := by - simp_to_raw using Raw₀.Const.get_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem theorem get!_ofList_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (l.map Prod.fst).contains k = false) : get! (ofList l) k = default := by - simp_to_raw using Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem get!_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} [Inhabited β] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : get! (ofList l) k' = v := by - simp_to_raw using Raw₀.Const.get!_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem theorem getD_ofList_of_contains_eq_false [LawfulBEq α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (l.map Prod.fst).contains k = false) : getD (ofList l) k fallback = fallback := by - simp_to_raw using Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getD_ofList_of_mem [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) : getD (ofList l) k' fallback = v := by - simp_to_raw using Raw₀.Const.getD_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : (ofList l).getKey? k = none := by - simp_to_raw using Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} @@ -2086,7 +2142,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : (ofList l).getKey? k' = some k := by - simp_to_raw using Raw₀.Const.getKey?_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} @@ -2095,13 +2151,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α] (mem : k ∈ l.map Prod.fst) {h'} : (ofList l).getKey k' h' = k := by - simp_to_raw using Raw₀.Const.getKey_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : (ofList l).getKey! k = default := by - simp_to_raw using Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} @@ -2109,13 +2165,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : (ofList l).getKey! k' = k := by - simp_to_raw using Raw₀.Const.getKey!_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : (ofList l).getKeyD k fallback = fallback := by - simp_to_raw using Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] {l : List (α × β)} @@ -2123,23 +2179,23 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : k ∈ l.map Prod.fst) : (ofList l).getKeyD k' fallback = k := by - simp_to_raw using Raw₀.Const.getKeyD_insertMany_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem theorem size_ofList [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : (ofList l).size = l.length := by - simp_to_raw using Raw₀.Const.size_insertMany_empty_list + simp_to_raw using Raw₀.Const.size_insertMany_emptyWithCapacity_list theorem size_ofList_le [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (ofList l).size ≤ l.length := by - simp_to_raw using Raw₀.Const.size_insertMany_empty_list_le + simp_to_raw using Raw₀.Const.size_insertMany_emptyWithCapacity_list_le @[simp] theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (ofList l).isEmpty = l.isEmpty := by - simp_to_raw using Raw₀.Const.isEmpty_insertMany_empty_list + simp_to_raw using Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list @[simp] theorem unitOfList_nil : @@ -2156,13 +2212,13 @@ theorem unitOfList_singleton {k : α} : theorem unitOfList_cons {hd : α} {tl : List α} : unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α (fun _ => Unit)).insertIfNew hd ()) tl := by simp_to_raw - rw [Raw₀.Const.insertManyIfNewUnit_empty_list_cons] + rw [Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons] @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (unitOfList l).contains k = l.contains k := by - simp_to_raw using Raw₀.Const.contains_insertManyIfNewUnit_empty_list + simp_to_raw using Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem mem_unitOfList [EquivBEq α] [LawfulHashable α] @@ -2173,13 +2229,13 @@ theorem mem_unitOfList [EquivBEq α] [LawfulHashable α] theorem getKey?_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : getKey? (unitOfList l) k = none := by - simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false theorem getKey?_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : getKey? (unitOfList l) k' = some k := by - simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} @@ -2187,56 +2243,56 @@ theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h'} : getKey (unitOfList l) k' h' = k := by - simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem theorem getKey!_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : getKey! (unitOfList l) k = default := by - simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false theorem getKey!_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : getKey! (unitOfList l) k' = k := by - simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem theorem getKeyD_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) : getKeyD (unitOfList l) k fallback = fallback := by - simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false + simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false theorem getKeyD_unitOfList_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l ) : getKeyD (unitOfList l) k' fallback = k := by - simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem + simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem theorem size_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : l.Pairwise (fun a b => (a == b) = false)) : (unitOfList l).size = l.length := by - simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_empty_list + simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α] {l : List α} : (unitOfList l).size ≤ l.length := by - simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_empty_list_le + simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le @[simp] theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} : (unitOfList l).isEmpty = l.isEmpty := by - simp_to_raw using Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list + simp_to_raw using Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem get?_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : get? (unitOfList l) k = if l.contains k then some () else none := by - simp_to_raw using Raw₀.Const.get?_insertManyIfNewUnit_empty_list + simp_to_raw using Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list @[simp] theorem get_unitOfList @@ -3186,14 +3242,18 @@ end Const end Equiv -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) : - m ~m empty c ↔ m.isEmpty := - ⟨fun h' => (Raw₀.equiv_empty_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mp h', - fun h' => (Raw₀.equiv_empty_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mpr h'⟩ +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) : + m ~m emptyWithCapacity c ↔ m.isEmpty := + ⟨fun h' => (Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mp h', + fun h' => (Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mpr h'⟩ -theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) : +theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) : m ~m ∅ ↔ m.isEmpty := - equiv_empty_iff_isEmpty h + equiv_emptyWithCapacity_iff_isEmpty h + +set_option linter.missingDocs false in +@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")] +abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap.Raw α β} [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index c15d0da887..bc94d50e8d 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -62,12 +62,15 @@ structure HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where namespace HashMap -@[inline, inherit_doc DHashMap.empty] def empty [BEq α] [Hashable α] (capacity := 8) : +@[inline, inherit_doc DHashMap.empty] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : HashMap α β := - ⟨DHashMap.empty capacity⟩ + ⟨DHashMap.emptyWithCapacity capacity⟩ + +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where - emptyCollection := empty + emptyCollection := emptyWithCapacity instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where default := ∅ @@ -83,7 +86,7 @@ structure Equiv (m₁ m₂ : HashMap α β) where (b : β) : HashMap α β := ⟨m.inner.insert a b⟩ -instance : Singleton (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ => HashMap.empty.insert a b⟩ +instance : Singleton (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ => (∅ : HashMap α β).insert a b⟩ instance : Insert (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩ diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 8a88c85898..8e75c53b2d 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -33,12 +33,16 @@ private theorem ext {m m' : HashMap α β} : m.inner = m'.inner → m = m' := by cases m; cases m'; rintro rfl; rfl @[simp] -theorem isEmpty_empty {c} : (empty c : HashMap α β).isEmpty := - DHashMap.isEmpty_empty +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : HashMap α β).isEmpty := + DHashMap.isEmpty_emptyWithCapacity @[simp] -theorem isEmpty_emptyc : (∅ : HashMap α β).isEmpty := - DHashMap.isEmpty_emptyc +theorem isEmpty_empty : (∅ : HashMap α β).isEmpty := + DHashMap.isEmpty_empty + +set_option linter.missingDocs false in +@[deprecated isEmpty_empty (since := "2025-03-12")] +abbrev isEmpty_emptyc := @isEmpty_empty @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : @@ -56,17 +60,26 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := DHashMap.mem_congr hab -@[simp] theorem contains_empty {a : α} {c} : (empty c : HashMap α β).contains a = false := +@[simp] +theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).contains a = false := + DHashMap.contains_emptyWithCapacity + +@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashMap α β) := + DHashMap.not_mem_emptyWithCapacity + +@[simp] theorem contains_empty {a : α} : (∅ : HashMap α β).contains a = false := DHashMap.contains_empty -@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : HashMap α β) := +set_option linter.missingDocs false in +@[deprecated contains_empty (since := "2025-03-12")] +abbrev contains_emptyc := @contains_empty + +@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : HashMap α β) := DHashMap.not_mem_empty -@[simp] theorem contains_emptyc {a : α} : (∅ : HashMap α β).contains a = false := - DHashMap.contains_emptyc - -@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : HashMap α β) := - DHashMap.not_mem_emptyc +set_option linter.missingDocs false in +@[deprecated not_mem_empty (since := "2025-03-12")] +abbrev not_mem_emptyc := @not_mem_empty theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty → m.contains a = false := @@ -123,12 +136,16 @@ theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k simp @[simp] -theorem size_empty {c} : (empty c : HashMap α β).size = 0 := - DHashMap.size_empty +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : HashMap α β).size = 0 := + DHashMap.size_emptyWithCapacity @[simp] -theorem size_emptyc : (∅ : HashMap α β).size = 0 := - DHashMap.size_emptyc +theorem size_empty : (∅ : HashMap α β).size = 0 := + DHashMap.size_empty + +set_option linter.missingDocs false in +@[deprecated size_empty (since := "2025-03-12")] +abbrev size_emptyc := @size_empty theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := DHashMap.isEmpty_eq_size_eq_zero @@ -146,12 +163,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : DHashMap.size_insert_le @[simp] -theorem erase_empty {a : α} {c : Nat} : (empty c : HashMap α β).erase a = empty c := - ext DHashMap.erase_empty +theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashMap α β).erase a = emptyWithCapacity c := + ext DHashMap.erase_emptyWithCapacity @[simp] -theorem erase_emptyc {a : α} : (∅ : HashMap α β).erase a = ∅ := - ext DHashMap.erase_emptyc +theorem erase_empty {a : α} : (∅ : HashMap α β).erase a = ∅ := + ext DHashMap.erase_empty + +set_option linter.missingDocs false in +@[deprecated erase_empty (since := "2025-03-12")] +abbrev erase_emptyc := @erase_empty @[simp] theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} : @@ -209,12 +230,16 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β} : @[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl @[simp] -theorem getElem?_empty {a : α} {c} : (empty c : HashMap α β)[a]? = none := - DHashMap.Const.get?_empty +theorem getElem?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β)[a]? = none := + DHashMap.Const.get?_emptyWithCapacity @[simp] -theorem getElem?_emptyc {a : α} : (∅ : HashMap α β)[a]? = none := - DHashMap.Const.get?_emptyc +theorem getElem?_empty {a : α} : (∅ : HashMap α β)[a]? = none := + DHashMap.Const.get?_empty + +set_option linter.missingDocs false in +@[deprecated getElem?_empty (since := "2025-03-12")] +abbrev getElem?_emptyc := @getElem?_empty theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m[a]? = none := @@ -275,12 +300,16 @@ theorem getElem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b DHashMap.Const.get_congr hab (h' := h') @[simp] -theorem getElem!_empty [Inhabited β] {a : α} {c} : (empty c : HashMap α β)[a]! = default := - DHashMap.Const.get!_empty +theorem getElem!_emptyWithCapacity [Inhabited β] {a : α} {c} : (emptyWithCapacity c : HashMap α β)[a]! = default := + DHashMap.Const.get!_emptyWithCapacity @[simp] -theorem getElem!_emptyc [Inhabited β] {a : α} : (∅ : HashMap α β)[a]! = default := - DHashMap.Const.get!_emptyc +theorem getElem!_empty [Inhabited β] {a : α} : (∅ : HashMap α β)[a]! = default := + DHashMap.Const.get!_empty + +set_option linter.missingDocs false in +@[deprecated getElem!_empty (since := "2025-03-12")] +abbrev getElem!_emptyc := @getElem!_empty theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.isEmpty = true → m[a]! = default := @@ -333,14 +362,18 @@ theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : DHashMap.Const.get!_congr hab @[simp] -theorem getD_empty {a : α} {fallback : β} {c} : - (empty c : HashMap α β).getD a fallback = fallback := - DHashMap.Const.getD_empty +theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : + (emptyWithCapacity c : HashMap α β).getD a fallback = fallback := + DHashMap.Const.getD_emptyWithCapacity @[simp] -theorem getD_emptyc {a : α} {fallback : β} : (∅ : HashMap α β).getD a fallback = fallback := +theorem getD_empty {a : α} {fallback : β} : (∅ : HashMap α β).getD a fallback = fallback := DHashMap.Const.getD_empty +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-12")] +abbrev getD_emptyc := @getD_empty + theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.isEmpty = true → m.getD a fallback = fallback := DHashMap.Const.getD_of_isEmpty @@ -396,12 +429,16 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} DHashMap.Const.getD_congr hab @[simp] -theorem getKey?_empty {a : α} {c} : (empty c : HashMap α β).getKey? a = none := - DHashMap.getKey?_empty +theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).getKey? a = none := + DHashMap.getKey?_emptyWithCapacity @[simp] -theorem getKey?_emptyc {a : α} : (∅ : HashMap α β).getKey? a = none := - DHashMap.getKey?_emptyc +theorem getKey?_empty {a : α} : (∅ : HashMap α β).getKey? a = none := + DHashMap.getKey?_empty + +set_option linter.missingDocs false in +@[deprecated getKey?_empty (since := "2025-03-12")] +abbrev getKey?_emptyc := @getKey?_empty theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.getKey? a = none := @@ -479,12 +516,16 @@ theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k := DHashMap.getKey_eq h @[simp] -theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : HashMap α β).getKey! a = default := - DHashMap.getKey!_empty +theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : HashMap α β).getKey! a = default := + DHashMap.getKey!_emptyWithCapacity @[simp] -theorem getKey!_emptyc [Inhabited α] {a : α} : (∅ : HashMap α β).getKey! a = default := - DHashMap.getKey!_emptyc +theorem getKey!_empty [Inhabited α] {a : α} : (∅ : HashMap α β).getKey! a = default := + DHashMap.getKey!_empty + +set_option linter.missingDocs false in +@[deprecated getKey!_empty (since := "2025-03-12")] +abbrev getKey!_emptyc := @getKey!_empty theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.isEmpty = true → m.getKey! a = default := @@ -544,14 +585,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : DHashMap.getKey!_eq_of_mem h @[simp] -theorem getKeyD_empty {a : α} {fallback : α} {c} : - (empty c : HashMap α β).getKeyD a fallback = fallback := - DHashMap.getKeyD_empty +theorem getKeyD_emptyWithCapacity {a : α} {fallback : α} {c} : + (emptyWithCapacity c : HashMap α β).getKeyD a fallback = fallback := + DHashMap.getKeyD_emptyWithCapacity @[simp] -theorem getKeyD_emptyc {a : α} {fallback : α} : (∅ : HashMap α β).getKeyD a fallback = fallback := +theorem getKeyD_empty {a : α} {fallback : α} : (∅ : HashMap α β).getKeyD a fallback = fallback := DHashMap.getKeyD_empty +set_option linter.missingDocs false in +@[deprecated getKeyD_empty (since := "2025-03-12")] +abbrev getKeyD_emptyc := @getKeyD_empty + theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} : m.isEmpty = true → m.getKeyD a fallback = fallback := DHashMap.getKeyD_of_isEmpty @@ -1992,23 +2037,31 @@ section Equiv variable {m m₁ m₂ : HashMap α β} @[simp] -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : - m ~m empty c ↔ m.isEmpty := - ⟨fun ⟨h⟩ => DHashMap.equiv_empty_iff_isEmpty.mp h, - fun h => ⟨DHashMap.equiv_empty_iff_isEmpty.mpr h⟩⟩ +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : + m ~m emptyWithCapacity c ↔ m.isEmpty := + ⟨fun ⟨h⟩ => DHashMap.equiv_emptyWithCapacity_iff_isEmpty.mp h, + fun h => ⟨DHashMap.equiv_emptyWithCapacity_iff_isEmpty.mpr h⟩⟩ @[simp] -theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty := - equiv_empty_iff_isEmpty +theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty := + equiv_emptyWithCapacity_iff_isEmpty + +set_option linter.missingDocs false in +@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")] +abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty @[simp] -theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : - empty c ~m m ↔ m.isEmpty := - Equiv.comm.trans equiv_empty_iff_isEmpty +theorem emptyWithCapacity_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : + emptyWithCapacity c ~m m ↔ m.isEmpty := + Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty @[simp] -theorem emptyc_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty := - empty_equiv_iff_isEmpty +theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty := + emptyWithCapacity_equiv_iff_isEmpty + +set_option linter.missingDocs false in +@[deprecated empty_equiv_iff_isEmpty (since := "2025-03-12")] +abbrev emptyc_equiv_iff_isEmpty := @empty_equiv_iff_isEmpty theorem equiv_iff_toList_perm [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 94f34982ba..17afb02cf6 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -60,11 +60,14 @@ structure Raw (α : Type u) (β : Type v) where namespace Raw -@[inline, inherit_doc DHashMap.Raw.empty] def empty (capacity := 8) : Raw α β := - ⟨DHashMap.Raw.empty capacity⟩ +@[inline, inherit_doc DHashMap.Raw.empty] def emptyWithCapacity (capacity := 8) : Raw α β := + ⟨DHashMap.Raw.emptyWithCapacity capacity⟩ + +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity instance : EmptyCollection (Raw α β) where - emptyCollection := empty + emptyCollection := emptyWithCapacity instance : Inhabited (Raw α β) where default := ∅ @@ -81,7 +84,7 @@ set_option linter.unusedVariables false in (a : α) (b : β) : Raw α β := ⟨m.inner.insert a b⟩ -instance [BEq α] [Hashable α] : Singleton (α × β) (Raw α β) := ⟨fun ⟨a, b⟩ => Raw.empty.insert a b⟩ +instance [BEq α] [Hashable α] : Singleton (α × β) (Raw α β) := ⟨fun ⟨a, b⟩ => (∅ : Raw α β).insert a b⟩ instance [BEq α] [Hashable α] : Insert (α × β) (Raw α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩ @@ -284,11 +287,15 @@ structure WF [BEq α] [Hashable α] (m : Raw α β) : Prop where /-- Internal implementation detail of the hash map -/ out : m.inner.WF -theorem WF.empty [BEq α] [Hashable α] {c} : (empty c : Raw α β).WF := - ⟨DHashMap.Raw.WF.empty⟩ +theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c} : (emptyWithCapacity c : Raw α β).WF := + ⟨DHashMap.Raw.WF.emptyWithCapacity⟩ -theorem WF.emptyc [BEq α] [Hashable α] : (∅ : Raw α β).WF := - WF.empty +theorem WF.empty [BEq α] [Hashable α] : (∅ : Raw α β).WF := + WF.emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated WF.empty (since := "2025-03-12")] +abbrev WF.emptyc := @WF.empty theorem WF.insert [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β} (h : m.WF) : (m.insert a b).WF := diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index de2db730dd..b2a130c844 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -29,12 +29,16 @@ namespace Raw variable {m : Raw α β} @[simp] -theorem size_empty {c} : (empty c : Raw α β).size = 0 := - DHashMap.Raw.size_empty +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).size = 0 := + DHashMap.Raw.size_emptyWithCapacity @[simp] -theorem size_emptyc : (∅ : Raw α β).size = 0 := - DHashMap.Raw.size_emptyc +theorem size_empty : (∅ : Raw α β).size = 0 := + DHashMap.Raw.size_empty + +set_option linter.missingDocs false in +@[deprecated size_empty (since := "2025-03-12")] +abbrev size_emptyc := @size_empty theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := DHashMap.Raw.isEmpty_eq_size_eq_zero @@ -45,12 +49,16 @@ private theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m' := by variable [BEq α] [Hashable α] @[simp] -theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty := - DHashMap.Raw.isEmpty_empty +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).isEmpty := + DHashMap.Raw.isEmpty_emptyWithCapacity @[simp] -theorem isEmpty_emptyc : (∅ : Raw α β).isEmpty := - DHashMap.Raw.isEmpty_emptyc +theorem isEmpty_empty : (∅ : Raw α β).isEmpty := + DHashMap.Raw.isEmpty_empty + +set_option linter.missingDocs false in +@[deprecated isEmpty_empty (since := "2025-03-12")] +abbrev isEmpty_emptyc := @isEmpty_empty @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} : @@ -68,17 +76,25 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a ∈ m ↔ b ∈ m := DHashMap.Raw.mem_congr h.out hab -@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false := +@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false := + DHashMap.Raw.contains_emptyWithCapacity + +@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) := + DHashMap.Raw.not_mem_emptyWithCapacity + +@[simp] theorem contains_empty {a : α} : (∅ : Raw α β).contains a = false := DHashMap.Raw.contains_empty -@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α β) := +set_option linter.missingDocs false in +@[deprecated contains_empty (since := "2025-03-12")] +abbrev contains_emptyc := @contains_empty + +@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : Raw α β) := DHashMap.Raw.not_mem_empty -@[simp] theorem contains_emptyc {a : α} : (∅ : Raw α β).contains a = false := - DHashMap.Raw.contains_emptyc - -@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) := - DHashMap.Raw.not_mem_emptyc +set_option linter.missingDocs false in +@[deprecated not_mem_empty (since := "2025-03-12")] +abbrev not_mem_emptyc := @not_mem_empty theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty → m.contains a = false := @@ -151,12 +167,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v DHashMap.Raw.size_insert_le h.out @[simp] -theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c := - ext DHashMap.Raw.erase_empty +theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α β).erase k = emptyWithCapacity c := + ext DHashMap.Raw.erase_emptyWithCapacity @[simp] -theorem erase_emptyc {k : α} : (∅ : Raw α β).erase k = ∅ := - ext DHashMap.Raw.erase_emptyc +theorem erase_empty {k : α} : (∅ : Raw α β).erase k = ∅ := + ext DHashMap.Raw.erase_empty + +set_option linter.missingDocs false in +@[deprecated erase_empty (since := "2025-03-12")] +abbrev erase_emptyc := @erase_empty @[simp] theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : @@ -218,12 +238,16 @@ theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β} : @[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl @[simp] -theorem getElem?_empty {a : α} {c} : (empty c : Raw α β)[a]? = none := - DHashMap.Raw.Const.get?_empty +theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β)[a]? = none := + DHashMap.Raw.Const.get?_emptyWithCapacity @[simp] -theorem getElem?_emptyc {a : α} : (∅ : Raw α β)[a]? = none := - DHashMap.Raw.Const.get?_emptyc +theorem get?_empty {a : α} : (∅ : Raw α β)[a]? = none := + DHashMap.Raw.Const.get?_empty + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-12")] +abbrev get?_emptyc := @get?_empty theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m[a]? = none := @@ -287,12 +311,16 @@ theorem getElem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (h DHashMap.Raw.Const.get_congr h.out hab (h' := h') @[simp] -theorem getElem!_empty [Inhabited β] {a : α} {c} : (empty c : Raw α β)[a]! = default := - DHashMap.Raw.Const.get!_empty +theorem getElem!_emptyWithCapacity [Inhabited β] {a : α} {c} : (emptyWithCapacity c : Raw α β)[a]! = default := + DHashMap.Raw.Const.get!_emptyWithCapacity @[simp] -theorem getElem!_emptyc [Inhabited β] {a : α} : (∅ : Raw α β)[a]! = default := - DHashMap.Raw.Const.get!_emptyc +theorem getElem!_empty [Inhabited β] {a : α} : (∅ : Raw α β)[a]! = default := + DHashMap.Raw.Const.get!_empty + +set_option linter.missingDocs false in +@[deprecated getElem!_empty (since := "2025-03-12")] +abbrev getElem!_emptyc := @getElem!_empty theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} : m.isEmpty = true → m[a]! = default := @@ -345,13 +373,17 @@ theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.W DHashMap.Raw.Const.get!_congr h.out hab @[simp] -theorem getD_empty {a : α} {fallback : β} {c} : (empty c : Raw α β).getD a fallback = fallback := - DHashMap.Raw.Const.getD_empty +theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : (emptyWithCapacity c : Raw α β).getD a fallback = fallback := + DHashMap.Raw.Const.getD_emptyWithCapacity @[simp] -theorem getD_emptyc {a : α} {fallback : β} : (∅ : Raw α β).getD a fallback = fallback := +theorem getD_empty {a : α} {fallback : β} : (∅ : Raw α β).getD a fallback = fallback := DHashMap.Raw.Const.getD_empty +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-12")] +abbrev getD_emptyc := @getD_empty + theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} : m.isEmpty = true → m.getD a fallback = fallback := DHashMap.Raw.Const.getD_of_isEmpty h.out @@ -407,12 +439,16 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall DHashMap.Raw.Const.getD_congr h.out hab @[simp] -theorem getKey?_empty {a : α} {c} : (empty c : Raw α β).getKey? a = none := - DHashMap.Raw.getKey?_empty +theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).getKey? a = none := + DHashMap.Raw.getKey?_emptyWithCapacity @[simp] -theorem getKey?_emptyc {a : α} : (∅ : Raw α β).getKey? a = none := - DHashMap.Raw.getKey?_emptyc +theorem getKey?_empty {a : α} : (∅ : Raw α β).getKey? a = none := + DHashMap.Raw.getKey?_empty + +set_option linter.missingDocs false in +@[deprecated getKey?_empty (since := "2025-03-12")] +abbrev getKey?_emptyc := @getKey?_empty theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m.getKey? a = none := @@ -496,12 +532,16 @@ theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) : DHashMap.Raw.getKey_eq h.out h' @[simp] -theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α β).getKey! a = default := - DHashMap.Raw.getKey!_empty +theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : Raw α β).getKey! a = default := + DHashMap.Raw.getKey!_emptyWithCapacity @[simp] -theorem getKey!_emptyc [Inhabited α] {a : α} : (∅ : Raw α β).getKey! a = default := - DHashMap.Raw.getKey!_emptyc +theorem getKey!_empty [Inhabited α] {a : α} : (∅ : Raw α β).getKey! a = default := + DHashMap.Raw.getKey!_empty + +set_option linter.missingDocs false in +@[deprecated getKey!_empty (since := "2025-03-12")] +abbrev getKey!_emptyc := @getKey!_empty theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : m.isEmpty = true → m.getKey! a = default := @@ -562,14 +602,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' DHashMap.Raw.getKey!_eq_of_mem h.out h' @[simp] -theorem getKeyD_empty {a fallback : α} {c} : - (empty c : Raw α β).getKeyD a fallback = fallback := - DHashMap.Raw.getKeyD_empty +theorem getKeyD_emptyWithCapacity {a fallback : α} {c} : + (emptyWithCapacity c : Raw α β).getKeyD a fallback = fallback := + DHashMap.Raw.getKeyD_emptyWithCapacity @[simp] -theorem getKeyD_emptyc {a fallback : α} : (∅ : Raw α β).getKeyD a fallback = fallback := +theorem getKeyD_empty {a fallback : α} : (∅ : Raw α β).getKeyD a fallback = fallback := DHashMap.Raw.getKeyD_empty +set_option linter.missingDocs false in +@[deprecated getKeyD_empty (since := "2025-03-12")] +abbrev getKeyD_emptyc := @getKeyD_empty + theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : m.isEmpty = true → m.getKeyD a fallback = fallback := DHashMap.Raw.getKeyD_of_isEmpty h.out @@ -2025,14 +2069,18 @@ theorem of_forall_mem_unit_iff [LawfulBEq α] end Equiv -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) : - m ~m empty c ↔ m.isEmpty := - ⟨fun ⟨h'⟩ => (DHashMap.Raw.equiv_empty_iff_isEmpty h.1).mp h', - fun h' => ⟨(DHashMap.Raw.equiv_empty_iff_isEmpty h.1).mpr h'⟩⟩ +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) : + m ~m emptyWithCapacity c ↔ m.isEmpty := + ⟨fun ⟨h'⟩ => (DHashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mp h', + fun h' => ⟨(DHashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mpr h'⟩⟩ -theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) : +theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) : m ~m ∅ ↔ m.isEmpty := - equiv_empty_iff_isEmpty h + equiv_emptyWithCapacity_iff_isEmpty h + +set_option linter.missingDocs false in +@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")] +abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty theorem equiv_iff_toList_perm {m₁ m₂ : Raw α β} [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 1fc14c7743..bf9792072b 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -61,11 +61,14 @@ set so that it can hold the given number of elements without reallocating. It is use the empty collection notations `∅` and `{}` to create an empty hash set with the default capacity. -/ -@[inline] def empty [BEq α] [Hashable α] (capacity := 8) : HashSet α := - ⟨HashMap.empty capacity⟩ +@[inline] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : HashSet α := + ⟨HashMap.emptyWithCapacity capacity⟩ + +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) where - emptyCollection := empty + emptyCollection := emptyWithCapacity instance [BEq α] [Hashable α] : Inhabited (HashSet α) where default := ∅ @@ -90,7 +93,7 @@ differently: it will overwrite an existing mapping. @[inline] def insert (m : HashSet α) (a : α) : HashSet α := ⟨m.inner.insertIfNew a ()⟩ -instance : Singleton α (HashSet α) := ⟨fun a => HashSet.empty.insert a⟩ +instance : Singleton α (HashSet α) := ⟨fun a => (∅ : HashSet α).insert a⟩ instance : Insert α (HashSet α) := ⟨fun a s => s.insert a⟩ diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 47761c73b8..19696051d3 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -32,12 +32,16 @@ private theorem ext {m m' : HashSet α} : m.inner = m'.inner → m = m' := by cases m; cases m'; rintro rfl; rfl @[simp] -theorem isEmpty_empty {c} : (empty c : HashSet α).isEmpty := - HashMap.isEmpty_empty +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).isEmpty := + HashMap.isEmpty_emptyWithCapacity @[simp] -theorem isEmpty_emptyc : (∅ : HashSet α).isEmpty := - HashMap.isEmpty_emptyc +theorem isEmpty_empty : (∅ : HashSet α).isEmpty := + HashMap.isEmpty_empty + +set_option linter.missingDocs false in +@[deprecated isEmpty_empty (since := "2025-03-12")] +abbrev isEmpty_emptyc := @isEmpty_empty @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {a : α} : (m.insert a).isEmpty = false := @@ -53,17 +57,26 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := HashMap.mem_congr hab -@[simp] theorem contains_empty {a : α} {c} : (empty c : HashSet α).contains a = false := +@[simp] +theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).contains a = false := + HashMap.contains_emptyWithCapacity + +@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashSet α) := + HashMap.not_mem_emptyWithCapacity + +@[simp] theorem contains_empty {a : α} : (∅ : HashSet α).contains a = false := HashMap.contains_empty -@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : HashSet α) := +set_option linter.missingDocs false in +@[deprecated contains_empty (since := "2025-03-12")] +abbrev contains_emptyc := @contains_empty + +@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : HashSet α) := HashMap.not_mem_empty -@[simp] theorem contains_emptyc {a : α} : (∅ : HashSet α).contains a = false := - HashMap.contains_emptyc - -@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : HashSet α) := - HashMap.not_mem_emptyc +set_option linter.missingDocs false in +@[deprecated not_mem_empty (since := "2025-03-12")] +abbrev not_mem_emptyc := @not_mem_empty theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty → m.contains a = false := @@ -128,12 +141,16 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.ins theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp @[simp] -theorem size_empty {c} : (empty c : HashSet α).size = 0 := - HashMap.size_empty +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).size = 0 := + HashMap.size_emptyWithCapacity @[simp] -theorem size_emptyc : (∅ : HashSet α).size = 0 := - HashMap.size_emptyc +theorem size_empty : (∅ : HashSet α).size = 0 := + HashMap.size_empty + +set_option linter.missingDocs false in +@[deprecated size_empty (since := "2025-03-12")] +abbrev size_emptyc := @size_empty theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := HashMap.isEmpty_eq_size_eq_zero @@ -150,12 +167,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} : HashMap.size_insertIfNew_le @[simp] -theorem erase_empty {a : α} {c : Nat} : (empty c : HashSet α).erase a = empty c := - ext HashMap.erase_empty +theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashSet α).erase a = emptyWithCapacity c := + ext HashMap.erase_emptyWithCapacity @[simp] -theorem erase_emptyc {a : α} : (∅ : HashSet α).erase a = ∅ := - ext HashMap.erase_emptyc +theorem erase_empty {a : α} : (∅ : HashSet α).erase a = ∅ := + ext HashMap.erase_empty + +set_option linter.missingDocs false in +@[deprecated erase_empty (since := "2025-03-12")] +abbrev erase_emptyc := @erase_empty @[simp] theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} : @@ -191,12 +212,16 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} : HashMap.size_le_size_erase @[simp] -theorem get?_empty {a : α} {c} : (empty c : HashSet α).get? a = none := - HashMap.getKey?_empty +theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).get? a = none := + HashMap.getKey?_emptyWithCapacity @[simp] -theorem get?_emptyc {a : α} : (∅ : HashSet α).get? a = none := - HashMap.getKey?_emptyc +theorem get?_empty {a : α} : (∅ : HashSet α).get? a = none := + HashMap.getKey?_empty + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-12")] +abbrev get?_emptyc := @get?_empty theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.get? a = none := @@ -263,12 +288,16 @@ theorem get_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k := HashMap.getKey_eq h @[simp] -theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : HashSet α).get! a = default := - HashMap.getKey!_empty +theorem get!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : HashSet α).get! a = default := + HashMap.getKey!_emptyWithCapacity @[simp] -theorem get!_emptyc [Inhabited α] {a : α} : (∅ : HashSet α).get! a = default := - HashMap.getKey!_emptyc +theorem get!_empty [Inhabited α] {a : α} : (∅ : HashSet α).get! a = default := + HashMap.getKey!_empty + +set_option linter.missingDocs false in +@[deprecated get!_empty (since := "2025-03-12")] +abbrev get!_emptyc := @get!_empty theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.get! a = default := @@ -322,12 +351,16 @@ theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m. HashMap.getKey!_eq_of_mem h @[simp] -theorem getD_empty {a fallback : α} {c} : (empty c : HashSet α).getD a fallback = fallback := - HashMap.getKeyD_empty +theorem getD_emptyWithCapacity {a fallback : α} {c} : (emptyWithCapacity c : HashSet α).getD a fallback = fallback := + HashMap.getKeyD_emptyWithCapacity @[simp] -theorem getD_emptyc {a fallback : α} : (∅ : HashSet α).getD a fallback = fallback := - HashMap.getKeyD_emptyc +theorem getD_empty {a fallback : α} : (∅ : HashSet α).getD a fallback = fallback := + HashMap.getKeyD_empty + +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-12")] +abbrev getD_emptyc := @getD_empty theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.isEmpty = true → m.getD a fallback = fallback := @@ -750,23 +783,31 @@ section Equiv variable {m m₁ m₂ : HashSet α} @[simp] -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : - m ~m empty c ↔ m.isEmpty := - ⟨fun ⟨h⟩ => HashMap.equiv_empty_iff_isEmpty.mp h, - fun h => ⟨HashMap.equiv_empty_iff_isEmpty.mpr h⟩⟩ +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : + m ~m emptyWithCapacity c ↔ m.isEmpty := + ⟨fun ⟨h⟩ => HashMap.equiv_emptyWithCapacity_iff_isEmpty.mp h, + fun h => ⟨HashMap.equiv_emptyWithCapacity_iff_isEmpty.mpr h⟩⟩ @[simp] -theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty := - equiv_empty_iff_isEmpty +theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty := + equiv_emptyWithCapacity_iff_isEmpty + +set_option linter.missingDocs false in +@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")] +abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty @[simp] -theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : - empty c ~m m ↔ m.isEmpty := - Equiv.comm.trans equiv_empty_iff_isEmpty +theorem emptyWithCapacity_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} : + emptyWithCapacity c ~m m ↔ m.isEmpty := + Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty @[simp] -theorem emptyc_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty := - empty_equiv_iff_isEmpty +theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty := + emptyWithCapacity_equiv_iff_isEmpty + +set_option linter.missingDocs false in +@[deprecated empty_equiv_iff_isEmpty (since := "2025-03-12")] +abbrev emptyc_equiv_iff_isEmpty := @empty_equiv_iff_isEmpty theorem equiv_iff_toList_perm [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index e492b26fc2..9d69422796 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -62,11 +62,14 @@ Creates a new empty hash set. The optional parameter `capacity` can be supplied so that it can hold the given number of elements without reallocating. It is also possible to use the empty collection notations `∅` and `{}` to create an empty hash set with the default capacity. -/ -@[inline] def empty (capacity := 8) : Raw α := - ⟨HashMap.Raw.empty capacity⟩ +@[inline] def emptyWithCapacity (capacity := 8) : Raw α := + ⟨HashMap.Raw.emptyWithCapacity capacity⟩ + +@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity] +abbrev empty := @emptyWithCapacity instance : EmptyCollection (Raw α) where - emptyCollection := empty + emptyCollection := emptyWithCapacity instance : Inhabited (Raw α) where default := ∅ @@ -91,7 +94,7 @@ differently: it will overwrite an existing mapping. @[inline] def insert [BEq α] [Hashable α] (m : Raw α) (a : α) : Raw α := ⟨m.inner.insertIfNew a ()⟩ -instance [BEq α] [Hashable α] : Singleton α (Raw α) := ⟨fun a => Raw.empty.insert a⟩ +instance [BEq α] [Hashable α] : Singleton α (Raw α) := ⟨fun a => (∅ : Raw α).insert a⟩ instance [BEq α] [Hashable α] : Insert α (Raw α) := ⟨fun a s => s.insert a⟩ @@ -283,11 +286,15 @@ structure WF [BEq α] [Hashable α] (m : Raw α) : Prop where /-- Internal implementation detail of the hash set -/ out : m.inner.WF -theorem WF.empty [BEq α] [Hashable α] {c} : (empty c : Raw α).WF := - ⟨HashMap.Raw.WF.empty⟩ +theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c} : (emptyWithCapacity c : Raw α).WF := + ⟨HashMap.Raw.WF.emptyWithCapacity⟩ -theorem WF.emptyc [BEq α] [Hashable α] : (∅ : Raw α).WF := - ⟨HashMap.Raw.WF.empty⟩ +theorem WF.empty [BEq α] [Hashable α] : (∅ : Raw α).WF := + WF.emptyWithCapacity + +set_option linter.missingDocs false in +@[deprecated WF.empty (since := "2025-03-12")] +abbrev WF.emptyc := @WF.empty theorem WF.insert [BEq α] [Hashable α] {m : Raw α} {a : α} (h : m.WF) : (m.insert a).WF := ⟨HashMap.Raw.WF.insertIfNew h.out⟩ diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 75aaa5b2e2..d94450c4b1 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -32,12 +32,16 @@ private theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m' := by cases m; cases m'; rintro rfl; rfl @[simp] -theorem size_empty {c} : (empty c : Raw α).size = 0 := - HashMap.Raw.size_empty +theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).size = 0 := + HashMap.Raw.size_emptyWithCapacity @[simp] -theorem size_emptyc : (∅ : Raw α).size = 0 := - HashMap.Raw.size_emptyc +theorem size_empty : (∅ : Raw α).size = 0 := + HashMap.Raw.size_empty + +set_option linter.missingDocs false in +@[deprecated size_empty (since := "2025-03-12")] +abbrev size_emptyc := @size_empty theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := HashMap.Raw.isEmpty_eq_size_eq_zero @@ -45,12 +49,16 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := variable [BEq α] [Hashable α] @[simp] -theorem isEmpty_empty {c} : (empty c : Raw α).isEmpty := - HashMap.Raw.isEmpty_empty +theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).isEmpty := + HashMap.Raw.isEmpty_emptyWithCapacity @[simp] -theorem isEmpty_emptyc : (∅ : Raw α).isEmpty := - HashMap.Raw.isEmpty_emptyc +theorem isEmpty_empty : (∅ : Raw α).isEmpty := + HashMap.Raw.isEmpty_empty + +set_option linter.missingDocs false in +@[deprecated isEmpty_empty (since := "2025-03-12")] +abbrev isEmpty_emptyc := @isEmpty_empty @[simp] theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : @@ -68,17 +76,25 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a ∈ m ↔ b ∈ m := HashMap.Raw.mem_congr h.out hab -@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α).contains a = false := +@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).contains a = false := + HashMap.Raw.contains_emptyWithCapacity + +@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α) := + HashMap.Raw.not_mem_emptyWithCapacity + +@[simp] theorem contains_empty {a : α} : (∅ : Raw α).contains a = false := HashMap.Raw.contains_empty -@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α) := +set_option linter.missingDocs false in +@[deprecated contains_empty (since := "2025-03-12")] +abbrev contains_emptyc := @contains_empty + +@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : Raw α) := HashMap.Raw.not_mem_empty -@[simp] theorem contains_emptyc {a : α} : (∅ : Raw α).contains a = false := - HashMap.Raw.contains_emptyc - -@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α) := - HashMap.Raw.not_mem_emptyc +set_option linter.missingDocs false in +@[deprecated not_mem_empty (since := "2025-03-12")] +abbrev not_mem_emptyc := @not_mem_empty theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty → m.contains a = false := @@ -160,12 +176,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : HashMap.Raw.size_insertIfNew_le h.out @[simp] -theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α).erase k = empty c := - ext HashMap.Raw.erase_empty +theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α).erase k = emptyWithCapacity c := + ext HashMap.Raw.erase_emptyWithCapacity @[simp] -theorem erase_emptyc {k : α} : (∅ : Raw α).erase k = ∅ := - ext HashMap.Raw.erase_emptyc +theorem erase_empty {k : α} : (∅ : Raw α).erase k = ∅ := + ext HashMap.Raw.erase_empty + +set_option linter.missingDocs false in +@[deprecated erase_empty (since := "2025-03-12")] +abbrev erase_emptyc := @erase_empty @[simp] theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : @@ -203,12 +223,16 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} HashMap.Raw.size_le_size_erase h.out @[simp] -theorem get?_empty {a : α} {c} : (empty c : Raw α).get? a = none := - HashMap.Raw.getKey?_empty +theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).get? a = none := + HashMap.Raw.getKey?_emptyWithCapacity @[simp] -theorem get?_emptyc {a : α} : (∅ : Raw α).get? a = none := - HashMap.Raw.getKey?_emptyc +theorem get?_empty {a : α} : (∅ : Raw α).get? a = none := + HashMap.Raw.getKey?_empty + +set_option linter.missingDocs false in +@[deprecated get?_empty (since := "2025-03-12")] +abbrev get?_emptyc := @get?_empty theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m.get? a = none := @@ -283,12 +307,16 @@ theorem get_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) : HashMap.Raw.getKey_eq h.out h' @[simp] -theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α).get! a = default := - HashMap.Raw.getKey!_empty +theorem get!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : Raw α).get! a = default := + HashMap.Raw.getKey!_emptyWithCapacity @[simp] -theorem get!_emptyc [Inhabited α] {a : α} : (∅ : Raw α).get! a = default := - HashMap.Raw.getKey!_emptyc +theorem get!_empty [Inhabited α] {a : α} : (∅ : Raw α).get! a = default := + HashMap.Raw.getKey!_empty + +set_option linter.missingDocs false in +@[deprecated get!_empty (since := "2025-03-12")] +abbrev get!_emptyc := @get!_empty theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m.get! a = default := @@ -344,12 +372,16 @@ theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k HashMap.Raw.getKey!_eq_of_mem h.out h' @[simp] -theorem getD_empty {a fallback : α} {c} : (empty c : Raw α).getD a fallback = fallback := - HashMap.Raw.getKeyD_empty +theorem getD_emptyWithCapacity {a fallback : α} {c} : (emptyWithCapacity c : Raw α).getD a fallback = fallback := + HashMap.Raw.getKeyD_emptyWithCapacity @[simp] -theorem getD_emptyc {a fallback : α} : (∅ : Raw α).getD a fallback = fallback := - HashMap.Raw.getKeyD_emptyc +theorem getD_empty {a fallback : α} : (∅ : Raw α).getD a fallback = fallback := + HashMap.Raw.getKeyD_empty + +set_option linter.missingDocs false in +@[deprecated getD_empty (since := "2025-03-12")] +abbrev getD_emptyc := @getD_empty theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : m.isEmpty = true → m.getD a fallback = fallback := @@ -783,14 +815,18 @@ theorem of_forall_mem_iff [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) end Equiv -theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) : - m ~m empty c ↔ m.isEmpty := - ⟨fun ⟨h'⟩ => (HashMap.Raw.equiv_empty_iff_isEmpty h.1).mp h', - fun h' => ⟨(HashMap.Raw.equiv_empty_iff_isEmpty h.1).mpr h'⟩⟩ +theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) : + m ~m emptyWithCapacity c ↔ m.isEmpty := + ⟨fun ⟨h'⟩ => (HashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mp h', + fun h' => ⟨(HashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mpr h'⟩⟩ -theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) : +theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) : m ~m ∅ ↔ m.isEmpty := - equiv_empty_iff_isEmpty h + equiv_emptyWithCapacity_iff_isEmpty h + +set_option linter.missingDocs false in +@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")] +abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty theorem equiv_iff_toList_perm {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h index ee225c1734..7bbed23ec5 100644 --- a/src/stdlib_flags.h +++ b/src/stdlib_flags.h @@ -11,12 +11,12 @@ options get_default_options() { opts = opts.update({"debug", "proofAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with // builtin elaborators - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); // changes to builtin parsers may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true); diff --git a/tests/lean/run/hashmap-implicits.lean b/tests/lean/run/hashmap-implicits.lean index c0e1b8efe8..4b96ffae51 100644 --- a/tests/lean/run/hashmap-implicits.lean +++ b/tests/lean/run/hashmap-implicits.lean @@ -15,14 +15,14 @@ structure A (α) extends BEq α, Hashable α where def A.add (xs : A α) (x : α) : A α := {xs with foo := xs.foo.insert x 5} -example (xs : A α) (x : α) : ¬x ∈ @DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5 := - DHashMap.not_mem_empty +example (xs : A α) (x : α) : ¬x ∈ @DHashMap.emptyWithCapacity _ (fun _ => Nat) xs.toBEq xs.toHashable 5 := + DHashMap.not_mem_emptyWithCapacity -example (xs : A α) (x : α) : (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by - rw [DHashMap.contains_empty] +example (xs : A α) (x : α) : (@DHashMap.emptyWithCapacity _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by + rw [DHashMap.contains_emptyWithCapacity] -example (xs : A α) (x : α) : DHashMap.Const.get? (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5) x = none := by - rw [DHashMap.Const.get?_empty] +example (xs : A α) (x : α) : DHashMap.Const.get? (@DHashMap.emptyWithCapacity _ (fun _ => Nat) xs.toBEq xs.toHashable 5) x = none := by + rw [DHashMap.Const.get?_emptyWithCapacity] example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size := DHashMap.size_le_size_insert @@ -37,14 +37,14 @@ structure A (α) extends BEq α, Hashable α where def A.add (xs : A α) (x : α) : A α := {xs with foo := xs.foo.insert x 5} -example (xs : A α) (x : α) : ¬x ∈ @HashMap.empty _ Nat xs.toBEq xs.toHashable 5 := - HashMap.not_mem_empty +example (xs : A α) (x : α) : ¬x ∈ @HashMap.emptyWithCapacity _ Nat xs.toBEq xs.toHashable 5 := + HashMap.not_mem_emptyWithCapacity -example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5).contains x = false := by - rw [HashMap.contains_empty] +example (xs : A α) (x : α) : (@HashMap.emptyWithCapacity _ Nat xs.toBEq xs.toHashable 5).contains x = false := by + rw [HashMap.contains_emptyWithCapacity] -example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by - rw [HashMap.getElem?_empty] +example (xs : A α) (x : α) : (@HashMap.emptyWithCapacity _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by + rw [HashMap.getElem?_emptyWithCapacity] example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size := HashMap.size_le_size_insert @@ -59,11 +59,11 @@ structure A (α) extends BEq α, Hashable α where def A.add (xs : A α) (x : α) : A α := {xs with foo := xs.foo.insert x} -example (xs : A α) (x : α) : ¬x ∈ @HashSet.empty _ xs.toBEq xs.toHashable 5 := - DHashMap.not_mem_empty +example (xs : A α) (x : α) : ¬x ∈ @HashSet.emptyWithCapacity _ xs.toBEq xs.toHashable 5 := + HashSet.not_mem_emptyWithCapacity -example (xs : A α) (x : α) : (@HashSet.empty _ xs.toBEq xs.toHashable 5).contains x = false := by - rw [HashSet.contains_empty] +example (xs : A α) (x : α) : (@HashSet.emptyWithCapacity _ xs.toBEq xs.toHashable 5).contains x = false := by + rw [HashSet.contains_emptyWithCapacity] example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x).size := HashSet.size_le_size_insert