Documentation

Std.Data.HashMap.WF

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.datab₁ = 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.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) :
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]) :
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 < iList.getD source.data j Std.AssocList.nil = Std.AssocList.nil) :
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 lrank x.fst = i) {target : Std.HashMap.Imp.Buckets α β} (ht₁ : Std.HashMap.Imp.Buckets.WF target) (ht₂ : ∀ (bucket : Std.AssocList α β), bucket target.val.dataStd.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.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 α] [Hashable α] {buckets : Std.HashMap.Imp.Buckets α β} (H : Std.HashMap.Imp.Buckets.WF 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.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 (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.dataStd.AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket) :
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) :
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) :
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) :
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) :
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) :
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) :
theorem Std.HashMap.Imp.WF.out {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Std.HashMap.Imp α β} (h : Std.HashMap.Imp.WF m) :
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) :
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) :
@[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
Instances For
    @[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
    Instances For
      @[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
      Instances For