Documentation

Std.Data.HashSet.RawLemmas

Hash set lemmas #

This module contains lemmas about Std.Data.HashSet.Raw. 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.Raw.isEmpty_empty {α : Type u} [BEq α] [Hashable α] {c : Nat} :
@[simp]
theorem Std.HashSet.Raw.isEmpty_emptyc {α : Type u} [BEq α] [Hashable α] :
.isEmpty = true
@[simp]
theorem Std.HashSet.Raw.isEmpty_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
(m.insert a).isEmpty = false
theorem Std.HashSet.Raw.mem_iff_contains {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} {a : α} :
a m m.contains a = true
theorem Std.HashSet.Raw.contains_congr {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
m.contains a = m.contains b
theorem Std.HashSet.Raw.mem_congr {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
a m b m
@[simp]
theorem Std.HashSet.Raw.contains_empty {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :
@[simp]
theorem Std.HashSet.Raw.not_mem_empty {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :
@[simp]
theorem Std.HashSet.Raw.contains_emptyc {α : Type u} [BEq α] [Hashable α] {a : α} :
.contains a = false
@[simp]
theorem Std.HashSet.Raw.not_mem_emptyc {α : Type u} [BEq α] [Hashable α] {a : α} :
theorem Std.HashSet.Raw.contains_of_isEmpty {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = truem.contains a = false
theorem Std.HashSet.Raw.not_mem_of_isEmpty {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true¬a m
theorem Std.HashSet.Raw.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ∃ (a : α), m.contains a = true
theorem Std.HashSet.Raw.isEmpty_eq_false_iff_exists_mem {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ∃ (a : α), a m
theorem Std.HashSet.Raw.isEmpty_iff_forall_contains {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ∀ (a : α), m.contains a = false
theorem Std.HashSet.Raw.isEmpty_iff_forall_not_mem {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ∀ (a : α), ¬a m
@[simp]
theorem Std.HashSet.Raw.contains_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.insert k).contains a = (k == a || m.contains a)
@[simp]
theorem Std.HashSet.Raw.mem_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
a m.insert k (k == a) = true a m
theorem Std.HashSet.Raw.contains_of_contains_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.insert k).contains a = true(k == a) = falsem.contains a = true
theorem Std.HashSet.Raw.mem_of_mem_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
a m.insert k(k == a) = falsea m
@[simp]
theorem Std.HashSet.Raw.contains_insert_self {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.insert k).contains k = true
@[simp]
theorem Std.HashSet.Raw.mem_insert_self {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
k m.insert k
@[simp]
theorem Std.HashSet.Raw.size_empty {α : Type u} {c : Nat} :
@[simp]
theorem Std.HashSet.Raw.size_emptyc {α : Type u} :
.size = 0
theorem Std.HashSet.Raw.isEmpty_eq_size_eq_zero {α : Type u} {m : Std.HashSet.Raw α} :
m.isEmpty = (m.size == 0)
theorem Std.HashSet.Raw.size_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.insert k).size = if k m then m.size else m.size + 1
theorem Std.HashSet.Raw.size_le_size_insert {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
m.size (m.insert k).size
theorem Std.HashSet.Raw.size_insert_le {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.insert k).size m.size + 1
@[simp]
theorem Std.HashSet.Raw.erase_empty {α : Type u} [BEq α] [Hashable α] {k : α} {c : Nat} :
@[simp]
theorem Std.HashSet.Raw.erase_emptyc {α : Type u} [BEq α] [Hashable α] {k : α} :
.erase k =
@[simp]
theorem Std.HashSet.Raw.isEmpty_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
@[simp]
theorem Std.HashSet.Raw.contains_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.erase k).contains a = (!k == a && m.contains a)
@[simp]
theorem Std.HashSet.Raw.mem_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
a m.erase k (k == a) = false a m
theorem Std.HashSet.Raw.contains_of_contains_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.erase k).contains a = truem.contains a = true
theorem Std.HashSet.Raw.mem_of_mem_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
a m.erase ka m
theorem Std.HashSet.Raw.size_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size = if k m then m.size - 1 else m.size
theorem Std.HashSet.Raw.size_erase_le {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size m.size
theorem Std.HashSet.Raw.size_le_size_erase {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
m.size (m.erase k).size + 1
@[simp]
theorem Std.HashSet.Raw.containsThenInsert_fst {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) {k : α} :
(m.containsThenInsert k).fst = m.contains k
@[simp]
theorem Std.HashSet.Raw.containsThenInsert_snd {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet.Raw α} (h : m.WF) {k : α} :
(m.containsThenInsert k).snd = m.insert k