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

@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

Paolo Giarrusso has marked this topic as unresolved.

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.

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.

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

written there!

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

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`

.

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.

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