Stream: Coq users

Topic: Renaming hypothesis in inversion


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

Hi everyone,

I am trying to invert the hypothesis Ha but want to give them names Hb : x = y and Hc : xs = ys. Coq is happy to accept the one below but I don't know how to name the other.

Require Import List Utf8.
Import Notations.

Lemma inversion_name {A : Type} :
   (x y : A) (xs ys : list A), x :: xs = y :: ys -> x = y  xs = ys.
Proof.
  intros * Ha.
  inversion Ha as [Hb]. (* I can't rename the other one  here *)

Best,
Mukesh

view this post on Zulip Mukesh Tiwari (Oct 05 2023 at 14:04):

@Olivier Laurent Thanks! But how did you figure this out? I read the doc [1, 2] and looked at the example [3], and I understood that in my case the and_intropattern is required (inversion Ha as [Hb Hc]), or did I get something wrong?

[1] https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.inversion
[2] https://coq.inria.fr/refman/proof-engine/tactics.html#grammar-token-or_and_intropattern
[3] https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#inversion-intropattern-ex

view this post on Zulip Notification Bot (Oct 05 2023 at 15:01):

Paolo Giarrusso has marked this topic as unresolved.

view this post on Zulip Olivier Laurent (Oct 05 2023 at 15:34):

Mukesh Tiwari said:

Olivier Laurent Thanks! But how did you figure this out?

Not clear. As far as I remember I faced a similar problem and tried a bunch of possibilities rather than looking at the manual.
Random trials led me to find such patterns to give name to the generated hypotheses I wanted.

view this post on Zulip Pierre Castéran (Oct 05 2023 at 18:46):

While maintaining long proofs, I found it useful to add an option to inversion, decompose, etc. to get a behaviour like case, using Pierre Courtieu's library LibHyps.

From LibHyps Require Import LibHyps.

Tactic Notation (at level 4) tactic4(Tac) "/" "dr" :=
  Tac ; {< fun h => try generalize dependent h }.

Tactic Notation (at level 4) tactic4(Tac) "/" "r?" :=
  Tac ; {< fun h  => try revert h }.

Tactic calls like inversion H /r make it possible to control the names of the hypotheses to introduce.

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

Wait. Is that really a notation that can suffix any tactic4? Cool! I've never seen that work, or at level 4 written there!

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

But I don't quite understand what the spec is. Will this call revert/generalize dependent on all new hypotheses?

view this post on Zulip Pierre Castéran (Oct 06 2023 at 04:57):

This tactic notation was an answer by @Pierre Courtieu to a question after a talk about libhyps. If I remember well, it works with a continuation applied to the new hypotheses generated by a tactic.
I used it only with inversion and decompose record.

view this post on Zulip Pierre Courtieu (Oct 06 2023 at 08:52):

Hi. Yes it is a generic continuation tac ;{ tac2 } that applies tac and then applies tac2 to all hypothesis that was not there before applying tac (more precisely hypothesis of which names were not there before tac). The variant {< >} is the same but tac2 is applied once to the list of all new hypothesis. I felt the need of this mainly for efficiency reason.

view this post on Zulip Pierre Courtieu (Oct 06 2023 at 08:54):

Usual examples for tac2 are :


Last updated: Jun 23 2024 at 05:02 UTC