smul inferred by function instance

Stream: Is there code for X?

[Alex Kontorovich]

Say I have a SMul with C acting on B. Should Lean know automatically how to extend that action to one on functions A → B? The following fails:

import Mathlib

example {A B C : Type*} (f : A → B) (c : C) (a : A) [HSMul C B B] : c • (f a) = (c • f) a :=
-- failed to synthesize HSMul C (A → B) ?m.32063
  rfl

But with a little help, it works

import Mathlib

instance {A B C : Type*} [HSMul C B B] : HSMul C (A → B) (A → B) where
    hSMul := fun c f a ↦ c • f a

example {A B C : Type*} (f : A → B) (c : C) (a : A) [HSMul C B B] : c • (f a) = (c • f) a :=
  rfl
-- works

Why does it need that help?

[Adam Topaz]

If you replace HSMul C B B with SMul C B then everything works as expected.

[Adam Topaz]

Is there a particular reason you want HSMul?

[Alex Kontorovich]

Ah that's what's wrong. Thanks!

[Alex Kontorovich]

Out of curiosity, what does the H in HSmul stand for? (Maybe that would've helped me notice the distinction...)

[Adam Topaz]

"Heterogeneous" :)

[Adam Topaz]

HSMul A B C means A acts on B but this action takes values in C

[Alex Kontorovich]

Yep, got it; thanks!!

[Adam Topaz]

(modulo some permutation of the variables :))

[Adam Topaz]

We have other heterogenous operations like HMul, HDiv, etc. but I don't think they're used much in mathlib.

[Sky Wilshaw]

The most common heterogeneous operation is natural/integer exponentiation.

[Edward van de Meent]

there might be some of these used in the Pointwise namespace, for their respective pointwise actions on Sets, iirc

[Alex Kontorovich]

Ok wait, so say we have a heterogeneous action. Why wouldn't Lean know to infer the action on functions? Example:

import Mathlib

example {A B C D : Type*} (f : A → B) (c : C) (a : A) [HSMul C B D] : c • (f a) = (c • f) a :=
-- failed to synthesize HSMul C (A → B) ?m.32913
  rfl

What else could I possibly mean? On the left, f a has type B and I'm bubbing it with c, so I must have in mind a term of type D. So the right must be a function which takes a : A and returns something of type D. Is there a reason that it doesn't automatically do the following:

import Mathlib

instance {A B C D : Type*} [HSMul C B D] : HSMul C (A → B) (A → D) where
    hSMul := fun c f a ↦ c • f a

example {A B C D : Type*} (f : A → B) (c : C) (a : A) [HSMul C B D] : c • (f a) = (c • f) a :=
  rfl
-- works

? Thanks!

[Adam Topaz]

I think it's just because such an instance was never added anywhere!

[Adam Topaz]

Here is the SMul instance: Pi.instSMul

[Alex Kontorovich]

Oh ok. So I guess that's what I'm asking - should such an instance exist? (Seems useful to me... Came up in something @Madison Crim was doing...)

[Adam Topaz]

But Pi.instHSMul doesn't exist

[Alex Kontorovich]

This is even a Pi version; I just have a single function -- even that doesn't seem to exist?

[Alex Kontorovich]

Worth a PR perhaps?

[Adam Topaz]

I think we're very timid about adding heterogeneous instances in mathlib.

[Adam Topaz]

I would continue this discussion at #mathlib4

[Alex Kontorovich]

Ah. Because there could be some other context where you'd want a different action, right?

[Notification Bot]

2 messages were moved from this topic to #mathlib4 > Should Pi.instHSMul exist in Mathlib? by Eric Wieser.

[Johan Commelin]

For those who want to find the new location of the topic... it's here #mathlib4>Should `Pi.instHSMul` exist in Mathlib?

[Notification Bot]

8 messages were moved from this topic to #Zulip meta > Broken thread links after moving by Eric Wieser.

[Eric Wieser]

(to avoid saddling @Alya Abbott with having to sift through this non-zulip-meta channel to re-find this thread)