[Merged by Bors] - feat: add reduce_mod_char! variant that searches through hypotheses#11478
Closed
Vierkantor wants to merge 2 commits intomasterfrom
Closed
[Merged by Bors] - feat: add reduce_mod_char! variant that searches through hypotheses#11478Vierkantor wants to merge 2 commits intomasterfrom
reduce_mod_char! variant that searches through hypotheses#11478Vierkantor wants to merge 2 commits intomasterfrom
Conversation
I won't have a lot of time to work on this PR until April, so please feel free to take it over before then. I initially wanted to use `synthInstance` rather than `findLocalDeclWithType?` but because `n` is not an outParam in `CharP R n`, the typeclass system won't work unless we know the value of `n` already. Perhaps `findLocalDeclWithType?` is cheap enough to make this part of standard `reduce_mod_char` behaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work
Member
|
How expensive is expensive? I know you said it saves some time in your test cases but I really wonder if we might want the expensive version to be the default, especially if the only users of reduce mod char are real users. |
Member
|
@Vierkantor this PR looks good to me! I'm fine merging with this behavior as optional for now, since maybe a proper performance comparison isn't on anyone's radar. It seems helpful to get the new behavior on master. Maybe we could make a tracking issue for changing the default. bors d+ |
Contributor
|
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
PR summary 1b64ccc5acImport changesNo significant changes to the import graph Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
Member
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 19, 2024
…#11478) I won't have a lot of time to work on this PR until April, so please feel free to take it over before then. I initially wanted to use `synthInstance` rather than `findLocalDeclWithType?` but because `n` is not an outParam in `CharP R n`, the typeclass system won't work unless we know the value of `n` already. Perhaps `findLocalDeclWithType?` is cheap enough to make this part of standard `reduce_mod_char` behaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
reduce_mod_char! variant that searches through hypothesesreduce_mod_char! variant that searches through hypotheses
AntoineChambert-Loir
pushed a commit
that referenced
this pull request
Jun 20, 2024
…#11478) I won't have a lot of time to work on this PR until April, so please feel free to take it over before then. I initially wanted to use `synthInstance` rather than `findLocalDeclWithType?` but because `n` is not an outParam in `CharP R n`, the typeclass system won't work unless we know the value of `n` already. Perhaps `findLocalDeclWithType?` is cheap enough to make this part of standard `reduce_mod_char` behaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
grunweg
pushed a commit
that referenced
this pull request
Jun 20, 2024
…#11478) I won't have a lot of time to work on this PR until April, so please feel free to take it over before then. I initially wanted to use `synthInstance` rather than `findLocalDeclWithType?` but because `n` is not an outParam in `CharP R n`, the typeclass system won't work unless we know the value of `n` already. Perhaps `findLocalDeclWithType?` is cheap enough to make this part of standard `reduce_mod_char` behaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
kbuzzard
pushed a commit
that referenced
this pull request
Jun 26, 2024
…#11478) I won't have a lot of time to work on this PR until April, so please feel free to take it over before then. I initially wanted to use `synthInstance` rather than `findLocalDeclWithType?` but because `n` is not an outParam in `CharP R n`, the typeclass system won't work unless we know the value of `n` already. Perhaps `findLocalDeclWithType?` is cheap enough to make this part of standard `reduce_mod_char` behaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
I won't have a lot of time to work on this PR until April, so please feel free to take it over before then.
I initially wanted to use
synthInstancerather thanfindLocalDeclWithType?but becausenis not an outParam inCharP R n, the typeclass system won't work unless we know the value ofnalready.Perhaps
findLocalDeclWithType?is cheap enough to make this part of standardreduce_mod_charbehaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated.Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work