max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add HashMap/TreeMap.isSome_X simp lemmas (#8143)

Browse source 
These lemmas were previously only stated the other way round, but in
this direction they are both good simp lemmas, and good grind lemmas.
This commit is contained in:
Kim Morrison 2025-04-28 23:48:06 +10:00 • committed by GitHub
parent bca36b2eba
commit d10d17ce03
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
16 changed files with 423 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

99
src/Std/Data/DHashMap/Lemmas.lean
View file

@ -49,12 +49,18 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
Iff.rfl
-- While setting up the API, often use this in the reverse direction,
-- but prefer this direction for users.
@[simp]
theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
Iff.rfl
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
Raw₀.contains_congr _ m.2 hab
theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := by
simp [mem_iff_contains, contains_congr hab]
simp [← contains_iff_mem, contains_congr hab]
@[simp]
theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).contains a = false :=
@ -83,7 +89,7 @@ theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty → ¬a ∈ m := by
simpa [mem_iff_contains] using contains_of_isEmpty
simpa [← contains_iff_mem] using contains_of_isEmpty
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ↔ ∃ a, m.contains a = true :=
@ -91,7 +97,7 @@ theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashab
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ↔ ∃ a, a ∈ m := by
simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true
simpa [← contains_iff_mem] using isEmpty_eq_false_iff_exists_contains_eq_true
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ↔ ∀ a, m.contains a = false :=
@ -99,7 +105,7 @@ theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
simpa [mem_iff_contains] using isEmpty_iff_forall_contains
simpa [← contains_iff_mem] using isEmpty_iff_forall_contains
@[simp] theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p m = m.insert p.1 p.2 := rfl
@ -115,7 +121,7 @@ theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k}
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
simp [mem_iff_contains, contains_insert]
simp [← contains_iff_mem, contains_insert]
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a → (k == a) = false → m.contains a :=
@ -123,7 +129,7 @@ theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α}
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a ∈ m.insert k v → (k == a) = false → a ∈ m := by
simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert
simpa [← contains_iff_mem, -contains_insert] using contains_of_contains_insert
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).contains k := by simp
@ -182,7 +188,7 @@ theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
simp [mem_iff_contains, contains_erase]
simp [← contains_iff_mem, contains_erase]
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a → m.contains a :=
@ -246,15 +252,23 @@ theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get
theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome :=
Raw₀.contains_eq_isSome_get? ⟨m.1, _⟩ m.2
@[simp]
theorem isSome_get?_eq_contains [LawfulBEq α] {a : α} : (m.get? a).isSome = m.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isSome :=
Bool.eq_iff_iff.mp contains_eq_isSome_get?
@[simp]
theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} :
m.contains a = false → m.get? a = none :=
Raw₀.get?_eq_none ⟨m.1, _⟩ m.2
theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := by
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = if k == a then none else m.get? a :=
@ -297,15 +311,24 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (get? m a).isSome :=
Raw₀.Const.contains_eq_isSome_get? ⟨m.1, _⟩ m.2
@[simp]
theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(get? m a).isSome = m.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ (get? m a).isSome :=
Bool.eq_iff_iff.mp contains_eq_isSome_get?
@[simp]
theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (get? m a).isSome ↔ a ∈ m :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → get? m a = none :=
Raw₀.Const.get?_eq_none ⟨m.1, _⟩ m.2
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → get? m a = none := by
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = if k == a then none else get? m a :=
@ -426,7 +449,7 @@ theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] {a : α} [Inhabited
theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
¬a ∈ m → m.get! a = default := by
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false
theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = if k == a then default else m.get! a :=
@ -443,7 +466,7 @@ theorem get?_eq_some_get!_of_contains [LawfulBEq α] {a : α} [Inhabited (β a)]
theorem get?_eq_some_get! [LawfulBEq α] {a : α} [Inhabited (β a)] :
a ∈ m → m.get? a = some (m.get! a) := by
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains
simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains
theorem get!_eq_get!_get? [LawfulBEq α] {a : α} [Inhabited (β a)] :
m.get! a = (m.get? a).get! :=
@ -489,7 +512,7 @@ theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
¬a ∈ m → get! m a = default := by
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = if k == a then default else get! m a :=
@ -506,7 +529,7 @@ theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabit
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
a ∈ m → get? m a = some (get! m a) := by
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains
simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
get! m a = (get? m a).get! :=
@ -560,7 +583,7 @@ theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] {a : α} {fallback
theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
¬a ∈ m → m.getD a fallback = fallback := by
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false
theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
@ -577,7 +600,7 @@ theorem get?_eq_some_getD_of_contains [LawfulBEq α] {a : α} {fallback : β a}
theorem get?_eq_some_getD [LawfulBEq α] {a : α} {fallback : β a} :
a ∈ m → m.get? a = some (m.getD a fallback) := by
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains
simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains
theorem getD_eq_getD_get? [LawfulBEq α] {a : α} {fallback : β a} :
m.getD a fallback = (m.get? a).getD fallback :=
@ -628,7 +651,7 @@ theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
¬a ∈ m → getD m a fallback = fallback := by
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback :=
@ -645,7 +668,7 @@ theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] {a : α}
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
a ∈ m → get? m a = some (getD m a fallback) := by
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains
simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
getD m a fallback = (get? m a).getD fallback :=
@ -698,10 +721,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome :=
Raw₀.contains_eq_isSome_getKey? ⟨m.1, _⟩ m.2
@[simp]
theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome = m.contains a :=
contains_eq_isSome_getKey?.symm
theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.getKey? a).isSome :=
Bool.eq_iff_iff.mp contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome ↔ a ∈ m :=
mem_iff_isSome_getKey?.symm
theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
(h : m.getKey? k = some k') : k' ∈ m :=
Raw₀.contains_of_getKey?_eq_some ⟨m.1, _⟩ m.2 h
@ -711,7 +744,7 @@ theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {
Raw₀.getKey?_eq_none ⟨m.1, _⟩ m.2
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.getKey? a = none := by
simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false
simpa [← contains_iff_mem] using getKey?_eq_none_of_contains_eq_false
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a :=
@ -812,7 +845,7 @@ theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
¬a ∈ m → m.getKey! a = default := by
simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false
simpa [← contains_iff_mem] using getKey!_eq_default_of_contains_eq_false
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a :=
@ -829,7 +862,7 @@ theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [I
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a ∈ m → m.getKey? a = some (m.getKey! a) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains
simpa [← contains_iff_mem] using getKey?_eq_some_getKey!_of_contains
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = (m.getKey? a).get! :=
@ -885,7 +918,7 @@ theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
¬a ∈ m → m.getKeyD a fallback = fallback := by
simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false
simpa [← contains_iff_mem] using getKeyD_eq_fallback_of_contains_eq_false
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
@ -902,7 +935,7 @@ theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] {a
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] {a fallback : α} :
a ∈ m → m.getKey? a = some (m.getKeyD a fallback) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains
simpa [← contains_iff_mem] using getKey?_eq_some_getKeyD_of_contains
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback :=
@ -941,7 +974,7 @@ theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v :
@[simp]
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
simp [mem_iff_contains, contains_insertIfNew]
simp [← contains_iff_mem, contains_insertIfNew]
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).contains k :=
@ -949,7 +982,7 @@ theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
k ∈ m.insertIfNew k v := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self
simpa [← contains_iff_mem, -contains_insertIfNew] using contains_insertIfNew_self
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
@ -957,7 +990,7 @@ theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew
simpa [← contains_iff_mem, -contains_insertIfNew] using contains_of_contains_insertIfNew
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`. -/
@ -969,7 +1002,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a
in the statement of `get_insertIfNew`. -/
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'
simpa [← contains_iff_mem, -contains_insertIfNew] using contains_of_contains_insertIfNew'
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
@ -1037,24 +1070,24 @@ end Const
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a := by
simp [mem_iff_contains, contains_insertIfNew]
simp [← contains_iff_mem, contains_insertIfNew]
exact Raw₀.getKey?_insertIfNew ⟨m.1, _⟩ m.2
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
getKey (m.insertIfNew k v) a h₁ =
if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂) := by
simp [mem_iff_contains, contains_insertIfNew]
simp [← contains_iff_mem, contains_insertIfNew]
exact Raw₀.getKey_insertIfNew ⟨m.1, _⟩ m.2
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a := by
simp [mem_iff_contains, contains_insertIfNew]
simp [← contains_iff_mem, contains_insertIfNew]
exact Raw₀.getKey!_insertIfNew ⟨m.1, _⟩ m.2
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
getKeyD (m.insertIfNew k v) a fallback =
if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback := by
simp [mem_iff_contains, contains_insertIfNew]
simp [← contains_iff_mem, contains_insertIfNew]
exact Raw₀.getKeyD_insertIfNew ⟨m.1, _⟩ m.2
@[simp]
@ -1380,7 +1413,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
{l : List ((a : α) × β a)} {k : α} :
k ∈ m.insertMany l ↔ k ∈ m ∨ (l.map Sigma.fst).contains k := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
{l : List ((a : α) × β a)} {k : α} (mem : k ∈ m.insertMany l)
@ -1574,7 +1607,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
{l : List (α × β)} {k : α} :
k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
{l : List (α × β)} {k : α} (mem : k ∈ insertMany m l)
@ -1764,7 +1797,7 @@ theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
theorem mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} :
k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :

109
src/Std/Data/DHashMap/RawLemmas.lean
View file

@ -102,13 +102,17 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v
theorem mem_iff_contains {m : Raw α β} {a : α} :
a ∈ m ↔ m.contains a := Iff.rfl
@[simp]
theorem contains_iff_mem {m : Raw α β} {a : α} :
m.contains a ↔ a ∈ m := Iff.rfl
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
m.contains a = m.contains b := by
simp_to_raw using Raw₀.contains_congr
theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
a ∈ m ↔ b ∈ m := by
simp [mem_iff_contains, contains_congr h hab]
simp [← contains_iff_mem, contains_congr h hab]
@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false := by
simp_to_raw using Raw₀.contains_emptyWithCapacity
@ -136,7 +140,7 @@ theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.isEmpty → ¬a ∈ m := by
simpa [mem_iff_contains] using contains_of_isEmpty h
simpa [← contains_iff_mem] using contains_of_isEmpty h
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.isEmpty = false ↔ ∃ a, m.contains a = true := by
@ -144,7 +148,7 @@ theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashab
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.isEmpty = false ↔ ∃ a, a ∈ m := by
simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h
simpa [← contains_iff_mem] using isEmpty_eq_false_iff_exists_contains_eq_true h
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.isEmpty = true ↔ ∀ a, m.contains a = false := by
@ -152,7 +156,7 @@ theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
simpa [mem_iff_contains] using isEmpty_iff_forall_contains h
simpa [← contains_iff_mem] using isEmpty_iff_forall_contains h
@[simp] theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p m = m.insert p.1 p.2 := rfl
@ -168,7 +172,7 @@ theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α}
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
simp [mem_iff_contains, contains_insert h]
simp [← contains_iff_mem, contains_insert h]
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
(m.insert k v).contains a → (k == a) = false → m.contains a := by
@ -176,7 +180,7 @@ theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF)
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
a ∈ m.insert k v → (k == a) = false → a ∈ m := by
simpa [mem_iff_contains] using contains_of_contains_insert h
simpa [← contains_iff_mem] using contains_of_contains_insert h
@[simp]
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
@ -227,7 +231,7 @@ theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
simp [mem_iff_contains, contains_erase h]
simp [← contains_iff_mem, contains_erase h]
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).contains a → m.contains a := by
@ -235,7 +239,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF)
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
a ∈ m.erase k → a ∈ m := by
simpa [mem_iff_contains] using contains_of_contains_erase h
simpa [← contains_iff_mem] using contains_of_contains_erase h
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.erase k).size = if k ∈ m then m.size - 1 else m.size := by
@ -298,17 +302,26 @@ theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
m.contains a = (m.get? a).isSome := by
simp_to_raw using Raw₀.contains_eq_isSome_get?
@[simp]
theorem isSome_get?_eq_contains [LawfulBEq α] (h : m.WF) {a : α} :
(m.get? a).isSome = m.contains a :=
(contains_eq_isSome_get? h).symm
theorem mem_iff_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
a ∈ m ↔ (m.get? a).isSome := by
simp only [mem_iff_contains, Bool.coe_iff_coe]
simp_to_raw using Raw₀.contains_eq_isSome_get?
@[simp]
theorem isSome_get?_iff_mem [LawfulBEq α] (h : m.WF) {a : α} : (m.get? a).isSome ↔ a ∈ m :=
(mem_iff_isSome_get? h).symm
theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} :
m.contains a = false → m.get? a = none := by
simp_to_raw using Raw₀.get?_eq_none
theorem get?_eq_none [LawfulBEq α] (h : m.WF) {a : α} : ¬a ∈ m → m.get? a = none := by
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false h
theorem get?_erase [LawfulBEq α] (h : m.WF) {k a : α} :
(m.erase k).get? a = if k == a then none else m.get? a := by
@ -351,18 +364,28 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
m.contains a = (get? m a).isSome := by
simp_to_raw using Raw₀.Const.contains_eq_isSome_get?
@[simp]
theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(get? m a).isSome = m.contains a :=
(contains_eq_isSome_get? h).symm
theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
a ∈ m ↔ (get? m a).isSome := by
simp only [mem_iff_contains, Bool.coe_iff_coe]
simp_to_raw using Raw₀.Const.contains_eq_isSome_get?
@[simp]
theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(get? m a).isSome ↔ a ∈ m :=
(mem_iff_isSome_get? h).symm
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false → get? m a = none := by
simp_to_raw using Raw₀.Const.get?_eq_none
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
¬a ∈ m → get? m a = none := by
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false h
theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
Const.get? (m.erase k) a = if k == a then none else get? m a := by
@ -484,7 +507,7 @@ theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α}
theorem get!_eq_default [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
¬a ∈ m → m.get! a = default := by
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false h
theorem get!_erase [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = if k == a then default else m.get! a := by
@ -501,7 +524,7 @@ theorem get?_eq_some_get!_of_contains [LawfulBEq α] (h : m.WF) {a : α} [Inhabi
theorem get?_eq_some_get! [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
a ∈ m → m.get? a = some (m.get! a) := by
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains h
theorem get!_eq_get!_get? [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
m.get! a = (m.get? a).get! := by
@ -547,7 +570,7 @@ theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
¬a ∈ m → get! m a = default := by
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false h
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} :
get! (m.erase k) a = if k == a then default else get! m a := by
@ -564,7 +587,7 @@ theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabit
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
a ∈ m → get? m a = some (get! m a) := by
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains h
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
get! m a = (get? m a).get! := by
@ -618,7 +641,7 @@ theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α}
theorem getD_eq_fallback [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
¬a ∈ m → m.getD a fallback = fallback := by
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false h
theorem getD_erase [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
@ -635,7 +658,7 @@ theorem get?_eq_some_getD_of_contains [LawfulBEq α] (h : m.WF) {a : α} {fallba
theorem get?_eq_some_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
a ∈ m → m.get? a = some (m.getD a fallback) := by
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains h
theorem getD_eq_getD_get? [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
m.getD a fallback = (m.get? a).getD fallback := by
@ -685,7 +708,7 @@ theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
¬a ∈ m → getD m a fallback = fallback := by
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false h
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback : β} :
getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
@ -702,7 +725,7 @@ theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.W
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
a ∈ m → get? m a = some (getD m a fallback) := by
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains h
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
getD m a fallback = (get? m a).getD fallback := by
@ -756,15 +779,25 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF)
m.contains a = (m.getKey? a).isSome := by
simp_to_raw using Raw₀.contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.getKey? a).isSome = m.contains a :=
(contains_eq_isSome_getKey? h).symm
theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
a ∈ m ↔ (m.getKey? a).isSome := by
simp only [mem_iff_contains, Bool.coe_iff_coe]
simp_to_raw using Raw₀.contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.getKey? a).isSome ↔ a ∈ m :=
(mem_iff_isSome_getKey? h).symm
theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
{a a' : α} (h : m.WF) :
m.getKey? a = some a' → a' ∈ m := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
simp_to_raw using Raw₀.contains_of_getKey?_eq_some
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
@ -773,7 +806,7 @@ theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
¬a ∈ m → m.getKey? a = none := by
simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false h
simpa [← contains_iff_mem] using getKey?_eq_none_of_contains_eq_false h
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a := by
@ -879,7 +912,7 @@ theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
¬a ∈ m → m.getKey! a = default := by
simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false h
simpa [← contains_iff_mem] using getKey!_eq_default_of_contains_eq_false h
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a := by
@ -897,7 +930,7 @@ theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [I
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
a ∈ m → m.getKey? a = some (m.getKey! a) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains h
simpa [← contains_iff_mem] using getKey?_eq_some_getKey!_of_contains h
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
m.getKey! a = (m.getKey? a).get! := by
@ -954,7 +987,7 @@ theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
¬a ∈ m → m.getKeyD a fallback = fallback := by
simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false h
simpa [← contains_iff_mem] using getKeyD_eq_fallback_of_contains_eq_false h
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback := by
@ -972,7 +1005,7 @@ theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
a ∈ m → m.getKey? a = some (m.getKeyD a fallback) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains h
simpa [← contains_iff_mem] using getKey?_eq_some_getKeyD_of_contains h
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback := by
@ -1012,7 +1045,7 @@ theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a :
@[simp]
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
simp [mem_iff_contains, contains_insertIfNew h]
simp [← contains_iff_mem, contains_insertIfNew h]
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
(m.insertIfNew k v).contains k := by
@ -1020,7 +1053,7 @@ theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
k ∈ m.insertIfNew k v := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self h
simpa [← contains_iff_mem, -contains_insertIfNew] using contains_insertIfNew_self h
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
{v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
@ -1028,7 +1061,7 @@ theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h :
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h
simpa [← contains_iff_mem, -contains_insertIfNew] using contains_of_contains_insertIfNew h
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`. -/
@ -1041,7 +1074,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h :
in the statement of `get_insertIfNew`. -/
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h
simpa [← contains_iff_mem] using contains_of_contains_insertIfNew' h
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := by
@ -1185,7 +1218,7 @@ theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
theorem mem_of_mem_keys [EquivBEq α] [LawfulHashable α] {k : α}
(h : m.WF) (h' : k ∈ m.keys) : k ∈ m := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
simp_to_raw using Raw₀.contains_of_mem_keys
theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
@ -1482,7 +1515,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
{l : List ((a : α) × β a)} {k : α} :
k ∈ (m.insertMany l) ↔ k ∈ m ∨ (l.map Sigma.fst).contains k := by
simp [mem_iff_contains, contains_insertMany_list h]
simp [← contains_iff_mem, contains_insertMany_list h]
theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
{l : List ((a : α) × β a)} {k : α} :
@ -1685,7 +1718,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
{l : List (α × β)} {k : α} :
k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k := by
simp [mem_iff_contains, contains_insertMany_list h]
simp [← contains_iff_mem, contains_insertMany_list h]
theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
{l : List (α × β)} {k : α} :
@ -1762,7 +1795,7 @@ theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
(distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
(∀ (a : α), a ∈ m → (l.map Prod.fst).contains a = false) →
(insertMany m l).size = m.size + l.length := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
simp_to_raw using Raw₀.Const.size_insertMany_list
theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
@ -1882,12 +1915,12 @@ theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h :
theorem mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
{l : List α} {k : α} :
k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k := by
simp [mem_iff_contains, contains_insertManyIfNewUnit_list h]
simp [← contains_iff_mem, contains_insertManyIfNewUnit_list h]
theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertManyIfNewUnit m l → k ∈ m := by
simp only [mem_iff_contains]
simp only [← contains_iff_mem]
simp_to_raw using Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list
theorem mem_insertManyIfNewUnit_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
@ -2470,7 +2503,7 @@ theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (
theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) :
k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m := by
simp [mem_iff_contains, contains_alter h]
simp [← contains_iff_mem, contains_alter h]
theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF)
(he : k == k') : k' ∈ m.alter k f ↔ (f (m.get? k)).isSome := by
@ -3584,7 +3617,7 @@ theorem isSome_apply_of_mem_filterMap [EquivBEq α] [LawfulHashable α]
∀ (h' : k ∈ m.filterMap f),
(f (m.getKey k (mem_of_mem_filterMap h h'))
(Const.get m k (mem_of_mem_filterMap h h'))).isSome := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
simp_to_raw using Raw₀.Const.isSome_apply_of_contains_filterMap
@[simp]
@ -3750,7 +3783,7 @@ theorem filter_equiv_self_iff [LawfulBEq α]
theorem filter_key_equiv_self_iff [EquivBEq α] [LawfulHashable α]
{f : (a : α) → Bool} (h : m.WF) :
m.filter (fun k _ => f k) ~m m ↔ ∀ k h, f (m.getKey k h) = true := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
simp_to_raw using Raw₀.filter_key_equiv_self_iff
theorem size_filter_key_eq_size_iff [EquivBEq α] [LawfulHashable α]
@ -3869,7 +3902,7 @@ theorem filter_equiv_self_iff [EquivBEq α] [LawfulHashable α]
{f : α → β → Bool} (h : m.WF) :
m.filter f ~m m ↔ ∀ (a : α) (h : a ∈ m),
f (m.getKey a h) (Const.get m a h) := by
simp [mem_iff_contains]
simp [← contains_iff_mem]
simp_to_raw using Raw₀.Const.filter_equiv_self_iff
theorem get?_filter [EquivBEq α] [LawfulHashable α]

3
src/Std/Data/DTreeMap/Internal/Queries.lean
View file

@ -42,6 +42,9 @@ instance [Ord α] : Membership α (Impl α β) where
theorem mem_iff_contains {_ : Ord α} {t : Impl α β} {k : α} : k ∈ t ↔ t.contains k :=
Iff.rfl
theorem contains_iff_mem {_ : Ord α} {t : Impl α β} {k : α} : t.contains k ↔ k ∈ t :=
Iff.rfl
instance [Ord α] {m : Impl α β} {a : α} : Decidable (a ∈ m) :=
inferInstanceAs <| Decidable (m.contains a)

34
src/Std/Data/DTreeMap/Lemmas.lean
View file

@ -41,6 +41,10 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} :
theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
Impl.mem_iff_contains
@[simp]
theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
Impl.contains_iff_mem
theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
t.contains k = t.contains k' :=
Impl.contains_congr t.wf hab
@ -231,10 +235,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
t.contains a = (t.get? a).isSome :=
Impl.contains_eq_isSome_get? t.wf
@[simp]
theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
(t.get? a).isSome = t.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
a ∈ t ↔ (t.get? a).isSome :=
Impl.mem_iff_isSome_get? t.wf
@[simp]
theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
(t.get? a).isSome ↔ a ∈ t :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
t.contains a = false → t.get? a = none :=
Impl.get?_eq_none_of_contains_eq_false t.wf
@ -279,10 +293,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
t.contains a = (get? t a).isSome :=
Impl.Const.contains_eq_isSome_get? t.wf
@[simp]
theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
(get? t a).isSome = t.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} :
a ∈ t ↔ (get? t a).isSome :=
Impl.Const.mem_iff_isSome_get? t.wf
@[simp]
theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} :
(get? t a).isSome ↔ a ∈ t :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
t.contains a = false → get? t a = none :=
Impl.Const.get?_eq_none_of_contains_eq_false t.wf
@ -631,10 +655,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] {a : α} :
t.contains a = (t.getKey? a).isSome :=
Impl.contains_eq_isSome_getKey? t.wf
@[simp]
theorem isSome_getKey?_eq_contains [TransCmp cmp] {a : α} :
(t.getKey? a).isSome = t.contains a :=
contains_eq_isSome_getKey?.symm
theorem mem_iff_isSome_getKey? [TransCmp cmp] {a : α} :
a ∈ t ↔ (t.getKey? a).isSome :=
Impl.mem_iff_isSome_getKey? t.wf
@[simp]
theorem isSome_getKey?_iff_mem [TransCmp cmp] {a : α} :
(t.getKey? a).isSome ↔ a ∈ t :=
mem_iff_isSome_getKey?.symm
theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
t.contains a = false → t.getKey? a = none :=
Impl.getKey?_eq_none_of_contains_eq_false t.wf

34
src/Std/Data/DTreeMap/Raw/Lemmas.lean
View file

@ -42,6 +42,10 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
Impl.mem_iff_contains
@[simp]
theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
Impl.contains_iff_mem
theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
t.contains k = t.contains k' :=
Impl.contains_congr h hab
@ -232,10 +236,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a :
t.contains a = (t.get? a).isSome :=
Impl.contains_eq_isSome_get? h
@[simp]
theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
(t.get? a).isSome = t.contains a :=
(contains_eq_isSome_get? h).symm
theorem mem_iff_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
a ∈ t ↔ (t.get? a).isSome :=
Impl.mem_iff_isSome_get? h
@[simp]
theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
(t.get? a).isSome ↔ a ∈ t :=
(mem_iff_isSome_get? h).symm
theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → t.get? a = none :=
Impl.get?_eq_none_of_contains_eq_false h
@ -280,10 +294,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = (get? t a).isSome :=
Impl.Const.contains_eq_isSome_get? h
@[simp]
theorem isSome_get?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
(get? t a).isSome = t.contains a :=
(contains_eq_isSome_get? h).symm
theorem mem_iff_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
a ∈ t ↔ (get? t a).isSome :=
Impl.Const.mem_iff_isSome_get? h
@[simp]
theorem isSome_get?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
(get? t a).isSome ↔ a ∈ t :=
(mem_iff_isSome_get? h).symm
theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → get? t a = none :=
Impl.Const.get?_eq_none_of_contains_eq_false h
@ -634,10 +658,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = (t.getKey? a).isSome :=
Impl.contains_eq_isSome_getKey? h
@[simp]
theorem isSome_getKey?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
(t.getKey? a).isSome = t.contains a :=
(contains_eq_isSome_getKey? h).symm
theorem mem_iff_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
a ∈ t ↔ (t.getKey? a).isSome :=
Impl.mem_iff_isSome_getKey? h
@[simp]
theorem isSome_getKey?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
(t.getKey? a).isSome ↔ a ∈ t :=
(mem_iff_isSome_getKey? h).symm
theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → t.getKey? a = none :=
Impl.getKey?_eq_none_of_contains_eq_false h

38
src/Std/Data/ExtDHashMap/Lemmas.lean
View file

@ -51,6 +51,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
Iff.rfl
@[simp]
theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
Iff.rfl
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b :=
m.inductionOn fun _ => DHashMap.contains_congr hab
@ -140,7 +144,7 @@ theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
simp [mem_iff_contains, contains_erase]
simp [← contains_iff_mem, contains_erase]
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a → m.contains a :=
@ -193,15 +197,23 @@ theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get
theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome :=
m.inductionOn fun _ => DHashMap.contains_eq_isSome_get?
@[simp]
theorem isSome_get?_eq_contains [LawfulBEq α] {a : α} : (m.get? a).isSome = m.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isSome :=
m.inductionOn fun _ => DHashMap.mem_iff_isSome_get?
@[simp]
theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} :
m.contains a = false → m.get? a = none :=
m.inductionOn fun _ => DHashMap.get?_eq_none_of_contains_eq_false
theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := by
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = if k == a then none else m.get? a :=
@ -232,15 +244,25 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (get? m a).isSome :=
m.inductionOn fun _ => DHashMap.Const.contains_eq_isSome_get?
@[simp]
theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(get? m a).isSome = m.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ (get? m a).isSome :=
m.inductionOn fun _ => DHashMap.Const.mem_iff_isSome_get?
@[simp]
theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(get? m a).isSome ↔ a ∈ m :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → get? m a = none :=
m.inductionOn fun _ => DHashMap.Const.get?_eq_none_of_contains_eq_false
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → get? m a = none := by
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = if k == a then none else get? m a :=
@ -569,10 +591,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome :=
m.inductionOn fun _ => DHashMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome = m.contains a :=
contains_eq_isSome_getKey?.symm
theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.getKey? a).isSome :=
m.inductionOn fun _ => DHashMap.mem_iff_isSome_getKey?
@[simp]
theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome ↔ a ∈ m :=
mem_iff_isSome_getKey?.symm
theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
(h : m.getKey? k = some k') : k' ∈ m :=
m.inductionOn (fun _ h => DHashMap.mem_of_getKey?_eq_some h) h

24
src/Std/Data/ExtHashMap/Lemmas.lean
View file

@ -55,6 +55,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
ExtDHashMap.mem_iff_contains
@[simp]
theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
Iff.rfl
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
ExtDHashMap.contains_congr hab
@ -204,10 +208,20 @@ theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = m[a]?.isSome :=
ExtDHashMap.Const.contains_eq_isSome_get?
@[simp]
theorem isSome_getElem?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
m[a]?.isSome = m.contains a :=
contains_eq_isSome_getElem?.symm
theorem mem_iff_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ m[a]?.isSome :=
ExtDHashMap.Const.mem_iff_isSome_get?
@[simp]
theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
m[a]?.isSome ↔ a ∈ m :=
mem_iff_isSome_getElem?.symm
theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m[a]? = none :=
ExtDHashMap.Const.get?_eq_none_of_contains_eq_false
@ -381,10 +395,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome :=
ExtDHashMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome = m.contains a :=
contains_eq_isSome_getKey?.symm
theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.getKey? a).isSome :=
ExtDHashMap.mem_iff_isSome_getKey?
@[simp]
theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome ↔ a ∈ m :=
mem_iff_isSome_getKey?.symm
theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
(h : m.getKey? k = some k') : k' ∈ m :=
ExtDHashMap.mem_of_getKey?_eq_some h

14
src/Std/Data/ExtHashSet/Lemmas.lean
View file

@ -55,6 +55,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} :
theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
ExtHashMap.mem_iff_contains
@[simp]
theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
ExtHashMap.contains_iff_mem
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
ExtHashMap.contains_congr hab
@ -184,10 +188,20 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.get? a).isSome :=
ExtHashMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(m.get? a).isSome = m.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.get? a).isSome :=
ExtHashMap.mem_iff_isSome_getKey?
@[simp]
theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(m.get? a).isSome ↔ a ∈ m :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m.get? a = none :=
ExtHashMap.getKey?_eq_none_of_contains_eq_false

24
src/Std/Data/HashMap/Lemmas.lean
View file

@ -52,6 +52,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
DHashMap.mem_iff_contains
@[simp]
theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
DHashMap.contains_iff_mem
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
DHashMap.contains_congr hab
@ -258,10 +262,20 @@ theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = m[a]?.isSome :=
DHashMap.Const.contains_eq_isSome_get?
@[simp]
theorem isSome_getElem?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
m[a]?.isSome = m.contains a :=
contains_eq_isSome_getElem?.symm
theorem mem_iff_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ m[a]?.isSome :=
DHashMap.Const.mem_iff_isSome_get?
@[simp]
theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
m[a]?.isSome ↔ a ∈ m :=
mem_iff_isSome_getElem?.symm
theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m[a]? = none :=
DHashMap.Const.get?_eq_none_of_contains_eq_false
@ -469,10 +483,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome :=
DHashMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome = m.contains a :=
contains_eq_isSome_getKey?.symm
theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.getKey? a).isSome :=
DHashMap.mem_iff_isSome_getKey?
@[simp]
theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome ↔ a ∈ m :=
mem_iff_isSome_getKey?.symm
theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
(h : m.getKey? k = some k') : k' ∈ m :=
DHashMap.mem_of_getKey?_eq_some h

24
src/Std/Data/HashMap/RawLemmas.lean
View file

@ -68,6 +68,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
DHashMap.Raw.mem_iff_contains
@[simp]
theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
DHashMap.Raw.contains_iff_mem
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
DHashMap.Raw.contains_congr h.out hab
@ -274,10 +278,20 @@ theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] (h : m.WF)
m.contains a = m[a]?.isSome :=
DHashMap.Raw.Const.contains_eq_isSome_get? h.out
@[simp]
theorem isSome_getElem?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m[a]?.isSome = m.contains a :=
(contains_eq_isSome_getElem? h).symm
theorem mem_iff_isSome_getElem? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
a ∈ m ↔ (m[a]?).isSome :=
DHashMap.Raw.Const.mem_iff_isSome_get? h.out
@[simp]
theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m[a]?).isSome ↔ a ∈ m :=
(mem_iff_isSome_getElem? h).symm
theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false → m[a]? = none :=
DHashMap.Raw.Const.get?_eq_none_of_contains_eq_false h.out
@ -487,6 +501,11 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF)
m.contains a = (m.getKey? a).isSome :=
DHashMap.Raw.contains_eq_isSome_getKey? h.out
@[simp]
theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.getKey? a).isSome = m.contains a :=
(contains_eq_isSome_getKey? h).symm
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false → m.getKey? a = none :=
DHashMap.Raw.getKey?_eq_none_of_contains_eq_false h.out
@ -533,6 +552,11 @@ theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
a ∈ m ↔ (m.getKey? a).isSome :=
DHashMap.Raw.mem_iff_isSome_getKey? h.out
@[simp]
theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.getKey? a).isSome ↔ a ∈ m :=
(mem_iff_isSome_getKey? h).symm
theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
{a a' : α} (h : m.WF) :
m.getKey? a = some a' → a' ∈ m :=

14
src/Std/Data/HashSet/Lemmas.lean
View file

@ -50,6 +50,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {a : α} : (m.insert a)
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
HashMap.mem_iff_contains
@[simp]
theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
HashMap.contains_iff_mem
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
HashMap.contains_congr hab
@ -235,10 +239,20 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.get? a).isSome :=
HashMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
(m.get? a).isSome = m.contains a :=
contains_eq_isSome_get?.symm
theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.get? a).isSome :=
HashMap.mem_iff_isSome_getKey?
@[simp]
theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
(m.get? a).isSome ↔ a ∈ m :=
mem_iff_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m.get? a = none :=
HashMap.getKey?_eq_none_of_contains_eq_false

14
src/Std/Data/HashSet/RawLemmas.lean
View file

@ -68,6 +68,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
HashMap.Raw.mem_iff_contains
@[simp]
theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
HashMap.Raw.contains_iff_mem
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
m.contains a = m.contains b :=
HashMap.Raw.contains_congr h.out hab
@ -246,10 +250,20 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
m.contains a = (m.get? a).isSome :=
HashMap.Raw.contains_eq_isSome_getKey? h.out
@[simp]
theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.get? a).isSome = m.contains a :=
(contains_eq_isSome_get? h).symm
theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
a ∈ m ↔ (m.get? a).isSome :=
HashMap.Raw.mem_iff_isSome_getKey? h.out
@[simp]
theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.get? a).isSome ↔ a ∈ m :=
(mem_iff_isSome_get? h).symm
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false → m.get? a = none :=
HashMap.Raw.getKey?_eq_none_of_contains_eq_false h.out

24
src/Std/Data/TreeMap/Lemmas.lean
View file

@ -38,6 +38,10 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} :
theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
DTreeMap.mem_iff_contains
@[simp]
theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
DTreeMap.contains_iff_mem
theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
t.contains k = t.contains k' :=
DTreeMap.contains_congr hab
@ -231,10 +235,20 @@ theorem contains_eq_isSome_getElem? [TransCmp cmp] {a : α} :
t.contains a = t[a]?.isSome :=
DTreeMap.Const.contains_eq_isSome_get?
@[simp]
theorem isSome_getElem?_eq_contains [TransCmp cmp] {a : α} :
t[a]?.isSome = t.contains a :=
contains_eq_isSome_getElem?.symm
theorem mem_iff_isSome_getElem? [TransCmp cmp] {a : α} :
a ∈ t ↔ t[a]?.isSome :=
DTreeMap.Const.mem_iff_isSome_get?
@[simp]
theorem isSome_getElem?_iff_mem [TransCmp cmp] {a : α} :
t[a]?.isSome ↔ a ∈ t :=
mem_iff_isSome_getElem?.symm
theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
t.contains a = false → t[a]? = none :=
DTreeMap.Const.get?_eq_none_of_contains_eq_false
@ -423,10 +437,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] {a : α} :
t.contains a = (t.getKey? a).isSome :=
DTreeMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_getKey?_eq_contains [TransCmp cmp] {a : α} :
(t.getKey? a).isSome = t.contains a :=
contains_eq_isSome_getKey?.symm
theorem mem_iff_isSome_getKey? [TransCmp cmp] {a : α} :
a ∈ t ↔ (t.getKey? a).isSome :=
DTreeMap.mem_iff_isSome_getKey?
@[simp]
theorem isSome_getKey?_iff_mem [TransCmp cmp] {a : α} :
(t.getKey? a).isSome ↔ a ∈ t :=
mem_iff_isSome_getKey?.symm
theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
t.contains a = false → t.getKey? a = none :=
DTreeMap.getKey?_eq_none_of_contains_eq_false

24
src/Std/Data/TreeMap/Raw/Lemmas.lean
View file

@ -39,6 +39,10 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
DTreeMap.Raw.mem_iff_contains
@[simp]
theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
DTreeMap.Raw.contains_iff_mem
theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
t.contains k = t.contains k' :=
DTreeMap.Raw.contains_congr h hab
@ -232,10 +236,20 @@ theorem contains_eq_isSome_getElem? [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = t[a]?.isSome :=
DTreeMap.Raw.Const.contains_eq_isSome_get? h
@[simp]
theorem isSome_getElem?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
t[a]?.isSome = t.contains a :=
(contains_eq_isSome_getElem? h).symm
theorem mem_iff_isSome_getElem? [TransCmp cmp] (h : t.WF) {a : α} :
a ∈ t ↔ t[a]?.isSome :=
DTreeMap.Raw.Const.mem_iff_isSome_get? h
@[simp]
theorem isSome_getElem?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
t[a]?.isSome ↔ a ∈ t :=
(mem_iff_isSome_getElem? h).symm
theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → t[a]? = none :=
DTreeMap.Raw.Const.get?_eq_none_of_contains_eq_false h
@ -424,10 +438,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = (t.getKey? a).isSome :=
DTreeMap.Raw.contains_eq_isSome_getKey? h
@[simp]
theorem isSome_getKey?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
(t.getKey? a).isSome = t.contains a :=
(contains_eq_isSome_getKey? h).symm
theorem mem_iff_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
a ∈ t ↔ (t.getKey? a).isSome :=
DTreeMap.Raw.mem_iff_isSome_getKey? h
@[simp]
theorem isSome_getKey?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
(t.getKey? a).isSome ↔ a ∈ t :=
(mem_iff_isSome_getKey? h).symm
theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → t.getKey? a = none :=
DTreeMap.Raw.getKey?_eq_none_of_contains_eq_false h

9
src/Std/Data/TreeSet/Lemmas.lean
View file

@ -38,6 +38,10 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} :
theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
TreeMap.mem_iff_contains
@[simp]
theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
TreeMap.contains_iff_mem
theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
t.contains k = t.contains k' :=
TreeMap.contains_congr hab
@ -207,6 +211,11 @@ theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
t.contains a = (t.get? a).isSome :=
TreeMap.contains_eq_isSome_getKey?
@[simp]
theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
(t.get? a).isSome = t.contains a :=
contains_eq_isSome_get?.symm
theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
t.contains a = false → t.get? a = none :=
TreeMap.getKey?_eq_none_of_contains_eq_false

9
src/Std/Data/TreeSet/Raw/Lemmas.lean
View file

@ -39,6 +39,10 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} :
theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
TreeMap.Raw.mem_iff_contains
@[simp]
theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
TreeMap.Raw.contains_iff_mem
theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
t.contains k = t.contains k' :=
TreeMap.Raw.contains_congr h hab
@ -208,6 +212,11 @@ theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = (t.get? a).isSome :=
TreeMap.Raw.contains_eq_isSome_getKey? h
@[simp]
theorem isSome_get?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
(t.get? a).isSome = t.contains a :=
(contains_eq_isSome_get? h).symm
theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → t.get? a = none :=
TreeMap.Raw.getKey?_eq_none_of_contains_eq_false h