Equivalent of subtype.eq for structures?

Stream: new members

[Vincent Beffara]

Hi,

subtype.eq shows that two members of a subtype with the same val are equal, is there something similar for structures (typically, a tactic that transforms a goal which states the equality of two structures into a list of goals, one for each non-Prop field)?

[Chris Hughes]

Sadly no, the closest would be subtype.mk.inj, a version of which is generated for all structures.

[Mario Carneiro]

I could have sworn there was a tactic for this, that Scott petitioned for and Simon wrote, although I forget the name

[Mario Carneiro]

These kinds of theorems usually go by the name *_ext

[Vincent Beffara]

subtype.mk.inj feels like it goes in the wrong direction

[Mario Carneiro]

Maybe I'm just thinking of the ext tactic, which applies @[extensionality] lemmas. But you have to state the theorem for your structure.

[Mario Carneiro]

luckily it's pretty easy to prove: case on the two structures, then congr; assumption

[Vincent Beffara]

Yes, that's more or less what I am doing, it works well enough

[Simon Hudon]

I remember receiving the request but I don't think I wrote it yet

[Simon Hudon]

Is this what you're looking for?

https://github.com/leanprover-community/mathlib/pull/1645

[Vincent Beffara]

Yes, exactly that.

[Vincent Beffara]

So this landed in mathlib, great, thanks a lot! I have a small issue though, this code:

import tactic

inductive toto (V : Type) : Type | P : V -> toto

def head {V : Type} : toto V -> V | (toto.P v) := v

@[ext] structure toto' (V : Type) (x : V) := (l : toto V) (hx : head l = x)

#check toto'.ext

tells me error: tactic failed, there are no goals to be solved on the line with the @[ext] (but otherwise it works, toto'.ext is generated and correct). One more case of lean being too clever?

[Vincent Beffara]

Even simpler version exhibiting the same message:

import tactic

@[ext] structure dumb (V : Type) := (val : V)

#check dumb.ext

[Johan Commelin]

Hmm, weird

[Kevin Buzzard]

I am lost. What's the question here? Is @[ext] a thing? Oh I see, it's a new thing

[Johan Commelin]

@Simon Hudon It looks like @[ext] is going through some growing pains...

[Rob Lewis]

https://github.com/leanprover-community/mathlib/pull/1721

[Simon Hudon]

Thanks @Rob Lewis !