feat: hash map lemmas for filter, map and filterMap #7400

Rob23oba · 2025-03-08T20:06:22Z

This PR adds lemmas for the filter, map and filterMap functions of the hash map.

…into hashmap-filter-map

leanprover-community-bot · 2025-03-08T20:51:53Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9f8a859e7f354f026de7c910e17ce29e23678f9 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-08 20:51:52)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase da2d877019c3cc393c24b18919e4c7829bc3b9fe --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-09 07:27:37)
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-10 18:41:15) View Log
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-10 19:39:30) View Log
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-11 17:12:12) View Log
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-11 19:35:28) View Log
🟡 Mathlib branch lean-pr-testing-7400 build against this PR was cancelled. (2025-03-11 21:01:27) View Log
🟡 Mathlib branch lean-pr-testing-7400 build this PR didn't complete normally. (2025-03-11 21:45:47) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 137f5595204c48ec9442711f0e9e43228e40a07c --onto 8fc8e8ed19ef218022f5a94cbf5e472e3b777e44. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 12:33:12)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 137f5595204c48ec9442711f0e9e43228e40a07c --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 17:49:59)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07ee2eea21545fb055f1a8bdb848e2a419502c97 --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 20:58:56)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07ee2eea21545fb055f1a8bdb848e2a419502c97 --onto d5f01f2db1efd18034421ae2f40120d1c608f3c0. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-15 22:06:58)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5a5e83c26c2c74948e32e103e155fb57079e8e6c --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-17 18:22:15)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a5348f4bdc95c5a327817b5c62ee9f99ec8a0bfa --onto a97813e11f962bc422a03c30b7e29dd2eefb92c8. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-19 18:26:39)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c66cb00c0fbdc28636a0ebe7c0ac264e68ecd15b --onto a97813e11f962bc422a03c30b7e29dd2eefb92c8. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-20 20:18:48)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5fb990fcbd8d56e61e4276adcbe6deb19b5d7c64 --onto 060b2fe46fe728934744ee52271b92ab74cbd5b4. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-28 18:00:17)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 107eb845847456ef554a763b16d579284b11ac53 --onto 12a21e79c71880424321d62e60449863c504048a. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-31 10:49:08)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 107eb845847456ef554a763b16d579284b11ac53 --onto 2edfe2e9cffd55e3c79291628ae091b942291ec9. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-01 10:51:40)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 83067d67d65efe4818205ddb3f9b2ab824735b10 --onto 1ee7e1a9d8a67d1d8dcf6a17ac5c92bc2c7e0fac. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-03 15:10:01)
❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-04-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-06 13:06:43)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-04-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-07 09:18:08)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acd6b13d7692c2bf2314c09e406a178407d02743 --onto da55b2e19b6af219f43f3599f1a72151799eb524. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-07 15:52:51)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acd6b13d7692c2bf2314c09e406a178407d02743 --onto 0f2ede45d50d8fc8cc542517867a9d6a29f805a3. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-08 07:43:03)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acd6b13d7692c2bf2314c09e406a178407d02743 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-09 17:50:35)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0669a0470407e46d1ae26be8e201e214d5a91e74 --onto deef1c2739a331899b0e536312e65e9815059014. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-12 09:24:34)

TwoFX

Lemmas LGTM except for the two remaining comments, so feel free to get started on the user-facing versions.

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

jt0202 · 2025-04-12T19:59:36Z

src/Std/Data/DHashMap/Lemmas.lean

 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
    m.keys.Pairwise (fun a b => (a == b) = false) :=
  Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2

 @[simp]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
-    m.1.toList.map Sigma.fst = m.1.keys  :=
+    m.toList.map Sigma.fst = m.keys  :=


I also changed these lines as they seemed to be nonsense for me with m.1.keys

…into hashmap-filter-map

TwoFX

Looking very good, so this is mainly blocked on #7855.

TwoFX · 2025-04-14T08:02:42Z

src/Std/Data/HashSet/Lemmas.lean

+    (m.filter f).get! k = ((m.get? k).filter f).get! :=
+  HashMap.getKey!_filter_key
+
+theorem getD_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]


Unnecessary Inhabited instance?

TwoFX · 2025-04-14T08:24:10Z

src/Std/Data/HashMap/Lemmas.lean

@@ -1589,7 +1624,7 @@ theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option
        f m[k]? |>.get h'
      else
        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
-        m[k']'h' :=
+        m[(k')]'h' :=


Why is this suddenly needed?

Without the brackets Lean inteprets this term as containing the string ']' and because of that raises an error.

A space helps alternatively as well.

TwoFX · 2025-04-14T08:52:18Z

src/Std/Data/HashMap/Lemmas.lean

+      f (m.getKey k (mem_iff_isSome_getElem?.mpr (Option.isSome_of_eq_some h'))) x)).getD fallback :=
+  DHashMap.Const.getD_filter
+
+theorem getD_filter_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhabited β]


Unneeded Inhabited instance?

TwoFX · 2025-04-14T08:56:39Z

src/Std/Data/HashMap/Lemmas.lean

+
+theorem mem_of_mem_filter [EquivBEq α] [LawfulHashable α]
+    {f : α → β → Bool} {k : α} :
+    k ∈ (m.filter f) → k ∈ m :=


Suggested change

k ∈ (m.filter f) → k ∈ m :=

k ∈ m.filter f → k ∈ m :=

TwoFX · 2025-04-14T09:30:56Z

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

+  have h' := containsKey_of_mem h
+  induction l with
+  | nil => simp at h
+  | cons hd tl ih =>
+    rw [containsKey_cons] at h'
+    by_cases hd_x : hd.1 == x.1
+    · have : x = hd := by
+        simp only [List.mem_cons] at h
+        cases h with
+        | inl h => exact h
+        | inr h =>
+          rw [distinctKeys_cons_iff] at distinct
+          rw [containsKey_eq_false_iff] at distinct
+          have := And.right distinct
+          specialize this x h
+          simp [this] at hd_x
+      simp only [← this]
+      rw [getValue_cons]
+      simp
+    · rw [getValue_cons]
+      rw [distinctKeys_cons_iff] at distinct
+      simp only [hd_x, Bool.false_eq_true, ↓reduceDIte]
+      simp only [Bool.not_eq_true] at hd_x
+      have hd_x' : ¬ x = hd := by
+        false_or_by_contra
+        rename_i h'
+        simp [h'] at hd_x
+      simp only [List.mem_cons, hd_x', false_or] at h
+      exact ih h (And.left distinct) (containsKey_of_mem h)


Shorter way:

Suggested change

have h' := containsKey_of_mem h

induction l with

| nil => simp at h

| cons hd tl ih =>

rw [containsKey_cons] at h'

by_cases hd_x : hd.1 == x.1

· have : x = hd := by

simp only [List.mem_cons] at h

cases h with

| inl h => exact h

| inr h =>

rw [distinctKeys_cons_iff] at distinct

rw [containsKey_eq_false_iff] at distinct

have := And.right distinct

specialize this x h

simp [this] at hd_x

simp only [← this]

rw [getValue_cons]

simp

· rw [getValue_cons]

rw [distinctKeys_cons_iff] at distinct

simp only [hd_x, Bool.false_eq_true, ↓reduceDIte]

simp only [Bool.not_eq_true] at hd_x

have hd_x' : ¬ x = hd := by

false_or_by_contra

rename_i h'

simp [h'] at hd_x

simp only [List.mem_cons, hd_x', false_or] at h

exact ih h (And.left distinct) (containsKey_of_mem h)

induction h with

| head => rw [getValue_cons_of_beq]; simp

| @tail y l hmem ih =>

obtain (h|h) := containsKey_cons_eq_true.1 h'

· have := containsKey_of_mem hmem ▸ containsKey_congr h ▸ distinct.containsKey_eq_false

simp at this

· rw [getValue_cons_of_false, ih distinct.tail]

refine Bool.not_eq_true _ ▸ (fun hb => ?_)

simp [← containsKey_congr hb, distinct.containsKey_eq_false] at h

And similar below.

TwoFX · 2025-04-14T09:46:04Z

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

+    simp only [getKey, getKey?_eq_getEntry?, this] at h
+    exact h
+
+theorem perm_filter_self_iff [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool}


This could be split into a general lemma and an associative-specific one:

theorem perm_filter_self_iff {f : α → Bool} {l : List α} : (l.filter f).Perm l ↔ ∀ a ∈ l, f a = true := by rw (occs := [1]) [← (List.filter_append_perm f _).congr_right, ← List.append_nil (List.filter _ _), List.perm_append_left_iff] simp theorem perm_filter_self_iff_forall_containsKey [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} (hl : DistinctKeys l) : List.Perm (l.filter fun p => f p.1 p.2) l ↔ ∀ (a : α) (h : containsKey a l), (f a (getValueCast a l h)) = true := by rw [perm_filter_self_iff] constructor · intro h a ha exact h _ (getValueCast_mem ha) · intro h a ha exact getValueCast_of_mem ha hl ▸ h _ (containsKey_of_mem ha)

Rob23oba and others added 9 commits March 8, 2025 15:31

getEntry?_filterMap + option lemmas + getValueCast?_filterMap

dbabda4

getEntry?_filter

1646b60

actually getEntry?_filter and getEntry?_map

fb3af25

Length result for filterMap

09c3bb3

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

6c9bb1f

…into hashmap-filter-map

Lengths results for hashmaps and hashsets

cf64f9e

finish getValueCast?

7b3813d

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

0d68565

…into hashmap-filter-map

Rewrote length results without LawfulBEq

a030b42

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

jt0202 and others added 5 commits March 8, 2025 22:30

getKey results for map

96cf77b

take care of todo in simp_to_model

0a9ac13

Merge remote-tracking branch 'upstream/master' into hashmap-filter-map

09d3a00

minor cleanup

615d558

finish getKey_...

49185c1

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

Update lean-toolchain for testing leanprover/lean4#7400

47caae0

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

Update lean-toolchain for testing leanprover/lean4#7400

891f25d

finish getValueCast_...

34e7803

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 10, 2025

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

Trigger CI for leanprover/lean4#7400

e3f88d3

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

Trigger CI for leanprover/lean4#7400

0b0c2ae

finish getValue_...

71b7315

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

Trigger CI for leanprover/lean4#7400

6ef71b7

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

Trigger CI for leanprover/lean4#7400

aae4ba9

Filter length

97cc513

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

Trigger CI for leanprover/lean4#7400

7035a7a

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

Trigger CI for leanprover/lean4#7400

a2ed060

Further work on isEmpty & length

c8dac7b

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

Trigger CI for leanprover/lean4#7400

4ab7f29

user-facing filterMap lemmas for DHashMap

c50b18d

TwoFX reviewed Apr 11, 2025

View reviewed changes

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

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

jt0202 and others added 7 commits April 11, 2025 20:23

Merge branch 'master' into hashmap-filter-map

fc7c4e7

Fixes

2cf82c5

Fixes

31895b9

Fixes

a4e697e

Fixes

d698ec9

Suggestions from review

8644252

DHashMap lemmas

1dec5f2

jt0202 reviewed Apr 12, 2025

View reviewed changes

jt0202 and others added 12 commits April 12, 2025 23:18

Raw lemmas for DHashMap

2eee19c

Minor fixes & simp lemmas

f68a734

cleanup lemmas, add get?_map_of_getKey?_eq_some

fd16600

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

d81d9a3

…into hashmap-filter-map

minor style fix

cf79b8c

Raw lemmas for HashMap

c244b49

improve proof of getValue?_map, add pfilter

a1678d9

Raw lemmas for hash set

769b654

lemmas for HashMap + small instance adjustments

671ba63

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

a9a2c58

…into hashmap-filter-map

HashSet lemmas

0e42339

more additions for consistency

f8dff37

github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 13, 2025

Rob23oba added 2 commits April 13, 2025 21:32

more cleanup

b204acb

more correctly depict which functions have lemmas about them

be4c0c8

TwoFX reviewed Apr 14, 2025

View reviewed changes

TwoFX added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Apr 14, 2025

Suggestions from review

fbaf1e9

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: hash map lemmas for filter, map and filterMap #7400

feat: hash map lemmas for filter, map and filterMap #7400

Rob23oba commented Mar 8, 2025

leanprover-community-bot commented Mar 8, 2025 •

edited

Loading

TwoFX left a comment

jt0202 Apr 12, 2025

TwoFX left a comment

TwoFX Apr 14, 2025

TwoFX Apr 14, 2025

jt0202 Apr 14, 2025

jt0202 Apr 14, 2025

TwoFX Apr 14, 2025

TwoFX Apr 14, 2025

TwoFX Apr 14, 2025

TwoFX Apr 14, 2025

	k ∈ (m.filter f) → k ∈ m :=
	k ∈ m.filter f → k ∈ m :=

feat: hash map lemmas for filter, map and filterMap #7400

Are you sure you want to change the base?

feat: hash map lemmas for filter, map and filterMap #7400

Conversation

Rob23oba commented Mar 8, 2025

leanprover-community-bot commented Mar 8, 2025 • edited Loading

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

leanprover-community-bot commented Mar 8, 2025 •

edited

Loading