Pure tactic · Elpi users & devs · Zulip Chat Archive

Hello. I hope I haven't already asked this question before. Is there a way to create a pure tactic in elpi ?

Proof.
  let y := stateless_tactic x in
  stateful_tactic y.

AFAIK an elpi tactic is implemented through a solve predicate acting on the proof state. This is how I would naturally implement stateful_tactic. In this case, the only way to "return" something is to "do" something. I don't know if there is another way, something like: (pseudo declaration of what elpi could expect)

pred pure-solve
  i:goal-ctx, % goal context
  i:term, % goal type
  i:(list argument), % tactic arguments
  o:A. % type of output known when the user implements the predicate

I remember that even in Ltac, mixing pure and impure tactics is not a good idea, and I would understand if it were the same in Elpi. But out of curiosity I prefer asking :)

Enrico Tassi (Aug 18 2021 at 19:55):

Hum, it is not so clear to me what you really want to do. FYI, I did update, recently, the tutorials and I wrote one for tactics.
IMO, you want to reason about the data type sealed-goal. The "proof state" is not special, it is just the the hole which is filled in by the tactic is referenced by Coq, you should be able to craft a new goal out of thin air if you want. If you give me a bit more context I can try to write a POC for you.

In general, if you take a goal Ctx Trigger Type Proof Arg and you run a piece of code on goal Ctx Trigger1 Type Proof1 Arg you get a "pure" piece of code, if I get you right.

Enrico Tassi (Aug 19 2021 at 07:22):

You can do the same to invoke any tactic-like piece of code yourself. elpi tac runs it on an evar which is part of the proof tree, a descendant of the initial goal. But you can run it on an evar which is out of the proof tree if you like.

Enrico Tassi (Aug 19 2021 at 07:23):

About generating an A instead of a term assignment for an evar, well, you would need to change a little the signature. But if you change it very much, then maybe it should not be a tactic at all. After all a tactic is just an elpi program, the convention that it makes progress by assigning a particular variable is arbitrary.

Enrico Tassi (Aug 19 2021 at 07:34):

Finally, nothing prevents you from writing a predicate of type A -> goal -> sealed-goal list -> prop and have it make no progress on goal, but assign A (as an output).

Enzo Crance (Aug 19 2021 at 09:19):

I understand. Thanks for your explanations. I am not sure about the architecture I need. I think I might be reasoning too much at an Ltac level, wanting to split tactics into several parts, but one big elpi tactic with pure parts can do the job.

Enrico Tassi (Aug 20 2021 at 08:50):

Yes, this is the same feeling I have. The truth is that "tactics" don't compose well as regular pieces of code do, and this holds for both OCaml tactics and elpi ones. So typically (at least in OCaml where I wrote tons of tactic code) you write a bunch of regular code, and then you end by calling this tactic with a little pre/post processing expressed in terms of tactics (like intro/clear).

Stream: Elpi users & devs