autogen instances for commutative operations?

Stream: new members

[Alok Singh]

take

instance : HMul Float (Matrix rows cols) (Matrix rows cols) where
  hMul scalar matrix := ⟨matrix.data.map (· * scalar)⟩
#eval 2.0 * mat

I'd like to have

instance : HMul (Matrix rows cols) Float (Matrix rows cols) where
  hMul matrix scalar := scalar * matrix
#eval mat * 2.0

generated automatically since the underlying op (in this case) is commutative. Is that possible already? if not, is there a way i could metaprogram my way to victory?

[Mitchell Lee]

It is technically possible to do what you are asking about. However, I very very strongly do not recommend it. * is not a "commutative operation"; it is just a symbol. It can be used as notation for both commutative and non-commutative operations.

If you decide you want to do it anyway, here is how you could.

import Mathlib

instance {α β γ : Type*} [HMul α β γ] : HMul β α γ := ⟨fun x y ↦ y * x⟩

/- Yields !![8, 11]. Note that these matrices are not of the correct dimensions to be multiplied,
so the instance above is used to reinterpret it as !![1, 2] * !![2, 1 ; 3, 5] first. -/
#eval !![2, 1 ; 3, 5] * !![1, 2]

[Alok Singh]

this works but is somewhat broader than intended. i'm very well aware that * is just a symbol not implying commutativity, which is why some way of tagging single instances to generate flipped instance is desirable