-
Notifications
You must be signed in to change notification settings - Fork 251
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: bump to nightly-2023-07-15 #5992
Conversation
This will need a fix to Std4. Edit: DONE. |
This is currently failing in |
Now it is failing on the |
This PR/issue depends on:
|
Thanks! 🎉 |
Various adaptations to changes when `Fin` API was moved to Std. One notable change is that many lemmas are now stated in terms of `i ≠ 0` (for `i : Fin n`) rather then `i.1 ≠ 0`, and as a consequence many `Fin.vne_of_ne` applications have been added or removed, mostly removed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Canceled. |
Mathlib/Data/Fin/Basic.lean
Outdated
/-- `succAbove p i` embeds `Fin n` into `Fin (n + 1)` with a hole around `p`. -/ | ||
def succAbove (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1) := | ||
if i.1 < p.1 then castSucc i else succ i | ||
|
||
/-- `predAbove p i` embeds `i : Fin (n+1)` into `Fin n` by subtracting one if `p < i`. -/ | ||
def predAbove (p : Fin n) (i : Fin (n + 1)) : Fin n := | ||
if h : castSucc p < i then i.pred ((ne_iff_vne i 0).mpr (Nat.not_eq_zero_of_lt h)) | ||
else i.castLT (Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h) p.2) | ||
|
||
/-- `castPred` embeds `i : Fin (n + 2)` into `Fin (n + 1)` | ||
by lowering just `last (n + 1)` to `last n`. -/ | ||
def castPred (i : Fin (n + 2)) : Fin (n + 1) := predAbove (last n) i |
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.
Should we put these back to how they were in mathlib3 (ie, rename succAboveEmb
back to succAbove
)
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.
mathlib4/Mathlib/Data/Fin/Basic.lean
Lines 2032 to 2042 in f4e4287
theorem succAbove_aux (p : Fin (n + 1)) : | |
StrictMono fun i : Fin n => if (castSuccEmb i) < p then (castSuccEmb i) else i.succ := | |
(castSuccEmb : Fin n ↪o _).strictMono.ite (succEmbedding n).strictMono | |
(fun _ _ hij hj => lt_trans ((castSuccEmb : Fin n ↪o _).lt_iff_lt.2 hij) hj) fun i => | |
(castSuccEmb_lt_succ i).le | |
#align fin.succ_above_aux Fin.succAbove_aux | |
/-- `succAbove p i` embeds `Fin n` into `Fin (n + 1)` with a hole around `p`. -/ | |
def succAbove (p : Fin (n + 1)) : Fin n ↪o Fin (n + 1) := | |
OrderEmbedding.ofStrictMono _ p.succAbove_aux | |
#align fin.succ_above Fin.succAbove |
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 these were removed in this diff
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.
Ah, only succAbove
was changed; I moved the other lemmas back to their original (unbundled) homes.
bors d+ The |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Various adaptations to changes when `Fin` API was moved to Std. One notable change is that many lemmas are now stated in terms of `i ≠ 0` (for `i : Fin n`) rather then `i.1 ≠ 0`, and as a consequence many `Fin.vne_of_ne` applications have been added or removed, mostly removed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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. |
Various adaptations to changes when `Fin` API was moved to Std. One notable change is that many lemmas are now stated in terms of `i ≠ 0` (for `i : Fin n`) rather then `i.1 ≠ 0`, and as a consequence many `Fin.vne_of_ne` applications have been added or removed, mostly removed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Various adaptations to changes when `Fin` API was moved to Std. One notable change is that many lemmas are now stated in terms of `i ≠ 0` (for `i : Fin n`) rather then `i.1 ≠ 0`, and as a consequence many `Fin.vne_of_ne` applications have been added or removed, mostly removed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Various adaptations to changes when
Fin
API was moved to Std. One notable change is that many lemmas are now stated in terms ofi ≠ 0
(fori : Fin n
) rather theni.1 ≠ 0
, and as a consequence manyFin.vne_of_ne
applications have been added or removed, mostly removed.