Zulip Chat Archive

Stream: new members

Topic: Equivalent of subtype.eq for structures?


view this post on Zulip Vincent Beffara (Nov 03 2019 at 23:49):

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

view this post on Zulip Chris Hughes (Nov 04 2019 at 00:14):

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

view this post on Zulip Mario Carneiro (Nov 04 2019 at 00:31):

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

view this post on Zulip Mario Carneiro (Nov 04 2019 at 00:32):

These kinds of theorems usually go by the name *_ext

view this post on Zulip Vincent Beffara (Nov 04 2019 at 00:33):

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

view this post on Zulip Mario Carneiro (Nov 04 2019 at 00:33):

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

view this post on Zulip Mario Carneiro (Nov 04 2019 at 00:34):

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

view this post on Zulip Vincent Beffara (Nov 04 2019 at 00:36):

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

view this post on Zulip Simon Hudon (Nov 04 2019 at 02:59):

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

view this post on Zulip Simon Hudon (Nov 04 2019 at 05:31):

Is this what you're looking for?

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

view this post on Zulip Vincent Beffara (Nov 04 2019 at 09:20):

Yes, exactly that.

view this post on Zulip Vincent Beffara (Nov 20 2019 at 10:56):

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?

view this post on Zulip Vincent Beffara (Nov 21 2019 at 13:32):

Even simpler version exhibiting the same message:

import tactic

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

#check dumb.ext

view this post on Zulip Johan Commelin (Nov 21 2019 at 13:37):

Hmm, weird

view this post on Zulip Kevin Buzzard (Nov 21 2019 at 13:38):

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

view this post on Zulip Johan Commelin (Nov 21 2019 at 13:40):

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

view this post on Zulip Rob Lewis (Nov 21 2019 at 13:44):

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

view this post on Zulip Simon Hudon (Nov 21 2019 at 13:55):

Thanks @Rob Lewis !


Last updated: May 17 2021 at 21:12 UTC