Stream: Coq users

Topic: Passing an ltac thunk to a tactic notation?


view this post on Zulip Ralf Jung (Oct 03 2023 at 08:00):

Sometimes it is necessary to convert an Ltac to a Tactic Notation, e.g. when one needs an argument to be parsed a certain way and ltac doesn't provide another way of forcing the right parsing (see https://github.com/coq/coq/issues/18111).
But which parsing "category" do I need to set for general ltac terms / ltac thunks? Let's say I have a tactic like this

Ltac run_tac tac := tac ().

How do I make that a notation? I tried this but it doesn't work:

Ltac run_tac tac := tac ().

Tactic Notation "run_tac2" tactic(tac) := tac.

Goal forall n : nat, True.
Proof.
  intros n.
  run_tac ltac:(fun _ => destruct n as [|n']).
Undo.
  run_tac2 ltac:(fun _ => destruct n as [|n']).
(* Error: An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _,
no arguments at all were provided. *)

view this post on Zulip Ralf Jung (Oct 03 2023 at 08:00):

I've looked through the table at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation but none of the categories seem to fit

view this post on Zulip Ralf Jung (Oct 03 2023 at 08:01):

but also the table is incomplete, e.g. open_constr is missing, so maybe there are other things missing as well

view this post on Zulip Janno (Oct 03 2023 at 08:41):

I am not sure I understand the question. You are passing an ltac fun to both run_tac and run_tac2 but only run_tac actually supplies the unit argument. If you change run_tac2 to tac () it seems to work.

view this post on Zulip Janno (Oct 03 2023 at 08:41):

You can also use ltac:(idtac; ..) to thunk tactics and that way you can skip fun _ => and the unit argument

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 08:46):

do you actually need thunk/idtac for tactics passed to Tactic Notation? The stdpp tactics don't seem to

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 08:49):

Tactic Notation "run_tac2" tactic(tac) := tac.

bewaretactic is probably almost always the wrong precedence, run_tac2 a; b; c would parse as run_tac2 (a; b; c).

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 08:49):

You have tactic0 to tactic4, matching ltac_expr0 to ltac_expr4 in the ltac grammar: https://coq.inria.fr/refman/proof-engine/ltac.html#syntax. I've recommended tactic3 in the past for stdpp, but I suspect tactic1 would make more sense.

view this post on Zulip Ralf Jung (Oct 03 2023 at 11:51):

Janno said:

I am not sure I understand the question. You are passing an ltac fun to both run_tac and run_tac2 but only run_tac actually supplies the unit argument. If you change run_tac2 to tac () it seems to work.

oh I am stupid, you are right.
I had some very strange trouble porting an existing Ltac to a Tactic Notation that lead to the same error and then made this fatal mistake while minimizing...

view this post on Zulip Ralf Jung (Oct 03 2023 at 11:51):

I wonder now if my original issue was a similar typo or something deeper. sadly the error doesn't say where arguments failed to be provided.

view this post on Zulip Ralf Jung (Oct 03 2023 at 11:52):

Paolo Giarrusso said:

You have tactic0 to tactic4, matching ltac_expr0 to ltac_expr4 in the ltac grammar: https://coq.inria.fr/refman/proof-engine/ltac.html#syntax. I've recommended tactic3 in the past for stdpp, but I suspect tactic1 would make more sense.

yeah I know, this is just for demonstration. I never know which number to pick, I just know the default is bad...

view this post on Zulip Ralf Jung (Oct 03 2023 at 11:52):

Paolo Giarrusso said:

do you actually need thunk/idtac for tactics passed to Tactic Notation? The stdpp tactics don't seem to

probably not but we always use thunks since it is the only way to be sure

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 16:25):

There's at least no visible thunking with naive_solver eauto with foo.

view this post on Zulip Jason Gross (Oct 03 2023 at 22:55):

All tactic arguments are delayed by default unless they are headed by match, lazymatch, multimatch, or let

view this post on Zulip Ralf Jung (Oct 04 2023 at 06:57):

Paolo Giarrusso said:

There's at least no visible thunking with naive_solver eauto with foo.

ah sure yes we avoid the thunks to get a nicer UI. I meant in the implementation. we have to use CPS for tons of stuff anyway so the few additional closures for thunking barely stick out^^


Last updated: Oct 13 2024 at 01:02 UTC