-
Notifications
You must be signed in to change notification settings - Fork 317
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.
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
[Merged by Bors] - chore(Data/Set): split Data/Set/Function #17091
Conversation
PR summary aa0f8babe1Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> The doc-module for |
Co-authored-by: Ruben Van de Velde <[email protected]> Co-authored-by: damiano <[email protected]>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can this be under Order
? Order.Monotone.Set
maybe?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not convinced by that name - a good chunk of the lemmas in Order.Monotone
involve Set
anyway, so it's not a good disambiguator. More specifically, what would be the deciding factor for a new lemma going in Order.Monotone.Set
as opposed to any one of the other files in Order.Monotone
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there's little to none, which surely is an argument for putting the files close together or even merge them?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not opposed to putting the files close together, I just don't think Order.Monotone.Set
is a good name for the new file!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Order.Monotone.SetFunction
? 🤷
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More importantly, the lemmas in this file use lemmas from Data.Set.Function
, which also creates an import cycle.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See
mathlib4/Mathlib/Order/Monotone/Basic.lean
Line 150 in 809c3fb
but right now this is not possible as `Set.preimage` is not defined yet, and importing it creates , for instance.
Sounds like the "right now" is very outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
the lemmas in this file use lemmas from
Data.Set.Function
Where? I don't see any lemma from Data.Set.Function
being used. I see definitions being used, but those could move to Data.Set.Operations
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unfortunately it is not just definitions that are used here, lemmas from Data.Set.Function
are used in the file. Furthermore, even if it were only definitions being used, it is out of scope of this PR to additionally move around definitions.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, but merging was merely a suggestion for how to put the material under Order.Monotone
. Please move this new file under Order.Monotone
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone. Also remove `Compl.decidableMem`, as it is already given in `decidableCompl` (instance search already finds it too) Co-authored-by: adomani <[email protected]>
Build failed (retrying...): |
Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone. Also remove `Compl.decidableMem`, as it is already given in `decidableCompl` (instance search already finds it too) Co-authored-by: adomani <[email protected]>
Pull request successfully merged into master. Build succeeded: |
Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone.
Also remove
Compl.decidableMem
, as it is already given indecidableCompl
(instance search already finds it too)