Documentation

Std.Data.HashMap.WF

theorem Std.HashMap.Imp.Buckets.ext {α : Type u_1} {β : Type u_2} {b₁ : } {b₂ : } :
b₁.val.data = b₂.val.datab₁ = b₂
theorem Std.HashMap.Imp.Buckets.update_data {α : Type u_1} {β : Type u_2} (self : ) (i : USize) (d : ) (h : < Array.size self.val) :
().val.data = List.set self.val.data () d
theorem Std.HashMap.Imp.Buckets.exists_of_update {α : Type u_1} {β : Type u_2} (self : ) (i : USize) (d : ) (h : < Array.size self.val) :
l₁ l₂, self.val.data = l₁ ++ self.val[i] :: l₂ ().val.data = l₁ ++ d :: l₂
theorem Std.HashMap.Imp.Buckets.update_update {α : Type u_1} {β : Type u_2} (self : ) (i : USize) (d : ) (d' : ) (h : < Array.size self.val) (h' : < Array.size ().val) :
theorem Std.HashMap.Imp.Buckets.size_eq {α : Type u_1} {β : Type u_2} (data : ) :
= Nat.sum (List.map (fun x => ) data.val.data)
theorem Std.HashMap.Imp.Buckets.mk_size {α : Type u_1} {β : Type u_2} {n : Nat} (h : 0 < n) :
theorem Std.HashMap.Imp.Buckets.WF.mk' {α : Type u_1} {β : Type u_2} {n : Nat} [BEq α] [] (h : 0 < n) :
theorem Std.HashMap.Imp.Buckets.WF.update {α : Type u_1} {β : Type u_2} [BEq α] [] {buckets : } {i : USize} {d : } {h : < Array.size buckets.val} (H : Std.HashMap.Imp.Buckets.WF buckets) (h₁ : ∀ [inst : ] [inst : ], 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) ()) (h₂ : Std.AssocList.All (fun k x => USize.toNat ( % Array.size buckets.val) = ) buckets.val[i]Std.AssocList.All (fun k x => USize.toNat ( % Array.size buckets.val) = ) d) :
theorem Std.HashMap.Imp.reinsertAux_size {α : Type u_1} {β : Type u_2} [] (data : ) (a : α) (b : β) :
theorem Std.HashMap.Imp.reinsertAux_WF {α : Type u_1} {β : Type u_2} [BEq α] [] {data : } {a : α} {b : β} (H : ) (h₁ : ∀ [inst : ] [inst : ], Std.AssocList.All (fun x x_1 => ¬(a == x) = true) data.val[(Std.HashMap.Imp.mkIdx (_ : 0 < Array.size data.val) ()).val]) :
theorem Std.HashMap.Imp.expand_size {α : Type u_1} {β : Type u_2} {sz : Nat} [] {buckets : } :
theorem Std.HashMap.Imp.expand_size.go {α : Type u_1} {β : Type u_2} [] (i : Nat) (source : Array ()) (target : ) (hs : ∀ (j : Nat), j < iList.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 => ) source.data) +
theorem Std.HashMap.Imp.expand_WF.foldl {α : Type u_1} {β : Type u_2} [BEq α] [] (rank : αNat) {l : List (α × β)} {i : Nat} (hl₁ : ∀ [inst : ] [inst : ], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l) (hl₂ : ∀ (x : α × β), x lrank x.fst = i) {target : } (ht₁ : ) (ht₂ : ∀ (bucket : ), bucket target.val.dataStd.AssocList.All (fun k x => rank k i ∀ [inst : ] [inst : ] (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 : ), bucket (List.foldl (fun d x => Std.HashMap.Imp.reinsertAux d x.fst x.snd) target l).val.dataStd.AssocList.All (fun k x => rank k i) bucket
theorem Std.HashMap.Imp.expand_WF {α : Type u_1} {β : Type u_2} {sz : Nat} [BEq α] [] {buckets : } (H : Std.HashMap.Imp.Buckets.WF buckets) :
theorem Std.HashMap.Imp.expand_WF.go {α : Type u_1} {β : Type u_2} [BEq α] [] (i : Nat) {source : Array ()} (hs₁ : ∀ [inst : ] [inst : ] (bucket : ), bucket source.dataList.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 ( % Array.size source) = j) source[j]) {target : } (ht : ∀ (bucket : ), bucket target.val.dataStd.AssocList.All (fun k x => USize.toNat ( % Array.size source) < i) bucket) :
theorem Std.HashMap.Imp.insert_size {α : Type u_1} {β : Type u_2} [BEq α] [] {m : } {k : α} {v : β} (h : m.size = Std.HashMap.Imp.Buckets.size m.buckets) :
().size = Std.HashMap.Imp.Buckets.size ().buckets
theorem Std.HashMap.Imp.insert_WF {α : Type u_1} {β : Type u_2} [BEq α] [] {m : } {k : α} {v : β} (h : Std.HashMap.Imp.Buckets.WF m.buckets) :
theorem Std.HashMap.Imp.erase_size {α : Type u_1} {β : Type u_2} [BEq α] [] {m : } {k : α} (h : m.size = Std.HashMap.Imp.Buckets.size m.buckets) :
().size = Std.HashMap.Imp.Buckets.size ().buckets
theorem Std.HashMap.Imp.erase_WF {α : Type u_1} {β : Type u_2} [BEq α] [] {m : } {k : α} (h : Std.HashMap.Imp.Buckets.WF m.buckets) :
theorem Std.HashMap.Imp.modify_size {α : Type u_1} {β : Type u_2} {f : αββ} [BEq α] [] {m : } {k : α} (h : m.size = Std.HashMap.Imp.Buckets.size m.buckets) :
().size = Std.HashMap.Imp.Buckets.size ().buckets
theorem Std.HashMap.Imp.modify_WF {α : Type u_1} {β : Type u_2} {f : αββ} [BEq α] [] {m : } {k : α} (h : Std.HashMap.Imp.Buckets.WF m.buckets) :
theorem Std.HashMap.Imp.WF.out {α : Type u_1} {β : Type u_2} [BEq α] [] {m : } (h : ) :
theorem Std.HashMap.Imp.WF_iff {α : Type u_1} {β : Type u_2} [BEq α] [] {m : } :
theorem Std.HashMap.Imp.WF.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} [BEq α] [] {m : } (H : ) :
theorem Std.HashMap.Imp.WF.filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} [BEq α] [] {m : } (H : ) :
@[inline]
def Std.HashMap.mapVal {α : Type u_1} :
{x : BEq α} → {x_1 : } → {β : Type u_2} → {γ : Type u_3} → (αβγ) →

Map a function over the values in the map.

Instances For
@[inline]
def Std.HashMap.filterMap {α : Type u_1} :
{x : BEq α} → {x_1 : } → {β : Type u_2} → {γ : Type u_3} → (αβ) →

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.

Instances For
@[inline]
def Std.HashMap.filter {α : Type u_1} :
{x : BEq α} → {x_1 : } → {β : Type u_2} → (αβBool) →

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

Instances For