Pierre Vial (Sep 08 2022 at 18:28): 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 ) ?
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?
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.
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 ;)
Pierre Vial (Sep 09 2022 at 08:30):Thanks @Enzo Crance !
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) *)
Pierre Vial has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC