Zulip Chat Archive

Stream: mathlib4

Topic: OfNat

Sky Wilshaw (Dec 04 2022 at 18:52):

I'm currently porting Algebra.Order.Monoid.WithZero. There are a few lemmas like

theorem zero_le_two [Preorder α] [One α] [AddZeroClass α] [ZeroLEOneClass α]
    [CovariantClass α α (· + ·) (· ≤ ·)] : (0 : α) ≤ 2 :=
  add_nonneg zero_le_one zero_le_one

Inserting the [OfNat α 2] assumption clears up the type error, but the proof doesn't type check because Lean doesn't know if the OfNat implementation of 2 agrees with 1 + 1. What's the correct Lean 4 way of fixing this? I heard some talk a while back about a Numeric typeclass or LawfulOfNat, but I can't see them in mathlib4 currently.

Gabriel Ebner (Dec 04 2022 at 20:45):

Yeah, numerals are only supported for structures extending AddMonoidWithOne. Separate One α and AddZeroClass α hypotheses won't do it anymore. One possibility would be to change [One α] [AddZeroClass α] to [AddMonoidWithOne α].

Gabriel Ebner (Dec 04 2022 at 20:46):

But really, I think that's a gratuitously general definition in mathlib3. My knee-jerk reaction is usually to specialize these to a sensible algebraic structure, i.e., ordered semirings. This doesn't seem to break much (I've just started the build): https://github.com/leanprover-community/mathlib/compare/zeroletwospec?expand=1

Yaël Dillies (Dec 04 2022 at 20:49):

@Yuyang Zhao literally just generalised those lemmas.

Gabriel Ebner (Dec 04 2022 at 21:02):

There's a couple of PRs in that direction, from what I can tell it began with #14510 (for zero_le_two and co.), then #17477 and #17465.

Gabriel Ebner (Dec 04 2022 at 21:08):

None of the PRs come with a good explanation what the generality is actually useful for. I fully share Floris' feelings in #14510:

I'm worried that every time we add a class like this, we do actually increase the compilation time (and timeout risk) of many files.
Does this class actually solve a problem, except proving that 0 <= 2 a couple times? [emphasis mine]

Yaël Dillies (Dec 04 2022 at 21:24):

I fully agree. There are a few more types that the lemmas apply to, but they are barely used afaict.

Patrick Massot (Dec 04 2022 at 21:30):

In my experience, #14510 only brought pain (through elaboration issues).

Sky Wilshaw (Dec 04 2022 at 22:39):

What would you recommend I do in my PR for mathlib4 then?

Sky Wilshaw (Dec 04 2022 at 22:40):

Perhaps the easiest thing to do is remove the lemmas for now, but add a TODO to come back to them later. This file is on the hot path towards algebra.order.field.defs, so I think it'd be preferable to merge something and fix it later.

Yuyang Zhao (Dec 05 2022 at 04:02):

I'll try to make a PR to solve this problem.

Kevin Buzzard (Dec 05 2022 at 07:17):

Why not just assume you have an AddMonoidWithOne and make a porting note? It's hard to imagine that this will cause problems down the line.

Yuyang Zhao (Dec 05 2022 at 08:42):

I made PR #17820 because zero_le_one_class seems should not be put in algebra.order.monoid.with_zero.defs

Yaël Dillies (Dec 05 2022 at 09:09):

Can't we just get rid of zero_le_one_class?

Scott Morrison (Dec 06 2022 at 02:47):

Gabriel Ebner said:

But really, I think that's a gratuitously general definition in mathlib3. My knee-jerk reaction is usually to specialize these to a sensible algebraic structure, i.e., ordered semirings. This doesn't seem to break much (I've just started the build): https://github.com/leanprover-community/mathlib/compare/zeroletwospec?expand=1

Let's merge this one. It has the great advantage that it makes life for Sky porting Algebra.Order.Monoid.WithZero.Defs strictly easier, as it is just moving content out of the way.

Sky Wilshaw (Dec 06 2022 at 11:08):

Thanks for your help, the PR mathlib4#851 is now building.

Scott Morrison (Dec 07 2022 at 00:38):

Okay, porting #17820 to mathlib4 was unpleasant (I am frankly embarrassed and disgusted that I wrote and used a lemma that says 3+1=4), but done in https://github.com/leanprover-community/mathlib4/pull/893. Hopefully thing means we can finally define an ordered ring.

These files aren't in mathlib3port yet, so they were just ported by hand.

Scott Morrison (Dec 07 2022 at 00:42):

@Moritz Doll just pinging you on this as you had claimed algebra.order.zero_le_one, which I've done in this file.

Moritz Doll (Dec 07 2022 at 00:43):

I saw that I had proofs for some of the stupidly obvious lemmas?

Scott Morrison (Dec 07 2022 at 00:45):

Did you have a PR? I didn't see anything. Please feel free to edit my PR directly (or comment / approve, etc)

Moritz Doll (Dec 07 2022 at 00:46):

mathlib4#664 and you closed it :joy:

lemma one_add_one [One α] [AddZeroClass α] : (1 : α) + 1 = (2 : ℕ).unaryCast := by
  change 1 + 1 = (0 + 1) + 1
  rw [zero_add 1]

theorem one_le_two [LE α] [One α] [AddZeroClass α] [ZeroLEOneClass α]
  [CovariantClass α α (· + ·) (· ≤ ·)] :
    (1 : α) ≤ (2 : ℕ).unaryCast := by
  rw [← add_zero 1, ← one_add_one]
  exact add_le_add_left zero_le_one _
#align one_le_two one_le_two

theorem one_le_two' [LE α] [One α] [AddZeroClass α] [ZeroLEOneClass α]
  [CovariantClass α α (swap (· + ·)) (· ≤ ·)] :
    (1 : α) ≤ (2 : ℕ).unaryCast := by
  rw [← zero_add 1, ← one_add_one]
  exact add_le_add_right zero_le_one _
#align one_le_two' one_le_two'

Moritz Doll (Dec 07 2022 at 00:47):

I think this was the part which did not come from mathport

Moritz Doll (Dec 07 2022 at 00:48):

I have to do informal math now, but I can take look at it in the evening

Yuyang Zhao (Dec 07 2022 at 00:51):

Scott Morrison said:

Okay, porting #17820 to mathlib4 was unpleasant (I am frankly embarrassed and disgusted that I wrote and used a lemma that says 3+1=4), but done in https://github.com/leanprover-community/mathlib4/pull/893. Hopefully thing means we can finally define an ordered ring.

These files aren't in mathlib3port yet, so they were just ported by hand.

Does the encoding of numerals in AddMonoidWithOne are not the same as lean3 numerals?

Moritz Doll (Dec 07 2022 at 00:52):

no, it is slightly different

Yuyang Zhao (Dec 07 2022 at 00:57):

oops

Scott Morrison (Dec 07 2022 at 00:59):

It's okay, we can clean it up later.

Heather Macbeth (Dec 08 2022 at 12:27):

There was some discussion upstream about reorganizing zero_le_one_class (possibly in fact reorganizing it out of existence). Where did this land? We currently have a discrepancy between
Lean 3 algebra/order/monoid/with_zero/defs and Lean 4 algebra/order/monoid/with_zero/defs, the former including zero_le_one_class instances and the latter not.

I hit this in mathlib4#903.

Yuyang Zhao (Dec 08 2022 at 13:49):

I think it's just because we merged mathlib4#851 before mathlib4#893.

Heather Macbeth (Dec 08 2022 at 15:00):

In that case, shouldn't there be an alert somewhere saying "this file has been modified since the last verified commit"? I wonder if something is broken in the tooling.

We have that

  1. Algebra/Order/Monoid/WithZero was ported in mathlib4#851 modelled on dad7ecf9a1feae63e6e49f07619b7087403fb8d4
  2. #17465 modified the file in mathlib3
  3. #17820 modified the file again in mathlib3
  4. mathlib4#851 was merged into mathlib4
  5. the file was marked in mathlib3 as frozen.

Heather Macbeth (Dec 08 2022 at 15:02):

The bot is supposed to check that the file hasn't been modified in mathlib3 since the porting basis commit, right?

Jireh Loreaux (Dec 08 2022 at 16:02):

There's no bot that checks for differences in files (so far, but I think there was talk about it), it has to be done manually, but the port status script should tell you which files have changes since the last commit at which they were verified

Heather Macbeth (Dec 08 2022 at 16:02):

The port status script is not complaining about this file, though!

Jireh Loreaux (Dec 08 2022 at 16:02):

Admittedly, this file doesn't show up on the port status script though.

Jireh Loreaux (Dec 08 2022 at 16:05):

Actually, it does, it's just not on @Johan Commelin's website. Johan, can you fix this problem?

Jireh Loreaux (Dec 08 2022 at 16:05):

Running port_status.py locally gave me: 

# The following files have been modified since the commit at which they were verified.
git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/combinatorics/quiver/subquiver.lean
git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/combinatorics/quiver/path.lean
git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/combinatorics/quiver/connected_component.lean
git diff 9b2660e1b25419042c8da10bf411aa3c67f14383..HEAD src/combinatorics/quiver/push.lean
git diff 8350c34a64b9bc3fc64335df8006bffcadc7baa6..HEAD src/combinatorics/quiver/basic.lean
git diff 8350c34a64b9bc3fc64335df8006bffcadc7baa6..HEAD src/category_theory/isomorphism.lean
git diff afad8e438d03f9d89da2914aa06cb4964ba87a18..HEAD src/category_theory/thin.lean
git diff 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904..HEAD src/category_theory/natural_isomorphism.lean
git diff 8350c34a64b9bc3fc64335df8006bffcadc7baa6..HEAD src/category_theory/natural_transformation.lean
git diff 8350c34a64b9bc3fc64335df8006bffcadc7baa6..HEAD src/category_theory/functor/category.lean
git diff afad8e438d03f9d89da2914aa06cb4964ba87a18..HEAD src/category_theory/functor/functorial.lean
git diff 8350c34a64b9bc3fc64335df8006bffcadc7baa6..HEAD src/category_theory/functor/basic.lean
git diff afad8e438d03f9d89da2914aa06cb4964ba87a18..HEAD src/category_theory/category/Rel.lean
git diff 8350c34a64b9bc3fc64335df8006bffcadc7baa6..HEAD src/category_theory/category/basic.lean
git diff a148d797a1094ab554ad4183a4ad6f130358ef64..HEAD src/algebra/ring/units.lean
git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/algebra/ring/regular.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/ring/divisibility.lean
git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/algebra/ring/basic.lean
git diff 9b2660e1b25419042c8da10bf411aa3c67f14383..HEAD src/algebra/group_power/basic.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/euclidean_domain/defs.lean
git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/hom/units.lean
git diff 8c53048add6ffacdda0b36c4917bfe37e209b0ba..HEAD src/algebra/hom/group.lean
git diff 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904..HEAD src/algebra/hom/commute.lean
git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/hom/equiv/basic.lean
git diff a95b16cbade0f938fc24abd05412bde1e84bab9b..HEAD src/algebra/hom/equiv/units/basic.lean
git diff 655994e298904d7e5bbd1e18c95defd7b543eb94..HEAD src/algebra/hom/equiv/units/group_with_zero.lean
git diff e574b1a4e891376b0ef974b926da39e05da12a06..HEAD src/algebra/group/ext.lean
git diff 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904..HEAD src/algebra/group/type_tags.lean
git diff e574b1a4e891376b0ef974b926da39e05da12a06..HEAD src/algebra/group/with_one/defs.lean
git diff 07fee0ca54c320250c98bacf31ca5f288b2bcbe2..HEAD src/algebra/order/zero_le_one.lean
git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/algebra/order/sub/canonical.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/order/monoid/units.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/order/monoid/type_tags.lean
git diff 99e8971dc62f1f7ecf693d75e75fbbabd55849de..HEAD src/algebra/order/monoid/lemmas.lean
git diff 07fee0ca54c320250c98bacf31ca5f288b2bcbe2..HEAD src/algebra/order/monoid/nat_cast.lean
git diff 9b2660e1b25419042c8da10bf411aa3c67f14383..HEAD src/algebra/order/monoid/basic.lean
git diff dad7ecf9a1feae63e6e49f07619b7087403fb8d4..HEAD src/algebra/order/monoid/with_zero/basic.lean
git diff dad7ecf9a1feae63e6e49f07619b7087403fb8d4..HEAD src/algebra/order/monoid/with_zero/defs.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/order/monoid/cancel/basic.lean
git diff a95b16cbade0f938fc24abd05412bde1e84bab9b..HEAD src/algebra/order/group/units.lean
git diff a95b16cbade0f938fc24abd05412bde1e84bab9b..HEAD src/algebra/order/group/order_iso.lean
git diff a95b16cbade0f938fc24abd05412bde1e84bab9b..HEAD src/algebra/order/group/instances.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/order/group/defs.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/algebra/group_with_zero/divisibility.lean
git diff e574b1a4e891376b0ef974b926da39e05da12a06..HEAD src/algebra/divisibility/units.lean
git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/algebra/divisibility/basic.lean
git diff 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3..HEAD src/order/boolean_algebra.lean
git diff 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904..HEAD src/order/symm_diff.lean
git diff c4658a649d216f57e99621708b09dcb3dcccbd23..HEAD src/order/monotone.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/order/antisymmetrization.lean
git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/order/rel_iso/group.lean
git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/order/rel_iso/basic.lean
git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/order/hom/basic.lean
git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/order/heyting/boundary.lean
git diff 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..HEAD src/order/heyting/basic.lean
git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/data/sigma/order.lean
git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/data/psigma/order.lean
git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/data/list/defs.lean
git diff d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..HEAD src/data/option/n_ary.lean
git diff 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3..HEAD src/data/stream/defs.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/group_theory/group_action/option.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/group_theory/group_action/sum.lean
git diff f1a2caaf51ef593799107fe9a8d5e411599f3996..HEAD src/group_theory/group_action/sigma.lean
git diff dad7ecf9a1feae63e6e49f07619b7087403fb8d4..HEAD src/group_theory/group_action/defs.lean
git diff d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..HEAD src/logic/basic.lean

Jireh Loreaux (Dec 08 2022 at 16:10):

Note: most of these are probably just the mathlib4 synchronization label, but I haven't checked.

Heather Macbeth (Dec 08 2022 at 16:13):

Probably Johan suppressed this output because there was so much noise, and now it's biting us.

Eric Wieser (Dec 08 2022 at 16:14):

The port status script already ignores changes due to the synchronization label

Eric Wieser (Dec 08 2022 at 16:15):

Or at least, it was supposed to...

Heather Macbeth (Dec 08 2022 at 16:15):

Jireh, are you running the latest version of the port status script?

Jireh Loreaux (Dec 08 2022 at 16:15):

The latest version is just tracked in mathlib right? Or did it get folded into mathlib-tools sometime?

Eric Wieser (Dec 08 2022 at 16:15):

It's in mathlib

Jireh Loreaux (Dec 08 2022 at 16:16):

Then yes, I have the latest version because I was on the latest master.

Jireh Loreaux (Dec 08 2022 at 16:19):

Seems like the port status script is not ignoring sync labels (at least not always) because some of these changes are only the sync label.

Johan Commelin (Dec 08 2022 at 16:19):

I will look into this issue asap

Heather Macbeth (Dec 08 2022 at 16:19):

I tried the first couple, 

git diff 70d50ecfd4900dd6d328da39ab7ebd516abe4025..HEAD src/combinatorics/quiver/subquiver.lean

is just the freezing message but

git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/combinatorics/quiver/path.lean

has a substantive change.

Eric Wieser (Dec 08 2022 at 16:21):

The output of the script is not the command it runs internally

Eric Wieser (Dec 08 2022 at 16:21):

I'll make a fix

Johan Commelin (Dec 08 2022 at 16:38):

I think every line of output of port_status.py has an accompanying line in my html page.

Johan Commelin (Dec 08 2022 at 16:39):

I'm walking home atm... I can probably debug in 2hrs or so

Eric Wieser (Dec 08 2022 at 16:43):

Ugh, I think there is a bug in git (edit: https://stackoverflow.com/q/74733674/102441)

Eric Wieser (Dec 08 2022 at 16:43):

git diff --ignore-matching-lines='^$' ignores everything even though I asked it to only ignore blank lines

Johan Commelin (Dec 08 2022 at 16:44):

ouch

Mauricio Collares (Dec 08 2022 at 16:59):

https://www.sjoerdlangkemper.nl/2021/08/13/how-does-git-diff-ignore-matching-lines-work/ provides git diff -I $'\\`\n\\\'' as an alternative, but I haven't tested it

Yuyang Zhao (Dec 08 2022 at 17:08):

Heather Macbeth said:

In that case, shouldn't there be an alert somewhere saying "this file has been modified since the last verified commit"? I wonder if something is broken in the tooling.

We have that

  1. Algebra/Order/Monoid/WithZero/Defs was ported in mathlib4#851 modelled on dad7ecf9a1feae63e6e49f07619b7087403fb8d4
  2. #17465 modified the file in mathlib3
  3. #17820 modified the file again in mathlib3
  4. mathlib4#851 was merged into mathlib4
  5. the bot marked the file in mathlib3 as frozen.

Also note that docs#linear_ordered_comm_monoid_with_zero.to_zero_le_one_class and docs#canonically_ordered_add_monoid.to_zero_le_one_class were already in algebra/order/monoid/with_zero/def before dad7ecf9a1feae63e6e49f07619b7087403fb8d4.

Heather Macbeth (Dec 08 2022 at 17:13):

I see. So in fact both dad7ecf9a1feae63e6e49f07619b7087403fb8d4 mathlib3 and current mathlib3 have the two zero_le_one_class instances in that file. But the people reviewing mathlib4#851, aware of the general chaos around zero_le_one_class, incorrectly assumed that their deletion was deliberate and supposed to match a mathlib3 change.

Heather Macbeth (Dec 08 2022 at 17:16):

One more reason not to refactor right when the port hits!

Johan Commelin (Dec 08 2022 at 17:59):

Do I need to take any particular action? Or will everything be fixed on the python side?

Notification Bot (Dec 08 2022 at 18:37):

32 messages were moved from this topic to #mathlib4 > #port-status not showing modified files by Eric Wieser.

Last updated: Dec 20 2023 at 11:08 UTC