Documentation

Batteries.Data.HashMap.WF

theorem Batteries.HashMap.Imp.Buckets.ext_iff {α : Type u_1} {β : Type u_2} {b₁ : Batteries.HashMap.Imp.Buckets α β} {b₂ : Batteries.HashMap.Imp.Buckets α β} :
b₁ = b₂ b₁.val.toList = b₂.val.toList
theorem Batteries.HashMap.Imp.Buckets.ext {α : Type u_1} {β : Type u_2} {b₁ : Batteries.HashMap.Imp.Buckets α β} {b₂ : Batteries.HashMap.Imp.Buckets α β} :
b₁.val.toList = b₂.val.toListb₁ = b₂
theorem Batteries.HashMap.Imp.Buckets.toList_update {α : Type u_1} {β : Type u_2} (self : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (h : i.toNat < self.val.size) :
(self.update i d h).val.toList = self.val.toList.set i.toNat d
@[deprecated Batteries.HashMap.Imp.Buckets.toList_update]
theorem Batteries.HashMap.Imp.Buckets.update_data {α : Type u_1} {β : Type u_2} (self : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (h : i.toNat < self.val.size) :
(self.update i d h).val.toList = self.val.toList.set i.toNat d

Alias of Batteries.HashMap.Imp.Buckets.toList_update.

theorem Batteries.HashMap.Imp.Buckets.exists_of_update {α : Type u_1} {β : Type u_2} (self : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (h : i.toNat < self.val.size) :
∃ (l₁ : List (Batteries.AssocList α β)), ∃ (l₂ : List (Batteries.AssocList α β)), self.val.toList = l₁ ++ self.val[i] :: l₂ l₁.length = i.toNat (self.update i d h).val.toList = l₁ ++ d :: l₂
theorem Batteries.HashMap.Imp.Buckets.update_update {α : Type u_1} {β : Type u_2} (self : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (d' : Batteries.AssocList α β) (h : i.toNat < self.val.size) (h' : i.toNat < (self.update i d h).val.size) :
(self.update i d h).update i d' h' = self.update i d' h
theorem Batteries.HashMap.Imp.Buckets.size_eq {α : Type u_1} {β : Type u_2} (data : Batteries.HashMap.Imp.Buckets α β) :
data.size = Nat.sum (List.map (fun (x : Batteries.AssocList α β) => x.toList.length) data.val.toList)
theorem Batteries.HashMap.Imp.Buckets.mk_size {α : Type u_1} {β : Type u_2} {n : Nat} (h : 0 < n) :
theorem Batteries.HashMap.Imp.Buckets.WF.mk' {α : Type u_1} {β : Type u_2} {n : Nat} [BEq α] [Hashable α] (h : 0 < n) :
theorem Batteries.HashMap.Imp.Buckets.WF.update {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {buckets : Batteries.HashMap.Imp.Buckets α β} {i : USize} {d : Batteries.AssocList α β} {h : i.toNat < buckets.val.size} (H : buckets.WF) (h₁ : ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α], List.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) buckets.val[i].toListList.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) d.toList) (h₂ : Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % buckets.val.size).toNat = i.toNat) buckets.val[i]Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % buckets.val.size).toNat = i.toNat) d) :
(buckets.update i d h).WF
theorem Batteries.HashMap.Imp.reinsertAux_size {α : Type u_1} {β : Type u_2} [Hashable α] (data : Batteries.HashMap.Imp.Buckets α β) (a : α) (b : β) :
(Batteries.HashMap.Imp.reinsertAux data a b).size = data.size.succ
theorem Batteries.HashMap.Imp.reinsertAux_WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {data : Batteries.HashMap.Imp.Buckets α β} {a : α} {b : β} (H : data.WF) (h₁ : ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α], Batteries.AssocList.All (fun (x : α) (x_1 : β) => ¬(a == x) = true) data.val[(Batteries.HashMap.Imp.mkIdx (hash a).toUSize).val]) :
theorem Batteries.HashMap.Imp.expand_size {α : Type u_1} {β : Type u_2} {sz : Nat} [Hashable α] {buckets : Batteries.HashMap.Imp.Buckets α β} :
(Batteries.HashMap.Imp.expand sz buckets).buckets.size = buckets.size
@[irreducible]
theorem Batteries.HashMap.Imp.expand_size.go {α : Type u_1} {β : Type u_2} [Hashable α] (i : Nat) (source : Array (Batteries.AssocList α β)) (target : Batteries.HashMap.Imp.Buckets α β) (hs : ∀ (j : Nat), j < isource.toList[j]?.getD Batteries.AssocList.nil = Batteries.AssocList.nil) :
(Batteries.HashMap.Imp.expand.go i source target).size = Nat.sum (List.map (fun (x : Batteries.AssocList α β) => x.toList.length) source.toList) + target.size
theorem Batteries.HashMap.Imp.expand_WF.foldl {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (rank : αNat) {l : List (α × β)} {i : Nat} (hl₁ : ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α], List.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) l) (hl₂ : ∀ (x : α × β), x lrank x.fst = i) {target : Batteries.HashMap.Imp.Buckets α β} (ht₁ : target.WF) (ht₂ : ∀ (bucket : Batteries.AssocList α β), bucket target.val.toListBatteries.AssocList.All (fun (k : α) (x : β) => rank k i ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α] (x : α × β), x l¬(x.fst == k) = true) bucket) :
(List.foldl (fun (d : Batteries.HashMap.Imp.Buckets α β) (x : α × β) => Batteries.HashMap.Imp.reinsertAux d x.fst x.snd) target l).WF ∀ (bucket : Batteries.AssocList α β), bucket (List.foldl (fun (d : Batteries.HashMap.Imp.Buckets α β) (x : α × β) => Batteries.HashMap.Imp.reinsertAux d x.fst x.snd) target l).val.toListBatteries.AssocList.All (fun (k : α) (x : β) => rank k i) bucket
theorem Batteries.HashMap.Imp.expand_WF {α : Type u_1} {β : Type u_2} {sz : Nat} [BEq α] [Hashable α] {buckets : Batteries.HashMap.Imp.Buckets α β} (H : buckets.WF) :
(Batteries.HashMap.Imp.expand sz buckets).buckets.WF
@[irreducible]
theorem Batteries.HashMap.Imp.expand_WF.go {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (i : Nat) {source : Array (Batteries.AssocList α β)} (hs₁ : ∀ [inst : Batteries.HashMap.LawfulHashable α] [inst : PartialEquivBEq α] (bucket : Batteries.AssocList α β), bucket source.toListList.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) bucket.toList) (hs₂ : ∀ (j : Nat) (h : j < source.size), Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % source.size).toNat = j) source[j]) {target : Batteries.HashMap.Imp.Buckets α β} (ht : target.WF ∀ (bucket : Batteries.AssocList α β), bucket target.val.toListBatteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % source.size).toNat < i) bucket) :
(Batteries.HashMap.Imp.expand.go i source target).WF
theorem Batteries.HashMap.Imp.insert_size {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} {k : α} {v : β} (h : m.size = m.buckets.size) :
(m.insert k v).size = (m.insert k v).buckets.size
theorem Batteries.HashMap.Imp.insert_WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} {k : α} {v : β} (h : m.buckets.WF) :
(m.insert k v).buckets.WF
theorem Batteries.HashMap.Imp.erase_size {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} {k : α} (h : m.size = m.buckets.size) :
(m.erase k).size = (m.erase k).buckets.size
theorem Batteries.HashMap.Imp.erase_WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} {k : α} (h : m.buckets.WF) :
(m.erase k).buckets.WF
theorem Batteries.HashMap.Imp.modify_size {α : Type u_1} {β : Type u_2} {f : αββ} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} {k : α} (h : m.size = m.buckets.size) :
(m.modify k f).size = (m.modify k f).buckets.size
theorem Batteries.HashMap.Imp.modify_WF {α : Type u_1} {β : Type u_2} {f : αββ} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} {k : α} (h : m.buckets.WF) :
(m.modify k f).buckets.WF
theorem Batteries.HashMap.Imp.WF.out {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} (h : m.WF) :
m.size = m.buckets.size m.buckets.WF
theorem Batteries.HashMap.Imp.WF_iff {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} :
m.WF m.size = m.buckets.size m.buckets.WF
theorem Batteries.HashMap.Imp.WF.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} (H : m.WF) :
theorem Batteries.HashMap.Imp.WF.filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβOption γ} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} (H : m.WF) :
@[inline]
def Batteries.HashMap.mapVal {α : Type u_1} :
{x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → {γ : Type u_3} → (αβγ)Batteries.HashMap α βBatteries.HashMap α γ

Map a function over the values in the map.

Equations
Instances For
    @[inline]
    def Batteries.HashMap.filterMap {α : Type u_1} :
    {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → {γ : Type u_3} → (αβOption γ)Batteries.HashMap α βBatteries.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 Batteries.HashMap.filter {α : Type u_1} :
      {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → (αβBool)Batteries.HashMap α βBatteries.HashMap α β

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

      Equations
      Instances For