chore: upstream HSMul notation typeclass (#8401)

Upstreaming the `HSMul` notation typeclass, to enable `grind` to process
goals using it.

Author: kim-em

src/Init/Notation.lean

@@ -295,6 +295,7 @@ recommended_spelling "PProd" for "×'" in [PProd, «term_×'_»]
 @[inherit_doc] prefix:75 "-"     => Neg.neg
 @[inherit_doc] prefix:100 "~~~"  => Complement.complement
 @[inherit_doc] postfix:max "⁻¹"  => Inv.inv
+@[inherit_doc] infixr:73 " • " => HSMul.hSMul
 
 /-!
   Remark: the infix commands above ensure a delaborator is generated for each relations.
@@ -312,6 +313,40 @@ macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
+/-!
+We have a macro to make `x • y` notation participate in the expression tree elaborator,
+like other arithmetic expressions such as `+`, `*`, `/`, `^`, `=`, inequalities, etc.
+The macro is using the `leftact%` elaborator introduced in
+[this RFC](https://github.com/leanprover/lean4/issues/2854).
+
+As a concrete example of the effect of this macro, consider
+```lean
+variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
+#check m + r • n
+```
+Without the macro, the expression would elaborate as `m + ↑(r • n : ↑N) : M`.
+With the macro, the expression elaborates as `m + r • (↑n : M) : M`.
+To get the first interpretation, one can write `m + (r • n :)`.
+
+Here is a quick review of the expression tree elaborator:
+1. It builds up an expression tree of all the immediately accessible operations
+   that are marked with `binop%`, `unop%`, `leftact%`, `rightact%`, `binrel%`, etc.
+2. It elaborates every leaf term of this tree
+   (without an expected type, so as if it were temporarily wrapped in `(... :)`).
+3. Using the types of each elaborated leaf, it computes a supremum type they can all be
+   coerced to, if such a supremum exists.
+4. It inserts coercions around leaf terms wherever needed.
+
+The hypothesis is that individual expression trees tend to be calculations with respect
+to a single algebraic structure.
+
+Note(kmill): If we were to remove `HSMul` and switch to using `SMul` directly,
+then the expression tree elaborator would not be able to insert coercions within the right operand;
+they would likely appear as `↑(x • y)` rather than `x • ↑y`, unlike other arithmetic operations.
+-/
+
+@[inherit_doc HSMul.hSMul]
+macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
 
 recommended_spelling "or" for "|||" in [HOr.hOr, «term_|||_»]
 recommended_spelling "xor" for "^^^" in [HXor.hXor, «term_^^^_»]
@@ -323,6 +358,7 @@ recommended_spelling "mul" for "*" in [HMul.hMul, «term_*_»]
 recommended_spelling "div" for "/" in [HDiv.hDiv, «term_/_»]
 recommended_spelling "mod" for "%" in [HMod.hMod, «term_%_»]
 recommended_spelling "pow" for "^" in [HPow.hPow, «term_^_»]
+recommended_spelling "smul" for "•" in [HSMul.hSMul, «term_•_»]
 recommended_spelling "append" for "++" in [HAppend.hAppend, «term_++_»]
 /-- when used as a unary operator -/
 recommended_spelling "neg" for "-" in [Neg.neg, «term-_»]

src/Init/Prelude.lean

@@ -1348,6 +1348,23 @@ class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   The meaning of this notation is type-dependent. -/
   hPow : α → β → γ
 
+/--
+The notation typeclass for heterogeneous scalar multiplication.
+This enables the notation `a • b : γ` where `a : α`, `b : β`.
+
+It is assumed to represent a left action in some sense.
+The notation `a • b` is augmented with a macro (below) to have it elaborate as a left action.
+Only the `b` argument participates in the elaboration algorithm: the algorithm uses the type of `b`
+when calculating the type of the surrounding arithmetic expression
+and it tries to insert coercions into `b` to get some `b'`
+such that `a • b'` has the same type as `b'`.
+See the module documentation near the macro for more details.
+-/
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  /-- `a • b` computes the product of `a` and `b`.
+  The meaning of this notation is type-dependent, but it is intended to be used for left actions. -/
+  hSMul : α → β → γ
+
 /--
 The notation typeclass for heterogeneous append.
 This enables the notation `a ++ b : γ` where `a : α`, `b : β`.
@@ -1510,6 +1527,12 @@ class HomogeneousPow (α : Type u) where
   /-- `a ^ b` computes `a` to the power of `b` where `a` and `b` both have the same type. -/
   protected pow : α → α → α
 
+/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
+class SMul (M : Type u) (α : Type v) where
+  /-- `a • b` computes the product of `a` and `b`. The meaning of this notation is type-dependent,
+  but it is intended to be used for left actions. -/
+  smul : M → α → α
+
 /-- The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. -/
 class Append (α : Type u) where
   /-- `a ++ b` is the result of concatenation of `a` and `b`. See `HAppend`. -/
@@ -1601,6 +1624,13 @@ instance instPowNat [NatPow α] : Pow α Nat where
 instance [HomogeneousPow α] : Pow α α where
   pow a b := HomogeneousPow.pow a b
 
+@[default_instance]
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
+instance (priority := 910) {α : Type u} [Mul α] : SMul α α where
+  smul x y := Mul.mul x y
+
 @[default_instance]
 instance [Append α] : HAppend α α α where
   hAppend a b := Append.append a b

tests/lean/run/2461.lean

@@ -93,17 +93,6 @@ end algebra_hierarchy_morphisms
 
 section HSMul_stuff
 
-class HSMul (α : Type) (β : Type) (γ : outParam Type) where
-  hSMul : α → β → γ
-
-class SMul (M : Type) (α : Type) where
-  smul : M → α → α
-
-infixr:73 " • " => HSMul.hSMul
-
-instance instHSMul {α β : Type} [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
-
 -- note that the function `SMulZeroClass.toSMul` is what disrupts `simp` later
 class SMulZeroClass (M A : Type) extends SMul M A where
 

tests/lean/run/3807.lean

@@ -751,19 +751,6 @@ universe u v w
 
 open Function
 
-class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  hSMul : α → β → γ
-
-class SMul (M : Type u) (α : Type v) where
-  smul : M → α → α
-
-infixr:73 " • " => HSMul.hSMul
-
-macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
-
-instance instHSMul {α β} [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
-
 variable {G : Type _}
 
 class Semigroup (G : Type u) extends Mul G where

tests/lean/run/binop_binrel_perf_issue.lean

@@ -153,22 +153,10 @@ universe u v w
 class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hVAdd : α → β → γ
 
-class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  hSMul : α → β → γ
-
 class VAdd (G : Type u) (P : Type v) where
   vadd : G → P → P
 
-class SMul (M : Type u) (α : Type v) where
-  smul : M → α → α
-
 infixl:65 " +ᵥ " => HVAdd.hVAdd
-infixr:73 " • " => HSMul.hSMul
-
-macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
-
-instance instHSMul {α β} [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
 
 instance instHVAdd {α β} [VAdd α β] : HVAdd α β β where
   hVAdd := VAdd.vadd

tests/lean/run/dsimpNatLitIssue.lean

@@ -8,12 +8,6 @@ class Bot (α : Type) where
 /-- The bot (`⊥`, `\bot`) element -/
 notation "⊥" => Bot.bot
 
-/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
-class SMul (M α : Type) where
-  smul : M → α → α
-
-infixr:73 " • " => SMul.smul
-
 structure Submodule (R : Type) (M : Type) [Zero M] [SMul R M] where
   carrier : M → Prop
   zero_mem : carrier (0 : M)

tests/lean/run/linearCategory_perf_issue.lean

@@ -2,19 +2,6 @@ universe u v w v₁ v₂ v₃ u₁ u₂ u₃
 
 section Mathlib.Algebra.Group.Defs
 
-class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  hSMul : α → β → γ
-
-class SMul (M : Type u) (α : Type v) where
-  smul : M → α → α
-
-infixr:73 " • " => SMul.smul
-
-macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
-
-instance instHSMul {α β} [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
-
 class AddMonoid (M : Type u) extends Add M, Zero M where
   protected add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
   protected zero_add : ∀ a : M, 0 + a = a

tests/lean/run/nestedtc.lean

@@ -3,11 +3,6 @@ variable {R : Type}
 
 class Zip (α : Type) -- represents `Zero`
 
-class SMul (R : Type) (α : Type) where
-  smul : R → α → α
-
-infixr:73 " • " => SMul.smul
-
 class MulAction (R : Type) (β : Type) extends SMul R β
 
 class SMulZeroClass (R α : Type) extends SMul R α where

tests/lean/run/structWithAlgTCSynth.lean

@@ -101,17 +101,6 @@ end Mathlib.Logic.Function.Basic
 
 section Mathlib.Algebra.Group.Defs
 
-class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  hSMul : α → β → γ
-
-class SMul (M : Type _) (α : Type _) where
-  smul : M → α → α
-
-infixr:73 " • " => HSMul.hSMul
-
-instance instHSMul [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
-
 class Semigroup (G : Type u) extends Mul G where
   mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
 

tests/lean/run/synthInstsIssue.lean

@@ -4,23 +4,6 @@ https://github.com/leanprover/lean4/pull/2793.
 We find that we need to either specify a named argument or use `..` in certain rewrites.
 -/
 
-section Mathlib.Algebra.Group.Defs
-
-universe u v w
-
-class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  hSMul : α → β → γ
-
-class SMul (M : Type u) (α : Type v) where
-  smul : M → α → α
-
-infixr:73 " • " => HSMul.hSMul
-
-instance instHSMul {α β} [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
-
-end Mathlib.Algebra.Group.Defs
-
 section Mathlib.Data.FunLike.Basic
 
 class DFunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where