Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: remove bif from hash map lemmas #4791

Merged
merged 1 commit into from
Jul 22, 2024
Merged

chore: remove bif from hash map lemmas #4791

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 59 additions & 57 deletions src/Std/Data/DHashMap/Internal/List/Associative.lean
View file
Open in desktop

Large diffs are not rendered by default.

30 changes: 15 additions & 15 deletions src/Std/Data/DHashMap/Internal/RawLemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by
simp [Raw.isEmpty]

theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by
(m.insert k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by
simp_to_model using List.length_insertEntry

theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
Expand All @@ -169,7 +169,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α}
simp_to_model using List.containsKey_of_containsKey_eraseKey

theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).1.size = bif m.contains k then m.1.size - 1 else m.1.size := by
(m.erase k).1.size = if m.contains k then m.1.size - 1 else m.1.size := by
simp_to_model using List.length_eraseKey

theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} :
Expand Down Expand Up @@ -215,7 +215,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a
simp_to_model using List.getValueCast?_eq_none

theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = bif k == a then none else m.get? a := by
(m.erase k).get? a = if k == a then none else m.get? a := by
simp_to_model using List.getValueCast?_eraseKey

theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by
Expand All @@ -234,7 +234,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
simp_to_model; empty

theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insert k v) a = bif k == a then some v else get? m a := by
get? (m.insert k v) a = if k == a then some v else get? m a := by
simp_to_model using List.getValue?_insertEntry

theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
Expand All @@ -250,7 +250,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} :
simp_to_model using List.getValue?_eq_none.2

theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = bif k == a then none else get? m a := by
Const.get? (m.erase k) a = if k == a then none else get? m a := by
simp_to_model using List.getValue?_eraseKey

theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} :
Expand Down Expand Up @@ -340,7 +340,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
simp_to_model using List.getValueCast!_eq_default

theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = bif k == a then default else m.get! a := by
(m.erase k).get! a = if k == a then default else m.get! a := by
simp_to_model using List.getValueCast!_eraseKey

theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] :
Expand Down Expand Up @@ -372,7 +372,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simp_to_model; empty

theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insert k v) a = bif k == a then v else get! m a := by
get! (m.insert k v) a = if k == a then v else get! m a := by
simp_to_model using List.getValue!_insertEntry

theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
Expand All @@ -384,7 +384,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simp_to_model using List.getValue!_eq_default

theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = bif k == a then default else get! m a := by
get! (m.erase k) a = if k == a then default else get! m a := by
simp_to_model using List.getValue!_eraseKey

theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
Expand Down Expand Up @@ -435,7 +435,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
simp_to_model using List.getValueCastD_eq_fallback

theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
simp_to_model using List.getValueCastD_eraseKey

theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} :
Expand Down Expand Up @@ -471,7 +471,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simp_to_model; empty

theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by
simp_to_model using List.getValueD_insertEntry

theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
Expand All @@ -483,7 +483,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simp_to_model using List.getValueD_eq_fallback

theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
simp_to_model using List.getValueD_eraseKey

theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
Expand Down Expand Up @@ -539,7 +539,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a
simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'

theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by
(m.insertIfNew k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by
simp_to_model using List.length_insertEntryIfNew

theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
Expand Down Expand Up @@ -575,7 +575,7 @@ namespace Const
variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)

theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
get? (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then some v else get? m a := by
simp_to_model using List.getValue?_insertEntryIfNew

theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
Expand All @@ -585,12 +585,12 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
simp_to_model using List.getValue_insertEntryIfNew

theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
get! (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then v else get! m a := by
simp_to_model using List.getValue!_insertEntryIfNew

theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insertIfNew k v) a fallback =
bif k == a && !m.contains k then v else getD m a fallback := by
if k == a ∧ m.contains k = false then v else getD m a fallback := by
simp_to_model using List.getValueD_insertEntryIfNew

end Const
Expand Down
3 changes: 2 additions & 1 deletion src/Std/Data/DHashMap/Internal/WF.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -472,7 +472,8 @@ theorem wfImp_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable
buckets_hash_self := isHashSelf_eraseₘaux m a h
size_eq := by
rw [(toListModel_eraseₘaux m a h).length_eq, eraseₘaux, length_eraseKey,
← containsₘ_eq_containsKey h, h', cond_true, h.size_eq]
← containsₘ_eq_containsKey h, h']
simp [h.size_eq]
distinct := h.distinct.eraseKey.perm (toListModel_eraseₘaux m a h)

theorem toListModel_perm_eraseKey_of_containsₘ_eq_false [BEq α] [Hashable α] [EquivBEq α]
Expand Down
39 changes: 21 additions & 18 deletions src/Std/Data/DHashMap/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ theorem size_emptyc : (∅ : DHashMap α β).size = 0 :=
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl

theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).size = bif m.contains k then m.size else m.size + 1 :=
(m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
Raw₀.size_insert ⟨m.1, _⟩ m.2

theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
Expand Down Expand Up @@ -140,7 +140,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
simp

theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
(m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
Raw₀.size_erase _ m.2

theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
Expand Down Expand Up @@ -194,7 +194,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false

theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = bif k == a then none else m.get? a :=
(m.erase k).get? a = if k == a then none else m.get? a :=
Raw₀.get?_erase ⟨m.1, _⟩ m.2

@[simp]
Expand All @@ -218,7 +218,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
Raw₀.Const.get?_of_isEmpty ⟨m.1, _⟩ m.2

theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insert k v) a = bif k == a then some v else get? m a :=
get? (m.insert k v) a = if k == a then some v else get? m a :=
Raw₀.Const.get?_insert ⟨m.1, _⟩ m.2

@[simp]
Expand All @@ -238,7 +238,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m →
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false

theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = bif k == a then none else get? m a :=
Const.get? (m.erase k) a = if k == a then none else get? m a :=
Raw₀.Const.get?_erase ⟨m.1, _⟩ m.2

@[simp]
Expand Down Expand Up @@ -339,7 +339,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false

theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = bif k == a then default else m.get! a :=
(m.erase k).get! a = if k == a then default else m.get! a :=
Raw₀.get!_erase ⟨m.1, _⟩ m.2

@[simp]
Expand Down Expand Up @@ -381,7 +381,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
Raw₀.Const.get!_of_isEmpty ⟨m.1, _⟩ m.2

theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insert k v) a = bif k == a then v else get! m a :=
get! (m.insert k v) a = if k == a then v else get! m a :=
Raw₀.Const.get!_insert ⟨m.1, _⟩ m.2

@[simp]
Expand All @@ -398,7 +398,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false

theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = bif k == a then default else get! m a :=
get! (m.erase k) a = if k == a then default else get! m a :=
Raw₀.Const.get!_erase ⟨m.1, _⟩ m.2

@[simp]
Expand Down Expand Up @@ -465,7 +465,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false

theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
Raw₀.getD_erase ⟨m.1, _⟩ m.2

@[simp]
Expand Down Expand Up @@ -512,7 +512,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
Raw₀.Const.getD_of_isEmpty ⟨m.1, _⟩ m.2

theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback :=
getD (m.insert k v) a fallback = if k == a then v else getD m a fallback :=
Raw₀.Const.getD_insert ⟨m.1, _⟩ m.2

@[simp]
Expand All @@ -529,7 +529,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false

theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback :=
getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback :=
Raw₀.Const.getD_erase ⟨m.1, _⟩ m.2

@[simp]
Expand Down Expand Up @@ -611,7 +611,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'

theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 :=
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
Raw₀.size_insertIfNew ⟨m.1, _⟩ m.2

theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
Expand Down Expand Up @@ -647,8 +647,9 @@ namespace Const
variable {β : Type v} {m : DHashMap α (fun _ => β)}

theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a :=
Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2
get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2

theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insertIfNew k v) a h₁ =
Expand All @@ -657,13 +658,15 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
exact Raw₀.Const.get_insertIfNew ⟨m.1, _⟩ m.2

theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a :=
Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2
get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2

theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insertIfNew k v) a fallback =
bif k == a && !m.contains k then v else getD m a fallback :=
Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2
if k == a ∧ ¬k ∈ m then v else getD m a fallback := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2

end Const

Expand Down
Loading
Loading