Use of variables in ltac1val quotation · Ltac2

I am currently trying to implement a Ltac2 function which is able to run a Ltac1 tactic.
Note that neither Ltac2 nor Ltac1 are supposed to know the number of arguments of this tactic in advance (this is why I would like to use the run function from the Ltac2.Ltac1 module.
However, the function should be parametrized by the name of the tactic : the user may
give an ident or a string.
But I couldn't find any satisfying solution. Here is my minimal example :

From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Ltac1.

Goal True.
(** 1st method **)
let id := ident:(easy) in
let tac := ref [ident:(Coq) ; ident:(Init); ident:(Tactics); id] in
Ltac1.apply tac [] run.
Restart.
(** 2nd method **)
Fail let id := ident:(easy) in
let tac := of_ident id in
Ltac1.apply tac [] run.
(* Variable F should be bound to a tactic. *)
(** 3rd method **)
Ltac1.apply ltac1val:(easy) [] run.
Restart.
(** 4th method **)
Fail let id := ident:(easy) in
let tac := of_ident id in
Ltac1.apply ltac1val:(tac) [] run.
(* The reference tac was not found in the current environment. *)
(** 5th method **)
Fail let id := ident:(easy) in
let tac := of_ident id in
Ltac1.apply (ltac1val:(tac |- tac) tac) [] run.
(* Expression does not evaluate to a tactic (got a ident). *)
Abort.

The first way of running easy solves the goal, but the function
ref needs the absolute path and throws an uncatchable exception
whenever there is no tactic corresponding to this path. This is a problem
for me, as the function that I want to implement is not supposed to know the absolute path in advance.
Furthermore, I don't even know how to use different paths in run and find the tactic among them,
instead of providing only one path.

The second method fails because of_ident returns a Ltac1 term
seen as a tactic but not seen as a value, whereas run needs a Ltac1 value.

The third method works but I should be able to know the tactic in advance and this is not the case.

The fourth method also fails because even if ltac1val:() transforms a Ltac1 tactic
into a value as I want, it cannot see the tac variable.

The fifth method also fails: even if I tried to use a context in ltac1val:()
in order to have access to the tac variable, I get a weird typing error
(why do I got an ident ? tac is not an ident ??).

Is there a solution that I am currently missing ? Thank you in advance for your help !

Gaëtan Gilbert (Dec 01 2023 at 09:31):

anything using of_ident won't work, of_ident produces the ltac1 which returns the ident, not the ltac1 from looking up the ident
We don't currently expose a way to lookup ltac1 definitions other than ref AFAIK

Louise Dubois de Prisque (Dec 01 2023 at 10:27):

Thank you very much for your answer ! It would be great to have a similar function which does not raise a fatal error, I would be curious to know why this implementation choice was made.
I have found a solution which mixes several meta-programming languages, as elpi's coq.ltac.call does not require the absolute path.

Pierre-Marie Pédrot (Dec 04 2023 at 09:51):

I think that my reasoning at the time was that non-absolute paths are very fragile. It's easy to get the tactic swept under your feet without realizing just by importing unrelated libraries. I guess it's fine to expose a function to look for a given tactic with a corresponding short name, but it should probably return a list rather than just a value.

Pierre-Marie Pédrot (Dec 04 2023 at 09:52):

(Unrelatedly, note also that instead of writing ident:(foo) you can just write @foo as a syntactic sugar.)

Janno (Dec 04 2023 at 10:03):

Would it make sense to also have ltac1reference:(..) for ltac1 tactics just like there's reference:(..) for terms (which is super useful, BTW)?

Louise Dubois de Prisque (Dec 04 2023 at 11:13):

@Pierre-Marie Pédrot yes you are right about absolute paths, it's just that in my use case I cannot know a priori where all the tactics that I need are.
The function that you mention would be useful, and if I remember correctly there is a counterpart for Std.references which can return a list of references given an ident, so why not for tactics as well ?

Stream: Ltac2

Topic: Use of variables in ltac1val quotation