Heterogeneous scalar multiplication

Stream: mathlib4

[Heather Macbeth]

In mathlib4#1169, having made the • notation heterogeneous seems to have broken some simps. Here's an import-free example: a simp that doesn't work, but if in the middle section you change

class HSMul (M α : Type) (β : outParam (Type)) where
  hSMul : M → α → β

infixr:73 " • " => HSMul.hSMul

instance instHSMul [SMul M α] : HSMul M α α where
  hSMul := SMul.smul

to

infixr:73 " • " => SMul.smul

then it does work.

/-! maps preserving addition -/

structure AddHom (M N : Type) [Add M] [Add N] where
to_fun : M → N
map_add : ∀ x y, to_fun (x + y) = to_fun x + to_fun y

instance [Add M] [Add N] : CoeFun (AddHom M N) fun _ => M → N where
coe := AddHom.to_fun

@[simp]
theorem map_add [Add M] [Add N] (f : AddHom M N) (x y : M) : f (x + y) = f x + f y :=
AddHom.map_add f x y

/-! scalar multiplication -/

class HSMul (M α : Type) (β : outParam (Type)) where
hSMul : M → α → β

infixr:73 " • " => HSMul.hSMul

class SMul (M α : Type) where
smul : M → α → α

-- infixr:73 " • " => SMul.smul

instance instHSMul [SMul M α] : HSMul M α α where
hSMul := SMul.smul

class Module (M α : Type) [Add M] [Add α] extends SMul M α where
add_smul : ∀ (r s : M) (x : α), (r + s) • x = r • x + s • x

/-! composition definitions -/

@[simp]
def SMul.comp.smul [SMul N α] (g : M → N) (m : M) (a : α) : α := g m • a

@[reducible]
def SMul.comp [SMul N α] (g : M → N) : SMul M α where
smul := SMul.comp.smul g

@[reducible]
def Module.compHom [Add α] [Add M] [Add N] [Module N α] (f : AddHom M N) : Module M α :=
{ smul := SMul.comp.smul f
add_smul := fun r s x => by simp [add_smul] }

[Heather Macbeth]

Is this a familiar problem? What's the fix? (And can someone remind me why we made • heterogeneous, anyway?)

[Gabriel Ebner]

This is the same issue as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unfolding.20earlier.20fields

[Gabriel Ebner]

One potential workaround is to define the smul instance separately, and add an explicit simp-lemma to unfold it.

[Heather Macbeth]

Thanks Gabriel! I don't understand your comment at that link, though -- could you explain more about the fix? snap :racecar:

[Gabriel Ebner]

import Std.Tactic.HaveI
import Mathlib.Tactic.Spread

/-! maps preserving addition -/

structure AddHom (M N : Type) [Add M] [Add N] where
to_fun : M → N
map_add : ∀ x y, to_fun (x + y) = to_fun x + to_fun y

instance [Add M] [Add N] : CoeFun (AddHom M N) fun _ => M → N where
coe := AddHom.to_fun

@[simp]
theorem map_add [Add M] [Add N] (f : AddHom M N) (x y : M) : f (x + y) = f x + f y :=
AddHom.map_add f x y

/-! scalar multiplication -/

class HSMul (M α : Type) (β : outParam (Type)) where
hSMul : M → α → β

infixr:73 " • " => HSMul.hSMul

class SMul (M α : Type) where
smul : M → α → α

-- infixr:73 " • " => SMul.smul

instance instHSMul [SMul M α] : HSMul M α α where
hSMul := SMul.smul

class Module (M α : Type) [Add M] [Add α] extends SMul M α where
add_smul : ∀ (r s : M) (x : α), (r + s) • x = r • x + s • x

/-! composition definitions -/

@[simp]
def SMul.comp.smul [SMul N α] (g : M → N) (m : M) (a : α) : α := g m • a

@[reducible]
def SMul.comp [SMul N α] (g : M → N) : SMul M α where
smul := SMul.comp.smul g

@[reducible]
def Module.compSMul [Add α] [Add M] [Add N] [Module N α] (f : AddHom M N) : SMul M α where
  smul := SMul.comp.smul f

@[simp]
theorem Module.compSMul_def [Add α] [Add M] [Add N] [Module N α] (f : AddHom M N) (m : M) (a : α) :
  letI : SMul M α := Module.compSMul f
  m • a = f m • a := rfl

@[reducible]
def Module.compHom [Add α] [Add M] [Add N] [Module N α] (f : AddHom M N) : Module M α where
  __ := Module.compSMul f
  add_smul := by simp [add_smul]

[Heather Macbeth]

Interesting! Yes, that works in the file, thanks.

[Heather Macbeth]

I just made an import-free example of a typeclass inference problem which came up in the port earlier today, where the problem is seemingly not a Lean 3/Lean 4 change, but a Mathlib 3/Mathlib 4 change: our choice to wrap scalar multiplication in an extra layer of heterogeneous scalar multiplication. Compare

variable {α β γ : Type}

class Singleton (α : outParam Type) (β : Type) where
  singleton : α → β

def Set (α : Type) := α → Prop

instance : Singleton α (Set α) := sorry

class HSMul (α : Type) (β : Type) (γ : outParam Type) where
 hSMul : α → β → γ

class SMul (α : Type) (β : Type) where
  smul : α → β → β

instance instHSMul [SMul α β] : HSMul α β β := ⟨SMul.smul⟩

variable [SMul α β] {s : Set α} {b : β}

instance Set.hasSmul : SMul (Set α) (Set β) := sorry

example : Set β := HSMul.hSMul s (Singleton.singleton b) -- fails

example : Set β := SMul.smul s (Singleton.singleton b) -- works

with the mathlib3 version.

[Heather Macbeth]

As far as I can tell these two are exact translations and fail in the same ways. So the culprit should be the HSMul layer.

[Heather Macbeth]

Did we previously discuss the choice to invent HSMul? Could someone link to that discussion? What is the expected benefit?

[Heather Macbeth]

While writing this message I discovered that I had previously started another thread with the same title, with something else that was broken by adding an HSMul layer. Scroll up to see it.

[Ruben Van de Velde]

I think we introduced hsmul to match the built-in operator type classes like hmul

[Heather Macbeth]

Right, it in fact has the same signature as HMul. But did we have some intended use case?

[James Gallicchio]

I vaguely remember it was about separating the notation (cdot) from the mathlib meaning (multiplication by scalar) because somebody wanted to use the notation for something that was not scalar multiplication?

[Mario Carneiro]

As far as I know there wasn't any particular motivation to add HSMul other than consistency with core. We certainly don't have any current things that need it.

[Yaël Dillies]

Yes, I would be happy to ditch it.

[Mario Carneiro]

I think this issue is caused by not marking the SMul -> HSMul instance as a default instance though

[Mario Carneiro]

unlike the Add -> HAdd instances

[Yaël Dillies]

@Jireh Loreaux introduced it because of to_additive troubles. But I think those could have been solved another way.

[Mario Carneiro]

I would be surprised if HSMul has any issues above and beyond what we already have to deal with for HAdd and HPow

[Heather Macbeth]

OK, I found Jireh's post in favour of HSMul using the pointers Yaël gave about the history with to_additive.

Jireh Loreaux said:

Look, I propose creating the HSMul class for now so that I can fix to_additive translating pow to smul without potentially clobbering HMul. If later we wish to change Lean 4 core to remove HPow and we can convince the devs, fine, we can do that when the time comes.

[Heather Macbeth]

Mario, does this clarify anything for you? Do you still think we need a SMul -> HSMul default instance to fix this?

[Jireh Loreaux]

@Yaël Dillies what other way?

Yes, the introduction of HSMul was primarily to fix to_additive, but I think the other benefit was keeping the smul and mul notations completely separate. Eric also mentioned a use case in that thread IIRC (can't link right now, on mobile, Heather, can you do it?).

[Eric Wieser]

Do you still think we need a SMul -> HSMul default instance to fix this?

I think we should certainly have this, and can revisit whether the H version is needed at all later

[Eric Wieser]

To be clear, docs4#instHSMul aleady exists, it's just missing the @[defaultInstance] attribute that docs4#instHMul has

[Floris van Doorn]

Added in mathlib4#1501