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)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto 019f8e175f9650b829aca8ee501f41c0a5d9076d. (2024-12-05 15:37:52)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto 8a3a806b1a8a1f0de8868c5bf96375b5dd6581fd. (2024-12-10 18:29:24)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto 8709ca35e9ddb977f7d050751e04981e2ab0d5c7. (2024-12-11 11:07:25)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto 48be424eaa2ae06972e9cfec4d355906b532204d. (2024-12-12 18:12:24)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto a8a160b09147c3225150703ac727eea6ee9a3b0e. (2024-12-15 19:38:27)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9d54c1f99363f42d1485f6b67f281a5985f684e --onto 6a839796fd537d14055e4a51a78c5272a1b52fb8. (2024-12-28 15:45:57)
✅ Mathlib branch lean-pr-testing-6211 has successfully built against this PR. (2024-12-28 18:08:08) View Log
✅ Mathlib branch lean-pr-testing-6211 has successfully built against this PR. (2025-01-05 18:03:16) View Log
✅ Mathlib branch lean-pr-testing-6211 has successfully built against this PR. (2025-01-05 20:19:35) View Log
✅ Mathlib branch lean-pr-testing-6211 has successfully built against this PR. (2025-01-05 21:40:27) View Log
✅ Mathlib branch lean-pr-testing-6211 has successfully built against this PR. (2025-01-05 22:37:08) View Log

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

src/Std/Data/DHashMap/Basic.lean

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

RawLemmas.lean is looking pretty good now, you should be able to start adding the user-facing lemmas after addressing these final two style remarks, but please don't forget about #6211 (comment) (which GitHub unhelpfully doesn't show on the PR page...)

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

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

TwoFX · 2025-01-02T15:25:27Z

src/Std/Data/DHashMap/Lemmas.lean

+
+theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
+    {l : List (α × β)} :
+    (ofList l).size ≤  l.length := by


Suggested change

(ofList l).size ≤ l.length := by

(ofList l).size ≤ l.length := by

TwoFX · 2025-01-02T15:26:18Z

src/Std/Data/DHashMap/Lemmas.lean

+  congr
+
+theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
+    (m.insertMany (⟨k, v⟩ :: l)) = ((m.insert k v).insertMany l) := by


Suggested change

(m.insertMany (⟨k, v⟩ :: l)) = ((m.insert k v).insertMany l) := by

m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l := by

TwoFX · 2025-01-02T15:26:52Z

src/Std/Data/DHashMap/Lemmas.lean

+  rw [Raw₀.insertMany_cons ⟨m.1, _⟩]
+  rfl
+
+theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]


This looks like a good simp lemma to me.

TwoFX · 2025-01-02T15:27:51Z

src/Std/Data/DHashMap/Lemmas.lean

+    (m.insertMany l).size ≤ m.size + l.length :=
+  Raw₀.size_insertMany_list_le ⟨m.1, _⟩  m.2
+
+theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α]


This is also a good simp lemma.

TwoFX · 2025-01-02T15:28:06Z

src/Std/Data/DHashMap/Lemmas.lean

+  apply Subtype.eq
+  simp [insertMany]
+  rw [Raw₀.Const.insertMany_cons ⟨m.1, _⟩]
+  rfl


Suggested change

rfl

rfl

TwoFX · 2025-01-02T15:54:14Z

src/Std/Data/DHashMap/Lemmas.lean

+  simp only [ofList]
+  rw [get?_insertMany_list_of_contains_eq_false h]
+  apply get?_emptyc


I don't love that you have multi-line proofs in DHashMap/Lemmas.lean and DHashMap/RawLemmas.lean, especially since the proofs are duplicated between the two files.

I think that you should prove things like

theorem size_insertMany_empty_list [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : ((Raw₀.empty : Raw₀ α β).insertMany l).1.1.size = l.length := by simp [size_insertMany_list _ Raw.WF.empty distinct]

in Internal/RawLemmas.lean and invoke that from DHashMap/Lemmas.lean and DHashMap/RawLemmas.lean.

TwoFX · 2025-01-02T15:56:24Z

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

@@ -224,6 +225,21 @@ def containsKey [BEq α] (a : α) : List ((a : α) × β a) → Bool
 @[simp] theorem containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
    containsKey a (⟨k, v⟩ :: l) = (k == a || containsKey a l) := rfl

+theorem containsKey_eq_false_iff [BEq α][PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :


You can move this below containsKey_eq_false_if_forall_mem_keys, then the proof is just
simp [containsKey_eq_false_iff_forall_mem_keys, keys_eq_map]

TwoFX · 2025-01-02T15:57:07Z

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

+theorem DistinctKeys.def [BEq α] {l : List ((a : α) × β a)} :
+    DistinctKeys l ↔ l.Pairwise (fun a b => (a.1 == b.1) = false) :=
+  ⟨fun h => by simpa [keys_eq_map, List.pairwise_map] using h.distinct,
+  fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩


Suggested change

fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩

fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩

TwoFX · 2025-01-02T15:57:13Z

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

+    · rw [getEntry?_cons_of_true hk]
+    · rw [getEntry?_cons_of_false, ih hl.tail hkv]
+      exact BEq.neq_of_neq_of_beq (containsKey_eq_false_iff.1 hl.containsKey_eq_false _ hkv) hk
+


Suggested change

TwoFX · 2025-01-02T15:58:45Z

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

+def Const.insertListIfNewUnitₘ [BEq α] [Hashable α](m : Raw₀ α (fun _ => Unit)) (l: List α): Raw₀ α (fun _ => Unit) :=
+  match l with
+  | .nil => m
+  | .cons hd tl => insertListIfNewUnitₘ (m.insertIfNew hd ()) tl


Suggested change

| .cons hd tl => insertListIfNewUnitₘ (m.insertIfNew hd ()) tl

| .cons hd tl => insertListIfNewUnitₘ (m.insertIfNew hd ()) tl

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 added 2 commits December 11, 2024 11:40

Fix formatting

0617166

Remove one theorem variant for Const

0f7fd51

TwoFX reviewed Dec 12, 2024

View reviewed changes

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

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

TwoFX reviewed Dec 12, 2024

View reviewed changes

jt0202 and others added 10 commits December 12, 2024 18:48

Style fix for Internal list

fe60013

Added size_insertMany_list_le & further style fixes

4b79e10

Moved results up to Raw

b233bc5

ofList lemmas introduced

41acb69

Small name correction

cd58f46

Added cons for ofList

e1234aa

Small style fixes

62f5a53

Further small fixes

ee522d3

Experimental: Pulled results up to DHashMap

57f188c

Merge branch 'master' into hashMap-insertList

2b5d6bf

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 28, 2024

Update lean-toolchain for testing leanprover/lean4#6211

b310f22

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 28, 2024

Update lean-toolchain for testing leanprover/lean4#6211

db3d311

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 28, 2024

TwoFX reviewed Jan 2, 2025

View reviewed changes

Small style fixes

340ac3a

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

41d30fb

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

c373aa7

Added predecessors for ofList into Raw0

7624c21

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

ceedd13

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

06dd947

Rework of DHashMap lemmas for ofList

37fd60f

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

3100951

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

19cb5bd

Style fixes

5f9dd86

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

04c0cfa

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025

Trigger CI for leanprover/lean4#6211

6a6c38a

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 left a comment

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

TwoFX Jan 2, 2025

	(ofList l).size ≤ l.length := by
	(ofList l).size ≤ l.length := by

	(m.insertMany (⟨k, v⟩ :: l)) = ((m.insert k v).insertMany l) := by
	m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l := by

	fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩
	fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩

	\| .cons hd tl => insertListIfNewUnitₘ (m.insertIfNew hd ()) tl
	\| .cons hd tl => insertListIfNewUnitₘ (m.insertIfNew hd ()) tl

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

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

leanprover-community-bot commented Nov 25, 2024 •

edited

Loading