inferring arguments for FunLike classes

Stream: mathlib4

[David Loeffler]

If I define a function which depends on some implicit parameters, and then I apply my function to something, Lean will try to figure out the implicit arguments from the types of the explicit ones.

However, when I define, rather than a function, some bundled FunLike thing, it seems that this doesn't apply: the implicit-parameter inference process doesn't "see through" the coercion-to-a-function operation. Is there a way of getting around this?

To be much more concrete: the following works, to define the "shift operator" that sends a function f : A → B to the function a ↦ f (a + 1), where A is a ring and B an abelian addgroup:

variable {A B : Type*} [Ring A] [AddCommGroup B]

/-- Shift-by-1 operator -/
def shift (f : A → B) := fun a ↦ f (a + 1)

variable (f : A → B) in
#check shift f -- works

Here the types A and B are implicit parameters to shift, but it can correctly deduce these from the type of f. However, if I define shiftₗ to be the same thing bundled as a linear operator on functions, not just a bare map, it seems to be unable to use f to figure out the type arguments to shiftₗ:

variable {A B : Type*} [Ring A] [AddCommGroup B]

/-- Shift-by-1 operator bundled as `ℤ`-linear endomorphism -/
def shiftₗ : Module.End ℤ (A → B) where
  toFun f a := f (a + 1)
  map_add' f g := by ext; simp
  map_smul' r f := by ext; simp

variable (f : A → B) in
#check shiftₗ f -- fails: function expected ... term has type Module.End ℤ (?m.5014 → ?m.5015)

variable (f : A → B) in
#check @shiftₗ A B _ _ f -- works, but ugly

Is there some clever hack that will allow me to write shiftₗ f without explicitly giving the types?

[Jireh Loreaux]

I've seen this kind of thing, before, but not for a long time. I think it's something to do with linear maps specifically. Note that the same problem does not exist if you make shiftₗ and AddMonoidHom, for instance.

[David Loeffler]

Interesting! It does indeed work bundled as an AddMonoidHom. Unfortunately I really do need to bundle it in some way that gives a ring structure, since I want to write things like (shiftₗ - 1)^7 f.

[Jireh Loreaux]

certainly, I'm not saying that you shouldn't be able to have the linear map version, I'm just trying to help narrow down where the problem occurs, because Lena definitely should be able to do this. I had similar issues about 10 months ago with star algebra homomorphisms, because those went away (I don't recall what the fix was, but I didn't implement it), so I'm surprised it's back.

[David Loeffler]

(the motivation here is to get Newton's formula for forward differences by applying the binomial theorem inside the ring Module.End ℤ (A → B).)

[David Loeffler]

Another remark about this: oddly, for shiftₗ applied to a function A → B, it seems to be able to figure out A, but not B: that is,

#check shiftₗ (A := A) f  -- fails
#check shiftₗ (B := B) f  -- works

[Kenny Lau]

so I would like to revive this thread. Basically, consider the following situation:

import Mathlib
variable {R A B : Type*} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

axiom f : A →ₐ[R] B
noncomputable example : A →ₗ[R] B := f

axiom g : A →+* B
noncomputable example : A →+ B := g

Basically, when we have different FunLike classes, with implicit arguments (R, A, B in the above examples), Lean struggles to infer the arguments. There are several work-arounds, but most of them require some more keystrokes than I would like (see code below). They don't even all produce the same result (see tests below).

So, I wonder what can be done to solve this problem. One solution I've come up with is more metaprogramming, so for example class(f) would hopefully infer the correct arguments. Do you guys have more suggestions?

PS: I would like to stress that moving to FunLike was a good thing in general and I thank all the involved parties for that, this is just a minor issue in comparison with the advantages of switching to FunLike.

[Kenny Lau]

Full test:

import Mathlib

namespace Test1

variable {R A B : Type*} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

axiom f : A →ₐ[R] B

noncomputable example : A →ₗ[R] B :=
  f

noncomputable def foo1 : A →ₗ[R] B :=
  (f : A →ₐ[R] B)

noncomputable def foo2 : A →ₗ[R] B :=
  LinearMapClass.linearMap f

noncomputable def foo3 : A →ₗ[R] B :=
  f.toLinearMap

#print foo1
#print foo2
#print foo3

example : foo1 (R := R) (A := A) (B := B) = foo2 := by simp? [foo1, foo2]
example : foo1 (R := R) (A := A) (B := B) = foo3 := by simp? [foo1, foo3]
example : foo2 (R := R) (A := A) (B := B) = foo3 := by simp? [foo2, foo3]

end Test1

namespace Test2

variable {A B : Type*} [CommRing A] [CommRing B]

axiom g : A →+* B

noncomputable example : A →+ B :=
  g

noncomputable def foo1 : A →+ B :=
  (g : A →+* B)

noncomputable def foo2 : A →+ B :=
  AddMonoidHomClass.toAddMonoidHom g

noncomputable def foo3 : A →+ B :=
  g.toAddMonoidHom

#print foo1
#print foo2
#print foo3

example : foo1 (A := A) (B := B) = foo2 := by simp? [foo1, foo2]
example : foo1 (A := A) (B := B) = foo3 := by simp? [foo1, foo3]
example : foo2 (A := A) (B := B) = foo3 := by simp? [foo2, foo3]

end Test2

[Kenny Lau]

I think another angle of attack might be more simp lemmas. As the examples demonstrate, in the second set of tests, even though #print produces different results, there were simp lemmas to link them all together, whereas all three simps in the first set of tests fail. Perhaps it wouldn't be as much of a problem if they are all simpable.

[Kenny Lau]

Summary of my ideas:

1. a tactic like class(f) to solve everything
2. more simp lemmas to connect the different workarounds

[Kenny Lau]

@Aaron Liu what do you think?

[Aaron Liu]

There are too many kinds of bundled maps

[Aaron Liu]

It's the casting problem

[Kenny Lau]

actually, there are enough simp lemmas to make the first test set pass if I use ext.

[Kenny Lau]

which is... still not good actually

[Aaron Liu]

the problem is, if you have a linear tower of $n$ types, you need $n(n-1)/2$ many casts between them, and you need $n(n-1)(n-2)/6$ many simp lemmas to collapse two casts into one

[Kenny Lau]

/poll What is the correct spelling of f : A →ₐ[R] B but as A →ₗ[R] B?
↑f.toLieHom
LinearMapClass.linearMap f
f.toLinearMap

[Kenny Lau]

Aaron Liu said:

the problem is, if you have a linear tower of $n$ types, you need $n(n-1)/2$ many casts between them, and you need $n(n-1)(n-2)/6$ many simp lemmas to collapse two casts into one

what if we just went the opposite way and use n casts

[Aaron Liu]

that's certainly an option

[Aaron Liu]

but remember at the bottom of this tower is DFunLike

[Aaron Liu]

and sometimes it's not a linear tower

[Kenny Lau]

oh no, diamonds

[Aaron Liu]

we have ContinuousMap and LinearMap and ContinuousLinearMap so there's some sort of diamond-shape happening here

[Kenny Lau]

surely we can just pick one to be more canonical right

[Aaron Liu]

that doesn't always work great

[Kenny Lau]

btw perhaps unrelatedly my code is taking like seconds to compile, like each definition

[Kenny Lau]

im gonna crash out