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_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
@[simp]
theorem
Std.HashSet.insert_eq_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
{a : α}
:
theorem
Std.HashSet.contains_of_contains_insert'
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : 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 : 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
.
theorem
Std.HashSet.contains_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.size_insert_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.isEmpty_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.contains_of_contains_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.HashSet.size_erase_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.size_le_size_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.contains_eq_isSome_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
theorem
Std.HashSet.get?_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.HashSet.get!_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[Inhabited α]
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.get_eq_get!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{h' : a ∈ m}
:
@[simp]
theorem
Std.HashSet.getD_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a fallback : α}
{c : Nat}
:
@[simp]
theorem
Std.HashSet.getD_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.getD_eq_fallback_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.getD_eq_fallback
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
@[simp]
theorem
Std.HashSet.getD_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
theorem
Std.HashSet.getD_eq_getD_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.HashSet.get_eq_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
{h' : a ∈ m}
:
@[simp]
theorem
Std.HashSet.containsThenInsert_fst
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
{k : α}
:
@[simp]
theorem
Std.HashSet.containsThenInsert_snd
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
{k : α}
:
@[simp]
theorem
Std.HashSet.length_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.HashSet.isEmpty_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.HashSet.contains_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.HashSet.distinct_toList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
@[simp]
theorem
Std.HashSet.insertMany_list_singleton
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
{k : α}
:
@[simp]
theorem
Std.HashSet.contains_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
@[simp]
theorem
Std.HashSet.mem_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
theorem
Std.HashSet.mem_of_mem_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
k ∈ m.insertMany l → k ∈ m
theorem
Std.HashSet.get?_insertMany_list_of_not_mem_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(not_mem : ¬k ∈ m)
(contains_eq_false : l.contains k = false)
:
theorem
Std.HashSet.get?_insertMany_list_of_not_mem_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k k' : α}
(k_beq : (k == k') = true)
(not_mem : ¬k ∈ m)
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
(mem : k ∈ l)
:
theorem
Std.HashSet.get?_insertMany_list_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(mem : k ∈ m)
:
theorem
Std.HashSet.get_insertMany_list_of_not_mem_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k k' : α}
(k_beq : (k == k') = true)
(not_mem : ¬k ∈ m)
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
(mem : k ∈ l)
{h : k' ∈ m.insertMany l}
:
theorem
Std.HashSet.get_insertMany_list_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(mem : k ∈ m)
{h : k ∈ m.insertMany l}
:
theorem
Std.HashSet.get!_insertMany_list_of_not_mem_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List α}
{k k' : α}
(k_beq : (k == k') = true)
(not_mem : ¬k ∈ m)
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
(mem : k ∈ l)
:
theorem
Std.HashSet.getD_insertMany_list_of_not_mem_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k fallback : α}
(not_mem : ¬k ∈ m)
(contains_eq_false : l.contains k = false)
:
theorem
Std.HashSet.getD_insertMany_list_of_not_mem_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k k' fallback : α}
(k_beq : (k == k') = true)
(not_mem : ¬k ∈ m)
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
(mem : k ∈ l)
:
theorem
Std.HashSet.getD_insertMany_list_of_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k fallback : α}
(mem : k ∈ m)
:
theorem
Std.HashSet.size_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
:
theorem
Std.HashSet.size_le_size_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
theorem
Std.HashSet.size_insertMany_list_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
@[simp]
theorem
Std.HashSet.isEmpty_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : HashSet α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
theorem
Std.HashSet.ofList_cons
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{hd : α}
{tl : List α}
:
@[simp]
theorem
Std.HashSet.contains_ofList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
theorem
Std.HashSet.get?_ofList_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
theorem
Std.HashSet.get!_ofList_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
theorem
Std.HashSet.getD_ofList_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k fallback : α}
(contains_eq_false : l.contains k = false)
:
theorem
Std.HashSet.size_ofList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
:
theorem
Std.HashSet.size_ofList_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
@[simp]
theorem
Std.HashSet.isEmpty_ofList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
: