feat: verify insertMany method for adding lists to HashMaps #6211

monsterkrampe · 2024-11-25T13:04:44Z

This PR verifies the insertMany method on HashMaps for the special case of inserting lists.

src/Std/Data/DHashMap/Internal/RawLemmas.lean

src/Std/Data/DHashMap/Internal/Defs.lean

src/Std/Data/DHashMap/Internal/List/Associative.lean

leanprover-community-bot · 2024-11-25T13:30:55Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 935fcfb6ec84342163a86058856edcb1dca70ff4 --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-25 13:30:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a22f8fa6fef34a6798785785237c66cab173197 --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-26 15:53:38)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b378fe98a7877276b7dff70527b6c924e672c435 --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-27 15:47:35)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b378fe98a7877276b7dff70527b6c924e672c435 --onto 609346f5e03f3f2d559e7cc905f72e950c3ed8c4. (2024-11-28 08:49:25)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b378fe98a7877276b7dff70527b6c924e672c435 --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 10:41:50)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b378fe98a7877276b7dff70527b6c924e672c435 --onto 86f303774a7fbf38406ae13bd4b66f2753643a45. (2024-11-30 15:42:21)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b378fe98a7877276b7dff70527b6c924e672c435 --onto 27df5e968a675780a7bcd105a19774c0c59295d8. (2024-12-01 19:35:29)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b378fe98a7877276b7dff70527b6c924e672c435 --onto 3c5e612dc54733cd707becb929457d2f9d8ca6fd. (2024-12-02 15:27:36)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto 3c5e612dc54733cd707becb929457d2f9d8ca6fd. (2024-12-02 22:28:30)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto cb600ed9b436e4290b819b0529f8454490bffeb6. (2024-12-03 16:10:17)

src/Std/Data/DHashMap/Internal/List/Associative.lean

TwoFX · 2024-11-26T08:51:07Z

src/Std/Data/DHashMap/Basic.lean

@@ -285,6 +285,11 @@ but will later become a primitive operation.
  ⟨(Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
   (Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩

+@[inline, inherit_doc Raw.insertList] def insertList (m : DHashMap α β)


I don't think we should expose an insertList function as part of the public API. Here is how I imagined this working:

you define insertListₘ (for example using the definition you have)

you prove a theorem insertMany_eq_insertListₘ in Model.lean which rewrites insertMany applied to a list directly to insertListₘ

in WF.lean, you prove theorems toListModel_insertListₘ, (wfImp_insertListₘ probably not needed) , toListModel_insertMany (which only applies to lists!)

all of the lemmas in Internal/RawLemmas.lean are stated in terms of insertMany but only apply if the input is a list.

I changed that. It remains open how to name the lemmas. I kept insertList for now in the name. Using just insertMany seems impractical in case someone verifies insertList for arrays, trees etc. insertMany_list seemed a bit long

Long lemma names aren't necessarily a problem (we have IDE autocomplete ;)), so insertMany_list seems like the correct name to me.

src/Std/Data/DHashMap/Internal/RawLemmas.lean

src/Std/Data/DHashMap/Internal/List/Associative.lean

src/Std/Data/DHashMap/Internal/RawLemmas.lean

…Raw0.insertList

TwoFX

Most of my comments focus on things like naming which make sense to get exactly right before copying the lemmas a bunch of times, because it is more fun to change a name two times compared to changing it eight times :)

src/Std/Data/DHashMap/Internal/Model.lean

TwoFX · 2024-12-02T16:18:42Z

src/Std/Data/DHashMap/Internal/WF.lean

@@ -706,6 +706,29 @@ theorem wfImp_filter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m
  rw [filter_eq_filterₘ]
  exact wfImp_filterₘ h

+/-! # `insertListₘ` -/
+theorem wfImp_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.insertListₘ l).1 := by


This line is very long. If you have opened the Lean 4 workspace correctly, you should see a ruler at 100 columns. Please reformat your lines to stay within 100 columns.

I have WordWrapper activated in my vs code and then the ruler isn't moved in the wrapped line, but thats probably an issue only affecting very few users. I can keep an eye on that.

If I'm understanding you correctly this only occurs if your editor window is less than 100 columns wide? If so, yes, I don't think many users do it that way :)

src/Std/Data/DHashMap/Internal/WF.lean

TwoFX · 2024-12-02T16:23:55Z

src/Std/Data/DHashMap/Internal/WF.lean

@@ -706,6 +706,29 @@ theorem wfImp_filter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m
  rw [filter_eq_filterₘ]
  exact wfImp_filterₘ h

+/-! # `insertListₘ` -/


Suggested change

/-! # `insertListₘ` -/

/-! # `insertListₘ` -/

(similar below)

TwoFX · 2024-12-02T16:24:07Z

src/Std/Data/DHashMap/Internal/WF.lean

+  apply ih (wfImp_insert h)
+  apply List.insertList_perm_of_perm_first
+  apply toListModel_insert h
+  apply (wfImp_insert h).distinct


Suggested change

apply (wfImp_insert h).distinct

apply (wfImp_insert h).distinct

src/Std/Data/DHashMap/Internal/RawLemmas.lean

TwoFX · 2024-12-02T16:53:56Z

src/Std/Data/DHashMap/Internal/RawLemmas.lean

+section
+variable {β: Type v} (m: Raw₀ α (fun _ => β))
+
+theorem get?_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]


Should this not be called Const.get?_insertMany_of_contains_eq_false?

This theorem appers twice for Const.get for general insertMany and for Const.get for Const.insertMany, which would collapse via this name. I introduced the const to differentiate between the normal get and this one, though I copied it also into the results in the Const namespace.

TwoFX · 2024-12-02T16:55:37Z

src/Std/Data/DHashMap/Internal/RawLemmas.lean

+    getKey (insertManyIfNewUnit m l).1 k' h' = k := by
+  simp_to_model using getKey_insertListIfNewUnit_mem
+
+theorem getKey_insertManyIfNewUnit_list_mem_both [EquivBEq α] [LawfulHashable α]


Let's avoid abbreviations as much as possible and derive theorem names as "mechanically" as possible. I would call this getKey_insertManyIfNewUnit_of_contains_of_contains. Note the of before hypotheses.

TwoFX · 2024-12-02T16:56:55Z

src/Std/Data/DHashMap/Internal/RawLemmas.lean

+theorem getKey_insertManyIfNewUnit_list_mem_both [EquivBEq α] [LawfulHashable α]
+    {l : List α} {k : α}
+    {distinct : l.Pairwise (fun a b => (a == b) = false)}
+    {mem : l.contains k} {mem' : m.contains k = true} {h'} (h : m.1.WF):


Here and in many other places, you should just write m.contains k instead of m.contains k = true when using a Prop statement.

TwoFX · 2024-12-02T16:58:07Z

src/Std/Data/DHashMap/Internal/RawLemmas.lean

+    getKeyD (insertManyIfNewUnit m l).1 k fallback = getKeyD m k fallback := by
+  simp_to_model using getKeyD_insertListIfNewUnit_mem_both
+
+theorem insertManyIfNewUnit_list_length [EquivBEq α] [LawfulHashable α]


We generally read function calls "outside-in", so the proper name here would be length_insertManyIfNewUnit.

src/Std/Data/DHashMap/Internal/RawLemmas.lean

TwoFX · 2024-12-03T10:40:01Z

src/Std/Data/DHashMap/Internal/RawLemmas.lean

+section
+variable {β: Type v} (m: Raw₀ α (fun _ => β))
+
+theorem get?_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)


Okay, I see the problem with naming these lemmas. I think the (admittedly slighly crazy) scheme we use for the naming here would be that the lemma lives in the namespace of the first thing that appears in the name and then other relevant namespaces are included in the theorem name as appropriate. So this lemma would be called Const.get?_insertMany_list_of_contains_eq_false and the lemma you're currently calling Const.get?_insertMany_list_of_contains_eq_false would be called Const.get?_constInsertMany_list_of_contains_eq_false. Luckily, it's unlikely that end users will need to interact with these lemmas directly.

src/Std/Data/DHashMap/Internal/WF.lean

monsterkrampe commented Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/RawLemmas.lean Outdated Show resolved Hide resolved

monsterkrampe commented Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/RawLemmas.lean Outdated Show resolved Hide resolved

kim-em reviewed Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/Defs.lean Outdated Show resolved Hide resolved

kim-em reviewed Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/Defs.lean Outdated Show resolved Hide resolved

kim-em reviewed Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/Defs.lean Outdated Show resolved Hide resolved

kim-em reviewed Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/List/Associative.lean Outdated Show resolved Hide resolved

kim-em reviewed Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/List/Associative.lean Outdated Show resolved Hide resolved

kim-em reviewed Nov 25, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/List/Associative.lean Outdated Show resolved Hide resolved

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 25, 2024

kim-em reviewed Nov 26, 2024

View reviewed changes

src/Std/Data/DHashMap/Internal/List/Associative.lean Outdated Show resolved Hide resolved

TwoFX self-assigned this Nov 26, 2024

TwoFX requested changes Nov 26, 2024

View reviewed changes

jt0202 and others added 17 commits November 27, 2024 15:35

Model function for insertManyList

05b86d2

Verified insertManyList_contains for Raw0

ea17bbb

verified InsertList together with insert/size

ed56c5e

Renamed List.insertMany to List.insertList and added Perm result for …

db8a642

…Raw0.insertList

Use simp_to_model for insertList_contains

2aecd5a

Add get_insertList result to internal hashmap

3845a2e

Try to show insertMany_eq_insertList

42d72e3

Add remarks from meeting

a1d965d

Added equality proof between insertMany & insertList by @TwoFX

83b4e10

Simplified size_insertList

ed9f63a

Added results for isEmpty

ceb23c9

Start get? verification

a9b4847

WIP: verification getValueCast?

da76a1d

Finished DistinctKeys for get?

9013992

Finish get verification

1d18281

Some formatting

f023e7f

Pull insertList up to DHashMap

fdd6bab

monsterkrampe and others added 5 commits November 27, 2024 15:35

Add results for getKey?_insertList

273a0d0

Add results for variants of getKey_insertList

be70b67

Multiple small changes

a5f7e12

Replace insertList with insertMany in lemmas

77bc339

Hotfix for build after rebase

cea3723

monsterkrampe force-pushed the hashMap-insertList branch from d58354d to cea3723 Compare November 27, 2024 15:20

monsterkrampe and others added 10 commits November 27, 2024 17:28

Split getKey? result into two cases

6f01fd3

Adjust remaining getKey results

c85b156

Remove obsolete auxiliary result

3a4c796

Use getKey?_of_perm for getKey?_insertList

0cb4f2a

Rework getValueCast? according to suggestion

a2d70af

Remove obsolete aux results; Fix colon spacing

4fd84f3

constant get for insertMany

8f3eaa2

Verify Const.insertMany

446e801

Verify insertManyIfNewUnit

49e4a9d

get results for insertManyIfNewUnit

8340caf

TwoFX reviewed Dec 2, 2024

View reviewed changes

jt0202 and others added 2 commits December 2, 2024 23:01

Style fixes

45e3bc0

Merge branch 'leanprover:master' into hashMap-insertList

7f4bc44

TwoFX reviewed Dec 3, 2024

View reviewed changes

monsterkrampe added 4 commits December 3, 2024 16:15

Adjust simp spacing

bddf6fb

Incorporate smaller remarks from PR

ae25818

Shorten List.pairwise statements

9bb3511

Fix two more small spacing issues

3266d6c

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: verify insertMany method for adding lists to HashMaps #6211

feat: verify insertMany method for adding lists to HashMaps #6211

monsterkrampe commented Nov 25, 2024

leanprover-community-bot commented Nov 25, 2024 •

edited

Loading

TwoFX Nov 26, 2024

jt0202 Nov 26, 2024

TwoFX Nov 27, 2024

TwoFX left a comment

TwoFX Dec 2, 2024

jt0202 Dec 2, 2024

TwoFX Dec 3, 2024

TwoFX Dec 2, 2024

TwoFX Dec 2, 2024

TwoFX Dec 2, 2024

jt0202 Dec 2, 2024

TwoFX Dec 2, 2024

TwoFX Dec 2, 2024

TwoFX Dec 2, 2024

TwoFX Dec 3, 2024

	apply (wfImp_insert h).distinct
	apply (wfImp_insert h).distinct

feat: verify insertMany method for adding lists to HashMaps #6211

Are you sure you want to change the base?

feat: verify insertMany method for adding lists to HashMaps #6211

Conversation

monsterkrampe commented Nov 25, 2024

leanprover-community-bot commented Nov 25, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

TwoFX left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

leanprover-community-bot commented Nov 25, 2024 •

edited

Loading