subring diamond

Stream: maths

[Johan Commelin]

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]

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

[Mario Carneiro]

it should be possible to make them defeq

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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]

Maybe some useful comments were made there

[Kevin Buzzard]

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

[Kevin Buzzard]

It was just me and Kenny moaning about a similar issue

[Kevin Buzzard]

I don't know what's going on

[Kenny Lau]

yeah no just fill in the blanks

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

Because now we can't fix it.

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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