Zulip Chat Archive

Stream: maths

Topic: subgroup set coercion


view this post on Zulip Patrick Massot (Sep 20 2019 at 12:46):

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.

view this post on Zulip Patrick Massot (Sep 20 2019 at 12:47):

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.

view this post on Zulip Patrick Massot (Sep 20 2019 at 12:48):

What should we do?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 13:03):

what does the trace look like?

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:04):

It looks bad

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:04):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 13:05):

both, what is the difference?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 13:06):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:09):

failure at https://pastebin.com/b9rgT8v7

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:10):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:11):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:11):

After 3662 lines

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:12):

And let me conjecture we have a little problem anyway.

view this post on Zulip Patrick Massot (Sep 20 2019 at 17:24):

So, any idea? Anyone?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:14):

I think it's just a big instance problem

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:14):

and it has the usual exponential blowup stuff

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:16):

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)))

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:17):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:18):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 18:18):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:19):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 18:20):

How weird

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:20):

I agree, I would have expected a has_coe

view this post on Zulip Johan Commelin (Sep 20 2019 at 18:32):

Should set be irreducible?

view this post on Zulip Johan Commelin (Sep 20 2019 at 18:32):

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

view this post on Zulip Johan Commelin (Sep 20 2019 at 18:32):

Doesn't sound good

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:42):

no, I think that's a bad idea

view this post on Zulip Mario Carneiro (Sep 20 2019 at 18:42):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 19:27):

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


Last updated: May 10 2021 at 08:14 UTC