Hash map lemmas #
This module contains lemmas about Std.Data.HashMap. Most of the lemmas require
EquivBEq α and LawfulHashable α for the key type α. The easiest way to obtain these instances
is to provide an instance of LawfulBEq α.
@[simp]
theorem
Std.HashMap.insert_eq_insert
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
{p : α × β}
:
Insert.insert p m = m.insert p.fst p.snd
theorem
Std.HashMap.mem_insert_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
k ∈ m.insert k v
theorem
Std.HashMap.size_le_size_insert
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
m.size ≤ (m.insert k v).size
theorem
Std.HashMap.size_erase_le
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).size ≤ m.size
theorem
Std.HashMap.contains_eq_isSome_getElem?
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = m[a]?.isSome
@[simp]
theorem
Std.HashMap.getElem_insert_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
(m.insert k v)[k] = v
@[simp]
theorem
Std.HashMap.getD_insert_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{fallback v : β}
:
(m.insert k v).getD k fallback = v
@[simp]
theorem
Std.HashMap.getD_erase_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{fallback : β}
:
(m.erase k).getD k fallback = fallback
theorem
Std.HashMap.getD_eq_getD_getElem?
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
m.getD a fallback = m[a]?.getD fallback
theorem
Std.HashMap.contains_eq_isSome_getKey?
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = (m.getKey? a).isSome
@[simp]
theorem
Std.HashMap.getKey_insert_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
(m.insert k v).getKey k ⋯ = k
@[simp]
theorem
Std.HashMap.getKeyD_insert_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
{v : β}
:
(m.insert k v).getKeyD k fallback = k
@[simp]
theorem
Std.HashMap.getKeyD_erase_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
(m.erase k).getKeyD k fallback = fallback
theorem
Std.HashMap.getKeyD_eq_getD_getKey?
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
m.getKeyD a fallback = (m.getKey? a).getD fallback
theorem
Std.HashMap.mem_insertIfNew_self
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
k ∈ m.insertIfNew k v
theorem
Std.HashMap.contains_of_contains_insertIfNew'
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
:
This is a restatement of contains_insertIfNew that is written to exactly match the proof
obligation in the statement of getElem_insertIfNew.
theorem
Std.HashMap.mem_of_mem_insertIfNew'
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
:
This is a restatement of mem_insertIfNew that is written to exactly match the proof obligation
in the statement of getElem_insertIfNew.
theorem
Std.HashMap.size_le_size_insertIfNew
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
m.size ≤ (m.insertIfNew k v).size
instance
Std.HashMap.instLawfulGetElemMemOfEquivBEqOfLawfulHashable
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
:
LawfulGetElem (HashMap α β) α β fun (m : HashMap α β) (a : α) => a ∈ m
@[simp]
theorem
Std.HashMap.length_keys
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
m.keys.length = m.size
@[simp]
theorem
Std.HashMap.isEmpty_keys
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
m.keys.isEmpty = m.isEmpty
@[simp]
theorem
Std.HashMap.contains_keys
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
m.keys.contains k = m.contains k
theorem
Std.HashMap.distinct_keys
{α : Type u}
{β : Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
List.Pairwise (fun (a b : α) => (a == b) = false) m.keys