theorem Std.HashMap.Imp.Buckets.ext {α : Type u_1} {β : Type u_2} {b₁ : Std.HashMap.Imp.Buckets α β} {b₂ : Std.HashMap.Imp.Buckets α β} : b₁.val.data = b₂.val.data → b₁ = b₂

theorem Std.HashMap.Imp.Buckets.update_data {α : Type u_1} {β : Type u_2} (self : Std.HashMap.Imp.Buckets α β) (i : USize) (d : Std.AssocList α β) (h : USize.toNat i < Array.size self.val) : (Std.HashMap.Imp.Buckets.update self i d h).val.data = List.set self.val.data (USize.toNat i) d

theorem Std.HashMap.Imp.Buckets.exists_of_update {α : Type u_1} {β : Type u_2} (self : Std.HashMap.Imp.Buckets α β) (i : USize) (d : Std.AssocList α β) (h : USize.toNat i < Array.size self.val) : ∃ l₁ l₂, self.val.data = l₁ ++ self.val[i] :: l₂ ∧ List.length l₁ = USize.toNat i ∧ (Std.HashMap.Imp.Buckets.update self i d h).val.data = l₁ ++ d :: l₂

theorem Std.HashMap.Imp.Buckets.update_update {α : Type u_1} {β : Type u_2} (self : Std.HashMap.Imp.Buckets α β) (i : USize) (d : Std.AssocList α β) (d' : Std.AssocList α β) (h : USize.toNat i < Array.size self.val) (h' : USize.toNat i < Array.size (Std.HashMap.Imp.Buckets.update self i d h).val) : Std.HashMap.Imp.Buckets.update (Std.HashMap.Imp.Buckets.update self i d h) i d' h' = Std.HashMap.Imp.Buckets.update self i d' h

theorem Std.HashMap.Imp.Buckets.size_eq {α : Type u_1} {β : Type u_2} (data : Std.HashMap.Imp.Buckets α β) : Std.HashMap.Imp.Buckets.size data = Nat.sum (List.map (fun x => List.length (Std.AssocList.toList x)) data.val.data)

theorem Std.HashMap.Imp.Buckets.mk_size {α : Type u_1} {β : Type u_2} {n : Nat} (h : 0 < n) : Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.Buckets.mk n) = 0

theorem Std.HashMap.Imp.Buckets.WF.mk' {α : Type u_1} {β : Type u_2} {n : Nat} [BEq α] [Hashable α] (h : 0 < n) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.Buckets.mk n)

theorem Std.HashMap.Imp.Buckets.WF.update {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {buckets : Std.HashMap.Imp.Buckets α β} {i : USize} {d : Std.AssocList α β} {h : USize.toNat i < Array.size buckets.val} (H : Std.HashMap.Imp.Buckets.WF buckets) (h₁ : ∀ [inst : PartialEquivBEq α] [inst : Std.HashMap.LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (Std.AssocList.toList buckets.val[i]) → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (Std.AssocList.toList d)) (h₂ : Std.AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size buckets.val) = USize.toNat i) buckets.val[i] → Std.AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size buckets.val) = USize.toNat i) d) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.Buckets.update buckets i d h)

theorem Std.HashMap.Imp.reinsertAux_size {α : Type u_1} {β : Type u_2} [Hashable α] (data : Std.HashMap.Imp.Buckets α β) (a : α) (b : β) : Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.reinsertAux data a b) = Nat.succ (Std.HashMap.Imp.Buckets.size data)

theorem Std.HashMap.Imp.reinsertAux_WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {data : Std.HashMap.Imp.Buckets α β} {a : α} {b : β} (H : Std.HashMap.Imp.Buckets.WF data) (h₁ : ∀ [inst : PartialEquivBEq α] [inst : Std.HashMap.LawfulHashable α], Std.AssocList.All (fun x x_1 => ¬(a == x) = true) data.val[(Std.HashMap.Imp.mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val]) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.reinsertAux data a b)

theorem Std.HashMap.Imp.expand_size {α : Type u_1} {β : Type u_2} {sz : Nat} [Hashable α] {buckets : Std.HashMap.Imp.Buckets α β} : Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.expand sz buckets).buckets = Std.HashMap.Imp.Buckets.size buckets

theorem Std.HashMap.Imp.expand_size.go {α : Type u_1} {β : Type u_2} [Hashable α] (i : Nat) (source : Array (Std.AssocList α β)) (target : Std.HashMap.Imp.Buckets α β) (hs : ∀ (j : Nat), j < i → List.getD source.data j Std.AssocList.nil = Std.AssocList.nil) : Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.expand.go i source target) = Nat.sum (List.map (fun x => List.length (Std.AssocList.toList x)) source.data) + Std.HashMap.Imp.Buckets.size target

theorem Std.HashMap.Imp.expand_WF.foldl {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (rank : α → Nat) {l : List (α × β)} {i : Nat} (hl₁ : ∀ [inst : PartialEquivBEq α] [inst : Std.HashMap.LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l) (hl₂ : ∀ (x : α × β), x ∈ l → rank x.fst = i) {target : Std.HashMap.Imp.Buckets α β} (ht₁ : Std.HashMap.Imp.Buckets.WF target) (ht₂ : ∀ (bucket : Std.AssocList α β), bucket ∈ target.val.data → Std.AssocList.All (fun k x => rank k ≤ i ∧ ∀ [inst : PartialEquivBEq α] [inst : Std.HashMap.LawfulHashable α] (x : α × β), x ∈ l → ¬(x.fst == k) = true) bucket) : Std.HashMap.Imp.Buckets.WF (List.foldl (fun d x => Std.HashMap.Imp.reinsertAux d x.fst x.snd) target l) ∧ ∀ (bucket : Std.AssocList α β), bucket ∈ (List.foldl (fun d x => Std.HashMap.Imp.reinsertAux d x.fst x.snd) target l).val.data → Std.AssocList.All (fun k x => rank k ≤ i) bucket

theorem Std.HashMap.Imp.expand_WF {α : Type u_1} {β : Type u_2} {sz : Nat} [BEq α] [Hashable α] {buckets : Std.HashMap.Imp.Buckets α β} (H : Std.HashMap.Imp.Buckets.WF buckets) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.expand sz buckets).buckets

theorem Std.HashMap.Imp.expand_WF.go {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (i : Nat) {source : Array (Std.AssocList α β)} (hs₁ : ∀ [inst : Std.HashMap.LawfulHashable α] [inst : PartialEquivBEq α] (bucket : Std.AssocList α β), bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (Std.AssocList.toList bucket)) (hs₂ : ∀ (j : Nat) (h : j < Array.size source), Std.AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]) {target : Std.HashMap.Imp.Buckets α β} (ht : Std.HashMap.Imp.Buckets.WF target ∧ ∀ (bucket : Std.AssocList α β), bucket ∈ target.val.data → Std.AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.expand.go i source target)

theorem Std.HashMap.Imp.insert_size {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} {k : α} {v : β} (h : m.size = Std.HashMap.Imp.Buckets.size m.buckets) : (Std.HashMap.Imp.insert m k v).size = Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.insert m k v).buckets

theorem Std.HashMap.Imp.insert_WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} {k : α} {v : β} (h : Std.HashMap.Imp.Buckets.WF m.buckets) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.insert m k v).buckets

theorem Std.HashMap.Imp.erase_size {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} {k : α} (h : m.size = Std.HashMap.Imp.Buckets.size m.buckets) : (Std.HashMap.Imp.erase m k).size = Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.erase m k).buckets

theorem Std.HashMap.Imp.erase_WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} {k : α} (h : Std.HashMap.Imp.Buckets.WF m.buckets) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.erase m k).buckets

theorem Std.HashMap.Imp.modify_size {α : Type u_1} {β : Type u_2} {f : α → β → β} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} {k : α} (h : m.size = Std.HashMap.Imp.Buckets.size m.buckets) : (Std.HashMap.Imp.modify m k f).size = Std.HashMap.Imp.Buckets.size (Std.HashMap.Imp.modify m k f).buckets

theorem Std.HashMap.Imp.modify_WF {α : Type u_1} {β : Type u_2} {f : α → β → β} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} {k : α} (h : Std.HashMap.Imp.Buckets.WF m.buckets) : Std.HashMap.Imp.Buckets.WF (Std.HashMap.Imp.modify m k f).buckets

theorem Std.HashMap.Imp.WF.out {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} (h : Std.HashMap.Imp.WF m) : m.size = Std.HashMap.Imp.Buckets.size m.buckets ∧ Std.HashMap.Imp.Buckets.WF m.buckets

theorem Std.HashMap.Imp.WF_iff {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} : Std.HashMap.Imp.WF m ↔ m.size = Std.HashMap.Imp.Buckets.size m.buckets ∧ Std.HashMap.Imp.Buckets.WF m.buckets

theorem Std.HashMap.Imp.WF.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} (H : Std.HashMap.Imp.WF m) : Std.HashMap.Imp.WF (Std.HashMap.Imp.mapVal f m)

theorem Std.HashMap.Imp.WF.filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → Option γ} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} (H : Std.HashMap.Imp.WF m) : Std.HashMap.Imp.WF (Std.HashMap.Imp.filterMap f m)

@[inline]

def Std.HashMap.mapVal {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → Std.HashMap α β → Std.HashMap α γ

Map a function over the values in the map.

Equations

• Std.HashMap.mapVal f self = { val := Std.HashMap.Imp.mapVal f self.val, property := (_ : Std.HashMap.Imp.WF (Std.HashMap.Imp.mapVal f self.val)) }

@[inline]

def Std.HashMap.filterMap {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → {γ : Type u_3} → (α → β → Option γ) → Std.HashMap α β → Std.HashMap α γ

Applies f to each key-value pair a, b in the map. If it returns some c then a, c is pushed into the new map; else the key is removed from the map.

Equations

• Std.HashMap.filterMap f self = { val := Std.HashMap.Imp.filterMap f self.val, property := (_ : Std.HashMap.Imp.WF (Std.HashMap.Imp.filterMap f self.val)) }

@[inline]

def Std.HashMap.filter {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → (α → β → Bool) → Std.HashMap α β → Std.HashMap α β

Constructs a map with the set of all pairs a, b such that f returns true.

Equations

• Std.HashMap.filter f self = Std.HashMap.filterMap (fun a b => bif f a b then some b else none) self