[Merged by Bors] - fix(data/mv_polynomial): add missing decidable_eq arguments to lemmas
#18848
Conversation
This file contains 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
github-actions
bot
added
the
modifies-synchronized-file
eric-wieser
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
Vierkantor
approved these changes
May 10, 2023
|
|
||
| lemma degree_of_def [decidable_eq σ] (n : σ) (p : mv_polynomial σ R) : | ||
| p.degree_of n = p.degrees.count n := | ||
| by convert rfl |
There was a problem hiding this comment.
Isn't convert rfl just the same as congr?
Suggested change
| by convert rfl | |
| by congr |
There was a problem hiding this comment.
No, this doesn't work.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
…leanprover-community/mathlib into eric-wieser/mv_poly-basic-deceq
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
May 14, 2023
…as (#18848) This does not change the type of any definitions; the effect of this PR is to make the *statement* of the lemmas syntactically more general. To ensure this catches them all, this removes `open_locale classical` from the beginning of every file in `data/mv_polynomial` and `ring_theory/mv_polynomial`. For definitions which bake in a `classical.dec_eq` assumption, this adds a lemma proven by `convert rfl` that unfolds them to a version with an arbitrary `decidable_eq` instance, following a pattern established elsewhere. Unlike previous refactors of this style this doesn't seemed to have helped any downstream proofs much.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
decidable_eq arguments to lemmasdecidable_eq arguments to lemmas
1 task
eric-wieser
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 15, 2023
This is currently just a placeholder
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 21, 2023
I've been someone sloppy about forward-porting the exact mathport here; a lot of the `classical` additions result in the whole proof being indented, which IMO just adds noise to the diff. What's important is that: * `open Classical` is removed from all the same files * `[DecidableEq _]` is added in the same position to all the same lemmas. In theory mathport will detect if we mess this up, so it's not essential to catch this in review. The linter will tell us if it is added unnecessarily, and the build will fail if is not added someewhere it is needed; so only the argument order is at risk of being wrong. * The new `foo_def` lemmas are all added in `variables.lean`
qawbecrdtey
pushed a commit
to qawbecrdtey/greedoid-mathlib4
that referenced
this pull request
Jun 12, 2023
…mmunity#4007) I've been someone sloppy about forward-porting the exact mathport here; a lot of the `classical` additions result in the whole proof being indented, which IMO just adds noise to the diff. What's important is that: * `open Classical` is removed from all the same files * `[DecidableEq _]` is added in the same position to all the same lemmas. In theory mathport will detect if we mess this up, so it's not essential to catch this in review. The linter will tell us if it is added unnecessarily, and the build will fail if is not added someewhere it is needed; so only the argument order is at risk of being wrong. * The new `foo_def` lemmas are all added in `variables.lean`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This does not change the type of any definitions; the effect of this PR is to make the statement of the lemmas syntactically more general.
To ensure this catches them all, this removes
open_locale classicalfrom the beginning of every file indata/mv_polynomialandring_theory/mv_polynomial.For definitions which bake in a
classical.dec_eqassumption, this adds a lemma proven byconvert rflthat unfolds them to a version with an arbitrarydecidable_eqinstance, following a pattern established elsewhere.Unlike previous refactors of this style this doesn't seemed to have helped any downstream proofs much.
Unlike #18791, this does not:
data/polynomial; I will do that in a separate PRdecidable_eqto anydefs; this is a much bigger change and not something worth exploring before the port is done