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

feat: HashMap getKey lemmas (#7289)

Browse source 
This PR adds `getKey_beq`, `getKey_congr` and variants to the hashmap
api.
This commit is contained in:
Rob23oba 2025-03-03 16:06:58 +01:00 • committed by GitHub
parent d2239a5770
commit d3eb2fe13c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 413 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Data/BEq.lean
View file

@ -49,6 +49,14 @@ theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = fal
theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c :=
PartialEquivBEq.trans
theorem BEq.congr_left [BEq α] [PartialEquivBEq α] {a b c : α} (h : a == b) :
(a == c) = (b == c) :=
Bool.eq_iff_iff.mpr ⟨BEq.trans (BEq.symm h), BEq.trans h⟩
theorem BEq.congr_right [BEq α] [PartialEquivBEq α] {a b c : α} (h : b == c) :
(a == b) = (a == c) :=
Bool.eq_iff_iff.mpr ⟨fun h' => BEq.trans h' h, fun h' => BEq.trans h' (BEq.symm h)⟩
theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
(a == b) = false → b == c → (a == c) = false :=
fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))

44
src/Std/Data/DHashMap/Internal/RawLemmas.lean
View file

@ -354,7 +354,7 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α}
theorem get_eq_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : get m a h = m.get a h := by
simp_to_model using List.getValue_eq_getValueCast
theorem get_congr [LawfulBEq α] (h : m.1.WF) {a b : α} (hab : a == b) {h'} :
theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab : a == b) {h'} :
get m a h' = get m b ((contains_congr _ h hab).symm.trans h') := by
simp_to_model using List.getValue_congr
@ -582,6 +582,19 @@ theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α}
m.contains a = false → m.getKey? a = none := by
simp_to_model using List.getKey?_eq_none
theorem getKey?_beq [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
(m.getKey? a).all (· == a) := by
simp_to_model using List.getKey?_beq
theorem getKey?_eq_some [LawfulBEq α] (h : m.1.WF) {a : α} :
m.contains a → m.getKey? a = some a := by
simp_to_model using List.getKey?_eq_some
theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
{k k' : α} (h : k == k') :
m.getKey? k = m.getKey? k' := by
simp_to_model using List.getKey?_congr
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a := by
simp_to_model [erase] using List.getKey?_eraseKey
@ -607,6 +620,19 @@ theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {
(m.erase k).getKey a h' = m.getKey a (contains_of_contains_erase _ h h') := by
simp_to_model [erase] using List.getKey_eraseKey
theorem getKey_beq [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} (h' : m.contains a) :
m.getKey a h' == a := by
simp_to_model using List.getKey_beq
@[simp]
theorem getKey_eq [LawfulBEq α] (h : m.1.WF) {a : α} (h' : m.contains a) : m.getKey a h' = a := by
simp_to_model using List.getKey_eq
theorem getKey_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
{k k' : α} (h' : k == k') (h'' : m.contains k) :
m.getKey k h'' = m.getKey k' ((contains_congr _ h h').symm.trans h'') := by
simp_to_model using List.getKey_congr
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h'} :
m.getKey? a = some (m.getKey a h') := by
simp_to_model using List.getKey?_eq_some_getKey
@ -652,6 +678,14 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h :
m.getKey a h = m.getKey! a := by
simp_to_model using List.getKey_eq_getKey!
theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
{k k' : α} (h : k == k') : m.getKey! k = m.getKey! k' := by
simp_to_model using List.getKey!_congr
theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.1.WF) {k : α} :
m.contains k → m.getKey! k = k := by
simp_to_model using List.getKey!_eq_of_containsKey
theorem getKeyD_empty {a : α} {fallback : α} {c} :
(empty c : Raw₀ α β).getKeyD a fallback = fallback := by
simp [getKeyD, empty]
@ -699,6 +733,14 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
m.getKey! a = m.getKeyD a default := by
simp_to_model using List.getKey!_eq_getKeyD_default
theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
{k k' fallback : α} (h : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback := by
simp_to_model using List.getKeyD_congr
theorem getKeyD_eq_of_contains [LawfulBEq α] (h : m.1.WF) {k fallback : α} :
m.contains k → m.getKeyD k fallback = k := by
simp_to_model using List.getKeyD_eq_of_containsKey
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
(m.insertIfNew k v).1.isEmpty = false := by
simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew

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

@ -334,7 +334,7 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h} :
theorem get_eq_get [LawfulBEq α] {a : α} {h} : get m a h = m.get a h :=
Raw₀.Const.get_eq_get ⟨m.1, _⟩ m.2
theorem get_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
theorem get_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h'} :
get m a h' = get m b ((mem_congr hab).1 h') :=
Raw₀.Const.get_congr ⟨m.1, _⟩ m.2 hab
@ -641,6 +641,21 @@ theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
Raw₀.getKey?_erase_self ⟨m.1, _⟩ m.2
theorem getKey?_beq [EquivBEq α] [LawfulHashable α] {k : α} :
(m.getKey? k).all (· == k) :=
Raw₀.getKey?_beq ⟨m.1, _⟩ m.2
theorem getKey?_congr [EquivBEq α] [LawfulHashable α] {k k' : α} (h : k == k') :
m.getKey? k = m.getKey? k' :=
Raw₀.getKey?_congr ⟨m.1, _⟩ m.2 h
theorem getKey?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) :
m.getKey? k = some k :=
Raw₀.getKey?_eq_some ⟨m.1, _⟩ m.2 h
theorem getKey?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey? k = some k := by
simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then
@ -664,6 +679,16 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α}
m.getKey? a = some (m.getKey a h) :=
Raw₀.getKey?_eq_some_getKey ⟨m.1, _⟩ m.2
theorem getKey_beq [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : m.getKey k h == k :=
Raw₀.getKey_beq ⟨m.1, _⟩ m.2 h
theorem getKey_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ == k₂)
(h₁ : k₁ ∈ m) : m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h).mp h₁) :=
Raw₀.getKey_congr ⟨m.1, _⟩ m.2 h h₁
theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
Raw₀.getKey_eq ⟨m.1, _⟩ m.2 h
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} :
(empty c : DHashMap α β).getKey! a = default :=
@ -722,6 +747,17 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a :
m.getKey a h = m.getKey! a :=
Raw₀.getKey_eq_getKey! ⟨m.1, _⟩ m.2
theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : k == k') :
m.getKey! k = m.getKey! k' :=
Raw₀.getKey!_congr ⟨m.1, _⟩ m.2 h
theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k) :
m.getKey! k = k :=
Raw₀.getKey!_eq_of_contains ⟨m.1, _⟩ m.2 h
theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.getKey! k = k :=
getKey!_eq_of_contains h
@[simp]
theorem getKeyD_empty {a fallback : α} {c} :
(empty c : DHashMap α β).getKeyD a fallback = fallback :=
@ -784,6 +820,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
m.getKey! a = m.getKeyD a default :=
Raw₀.getKey!_eq_getKeyD_default ⟨m.1, _⟩ m.2
theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
(h : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback :=
Raw₀.getKeyD_congr ⟨m.1, _⟩ m.2 h
theorem getKeyD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k) :
m.getKeyD k fallback = k :=
Raw₀.getKeyD_eq_of_contains ⟨m.1, _⟩ m.2 h
theorem getKeyD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) :
m.getKeyD k fallback = k :=
getKeyD_eq_of_contains h
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).isEmpty = false :=

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

@ -411,7 +411,7 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {
theorem get_eq_get [LawfulBEq α] (h : m.WF) {a : α} {h} : get m a h = m.get a h := by
simp_to_raw using Raw₀.Const.get_eq_get
theorem get_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
get m a h' = get m b ((mem_congr h hab).1 h') := by
simp_to_raw using Raw₀.Const.get_congr
@ -719,6 +719,22 @@ theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
(m.erase k).getKey? k = none := by
simp_to_raw using Raw₀.getKey?_erase_self
theorem getKey?_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.getKey? a).all (· == a) := by
simp_to_raw using Raw₀.getKey?_beq
theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : k == k') :
m.getKey? k = m.getKey? k' := by
simp_to_raw using Raw₀.getKey?_congr
theorem getKey?_eq_some_of_contains [LawfulBEq α] (h : m.WF) {k : α} :
m.contains k → m.getKey? k = some k := by
simp_to_raw using Raw₀.getKey?_eq_some
theorem getKey?_eq_some [LawfulBEq α] (h : m.WF) {k : α} :
k ∈ m → m.getKey? k = some k := by
simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then
@ -741,6 +757,19 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
m.getKey? a = some (m.getKey a h) := by
simp_to_raw using Raw₀.getKey?_eq_some_getKey
theorem getKey_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} (h') :
m.getKey a h' == a := by
simp_to_raw using Raw₀.getKey_beq
theorem getKey_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
(h' : k₁ == k₂) (h₁ : k₁ ∈ m) :
m.getKey k₁ h₁ = m.getKey k₂ (((mem_congr h h').mp h₁)) := by
simp_to_raw using Raw₀.getKey_congr
theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h') :
m.getKey k h' = k := by
simp_to_raw using Raw₀.getKey_eq
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} :
(empty c : Raw α β).getKey! a = default := by
@ -800,6 +829,18 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h :
m.getKey a h = m.getKey! a := by
simp_to_raw using Raw₀.getKey_eq_getKey!
theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
{k₁ k₂ : α} (h' : k₁ == k₂) : m.getKey! k₁ = m.getKey! k₂ := by
simp_to_raw using Raw₀.getKey!_congr
theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} :
m.contains k → m.getKey! k = k := by
simp_to_raw using Raw₀.getKey!_eq_of_contains
theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} :
k ∈ m → m.getKey! k = k := by
simpa only [mem_iff_contains] using getKey!_eq_of_contains h
@[simp]
theorem getKeyD_empty {a fallback : α} {c} :
(empty c : Raw α β).getKeyD a fallback = fallback := by
@ -864,6 +905,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
m.getKey! a = m.getKeyD a default := by
simp_to_raw using Raw₀.getKey!_eq_getKeyD_default
theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ fallback : α}
(h' : k₁ == k₂) : m.getKeyD k₁ fallback = m.getKeyD k₂ fallback := by
simp_to_raw using Raw₀.getKeyD_congr
theorem getKeyD_eq_of_contains [LawfulBEq α] (h : m.WF) {k fallback : α} :
m.contains k → m.getKeyD k fallback = k := by
simp_to_raw using Raw₀.getKeyD_eq_of_contains
theorem getKeyD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} :
k ∈ m → m.getKeyD k fallback = k := by
simpa only [mem_iff_contains] using getKeyD_eq_of_contains h
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
(m.insertIfNew k v).isEmpty = false := by

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

@ -269,7 +269,7 @@ theorem getElem?_eq_some_getElem [EquivBEq α] [LawfulHashable α] {a : α} {h'
m[a]? = some (m[a]'h') :=
@DHashMap.Const.get?_eq_some_get _ _ _ _ _ _ _ _ h'
theorem getElem_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
theorem getElem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h'} :
m[a]'h' = m[b]'((mem_congr hab).1 h') :=
DHashMap.Const.get_congr hab (h' := h')
@ -434,6 +434,20 @@ theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
DHashMap.getKey?_erase_self
theorem getKey?_beq [EquivBEq α] [LawfulHashable α] {k : α} : (m.getKey? k).all (· == k) :=
DHashMap.getKey?_beq
theorem getKey?_congr [EquivBEq α] [LawfulHashable α] {k k' : α} (h : k == k') :
m.getKey? k = m.getKey? k' :=
DHashMap.getKey?_congr h
theorem getKey?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) :
m.getKey? k = some k :=
DHashMap.getKey?_eq_some h
theorem getKey?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey? k = some k := by
simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
(m.insert k v)[a]'h₁ =
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
@ -453,6 +467,16 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α} {h' :
m.getKey? a = some (m.getKey a h') :=
@DHashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
theorem getKey_beq [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : m.getKey k h == k :=
DHashMap.getKey_beq h
theorem getKey_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ == k₂)
(h₁ : k₁ ∈ m) : m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h).mp h₁) :=
DHashMap.getKey_congr h h₁
theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
DHashMap.getKey_eq h
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : HashMap α β).getKey! a = default :=
DHashMap.getKey!_empty
@ -507,6 +531,17 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a :
m.getKey a h' = m.getKey! a :=
@DHashMap.getKey_eq_getKey! _ _ _ _ _ _ _ _ _ h'
theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : k == k') :
m.getKey! k = m.getKey! k' :=
DHashMap.getKey!_congr h
theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k) :
m.getKey! k = k :=
DHashMap.getKey!_eq_of_contains h
theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.getKey! k = k :=
DHashMap.getKey!_eq_of_mem h
@[simp]
theorem getKeyD_empty {a : α} {fallback : α} {c} :
(empty c : HashMap α β).getKeyD a fallback = fallback :=
@ -566,6 +601,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
m.getKey! a = m.getKeyD a default :=
DHashMap.getKey!_eq_getKeyD_default
theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
(h : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback :=
DHashMap.getKeyD_congr h
theorem getKeyD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k) :
m.getKeyD k fallback = k :=
DHashMap.getKeyD_eq_of_contains h
theorem getKeyD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) :
m.getKeyD k fallback = k :=
DHashMap.getKeyD_eq_of_mem h
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).isEmpty = false :=

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

@ -282,7 +282,7 @@ theorem getElem?_eq_some_getElem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
m[a]? = some (m[a]'h') :=
@DHashMap.Raw.Const.get?_eq_some_get _ _ _ _ _ _ _ h.out _ h'
theorem getElem_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
theorem getElem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
m[a]'h' = m[b]'((mem_congr h hab).1 h') :=
DHashMap.Raw.Const.get_congr h.out hab (h' := h')
@ -448,6 +448,21 @@ theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
(m.erase k).getKey? k = none :=
DHashMap.Raw.getKey?_erase_self h.out
theorem getKey?_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.getKey? k).all (· == k) :=
DHashMap.Raw.getKey?_beq h.out
theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : k == k') :
m.getKey? k = m.getKey? k' :=
DHashMap.Raw.getKey?_congr h.out h'
theorem getKey?_eq_some_of_contains [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
m.getKey? k = some k :=
DHashMap.Raw.getKey?_eq_some_of_contains h.out h'
theorem getKey?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) : m.getKey? k = some k :=
DHashMap.Raw.getKey?_eq_some h.out h'
theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then k else m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
@ -467,6 +482,19 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
m.getKey? a = some (m.getKey a h') :=
@DHashMap.Raw.getKey?_eq_some_getKey _ _ _ _ _ _ _ h.out _ h'
theorem getKey_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.getKey k h' == k :=
DHashMap.Raw.getKey_beq h.out h'
theorem getKey_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
(h' : k₁ == k₂) (h₁ : k₁ ∈ m) :
m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h h').mp h₁) :=
DHashMap.Raw.getKey_congr h.out h' h₁
theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.getKey k h' = k :=
DHashMap.Raw.getKey_eq h.out h'
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α β).getKey! a = default :=
DHashMap.Raw.getKey!_empty
@ -521,6 +549,18 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h :
m.getKey a h' = m.getKey! a :=
DHashMap.Raw.getKey_eq_getKey! h.out
theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k k' : α}
(h' : k == k') : m.getKey! k = m.getKey! k' :=
DHashMap.Raw.getKey!_congr h.out h'
theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : m.contains k) :
m.getKey! k = k :=
DHashMap.Raw.getKey!_eq_of_contains h.out h'
theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.getKey! k = k :=
DHashMap.Raw.getKey!_eq_of_mem h.out h'
@[simp]
theorem getKeyD_empty {a fallback : α} {c} :
(empty c : Raw α β).getKeyD a fallback = fallback :=
@ -581,6 +621,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
m.getKey! a = m.getKeyD a default :=
DHashMap.Raw.getKey!_eq_getKeyD_default h.out
theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' fallback : α}
(h' : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback :=
DHashMap.Raw.getKeyD_congr h.out h'
theorem getKeyD_eq_of_contains [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : m.contains k) :
m.getKeyD k fallback = k :=
DHashMap.Raw.getKeyD_eq_of_contains h.out h'
theorem getKeyD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : k ∈ m) :
m.getKeyD k fallback = k :=
DHashMap.Raw.getKeyD_eq_of_mem h.out h'
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
(m.insertIfNew k v).isEmpty = false :=

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

@ -225,6 +225,19 @@ theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).get? k = none :=
HashMap.getKey?_erase_self
theorem get?_beq [EquivBEq α] [LawfulHashable α] {k : α} : (m.get? k).all (· == k) :=
HashMap.getKey?_beq
theorem get?_congr [EquivBEq α] [LawfulHashable α] {k k' : α} (h : k == k') :
m.get? k = m.get? k' :=
HashMap.getKey?_congr h
theorem get?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) : m.get? k = some k :=
HashMap.getKey?_eq_some_of_contains h
theorem get?_eq_some_of_mem [LawfulBEq α] {k : α} (h : k ∈ m) : m.get? k = some k :=
HashMap.getKey?_eq_some_of_contains h
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
(m.insert k).get a h₁ =
if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
@ -239,6 +252,16 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈
m.get? a = some (m.get a h') :=
@HashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
theorem get_beq [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : m.get k h == k :=
HashMap.getKey_beq h
theorem get_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ == k₂)
(h₁ : k₁ ∈ m) : m.get k₁ h₁ = m.get k₂ ((mem_congr h).mp h₁) :=
HashMap.getKey_congr h h₁
theorem get_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k :=
HashMap.getKey_eq h
@[simp]
theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : HashSet α).get! a = default :=
HashMap.getKey!_empty
@ -288,6 +311,16 @@ theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h
m.get a h' = m.get! a :=
HashMap.getKey_eq_getKey!
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : k == k') :
m.get! k = m.get! k' :=
HashMap.getKey!_congr h
theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k) : m.get! k = k :=
HashMap.getKey!_eq_of_contains h
theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.get! k = k :=
HashMap.getKey!_eq_of_mem h
@[simp]
theorem getD_empty {a fallback : α} {c} : (empty c : HashSet α).getD a fallback = fallback :=
HashMap.getKeyD_empty
@ -342,6 +375,17 @@ theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a
m.get! a = m.getD a default :=
HashMap.getKey!_eq_getKeyD_default
theorem getD_congr [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
(h : k == k') : m.getD k fallback = m.getD k' fallback :=
HashMap.getKeyD_congr h
theorem getD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k) :
m.getD k fallback = k :=
HashMap.getKeyD_eq_of_contains h
theorem getD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) : m.getD k fallback = k :=
HashMap.getKeyD_eq_of_mem h
@[simp]
theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
HashMap.containsThenInsertIfNew_fst

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

@ -234,6 +234,22 @@ theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).get? a = if k == a then none else m.get? a :=
HashMap.Raw.getKey?_erase h.out
theorem get?_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.get? k).all (· == k) :=
HashMap.Raw.getKey?_beq h.out
theorem get?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : k == k') :
m.get? k = m.get? k' :=
HashMap.Raw.getKey?_congr h.out h'
theorem get?_eq_some_of_contains [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
m.get? k = some k :=
HashMap.Raw.getKey?_eq_some_of_contains h.out h'
theorem get?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.get? k = some k :=
HashMap.Raw.getKey?_eq_some h.out h'
theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁} :
(m.insert k).get a h₁ =
if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h h₁ h₂) :=
@ -253,6 +269,19 @@ theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.erase k).get? k = none :=
HashMap.Raw.getKey?_erase_self h.out
theorem get_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.get k h' == k :=
HashMap.Raw.getKey_beq h.out h'
theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
(h' : k₁ == k₂) (h₁ : k₁ ∈ m) :
m.get k₁ h₁ = m.get k₂ (((mem_congr h h').mp h₁)) :=
HashMap.Raw.getKey_congr h.out h' h₁
theorem get_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
m.get k h' = k :=
HashMap.Raw.getKey_eq h.out h'
@[simp]
theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α).get! a = default :=
HashMap.Raw.getKey!_empty
@ -303,6 +332,17 @@ theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
m.get a h' = m.get! a :=
HashMap.Raw.getKey_eq_getKey! h.out
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k k' : α}
(h' : k == k') : m.get! k = m.get! k' :=
HashMap.Raw.getKey!_congr h.out h'
theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : m.contains k) :
m.get! k = k :=
HashMap.Raw.getKey!_eq_of_contains h.out h'
theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k ∈ m) : m.get! k = k :=
HashMap.Raw.getKey!_eq_of_mem h.out h'
@[simp]
theorem getD_empty {a fallback : α} {c} : (empty c : Raw α).getD a fallback = fallback :=
HashMap.Raw.getKeyD_empty
@ -358,6 +398,18 @@ theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h
m.get! a = m.getD a default :=
HashMap.Raw.getKey!_eq_getKeyD_default h.out
theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' fallback : α}
(h' : k == k') : m.getD k fallback = m.getD k' fallback :=
HashMap.Raw.getKeyD_congr h.out h'
theorem getD_eq_of_contains [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : m.contains k) :
m.getD k fallback = k :=
HashMap.Raw.getKeyD_eq_of_contains h.out h'
theorem getD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : k ∈ m) :
m.getD k fallback = k :=
HashMap.Raw.getKeyD_eq_of_mem h.out h'
@[simp]
theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k :=
HashMap.Raw.containsThenInsertIfNew_fst h.out

74
src/Std/Data/Internal/List/Associative.lean
View file

@ -580,6 +580,21 @@ theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
· rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih]
· rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some']
theorem getKey?_beq [BEq α] {l : List ((a : α) × β a)} {a : α} :
(getKey? a l).all (· == a) := by
induction l using assoc_induction with
| nil => rfl
| cons k v l ih =>
rw [getKey?_cons, cond_eq_if]
split <;> assumption
theorem getKey?_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
{k k' : α} (h : k == k') : getKey? k l = getKey? k' l := by
induction l with
| nil => rfl
| cons x l ih =>
rw [getKey?_cons, getKey?_cons, BEq.congr_right h, ih]
theorem containsKey_eq_isSome_getKey? [BEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = (getKey? a l).isSome := by
simp [containsKey_eq_isSome_getEntry?, getKey?_eq_getEntry?]
@ -613,6 +628,23 @@ theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
· rfl
· exact getKey?_eq_some_getKey _
theorem getKey_beq [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
getKey a l h == a := by
simpa only [getKey?_eq_some_getKey h] using getKey?_beq (l := l) (a := a)
@[simp]
theorem getKey_eq [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
getKey a l h = a := by
simpa only [beq_iff_eq] using getKey_beq h
theorem getKey?_eq_some [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
(h : containsKey a l) : getKey? a l = some a := by
simp only [getKey?_eq_some_getKey h, getKey_eq]
theorem getKey_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
{k k' : α} (h : k == k') {h'} {h''} : getKey k l h' = getKey k' l h'' := by
simpa only [getKey?_eq_some_getKey, h', h'', Option.some.injEq] using getKey?_congr (l := l) h
/-- Internal implementation detail of the hash map -/
def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
(getKey? a l).getD fallback
@ -635,6 +667,15 @@ theorem getKey_eq_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {
getKey a l h = getKeyD a l fallback := by
rw [getKeyD_eq_getKey?, getKey, Option.get_eq_getD]
theorem getKeyD_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
{k k' fallback : α} (h : k == k') : getKeyD k l fallback = getKeyD k' l fallback := by
simp only [getKeyD_eq_getKey?, getKey?_congr h]
theorem getKeyD_eq_of_containsKey [BEq α] [LawfulBEq α]
{l : List ((a : α) × β a)} {k fallback : α} (h : containsKey k l) :
getKeyD k l fallback = k := by
simp only [← getKey_eq_getKeyD h, getKey_eq]
theorem getKey?_eq_some_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
(h : containsKey a l = true) :
getKey? a l = some (getKeyD a l fallback) := by
@ -661,6 +702,15 @@ theorem getKey_eq_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)}
(h : containsKey a l = true) : getKey a l h = getKey! a l := by
rw [getKey!_eq_getKey?, getKey, Option.get_eq_get!]
theorem getKey!_congr [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
{k k' : α} (h : k == k') : getKey! k l = getKey! k' l := by
simp only [getKey!_eq_getKey?, getKey?_congr h]
theorem getKey!_eq_of_containsKey [BEq α] [LawfulBEq α] [Inhabited α]
{l : List ((a : α) × β a)} {k : α} (h : containsKey k l) :
getKey! k l = k := by
simp only [← getKey_eq_getKey! h, getKey_eq]
theorem getKey?_eq_some_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
(h : containsKey a l = true) :
getKey? a l = some (getKey! a l) := by
@ -3260,7 +3310,7 @@ theorem getKey!_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Optio
· next heq =>
rfl
theorem getKey_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
theorem getKey_alterKey {k k' : α} {f : Option (β k) → Option (β k)}
(l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
getKey k' (alterKey k f l) hc =
if heq : k == k' then
@ -3533,7 +3583,7 @@ theorem getKey!_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β
getKey! k' l := by
simp [hl, getKey!_eq_getKey?, getKey?_alterKey, apply_ite Option.get!]
theorem getKey_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β}
theorem getKey_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β}
(l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
getKey k' (alterKey k f l) hc =
if heq : k == k' then
@ -3719,7 +3769,7 @@ theorem getKey!_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {
getKey! k (modifyKey k f l) = if containsKey k l then k else default := by
simp [getKey!_modifyKey, hl]
theorem getKey_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
theorem getKey_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k}
(l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) :
getKey k' (modifyKey k f l) h =
if k == k' then
@ -3727,13 +3777,13 @@ theorem getKey_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f :
else
haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h
getKey k' l h' := by
simp [modifyKey_eq_alterKey, getKey_alterKey, hl, ← dite_eq_ite]
simp only [modifyKey_eq_alterKey, getKey_alterKey, hl, ← dite_eq_ite]
@[simp]
theorem getKey_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
(l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
theorem getKey_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k}
(l : List ((a : α) × β a)) (_ : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
getKey k (modifyKey k f l) h = k := by
simp [getKey_modifyKey, hl]
simp only [getKey_eq]
theorem getKeyD_modifyKey [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k → β k}
(l : List ((a : α) × β a)) (hl : DistinctKeys l) :
@ -3744,7 +3794,7 @@ theorem getKeyD_modifyKey [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k
getKeyD k' l fallback := by
simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValueCast?, hl]
theorem getKeyD_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k}
theorem getKeyD_modifyKey_self [BEq α] [LawfulBEq α] {k fallback : α} {f : β k → β k}
(l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback := by
simp [getKeyD_modifyKey, hl]
@ -3884,7 +3934,7 @@ theorem getKey!_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β →
getKey! k (modifyKey k f l) = if containsKey k l then k else default := by
simp [getKey!_modifyKey, hl]
theorem getKey_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
theorem getKey_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
(hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) :
getKey k' (modifyKey k f l) h =
if k == k' then
@ -3892,11 +3942,11 @@ theorem getKey_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β
else
haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h
getKey k' l h' := by
simp [modifyKey_eq_alterKey, getKey_alterKey, hl]
simp only [modifyKey_eq_alterKey, getKey_alterKey, hl]
rfl
@[simp]
theorem getKey_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β → β}
theorem getKey_modifyKey_self [EquivBEq α] {k : α} {f : β → β}
(l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
getKey k (modifyKey k f l) h = k := by
simp [getKey_modifyKey, hl]
@ -3910,7 +3960,7 @@ theorem getKeyD_modifyKey [EquivBEq α] {k k' fallback : α} {f : β → β} (l
getKeyD k' l fallback := by
simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValue?, hl]
theorem getKeyD_modifyKey_self [EquivBEq α] [Inhabited α] {k fallback : α} {f : β → β}
theorem getKeyD_modifyKey_self [EquivBEq α] {k fallback : α} {f : β → β}
(l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback := by
simp [getKeyD_modifyKey, hl]