Stream: Coq users

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


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 13:39):

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

view this post on Zulip Théo Winterhalter (Dec 08 2020 at 13:40):

Just in case Pierre-Marie is right.

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 13:47):

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

view this post on Zulip Théo Winterhalter (Dec 08 2020 at 14:25):

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

view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Dec 08 2020 at 15:11):

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

view this post on Zulip Pierre Vial (Dec 08 2020 at 15:12):

OK, thanks to you all!


Last updated: Jan 31 2023 at 12:01 UTC