Writing tactics in Elpi 

Defining tactics 

In Rocq a proof is just a term, and an incomplete proof is just a term with holes standing for the open goals.

When a proof starts there is just one hole (one goal) and its type is the statement one wants to prove. Then proof construction makes progress by instantiation: a term possibly containing holes is grafted to the hole corresponding to the current goal. What a tactic does behind the scenes is to synthesize this partial term.

Let's define a simple tactic that prints the current goal.

Set Warnings "-elpi.linear-variable".


From elpi Require Import elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]

Elpi Tactic show.
Elpi Accumulate lp:{{

  solve (goal Ctx _Trigger Type Proof _) _ :-
    coq.say "Goal:" Ctx "|-" Proof ":" Type.

}}.

The tactic declaration is made of 3 parts.

The first one Elpi Tactic show. sets the current program to show. Since it is declared as a Tactic some code is loaded automatically:

APIs (eg coq.say) and data types (eg Rocq term s) are loaded from coq-builtin.elpi
some utilities, like copy or whd1 are loaded from elpi-tactic-template.elpi

The second one Elpi Accumulate ... loads some extra code. The Elpi Accumulate ... family of commands lets one accumulate code taken from:

verbatim text Elpi Accumulate lp:{{ code }}
source files Elpi Accumulate File path
data bases (Db) Elpi Accumulate Db name

Accumulating code via inline text or file is equivalent, the AST of code is stored in the .vo file (the external file does not need to be installed). We invite the reader to look up the description of data bases in the tutorial about commands.

When some code is accumulated Elpi verifies that the code does not contain the most frequent kind of mistakes, via some type checking and linting. Some mistakes are minor and Elpi only warns about them. You can pass -w +elpi.typecheck to coqc to turn these warnings into errors.

The entry point for tactics is called solve which maps a goal into a list of sealed-goal (representing subgoals).

Tactics written in Elpi can be invoked by prefixing its name with elpi.

Lemma tutorial x y  : x + 1 = y.
1 goal
  
  x, y : nat
  ============================
  x + 1 = y

elpi show.
Goal: 
[decl c1 `y:r` (global (indt «nat»)), decl c0 `x:r` (global (indt «nat»))] 
|- X0 c0 c1 : 
app
 [global (indt «eq»), global (indt «nat»), 
  app
   [global (const «Nat.add»), c0, 
    app [global (indc «S»), global (indc «O»)]], c1]

Abort.

In the Elpi code up there Proof is the hole for the current goal, Type the statement to be proved and Ctx the proof context (the list of hypotheses). Since we don't assign Proof the tactic makes no progress, as the output above shows: the first line is the proof context, where proof variables are bound Elpi variables (here c0 and c1), and the context is a list of predicates holding on them (their type in Rocq). For example:

decl c0 `x` (global (indt «nat»))

asserts that c0 (pretty printed as x) has type nat.

Then we see that the value of Proof is X0 c0 c1. This means that the proof of the current goal is represented by Elpi's variable X0 and that the variable has c0 and c1 in scope (the proof term can use them).

Finally we see the type of the goal x + 1 = y.

The _Trigger component, which we did not print, is a variable that, when assigned, triggers the elaboration of its value against the type of the goal and obtains a value for Proof this way.

Keeping in mind that the solve predicate relates one goal to a list of subgoals, we implement our first tactic which blindly tries to solve the goal.

Elpi Tactic blind.
Elpi Accumulate lp:{{
  solve (goal _ Trigger _ _ _) [] :- Trigger = {{0}}.
  solve (goal _ Trigger _ _ _) [] :- Trigger = {{I}}.
}}.
Lemma test_blind : True * nat.
1 goal
  
  ============================
  True * nat

Proof.
split.
2 goals
  
  ============================
  True

goal 2 is:
 nat

- elpi blind.
1 goal
  
  ============================
  True

This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

1 goal

goal 1 is:
 nat

- elpi blind.
1 goal
  
  ============================
  nat

No more goals.

Show Proof.
(I, 0)

Qed.

Since the assignment of a term to Trigger triggers its elaboration against the expected type (the goal statement), assigning the wrong proof term results in a failure which in turn results in the other rule being tried.

For now, this is all about the low level mechanics of tactics which is developed further in More tactic examples and the proof engine.

We now focus on how to better integrate tactics written in Elpi with Ltac.

Integration with Ltac 

For a simple tactic like blind the list of subgoals is easy to write, since it is empty, but in general one should collect all the holes in the value of Proof (the checked proof term) and build goals out of them.

There is a family of APIs named after refine, the mother of all tactics, in elpi-ltac.elpi which does this job for you.

Usually a tactic builds a (possibly partial) term and calls refine on it.

Let's rewrite the blind tactic using this schema.

Elpi Tactic blind2.
Elpi Accumulate lp:{{
  solve G GL :- refine {{0}} G GL.
  solve G GL :- refine {{I}} G GL.
}}.
Lemma test_blind2 : True * nat.
1 goal
  
  ============================
  True * nat

Proof.
split.
2 goals
  
  ============================
  True

goal 2 is:
 nat

- elpi blind2.
1 goal
  
  ============================
  True

This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

1 goal

goal 1 is:
 nat

- elpi blind2.
1 goal
  
  ============================
  nat

No more goals.

Qed.

This schema works even if the term is partial, that is if it contains holes corresponding to missing sub proofs.

Let's write a tactic which opens a few subgoals, for example let's implement the split tactic.

Important

Elpi's equality (that is, unification) on Rocq terms corresponds to alpha equivalence, we can use that to make our tactic less blind.

The head of a rule for the solve predicate is matched against the goal. This operation cannot assign unification variables in the goal, only variables in the rule's head. As a consequence the following rule for solve is only used when the statement features an explicit conjunction.

About conj. (* remark the implicit arguments *)
conj : forall [A B : Prop], A -> B -> A /\ B

conj is not universe polymorphic
Arguments conj [A B]%_type_scope _ _
Expands to: Constructor Corelib.Init.Logic.conj
Declared in library Corelib.Init.Logic, line 62, characters 2-6

Elpi Tactic split.
Elpi Accumulate lp:{{
  solve (goal _ _ {{ _ /\ _ }} _ _ as G) GL :- !,
    % conj has 4 arguments, but two are implicits
    % (_ are added for them and are inferred from the goal)
    refine {{ conj _ _ }} G GL.

  solve _ _ :-
    % This signals a failure in the Ltac model. A failure
    % in Elpi, that is no more clauses to try, is a fatal
    % error that cannot be caught by Ltac combinators like repeat.
    coq.ltac.fail _ "not a conjunction".
}}.
Lemma test_split : exists t : Prop, True /\ True /\ t.
1 goal
  
  ============================
  exists t : Prop, True /\ True /\ t

Proof.
eexists.
1 focused goal (shelved: 1)
  
  ============================
  True /\ True /\ ?t

repeat elpi split. (* The failure is caught by Ltac's repeat *)
3 focused goals (shelved: 2)
  
  ============================
  True

goal 2 is:
 True
goal 3 is:
 ?t

(* Remark that the last goal is left untouched, since
   it did not match the pattern {{ _ /\ _ }}. *)
all: elpi blind.
No more goals.

Show Proof.
(ex_intro (fun t : Prop => True /\ True /\ t) True (conj I (conj I I)))

Qed.

The tactic split succeeds twice, stopping on the two identical goals True and the one which is an evar of type Prop.

We then invoke blind on all goals. In the third case the type checking constraint triggered by assigning {{0}} to Trigger fails because its type nat is not of sort Prop, so it backtracks and picks {{I}}.

Another common way to build an Elpi tactic is to synthesize a term and then call some Ltac piece of code finishing the work.

The API coq.ltac.call invokes some Ltac piece of code passing to it the desired arguments. Then it builds the list of subgoals.

Here we pass an integer, which in turn is passed to fail, and a term, which in turn is passed to apply.

Ltac helper_split2 n t := fail n || apply t.
helper_split2 is defined

Elpi Tactic split2.
Elpi Accumulate lp:{{
  solve (goal _ _ {{ _ /\ _ }} _ _ as G) GL :-
    coq.ltac.call "helper_split2" [int 0, trm {{ conj }}] G GL ok.
  solve _ _ :-
    coq.ltac.fail _ "not a conjunction".
}}.
Lemma test_split2 : exists t : Prop, True /\ True /\ t.
1 goal
  
  ============================
  exists t : Prop, True /\ True /\ t

Proof.
eexists.
1 focused goal (shelved: 1)
  
  ============================
  True /\ True /\ ?t

repeat elpi split2.
3 focused goals (shelved: 2)
  
  ============================
  True

goal 2 is:
 True
goal 3 is:
 ?t

all: elpi blind.
No more goals.

Qed.

Arguments and Tactic Notation 

Elpi tactics can receive arguments. Arguments are received as a list, which is the last argument of the goal constructor. This suggests that arguments are attached to the current goal being observed, but we will dive into this detail later on.

Elpi Tactic print_args.
Elpi Accumulate lp:{{
  solve (goal _ _ _ _ Args) _ :- coq.say Args.
}}.
Lemma test_print_args : True.
1 goal
  
  ============================
  True

elpi print_args 1 x "a b" (1 = 0).
[int 1, str x, str a b, 
 trm
  (app
    [global (indt «eq»), X0, 
     app [global (indc «S»), global (indc «O»)], global (indc «O»)])]

Abort.

The convention is that numbers like 1 are passed as int 1, identifiers or strings are passed as str "arg" and terms have to be put between parentheses.

Important

terms are received in raw format, eg before elaboration

Indeed the type argument to eq is a variable. One can use APIs like coq.elaborate-skeleton to infer holes like X0.

See the argument data type for a detailed description of all the arguments a tactic can receive.

Now let's write a tactic which behaves pretty much like the refine one from Rocq, but prints what it does using the API coq.term->string.

Elpi Tactic refine.
Elpi Accumulate lp:{{
  solve (goal _ _ Ty _ [trm S] as G) GL :-
    % check S elaborates to T of type Ty (the goal)
    coq.elaborate-skeleton S Ty T ok,

    coq.say "Using" {coq.term->string T}
            "of type" {coq.term->string Ty},

    % since T is already checked, we don't check it again
    refine.no_check T G GL.

  solve (goal _ _ _ _ [trm S]) _ :-
    Msg is {coq.term->string S} ^ " does not fit",
    coq.ltac.fail _ Msg.
}}.
Lemma test_refine (P Q : Prop) (H : P -> Q) : Q.
1 goal
  
  P, Q : Prop
  H : P -> Q
  ============================
  Q

Proof.
Fail elpi refine (H).
The command has indeed failed with message:
Tactic failure: H does not fit.

elpi refine (H _).
Using H ?p of type Q
1 goal
  
  P, Q : Prop
  H : P -> Q
  ============================
  P

Abort.

Ltac arguments to Elpi arguments 

It is customary to use the Tactic Notation command to attach a nicer syntax to Elpi tactics.

In particular elpi tacname accepts as arguments the following bridges for Ltac values :

ltac_string:(v) (for v of type string or ident)
ltac_int:(v) (for v of type int or integer)
ltac_term:(v) (for v of type constr or open_constr or uconstr or hyp)
ltac_(string|int|term)_list:(v) (for v of type list of ...)

Note that the Ltac type associates some semantics to the action of passing the arguments. For example hyp will accept an identifier only if it is an hypotheses of the context. While uconstr does not type check the term, which is the recommended way to pass terms to an Elpi tactic (since it is likely to be typed anyway by the Elpi tactic).

Tactic Notation "use" uconstr(t) :=
  elpi refine ltac_term:(t).
Tactic Notation "use" hyp(t) :=
  elpi refine ltac_term:(t).
Lemma test_use (P Q : Prop) (H : P -> Q) (p : P) : Q.
1 goal
  
  P, Q : Prop
  H : P -> Q
  p : P
  ============================
  Q

Proof.
use (H _).
Using H ?p of type Q
1 goal
  
  P, Q : Prop
  H : P -> Q
  p : P
  ============================
  P

Fail use q.
The command has indeed failed with message:
No such hypothesis: q

use p.
Using p of type P
No more goals.

Qed.
Tactic Notation "print" uconstr_list_sep(l, ",") :=
  elpi print_args ltac_term_list:(l).
Lemma test_print (P Q : Prop) (H : P -> Q) (p : P) : Q.
1 goal
  
  P, Q : Prop
  H : P -> Q
  p : P
  ============================
  Q

print P, p, (H p).
[trm c0, trm c3, trm (app [c2, c3])]

Abort.

Failure 

The coq.error aborts the execution of both Elpi and any enclosing Ltac context. This failure cannot be caught by Ltac.

On the contrary the coq.ltac.fail builtin can be used to abort the execution of Elpi code in such a way that Ltac can catch it. This API takes an integer akin to Ltac's fail depth together with the error message to be displayed to the user.

Library functions of the assert! family call, by default, coq.error. The flag @ltacfail! N can be set to alter this behavior and turn errors into calls to coq.ltac.fail N.

Elpi Tactic abort.
Elpi Accumulate lp:{{
  solve _ _ :- coq.error "uncatchable".
}}.
Goal True.
1 goal
  
  ============================
  True

Fail elpi abort || idtac.
The command has indeed failed with message:
uncatchable

Abort.
Elpi Tactic fail.
Elpi Accumulate lp:{{
  solve (goal _ _ _ _ [int N]) _ :- coq.ltac.fail N "catchable".
}}.
Goal True.
1 goal
  
  ============================
  True

elpi fail 0 || idtac.
Fail elpi fail 1 || idtac.
The command has indeed failed with message:
Tactic failure: catchable.

Abort.

Continue with More tactic examples and the proof engine.

Writing tactics in Elpi

Defining tactics

Integration with Ltac

Arguments and Tactic Notation

Ltac arguments to Elpi arguments

Failure