## Stream: Coq users

### Topic: Renaming hypothesis in inversion

#### 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

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

#### Notification Bot (Oct 05 2023 at 15:01):

Paolo Giarrusso has marked this topic as unresolved.

#### 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.

#### 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.

#### 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!

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

#### 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`.

#### 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.

#### Pierre Courtieu (Oct 06 2023 at 08:54):

Usual examples for `tac2` are :

• revert
• try subst with this hyp
• try subst and revert otherwise
• rename automatically

Last updated: Jun 23 2024 at 05:02 UTC