I can't use an implicit argument. What else can I do?

Stream: lean4

[Mitchell Lee]

I am currently working on the theory of Coxeter groups. The specifics aren't important; what's important is that for every matrix M : Matrix B B ℕ, we have a group CoxeterGroup M. I have also defined a function wordProd that takes as input a List B and outputs an element of CoxeterGroup M; see below.

import Mathlib.Data.Matrix.Notation
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.SpecificGroups.Coxeter

namespace CoxeterGroup

open List Matrix
variable {B : Type*} [DecidableEq B]
variable (M : Matrix B B ℕ)

def simpleReflection (i : B) : CoxeterGroup M := PresentedGroup.of i
def wordProd (ω : List B) : CoxeterGroup M := prod (map (simpleReflection M) ω)

@[simp] theorem wordProd_append (ω ω' : List B) :
    wordProd M (ω ++ ω') = (wordProd M ω) * (wordProd M ω') := by
  sorry

end CoxeterGroup

Now, let's say that I am planning to have many more theorems like wordProd_append in the same file. I don't want to type wordProd M ω every time I use the wordProd function; I would rather type something like wordProd ω or π ω or something similar. This should be fine because the matrix M is "staying the same" throughout the section.

(The equivalent in informally written mathematics would be something like "Fix a matrix M, and let π = π_M be the associated word product function". From then on, I could just write π and it would be understood to mean π_M.)

Normally, I would accomplish this by making the argument M implicit in wordProd. However, I can't do that here. The problem is that Lean does not have any way to infer the implicit argument, because the only other place that M appears in the signature of wordProd is in the return type.

What are my options?

[Joël Riou]

If M is declared as {M}, then you should be able to write wordProd ω : CoxeterGroup M or wordProd (M := M) ω (warning: untested). However, in this particular situation, instead of using the type CoxeterGroup M, I would suggest using cs : CoxeterSystem M W as a variable (and use dot notation, like cs.wordProd ...), so that the API applies not only to the group CoxeterGroup M but to any group W that is part of a Coxeter system.

[Raghuram]

Incidentally, (independent of the suggestion above) Lean 3 used to have a command just for this: parameter. I don't know whether any analogue has been implemented in Lean 4 / Mathlib4.

[Kyle Miller]

The only analogue is making a local notation, which works since local notations are allowed to refer to variables

[Mitchell Lee]

Thanks for the suggestions.

I have tried multiple ways to make the argument M implicit. I have gotten it to work by doing this:

import Mathlib.Data.Matrix.Notation
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.SpecificGroups.Coxeter

namespace CoxeterGroup

open List Matrix
variable {B : Type*} [DecidableEq B]
variable {M : Matrix B B ℕ}

def simpleReflection (i : B) : CoxeterGroup M := PresentedGroup.of i
def wordProd (ω : List B) : CoxeterGroup M := prod (map simpleReflection ω)

@[simp] theorem wordProd_append (ω ω' : List B) :
    wordProd (M := M) (ω ++ ω') = (wordProd (M := M) ω) * (wordProd (M := M) ω') := by
  sorry

end CoxeterGroup

I can do the same thing with a type annotation on each use of wordProd. But, of course, this is even more cumbersome than writing just writing wordProd M ω. Removing any one of the occurrences of (M := M)or any one of the type annotations yields an error message:

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

I don't know whether this is intended behavior.

The notation idea is working great, though. Thank you for the suggestion.

[Mitchell Lee]

Yes, it does seem like I really want something like parameter, though.