diamond

Stream: general

[Johan Commelin]

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.

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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.

[Yakov Pechersky]

lean#551

[Johan Commelin]

courage!

[Johan Commelin]

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

[Yakov Pechersky]

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

[Sebastien Gouezel]

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]

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]

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

[Eric Wieser]

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]

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

[Yakov Pechersky]

branch#pechersky/mul-on-left

[Yakov Pechersky]

Seems like it build on my machine

[Yakov Pechersky]

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]

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.

[Yakov Pechersky]

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]

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]

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

[Kevin Buzzard]

I think nat should be renamed pnat_with_zero

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Kevin Buzzard]

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]

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

[Ruben Van de Velde]

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

[Kevin Buzzard]

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

[Scott Morrison]

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]

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

[Sebastien Gouezel]

Is that on master or on your branch?

[Sebastien Gouezel]

(or is that irrelevant)?

[Yakov Pechersky]

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]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Eric Wieser]

What branch of lean are you working from?

[Yakov Pechersky]

lean#551 sorry, typo

[Eric Wieser]

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]

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

[Sebastien Gouezel]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Eric Wieser]

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]

I think you have to push a tag to your fork

[Eric Wieser]

@Gabriel Ebner would know more

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Wieser]

And then nsmul / pow can have different conventions

[Eric Wieser]

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]

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]

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]

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

[Sebastien Gouezel]

Thanks for pushing.

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

a * 1 = 0 + a IIRC

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Yakov Pechersky]

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]

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]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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]

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]

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

[Yakov Pechersky]

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

[Eric Wieser]

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.

[Yakov Pechersky]

(or int)

[Eric Wieser]

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]

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

[Yakov Pechersky]

Maybe I was using an outdated master

[Sebastien Gouezel]

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]

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

[Alex J. Best]

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]

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

[Kevin Buzzard]

who needs gitpod