Hash set lemmas #
This module contains lemmas about Std.Data.HashSet. 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.HashSet.isEmpty_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{c : Nat}
:
(Std.HashSet.empty c).isEmpty = true
@[simp]
theorem
Std.HashSet.isEmpty_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.mem_iff_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
{a : α}
:
theorem
Std.HashSet.contains_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a b : α}
(hab : (a == b) = true)
:
m.contains a = m.contains b
theorem
Std.HashSet.mem_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a b : α}
(hab : (a == b) = true)
:
@[simp]
theorem
Std.HashSet.contains_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
(Std.HashSet.empty c).contains a = false
@[simp]
theorem
Std.HashSet.not_mem_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
¬a ∈ Std.HashSet.empty c
theorem
Std.HashSet.contains_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.not_mem_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.isEmpty_eq_false_iff_exists_contains_eq_true
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.HashSet.isEmpty_eq_false_iff_exists_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.HashSet.isEmpty_iff_forall_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.HashSet.isEmpty_iff_forall_not_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.HashSet.insert_eq_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
{a : α}
:
@[simp]
theorem
Std.HashSet.contains_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
@[simp]
theorem
Std.HashSet.mem_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.contains_of_contains_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.mem_of_mem_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.contains_of_contains_insert'
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
This is a restatement of contains_insert that is written to exactly match the proof
obligation in the statement of get_insert.
theorem
Std.HashSet.mem_of_mem_insert'
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
This is a restatement of mem_insert that is written to exactly match the proof obligation
in the statement of get_insert.
@[simp]
theorem
Std.HashSet.contains_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.mem_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
k ∈ m.insert k
@[simp]
theorem
Std.HashSet.size_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{c : Nat}
:
(Std.HashSet.empty c).size = 0
theorem
Std.HashSet.isEmpty_eq_size_eq_zero
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
:
theorem
Std.HashSet.size_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.size_le_size_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
m.size ≤ (m.insert k).size
theorem
Std.HashSet.size_insert_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.erase_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
(Std.HashSet.empty c).erase a = Std.HashSet.empty c
@[simp]
theorem
Std.HashSet.isEmpty_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.contains_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
@[simp]
theorem
Std.HashSet.mem_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.contains_of_contains_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.mem_of_mem_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.size_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.size_erase_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).size ≤ m.size
theorem
Std.HashSet.size_le_size_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.get?_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
(Std.HashSet.empty c).get? a = none
theorem
Std.HashSet.get?_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.contains_eq_isSome_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = (m.get? a).isSome
theorem
Std.HashSet.get?_eq_none_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.get?_eq_none
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.get?_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
@[simp]
theorem
Std.HashSet.get?_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).get? k = none
@[simp]
theorem
Std.HashSet.get_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{h' : a ∈ m.erase k}
:
(m.erase k).get a h' = m.get a ⋯
theorem
Std.HashSet.get?_eq_some_get
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{h' : a ∈ m}
:
@[simp]
theorem
Std.HashSet.get!_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[Inhabited α]
{a : α}
{c : Nat}
:
(Std.HashSet.empty c).get! a = default
theorem
Std.HashSet.get!_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[Inhabited α]
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.get!_eq_default_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[Inhabited α]
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.get!_eq_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[Inhabited α]
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.HashSet.get!_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[Inhabited α]
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
@[simp]
theorem
Std.HashSet.get!_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[Inhabited α]
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).get! k = default
theorem
Std.HashSet.get?_eq_some_get!_of_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.HashSet.get?_eq_some_get!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.HashSet.get!_eq_get!_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
m.get! a = (m.get? a).get!
theorem
Std.HashSet.get_eq_get!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{h' : a ∈ m}
:
m.get a h' = m.get! a
@[simp]
theorem
Std.HashSet.getD_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a fallback : α}
{c : Nat}
:
(Std.HashSet.empty c).getD a fallback = fallback
theorem
Std.HashSet.getD_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.getD_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a fallback : α}
:
theorem
Std.HashSet.getD_eq_fallback_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.getD_eq_fallback
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.getD_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a fallback : α}
:
@[simp]
theorem
Std.HashSet.getD_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
(m.erase k).getD k fallback = fallback
theorem
Std.HashSet.get?_eq_some_getD_of_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.get?_eq_some_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.getD_eq_getD_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
m.getD a fallback = (m.get? a).getD fallback
theorem
Std.HashSet.get_eq_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
{h' : a ∈ m}
:
m.get a h' = m.getD a fallback
theorem
Std.HashSet.get!_eq_getD_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
m.get! a = m.getD a default
@[simp]
theorem
Std.HashSet.containsThenInsert_fst
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
{k : α}
:
(m.containsThenInsert k).fst = m.contains k
@[simp]
theorem
Std.HashSet.containsThenInsert_snd
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
{k : α}
:
(m.containsThenInsert k).snd = m.insert k
@[simp]
theorem
Std.HashSet.length_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
m.toList.length = m.size
@[simp]
theorem
Std.HashSet.isEmpty_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
m.toList.isEmpty = m.isEmpty
@[simp]
theorem
Std.HashSet.contains_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
m.toList.contains k = m.contains k
@[simp]
theorem
Std.HashSet.mem_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[LawfulBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.distinct_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
List.Pairwise (fun (a b : α) => (a == b) = false) m.toList