## Stream: general

### Topic: Instance diamonds in ℤ-module structure of linear_map

#### Eric Wieser (Dec 14 2020 at 10:28):

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:

Can priority fix this?

#### Eric Wieser (Dec 14 2020 at 10:45):

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

#### Kevin Buzzard (Dec 14 2020 at 10:56):

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

#### Johan Commelin (Dec 14 2020 at 10:57):

Kevin Buzzard said:

Can this ever be right?

When the future arrives :four_leaf_clover:

#### Eric Wieser (Dec 14 2020 at 11:08):

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 (Dec 14 2020 at 11:09):

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 (Dec 14 2020 at 12:01):

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 (Dec 14 2020 at 12:02):

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

#### Eric Wieser (Dec 14 2020 at 12:02):

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

#### Gabriel Ebner (Dec 14 2020 at 12:17):

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 (Dec 14 2020 at 12:18):

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 (Dec 14 2020 at 12:27):

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

#### Eric Wieser (Dec 14 2020 at 12:39):

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

#### Mario Carneiro (Dec 14 2020 at 12:39):

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

#### Eric Wieser (Dec 14 2020 at 12:41):

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 (Dec 14 2020 at 12:43):

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

#### Mario Carneiro (Dec 14 2020 at 12:44):

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

#### Eric Wieser (Dec 14 2020 at 12:46):

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 (Dec 14 2020 at 12:46):

nat.smul_comm_class can have a commuted instance

#### Mario Carneiro (Dec 14 2020 at 12:46):

maybe this is what you mean

#### Eric Wieser (Dec 14 2020 at 12:47):

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 (Dec 14 2020 at 12:59):

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

#### Eric Wieser (Dec 14 2020 at 13:12):

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 (Dec 14 2020 at 13:15):

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 (Dec 14 2020 at 14:28):

Sure enough, it fails the linter

#### Eric Wieser (Dec 14 2020 at 15:53):

Mario Carneiro said:

nat.smul_comm_class can have a commuted instance

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

#### Eric Wieser (Dec 17 2020 at 17:17):

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


Last updated: May 09 2021 at 19:11 UTC