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(Algebra/BigOperators/List): Use Std lemmas #11725
Conversation
I'm not convinced that introducing |
Note that the lemma statements haven't changed. It's just that there are a few extra lemmas stated using |
This PR/issue depends on: |
induction' l with a l ih | ||
· simp only [Nat.zero_mod, map_nil] | ||
· simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n) |
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.
Nat.add_mod
rewrites infinitely on its own. I'm not sure how this proof ever worked.
induction' l with a l ih | ||
· simp only [Nat.zero_mod, map_nil] | ||
· simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n) |
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.
Similarly, simping with Nat.mul_mod
is a terrible idea.
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.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
bors r+ |
* Make `Algebra.BigOperators.List.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Algebra.BigOperators.List.Basic` is algebra territory. * Make `Algebra.BigOperators.List.Basic` not depend on `Algebra.Divisibility.Basic`. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor. * As a consequence, move the divisibility and `MonoidWithZero` lemmas from `Algebra.BigOperators.List.Basic` to `Algebra.BigOperators.List.Lemmas`. * Move the content of `Algebra.BigOperators.List.Defs` to `Algebra.BigOperators.List.Basic` since no file imported the former without the latter and their imports are becoming very close after this PR. * Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Zip` not depend on `Algebra.BigOperators.List.Basic`. * As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat` -specific, keep a version of them stated using `Nat.sum`. * To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.
Pull request successfully merged into master. Build succeeded: |
* Make `Algebra.BigOperators.List.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Algebra.BigOperators.List.Basic` is algebra territory. * Make `Algebra.BigOperators.List.Basic` not depend on `Algebra.Divisibility.Basic`. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor. * As a consequence, move the divisibility and `MonoidWithZero` lemmas from `Algebra.BigOperators.List.Basic` to `Algebra.BigOperators.List.Lemmas`. * Move the content of `Algebra.BigOperators.List.Defs` to `Algebra.BigOperators.List.Basic` since no file imported the former without the latter and their imports are becoming very close after this PR. * Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Zip` not depend on `Algebra.BigOperators.List.Basic`. * As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat` -specific, keep a version of them stated using `Nat.sum`. * To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.
* Make `Algebra.BigOperators.List.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Algebra.BigOperators.List.Basic` is algebra territory. * Make `Algebra.BigOperators.List.Basic` not depend on `Algebra.Divisibility.Basic`. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor. * As a consequence, move the divisibility and `MonoidWithZero` lemmas from `Algebra.BigOperators.List.Basic` to `Algebra.BigOperators.List.Lemmas`. * Move the content of `Algebra.BigOperators.List.Defs` to `Algebra.BigOperators.List.Basic` since no file imported the former without the latter and their imports are becoming very close after this PR. * Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Zip` not depend on `Algebra.BigOperators.List.Basic`. * As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat` -specific, keep a version of them stated using `Nat.sum`. * To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.
* Make `Algebra.BigOperators.List.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Algebra.BigOperators.List.Basic` is algebra territory. * Make `Algebra.BigOperators.List.Basic` not depend on `Algebra.Divisibility.Basic`. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor. * As a consequence, move the divisibility and `MonoidWithZero` lemmas from `Algebra.BigOperators.List.Basic` to `Algebra.BigOperators.List.Lemmas`. * Move the content of `Algebra.BigOperators.List.Defs` to `Algebra.BigOperators.List.Basic` since no file imported the former without the latter and their imports are becoming very close after this PR. * Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Zip` not depend on `Algebra.BigOperators.List.Basic`. * As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat` -specific, keep a version of them stated using `Nat.sum`. * To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.
* Make `Algebra.BigOperators.List.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Algebra.BigOperators.List.Basic` is algebra territory. * Make `Algebra.BigOperators.List.Basic` not depend on `Algebra.Divisibility.Basic`. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor. * As a consequence, move the divisibility and `MonoidWithZero` lemmas from `Algebra.BigOperators.List.Basic` to `Algebra.BigOperators.List.Lemmas`. * Move the content of `Algebra.BigOperators.List.Defs` to `Algebra.BigOperators.List.Basic` since no file imported the former without the latter and their imports are becoming very close after this PR. * Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Zip` not depend on `Algebra.BigOperators.List.Basic`. * As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat` -specific, keep a version of them stated using `Nat.sum`. * To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.
Algebra.BigOperators.List.Basic
,Data.List.Chain
not depend onData.Nat.Order.Basic
by usingNat
-specific Std lemmas rather than general mathlib ones. I leave theData.Nat.Basic
import sinceAlgebra.BigOperators.List.Basic
is algebra territory.Algebra.BigOperators.List.Basic
not depend onAlgebra.Divisibility.Basic
. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor.MonoidWithZero
lemmas fromAlgebra.BigOperators.List.Basic
toAlgebra.BigOperators.List.Lemmas
.Algebra.BigOperators.List.Defs
toAlgebra.BigOperators.List.Basic
since no file imported the former without the latter and their imports are becoming very close after this PR.Data.List.Count
,Data.List.Dedup
,Data.List.ProdSigma
,Data.List.Zip
not depend onAlgebra.BigOperators.List.Basic
.Algebra.BigOperators.List.Basic
. For the lemmas that wereNat
-specific, keep a version of them stated usingNat.sum
.Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum
.