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

feat: lemmas for HashMap.alter and .modify (#6620)

Browse source 
This PR adds lemmas about HashMap.alter and .modify. These lemmas
describe the interaction of alter and modify with the read methods of
the HashMap. The additions affect the HashMap, the DHashMap and their
respective raw versions. Moreover, the raw versions of alter and modify
are defined.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert 2025-01-21 13:34:19 +01:00 • committed by GitHub
parent 3569797377
commit 31929c0acd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 3515 additions and 203 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1011
src/Std/Data/DHashMap/Internal/List/Associative.lean
View file

File diff suppressed because it is too large Load diff

4
src/Std/Data/DHashMap/Internal/Model.lean
View file

@ -486,7 +486,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β)
simp only [AssocList.contains_eq] at h
simp only [AssocList.modify_eq_alter, Array.set_set, AssocList.contains_eq,
containsKey_of_perm AssocList.toList_alter, ← modifyKey_eq_alterKey,
containsKey_modifyKey_self, h, ↓reduceIte]
containsKey_modifyKey, h, reduceIte]
· rfl
theorem modify_eq_modifyₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
@ -516,7 +516,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun
simp only [AssocList.contains_eq] at h
simp only [AssocList.Const.modify_eq_alter, Array.set_set, AssocList.contains_eq,
containsKey_of_perm AssocList.Const.toList_alter, ← Const.modifyKey_eq_alterKey,
Const.containsKey_modifyKey_self, h, ↓reduceIte]
Const.containsKey_modifyKey, h, reduceIte]
· rfl
theorem modify_eq_modifyₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)

16
src/Std/Data/DHashMap/Internal/Raw.lean
View file

@ -212,6 +212,14 @@ theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
congr
theorem alter_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : Option (β k) → Option (β k)} :
m.alter k f = Raw₀.alter ⟨m, h.size_buckets_pos⟩ k f := by
simp [Raw.alter, h.size_buckets_pos]
theorem modify_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : β k → β k} :
m.modify k f = Raw₀.modify ⟨m, h.size_buckets_pos⟩ k f := by
simp [Raw.modify, h.size_buckets_pos]
section
variable {β : Type v}
@ -299,6 +307,14 @@ theorem Const.getThenInsertIfNew?_fst_val [BEq α] [Hashable α] {m : Raw₀ α
(Raw₀.Const.getThenInsertIfNew? m a b).1 := by
simp [Raw.Const.getThenInsertIfNew?, m.2]
theorem Const.alter_eq [BEq α] [EquivBEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {k : α} {f : Option β → Option β} :
Raw.Const.alter m k f = Raw₀.Const.alter ⟨m, h.size_buckets_pos⟩ k f := by
simp [Raw.Const.alter, h.size_buckets_pos]
theorem Const.modify_eq [BEq α] [EquivBEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {k : α} {f : β → β} :
Raw.Const.modify m k f = Raw₀.Const.modify ⟨m, h.size_buckets_pos⟩ k f := by
simp [Raw.Const.modify, h.size_buckets_pos]
end
end Raw

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

@ -71,7 +71,9 @@ variable [BEq α] [Hashable α]
scoped macro "wf_trivial" : tactic => `(tactic|
repeat (first
| apply Raw₀.wfImp_insert | apply Raw₀.wfImp_insertIfNew | apply Raw₀.wfImp_insertMany
| apply Raw₀.Const.wfImp_insertMany| apply Raw₀.Const.wfImp_insertManyIfNewUnit
| apply Raw₀.Const.wfImp_insertMany | apply Raw₀.Const.wfImp_insertManyIfNewUnit
| apply Raw₀.wfImp_alter | apply Raw₀.wfImp_modify
| apply Raw₀.Const.wfImp_alter | apply Raw₀.Const.wfImp_modify
| apply Raw₀.wfImp_erase | apply Raw.WF.out | assumption | apply Raw₀.wfImp_empty
| apply Raw.WFImp.distinct | apply Raw.WF.empty₀))
@ -92,8 +94,9 @@ private def queryNames : Array Name :=
private def modifyNames : Array Name :=
#[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew,
``toListModel_insertMany_list, ``Const.toListModel_insertMany_list,
``Const.toListModel_insertManyIfNewUnit_list]
``toListModel_insertMany_list, ``Const.toListModel_insertMany_list,
``Const.toListModel_insertManyIfNewUnit_list, ``toListModel_alter,
``toListModel_modify, ``Const.toListModel_alter, ``Const.toListModel_modify]
private def congrNames : MacroM (Array (TSyntax `term)) := do
return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
@ -310,7 +313,7 @@ theorem get_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {h'} :
(m.erase k).get a h' = m.get a (contains_of_contains_erase _ h h') := by
simp_to_model using List.getValueCast_eraseKey
theorem get?_eq_some_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : m.get? a = some (m.get a h) := by
theorem get?_eq_some_get [LawfulBEq α] (h : m.1.WF) {a : α} {h'} : m.get? a = some (m.get a h') := by
simp_to_model using List.getValueCast?_eq_some_getValueCast
namespace Const
@ -592,8 +595,8 @@ 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 using List.getKey_eraseKey
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h} :
m.getKey? a = some (m.getKey a h) := by
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
theorem getKey!_empty {a : α} [Inhabited α] {c} :
@ -1312,12 +1315,6 @@ theorem getD_insertManyIfNewUnit_list
end Const
end Raw₀
namespace Raw₀
variable [BEq α] [Hashable α]
@[simp]
theorem insertMany_empty_list_nil :
(insertMany empty ([] : List ((a : α) × (β a)))).1 = empty := by
@ -1720,6 +1717,550 @@ theorem getD_insertManyIfNewUnit_empty_list
end Const
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] (h : m.1.WF) {k : α}
{f : Option (β k) → Option (β k)} :
(m.alter k f).1.isEmpty = ((m.erase k).1.isEmpty && (f (m.get? k)).isNone) := by
simp_to_model using List.isEmpty_alterKey_eq_isEmpty_eraseKey
@[simp]
theorem isEmpty_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).1.isEmpty = (((m.1.isEmpty || (m.1.size == 1 && m.contains k))) &&
(f (m.get? k)).isNone) := by
simp_to_model using List.isEmpty_alterKey
theorem contains_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k' := by
simp_to_model using List.containsKey_alterKey
theorem size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).1.size =
if m.contains k && (f (m.get? k)).isNone then
m.1.size - 1
else if !m.contains k && (f (m.get? k)).isSome then
m.1.size + 1
else
m.1.size := by
simp_to_model using List.length_alterKey'
theorem size_alter_eq_add_one [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)}
(h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isSome) :
(m.alter k f).1.size = m.1.size + 1 := by
simp [size_alter, h, h₁, h₂]
theorem size_alter_eq_sub_one [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)}
(h₁ : m.contains k) (h₂ : (f (m.get? k)).isNone) :
(m.alter k f).1.size = m.1.size - 1 := by
simp [size_alter, h, h₁, h₂]
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] (h : m.1.WF) {k : α}
{f : Option (β k) → Option (β k)} (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isNone) :
(m.alter k f).1.size = m.1.size := by
simp [size_alter, h, h₁, h₂]
theorem size_alter_eq_self_of_mem [LawfulBEq α] (h : m.1.WF) {k : α}
{f : Option (β k) → Option (β k)} (h₁ : m.contains k) (h₂ : (f (m.get? k)).isSome) :
(m.alter k f).1.size = m.1.size := by
simp [size_alter, h, h₁, Option.isSome_iff_ne_none.mp h₂]
theorem size_alter_le_size [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).1.size ≤ m.1.size + 1 := by
simp [size_alter, h]
split <;> try split
all_goals omega
theorem size_le_size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
m.1.size - 1 ≤ (m.alter k f).1.size := by
simp [size_alter, h]
split <;> try split
all_goals omega
theorem get?_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).get? k' =
if h : k == k' then
cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))
else
m.get? k' := by
simp_to_model using List.getValueCast?_alterKey
theorem get_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)}
(hc : (m.alter k f).contains k') :
(m.alter k f).get k' hc =
if heq : k == k' then
haveI h' : (f (m.get? k)).isSome := by rwa [contains_alter _ h, if_pos heq] at hc
cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h'
else
haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc
m.get k' h' := by
simp_to_model using List.getValueCast_alterKey
theorem get_alter_self [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)}
{hc : (m.alter k f).contains k} :
haveI h' : (f (m.get? k)).isSome := by rwa [contains_alter _ h, beq_self_eq_true] at hc
(m.alter k f).get k hc = (f (m.get? k)).get h' := by
simp_to_model using List.getValueCast_alterKey_self
theorem get!_alter [LawfulBEq α] {k k' : α} (h : m.1.WF) [Inhabited (β k')]
{f : Option (β k) → Option (β k)} :
(m.alter k f).get! k' =
if heq : k == k' then
(f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get!
else
m.get! k' := by
simp_to_model using List.getValueCast!_alterKey
theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} (h : m.1.WF)
{f : Option (β k) → Option (β k)} :
(m.alter k f).getD k' fallback =
if heq : k == k' then
f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
else
m.getD k' fallback := by
simp_to_model using List.getValueCastD_alterKey
private theorem cast_eq_id {α : Type u} : cast (rfl : α = α) = id := by rfl
theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} (h : m.1.WF)
{f : Option (β k) → Option (β k)} :
(m.alter k f).getD k fallback = (f (m.get? k)).getD fallback := by
simp only [getD_alter, h, beq_self_eq_true, reduceDIte, cast_eq_id, Option.map_id_fun, id_eq]
theorem getKey?_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).getKey? k' =
if k == k' then
if (f (m.get? k)).isSome then some k else none
else
m.getKey? k' := by
simp_to_model using List.getKey?_alterKey
theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.1.WF)
{f : Option (β k) → Option (β k)} : (m.alter k f).getKey! k' =
if k == k' then
if (f (m.get? k)).isSome then k else default
else
m.getKey! k' := by
simp_to_model using List.getKey!_alterKey
theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.1.WF)
{f : Option (β k) → Option (β k)} (hc : (m.alter k f).contains k') :
(m.alter k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc
m.getKey k' h' := by
simp_to_model using List.getKey_alterKey
theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} (h : m.1.WF)
{f : Option (β k) → Option (β k)} :
(m.alter k f).getKeyD k' fallback =
if k == k' then
if (f (m.get? k)).isSome then k else fallback
else
m.getKeyD k' fallback := by
simp_to_model using List.getKeyD_alterKey
namespace Const
variable {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α (fun _ => β))
theorem isEmpty_alter_eq_isEmpty_erase (h : m.1.WF) {k : α} {f : Option β → Option β} :
(Const.alter m k f).1.isEmpty = ((m.erase k).1.isEmpty && (f (Const.get? m k)).isNone) := by
simp_to_model using List.Const.isEmpty_alterKey_eq_isEmpty_eraseKey
@[simp]
theorem isEmpty_alter (h : m.1.WF) {k : α} {f : Option β → Option β} :
(Const.alter m k f).1.isEmpty = ((m.1.isEmpty || (m.1.size == 1 && m.contains k)) &&
(f (Const.get? m k)).isNone) := by
simp_to_model using List.Const.isEmpty_alterKey
theorem contains_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} :
(Const.alter m k f).contains k' =
if k == k' then
(f (Const.get? m k)).isSome
else
m.contains k' := by
simp_to_model using List.Const.containsKey_alterKey
theorem size_alter (h : m.1.WF) {k : α} {f : Option β → Option β} :
(Const.alter m k f).1.size =
if m.contains k && (f (Const.get? m k)).isNone then
m.1.size - 1
else if !m.contains k && (f (Const.get? m k)).isSome then
m.1.size + 1
else
m.1.size := by
simp_to_model using List.Const.length_alterKey'
theorem size_alter_eq_add_one (h : m.1.WF) {k : α} {f : Option β → Option β}
(h₁ : m.contains k = false) (h₂ : (f (Const.get? m k)).isSome) :
(Const.alter m k f).1.size = m.1.size + 1 := by
simp [size_alter, h, h₁, h₂]
theorem size_alter_eq_sub_one (h : m.1.WF) {k : α} {f : Option β → Option β}
(h₁ : m.contains k) (h₂ : (f (Const.get? m k)).isNone) :
(Const.alter m k f).1.size = m.1.size - 1 := by
simp [size_alter, h, h₁, h₂]
theorem size_alter_eq_self_of_not_mem (h : m.1.WF) {k : α} {f : Option β → Option β}
(h₁ : m.contains k = false) (h₂ : (f (Const.get? m k)).isNone) :
(Const.alter m k f).1.size = m.1.size := by
simp [size_alter, h, h₁, h₂]
theorem size_alter_eq_self_of_mem (h : m.1.WF) {k : α} {f : Option β → Option β}
(h₁ : m.contains k) (h₂ : (f (Const.get? m k)).isSome) :
(Const.alter m k f).1.size = m.1.size := by
simp [size_alter, h, h₁, Option.isSome_iff_ne_none.mp h₂]
theorem size_alter_le_size [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option β → Option β} :
(Const.alter m k f).1.size ≤ m.1.size + 1 := by
simp [size_alter, h]
split <;> try split
all_goals omega
theorem size_le_size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option β → Option β} :
m.1.size - 1 ≤ (Const.alter m k f).1.size := by
simp [size_alter, h]
split <;> try split
all_goals omega
theorem get?_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} :
Const.get? (Const.alter m k f) k' =
if k == k' then
f (Const.get? m k)
else
Const.get? m k' := by
simp_to_model using List.Const.getValue?_alterKey
theorem get_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β}
(hc : (Const.alter m k f).contains k') :
Const.get (Const.alter m k f) k' hc =
if heq : k == k' then
haveI h' : (f (Const.get? m k)).isSome := by rwa [contains_alter _ h, if_pos heq] at hc
(f (Const.get? m k)).get <| h'
else
haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc
Const.get m k' h' := by
simp_to_model using List.Const.getValue_alterKey
theorem get_alter_self (h : m.1.WF) {k : α} {f : Option β → Option β}
{hc : (Const.alter m k f).contains k} :
haveI h' : (f (Const.get? m k)).isSome := by rwa [contains_alter _ h, BEq.refl] at hc
Const.get (Const.alter m k f) k hc = (f (Const.get? m k)).get h' := by
simp_to_model using List.Const.getValue_alterKey_self
theorem get!_alter {k k' : α} (h : m.1.WF) [Inhabited β] {f : Option β → Option β} :
Const.get! (Const.alter m k f) k' =
if k == k' then
(f (Const.get? m k)).get!
else
Const.get! m k' := by
simp_to_model using List.Const.getValue!_alterKey
theorem getD_alter {k k' : α} {fallback : β} (h : m.1.WF) {f : Option β → Option β} :
Const.getD (Const.alter m k f) k' fallback =
if k == k' then
f (Const.get? m k) |>.getD fallback
else
Const.getD m k' fallback := by
simp_to_model using List.Const.getValueD_alterKey
theorem getD_alter_self {k : α} {fallback : β} (h : m.1.WF) {f : Option β → Option β} :
Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback := by
simp only [h, getD_alter, BEq.refl, reduceIte]
theorem getKey?_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} :
(Const.alter m k f).getKey? k' =
if k == k' then
if (f (Const.get? m k)).isSome then some k else none
else
m.getKey? k' := by
simp_to_model using List.Const.getKey?_alterKey
theorem getKey!_alter [Inhabited α] {k k' : α} (h : m.1.WF) {f : Option β → Option β} :
(Const.alter m k f).getKey! k' =
if k == k' then
if (f (Const.get? m k)).isSome then k else default
else
m.getKey! k' := by
simp_to_model using List.Const.getKey!_alterKey
theorem getKey_alter [Inhabited α] {k k' : α} (h : m.1.WF) {f : Option β → Option β}
(hc : (Const.alter m k f).contains k') :
(Const.alter m k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc
m.getKey k' h' := by
simp_to_model using List.Const.getKey_alterKey
theorem getKeyD_alter {k k' fallback : α} (h : m.1.WF) {f : Option β → Option β} :
(Const.alter m k f).getKeyD k' fallback =
if k == k' then
if (f (Const.get? m k)).isSome then k else fallback
else
m.getKeyD k' fallback := by
simp_to_model using List.Const.getKeyD_alterKey
end Const
end Alter
section Modify
variable [LawfulBEq α]
@[simp]
theorem isEmpty_modify (h : m.1.WF) {k : α} {f : β k → β k} :
(m.modify k f).1.isEmpty = m.1.isEmpty := by
simp_to_model using List.isEmpty_modifyKey
theorem contains_modify (h : m.1.WF) {k k' : α} {f : β k → β k} :
(m.modify k f).contains k' = m.contains k' := by
simp_to_model using List.containsKey_modifyKey
theorem size_modify (h : m.1.WF) {k : α} {f : β k → β k} :
(m.modify k f).1.size = m.1.size := by
simp_to_model using List.length_modifyKey
theorem get?_modify (h : m.1.WF) {k k' : α} {f : β k → β k} :
(m.modify k f).get? k' =
if h : k == k' then
(cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f))
else
m.get? k' := by
simp_to_model using List.getValueCast?_modifyKey
@[simp]
theorem get?_modify_self (h : m.1.WF) {k : α} {f : β k → β k} :
(m.modify k f).get? k = (m.get? k).map f := by
simp_to_model using List.getValueCast?_modifyKey_self
theorem get_modify (h : m.1.WF) {k k' : α} {f : β k → β k}
(hc : (m.modify k f).contains k') :
(m.modify k f).get k' hc =
if heq : k == k' then
haveI h' : m.contains k := by rwa [contains_modify _ h, ← eq_of_beq heq] at hc
cast (congrArg β (eq_of_beq heq)) <| f (m.get k h')
else
haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc
m.get k' h' := by
simp_to_model using List.getValueCast_modifyKey
@[simp]
theorem get_modify_self (h : m.1.WF) {k : α} {f : β k → β k} {hc : (m.modify k f).contains k} :
haveI h' : m.contains k := by rwa [contains_modify _ h] at hc
(m.modify k f).get k hc = f (m.get k h') := by
simp_to_model using List.getValueCast_modifyKey_self
theorem get!_modify (h : m.1.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
(m.modify k f).get! k' =
if heq : k == k' then
m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!
else
m.get! k' := by
simp_to_model using List.getValueCast!_modifyKey
@[simp]
theorem get!_modify_self (h : m.1.WF) {k : α} [Inhabited (β k)] {f : β k → β k} :
(m.modify k f).get! k = ((m.get? k).map f).get! := by
simp_to_model using List.getValueCast!_modifyKey_self
theorem getD_modify (h : m.1.WF) {k k' : α} {fallback : β k'} {f : β k → β k} :
(m.modify k f).getD k' fallback =
if heq : k == k' then
m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
else
m.getD k' fallback := by
simp_to_model using List.getValueCastD_modifyKey
@[simp]
theorem getD_modify_self (h : m.1.WF) {k : α} {fallback : β k} {f : β k → β k} :
(m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback := by
simp_to_model using List.getValueCastD_modifyKey_self
theorem getKey?_modify (h : m.1.WF) {k k' : α} {f : β k → β k} :
(m.modify k f).getKey? k' =
if k == k' then
if m.contains k then some k else none
else
m.getKey? k' := by
simp_to_model using List.getKey?_modifyKey
theorem getKey?_modify_self (h : m.1.WF) {k : α} {f : β k → β k} :
(m.modify k f).getKey? k = if m.contains k then some k else none := by
simp_to_model using List.getKey?_modifyKey_self
theorem getKey!_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k} :
(m.modify k f).getKey! k' =
if k == k' then
if m.contains k then k else default
else
m.getKey! k' := by
simp_to_model using List.getKey!_modifyKey
theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → β k} :
(m.modify k f).getKey! k = if m.contains k then k else default := by
simp_to_model using List.getKey!_modifyKey_self
theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k}
(hc : (m.modify k f).contains k') :
(m.modify k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc
m.getKey k' h' := by
simp_to_model using List.getKey_modifyKey
@[simp]
theorem getKey_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → β k}
(hc : (m.modify k f).contains k) : (m.modify k f).getKey k hc = k := by
simp_to_model using List.getKey_modifyKey_self
theorem getKeyD_modify (h : m.1.WF) {k k' fallback : α} {f : β k → β k} :
(m.modify k f).getKeyD k' fallback =
if k == k' then
if m.contains k then k else fallback
else
m.getKeyD k' fallback := by
simp_to_model using List.getKeyD_modifyKey
theorem getKeyD_modify_self (h : m.1.WF) [Inhabited α] {k fallback : α} {f : β k → β k} :
(m.modify k f).getKeyD k fallback = if m.contains k then k else fallback := by
simp_to_model using List.getKeyD_modifyKey_self
namespace Const
variable {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α (fun _ => β))
omit [LawfulBEq α]
@[simp]
theorem isEmpty_modify (m : Raw₀ α (fun _ => β)) (h : m.1.WF) {k : α} {f : β → β} :
(Const.modify m k f).1.isEmpty = m.1.isEmpty := by
simp_to_model using List.Const.isEmpty_modifyKey
theorem contains_modify (h : m.1.WF) {k k' : α} {f : β → β} :
(Const.modify m k f).contains k' = m.contains k' := by
simp_to_model using List.Const.containsKey_modifyKey
theorem size_modify (h : m.1.WF) {k : α} {f : β → β} :
(Const.modify m k f).1.size = m.1.size := by
simp_to_model using List.Const.length_modifyKey
theorem get?_modify (h : m.1.WF) {k k' : α} {f : β → β} :
Const.get? (Const.modify m k f) k' =
if k == k' then
(Const.get? m k).map f
else
Const.get? m k' := by
simp_to_model using List.Const.getValue?_modifyKey
@[simp]
theorem get?_modify_self (h : m.1.WF) {k : α} {f : β → β} :
Const.get? (Const.modify m k f) k = (Const.get? m k).map f := by
simp_to_model using List.Const.getValue?_modifyKey_self
theorem get_modify (h : m.1.WF) {k k' : α} {f : β → β}
(hc : (Const.modify m k f).contains k') :
Const.get (Const.modify m k f) k' hc =
if heq : k == k' then
haveI h' : m.contains k := by rwa [contains_modify _ h, ← contains_congr _ h heq] at hc
f (Const.get m k h')
else
haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc
Const.get m k' h' := by
simp_to_model using List.Const.getValue_modifyKey
@[simp]
theorem get_modify_self (h : m.1.WF) {k : α} {f : β → β} {hc : (Const.modify m k f).contains k} :
haveI h' : m.contains k := by rwa [contains_modify _ h] at hc
Const.get (Const.modify m k f) k hc = f (Const.get m k h') := by
simp_to_model using List.Const.getValue_modifyKey_self
theorem get!_modify (h : m.1.WF) {k k' : α} [hi : Inhabited β] {f : β → β} :
Const.get! (Const.modify m k f) k' =
if k == k' then
Const.get? m k |>.map f |>.get!
else
Const.get! m k' := by
simp_to_model using List.Const.getValue!_modifyKey
@[simp]
theorem get!_modify_self (h : m.1.WF) {k : α} [Inhabited (β)] {f : β → β} :
Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get! := by
simp_to_model using List.Const.getValue!_modifyKey_self
theorem getD_modify (h : m.1.WF) {k k' : α} {fallback : β} {f : β → β} :
Const.getD (Const.modify m k f) k' fallback =
if k == k' then
Const.get? m k |>.map f |>.getD fallback
else
Const.getD m k' fallback := by
simp_to_model using List.Const.getValueD_modifyKey
@[simp]
theorem getD_modify_self (h : m.1.WF) {k : α} {fallback : β} {f : β → β} :
Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback := by
simp_to_model using List.Const.getValueD_modifyKey_self
theorem getKey?_modify (h : m.1.WF) {k k' : α} {f : β → β} :
(Const.modify m k f).getKey? k' =
if k == k' then
if m.contains k then some k else none
else
m.getKey? k' := by
simp_to_model using List.Const.getKey?_modifyKey
theorem getKey?_modify_self (h : m.1.WF) {k : α} {f : β → β} :
(Const.modify m k f).getKey? k = if m.contains k then some k else none := by
simp_to_model using List.Const.getKey?_modifyKey_self
theorem getKey!_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β} :
(Const.modify m k f).getKey! k' =
if k == k' then
if m.contains k then k else default
else
m.getKey! k' := by
simp_to_model using List.Const.getKey!_modifyKey
theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β} :
(Const.modify m k f).getKey! k = if m.contains k then k else default := by
simp_to_model using List.Const.getKey!_modifyKey_self
theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β}
(hc : (Const.modify m k f).contains k') :
(Const.modify m k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc
m.getKey k' h' := by
simp_to_model using List.Const.getKey_modifyKey
@[simp]
theorem getKey_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β}
(hc : (Const.modify m k f).contains k) : (Const.modify m k f).getKey k hc = k := by
simp_to_model using List.Const.getKey_modifyKey_self
theorem getKeyD_modify (h : m.1.WF) {k k' fallback : α} {f : β → β} :
(Const.modify m k f).getKeyD k' fallback =
if k == k' then
if m.contains k then k else fallback
else
m.getKeyD k' fallback := by
simp_to_model using List.Const.getKeyD_modifyKey
theorem getKeyD_modify_self (h : m.1.WF) [Inhabited α] {k fallback : α} {f : β → β} :
(Const.modify m k f).getKeyD k fallback = if m.contains k then k else fallback := by
simp_to_model using List.Const.getKeyD_modifyKey_self
end Const
end Modify
end Raw₀
end Std.DHashMap.Internal

18
src/Std/Data/DHashMap/Internal/WF.lean
View file

@ -641,6 +641,12 @@ theorem toListModel_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashabl
rw [insertEntry_of_containsKey_eq_false]
exact hc
theorem toListModel_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
{m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} :
Perm (toListModel (Const.alter m a f).1.2) (Const.alterKey a f (toListModel m.1.2)) := by
rw [alter_eq_alterₘ]
exact toListModel_alterₘ h
theorem wfImp_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)}
(h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : Raw.WFImp (Const.alterₘ m a f).1 where
buckets_hash_self := isHashSelf_alterₘ m h a f
@ -691,13 +697,19 @@ theorem wfImp_modify [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h
namespace Const
variable {β : Type v}
variable {β : Type v} {m : Raw₀ α (fun _ => β)}
theorem wfImp_modifyₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)}
theorem toListModel_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.1)
{a : α} {f : β → β} :
Perm (toListModel (Const.modify m a f).1.2) (Const.modifyKey a f (toListModel m.1.2)) := by
rw [Const.modify_eq_alter, Const.modifyKey_eq_alterKey]
exact Const.toListModel_alter h
theorem wfImp_modifyₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
(h : Raw.WFImp m.1) {a : α} {f : β → β} : Raw.WFImp (Const.modifyₘ m a f).1 :=
Const.wfImp_alterₘ h
theorem wfImp_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)}
theorem wfImp_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
(h : Raw.WFImp m.1) {a : α} {f : β → β} : Raw.WFImp (Const.modify m a f).1 := by
rw [Const.modify_eq_modifyₘ]
exact wfImp_alterₘ h

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

@ -1866,4 +1866,669 @@ theorem getD_unitOfList
end Const
variable {m : DHashMap α β}
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone) :=
Raw₀.isEmpty_alter_eq_isEmpty_erase _ m.2
@[simp]
theorem isEmpty_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (get? m k)).isNone) :=
Raw₀.isEmpty_alter _ m.2
theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} :
(m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k' :=
Raw₀.contains_alter ⟨_, _⟩ m.2
theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} :
k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m := by
simp only [mem_iff_contains, contains_alter, beq_iff_eq, Bool.ite_eq_true_distrib]
theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : k == k') :
k' ∈ m.alter k f ↔ (f (m.get? k)).isSome := by
rw [mem_alter, if_pos h]
@[simp]
theorem contains_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).contains k = (f (m.get? k)).isSome := by
simp only [contains_alter, beq_self_eq_true, reduceIte]
@[simp]
theorem mem_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
k ∈ m.alter k f ↔ (f (m.get? k)).isSome := by
rw [mem_iff_contains, contains_alter_self]
theorem contains_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : (k == k') = false) : (m.alter k f).contains k' = m.contains k' := by
simp only [contains_alter, h, Bool.false_eq_true, reduceIte]
theorem mem_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_alter_of_beq_eq_false, h]
theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).size =
if m.contains k && (f (m.get? k)).isNone then
m.size - 1
else if !m.contains k && (f (m.get? k)).isSome then
m.size + 1
else
m.size :=
Raw₀.size_alter ⟨m.1, _⟩ m.2
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : k ∉ m) (h' : (f (m.get? k)).isSome) :
(m.alter k f).size = m.size + 1 := by
rw [mem_iff_contains, Bool.not_eq_true] at h
exact Raw₀.size_alter_eq_add_one ⟨m.1, _⟩ m.2 h h'
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : k ∈ m) (h' : (f (m.get? k)).isNone) :
(m.alter k f).size = m.size - 1 :=
Raw₀.size_alter_eq_sub_one ⟨m.1, _⟩ m.2 h h'
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : k ∉ m) (h' : (f (m.get? k)).isNone) : (m.alter k f).size = m.size := by
rw [mem_iff_contains, Bool.not_eq_true] at h
exact Raw₀.size_alter_eq_self_of_not_mem ⟨m.1, _⟩ m.2 h h'
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : k ∈ m) (h' : (f (m.get? k)).isSome) : (m.alter k f).size = m.size :=
Raw₀.size_alter_eq_self_of_mem ⟨m.1, _⟩ m.2 h h'
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).size ≤ m.size + 1 :=
Raw₀.size_alter_le_size ⟨m.1, _⟩ m.2
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
m.size - 1 ≤ (m.alter k f).size :=
Raw₀.size_le_size_alter ⟨m.1, _⟩ m.2
theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).get? k' =
if h : k == k' then
(cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k)))
else
m.get? k' :=
Raw₀.get?_alter ⟨m.1, _⟩ m.2
@[simp]
theorem get?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).get? k = f (m.get? k) := by
simp only [get?_alter, beq_self_eq_true, reduceDIte, Function.comp_apply, cast_eq]
theorem get_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
{h : k' ∈ m.alter k f} :
(m.alter k f).get k' h =
if heq : k == k' then
haveI h' : (f (m.get? k)).isSome := mem_alter_of_beq heq |>.mp h
cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h'
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
m.get k' h' :=
Raw₀.get_alter ⟨m.1, _⟩ m.2 h
@[simp]
theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
{h : k ∈ m.alter k f} :
haveI h' : (f (m.get? k)).isSome := mem_alter_self.mp h
(m.alter k f).get k h = (f (m.get? k)).get h' :=
Raw₀.get_alter_self ⟨m.1, _⟩ m.2
theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')]
{f : Option (β k) → Option (β k)} : (m.alter k f).get! k' =
if heq : k == k' then
(f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get!
else
m.get! k' :=
Raw₀.get!_alter ⟨m.1, _⟩ m.2
private theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) :
Option.map (cast h) x = cast (congrArg Option h) x := by
cases h; cases x <;> simp
@[simp]
theorem get!_alter_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k) → Option (β k)} :
(m.alter k f).get! k = (f (m.get? k)).get! := by
simp only [get!_alter, beq_self_eq_true, reduceDIte, cast_eq, Option.map_cast_apply]
theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} :
(m.alter k f).getD k' fallback =
if heq : k == k' then
f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
else
m.getD k' fallback :=
Raw₀.getD_alter ⟨m.1, _⟩ m.2
@[simp]
theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} :
(m.alter k f).getD k fallback = (f (m.get? k)).getD fallback :=
Raw₀.getD_alter_self ⟨m.1, _⟩ m.2
theorem getKey?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).getKey? k' =
if k == k' then
if (f (m.get? k)).isSome then some k else none
else
m.getKey? k' :=
Raw₀.getKey?_alter ⟨m.1, _⟩ m.2
theorem getKey?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).getKey? k = if (f (m.get? k)).isSome then some k else none := by
simp only [getKey?_alter, beq_self_eq_true, ↓reduceIte]
theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).getKey! k' =
if k == k' then
if (f (m.get? k)).isSome then k else default
else
m.getKey! k' := by
simp [getKey!_eq_get!_getKey?, getKey?_alter]
split
· next heq =>
cases eq_of_beq heq
split <;> rfl
· next heq =>
rfl
theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default := by
simp only [getKey!_alter, beq_self_eq_true, reduceIte]
theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
{h : k' ∈ m.alter k f} :
(m.alter k f).getKey k' h =
if heq : k == k' then
k
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
m.getKey k' h' :=
Raw₀.getKey_alter ⟨m.1, _⟩ m.2 h
@[simp]
theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
{h : k ∈ m.alter k f} : (m.alter k f).getKey k h = k := by
simp [getKey_alter]
theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} {f : Option (β k) → Option (β k)} :
(m.alter k f).getKeyD k' fallback =
if k == k' then
if (f (m.get? k)).isSome then k else fallback
else
m.getKeyD k' fallback :=
Raw₀.getKeyD_alter ⟨m.1, _⟩ m.2
@[simp]
theorem getKeyD_alter_self [LawfulBEq α] [Inhabited α] {k : α} {fallback : α}
{f : Option (β k) → Option (β k)} :
(m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome then k else fallback := by
simp [getKeyD_alter]
namespace Const
variable {β : Type v} {m : DHashMap α (fun _ => β)}
theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α}
{f : Option β → Option β} :
(Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Const.get? m k)).isNone) :=
Raw₀.Const.isEmpty_alter_eq_isEmpty_erase _ m.2
@[simp]
theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(Const.alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k))
&& (f (Const.get? m k)).isNone) :=
Raw₀.Const.isEmpty_alter _ m.2
theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
(Const.alter m k f).contains k' =
if k == k' then (f (Const.get? m k)).isSome else m.contains k' :=
Raw₀.Const.contains_alter ⟨m.1, _⟩ m.2
theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
k' ∈ Const.alter m k f ↔ if k == k' then (f (Const.get? m k)).isSome = true else k' ∈ m := by
simp only [mem_iff_contains, contains_alter, Bool.ite_eq_true_distrib]
theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
(h : k == k') : k' ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by
rw [mem_alter, if_pos h]
@[simp]
theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(Const.alter m k f).contains k = (f (Const.get? m k)).isSome := by
simp only [contains_alter, BEq.refl, reduceIte]
@[simp]
theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
k ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by
rw [mem_iff_contains, contains_alter_self]
theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : (k == k') = false) :
(Const.alter m k f).contains k' = m.contains k' := by
simp only [contains_alter, h, Bool.false_eq_true, reduceIte]
theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : (k == k') = false) : k' ∈ Const.alter m k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_alter_of_beq_eq_false, h]
theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} :
(Const.alter m k f).size =
if m.contains k && (f (Const.get? m k)).isNone then
m.size - 1
else if !m.contains k && (f (Const.get? m k)).isSome then
m.size + 1
else
m.size :=
Raw₀.Const.size_alter ⟨m.1, _⟩ m.2
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∉ m) (h' : (f (Const.get? m k)).isSome) :
(Const.alter m k f).size = m.size + 1 := by
rw [mem_iff_contains, Bool.not_eq_true] at h
exact Raw₀.Const.size_alter_eq_add_one ⟨m.1, _⟩ m.2 h h'
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∈ m) (h' : (f (Const.get? m k)).isNone) :
(Const.alter m k f).size = m.size - 1 :=
Raw₀.Const.size_alter_eq_sub_one ⟨m.1, _⟩ m.2 h h'
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∉ m) (h' : (f (Const.get? m k)).isNone) : (Const.alter m k f).size = m.size := by
rw [mem_iff_contains, Bool.not_eq_true] at h
exact Raw₀.Const.size_alter_eq_self_of_not_mem ⟨m.1, _⟩ m.2 h h'
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∈ m) (h' : (f (Const.get? m k)).isSome) : (Const.alter m k f).size = m.size :=
Raw₀.Const.size_alter_eq_self_of_mem ⟨m.1, _⟩ m.2 h h'
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} :
(Const.alter m k f).size ≤ m.size + 1 :=
Raw₀.Const.size_alter_le_size ⟨m.1, _⟩ m.2
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} :
m.size - 1 ≤ (Const.alter m k f).size :=
Raw₀.Const.size_le_size_alter ⟨m.1, _⟩ m.2
theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
Const.get? (Const.alter m k f) k' =
if k == k' then
f (Const.get? m k)
else
Const.get? m k' :=
Raw₀.Const.get?_alter ⟨m.1, _⟩ m.2
@[simp]
theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
Const.get? (Const.alter m k f) k = f (Const.get? m k) := by
simp [get?_alter]
theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
{h : k' ∈ Const.alter m k f} :
Const.get (Const.alter m k f) k' h =
if heq : k == k' then
haveI h' : (f (Const.get? m k)).isSome := mem_alter_of_beq heq |>.mp h
f (Const.get? m k) |>.get h'
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
Const.get m k' h' :=
Raw₀.Const.get_alter ⟨m.1, _⟩ m.2 h
@[simp]
theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
{h : k ∈ Const.alter m k f} :
haveI h' : (f (Const.get? m k)).isSome := mem_alter_self.mp h
Const.get (Const.alter m k f) k h = (f (Const.get? m k)).get h' := by
simp [get_alter]
theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
{f : Option β → Option β} : Const.get! (Const.alter m k f) k' =
if k == k' then
f (Const.get? m k) |>.get!
else
Const.get! m k' :=
Raw₀.Const.get!_alter ⟨m.1, _⟩ m.2
@[simp]
theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
{f : Option β → Option β} : Const.get! (Const.alter m k f) k = (f (Const.get? m k)).get! := by
simp [get!_alter]
theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
{f : Option β → Option β} :
Const.getD (Const.alter m k f) k' fallback =
if k == k' then
f (Const.get? m k) |>.getD fallback
else
Const.getD m k' fallback :=
Raw₀.Const.getD_alter ⟨m.1, _⟩ m.2
@[simp]
theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β}
{f : Option β → Option β} :
Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback := by
simp [getD_alter]
theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
(Const.alter m k f).getKey? k' =
if k == k' then
if (f (Const.get? m k)).isSome then some k else none
else
m.getKey? k' :=
Raw₀.Const.getKey?_alter ⟨m.1, _⟩ m.2
theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(Const.alter m k f).getKey? k = if (f (Const.get? m k)).isSome then some k else none := by
simp [getKey?_alter]
theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} : (Const.alter m k f).getKey! k' =
if k == k' then
if (f (Const.get? m k)).isSome then k else default
else
m.getKey! k' :=
Raw₀.Const.getKey!_alter ⟨m.1, _⟩ m.2
theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} :
(Const.alter m k f).getKey! k = if (f (Const.get? m k)).isSome then k else default := by
simp [getKey!_alter]
theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} {h : k' ∈ Const.alter m k f} :
(Const.alter m k f).getKey k' h =
if heq : k == k' then
k
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
m.getKey k' h' :=
Raw₀.Const.getKey_alter ⟨m.1, _⟩ m.2 h
@[simp]
theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} {h : k ∈ Const.alter m k f} :
(Const.alter m k f).getKey k h = k := by
simp [getKey_alter]
theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} :
(Const.alter m k f).getKeyD k' fallback =
if k == k' then
if (f (Const.get? m k)).isSome then k else fallback
else
m.getKeyD k' fallback :=
Raw₀.Const.getKeyD_alter ⟨m.1, _⟩ m.2
theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
{f : Option β → Option β} :
(Const.alter m k f).getKeyD k fallback =
if (f (Const.get? m k)).isSome then k else fallback := by
simp [getKeyD_alter]
end Const
end Alter
section Modify
@[simp]
theorem isEmpty_modify [LawfulBEq α] {k : α} {f : β k → β k} :
(m.modify k f).isEmpty = m.isEmpty :=
Raw₀.isEmpty_modify _ m.2
@[simp]
theorem contains_modify [LawfulBEq α] {k k': α} {f : β k → β k} :
(m.modify k f).contains k' = m.contains k' :=
Raw₀.contains_modify ⟨m.1, _⟩ m.2
@[simp]
theorem mem_modify [LawfulBEq α] {k k': α} {f : β k → β k} : k' ∈ m.modify k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_modify]
@[simp]
theorem size_modify [LawfulBEq α] {k : α} {f : β k → β k} : (m.modify k f).size = m.size :=
Raw₀.size_modify ⟨m.1, _⟩ m.2
theorem get?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} :
(m.modify k f).get? k' = if h : k == k' then
(cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f))
else
m.get? k' :=
Raw₀.get?_modify ⟨m.1, _⟩ m.2
@[simp]
theorem get?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} :
(m.modify k f).get? k = (m.get? k).map f :=
Raw₀.get?_modify_self ⟨m.1, _⟩ m.2
theorem get_modify [LawfulBEq α] {k k' : α} {f : β k → β k}
(h : k' ∈ m.modify k f) :
(m.modify k f).get k' h =
if heq : k == k' then
haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h
cast (congrArg β (eq_of_beq heq)) <| f (m.get k h')
else
haveI h' : k' ∈ m := mem_modify.mp h
m.get k' h' :=
Raw₀.get_modify ⟨m.1, _⟩ m.2 h
@[simp]
theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} {h : k ∈ m.modify k f} :
haveI h' : k ∈ m := mem_modify.mp h
(m.modify k f).get k h = f (m.get k h') :=
Raw₀.get_modify_self ⟨m.1, _⟩ m.2
theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
(m.modify k f).get! k' =
if heq : k == k' then
m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!
else
m.get! k' :=
Raw₀.get!_modify ⟨m.1, _⟩ m.2
@[simp]
theorem get!_modify_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} :
(m.modify k f).get! k = ((m.get? k).map f).get! :=
Raw₀.get!_modify_self ⟨m.1, _⟩ m.2
theorem getD_modify [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} :
(m.modify k f).getD k' fallback =
if heq : k == k' then
m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
else
m.getD k' fallback :=
Raw₀.getD_modify ⟨m.1, _⟩ m.2
@[simp]
theorem getD_modify_self [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} :
(m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback :=
Raw₀.getD_modify_self ⟨m.1, _⟩ m.2
theorem getKey?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} :
(m.modify k f).getKey? k' =
if k == k' then
if k ∈ m then some k else none
else
m.getKey? k' :=
Raw₀.getKey?_modify ⟨m.1, _⟩ m.2
theorem getKey?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} :
(m.modify k f).getKey? k = if k ∈ m then some k else none :=
Raw₀.getKey?_modify_self ⟨m.1, _⟩ m.2
theorem getKey!_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} :
(m.modify k f).getKey! k' =
if k == k' then
if k ∈ m then k else default
else
m.getKey! k' :=
Raw₀.getKey!_modify ⟨m.1, _⟩ m.2
theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} :
(m.modify k f).getKey! k = if k ∈ m then k else default :=
Raw₀.getKey!_modify_self ⟨m.1, _⟩ m.2
theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
{h : k' ∈ m.modify k f} :
(m.modify k f).getKey k' h =
if k == k' then
k
else
haveI h' : k' ∈ m := mem_modify.mp h
m.getKey k' h' :=
Raw₀.getKey_modify ⟨m.1, _⟩ m.2 h
@[simp]
theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
{h : k ∈ m.modify k f} : (m.modify k f).getKey k h = k :=
Raw₀.getKey_modify_self ⟨m.1, _⟩ m.2 h
theorem getKeyD_modify [LawfulBEq α] {k k' fallback : α} {f : β k → β k} :
(m.modify k f).getKeyD k' fallback =
if k == k' then
if k ∈ m then k else fallback
else
m.getKeyD k' fallback :=
Raw₀.getKeyD_modify ⟨m.1, _⟩ m.2
theorem getKeyD_modify_self [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} :
(m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback :=
Raw₀.getKeyD_modify_self ⟨m.1, _⟩ m.2
namespace Const
variable {β : Type v} {m : DHashMap α (fun _ => β)}
@[simp]
theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(Const.modify m k f).isEmpty = m.isEmpty :=
Raw₀.Const.isEmpty_modify _ m.2
@[simp]
theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
(Const.modify m k f).contains k' = m.contains k' :=
Raw₀.Const.contains_modify ⟨m.1, _⟩ m.2
@[simp]
theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
k' ∈ Const.modify m k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_modify]
@[simp]
theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(Const.modify m k f).size = m.size :=
Raw₀.Const.size_modify ⟨m.1, _⟩ m.2
theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
Const.get? (Const.modify m k f) k' = if k == k' then
Const.get? m k |>.map f
else
Const.get? m k' :=
Raw₀.Const.get?_modify ⟨m.1, _⟩ m.2
@[simp]
theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
Const.get? (Const.modify m k f) k = (Const.get? m k).map f :=
Raw₀.Const.get?_modify_self ⟨m.1, _⟩ m.2
theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
{h : k' ∈ Const.modify m k f} :
Const.get (Const.modify m k f) k' h =
if heq : k == k' then
haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h
f (Const.get m k h')
else
haveI h' : k' ∈ m := mem_modify.mp h
Const.get m k' h' :=
Raw₀.Const.get_modify ⟨m.1, _⟩ m.2 h
@[simp]
theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
{h : k ∈ Const.modify m k f} :
haveI h' : k ∈ m := mem_modify.mp h
Const.get (Const.modify m k f) k h = f (Const.get m k h') :=
Raw₀.Const.get_modify_self ⟨m.1, _⟩ m.2
theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
Const.get! (Const.modify m k f) k' =
if k == k' then
Const.get? m k |>.map f |>.get!
else
Const.get! m k' :=
Raw₀.Const.get!_modify ⟨m.1, _⟩ m.2
@[simp]
theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get! :=
Raw₀.Const.get!_modify_self ⟨m.1, _⟩ m.2
theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
Const.getD (Const.modify m k f) k' fallback =
if k == k' then
Const.get? m k |>.map f |>.getD fallback
else
Const.getD m k' fallback :=
Raw₀.Const.getD_modify ⟨m.1, _⟩ m.2
@[simp]
theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} :
Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback :=
Raw₀.Const.getD_modify_self ⟨m.1, _⟩ m.2
theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
(Const.modify m k f).getKey? k' =
if k == k' then
if k ∈ m then some k else none
else
m.getKey? k' :=
Raw₀.Const.getKey?_modify ⟨m.1, _⟩ m.2
theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(Const.modify m k f).getKey? k = if k ∈ m then some k else none :=
Raw₀.Const.getKey?_modify_self ⟨m.1, _⟩ m.2
theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} :
(Const.modify m k f).getKey! k' =
if k == k' then
if k ∈ m then k else default
else
m.getKey! k' :=
Raw₀.Const.getKey!_modify ⟨m.1, _⟩ m.2
theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} :
(Const.modify m k f).getKey! k = if k ∈ m then k else default :=
Raw₀.Const.getKey!_modify_self ⟨m.1, _⟩ m.2
theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
{h : k' ∈ Const.modify m k f} :
(Const.modify m k f).getKey k' h =
if k == k' then
k
else
haveI h' : k' ∈ m := mem_modify.mp h
m.getKey k' h' :=
Raw₀.Const.getKey_modify ⟨m.1, _⟩ m.2 h
@[simp]
theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
{h : k ∈ Const.modify m k f} : (Const.modify m k f).getKey k h = k :=
Raw₀.Const.getKey_modify_self ⟨m.1, _⟩ m.2 h
theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} :
(Const.modify m k f).getKeyD k' fallback =
if k == k' then
if k ∈ m then k else fallback
else
m.getKeyD k' fallback :=
Raw₀.Const.getKeyD_modify ⟨m.1, _⟩ m.2
theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β} :
(Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback :=
Raw₀.Const.getKeyD_modify_self ⟨m.1, _⟩ m.2
end Const
end Modify
end Std.DHashMap

39
src/Std/Data/DHashMap/Raw.lean
View file

@ -296,6 +296,45 @@ to get anything out of the hash map.
@[inline] def isEmpty (m : Raw α β) : Bool :=
m.size == 0
/--
Modifies in place the value associated with a given key.
This function ensures that the value is used linearly.
-/
@[inline] def modify [BEq α] [LawfulBEq α] [Hashable α] (m : Raw α β) (a : α) (f : β a → β a) :
Raw α β :=
if h : 0 < m.buckets.size then
Raw₀.modify ⟨m, h⟩ a f
else
∅
@[inline, inherit_doc Raw.modify] def Const.modify [BEq α] [EquivBEq α] [Hashable α] {β : Type v}
(m : Raw α (fun _ => β)) (a : α) (f : β → β) : Raw α (fun _ => β) :=
if h : 0 < m.buckets.size then
Raw₀.Const.modify ⟨m, h⟩ a f
else
∅
/--
Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.
This function ensures that the value is used linearly.
-/
@[inline] def alter [BEq α] [LawfulBEq α] [Hashable α] (m : Raw α β)
(a : α) (f : Option (β a) → Option (β a)) : Raw α β :=
if h : 0 < m.buckets.size then
Raw₀.alter ⟨m, h⟩ a f
else
∅
@[inline, inherit_doc Raw.alter] def Const.alter [BEq α] [EquivBEq α] [Hashable α] {β : Type v}
(m : Raw α (fun _ => β)) (a : α) (f : Option β → Option β) : Raw α (fun _ => β) :=
if h : 0 < m.buckets.size then
Raw₀.Const.alter ⟨m, h⟩ a f
else
∅
section Unverified
/-! We currently do not provide lemmas for the functions below. -/

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

@ -62,7 +62,8 @@ private def baseNames : Array Name :=
``insertMany_eq, ``insertMany_val,
``Const.insertMany_eq, ``Const.insertMany_val,
``Const.insertManyIfNewUnit_eq, ``Const.insertManyIfNewUnit_val,
``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq]
``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq,
``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq]
/-- Internal implementation detail of the hash map -/
scoped syntax "simp_to_raw" ("using" term)? : tactic
@ -1978,4 +1979,728 @@ theorem getD_unitOfList
end Const
end Raw
namespace Raw
variable [BEq α] [Hashable α] {m : Raw α β}
open Internal.Raw Internal.Raw₀
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) : (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone) := by
simp_to_raw using Raw₀.isEmpty_alter_eq_isEmpty_erase
@[simp]
theorem isEmpty_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (m.get? k)).isNone) := by
simp_to_raw using Raw₀.isEmpty_alter
theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k' := by
simp_to_raw using Raw₀.contains_alter
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]
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
rw [mem_alter h, if_pos he]
@[simp]
theorem contains_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).contains k = (f (m.get? k)).isSome := by
simp only [contains_alter h, beq_self_eq_true, reduceIte]
@[simp]
theorem mem_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
k ∈ m.alter k f ↔ (f (m.get? k)).isSome := by
rw [mem_iff_contains, contains_alter_self h]
theorem contains_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : m.WF) (he : (k == k') = false) : (m.alter k f).contains k' = m.contains k' := by
simp only [contains_alter h, he, Bool.false_eq_true, reduceIte]
theorem mem_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : m.WF) (he : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_alter_of_beq_eq_false h, he]
theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).size =
if m.contains k && (f (m.get? k)).isNone then
m.size - 1
else if !m.contains k && (f (m.get? k)).isSome then
m.size + 1
else
m.size := by
simp_to_raw using Raw₀.size_alter
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isSome) :
(m.alter k f).size = m.size + 1 := by
revert h₁ h₂
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.size_alter_eq_add_one
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) (h₁ : k ∈ m) (h₂ : (f (m.get? k)).isNone) :
(m.alter k f).size = m.size - 1 := by
revert h₁ h₂
simp only [mem_iff_contains]
simp_to_raw using Raw₀.size_alter_eq_sub_one
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isNone) :
(m.alter k f).size = m.size := by
revert h₁ h₂
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.size_alter_eq_self_of_not_mem
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) (h₁ : k ∈ m) (h₂ : (f (m.get? k)).isSome) :
(m.alter k f).size = m.size := by
revert h₁ h₂
simp only [mem_iff_contains]
simp_to_raw using Raw₀.size_alter_eq_self_of_mem
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).size ≤ m.size + 1 := by
simp_to_raw using Raw₀.size_alter_le_size
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
m.size - 1 ≤ (m.alter k f).size := by
simp_to_raw using Raw₀.size_le_size_alter ⟨m, h.size_buckets_pos⟩
theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).get? k' = if h : k == k' then
(cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k)))
else m.get? k' := by
simp_to_raw using Raw₀.get?_alter
@[simp]
theorem get?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).get? k = f (m.get? k) := by
simp [get?_alter h]
theorem get_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : m.WF) {hc : k' ∈ m.alter k f} :
(m.alter k f).get k' hc =
if heq : k == k' then
haveI h' : (f (m.get? k)).isSome := mem_alter_of_beq h heq |>.mp hc
cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h'
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
m.get k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.get_alter
@[simp]
theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) {hc : k ∈ m.alter k f} :
haveI h' : (f (m.get? k)).isSome := mem_alter_self h |>.mp hc
(m.alter k f).get k hc = (f (m.get? k)).get h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.get_alter_self
theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')]
{f : Option (β k) → Option (β k)} (h : m.WF) : (m.alter k f).get! k' =
if heq : k == k' then
(f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get!
else
m.get! k' := by
simp_to_raw using Raw₀.get!_alter
private theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) :
Option.map (cast h) x = cast (congrArg Option h) x := by
cases h; cases x <;> simp
@[simp]
theorem get!_alter_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k) → Option (β k)}
(h : m.WF) : (m.alter k f).get! k = (f (m.get? k)).get! := by
simp [get!_alter h, Option.map_cast_apply]
theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)}
(h : m.WF) : (m.alter k f).getD k' fallback =
if heq : k == k' then
f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
else
m.getD k' fallback := by
simp_to_raw using Raw₀.getD_alter
@[simp]
theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)}
(h : m.WF) : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback := by
simp_to_raw using Raw₀.getD_alter_self
theorem getKey?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).getKey? k' =
if k == k' then
if (f (m.get? k)).isSome then some k else none
else
m.getKey? k' := by
simp_to_raw using Raw₀.getKey?_alter
theorem getKey?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).getKey? k = if (f (m.get? k)).isSome then some k else none := by
simp [getKey?_alter h]
theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : m.WF) : (m.alter k f).getKey! k' =
if k == k' then
if (f (m.get? k)).isSome then k else default
else
m.getKey! k' := by
simp_to_raw using Raw₀.getKey!_alter
theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) : (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default := by
simp [getKey!_alter h]
theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
(h : m.WF) {hc : k' ∈ m.alter k f} :
(m.alter k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
m.getKey k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.getKey_alter
@[simp]
theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
(h : m.WF) {hc : k ∈ m.alter k f} : (m.alter k f).getKey k hc = k := by
simp [getKey_alter h]
theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).getKeyD k' fallback =
if k == k' then
if (f (m.get? k)).isSome then k else fallback
else
m.getKeyD k' fallback := by
simp_to_raw using Raw₀.getKeyD_alter
@[simp]
theorem getKeyD_alter_self [LawfulBEq α] [Inhabited α] {k : α} {fallback : α}
{f : Option (β k) → Option (β k)} (h : m.WF) :
(m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome then k else fallback := by
simp [getKeyD_alter h]
namespace Const
variable {β : Type v} {m : Raw α (fun _ => β)}
theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α}
{f : Option β → Option β} (h : m.WF) :
(Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Const.get? m k)).isNone) := by
simp_to_raw using Raw₀.Const.isEmpty_alter_eq_isEmpty_erase
@[simp]
theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF) :
(Const.alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) &&
(f (get? m k)).isNone) := by
simp_to_raw using Raw₀.Const.isEmpty_alter
theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
(h : m.WF) : (Const.alter m k f).contains k' =
if k == k' then (f (Const.get? m k)).isSome else m.contains k' := by
simp_to_raw using Raw₀.Const.contains_alter
theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} (h : m.WF) :
k' ∈ Const.alter m k f ↔ if k == k' then (f (Const.get? m k)).isSome = true else k' ∈ m := by
simp only [mem_iff_contains, contains_alter h, Bool.ite_eq_true_distrib]
theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
(h : m.WF) (he : k == k') : k' ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by
rw [mem_alter h, if_pos he]
@[simp]
theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : (Const.alter m k f).contains k = (f (Const.get? m k)).isSome := by
simp only [contains_alter h, BEq.refl, reduceIte]
@[simp]
theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : k ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by
rw [mem_iff_contains, contains_alter_self h]
theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : m.WF) (he : (k == k') = false) :
(Const.alter m k f).contains k' = m.contains k' := by
simp only [contains_alter h, he, Bool.false_eq_true, reduceIte]
theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : m.WF) (he : (k == k') = false) :
k' ∈ Const.alter m k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_alter_of_beq_eq_false h, he]
theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
(Const.alter m k f).size =
if m.contains k && (f (Const.get? m k)).isNone then
m.size - 1
else if !m.contains k && (f (Const.get? m k)).isSome then
m.size + 1
else
m.size := by
simp_to_raw using Raw₀.Const.size_alter
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Const.get? m k)).isSome) :
(Const.alter m k f).size = m.size + 1 := by
revert h₁ h₂
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.size_alter_eq_add_one
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : m.WF) (h₁ : k ∈ m) (h₂ : (f (Const.get? m k)).isNone) :
(Const.alter m k f).size = m.size - 1 := by
revert h₁ h₂
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.size_alter_eq_sub_one
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Const.get? m k)).isNone) :
(Const.alter m k f).size = m.size := by
revert h₁ h₂
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.size_alter_eq_self_of_not_mem
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : m.WF) (h₁ : k ∈ m) (h₂ : (f (Const.get? m k)).isSome) :
(Const.alter m k f).size = m.size := by
revert h₁ h₂
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.size_alter_eq_self_of_mem
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
(Const.alter m k f).size ≤ m.size + 1 := by
simp_to_raw using Raw₀.Const.size_alter_le_size
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
m.size - 1 ≤ (Const.alter m k f).size := by
simp_to_raw using Raw₀.Const.size_le_size_alter ⟨m, h.size_buckets_pos⟩
theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) :
Const.get? (Const.alter m k f) k' =
if k == k' then
f (Const.get? m k)
else
Const.get? m k' := by
simp_to_raw using Raw₀.Const.get?_alter
@[simp]
theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : Const.get? (Const.alter m k f) k = f (Const.get? m k) := by
simp [get?_alter h]
theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
(h : m.WF) {hc : k' ∈ Const.alter m k f} :
Const.get (Const.alter m k f) k' hc =
if heq : k == k' then
haveI h' : (f (Const.get? m k)).isSome := mem_alter_of_beq h heq |>.mp hc
f (Const.get? m k) |>.get h'
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
Const.get m k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.Const.get_alter
@[simp]
theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) {hc : k ∈ Const.alter m k f} :
haveI h' : (f (Const.get? m k)).isSome := mem_alter_self h |>.mp hc
Const.get (Const.alter m k f) k hc = (f (Const.get? m k)).get h' := by
simp only [mem_iff_contains] at hc
revert hc
simp [get_alter h]
theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
{f : Option β → Option β} (h : m.WF) : Const.get! (Const.alter m k f) k' =
if k == k' then
f (Const.get? m k) |>.get!
else
Const.get! m k' := by
simp_to_raw using Raw₀.Const.get!_alter
@[simp]
theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
{f : Option β → Option β} (h : m.WF) :
Const.get! (Const.alter m k f) k = (f (Const.get? m k)).get! := by
simp [get!_alter h]
theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β}
(h : m.WF) : Const.getD (Const.alter m k f) k' fallback =
if k == k' then
f (Const.get? m k) |>.getD fallback
else
Const.getD m k' fallback := by
simp_to_raw using Raw₀.Const.getD_alter
@[simp]
theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β}
{f : Option β → Option β} (h : m.WF) :
Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback := by
simp [getD_alter h]
theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
(h : m.WF) : (Const.alter m k f).getKey? k' =
if k == k' then
if (f (Const.get? m k)).isSome then some k else none
else
m.getKey? k' := by
simp_to_raw using Raw₀.Const.getKey?_alter
theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) :
(Const.alter m k f).getKey? k = if (f (Const.get? m k)).isSome then some k else none := by
simp [getKey?_alter h]
theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} (h : m.WF) : (Const.alter m k f).getKey! k' =
if k == k' then
if (f (Const.get? m k)).isSome then k else default
else
m.getKey! k' := by
simp_to_raw using Raw₀.Const.getKey!_alter
theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} (h : m.WF) :
(Const.alter m k f).getKey! k = if (f (Const.get? m k)).isSome then k else default := by
simp [getKey!_alter h]
theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} (h : m.WF) {hc : k' ∈ Const.alter m k f} :
(Const.alter m k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
m.getKey k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.Const.getKey_alter
@[simp]
theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} (h : m.WF) {hc : k ∈ Const.alter m k f} :
(Const.alter m k f).getKey k hc = k := by
simp [getKey_alter h]
theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β}
(h : m.WF) : (Const.alter m k f).getKeyD k' fallback =
if k == k' then
if (f (Const.get? m k)).isSome then k else fallback
else
m.getKeyD k' fallback := by
simp_to_raw using Raw₀.Const.getKeyD_alter
theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
{f : Option β → Option β} (h : m.WF) :
(Const.alter m k f).getKeyD k fallback = if (f (Const.get? m k)).isSome then k else fallback := by
simp [getKeyD_alter h]
end Const
end Alter
section Modify
@[simp]
theorem isEmpty_modify [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).isEmpty = m.isEmpty := by
simp_to_raw using Raw₀.isEmpty_modify
@[simp]
theorem contains_modify [LawfulBEq α] {k k': α} {f : β k → β k} (h : m.WF) :
(m.modify k f).contains k' = m.contains k' := by
simp_to_raw using Raw₀.contains_modify
@[simp]
theorem mem_modify [LawfulBEq α] {k k': α} {f : β k → β k} (h : m.WF) :
k' ∈ m.modify k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_modify h]
@[simp]
theorem size_modify [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).size = m.size := by
simp_to_raw using Raw₀.size_modify
theorem get?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).get? k' =
if h : k == k' then
(cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f))
else
m.get? k' := by
simp_to_raw using Raw₀.get?_modify
@[simp]
theorem get?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).get? k = (m.get? k).map f := by
simp_to_raw using Raw₀.get?_modify_self
theorem get_modify [LawfulBEq α] {k k' : α} {f : β k → β k}
(h : m.WF) {hc : k' ∈ m.modify k f} :
(m.modify k f).get k' hc =
if heq : k == k' then
haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
cast (congrArg β (eq_of_beq heq)) <| f (m.get k h')
else
haveI h' : k' ∈ m := mem_modify h |>.mp hc
m.get k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.get_modify
@[simp]
theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) {hc : k ∈ m.modify k f} :
haveI h' : k ∈ m := mem_modify h |>.mp hc
(m.modify k f).get k hc = f (m.get k h') := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.get_modify_self
theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} (h : m.WF) :
(m.modify k f).get! k' =
if heq : k == k' then
m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!
else
m.get! k' := by
simp_to_raw using Raw₀.get!_modify
@[simp]
theorem get!_modify_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} (h : m.WF) :
(m.modify k f).get! k = ((m.get? k).map f).get! := by
simp_to_raw using Raw₀.get!_modify_self
theorem getD_modify [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} (h : m.WF) :
(m.modify k f).getD k' fallback =
if heq : k == k' then
m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
else
m.getD k' fallback := by
simp_to_raw using Raw₀.getD_modify
@[simp]
theorem getD_modify_self [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (h : m.WF) :
(m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback := by
simp_to_raw using Raw₀.getD_modify_self
theorem getKey?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).getKey? k' =
if k == k' then
if k ∈ m then some k else none
else
m.getKey? k' := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.getKey?_modify
theorem getKey?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).getKey? k = if k ∈ m then some k else none := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.getKey?_modify_self
theorem getKey!_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).getKey! k' =
if k == k' then
if k ∈ m then k else default
else
m.getKey! k' := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.getKey!_modify
theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).getKey! k = if k ∈ m then k else default := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.getKey!_modify_self
theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
(h : m.WF) {hc : k' ∈ m.modify k f} :
(m.modify k f).getKey k' hc =
if k == k' then
k
else
haveI h' : k' ∈ m := mem_modify h |>.mp hc
m.getKey k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.getKey_modify
@[simp]
theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
(h : m.WF) {hc : k ∈ m.modify k f} : (m.modify k f).getKey k hc = k := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.getKey_modify_self
theorem getKeyD_modify [LawfulBEq α] {k k' fallback : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).getKeyD k' fallback =
if k == k' then
if k ∈ m then k else fallback
else
m.getKeyD k' fallback := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.getKeyD_modify
theorem getKeyD_modify_self [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} (h : m.WF) :
(m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.getKeyD_modify_self
namespace Const
variable {β : Type v} {m : Raw α (fun _ => β)}
@[simp]
theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
(Const.modify m k f).isEmpty = m.isEmpty := by
simp_to_raw using Raw₀.Const.isEmpty_modify
@[simp]
theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) :
(Const.modify m k f).contains k' = m.contains k' := by
simp_to_raw using Raw₀.Const.contains_modify
@[simp]
theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) :
k' ∈ Const.modify m k f ↔ k' ∈ m := by
simp only [mem_iff_contains, contains_modify h]
@[simp]
theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
(Const.modify m k f).size = m.size := by
simp_to_raw using Raw₀.Const.size_modify
theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) :
Const.get? (Const.modify m k f) k' =
if k == k' then
Const.get? m k |>.map f
else
Const.get? m k' := by
simp_to_raw using Raw₀.Const.get?_modify
@[simp]
theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
Const.get? (Const.modify m k f) k = (Const.get? m k).map f := by
simp_to_raw using Raw₀.Const.get?_modify_self
theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
(h : m.WF) {hc : k' ∈ Const.modify m k f} :
Const.get (Const.modify m k f) k' hc =
if heq : k == k' then
haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
f (Const.get m k h')
else
haveI h' : k' ∈ m := mem_modify h |>.mp hc
Const.get m k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.Const.get_modify
@[simp]
theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
(h : m.WF) {hc : k ∈ Const.modify m k f} :
haveI h' : k ∈ m := mem_modify h |>.mp hc
Const.get (Const.modify m k f) k hc = f (Const.get m k h') := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.Const.get_modify_self
theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β}
(h : m.WF) : Const.get! (Const.modify m k f) k' =
if k == k' then
Const.get? m k |>.map f |>.get!
else
Const.get! m k' := by
simp_to_raw using Raw₀.Const.get!_modify
@[simp]
theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β}
(h : m.WF) : Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get! := by
simp_to_raw using Raw₀.Const.get!_modify_self
theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} (h : m.WF) :
Const.getD (Const.modify m k f) k' fallback =
if k == k' then
Const.get? m k |>.map f |>.getD fallback
else
Const.getD m k' fallback := by
simp_to_raw using Raw₀.Const.getD_modify
@[simp]
theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} (h : m.WF) :
Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback := by
simp_to_raw using Raw₀.Const.getD_modify_self
theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) :
(Const.modify m k f).getKey? k' =
if k == k' then
if k ∈ m then some k else none
else
m.getKey? k' := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKey?_modify
theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
(Const.modify m k f).getKey? k = if k ∈ m then some k else none := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKey?_modify_self
theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
(h : m.WF) : (Const.modify m k f).getKey! k' =
if k == k' then
if k ∈ m then k else default
else
m.getKey! k' := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKey!_modify
theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
(h : m.WF) : (Const.modify m k f).getKey! k = if k ∈ m then k else default := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKey!_modify_self
theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
(h : m.WF) {hc : k' ∈ Const.modify m k f} :
(Const.modify m k f).getKey k' hc =
if k == k' then
k
else
haveI h' : k' ∈ m := mem_modify h |>.mp hc
m.getKey k' h' := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.Const.getKey_modify
@[simp]
theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
(h : m.WF) {hc : k ∈ Const.modify m k f} : (Const.modify m k f).getKey k hc = k := by
simp only [mem_iff_contains] at hc
revert hc
simp_to_raw using Raw₀.Const.getKey_modify_self
theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} (h : m.WF) :
(Const.modify m k f).getKeyD k' fallback =
if k == k' then
if k ∈ m then k else fallback
else
m.getKeyD k' fallback := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKeyD_modify
theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β}
(h : m.WF) : (Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback := by
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKeyD_modify_self
end Const
end Modify
end Raw
end Std.DHashMap

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

@ -1269,4 +1269,337 @@ theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
end
section Alter
variable {m : HashMap α β}
theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α}
{f : Option β → Option β} :
(alter m k f).isEmpty = ((m.erase k).isEmpty && (f (get? m k)).isNone) :=
DHashMap.Const.isEmpty_alter_eq_isEmpty_erase
@[simp]
theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (get? m k)).isNone) :=
DHashMap.Const.isEmpty_alter
theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
(alter m k f).contains k' = if k == k' then (f (get? m k)).isSome else m.contains k' :=
DHashMap.Const.contains_alter
theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
k' ∈ alter m k f ↔ if k == k' then (f (get? m k)).isSome = true else k' ∈ m :=
DHashMap.Const.mem_alter
theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
(h : k == k') : k' ∈ alter m k f ↔ (f (get? m k)).isSome :=
DHashMap.Const.mem_alter_of_beq h
@[simp]
theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(alter m k f).contains k = (f (get? m k)).isSome :=
DHashMap.Const.contains_alter_self
@[simp]
theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
k ∈ alter m k f ↔ (f (get? m k)).isSome :=
DHashMap.Const.mem_alter_self
theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : (k == k') = false) :
(alter m k f).contains k' = m.contains k' :=
DHashMap.Const.contains_alter_of_beq_eq_false h
theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : (k == k') = false) : k' ∈ alter m k f ↔ k' ∈ m :=
DHashMap.Const.mem_alter_of_beq_eq_false h
theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} :
(alter m k f).size =
if m.contains k && (f (get? m k)).isNone then
m.size - 1
else if !m.contains k && (f (get? m k)).isSome then
m.size + 1
else
m.size :=
DHashMap.Const.size_alter
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∉ m) (h' : (f (get? m k)).isSome) :
(alter m k f).size = m.size + 1 :=
DHashMap.Const.size_alter_eq_add_one h h'
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∈ m) (h' : (f (get? m k)).isNone) :
(alter m k f).size = m.size - 1 :=
DHashMap.Const.size_alter_eq_sub_one h h'
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∉ m) (h' : (f (get? m k)).isNone) :
(alter m k f).size = m.size :=
DHashMap.Const.size_alter_eq_self_of_not_mem h h'
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
(h : k ∈ m) (h' : (f (get? m k)).isSome) :
(alter m k f).size = m.size :=
DHashMap.Const.size_alter_eq_self_of_mem h h'
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} :
(alter m k f).size ≤ m.size + 1 :=
DHashMap.Const.size_alter_le_size
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} :
m.size - 1 ≤ (alter m k f).size :=
DHashMap.Const.size_le_size_alter
theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
get? (alter m k f) k' =
if k == k' then
f (get? m k)
else
get? m k' :=
DHashMap.Const.get?_alter
@[simp]
theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
get? (alter m k f) k = f (get? m k) :=
DHashMap.Const.get?_alter_self
theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
{h : k' ∈ alter m k f} :
get (alter m k f) k' h =
if heq : k == k' then
haveI h' : (f (get? m k)).isSome := mem_alter_of_beq heq |>.mp h
f (get? m k) |>.get h'
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
get m k' h' :=
DHashMap.Const.get_alter
@[simp]
theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
{h : k ∈ alter m k f} :
haveI h' : (f (get? m k)).isSome := mem_alter_self.mp h
get (alter m k f) k h = (f (get? m k)).get h' :=
DHashMap.Const.get_alter_self
theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
{f : Option β → Option β} : get! (alter m k f) k' =
if k == k' then
f (get? m k) |>.get!
else
get! m k' :=
DHashMap.Const.get!_alter
@[simp]
theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
{f : Option β → Option β} : get! (alter m k f) k = (f (get? m k)).get! :=
DHashMap.Const.get!_alter_self
theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
{f : Option β → Option β} :
getD (alter m k f) k' fallback =
if k == k' then
f (get? m k) |>.getD fallback
else
getD m k' fallback :=
DHashMap.Const.getD_alter
@[simp]
theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β}
{f : Option β → Option β} :
getD (alter m k f) k fallback = (f (get? m k)).getD fallback :=
DHashMap.Const.getD_alter_self
theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
(alter m k f).getKey? k' =
if k == k' then
if (f (get? m k)).isSome then some k else none
else
m.getKey? k' :=
DHashMap.Const.getKey?_alter
theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(alter m k f).getKey? k = if (f (get? m k)).isSome then some k else none :=
DHashMap.Const.getKey?_alter_self
theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} : (alter m k f).getKey! k' =
if k == k' then
if (f (get? m k)).isSome then k else default
else
m.getKey! k' :=
DHashMap.Const.getKey!_alter
theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} :
(alter m k f).getKey! k = if (f (get? m k)).isSome then k else default :=
DHashMap.Const.getKey!_alter_self
theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} {h : k' ∈ alter m k f} :
(alter m k f).getKey k' h =
if heq : k == k' then
k
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
m.getKey k' h' :=
DHashMap.Const.getKey_alter
@[simp]
theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} {h : k ∈ alter m k f} :
(alter m k f).getKey k h = k :=
DHashMap.Const.getKey_alter_self
theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
{f : Option β → Option β} :
(alter m k f).getKeyD k' fallback =
if k == k' then
if (f (get? m k)).isSome then k else fallback
else
m.getKeyD k' fallback :=
DHashMap.Const.getKeyD_alter
theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
{f : Option β → Option β} :
(alter m k f).getKeyD k fallback = if (f (get? m k)).isSome then k else fallback :=
DHashMap.Const.getKeyD_alter_self
end Alter
section Modify
variable {m : HashMap α β}
@[simp]
theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(modify m k f).isEmpty = m.isEmpty :=
DHashMap.Const.isEmpty_modify
@[simp]
theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
(modify m k f).contains k' = m.contains k' :=
DHashMap.Const.contains_modify
@[simp]
theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
k' ∈ modify m k f ↔ k' ∈ m :=
DHashMap.Const.mem_modify
@[simp]
theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(modify m k f).size = m.size :=
DHashMap.Const.size_modify
theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
get? (modify m k f) k' =
if k == k' then
get? m k |>.map f
else
get? m k' :=
DHashMap.Const.get?_modify
@[simp]
theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
get? (modify m k f) k = (get? m k).map f :=
DHashMap.Const.get?_modify_self
theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
{h : k' ∈ modify m k f} :
get (modify m k f) k' h =
if heq : k == k' then
haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h
f (get m k h')
else
haveI h' : k' ∈ m := mem_modify.mp h
get m k' h' :=
DHashMap.Const.get_modify
@[simp]
theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
{h : k ∈ modify m k f} :
haveI h' : k ∈ m := mem_modify.mp h
get (modify m k f) k h = f (get m k h') :=
DHashMap.Const.get_modify_self
theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
get! (modify m k f) k' =
if k == k' then
get? m k |>.map f |>.get!
else
get! m k' :=
DHashMap.Const.get!_modify
@[simp]
theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
get! (modify m k f) k = ((get? m k).map f).get! :=
DHashMap.Const.get!_modify_self
theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
getD (modify m k f) k' fallback =
if k == k' then
get? m k |>.map f |>.getD fallback
else
getD m k' fallback :=
DHashMap.Const.getD_modify
@[simp]
theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} :
getD (modify m k f) k fallback = ((get? m k).map f).getD fallback :=
DHashMap.Const.getD_modify_self
theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
(modify m k f).getKey? k' =
if k == k' then
if k ∈ m then some k else none
else
m.getKey? k' :=
DHashMap.Const.getKey?_modify
theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(modify m k f).getKey? k = if k ∈ m then some k else none :=
DHashMap.Const.getKey?_modify_self
theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} :
(modify m k f).getKey! k' =
if k == k' then
if k ∈ m then k else default
else
m.getKey! k' :=
DHashMap.Const.getKey!_modify
theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} :
(modify m k f).getKey! k = if k ∈ m then k else default :=
DHashMap.Const.getKey!_modify_self
theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
{h : k' ∈ modify m k f} :
(modify m k f).getKey k' h =
if k == k' then
k
else
haveI h' : k' ∈ m := mem_modify.mp h
m.getKey k' h' :=
DHashMap.Const.getKey_modify
@[simp]
theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
{h : k ∈ modify m k f} : (modify m k f).getKey k h = k :=
DHashMap.Const.getKey_modify_self
theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} :
(modify m k f).getKeyD k' fallback =
if k == k' then
if k ∈ m then k else fallback
else
m.getKeyD k' fallback :=
DHashMap.Const.getKeyD_modify
theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
{f : β → β} : (modify m k f).getKeyD k fallback = if k ∈ m then k else fallback :=
DHashMap.Const.getKeyD_modify_self
end Modify
end Std.HashMap

8
src/Std/Data/HashMap/Raw.lean
View file

@ -181,6 +181,14 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
(l : List α) : Raw α Unit :=
⟨DHashMap.Raw.Const.unitOfList l⟩
@[inline, inherit_doc DHashMap.Raw.Const.alter] def alter [BEq α] [EquivBEq α] [Hashable α]
(m : Raw α β) (a : α) (f : Option β → Option β) : Raw α β :=
⟨DHashMap.Raw.Const.alter m.inner a f⟩
@[inline, inherit_doc DHashMap.Raw.Const.modify] def modify [BEq α] [EquivBEq α] [Hashable α]
(m : Raw α β) (a : α) (f : β → β) : Raw α β :=
⟨DHashMap.Raw.Const.modify m.inner a f⟩
section Unverified
/-! We currently do not provide lemmas for the functions below. -/

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

@ -1286,4 +1286,336 @@ theorem getD_unitOfList
end Raw
namespace Raw
variable [BEq α] [Hashable α] {m : Raw α β}
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α}
{f : Option β → Option β} (h : m.WF) :
(alter m k f).isEmpty = ((m.erase k).isEmpty && (f (get? m k)).isNone) :=
DHashMap.Raw.Const.isEmpty_alter_eq_isEmpty_erase h.out
@[simp]
theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF) :
(alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (get? m k)).isNone) :=
DHashMap.Raw.Const.isEmpty_alter h.out
theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
(h : m.WF) : (alter m k f).contains k' =
if k == k' then (f (get? m k)).isSome else m.contains k' :=
DHashMap.Raw.Const.contains_alter h.out
theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} (h : m.WF) :
k' ∈ alter m k f ↔ if k == k' then (f (get? m k)).isSome = true else k' ∈ m :=
DHashMap.Raw.Const.mem_alter h.out
theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
(h : m.WF) (he : k == k') : k' ∈ alter m k f ↔ (f (get? m k)).isSome :=
DHashMap.Raw.Const.mem_alter_of_beq h.out he
@[simp]
theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : (alter m k f).contains k = (f (get? m k)).isSome :=
DHashMap.Raw.Const.contains_alter_self h.out
@[simp]
theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : k ∈ alter m k f ↔ (f (get? m k)).isSome :=
DHashMap.Raw.Const.mem_alter_self h.out
theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : m.WF) (he : (k == k') = false) :
(alter m k f).contains k' = m.contains k' :=
DHashMap.Raw.Const.contains_alter_of_beq_eq_false h.out he
theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
{f : Option β → Option β} (h : m.WF) (he : (k == k') = false) : k' ∈ alter m k f ↔ k' ∈ m :=
DHashMap.Raw.Const.mem_alter_of_beq_eq_false h.out he
theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
(alter m k f).size =
if m.contains k && (f (get? m k)).isNone then
m.size - 1
else if !m.contains k && (f (get? m k)).isSome then
m.size + 1
else
m.size :=
DHashMap.Raw.Const.size_alter h.out
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF)
(h₁ : k ∉ m) (h₂ : (f (get? m k)).isSome) :
(alter m k f).size = m.size + 1 :=
DHashMap.Raw.Const.size_alter_eq_add_one h.out h₁ h₂
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF)
(h₁ : k ∈ m) (h₂ : (f (get? m k)).isNone) :
(alter m k f).size = m.size - 1 :=
DHashMap.Raw.Const.size_alter_eq_sub_one h.out h₁ h₂
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF)
(h₁ : k ∉ m) (h₂ : (f (get? m k)).isNone) : (alter m k f).size = m.size :=
DHashMap.Raw.Const.size_alter_eq_self_of_not_mem h.out h₁ h₂
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF)
(h₁ : k ∈ m) (h₂ : (f (get? m k)).isSome) : (alter m k f).size = m.size :=
DHashMap.Raw.Const.size_alter_eq_self_of_mem h.out h₁ h₂
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
(alter m k f).size ≤ m.size + 1 :=
DHashMap.Raw.Const.size_alter_le_size h.out
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
m.size - 1 ≤ (alter m k f).size :=
DHashMap.Raw.Const.size_le_size_alter h.out
theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) :
get? (alter m k f) k' =
if k == k' then
f (get? m k)
else
get? m k' :=
DHashMap.Raw.Const.get?_alter h.out
@[simp]
theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : get? (alter m k f) k = f (get? m k) :=
DHashMap.Raw.Const.get?_alter_self h.out
theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
(h : m.WF) {hc : k' ∈ alter m k f} :
get (alter m k f) k' hc =
if heq : k == k' then
haveI h' : (f (get? m k)).isSome := mem_alter_of_beq h heq |>.mp hc
f (get? m k) |>.get h'
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
get m k' h' :=
DHashMap.Raw.Const.get_alter h.out
@[simp]
theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) {hc : k ∈ alter m k f} :
haveI h' : (f (get? m k)).isSome := mem_alter_self h |>.mp hc
get (alter m k f) k hc = (f (get? m k)).get h' :=
DHashMap.Raw.Const.get_alter_self h.out
theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
{f : Option β → Option β} (h : m.WF) : get! (alter m k f) k' =
if k == k' then
f (get? m k) |>.get!
else
get! m k' :=
DHashMap.Raw.Const.get!_alter h.out
@[simp]
theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
{f : Option β → Option β} (h : m.WF) : get! (alter m k f) k = (f (get? m k)).get! :=
DHashMap.Raw.Const.get!_alter_self h.out
theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
{f : Option β → Option β} (h : m.WF) : getD (alter m k f) k' fallback =
if k == k' then
f (get? m k) |>.getD fallback
else
getD m k' fallback :=
DHashMap.Raw.Const.getD_alter h.out
@[simp]
theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β}
{f : Option β → Option β} (h : m.WF) :
getD (alter m k f) k fallback = (f (get? m k)).getD fallback :=
DHashMap.Raw.Const.getD_alter_self h.out
theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
(h : m.WF) : (alter m k f).getKey? k' =
if k == k' then
if (f (get? m k)).isSome then some k else none
else
m.getKey? k' :=
DHashMap.Raw.Const.getKey?_alter h.out
theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
(h : m.WF) : (alter m k f).getKey? k = if (f (get? m k)).isSome then some k else none :=
DHashMap.Raw.Const.getKey?_alter_self h.out
theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} (h : m.WF) : (alter m k f).getKey! k' =
if k == k' then
if (f (get? m k)).isSome then k else default
else
m.getKey! k' :=
DHashMap.Raw.Const.getKey!_alter h.out
theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} (h : m.WF) :
(alter m k f).getKey! k = if (f (get? m k)).isSome then k else default :=
DHashMap.Raw.Const.getKey!_alter_self h.out
theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
{f : Option β → Option β} (h : m.WF) {hc : k' ∈ alter m k f} :
(alter m k f).getKey k' hc =
if heq : k == k' then
k
else
haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
m.getKey k' h' :=
DHashMap.Raw.Const.getKey_alter h.out
@[simp]
theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
{f : Option β → Option β} (h : m.WF) {hc : k ∈ alter m k f} :
(alter m k f).getKey k hc = k :=
DHashMap.Raw.Const.getKey_alter_self h.out
theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β}
(h : m.WF) : (alter m k f).getKeyD k' fallback =
if k == k' then
if (f (get? m k)).isSome then k else fallback
else
m.getKeyD k' fallback :=
DHashMap.Raw.Const.getKeyD_alter h.out
theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
{f : Option β → Option β} (h : m.WF) :
(alter m k f).getKeyD k fallback = if (f (get? m k)).isSome then k else fallback :=
DHashMap.Raw.Const.getKeyD_alter_self h.out
end Alter
section Modify
@[simp]
theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
(modify m k f).isEmpty = m.isEmpty :=
DHashMap.Raw.Const.isEmpty_modify h.out
@[simp]
theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) :
(modify m k f).contains k' = m.contains k' :=
DHashMap.Raw.Const.contains_modify h.out
@[simp]
theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) :
k' ∈ modify m k f ↔ k' ∈ m :=
DHashMap.Raw.Const.mem_modify h.out
@[simp]
theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
(modify m k f).size = m.size :=
DHashMap.Raw.Const.size_modify h.out
theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) :
get? (modify m k f) k' =
if k == k' then
get? m k |>.map f
else
get? m k' :=
DHashMap.Raw.Const.get?_modify h.out
@[simp]
theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
get? (modify m k f) k = (get? m k).map f :=
DHashMap.Raw.Const.get?_modify_self h.out
theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
(h : m.WF) {hc : k' ∈ modify m k f} :
get (modify m k f) k' hc =
if heq : k == k' then
haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
f (get m k h')
else
haveI h' : k' ∈ m := mem_modify h |>.mp hc
get m k' h' :=
DHashMap.Raw.Const.get_modify h.out
@[simp]
theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF)
{hc : k ∈ modify m k f} :
haveI h' : k ∈ m := mem_modify h |>.mp hc
get (modify m k f) k hc = f (get m k h') :=
DHashMap.Raw.Const.get_modify_self h.out
theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β}
(h : m.WF) : get! (modify m k f) k' =
if k == k' then
get? m k |>.map f |>.get!
else
get! m k' :=
DHashMap.Raw.Const.get!_modify h.out
@[simp]
theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β}
(h : m.WF) : get! (modify m k f) k = ((get? m k).map f).get! :=
DHashMap.Raw.Const.get!_modify_self h.out
theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} (h : m.WF) :
getD (modify m k f) k' fallback =
if k == k' then
get? m k |>.map f |>.getD fallback
else
getD m k' fallback :=
DHashMap.Raw.Const.getD_modify h.out
@[simp]
theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} (h : m.WF) :
getD (modify m k f) k fallback = ((get? m k).map f).getD fallback :=
DHashMap.Raw.Const.getD_modify_self h.out
theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) :
(modify m k f).getKey? k' =
if k == k' then
if k ∈ m then some k else none
else
m.getKey? k' :=
DHashMap.Raw.Const.getKey?_modify h.out
theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
(modify m k f).getKey? k = if k ∈ m then some k else none :=
DHashMap.Raw.Const.getKey?_modify_self h.out
theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
(h : m.WF) : (modify m k f).getKey! k' =
if k == k' then
if k ∈ m then k else default
else
m.getKey! k' :=
DHashMap.Raw.Const.getKey!_modify h.out
theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
(h : m.WF) : (modify m k f).getKey! k = if k ∈ m then k else default :=
DHashMap.Raw.Const.getKey!_modify_self h.out
theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
(h : m.WF) {hc : k' ∈ modify m k f} :
(modify m k f).getKey k' hc =
if k == k' then
k
else
haveI h' : k' ∈ m := mem_modify h |>.mp hc
m.getKey k' h' :=
DHashMap.Raw.Const.getKey_modify h.out
@[simp]
theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
(h : m.WF) {hc : k ∈ modify m k f} : (modify m k f).getKey k hc = k :=
DHashMap.Raw.Const.getKey_modify_self h.out
theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} (h : m.WF) :
(modify m k f).getKeyD k' fallback =
if k == k' then
if k ∈ m then k else fallback
else
m.getKeyD k' fallback :=
DHashMap.Raw.Const.getKeyD_modify h.out
theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
{f : β → β} (h : m.WF) : (modify m k f).getKeyD k fallback = if k ∈ m then k else fallback :=
DHashMap.Raw.Const.getKeyD_modify_self h.out
end Modify
end Raw
end Std.HashMap