Pierre Vial (Dec 08 2020 at 11:27): 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
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
| ..
].
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: Sep 30 2023 at 05:01 UTC