Skip to content

[Merged by Bors] - feat: port Data.Int.Cast.Basic#670

Closed
j-loreaux wants to merge 8 commits intomasterfrom
data.int.cast.basic
Closed

[Merged by Bors] - feat: port Data.Int.Cast.Basic#670
j-loreaux wants to merge 8 commits intomasterfrom
data.int.cast.basic

Conversation

@j-loreaux
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux commented Nov 21, 2022

mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Porting notes:

  1. Some lemmas were transferred from Data.Int.Cast.Defs in order to match mathlib3 (I accidentally put them in the wrong place when I had ported that file because those lemmas were already present in mathlib4.)
  2. The lemmas just mentioned have retained their simp attribute for the reason Gabriel mentioned on that PR ([Merged by Bors] - feat: port data.{nat, int}.cast.defs #641), even though that attribute isn't present on the mathlib3 version.
  3. The bit0 and bit1 lemmas have been marked as deprecated.
  4. There were many dubious translation errors, I believe primarily because of the difference in the way coercions are handled, so I have #aligned all of these with ₓ. I believe this is the correct thing to do, but confirmation would be nice.
  • The first commit is the raw mathport output
  • After getting the file to compile, I left one commit before I deleted the dubious translation warnings, so you can look at that to compare.

@j-loreaux j-loreaux added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Nov 21, 2022
@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Nov 21, 2022

@digama0 can you confirm for me that #align ...ₓ is the right thing to do in this situation?

digama0
digama0 reviewed Nov 21, 2022
View reviewed changes
@digama0
Copy link
Copy Markdown
Member

digama0 commented Nov 21, 2022

I use the convention that any #align ...ₓ should have a short comment after it identifying why it's a dubious translation, e.g. reordered implicits, mismatching universes, Int.div alignment. In this case, I take it it's the typeclass args on the function? The answer to your question is probably yes, but it would be good to document the reason.

gebner
gebner reviewed Nov 21, 2022
View reviewed changes
Mathlib/Data/Int/Cast/Basic.lean
@[simp, norm_cast]
theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
AddGroupWithOne.intCast_negSucc n
#align int.cast_neg_succ_of_nat Int.cast_negSuccₓ
Copy link
Copy Markdown
Member

@gebner gebner Nov 21, 2022

Choose a reason for hiding this comment

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

Suggested change
#align int.cast_neg_succ_of_nat Int.cast_negSuccₓ
#align int.cast_neg_succ_of_nat Int.cast_negSucc

We definitely want to translate these without the ₓ. The only reason this statement is different is because coe is gone now, but this lemma is the closest approximation we've got in Lean 4. I think the statement is even defeq to the Lean 3 version.

(Note sure about the precise semantics of #align foo Fooₓ so maybe the ₓ does what I want.)

Copy link
Copy Markdown
Contributor Author

@j-loreaux j-loreaux Nov 21, 2022

Choose a reason for hiding this comment

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

There is no ₓ that appears in the final translation. The ₓ is just a signal to mathport that the types don't match and it should use the type of Foo downstream instead of foo.

I think in this case the dubious translations are arising mostly (if not entirely) from the fact that the nightly on which this mathport output was based came from a mathlib4 before I had ported Data.{Nat, Int}.Cast.Defs. I will check again when the next nightly comes out to see if these are still marked as dubious.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 23, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 23, 2022
@j-loreaux
feat: port Data.Int.Cast.Basic (#670)
76b3234 
mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Porting notes:

1. Some lemmas were transferred from `Data.Int.Cast.Defs` in order to match mathlib3 (I accidentally put them in the wrong place when I had ported that file because those lemmas were already present in mathlib4.)
2. The lemmas just mentioned have retained their `simp` attribute for the reason Gabriel mentioned on that PR (#641), even though that attribute isn't present on the mathlib3 version.
3. The `bit0` and `bit1` lemmas have been marked as deprecated.
4. There were many dubious translation errors, I believe primarily because of the difference in the way coercions are handled, so I have `#align`ed all of these with `ₓ`. I believe this is the correct thing to do, but confirmation would be nice.
@bors
Copy link
Copy Markdown

bors bot commented Nov 23, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Int.Cast.Basic [Merged by Bors] - feat: port Data.Int.Cast.Basic Nov 23, 2022
@bors bors bot closed this Nov 23, 2022
@bors bors bot deleted the data.int.cast.basic branch November 23, 2022 03:20
@github-actions github-actions bot mentioned this pull request Nov 23, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 23, 2022
@eric-wieser
chore(*): add mathlibport comments (#17686)
4afb682 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* leanprover-community/mathlib4#643
* leanprover-community/mathlib4#646
* leanprover-community/mathlib4#648
* leanprover-community/mathlib4#649
* leanprover-community/mathlib4#651
* leanprover-community/mathlib4#655
* leanprover-community/mathlib4#656
* leanprover-community/mathlib4#657
* leanprover-community/mathlib4#661
* leanprover-community/mathlib4#670
* leanprover-community/mathlib4#671
* leanprover-community/mathlib4#672
* leanprover-community/mathlib4#686
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 23, 2022
chore(*): add mathlib4 synchronization comments (#17686)
1044429 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 24, 2022
chore(*): add mathlib4 synchronization comments (#17686)
fe771af 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.inj_surj`: leanprover-community/mathlib4#707
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.group.units`: leanprover-community/mathlib4#549
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `data.ulift`: leanprover-community/mathlib4#703
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 25, 2022
chore(*): add mathlib4 synchronization comments (#17686)
cb1d279 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.inj_surj`: leanprover-community/mathlib4#707
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.group.units`: leanprover-community/mathlib4#549
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.opposites`: leanprover-community/mathlib4#644
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `data.ulift`: leanprover-community/mathlib4#703
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gebner gebner gebner left review comments

@digama0 digama0 digama0 left review comments

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@j-loreaux @digama0 @kim-em @gebner