Instance diamonds in ℤ-module structure of linear_map

Stream: general

[Eric Wieser]

How do I close this goal?

import linear_algebra.basic

variables {R M N : Type*} [ring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]

example (l : M →ₗ[R] N) (z : ℤ) (m : M) : (z • l) m = z • l m :=
begin
  haveI : smul_comm_class R ℤ N := smul_comm_class.symm _ _ _,
  convert linear_map.smul_apply l z m,
  sorry  -- mul_action.to_has_scalar = linear_map.has_scalar
end

In the presence of the smul_comm_class instance from docs#smul_comm_class.symm, there are now two semimodule ℤ structures on linear_map:

• docs#add_comm_group.int_module
• docs#linear_map.semimodule (which uses the add_comm_group.int_module : semimodul ℤ N)

Can priority fix this?

[Eric Wieser]

Seems it might be able to, at least in that tiny example. Let's see if #5365 works...

[Kevin Buzzard]

You're adding a loop into the instance search graph? Can this ever be right?

[Johan Commelin]

Kevin Buzzard said:

Can this ever be right?

When the future arrives :four_leaf_clover:

[Eric Wieser]

My other idea is to just swap the arguments in all users of smul_comm_class so that they match docs#int.smul_comm_class

[Eric Wieser]

With the idea that if you have an object T with an innate R-module structure (linear_map, tensor_product, etc), smul_comm_class S R T is the preferred order

[Eric Wieser]

I think the caching in the typeclass search makes this loop safe? My guess is that the behavior is:

• I need a smul_comm_class R1 R2 M
• Hey, I found .symm
  • I need a smul_comm_class R2 R1 M
  • Hey, I found .symm
    • I need a smul_comm_class R1 R2 M
    • Oh, I'm already looking for one of those, so prune this search branch

[Eric Wieser]

At any rate, by adding priority, the loop now only fires if an instance can't be found

[Eric Wieser]

Which is frustrating but not as frustrating as trying to prove instance equality

[Gabriel Ebner]

Eric Wieser said:

I think the caching in the typeclass search makes this loop safe? My guess is that the behavior is:

• I need a smul_comm_class R1 R2 M
• Hey, I found .symm
  • I need a smul_comm_class R2 R1 M
  • Hey, I found .symm
    • I need a smul_comm_class R1 R2 M
    • Oh, I'm already looking for one of those, so prune this search branch

It wouldn't be hard to implement this, but it is not implemented in Lean 3.

[Gabriel Ebner]

The reason why I didn't implement it (and why I'm a bit skeptical about the Lean 4 version) is that it seems very fragile: smul_comm_class has two type-class parameters, and there are usually many ways to write the same instances (thus defeating the loop detection).

[Eric Wieser]

By"many ways", do you mean "with instances that are defeq but not syntactically equal"?

[Eric Wieser]

Assuming the linked PR passes CI, is the loop still a deal-breaker?

[Mario Carneiro]

I think there is a linter for this, so it shouldn't pass CI

[Eric Wieser]

Maybe the solution to my original problem is to make the symm instances available only for nat and int, rather than for all types

[Mario Carneiro]

Where does smul_comm_class get involved here? The two linear map structures don't mention it

[Mario Carneiro]

I think add_comm_group.int_module is a little dubious as a global instance, it can be selectively introduced

[Eric Wieser]

Mario Carneiro said:

Where does smul_comm_class get involved here? The two linear map structures don't mention it

What do you mean? It's the last item in the signature of docs#linear_map.semimodule

[Mario Carneiro]

nat.smul_comm_class can have a commuted instance

[Mario Carneiro]

maybe this is what you mean

[Eric Wieser]

Mario Carneiro said:

nat.smul_comm_class can have a commuted instance

That's what I meant by "Maybe the solution to my original problem is to ...", yes

[Sebastien Gouezel]

Isn't the right solution to fix the definition of multiplication on nat and int so that the instances are defeq?

[Eric Wieser]

I suppose that could fix the diamond, although I'd still have to use the haveI.

Is there any way to unfold the goal in my top-most post to see what currently _isn't_ defeq?

[Eric Wieser]

Mario Carneiro said:

I think there is a linter for this, so it shouldn't pass CI

It passes CI - github lied to me, and didn't show me the lint run at all

[Eric Wieser]

Sure enough, it fails the linter

[Eric Wieser]

Mario Carneiro said:

nat.smul_comm_class can have a commuted instance

Done in #5369, hopefully the linter is happy with that

[Eric Wieser]

With that merged, the original problem doesn't exist - and it turns out that docs#module.gsmul_eq_smul can close the diamond if it's forced to appear, as with:

import linear_algebra.basic

variables {R M N : Type*} [ring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]

example (l : M →ₗ[R] N) (z : ℤ) (m : M) : (z •ℤ l) m = z • l m :=
begin
  convert linear_map.smul_apply l z m,
  -- rw gsmul_eq_smul, -- does not close the goal
  rw module.gsmul_eq_smul, -- closes the goal
end