Dependent hash map lemmas #
This file contains lemmas about Std.Data.DHashMap. 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.DHashMap.insert_eq_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
{p : (a : α) × β a}
:
Insert.insert p m = m.insert p.fst p.snd
theorem
Std.DHashMap.mem_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
k ∈ m.insert k v
theorem
Std.DHashMap.size_le_size_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
m.size ≤ (m.insert k v).size
theorem
Std.DHashMap.size_erase_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).size ≤ m.size
theorem
Std.DHashMap.contains_eq_isSome_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = (m.getKey? a).isSome
@[simp]
theorem
Std.DHashMap.getKey_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
(m.insert k v).getKey k ⋯ = k
@[simp]
theorem
Std.DHashMap.getKeyD_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
{v : β k}
:
(m.insert k v).getKeyD k fallback = k
@[simp]
theorem
Std.DHashMap.getKeyD_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
(m.erase k).getKeyD k fallback = fallback
theorem
Std.DHashMap.getKeyD_eq_getD_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
m.getKeyD a fallback = (m.getKey? a).getD fallback
theorem
Std.DHashMap.mem_insertIfNew_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
k ∈ m.insertIfNew k v
theorem
Std.DHashMap.contains_of_contains_insertIfNew'
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
This is a restatement of contains_insertIfNew that is written to exactly match the proof
obligation in the statement of get_insertIfNew.
theorem
Std.DHashMap.mem_of_mem_insertIfNew'
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
This is a restatement of mem_insertIfNew that is written to exactly match the proof obligation
in the statement of get_insertIfNew.
theorem
Std.DHashMap.size_le_size_insertIfNew
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
m.size ≤ (m.insertIfNew k v).size
theorem
Std.DHashMap.Const.get_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
{h₁ : a ∈ m.insertIfNew k v}
:
@[simp]
theorem
Std.DHashMap.Const.getThenInsertIfNew?_fst
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
{k : α}
{v : β}
:
(getThenInsertIfNew? m k v).fst = get? m k
@[simp]
theorem
Std.DHashMap.Const.getThenInsertIfNew?_snd
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
{k : α}
{v : β}
:
(getThenInsertIfNew? m k v).snd = m.insertIfNew k v
@[simp]
theorem
Std.DHashMap.length_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
m.keys.length = m.size
@[simp]
theorem
Std.DHashMap.isEmpty_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
m.keys.isEmpty = m.isEmpty
@[simp]
theorem
Std.DHashMap.contains_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
m.keys.contains k = m.contains k
theorem
Std.DHashMap.distinct_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
List.Pairwise (fun (a b : α) => (a == b) = false) m.keys