Skip to content

feat: add difference on DTreeMap/TreeMap/TreeSet #11407

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

Jump to bottom
Merged
merged 106 commits into from
Dec 1, 2025
Merged

feat: add difference on DTreeMap/TreeMap/TreeSet #11407

merged 106 commits into from
Dec 1, 2025
+2,385 −2

Conversation

@wkrozowski
Copy link
Contributor

@wkrozowski wkrozowski commented Nov 27, 2025

This PR adds the difference operation on DTreeMap/TreeMap/TreeSet and proves several lemmas about it.

wkrozowski and others added 30 commits October 31, 2025 16:43
@wkrozowski
Initial getEntry work
f59fa7d
@wkrozowski
end of day push
5911740
@wkrozowski
push intermediate changes
e44545c
@wkrozowski
end of day push
cb7ac1d
@wkrozowski
chore: push lemma about getEntry
b54f683
@wkrozowski
foldl model
037c5b8
@wkrozowski
chore: intermediate work
cd12c0a
@wkrozowski
Massive lemma is done
2239c23
@wkrozowski
refactor
8b8f3bb
@wkrozowski
WF lemma is now working
02226fc
@wkrozowski
chore : the wf variant works
69669c6
@wkrozowski
chore add lemmas
439e242
@wkrozowski
more lemmas
a7c71fa
@wkrozowski
all get lemmas are done
725689c
@wkrozowski
getKey? lemmas are done
64a7891
@wkrozowski
Add const lemmas
9298608
@wkrozowski
Remove sorried proof
c7d1e13
@wkrozowski
push unfinished work
3bf6ad4
@wkrozowski
Prove length lemma
20bd320
@wkrozowski
push changes
8bf7034
@wkrozowski
Finish sublemma
db949a8
@wkrozowski
add wf predicate
8c035db
@wkrozowski
Add getEntry?/getEntry lemmas
ad46950
@wkrozowski
Add getEntry! and getEntryD
247fb58
@wkrozowski
fix naming
5b6274d
@wkrozowski
push what i have
8a80729
@wkrozowski
Cleanup old fold
804fba0
@wkrozowski
Add isEmpty lemma
5411489
@wkrozowski
add size lemma
86f2b74
@wkrozowski
fix simp_to_model
bae20a2
@wkrozowski wkrozowski marked this pull request as ready for review November 27, 2025 18:56
@wkrozowski wkrozowski requested a review from TwoFX as a code owner November 27, 2025 18:56
This was referenced Nov 27, 2025
Closed
Open
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 27, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6eeb215e8f1986cd1628f8e02d6c69e337db034e --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-27 19:59:58)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 27, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6eeb215e8f1986cd1628f8e02d6c69e337db034e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-27 20:00:00)

TwoFX
TwoFX approved these changes Dec 1, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, feel free to merge after addressing the naming nitpick.

@wkrozowski wkrozowski added this pull request to the merge queue Dec 1, 2025
Merged via the queue into leanprover:master with commit 2da5b52 Dec 1, 2025
13 of 14 checks passed
@wkrozowski wkrozowski deleted the wojciech/treemap_diff2 branch December 1, 2025 17:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

Assignees

No one assigned

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@wkrozowski @leanprover-community-bot @leanprover-bot @TwoFX