Following a discussion in https://github.com/ProofGeneral/PG/issues/494 started by @Christian Doczkal, I am wondering if there would exist a way to "expand" a tactic line involving the ssreflect last tactical, into separated tactics?
Basically, for the first tactical, the script by rewrite lem1 //= lem2; first tac3.
could be rewritten into something like
{ rewrite lem1.
all: rewrite //=.
all: rewrite lem2.
1: tac3.
all: done. }
(the idea would be to temporarily generate (e.g. syntactically from the prover frontend) that expanded script to inspect more easily the outcome of each rewrite step; that transformation wouldn't necessarily need to be complete, some heuristics handling most one-liners idioms would be very OK, with a no-op (no-expansion) as a fallback)
but what about by rewrite lem1 //= lem2; last tac3.
?
I tried doing something like:
{ rewrite lem1.
all: rewrite //=.
all: rewrite lem2.
all: idtac; [..|tac3]. }
or relying on the only selector, but these attempts were not successful.
would you be aware of a Ltac1 workaround to do this?
otherwise, would it make sense to add a last:
selector in Coq? or a way to perform in Ltac1 a dispatch […|…] on all focused goals?
I think I find some working solution by diving in the ltac doc:
{ rewrite lem1.
all: rewrite //=.
all: rewrite lem2.
all: [> | .. | tac3]. }
but maybe this is not the only solution :-) − and my initial question still holds: would we want to define some last: tac3.
selector instead?
BTW I have a question on the documentation of this variant:
Variant
[> ltac_expr .. ]
In this variant, the tactic ltac_expr is applied independently to each of the goals, rather than globally. In particular, if there are no goals, the tactic is not run at all. A tactic which expects multiple goals, such as swap, would act as if a single goal is focused.
I understand this is not the same semantics as [> ltac_expr | .. ]
(the latter assuming idtac
for the i-th goals, i≥2)
but is there a difference between, say, all: simpl.
and all: [> simpl .. ]
?
To answer you first question, yes use all: [> .. | tac3 ].
(not [> | .. | tac3 ]
unless you know there are at least two goals).
And why not defining last:
, or simply accepting negative numbers as goal selectors.
To answer your second question, since simpl
is not a multigoal tactic, there is no difference between the two forms. You can have a different behavior with tactics swap
, cycle
, typeclasses eauto
and gfail
(which is a tactic that fails even if there are no goals left:
Goal True.
easy.
Fail all: gfail.
all: [> gfail .. ].
OK, thank you Théo for your answers!
Last updated: Oct 13 2024 at 01:02 UTC