## Stream: general

### Topic: diamond

#### Johan Commelin (Mar 10 2021 at 10:47):

import algebra.module.basic

@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.

#### 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?

#### 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

#### 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.

#### 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.

lean#551

courage!

#### Johan Commelin (Mar 10 2021 at 15:58):

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

#### Yakov Pechersky (Mar 10 2021 at 16:01):

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

#### 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.

#### 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 _ _ }


#### Yakov Pechersky (Mar 10 2021 at 16:07):

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

#### 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?

#### Eric Wieser (Mar 10 2021 at 16:21):

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

#### Yakov Pechersky (Mar 10 2021 at 22:33):

branch#pechersky/mul-on-left

#### Yakov Pechersky (Mar 10 2021 at 22:33):

Seems like it build on my machine

#### 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.

#### 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

@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.

#### 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)


#### 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.

#### 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.

#### Kevin Buzzard (Mar 11 2021 at 07:56):

I think nat should be renamed pnat_with_zero

#### Sebastien Gouezel (Mar 11 2021 at 07:56):

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

#### Sebastien Gouezel (Mar 11 2021 at 07:57):

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

#### 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

#### Kevin Buzzard (Mar 11 2021 at 08:28):

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

#### Ruben Van de Velde (Mar 11 2021 at 08:28):

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

#### Kevin Buzzard (Mar 11 2021 at 08:29):

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

#### 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/

#### 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

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

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


#### Sebastien Gouezel (Mar 11 2021 at 14:52):

Is that on master or on your branch?

#### Sebastien Gouezel (Mar 11 2021 at 14:53):

(or is that irrelevant)?

#### 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


#### 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

#### 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

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


#### 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


#### 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?

#### Yakov Pechersky (Mar 12 2021 at 19:34):

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

import algebra.module.basic

@semiring.to_semimodule.{0} int
(@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) := rfl


#### Yakov Pechersky (Mar 12 2021 at 19:35):

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

#### 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 { ... }.

#### Eric Wieser (Mar 12 2021 at 19:38):

What branch of lean are you working from?

#### Yakov Pechersky (Mar 12 2021 at 19:39):

lean#551 sorry, typo

#### 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?

#### Eric Wieser (Mar 12 2021 at 19:43):

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

#### Sebastien Gouezel (Mar 12 2021 at 19:43):

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

#### 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⟩

protected def mul : ℤ → ℤ → ℤ :=
int.smul


#### Yakov Pechersky (Mar 12 2021 at 19:46):

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

#### 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.

#### Yakov Pechersky (Mar 12 2021 at 19:47):

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

#### 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.

#### Eric Wieser (Mar 12 2021 at 19:47):

I think you have to push a tag to your fork

#### Eric Wieser (Mar 12 2021 at 19:47):

@Gabriel Ebner would know more

#### Yakov Pechersky (Mar 12 2021 at 19:48):

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

#### Eric Wieser (Mar 12 2021 at 19:49):

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

#### Eric Wieser (Mar 12 2021 at 19:50):

And then nsmul / pow can have different conventions

#### 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

#### 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.

#### 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"


#### Yakov Pechersky (Mar 12 2021 at 20:04):

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

#### 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.

#### 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.

#### 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.

#### 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?

#### 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

#### Yakov Pechersky (Mar 12 2021 at 20:54):

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

#### Kevin Buzzard (Mar 12 2021 at 21:02):

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

#### Kevin Buzzard (Mar 12 2021 at 21:02):

a * 1 = 0 + a IIRC

#### 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!

#### Kevin Buzzard (Mar 12 2021 at 21:03):

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

#### 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.

#### 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!

#### Kevin Buzzard (Mar 13 2021 at 00:10):

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

#### 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?

#### 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

#### 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.

#### 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"?

#### Eric Wieser (Apr 26 2021 at 14:26):

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

#### Yakov Pechersky (Apr 26 2021 at 14:30):

No, this is not rfl:

import algebra.module.basic

@semiring.to_module.{0} int
(@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) := rfl -- nope


#### 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.

(or int)

#### 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

#### Sebastien Gouezel (Apr 26 2021 at 15:35):

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

#### Yakov Pechersky (Apr 26 2021 at 15:36):

Maybe I was using an outdated master

#### 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.

#### Yakov Pechersky (Apr 26 2021 at 15:58):

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

#### 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

#### Yakov Pechersky (Apr 26 2021 at 16:47):

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

#### Kevin Buzzard (Apr 26 2021 at 18:41):

who needs gitpod

Last updated: May 14 2021 at 13:24 UTC