[Merged by Bors] - feat: port data.{nat, int}.cast.defs by j-loreaux · Pull Request #641 · leanprover-community/mathlib4

j-loreaux · 2022-11-18T06:42:57Z

mathlib3 SHA: bb168510ef455e9280a152e7f31673cabd3d7496

Porting notes for Mathlib.Data.Nat.Cast.Defs

I have moved AddMonoidWithOne and related lemmas from Mathlib.Algebra.GroupWithZero.Defs into this file. All but 3 of these were in this file in mathlib3, so this is the correct place. The extra 3 are new lemmas in Mathlib4, and I made a note to this effect.
mathport marked some translations as dubious because they used AddMonoidWithOne instead of NatCast because the latter didn't exist until this PR, so I just fixed them to use NatCast and #aligned (with no ₓ).
I need someone (e.g., @gebner) to rewrite the library note about coercions because I don't know enough.
I reimplemented Nat.binCast from scratch because we don't have Nat.binaryRec. The proof of Nat.binCast_eq can likely be improved quite a bit.
I marked Nat.cast_bit0 and Nat.cast_bit1 as deprecated since bit0 and bit1 are deprecated.
I added an instance of OfNat R n for n : ℕ when R has an AddMonoidWithOne instance. I think we want this in order to talk about literals as terms in R (e.g., 37 : R). This instance does not appear in mathlib3 and is new.
I kept the (lack of) simp attributes from mathlib3 for certain lemmas which were already ported to mathlib4. This caused some breakage which I fixed. I thought it was better to be consistent with the mathlib3 simp set. Per Gabriel's suggestion, I have kept these as simp lemmas.

Porting notes for Mathlib.Data.Int.Cast.Defs

This file already existed in Mathlib4, but it's contents corresponded to things in mathlib3's data.int.cast.basic, so I have moved the previous contents to Mathlib.Data.Int.Cast.Basic, hence the reason for the weird diff.
I have moved AddGroupWithOne and the rest of that material out of Mathlib.Algebra.GroupWithZero.Defs so these files are now independent and Mathlib.Data.Int.Cast.Defs I think is a faithful and complete translation of the mathlib3 file.

digama0 · 2022-11-18T06:50:18Z

This file has been modified in a more recent mathlib3 commit, namely #17477: bb168510ef455e9280a152e7f31673cabd3d7496, but the changes were minor and I have tried to incorporate them here.

In that case you should put this SHA at the top of the PR message (unless you are not sure you were effective in incorporating the changes?).

j-loreaux · 2022-11-18T06:54:17Z

Okay, I've changed it. It was only a rename of a single lemma.

Mathlib/Data/Nat/Cast/Defs.lean

gebner · 2022-11-18T18:43:54Z

I kept the (lack of) simp attributes from mathlib3 for certain lemmas which were already ported to mathlib4. This caused some breakage which I fixed. I thought it was better to be consistent with the mathlib3 simp set.

I think we should keep the @[simp] here for now. It's different in mathlib3 because of a recent PR: leanprover-community/mathlib3#17048

However, that PR is going to be very ugly to port to Lean 4, since we no longer have a coe constant.

This reverts commit 698f6ec.

j-loreaux · 2022-11-18T20:54:57Z

I have reinstated the simp attribute on these lemmas.

j-loreaux · 2022-11-18T22:35:29Z

Note in case you already looked at this PR and didn't read the updated description: I have added a port of data.int.cast.defs into this PR.

kim-em · 2022-11-20T00:08:56Z

bors merge

@gebner

mathlib3 SHA: bb168510ef455e9280a152e7f31673cabd3d7496 Porting notes for `Mathlib.Data.Nat.Cast.Defs` 1. I have moved `AddMonoidWithOne` and related lemmas from `Mathlib.Algebra.GroupWithZero.Defs` into this file. All but 3 of these were in this file in mathlib3, so this is the correct place. The extra 3 are new lemmas in Mathlib4, and I made a note to this effect. 2. mathport marked some translations as dubious because they used `AddMonoidWithOne` instead of `NatCast` because the latter didn't exist until this PR, so I just fixed them to use `NatCast` and `#align`ed (with no `ₓ`). 3. I need someone (e.g., @gebner) to rewrite the library note about coercions because I don't know enough. 4. I reimplemented `Nat.binCast` from scratch because we don't have `Nat.binaryRec`. The proof of `Nat.binCast_eq` can likely be improved quite a bit. 5. I marked `Nat.cast_bit0` and `Nat.cast_bit1` as deprecated since `bit0` and `bit1` are deprecated. 6. I added an instance of `OfNat R n` for `n : ℕ` when `R` has an `AddMonoidWithOne` instance. I think we want this in order to talk about literals as terms in `R` (e.g., `37 : R`). This instance does not appear in mathlib3 and is new. 7. ~~I kept the (lack of) `simp` attributes from mathlib3 for certain lemmas which were already ported to mathlib4. This caused some breakage which I fixed. I thought it was better to be consistent with the mathlib3 `simp` set.~~ Per Gabriel's suggestion, I have kept these as `simp` lemmas. Porting notes for `Mathlib.Data.Int.Cast.Defs` 1. This file already existed in Mathlib4, but it's contents corresponded to things in mathlib3's `data.int.cast.basic`, so I have moved the previous contents to `Mathlib.Data.Int.Cast.Basic`, hence the reason for the weird diff. 2. I have moved `AddGroupWithOne` and the rest of that material out of `Mathlib.Algebra.GroupWithZero.Defs` so these files are now independent and `Mathlib.Data.Int.Cast.Defs` I think is a faithful and complete translation of the mathlib3 file. Co-authored-by: Gabriel Ebner <gebner@gebner.org>

bors · 2022-11-20T00:14:50Z

Build failed:

Build

gebner · 2022-11-20T00:16:58Z

bors merge

@gebner

mathlib3 SHA: bb168510ef455e9280a152e7f31673cabd3d7496 Porting notes for `Mathlib.Data.Nat.Cast.Defs` 1. I have moved `AddMonoidWithOne` and related lemmas from `Mathlib.Algebra.GroupWithZero.Defs` into this file. All but 3 of these were in this file in mathlib3, so this is the correct place. The extra 3 are new lemmas in Mathlib4, and I made a note to this effect. 2. mathport marked some translations as dubious because they used `AddMonoidWithOne` instead of `NatCast` because the latter didn't exist until this PR, so I just fixed them to use `NatCast` and `#align`ed (with no `ₓ`). 3. I need someone (e.g., @gebner) to rewrite the library note about coercions because I don't know enough. 4. I reimplemented `Nat.binCast` from scratch because we don't have `Nat.binaryRec`. The proof of `Nat.binCast_eq` can likely be improved quite a bit. 5. I marked `Nat.cast_bit0` and `Nat.cast_bit1` as deprecated since `bit0` and `bit1` are deprecated. 6. I added an instance of `OfNat R n` for `n : ℕ` when `R` has an `AddMonoidWithOne` instance. I think we want this in order to talk about literals as terms in `R` (e.g., `37 : R`). This instance does not appear in mathlib3 and is new. 7. ~~I kept the (lack of) `simp` attributes from mathlib3 for certain lemmas which were already ported to mathlib4. This caused some breakage which I fixed. I thought it was better to be consistent with the mathlib3 `simp` set.~~ Per Gabriel's suggestion, I have kept these as `simp` lemmas. Porting notes for `Mathlib.Data.Int.Cast.Defs` 1. This file already existed in Mathlib4, but it's contents corresponded to things in mathlib3's `data.int.cast.basic`, so I have moved the previous contents to `Mathlib.Data.Int.Cast.Basic`, hence the reason for the weird diff. 2. I have moved `AddGroupWithOne` and the rest of that material out of `Mathlib.Algebra.GroupWithZero.Defs` so these files are now independent and `Mathlib.Data.Int.Cast.Defs` I think is a faithful and complete translation of the mathlib3 file. Co-authored-by: Gabriel Ebner <gebner@gebner.org>

bors · 2022-11-20T00:23:36Z

Pull request successfully merged into master.

Build succeeded:

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#563 * leanprover-community/mathlib4#608 * leanprover-community/mathlib4#627 * leanprover-community/mathlib4#638 * leanprover-community/mathlib4#641 * leanprover-community/mathlib4#645 * leanprover-community/mathlib4#650

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.

j-loreaux added 4 commits November 17, 2022 23:50

Port data.nat.cast.defs

c36c9ff

fix breakage due to simp set changes

698f6ec

add docstring

51abcf4

add import

bd180f5

j-loreaux added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Nov 18, 2022

j-loreaux mentioned this pull request Nov 18, 2022

[Merged by Bors] - feat: port remaining missing Algebra.GroupWithZero.Defs #563

Closed

kim-em reviewed Nov 18, 2022

View reviewed changes

Mathlib/Data/Nat/Cast/Defs.lean Outdated Show resolved Hide resolved

kim-em requested a review from gebner November 18, 2022 10:16

Move Nat.AtLeastTwo earlier in the file.

4824c40

j-loreaux added 3 commits November 18, 2022 14:48

reapply simp attribute

007c673

Revert "fix breakage due to simp set changes"

7871670

This reverts commit 698f6ec.

fix

261b4f7

j-loreaux added 2 commits November 18, 2022 15:45

port data.int.cast.defs

36bbdd9

add to import list

daab3bb

j-loreaux changed the title ~~feat: port data.nat.cast.defs~~ feat: port data.{nat, int}.cast.defs Nov 18, 2022

appease linter?

6417536

j-loreaux and others added 3 commits November 18, 2022 16:41

alphabetize much?

c8aab54

oops, fix a few things

53afda5

Update library note.

2f2e614

Fix.

45b3b7d

bors bot changed the title ~~feat: port data.{nat, int}.cast.defs~~ [Merged by Bors] - feat: port data.{nat, int}.cast.defs Nov 20, 2022

bors bot closed this Nov 20, 2022

bors bot deleted the j-loreaux/data.nat.cast.defs branch November 20, 2022 00:23

github-actions bot mentioned this pull request Nov 20, 2022

[Merged by Bors] - chore(*): add mathlibport comments leanprover-community/mathlib3#17642

Closed

j-loreaux mentioned this pull request Nov 21, 2022

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

Closed

github-actions bot mentioned this pull request Dec 19, 2022

[Merged by Bors] - chore(*): add mathlib4 synchronization comments leanprover-community/mathlib3#17979

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: port data.{nat, int}.cast.defs#641

[Merged by Bors] - feat: port data.{nat, int}.cast.defs#641
j-loreaux wants to merge 15 commits intomasterfrom
j-loreaux/data.nat.cast.defs

j-loreaux commented Nov 18, 2022 •

edited

Loading

Uh oh!

digama0 commented Nov 18, 2022

Uh oh!

j-loreaux commented Nov 18, 2022

Uh oh!

Uh oh!

gebner commented Nov 18, 2022

Uh oh!

j-loreaux commented Nov 18, 2022

Uh oh!

j-loreaux commented Nov 18, 2022

Uh oh!

kim-em commented Nov 20, 2022

Uh oh!

bors bot commented Nov 20, 2022

Uh oh!

gebner commented Nov 20, 2022

Uh oh!

bors bot commented Nov 20, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

j-loreaux commented Nov 18, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

digama0 commented Nov 18, 2022

Uh oh!

j-loreaux commented Nov 18, 2022

Uh oh!

Uh oh!

gebner commented Nov 18, 2022

Uh oh!

j-loreaux commented Nov 18, 2022

Uh oh!

j-loreaux commented Nov 18, 2022

Uh oh!

kim-em commented Nov 20, 2022

Uh oh!

bors bot commented Nov 20, 2022

Uh oh!

gebner commented Nov 20, 2022

Uh oh!

bors bot commented Nov 20, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

j-loreaux commented Nov 18, 2022 •

edited

Loading