Zulip Chat Archive

Stream: maths

Topic: subring diamond


view this post on Zulip Johan Commelin (Mar 11 2019 at 15:44):

If you have a subring S of a comm_ring then:

is_subring S ---- subset.comm_ring ---> comm_ring S
   |                                        |
   | comm_ring.ring                         | comm_ring.ring
   v                                        v
is_subring S ---- subset.ring ----------> ring S

The downwards arrow on the left is taking place on the ambient ring.

view this post on Zulip Kevin Buzzard (Mar 11 2019 at 21:47):

Does that mean that one of these instances has to be removed? They're not defeq, right?

view this post on Zulip Mario Carneiro (Mar 11 2019 at 21:56):

it should be possible to make them defeq

view this post on Zulip Mario Carneiro (Mar 11 2019 at 21:57):

What is subset.comm_ring? If it extends subset.ring then this should work out

view this post on Zulip Johan Commelin (Mar 12 2019 at 09:44):

This is really confusing

set_option pp.all true

example {R : Type u} [comm_ring R] {S : set R} [is_subring S] :
  @comm_ring.to_ring S _ = @subset.ring R _ S _ := rfl -- works

example {R : Type u} [comm_ring R] {S : set R} [is_subring S] :
  @comm_ring.to_ring S _ = @subset.ring _ _ _ _ := rfl -- fails

If you replace the first rfl with _ you will see that the pp.all output is identical to what you get in the second example.

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:01):

Kenny had something like this recently, and I think it was caused by the elaborator doing things in a funny order.

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:02):

I don't have time to find the thread right now, but I suggested to Kenny that he start filling in the holes, and he was surprised to find that it fixed the problem. @Kenny Lau do you remember this thread?

view this post on Zulip Johan Commelin (Mar 12 2019 at 12:05):

Of course I don't mind filling in those holes if it's a one time thing. But it becomes a problem if type class search is the one who ought to be filling in the holes and just breaks down in tears saying it hit a diamond.

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:05):

Maybe some useful comments were made there

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:08):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/type.20mismatch

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:08):

It was just me and Kenny moaning about a similar issue

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:08):

I don't know what's going on

view this post on Zulip Kenny Lau (Mar 12 2019 at 12:09):

yeah no just fill in the blanks

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:09):

Is the conclusion that this is not a diamond after all?

view this post on Zulip Johan Commelin (Mar 12 2019 at 12:10):

Yes, I think that is the conclusion. Which only makes the situation worse.

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:10):

and the real problem is that we don't understand why rfl fails? [like we already didn't with Kenny's example]

view this post on Zulip Johan Commelin (Mar 12 2019 at 12:10):

Because now we can't fix it.

view this post on Zulip Johan Commelin (Mar 12 2019 at 12:11):

Because I have some ring hom, and I can't use it, because type class inference fails.

view this post on Zulip Johan Commelin (Mar 12 2019 at 12:11):

And then you need to put @s everywhere, and fill in lots of holes, and all of a sudden the code is unreadable

view this post on Zulip Johan Commelin (Mar 12 2019 at 12:12):

Anyway, Kevin, thanks for the link to that other thread. It's encouraging to know I'm not alone (-;

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:14):

It is actually possible to debug this sort of thing yourself, using the tricks Sebastian mentioned in the "leaves office again" thread. I've seen Kenny doing this live.

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:15):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unification/near/156841375

view this post on Zulip Kevin Buzzard (Mar 12 2019 at 12:16):

set_option pp.implicit true
set_option pp.notation false
set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

Last updated: May 14 2021 at 18:28 UTC