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/fin): succ_above defn compares fin terms instead of values #3999
Conversation
Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
This change makes quadratic_reciprocity compile again, likely. The lemma could probably have norm_cast attr.
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 your proposed generalisation is worth trying out. If it makes things smoother, that's a sign that you should definitely go that way.
Co-authored by: Bryan Gin-ge Chen bryangingechen@gmail.com
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
…#3999) `fin.succ_above` is redefined to use a comparison between two `fin (n + 1)` instead of their coerced values in `nat`. This should delay any "escape" from `fin` into `nat` until necessary. Lemmas are added regarding `fin.succ_above`. Some proofs for existing lemmas reworked for new definition and simplified. Additionally, docstrings are added for related lemmas. New lemmas: Comparison after embedding: `succ_above_lt_ge` `succ_above_lt_gt` Injectivity lemmas: `succ_above_right_inj` `succ_above_right_injective` `succ_above_left_inj` `succ_above_left_injective` finset lemma: `fin.univ_succ_above` prod and sum lemmas: `fin.prod_univ_succ_above` Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…#3999) `fin.succ_above` is redefined to use a comparison between two `fin (n + 1)` instead of their coerced values in `nat`. This should delay any "escape" from `fin` into `nat` until necessary. Lemmas are added regarding `fin.succ_above`. Some proofs for existing lemmas reworked for new definition and simplified. Additionally, docstrings are added for related lemmas. New lemmas: Comparison after embedding: `succ_above_lt_ge` `succ_above_lt_gt` Injectivity lemmas: `succ_above_right_inj` `succ_above_right_injective` `succ_above_left_inj` `succ_above_left_injective` finset lemma: `fin.univ_succ_above` prod and sum lemmas: `fin.prod_univ_succ_above` Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
fin.succ_above
is redefined to use a comparison between twofin (n + 1)
instead of their coerced values innat
. This should delay any "escape" fromfin
intonat
until necessary. Lemmas are added regardingfin.succ_above
. Some proofs for existing lemmas reworked for new definition and simplified. Additionally, docstrings are added for related lemmas.New lemmas:
Comparison after embedding:
succ_above_lt_ge
succ_above_lt_gt
Injectivity lemmas:
succ_above_right_inj
succ_above_right_injective
succ_above_left_inj
succ_above_left_injective
finset lemma:
fin.univ_succ_above
prod and sum lemmas:
fin.prod_univ_succ_above
I'm working on some statements like
It seems that generalization might make the
fin.prod_*
lemmas generalizable over genericfinset.erase
prod
lemmas. Is it worth it to express them in that general way? In particular, due to howfin n
andfin (n + 1)
are different types, rearranging indices (that usefin
as the type) within those sums gets clunky. Hopefully the generalizations will ease that clunkiness.