SMul diamond on subsets

Stream: mathlib4

[Michael Stoll]

There seems to be a diamond between two docs#SMul instances for pointwise multiplication of subsets by natural numbers: there is docs#Set.NSMul and docs#Set.smulSet.

The second example below shows that when we coerce the result of an nsmul on a subgroup to a subset, we end up with a different instance than when first coercing and then nsmuling. These two instances are not defeq, which leads to problems when I want to prove stuff.

import Mathlib

open scoped Pointwise

variable {G : Type*} [AddCommGroup G]

example {n : ℕ} : n • (.univ : Set G) = n • (⊤ : AddSubgroup G) := by
  ext g
  simp -- works

example {n : ℕ} : n • (.univ : Set G) = (n • (⊤ : AddSubgroup G) :) := by
  ext g
  simp -- does not close the goal; leaves
  -- ⊢ g ∈ n • Set.univ ↔ g ∈ n • Set.univ
  sorry

example : Set.NSMul (α := G) = Set.smulSet (β := G) := rfl -- fails

Indeed, it is even worse: these two are not even propositionally equal:

import Mathlib

open scoped Pointwise

variable {G : Type*} [AddCommGroup G]

example : @SMul.smul ℕ (Set G) Set.NSMul 0 ⊥ ≠ @SMul.smul ℕ (Set G) Set.smulSet 0 ⊥ := by
  intro H
  simp [Set.NSMul, Set.smulSet, nsmulRec, Set.ext_iff] at H

I don't see why it would make sense to define 0 • ∅ to be {0}... (the culprit is docs#nsmulRec in docs#Set.NSMul combined with docs#Set.zero .)

[Michael Stoll]

Also, docs#Set.mem_smul_set vs. docs#Set.mem_nsmul .

theorem Set.mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {x : β} :
    x ∈ a • t ↔ ∃ y ∈ t, a • y = x

theorem Set.mem_nsmul {α : Type u_1} [AddMonoid α] {s : Set α} {a : α} {n : ℕ} :
    a ∈ n • s ↔ ∃ (f : Fin n → ↑s), (List.ofFn fun (i : Fin n) => ↑(f i)).sum = a

These are plainly completely different things (for general sets).

[Michael Stoll]

This reminds me of this earlier thread: #mathlib4 > Too many 'Smul's @ 💬

[Yaël Dillies]

This is a well-known diamond. Since repeated addition cannot be conveniently written any other way, it was decided to make it have priority. Elementwise scalar multiplication should be written (n • ·) '' s instead.

[Michael Stoll]

Could the repeated addition version be hidden in a scope?

[Yaël Dillies]

It's already hidden in a scope

[Yaël Dillies]

It is also possible to introduce n •ℕ s notation for the thing you want. I didn't do it because I didn't have an application.

[Michael Stoll]

In a different scope, I mean. I guess right now you get both with Poinwise?

[Michael Stoll]

I find this rather disconcerting:

import Mathlib

open scoped Pointwise

variable {G : Type*} [AddCommGroup G]

example {n : ℕ} : (n • (⊤ : AddSubgroup G) : Set G) = (n • (⊤ : AddSubgroup G) :) := by
  simp
  -- ⊢ n • Set.univ = n • Set.univ
  sorry

This should really be rfl.

I'd also argue for the slightly more complicated notation to be used for the less obvious thing (repeated pointwise addition).

[Michael Stoll]

Maybe it is better to have a type synonym for Set M with the additive monoid structure given by pointwise addition of sets?

There are clearly two quite natural nmsuls on subsets of an additive monoid, and I don't think it is a good idea to have both cropping up and mixing unexpectedly.

[Yaël Dillies]

Pointwise addition is the bread and butter of additive combinatorics, which is why things are designed the way they are right now.

[Yaël Dillies]

Why not standardise your use case to be spelled {n} • s instead?

[Michael Stoll]

That might be a possibility, although I'd still prefer there to be an AdditiveCombinatorics scope to protect unsuspecting non-(additive combinatorialists).

I guess that would mean to

• remove the SMul instance α → Set β → Set β (when there is SMul α β) and only keep Set α → Set β → Set β
• add simp lemmas like ((n • S :) : Set M) = {n} • (S : Set M) for S : AddSubgroup M
• maybe more?

Somebody would have to do that...

[Michael Stoll]

Although after more thought, I think that the clean solution would be to have a type synonym for Set M, which can then get an AddMonoid instance.

I was under the impression that one of the design principles of Mathlib is to not have non-defeq type class diamonds. But now I learn that there is a "well-known" diamond of this kind that has existed for years and which has just cost me a few hours of frustration. Is the plan to leave things like this?

(And don't try to convince a number theorist that 37 • ℤ = ℤ...)

[Sébastien Gouëzel]

I think we should just have two different scopes for the two different actions, because I agree it's dangerous to have them together.