subgroup set coercion

Stream: maths

[Patrick Massot]

Here is a little type class failure experiment. In a Lean file, write:

import algebra.module

variables {A : Type*} [comm_ring A] (S : submodule ℤ A)

#check (↑S : set A)

#check (S : set A)

Both check succeed instantly. Now replace the first line by import ring_theory.algebra. The second check times out.

[Patrick Massot]

Next, create a dummy copy of ring_theory.algebra where the instance on https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/algebra.lean#L537 is only a local instance. Then both checks succeed, but the second one is very slow.

[Patrick Massot]

What should we do?

[Mario Carneiro]

what does the trace look like?

[Patrick Massot]

It looks bad

[Patrick Massot]

Do you mean the trace that works quickly, the one that works slowly or the one that fail?

[Mario Carneiro]

both, what is the difference?

[Mario Carneiro]

I am guessing that it has to do with has lift vs has coe

[Patrick Massot]

failure at https://pastebin.com/b9rgT8v7

[Patrick Massot]

fast success at https://pastebin.com/D804HUNU

[Patrick Massot]

Note how the lovely successful one still ends up in (message too long, truncated at 262144 characters)

[Patrick Massot]

After 3662 lines

[Patrick Massot]

And let me conjecture we have a little problem anyway.

[Patrick Massot]

So, any idea? Anyone?

[Mario Carneiro]

I think it's just a big instance problem

[Mario Carneiro]

and it has the usual exponential blowup stuff

[Mario Carneiro]

Note that the added import both significantly increases the number of available instances and also changes the type of the problem:
before:

has_coe_to_fun
  (@submodule ℤ A
     (@domain.to_ring ℤ
        (@to_domain ℤ
           (@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
              (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
                 int.decidable_linear_ordered_comm_ring))))
     (@ring.to_add_comm_group A (@comm_ring.to_ring A _inst_1))
     (@add_comm_group.module A (@ring.to_add_comm_group A (@comm_ring.to_ring A _inst_1))))

after:

has_coe_to_fun
  (@submodule ℤ A
     (@domain.to_ring ℤ
        (@to_domain ℤ
           (@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
              (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
                 int.decidable_linear_ordered_comm_ring))))
     (@ring.to_add_comm_group A (@comm_ring.to_ring A _inst_1))
     (@algebra.module ℤ A
        (@nonzero_comm_ring.to_comm_ring ℤ (@euclidean_domain.to_nonzero_comm_ring ℤ int.euclidean_domain))
        (@comm_ring.to_ring A _inst_1)
        (@algebra_int A _inst_1)))

[Mario Carneiro]

I think it's probably not good that the proof of module ℤ A changes to this more complicated one after the import

[Mario Carneiro]

we really need to think about using instance priorities in a systematic and coherent way across the library

[Patrick Massot]

I don't even understand how we get a has_coe_to_fun search

[Mario Carneiro]

I think it's because set A is a function type

[Patrick Massot]

How weird

[Mario Carneiro]

I agree, I would have expected a has_coe

[Johan Commelin]

Should set be irreducible?

[Johan Commelin]

That would prevent a lot of defeqness that we currently depend on...

[Johan Commelin]

Doesn't sound good

[Mario Carneiro]

no, I think that's a bad idea

[Mario Carneiro]

it might work in principle but there isn't a strong argument for the distinction and we occasionally make use of the defeqness

[Patrick Massot]

At least this explains why using a (↑S : set A) works better than (S : set A)