This repository was archived by the owner on Jul 24, 2024. It is now read-only.
[Merged by Bors] - fix(data/mv_polynomial): add missing decidable_eq arguments to lemmas#18848
Closed
eric-wieser wants to merge 11 commits intomasterfrom
Closed
[Merged by Bors] - fix(data/mv_polynomial): add missing decidable_eq arguments to lemmas#18848eric-wieser wants to merge 11 commits intomasterfrom
decidable_eq arguments to lemmas#18848eric-wieser wants to merge 11 commits intomasterfrom
Conversation
Vierkantor
approved these changes
May 10, 2023
Collaborator
Vierkantor
left a comment
There was a problem hiding this comment.
Thank you for taking care of this! It touches quite a few files so let's get this merged quickly.
bors d+
|
|
||
| lemma degree_of_def [decidable_eq σ] (n : σ) (p : mv_polynomial σ R) : | ||
| p.degree_of n = p.degrees.count n := | ||
| by convert rfl |
Collaborator
There was a problem hiding this comment.
Isn't convert rfl just the same as congr?
Suggested change
| by convert rfl | |
| by congr |
Member
Author
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
Member
Author
|
bors 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. |
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`
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
2 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.
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