failed to synthesize HMul

Stream: general

[Alessandro Pinto]

Hello,

I have the following lean4 definitions:

import Mathlib.Data.Matrix.Basic

class Flow (α : Type) (n: Nat) where
  f :  (Matrix (Fin n) (Fin 1) α) → (Matrix (Fin n) (Fin 1) α)

/-- Linear Flow --/
instance LinearRealFlow {n:Nat} (A: Matrix (Fin n) (Fin n) ℝ): Flow ℝ n where
  f v :=  A * v

However, an error is reported about A * v:

failed to synthesize
  HMul (Matrix (Fin n) (Fin n) ℝ) (Matrix (Fin n) (Fin 1) ℝ) ?m.1734

It seems that the type of the range of f could not be inferred. However, it is specified in the Flow class.
The definition of HMul is in the Mathlib.Data.Matric.Basic.lean file:

@[default_instance 100]
instance [Fintype m] [Mul α] [AddCommMonoid α] :
    HMul (Matrix l m α) (Matrix m n α) (Matrix l n α) where
  hMul M N := fun i k => (fun j => M i j) ⬝ᵥ fun j => N j k

The last type Matrix l n α is not defined as an output. I am wondering if that could be the cause of the problem, or if there is something obvious that I can't see in the very simple lean4 code above.

Thank you very much.

[Kevin Buzzard]

If you put set_option autoImplicit false you'll see the problem. This footgun is a common problem when doing mathematics (although it's a great option for more CS-related projects) and I have autoImplicit switched off in all my projects.

[Alessandro Pinto]

Thank you, Kevin. I tried the option you mentioned, but I got the same error, unfortunately.

[Kevin Buzzard]

Oh maybe you need relaxedAutoImplicit false as well? I also have this set locally on all my projects. To put you out of your misery, the issue with your code is that you are not importing the real numbers, so Lean interprets ℝ as "the user wants to create a random new type with this name", and thus it can't find a Mul on it.

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Real.Basic

class Flow (α : Type) (n: Nat) where
  f :  (Matrix (Fin n) (Fin 1) α) → (Matrix (Fin n) (Fin 1) α)

/-- Linear Flow --/
instance LinearRealFlow {n:Nat} (A: Matrix (Fin n) (Fin n) ℝ): Flow ℝ n where
  f v :=  A * v

works fine for me.

[Kevin Buzzard]

PS on the live web editor (which does have the footguns enabled)

import Mathlib.Data.Matrix.Basic
set_option autoImplicit false

class Flow (α : Type) (n: Nat) where
  f :  (Matrix (Fin n) (Fin 1) α) → (Matrix (Fin n) (Fin 1) α)

/-- Linear Flow --/
instance LinearRealFlow {n:Nat} (A: Matrix (Fin n) (Fin n) ℝ): Flow ℝ n where
  f v :=  A * v

does give the error I expected you to see -- unknown identifier 'ℝ'

[Eric Wieser]

There's no need to touch relaxedAutoImplicit if you set_option autoImplicit false

[Alessandro Pinto]

Thank you very much, @Kevin Buzzard and @Eric Wieser!