Stream: Coq users

Topic: Destruct product type equality?


view this post on Zulip Guillaume Dubach (Oct 31 2020 at 09:10):

Is there a one-tactic way of replacing "h: (a1,b1)=(a2,b2)" (for a given product type A*B) by "ha: a1=a2" and "hb: b1=b2" in the context? destruct does not work. I have a way to do this in several steps but it doesn't look optimal...

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 10:01):

injection h. Or injection h as as [= [ha hb]]?

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 10:02):

or ssreflect's "move: h => [ha hb]", which is basically the same syntax as for ssreflect's destruct

view this post on Zulip Guillaume Dubach (Oct 31 2020 at 16:54):

@Paolo Giarrusso Got it. Thank you very much!


Last updated: Feb 06 2023 at 12:04 UTC