## Stream: Coq users

### Topic: ltac intros: recover the ident of the last hypothesis

#### Pierre Vial (Dec 08 2020 at 11:27):

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

#### Théo Winterhalter (Dec 08 2020 at 11:37):

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.

#### Théo Winterhalter (Dec 08 2020 at 11:37):

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.

#### Pierre Vial (Dec 08 2020 at 13:30):

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

#### Pierre-Marie Pédrot (Dec 08 2020 at 13:32):

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

#### Théo Winterhalter (Dec 08 2020 at 13:32):

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

#### Pierre Vial (Dec 08 2020 at 13:37):

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

#### Pierre-Marie Pédrot (Dec 08 2020 at 13:39):

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

#### Théo Winterhalter (Dec 08 2020 at 13:40):

Just in case Pierre-Marie is right.

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

#### Théo Winterhalter (Dec 08 2020 at 13:41):

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.

#### Pierre Vial (Dec 08 2020 at 13:45):

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?

#### Pierre-Marie Pédrot (Dec 08 2020 at 13:47):

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

#### Théo Winterhalter (Dec 08 2020 at 14:25):

Yeah the `..` part means that it works on any number of goals.

#### Pierre Vial (Dec 08 2020 at 15:09):

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?

#### Théo Winterhalter (Dec 08 2020 at 15:11):

Yeah. `..` is equivalent to `idtac ..` and `t ..` just applies tactic `t` to all other goals.

#### Pierre Vial (Dec 08 2020 at 15:12):

OK, thanks to you all!

Last updated: Jan 31 2023 at 12:01 UTC