## Stream: maths

### Topic: subring diamond

#### 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.

#### 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?

#### Mario Carneiro (Mar 11 2019 at 21:56):

it should be possible to make them defeq

#### Mario Carneiro (Mar 11 2019 at 21:57):

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

#### 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.

#### 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.

#### 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?

#### 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.

#### Kevin Buzzard (Mar 12 2019 at 12:08):

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

#### Kevin Buzzard (Mar 12 2019 at 12:08):

It was just me and Kenny moaning about a similar issue

#### Kevin Buzzard (Mar 12 2019 at 12:08):

I don't know what's going on

#### Kenny Lau (Mar 12 2019 at 12:09):

yeah no just fill in the blanks

#### Kevin Buzzard (Mar 12 2019 at 12:09):

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

#### Johan Commelin (Mar 12 2019 at 12:10):

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

#### 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]

#### Johan Commelin (Mar 12 2019 at 12:10):

Because now we can't fix it.

#### 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.

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

#### 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 (-;

#### 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.

#### Kevin Buzzard (Mar 12 2019 at 12:15):

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

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