Stream: Coq users

Topic: Ltac1/ssr: toplevel_selector to emulate the "last" tactical?


view this post on Zulip Erik Martin-Dorel (Jun 03 2020 at 21:24):

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?

view this post on Zulip Erik Martin-Dorel (Jun 03 2020 at 22:14):

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?

view this post on Zulip Erik Martin-Dorel (Jun 03 2020 at 22:19):

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

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 08:30):

To answer you first question, yes use all: [> .. | tac3 ]. (not [> | .. | tac3 ] unless you know there are at least two goals).

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 08:34):

And why not defining last:, or simply accepting negative numbers as goal selectors.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 08:38):

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

view this post on Zulip Erik Martin-Dorel (Jun 04 2020 at 11:31):

OK, thank you Théo for your answers!


Last updated: Feb 06 2023 at 13:03 UTC