Zulip Chat Archive

Stream: general

Topic: Instance diamonds in ℤ-module structure of linear_map


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Dec 14 2020 at 10:56):

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

view this post on Zulip Johan Commelin (Dec 14 2020 at 10:57):

Kevin Buzzard said:

Can this ever be right?

When the future arrives :four_leaf_clover:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 14 2020 at 12:02):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Eric Wieser (Dec 14 2020 at 12:27):

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

view this post on Zulip Eric Wieser (Dec 14 2020 at 12:39):

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

view this post on Zulip Mario Carneiro (Dec 14 2020 at 12:39):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 14 2020 at 12:46):

nat.smul_comm_class can have a commuted instance

view this post on Zulip Mario Carneiro (Dec 14 2020 at 12:46):

maybe this is what you mean

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 14 2020 at 14:28):

Sure enough, it fails the linter

view this post on Zulip 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

view this post on Zulip 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