Stream: Coq users

Topic: ✔ Renaming hypothesis in inversion


view this post on Zulip Gaëtan Gilbert (Oct 05 2023 at 13:05):

inversion accepts as but it's hard to tell what it does with it
injection may be more predictable

view this post on Zulip Mukesh Tiwari (Oct 05 2023 at 13:08):

You mean the proper way to go is something like this?

Lemma inversion_name {A : Type} :
   (x y : A) (xs ys : list A), x :: xs = y :: ys -> x = y  xs = ys.
Proof.
  intros * Ha.
  injection Ha; intros Hb Hc.

view this post on Zulip Gaëtan Gilbert (Oct 05 2023 at 13:08):

probably
the typical use of inversion goes like inversion; subst; some automation tactic I think

view this post on Zulip Mukesh Tiwari (Oct 05 2023 at 13:10):

Thanks @Gaëtan Gilbert ! While you are here, what is that pragma that forces you to rename all your assumption and not let Coq chose it?

view this post on Zulip Gaëtan Gilbert (Oct 05 2023 at 13:13):

Set Mangle Names?

view this post on Zulip Mukesh Tiwari (Oct 05 2023 at 13:15):

Yeah, Mangle Names. Thanks again!

view this post on Zulip Notification Bot (Oct 05 2023 at 13:16):

Mukesh Tiwari has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Oct 05 2023 at 13:20):

@Mukesh Tiwari usually, I just pass more names than you expect to inversion and see what it does with it :-). But you're right, here inversion Ha as [Hb A]. gives Unexpected introduction pattern: A.

view this post on Zulip Olivier Laurent (Oct 05 2023 at 13:46):

Both
inversion Ha as [[Hb Hc]].
and
injection Ha as [= Hb Hc].
do the job here.


Last updated: Jun 18 2024 at 21:01 UTC