Zulip Chat Archive

Stream: general

Topic: New structures breaking definitional equality


Chris Hughes (Feb 12 2019 at 23:13):

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 (Feb 12 2019 at 23:59):

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 (Feb 13 2019 at 00:00):

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

Chris Hughes (Feb 13 2019 at 00:02):

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 (Feb 13 2019 at 00:02):

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

Chris Hughes (Feb 13 2019 at 00:28):

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 (Feb 13 2019 at 00:32):

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 (Feb 13 2019 at 00:37):

@Chris Hughes a surprising solution to your question:

Kenny Lau (Feb 13 2019 at 00:37):

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 (Feb 13 2019 at 00:37):

the solution is old_structure_cmd

Kenny Lau (Feb 13 2019 at 00:41):

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

Kevin Buzzard (Feb 13 2019 at 06:53):

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

Chris Hughes (Feb 13 2019 at 11:47):

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 (Feb 13 2019 at 17:25):

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

Mario Carneiro (Feb 13 2019 at 17:26):

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 (Feb 15 2019 at 10:41):

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 (Feb 15 2019 at 10:49):

it does work by defeq though

Mario Carneiro (Feb 15 2019 at 10:49):

i.e. just h proves this

Chris Hughes (Feb 15 2019 at 10:51):

Yeah, but that's not always convenient.

Mario Carneiro (Feb 15 2019 at 10:52):

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

Chris Hughes (Feb 15 2019 at 10:52):

Like old structures?

Mario Carneiro (Feb 15 2019 at 10:53):

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 (Feb 15 2019 at 10:53):

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

Mario Carneiro (Feb 15 2019 at 10:53):

so it really is a pack/unpack

Mario Carneiro (Feb 15 2019 at 10:53):

here it's an entirely superfluous pack/unpack

Chris Hughes (Feb 15 2019 at 10:55):

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 (Feb 15 2019 at 10:57):

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

Chris Hughes (Feb 15 2019 at 10:58):

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

Mario Carneiro (Feb 15 2019 at 10:58):

I don't think so...

Chris Hughes (Feb 15 2019 at 10:58):

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

Mario Carneiro (Feb 15 2019 at 10:59):

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

Mario Carneiro (Feb 15 2019 at 10:59):

including a' in the example

Mario Carneiro (Feb 15 2019 at 10:59):

so the rule is that these need to be defeq

Chris Hughes (Feb 15 2019 at 10:59):

If you want to never use rw

Mario Carneiro (Feb 15 2019 at 11:00):

you can have rw take a variable for this argument

Mario Carneiro (Feb 15 2019 at 11:01):

Alternatively, structure eta

Kevin Buzzard (Feb 15 2019 at 11:02):

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 (Feb 15 2019 at 11:02):

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

Chris Hughes (Feb 15 2019 at 11:02):

Otherwise it uses a non defeq comm_ring instance

Chris Hughes (Feb 15 2019 at 11:04):

It happens enough to be very annoying.


Last updated: Dec 20 2023 at 11:08 UTC