Zulip Chat Archive

Stream: general

Topic: diamond


view this post on Zulip Johan Commelin (Mar 10 2021 at 10:47):

import algebra.module.basic

example : @add_comm_group.int_module.{0} int (@ring.to_add_comm_group _ int.ring) =
  @semiring.to_semimodule.{0} int
    (@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) :=
rfl -- fails

This one might be well-known. I think @Eric Wieser reported similar issues before.

view this post on Zulip Johan Commelin (Mar 10 2021 at 10:47):

It is stopping some statement from typechecking in LTE. Is there a chance that we can fix this?

view this post on Zulip Eric Wieser (Mar 10 2021 at 10:52):

Usinglocal attribute [-instance] add_comm_group.int_module so it doesn't appear in the first place is one solution

view this post on Zulip Eric Wieser (Mar 10 2021 at 10:53):

I think this is the diamond that @Sebastien Gouezel's approach of redefining int/nat multiply might fix, although I don't recall whether their proposal worked for int too, or just nat.

view this post on Zulip Sebastien Gouezel (Mar 10 2021 at 11:11):

The proposal is to redefine the definitions of both nat and int multiplication in core, to make sure that this precise diamond is defeq. I have never tried it because I don't know how to work on core.

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 15:53):

lean#551

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:58):

courage!

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:58):

I wonder how big of a refactor this will be for mathlib

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 16:01):

Depends on how often people (ab)use defeq of m * 0 = 0 and the succ version.

view this post on Zulip Sebastien Gouezel (Mar 10 2021 at 16:03):

I suspect it's rather on the other end: people didn't abuse defeq of 0 * m = 0 because it wasn't true. The change would make it possible to abuse it, but we won't notice because we already have the non-abusing proofs.

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 16:06):

Case in point:

@[simp, norm_cast] theorem cast_mul [semiring α] (m) :  n, ((m * n : ) : α) = m * n
| 0     := by { convert (mul_zero _).symm, rw [mul_zero], refl }
| (n+1) := by { convert (cast_add _ _).trans (
show ((m * n : ) : α) + m = m * (n + 1), by rw [cast_mul n, left_distrib, mul_one]),
  exact mul_succ _ _ }

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 16:07):

I added the convert, because before, it would "just work"

view this post on Zulip Eric Wieser (Mar 10 2021 at 16:17):

The unfolded version of the new nat.mul / the current src#monoid.pow is very ugly compared to the current nat.mul, most notably now involving nat.brec. Does this have bad consequences for speed of definitional reduction?

view this post on Zulip Eric Wieser (Mar 10 2021 at 16:21):

Why can't the equation compiler reduce monoid.pow to nat.rec_on n 1 (λ _, (*) a)?

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 22:33):

branch#pechersky/mul-on-left

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 22:33):

Seems like it build on my machine

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 22:34):

That is, using the modified lean core. It should still work on regular lean, I think, because the proofs have been changed just to avoid the defeq x * 0 = 0 mostly.

view this post on Zulip Yakov Pechersky (Mar 11 2021 at 04:32):

This mathlib branch now builds on both 3.27.0 and the dev-nat-mul-on-left without needing any changes to support either lean version. However, Johan's example is still not rfl in either version:

import algebra.module.basic

example : @add_comm_group.int_module.{0} int (@ring.to_add_comm_group _ int.ring) =
  @semiring.to_semimodule.{0} int
    (@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) :=
begin
  convert rfl,
  apply_instance
end

Do you foresee that some other change is needed to make it work? I didn't change the defn of int-multiplication.

view this post on Zulip Yakov Pechersky (Mar 11 2021 at 04:34):

In fact, I'm not sure how core int mul would be changed. This is what I have on the lean#511 branch right now. To me, that just seems like a case-bash against the two constructors.

protected def mul :     
| (of_nat m) (of_nat n) := of_nat (m * n)
| (of_nat m) -[1+ n]    := neg_of_nat (m * succ n)
| -[1+ m]    (of_nat n) := neg_of_nat (succ m * n)
| -[1+ m]    -[1+ n]    := of_nat (succ m * succ n)

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 07:52):

Yes, you would also need to change int multiplication. What matters is that it is defeq to docs#gsmul (in the sense that you can modify the definition of docs#gsmul if you like, to have two matching definitions). In particular, I don't think the int multiplication should case on the second variable: first, one should have the nat action on int, as on any semigroup, and then construct int multiplication from this.

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 07:55):

You need a monoid for a nat action. Semigroups just have a pnat action, as observed by Damiano Testa recently.

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 07:56):

I think nat should be renamed pnat_with_zero

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 07:56):

You're right. I am using semigroup and monoid interchangeably in my head!

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 07:57):

(I was saying "you're right" to your first line, not to the second one :-)

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 08:27):

The fundamental object is pnat, proved by Euclid to be a free monoid on an infinite generating set. Then you make nat by adding a zero and defining a pathological + operation

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 08:28):

You can tell it's pathological because Goldbach and twin primes are still open

view this post on Zulip Ruben Van de Velde (Mar 11 2021 at 08:28):

Then shouldn't \N be notation for pnat? :thinking:

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 08:29):

Sure! That's how I used the notation for 30 years

view this post on Zulip Scott Morrison (Mar 11 2021 at 09:33):

Kevin Buzzard said:

You can tell it's pathological because Goldbach and twin primes are still open

I can't resist: https://themoreyouknow.github.io/div/

view this post on Zulip Yakov Pechersky (Mar 11 2021 at 14:37):

Here's one of the problems (thanks Eric for explaining). Why doesn't rfl work here?

import algebra.module.basic

-- dev branch
#reduce λ k : , nat.mul 5 k -- λ (k : ℕ), ((((0.add k).add k).add k).add k).add k

protected def nat.mul' : nat  nat  nat
| 0     := λ b, 0
| (a+1) := λ b, b + nat.mul' a b

#reduce λ k : , nsmul 5 k    -- λ (k : ℕ), k.add (k.add (k.add (k.add k)))
#reduce λ k : , nat.mul' 5 k -- λ (k : ℕ), k.add (k.add (k.add (k.add k)))

example (n m : ) : nsmul n m = n.mul' m := rfl -- does not work??

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 14:52):

Is that on master or on your branch?

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 14:53):

(or is that irrelevant)?

view this post on Zulip Yakov Pechersky (Mar 11 2021 at 14:56):

For the mul' and nsmul, it is irrelevant. Here is that regular old nat.mul does on 3.27:

-- 3.27 branch
#reduce λ k : , nat.mul 5 k -- λ (k : ℕ), 5.mul k

view this post on Zulip Yakov Pechersky (Mar 11 2021 at 14:56):

It's not relevant for mul' and nsmul because both are defined via addition on the left

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 14:58):

Even better (or worse?):

protected def nat.mul' : nat  nat  nat
| 0     := λ b, 0
| (a+1) := λ b, b + nat.mul' a b

def nsmul' {A : Type*} [has_add A] [has_zero A] :   A  A
| 0     := λ b, 0
| (a+1) := λ b, b + nsmul' a b

#reduce λ k : , nsmul 5 k    -- λ (k : ℕ), k.add (k.add (k.add (k.add k)))
#reduce λ k : , nat.mul' 5 k -- λ (k : ℕ), k.add (k.add (k.add (k.add k)))

example (n m : ) : nsmul' n m = nat.mul' n m := rfl -- does not work??

view this post on Zulip Sebastien Gouezel (Mar 11 2021 at 15:06):

A way out is to avoid the equation compiler, which is just not good here, and use instead

protected def nat.mul' (n : ) (a : ) :  :=
nat.rec_on n 0 (λ b rec, rec + a)

def nsmul' {A : Type*} [has_add A] [has_zero A] (n : ) (a : A) : A :=
nat.rec_on n 0 (λ b rec, rec + a)

example (n m : ) : nsmul' n m = nat.mul' n m := rfl -- works
example (n m : ) : nsmul' (n + 2) m = nat.mul' n m + m + m := rfl -- works

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 06:43):

I would have thought that the way to define (a+1)b was ab+b rather than b+ab?

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:34):

Okay, wow, I have the following working on dev lean:

import algebra.module.basic

example : @add_comm_group.int_module.{0} int (@ring.to_add_comm_group _ int.ring) =
  @semiring.to_semimodule.{0} int
    (@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) := rfl

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:35):

But -- is it worth it? Check out the branch#pechersky/mul-on-left

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:37):

I removed many multiplicative proofs that (ab)used(?) defeq(?) I got lazy at the end and fell back to convert multiplicative; try { ... }.

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:38):

What branch of lean are you working from?

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:39):

lean#551 sorry, typo

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:42):

My confusion is the same as CI's: https://github.com/leanprover-community/mathlib/compare/pechersky/mul-on-left#diff-037522102a2edcd0b33801a2dc6dc56ea0eacefd5bd58c17402eec520dff4fffR52. Where is nat.smul defined?

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:43):

(I think you can edit the leanproject.yml to point at your branch somehow, also)

view this post on Zulip Sebastien Gouezel (Mar 12 2021 at 19:43):

Nice! Finally, you didn't need to change int multiplication?

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:45):

No, I did:

protected def smul {α : Type*} [has_add α] [has_zero α] :   α  α
| 0       := λ _, 0
| (n + 1) := λ b, b + smul n b

protected def mul :      :=
nat.smul

protected def smul {α : Type*} [has_add α] [has_zero α] [has_neg α] :   α  α
| (of_nat m) := m.smul
| -[1+ m]    := λ x, - (m.succ.smul x)

instance : has_neg  := int.neg
instance : has_add  := int.add

protected def mul :      :=
int.smul

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:46):

Testing now with your nat.rec style instead of eq compiler style.

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:46):

So that I can have a branch of mathlib that compiles in both dev and 3.27 contexts.

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:47):

@Eric Wieser what's the syntax to change the toml to a lean branch?

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:47):

Wouldn't smul n b + b be closed to the current definition? I think swapping the order of that plus is making things hard for you.

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:47):

I think you have to push a tag to your fork

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:47):

@Gabriel Ebner would know more

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:48):

I did addition on left to style after the pow preference.

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:49):

Perhaps pow should be defined as nat.smul n (opposite.op (additive.of_mul x))

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:50):

And then nsmul / pow can have different conventions

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:50):

I guess my argument is more that you're changing two things at once, and it makes it hard to tell how much fallout each change is responsible for

view this post on Zulip Sebastien Gouezel (Mar 12 2021 at 20:00):

I can't see the new definition of int.mul on the branch of lean#551. I am probably not looking at the right branch.

view this post on Zulip Gabriel Ebner (Mar 12 2021 at 20:02):

Eric Wieser said:

I think you have to push a tag to your fork

Exactly. Once you've pushed a tag, github actions will automatically build and upload a release. You can then refer to this release in the leanpkg.toml:

lean_version = "pechersky/lean:mytagname"

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:04):

Ah apologies. OK I've pushed to the lean branch.

view this post on Zulip Sebastien Gouezel (Mar 12 2021 at 20:32):

Thanks for pushing.

I agree that (n + 1) * a = n * a + a is more natural that (n + 1) * a = a + n * a.

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:34):

OK I'll test that instead. I realized recently that I had been checking for the module typeclass rfl proof via

convert rfl

and that can fail even when := rfl works. So perhaps not as many changes needed to happen as I made. But still, more proofs avoid defeq now so they'll work in either case. I'll see how brittle it is to switching the mul direction.

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 20:35):

convert rfl is extremely close to congr' which is better because it takes an optional numeral argument.

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:36):

But why would convert rfl leave with me with a module Z Z goal when := rfl just works?

view this post on Zulip Mario Carneiro (Mar 12 2021 at 20:52):

Sebastien Gouezel said:

I agree that (n + 1) * a = n * a + a is more natural that (n + 1) * a = a + n * a.

But that means that 1 * a is not defeq to a

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:54):

and, as more detail, with that definition, neither is a * 1 defeq to a

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 21:02):

but we already have that neither a * 1 nor 1 * a are equal to a.

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 21:02):

a * 1 = 0 + a IIRC

view this post on Zulip Sebastien Gouezel (Mar 12 2021 at 21:02):

That's a very good point. Then I agree that (n + 1) * a = a + n * a is better!

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 21:03):

who says succ n isn't 1 + n anyway? :-)

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 21:04):

I have a dev lean build with the mul-on-right working, where I've fixed defeq proofs to be robust to both versions. Now I'm polishing away mathlib proofs that use that defeq. That will allow us to test one vs the other more easily.

view this post on Zulip Sebastien Gouezel (Mar 12 2021 at 21:08):

It's true that currently neither of 1 * a and a * 1 are defeq to a. Having 1 * a = a by defeq (and even 1 • a = a in a monoid) looks like it couldn't hurt!

view this post on Zulip Kevin Buzzard (Mar 13 2021 at 00:10):

It might lead some computer scientists astray, they might abuse definitional equality

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 13:12):

What is the situation here?

After Sebastien's heroic efforts we now have a new definition of group and monoid. Is there now still an argument for changing the definition of int.mul?

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:05):

I think the argument was to make docs#smul_eq_mul true by rfl for nat and int

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:05):

But I don't think there is a diamond any more to motivate this. Edit: Hmm, that's already true by rfl, so I must be missing something.

view this post on Zulip Yakov Pechersky (Apr 26 2021 at 14:07):

My understanding is that my dev rebuilds and mathlib refactors were coming from the point of view of "we can't change nsmul or gsmul, so let's change nat mul and int mul instead". While Sebastien then said "hey, why the restricted assumption that we can't change how we work with nsmul and gsmul"?

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:26):

Is the diamond behind semiring.to_semimodule and add_comm_monoid.nat_semimodule now defeq?

view this post on Zulip Yakov Pechersky (Apr 26 2021 at 14:30):

No, this is not rfl:

import algebra.module.basic

example : @add_comm_group.int_module.{0} int (@ring.to_add_comm_group _ int.ring) =
  @semiring.to_module.{0} int
    (@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) := rfl -- nope

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:37):

Then the problem is still there. The diamond problem that Sebastien solved was one that came up with composite types like prod and tensor_product where add_comm_monoid.nat_semimodule would form a diamond with itself, rather than a niche one that only really comes up when working heavily with nat.

view this post on Zulip Yakov Pechersky (Apr 26 2021 at 14:39):

(or int)

view this post on Zulip Eric Wieser (Apr 26 2021 at 14:41):

Perhaps though this raises that the subsingleton (module nat N) instance needs to come back (it's now a lemma), since the problem isn't fully gone yet

view this post on Zulip Sebastien Gouezel (Apr 26 2021 at 15:35):

This works for me (on master). Are you up to date?

view this post on Zulip Yakov Pechersky (Apr 26 2021 at 15:36):

Maybe I was using an outdated master

view this post on Zulip Sebastien Gouezel (Apr 26 2021 at 15:40):

Kevin Buzzard said:

What is the situation here?

After Sebastien's heroic efforts we now have a new definition of group and monoid. Is there now still an argument for changing the definition of int.mul?

There could still be an argument, if we wanted to refactor nat.cast and int.cast, replacing them with n • 1 to get nice definitional behavior on most types. With this definition, if you want the cast from nat to itself to be equal to the identity definitionally, you would need to have n * 1 = n, which requires swapping multiplication. But this is way less important than before, since we got rid of all of our diamonds and this thing I mentioned would just require one additional rewrite in a few places.

view this post on Zulip Yakov Pechersky (Apr 26 2021 at 15:58):

https://olive-caribou-rfe62wpk.ws-us03.gitpod.io/#/workspace/mathlib indicates that yes, it is rfl

view this post on Zulip Alex J. Best (Apr 26 2021 at 16:11):

I think you have to share a gitpod workspace by doing "Gitpod: share workspace snapshot" in the control+shift+p menu for us to see what you see, that link is private

view this post on Zulip Yakov Pechersky (Apr 26 2021 at 16:47):

I see. In any case, it's just the example from above copied, and no errors.

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 18:41):

who needs gitpod


Last updated: May 14 2021 at 13:24 UTC