New structures breaking definitional equality

Stream: general

[Chris Hughes]

The last lemma here is hard to prove, and really should be defeq for type class inference to be useful. Is this a bug or user error? I think the use of macros maybe breaks it, since B.to_A is defined using a macro and not A.mk _, but I don't really know what I'm talking about.

class A (α : Type*) :=
(a : α)

class B (α : Type*) extends A α :=
(b : α)

class C (α : Type*) :=
(a : α)
(t : true)

instance C.to_A (α : Type*) [C α] : A α :=
{ ..show C α, by apply_instance }

instance B.to_C {α : Type*} [B α] : C α :=
{ t := trivial, .. show B α, by apply_instance }

example {α : Type*} [B α] : B.to_A α = C.to_A α := rfl

[Simon Hudon]

think the use of macros maybe breaks it, since B.to_A is defined using a macro and not A.mk _

That's not it. When you have extends A a, that gives B a to_A field of type A a

[Simon Hudon]

In the example, where is the C instance coming from?

[Chris Hughes]

In real life B is euclidean domain, C is integral domain and A is comm ring more or less. I'm getting rid of nonzero_comm_ring and replacing it with zero_ne_one_class' as discussed in

[Chris Hughes]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/semiring.20polynomials

[Chris Hughes]

I guess the difference is an eta expansion somewhere. This one works.

def B.to_A' (α : Type*) [n : B α] : A α :=
A.mk (B.to_A α).a

example {α : Type*} [n : B α] : B.to_A' α = C.to_A α := rfl

[Kenny Lau]

import tactic.interactive

class A (α : Type*) :=
(a : α)

class B (α : Type*) extends A α :=
(b : α)

class C (α : Type*) :=
(a : α)
(t : true)

instance C.to_A (α : Type*) [C α] : A α :=
{ ..show C α, by apply_instance }

instance B.to_C {α : Type*} [B α] : C α :=
{ t := trivial, .. show B α, by apply_instance }

example {α : Type*} [B α] : B.to_A α = C.to_A α :=
by unfreezeI; cases _inst_1; cases _to_A; refl

[Kenny Lau]

@Chris Hughes a surprising solution to your question:

[Kenny Lau]

set_option old_structure_cmd true

class A (α : Type*) :=
(a : α)

class B (α : Type*) extends A α :=
(b : α)

class C (α : Type*) :=
(a : α)
(t : true)

instance C.to_A (α : Type*) [C α] : A α :=
{ a := C.a α }

instance B.to_C {α : Type*} [B α] : C α :=
{ a := A.a α, t := trivial }

example {α : Type*} [B α] : B.to_A α = C.to_A α := rfl

[Kenny Lau]

the solution is old_structure_cmd

[Kenny Lau]

could this be the solution for the snailish elaboration of polynomials?

[Kevin Buzzard]

Will the old structure command still be there in Lean 4?

[Chris Hughes]

I'm not sure. This does look like a major problem with new structures right now. old_structure_cmd works in this example, but breaks in my use case, and I haven't managed to minimise that yet.

[Mario Carneiro]

I'm not sure why this is essential. Mostly we only need that projections work out to defeq, not the instances themselves

[Mario Carneiro]

it's actually pretty hard to get instances to work out since you almost always end up doing an unpacking and rebuilding step that would require eta for structures to undo

[Chris Hughes]

I'm not sure why this is essential. Mostly we only need that projections work out to defeq, not the instances themselves

This is why it's essential. There are more functions defined on a class than just it's projections

def a' {α : Type*} [A α] := A.a α

example {α : Type*} [n : B α] (x : α) (h : @a' _ (B.to_A α) = x) : @a' _ (C.to_A α) = x :=
by rw h -- doesn't work

[Mario Carneiro]

it does work by defeq though

[Mario Carneiro]

i.e. just h proves this

[Chris Hughes]

Yeah, but that's not always convenient.

[Mario Carneiro]

I'm not sure there is any good solution unless we unpack and repack the argument in B.to_A

[Chris Hughes]

Like old structures?

[Mario Carneiro]

instance B.to_A' (α : Type*) [B α] : A α := {..B.to_A α}

example {α : Type*} [n : B α] (x : α) (h : @a' _ (B.to_A' α) = x) : @a' _ (C.to_A α) = x :=
by rw h

[Mario Carneiro]

old structures have to do this because they don't have a field for it

[Mario Carneiro]

so it really is a pack/unpack

[Mario Carneiro]

here it's an entirely superfluous pack/unpack

[Chris Hughes]

Does this mean it is impossible to do classes that extend each other in complex ways using new structures. Something like monoid, comm_monoid, group, comm_group seems difficult to do with new structures without this issue.

[Mario Carneiro]

no, it just means that functions with dependencies like this will be difficult to work with

[Chris Hughes]

But that's quite a lot of functions though right?

[Mario Carneiro]

I don't think so...

[Chris Hughes]

Isn't it more or less any function on a monoid other than mul

[Mario Carneiro]

Functions are almost always defined in terms of projections out of the structure instance

[Mario Carneiro]

including a' in the example

[Mario Carneiro]

so the rule is that these need to be defeq

[Chris Hughes]

If you want to never use rw

[Mario Carneiro]

you can have rw take a variable for this argument

[Mario Carneiro]

Alternatively, structure eta

[Kevin Buzzard]

I think that my model of a "generic class" is something like a perfectoid space, and Mario's might be something very different.

[Chris Hughes]

Here's what I had to change to the proof that ED -> PID to principal := λ S, @is_principal.mk _ (id _) _.

[Chris Hughes]

Otherwise it uses a non defeq comm_ring instance

[Chris Hughes]

It happens enough to be very annoying.