Definition of nat multiplication

Stream: maths

[Sebastien Gouezel]

I posted a question on the lean4 thread asking if the Lean4 developers would agree to change the definition of nat multiplication to avoid non-defeq instances of semimodule on nat. Leo's answer was very reasonable: they may consider this, but first all users should agree on this. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PR.20welcome.3F/near/221693092

I have the impression that this change would solve a problem we have encountered in Lean 3, but if I understand correctly @Eric Wieser was not convinced it would really solve the issue. Since I'm not completely sure either way, I thought I'd ask here. What do you think?

[Johan Commelin]

I think it will at least solve more problems than it will create (from a maths perspective). I have no idea if there are CS reasons to keep it the way it is.

[Eric Wieser]

Did you mean to link to the same topic you posted in?

[Gabriel Ebner]

I'm not sure there's a reason for the right-recursiveness of multiplication except to be consistent with addition. (And I really prefer n+1 over 1+n.)

[Gabriel Ebner]

If we want to change this in Lean 4, we should first try it out in Lean 3 and see if there's any unexpected breakage in mathlib.

[Floris van Doorn]

So is the suggestion to keep addition right-recursive? I agree with Gabriel that n+1 looks much nicer than 1+n.
Left-recursive multiplication and right-recursive addition sounds weird, but maybe that's pretty nice. 2 * n looks nicer than (or equally nice as) n * 2.

[Eric Wieser]

Ok, here's the diamond in nat.semimodule that this won't help with removing:

import algebra.module.basic

@[ext]
structure has_nat_diamond (M : Type*) :=
(value : M)

namespace has_nat_diamond

variables {M : Type*}

instance [add_comm_monoid M] : add_comm_monoid (has_nat_diamond M) :=
{ zero := ⟨0⟩,
  add := λ a b, ⟨a.1 + b.1⟩,
  zero_add := λ a, ext _ _ (zero_add _),
  add_zero := λ a, ext _ _ (add_zero _),
  add_comm := λ a b, ext _ _ (add_comm _ _),
  add_assoc := λ a b c, ext _ _ (add_assoc _ _ _) }

instance {R : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] :
  semimodule R (has_nat_diamond M) :=
{ smul := λ r x, ⟨r • x.1⟩,
  one_smul := λ _, ext _ _ (one_smul _ _),
  mul_smul := λ _ _ _, ext _ _ (mul_smul _ _ _),
  smul_add := λ _ _ _, ext _ _ (smul_add _ _ _),
  smul_zero := λ _, ext _ _ (smul_zero _),
  add_smul := λ _ _ _, ext _ _ (add_smul _ _ _),
  zero_smul := λ _, ext _ _ (zero_smul _ _) }

-- fails
example {R : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] :
  (add_comm_monoid.nat_semimodule : semimodule ℕ (has_nat_diamond M)) = has_nat_diamond.semimodule := rfl

end has_nat_diamond

[Eric Wieser]

The proof := subsingleton.elim _ _ works, but type-class resolution doesn't try that

[Eric Wieser]

That's not to say that your suggestion is pointless - it does solve diamonds between docs#mul_action.regular and docs#add_comm_monoid.nat_semimodule

[Sebastien Gouezel]

Yes indeed, the diamond you're pointing out is not solved by my proposition, which is only to solve the two ℕ-modules structure on ℕ.

[Eric Wieser]

The diamond above is quite pervasive - because it affects linear_map, a chain of N linear maps has N+1 different nat-semimodule instances

[Sebastien Gouezel]

Gabriel Ebner said:

If we want to change this in Lean 4, we should first try it out in Lean 3 and see if there's any unexpected breakage in mathlib.

I had a look at the change in Lean 3, and there is an issue that there is non-homogeneous multiplication in Lean 4 but not in Lean 3, so making the "same" change and checking the consequences does not seem obvious. In Lean 4, it would be possible to define a multiplication ℕ → α → α for any α with an addition and a zero, by induction, and then specialize it to a multiplication on ℕ. And then define a multiplication ℤ → α → α for any α with an addition, a zero and a negation (by using the nat addition already defined), and specialize it to get the ℤ-multiplication. In the current state of Lean 3 and mathlib, making the same change would require moving has_scalar to core, so I am not sure it is desirable.

[Eric Wieser]

For what it's worth, there's now a docs#nsmul_eq_smul lemma that will rewrite the "backwards" multiplication of docs#add_comm_monoid.int_semimodule into the forwards multiplication of docs#mul_action.regular, as long as you use local attribute [instance] mul_action.regular