Stream: Elpi users & devs

Topic: Elpi tactic returning a term


view this post on Zulip Pierre Vial (Sep 08 2022 at 18:28):

Hello,
Out of curiosity, how should I do to write an Elpi tactic which returns a term? As a toy example, a tactic which takes a Coq term t and outputs the pair ( t , t ) ?

view this post on Zulip Enrico Tassi (Sep 08 2022 at 19:05):

All tactics return a term, in the sense that they are called on a goal (a type) and they inhabit it. Your question seems like: "how do I write a tactics which proves A -> A /\ A". What am I missing?

view this post on Zulip Pierre Vial (Sep 09 2022 at 06:44):

Well, I'm looking for a tactic which returns a term that I can use. So that if foo is my elpi tactic which takes a term t and outputs ( t , t ) and x is a term in the context, I can write something like :

let na := fresh in let xx:= foo x in pose x as na.

view this post on Zulip Enzo Crance (Sep 09 2022 at 08:00):

Hi. An Elpi tactic cannot directly return a term, it more or less takes the proof state and has the ability to modify it with various API calls, but one of them is refine. Among other features, it lets you pose a term in the context.

IIUC, the line you posted is roughly equivalent to

refine (let na := foo x in _).

If you write an Elpi predicate taking any term x and generating the content of what you currently call foo x, in 2 lines you can have a tactic that takes x as an argument, computes the output term, and calls refine to add it to the context.

solve (goal _ _ GoalTy _ [trm X] as Goal) NewGoals :-
  compute-foo X FooX,
  refine (let _ _ FooX (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.

NB: I just made up this code on Zulip but I know this technique works, I have used it in Trakt ;)

view this post on Zulip Pierre Vial (Sep 09 2022 at 08:30):

Thanks @Enzo Crance !

view this post on Zulip Enrico Tassi (Sep 09 2022 at 09:17):

Thanks @Enzo Crance you were faster than me! Since I was too writing a solution, here it is:

Elpi Tactic double.
Elpi Accumulate lp:{{

solve (goal _ _ _ _ [trm X] as G) GL :-
  refine {{ ( lp:X , lp:X ) }} G GL.

}}.
Elpi Typecheck.
Tactic Notation "foo" uconstr(x) := elpi double ltac_term:(x).

Goal forall x : nat, True.
Proof.
intro x.
let xx := foo x in
pose (ltac:(xx)) as na.
(* in the context you now have  na : nat * nat := (x, x) *)

Last updated: Feb 04 2023 at 02:03 UTC