Hello,

I writing a tactic which starts with asserting and proving the injectivity of a data type constructor.

Thus, the first step of the tactic is to give something like

```
H : forall (x1 y1: nat), forall (x2 y2 :list nat), x1 :: x2 = y1 :: y2 -> x1 = y1 /\ x2 = y2
```

as a subgoal.

To prove this, I will do `intros`

. The last named hypothesis produced will be a witness of `x1 :: x2 = y1 :: y2`

. It will probably be named `H0`

. Then, I would like to just du `inversion H0`

. But how can I automate this? I would need to have a way of recovering the ident of the last introduced variable (perhaps `H0`

, perhaps something else).

If you know how many intros you will do you can just give them names. But I guess you don't know.

You can also do the `intros`

and then try to recover the argument if you know its shape.

It's probably always going to be an equality right?

So

```
intros ;
match goal with
| h : _ = _ |- _ => inversion h
end.
```

should do it.

`match goal`

allows you to match on the hypotheses (left of the `|-`

) and the goal itself (right of the `|-`

).

It looks at hypotheses that match starting from the most recently introduced.

Note that `match goal`

will backtrack and try to find another matching hypothesis if the tactic inside fails.

To avoid this I would recommend using `lazymatch goal`

instead.

This seems like a great idea. Indeed, when I write `match goal ...`

in the proof after having invoked my tactic, it will perform the inversion. However, if I write `; match goal with ...`

in the tactic, it fails while I invoke it with the following message:

```
Error: No matching clauses for match.
```

whereas when the `match goal`

, the last introduced hypothesis is indeed an equality...

Did you generate several goals? If so, you need to only apply the match goal to the first one.

As I said, it might backtrack if some later tactic fails. It backtracks until it doesn't find any hypothesis that matches, and then says "no matching clause". That's why I would suggest you use `lazymatch`

.

Just after I call the tactic (without the `match`

or the `lazymatch`

), I'm in this environment. The subgoal `2+ 2 =4`

is just the the dummy goal I use to be in proof mode (it's not generated by the tactic).

```
2 subgoals (ID 368)
H := forall (x y : nat) (x0 y0 : list nat), x :: x0 = y :: y0 -> y = x /\ y0 = x0 /\ True : Prop
x, y : nat
x0, y0 : list nat
H0 : x :: x0 = y :: y0
============================
y = x /\ y0 = x0 /\ True
subgoal 2 (ID 363) is:
2 + 2 = 4
```

If I were you I'd first debug replacing inversion by some idtac

Just in case Pierre-Marie is right.

```
intros ; [
lazymatch goal with
| h : _ = _ |- _ => inversion h
end
| ..
].
```

By the way, if you are sure you want to get the last hypothesis, just

```
intros ;
lazymatch goal with
| h : _ |- _ => inversion h
end.
```

should be enough.

When I replace the whole `match goal `

with `idatc "hello world`

, everything goes fine.

When I write `...| h : _ = _ |- _ => idtac "hello world"`

, I have the same problem.

If I do as you suggest @Théo Winterhalter , this works, but I guess its only because I have 2 (and not 3, 4, 5...) subgoals. How do I specify that `match`

should only be applied to the first subgoal?

Nope, @Théo Winterhalter 's syntax works for any number of goals.

Yeah the `..`

part means that it works on any number of goals.

OK, I think I had replaced the two dots .. by something else. So basically, this means that I won't do anything to the other goals?

Yeah. `..`

is equivalent to `idtac ..`

and `t ..`

just applies tactic `t`

to all other goals.

OK, thanks to you all!

Last updated: Sep 30 2023 at 05:01 UTC