Many Coq tactics such as `destruct`

and `inversion`

can be used as `inversion N`

to invert the Nth term on the goal. How can I write a wrapper around them that does the same? e.g. I want to write a wrapper around `inversion`

that does some extra things like `subst`

, but still supports both `inversion H`

and `inversion 1`

.

(I'd be okay *implementing* such a tactic in Ltac2, but it is fundamentally required that the tactic can be called directly from Ltac1)

I found the `int_or_var`

tactic notation argument class, but it says that's the same as for `do`

, so it's probably not the `ident|natural`

that I want here

filed a feature request: https://github.com/coq/coq/issues/18167

At least for `ident | natural`

, overloading the tactic seems to work?

```
Tactic Notation "my_inversion" int_or_var(n) := idtac "got int"; inversion n.
Tactic Notation "my_inversion" ident(c) := idtac "got ident"; inversion c.
Lemma test (A B C D : Prop) : A /\ B -> B /\ C -> C /\ D -> C.
Proof.
my_inversion 3. Undo 1.
intros H1 H2. my_inversion H1.
Fail my_inversion True.
Abort.
```

that seems to work, thanks!

However, now I have the next problem... the point of the tactic is to clear the term being inverted. `inversion 1`

introduces a new term under some fresh name which we hence should clear. but I don't think there is a way to tell Coq which name to use?

Currently it seems like we have to completely re-implement the logic for "invert the n-th term", but maybe there is some clever way to reuse the logic from the core tactics?

Ralf Jung said:

However, now I have the next problem... the point of the tactic is to clear the term being inverted.

`inversion 1`

introduces a new term under some fresh name which we hence should clear. but I don't think there is a way to tell Coq which name to use?

Currently it seems like we have to completely re-implement the logic for "invert the n-th term", but maybe there is some clever way to reuse the logic from the core tactics?

You can try to use or take ideas from my library LibHyps. There is a tactical "tac1; { tac2 }" that applies tac1 and then tac2 to "new" hyps i.e. hyps having names that wern't there before tac1 was applied).

Here is a solution with `LibHyps`

. Several points:

- first intros until n, so that the the last introduced hyps is the one you want to inverse.
- get the list of all new hyps
- only apply inversion + clear to the last introduced hyps.

```
Require Import LibHyps.LibHyps.
Tactic Notation "my_inversion" ident(c) := idtac "got ident"; inversion c.
(* Apply tac ont he first hypothesis of the list l. *)
Ltac onFirstHyp tac l :=
match l with
@DCons _ ?H _ => inversion H;clear H
| _ => idtac "vide"
end.
Tactic Notation "my_inversion" int_or_var(n) :=
idtac "got int";
(* tactical ;{!< tac } applies on the list of new hyps in order
"newest first", so the the first hyp is actually the last introduced. *)
intros until n; {!< onFirstHyp ltac:(fun h => (inversion h; clear h))}.
```

Well actually this also works without LibHyps:

```
intros until n;
(match goal with
H: _ |- _ => (inversion H; clear H)
end).
```

`intros until`

is new to me, Im going to check that out, thanks!

oh wait, the actual magic is `match goal`

here. this relies on hypothesis match order, doesn't it?

is that guaranteed? I can't see it in https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.match-goal

ah it is

Hypothesis matching for match_hyps normally begins by matching them from left to right, to hypotheses, last to first.

@Pierre Courtieu that seems to work, thanks a lot :)

Last updated: Jun 13 2024 at 21:01 UTC