Skip to content

feat: Data.Fin.Lemmas <- mathlib#173

Merged
digama0 merged 8 commits intomainfrom
fin_lemmas
Jul 6, 2023
Merged

feat: Data.Fin.Lemmas <- mathlib#173
digama0 merged 8 commits intomainfrom
fin_lemmas

Conversation

@digama0
Copy link
Copy Markdown
Member

@digama0 digama0 commented Jul 2, 2023

A WIP branch for porting Mathlib.Data.Fin.Basic to std.

@digama0 digama0 added the help wanted Extra attention is needed label Jul 2, 2023
@fgdorais
Copy link
Copy Markdown
Collaborator

fgdorais commented Jul 4, 2023

What kind of assistance do you require?

@digama0
Copy link
Copy Markdown
Member Author

digama0 commented Jul 4, 2023

It's basically unfinished work, I made it about 1/4 of the way through the file. The task here is to remove anything referencing mathlib notions like NeZero or Equiv and otherwise de-mathlibify all the other lemmas in the file. I haven't looked too carefully at the tail end of the file, maybe there is something that shouldn't be translated, but I would expect roughly the whole thing can move to std. This is relatively high priority since the mathlib std4 bump is blocked on this (in part).

@kim-em kim-em mentioned this pull request Jul 5, 2023
Closed
5 tasks
@digama0 digama0 changed the title [WIP] feat: Data.Fin.Lemmas <- mathlib feat: Data.Fin.Lemmas <- mathlib Jul 5, 2023
@digama0 digama0 marked this pull request as ready for review July 5, 2023 09:26
@digama0 digama0 removed the help wanted Extra attention is needed label Jul 5, 2023
fgdorais
fgdorais requested changes Jul 5, 2023
View reviewed changes
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Custom recursors work better when the hypotheses have predictable and meaningful names. This is to facilitate the use of the pattern induction x using foo with | hyp ... => ... I went through and recommended better names.

PS: Also consider using motive instead of C but I don't think that's essential.

@kmill
Copy link
Copy Markdown
Contributor

kmill commented Jul 5, 2023

The de-ord-embedding/iso-ification seems like it was done right, so here's a 👍 from me, though I only checked about 400-500 lines in detail

@digama0 digama0 merged commit cd11695 into main Jul 6, 2023
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 13, 2023
@kim-em @Komyyy
@Ruben-VandeVelde @digama0
chore: bump to nightly-2023-07-01 (#5409)
57e81ae 
- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 13, 2023
@kim-em @Komyyy
@Ruben-VandeVelde @digama0
chore: bump to nightly-2023-07-01 (#5409)
906f722 
- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Aug 14, 2023
@kim-em @Komyyy
@Ruben-VandeVelde @digama0
chore: bump to nightly-2023-07-01 (#5409)
f587581 
- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fgdorais fgdorais fgdorais approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@digama0 @fgdorais @kmill