Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.

Tutorial on Coq tactics

Author: Enrico Tassi

This tutorial focuses on the implementation of Coq tactics.

This tutorial assumes the reader is familiar with Elpi and the HOAS representation of Coq terms; if it is not the case, please take a look at these other tutorials first: Elpi tutorial and Coq HOAS tutorial.

Defining tactics

In Coq 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.

[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Elpi Tactic show. Elpi Accumulate lp:{{ solve (goal Ctx _Trigger Type Proof _) _ :- coq.say "Goal:" Ctx "|-" Proof ":" Type. }}. Elpi Typecheck.

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:

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.

Once all the code is accumulated Elpi Typecheck verifies that the code does not contain the most frequent kind of mistakes. This command considers some mistakes minor and 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.

x, y: nat

x + 1 = y
Goal: [decl c1 `y` (global (indt «nat»)), decl c0 `x` (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. Elpi prints somethinglike this:

Goal: 
[decl c1 `y` (global (indt «nat»)), decl c0 `x` (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]

The first line is the proof context: proof variables are bound Elpi variables (here c0 and c1), the context is a list of predicates holding on them (their type in Coq). 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}}.
}}.
Elpi Typecheck.


(True * nat)%type
Proof.

True

nat

True
elpi blind.

nat
elpi blind.
(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 the section 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.
}}.
Elpi Typecheck.


(True * nat)%type
Proof.

True

nat

True
elpi blind2.

nat
elpi blind2. 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 Coq 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.

conj : forall [A B : Prop], A -> B -> A /\ B conj is not universe polymorphic Arguments conj [A B]%type_scope _ _ Expands to: Constructor Coq.Init.Logic.conj
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". }}. Elpi Typecheck.

exists t : Prop, True /\ True /\ t
Proof.

True /\ True /\ ?t

True

True

?t
(* Remark that the last goal is left untouched, since it did not match the pattern {{ _ /\ _ }}. *) all: elpi blind.
(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.

Elpi Tactic split2.
Elpi Accumulate lp:{{
  solve (goal _ _ {{ _ /\ _ }} _ _ as G) GL :-
    coq.ltac.call "helper_split2" [int 0, trm {{ conj }}] G GL.
  solve _ _ :-
    coq.ltac.fail _ "not a conjunction".
}}.
Elpi Typecheck.


exists t : Prop, True /\ True /\ t
Proof.

True /\ True /\ ?t

True

True

?t
all: elpi blind. 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.
}}.
Elpi Typecheck.

Lemma test_print_args : True.
[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 Coq, 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.
}}.
Elpi Typecheck.

P, Q: Prop
H: P -> Q

Q
Proof.
Tactic failure: H does not fit.
P, Q: Prop
H: P -> Q

Q
Using H ?p of type Q
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).

P, Q: Prop
H: P -> Q
p: P

Q
Proof.
Using H ?p of type Q
P, Q: Prop
H: P -> Q
p: P

P
No such hypothesis: q
Using p of type P
Qed. Tactic Notation "print" uconstr_list_sep(l, ",") := elpi print_args ltac_term_list:(l).
P, Q: Prop
H: P -> Q
p: P

Q
[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".
}}.


True
The command has indeed failed with message: uncatchable

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

True

True
The command has indeed failed with message: Tactic failure: catchable.

True
Abort.

Examples

Let's code assumption in Elpi

assumption is a very simple tactic: we look up in the proof context for an hypothesis which unifies with the goal. Recall that Ctx is made of decl and def (here, for simplicity, we ignore the latter case).

Elpi Tactic assumption.
Elpi Accumulate lp:{{
  solve (goal Ctx _ Ty _ _ as G) GL :-
    % H is the name for hyp, Ty is the goal
    std.mem Ctx (decl H _ Ty),
    refine H G GL.
  solve _ _ :-
    coq.ltac.fail _ "no such hypothesis".
}}.
Elpi Typecheck.

P, Q: Prop
p: P
q: Q

P /\ id Q
Proof.
P, Q: Prop
p: P
q: Q

P
P, Q: Prop
p: P
q: Q
id Q
P, Q: Prop
p: P
q: Q

id Q
Tactic failure: no such hypothesis.
P, Q: Prop
p: P
q: Q

id Q
Abort.

As we hinted before, Elpi's equality is alpha equivalence. In the second goal the assumption has type Q but the goal has type id Q which is convertible (unifiable, for Coq's unification) to Q.

Let's improve our tactic by looking for an assumption which is unifiable with the goal, and not just alpha convertible. The coq.unify-leq calls Coq's unification for types (on which cumulativity applies, hence the -leq suffix). The std.mem utility, thanks to backtracking, eventually finds an hypothesis that satisfies the following predicate (ie unifies with the goal).

Elpi Tactic assumption2.
Elpi Accumulate lp:{{
  solve (goal Ctx _ Ty _ _ as G) GL :-
    % std.mem is backtracking (std.mem! would stop at the first hit)
    std.mem Ctx (decl H _ Ty'), coq.unify-leq Ty' Ty ok,
    refine H G GL.
  solve _ _ :-
    coq.ltac.fail _ "no such hypothesis".
}}.
Elpi Typecheck.

P, Q: Prop
p: P
q: Q

P /\ id Q
Proof.
P, Q: Prop
p: P
q: Q

P
P, Q: Prop
p: P
q: Q
id Q
all: elpi assumption2. Qed.

refine does unify the type of goal with the type of the term, hence we can simplify the code further. We obtain a tactic very similar to our initial blind tactic, which picks candidates from the context rather than from the program itself.

Elpi Tactic assumption3.
Elpi Accumulate lp:{{
  solve (goal Ctx _ _ _ _ as G) GL :-
    std.mem Ctx (decl H _ _),
    refine H G GL.
  solve _ _ :-
    coq.ltac.fail _ "no such hypothesis".
}}.
Elpi Typecheck.

P, Q: Prop
p: P
q: Q

P /\ id Q
Proof.
P, Q: Prop
p: P
q: Q

P
P, Q: Prop
p: P
q: Q
id Q
all: elpi assumption3. Qed.

Let's code set in Elpi

The set tactic takes a term, possibly with holes, and makes a let-in out of it.

It gives us the occasion to explain the copy utility.

Elpi Tactic find.
Elpi Accumulate lp:{{

solve (goal _ _ T _ [trm X]) _ :-
  pi x\
    copy X x => copy T (Tabs x),
    if (occurs x (Tabs x))
       (coq.say "found" {coq.term->string X})
       (coq.ltac.fail _ "not found").
}}.
Elpi Typecheck.

P, Q: Prop

P /\ P \/ P /\ Q
Proof.
found P
P, Q: Prop

P /\ P \/ P /\ Q
Tactic failure: not found.
found P /\ P
P, Q: Prop

P /\ P \/ P /\ Q
Abort.

This first approximation only prints the term it found, or better the first instance of the given term.

Now lets focus on copy. An excerpt:

copy X X :- name X.     % checks X is a bound variable
copy (global _ as C) C.
copy (fun N T F) (fun N T1 F1).
  copy T T1, pi x\ copy (F x) (F1 x).
copy (app L) (app L1) :- !, std.map L copy L1.

Copy implements the identity: it builds, recursively, a copy of the first term into the second argument. Unless one loads in the context a new rule, which takes precedence over the identity ones. Here we load:

copy X x

which, at run time, looks like

copy (app [global (indt «andn»), sort prop, sort prop, c0, X0 c0 c1]) c2

and that rule masks the one for app when the sub-term being copied matches (P /\ _). The first time this rule is used X0 is assigned, making the rule represent the term (P /\ P).

Now let's refine the tactic to build a let-in, and complain if the desired name is already taken.

Elpi Tactic set.
Elpi Accumulate lp:{{

solve (goal _ _ T _ [str ID, trm X] as G) GL :-
  pi x\
    copy X x => copy T (Tabs x),
    if (occurs x (Tabs x))
       (if (coq.ltac.id-free? ID G) true
           (coq.warn ID "is already taken, Elpi will make a name up"),
        coq.id->name ID Name,
        Hole x = {{ _ : lp:{{ Tabs x }} }}, % a hole with a type
        refine (let Name _ X x\ Hole x) G GL)
       (coq.ltac.fail _ "not found").

}}.
Elpi Typecheck.

P, Q: Prop

P /\ P \/ P /\ Q
Proof.
P, Q: Prop
x:= P: Prop

x /\ x \/ x /\ Q
P, Q: Prop
x:= P: Prop

P /\ P \/ P /\ Q
Tactic failure: not found.
x is already taken, Elpi will make a name up [lib,elpi,default]
P, Q: Prop
x:= P: Prop
elpi_ctx_entry_4_:= P /\ P: Prop

elpi_ctx_entry_4_ \/ P /\ Q
Abort.

For more examples of (basic) tactics written in Elpi see the eltac app.

The proof engine

In this section we dive into the details of the proof engine, that is how goals are represented in Elpi and how things are wired up behind the scenes.

Let's inspect the proof state a bit deeper:

Elpi Tactic show_more.
Elpi Accumulate lp:{{

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

}}.
Elpi Typecheck.

x: nat

x + 1 = 0
Goal: [decl c0 `x` (global (indt «nat»))] |- X0 c0 : app [global (indt «eq»), global (indt «nat»), app [global (const «Nat.add»), c0, app [global (indc «S»), global (indc «O»)]], global (indc «O»)]
Proof state:
{c0} : decl c0 `x` (global (indt «nat»)) ?- evar (X1 c0) (app [global (indt «eq»), global (indt «nat»), app [global (const «Nat.add»), c0, app [global (indc «S»), global (indc «O»)]], global (indc «O»)]) (X0 c0) /* suspended on X1, X0 */
EVARS: ?X57==[x |- x + 1 = 0] (goal evar) {?Goal} ?X56==[ |- => fun x : nat => ?Goal] (goal evar) ?X55==[x |- => nat] (parameter A of eq) ?X54==[ |- => nat] (type of x) SHELF:|| FUTURE GOALS STACK: ||
Coq-Elpi mapping: RAW: ?X57 <-> c0 \ X1 c0 ELAB: ?X57 <-> X0
Abort.

In addition to the goal we print the Elpi and Coq proof state, plus the link between them. The proof state is the collection of goals together with their types.

On the Elpi side this state is represented by constraints for the evar predicate.

{c0} : decl c0 `x` (global (indt «nat»))
  ?- evar (X1 c0) 
      (app
        [global (indt «eq»), global (indt «nat»), 
         app
          [global (const «Nat.add»), c0, 
           app [global (indc «S»), global (indc «O»)]], 
         global (indc «O»)]) (X0 c0)  /* suspended on X1, X0 */

One can recognize the set of bound variables {c0}, the hypothetical context of rules about these variable (that also corresponds to the proof context), and finally the suspended goal evar (X1 c0) .. (X0 c0).

The set of constraints on evar represents the Coq data structure called sigma (sometimes also called evd or evar_map) that is used to represent the proof state in Coq. It is printed just afterwards:

EVARS:
 ?X57==[x |- x + 1 = 0] (goal evar) {?Goal}
 ?X56==[ |- => fun x : nat => ?Goal] (goal evar)
 ?X55==[x |- => nat] (parameter A of eq)
 ?X54==[ |- => nat] (type of x)

SHELF:||
FUTURE GOALS STACK:
 ||
Coq-Elpi mapping:
RAW:
?X57 <-> c0 \ X1 c0
ELAB:
?X57 <-> X0

Here ?X57 is a Coq evar linked with Elpi's X0 and X1. X1 represents the goal (the trigger) while X0 represent the proof. The meaning of the evar Elpi predicate linking the two is that the term assigned to the trigger X1 has to be elaborated to the final proof term X0, that should be a well typed term of type x + 1 = 0. This means that when an Elpi tactic assigns a value to X1 some procedure to turn that value into X0 is triggered. That procedure is called elaboration and it is currently implemented by calling the coq.elaborate-skeleton API.

Given this set up, it is impossible to use a term of the wrong type as a Proof. Let's rewrite the split tactic without using refine.

Elpi Tactic split_ll.
Elpi Accumulate lp:{{
  solve (goal Ctx Trigger {{ lp:A /\ lp:B }} Proof []) GL :- !,
    Trigger = {{ conj _ _ }}, % triggers elaboration, filling Proof
    Proof = {{ conj lp:Pa lp:Pb }},
    GL = [seal G1, seal G2],
    G1 = goal Ctx _ A Pa [],
    G2 = goal Ctx _ B Pb [].
  solve _ _ :-
    coq.ltac.fail _ "not a conjunction".
}}.
Elpi Typecheck.


exists t : Prop, True /\ True /\ t
Proof.

True /\ True /\ ?t

True

True

?t
all: elpi blind. Qed.

Crafting by hand the list of subgoal is not easy. In particular here we did not set up the new trigger for Pa and Pb, nor seal the goals appropriately (we did not bind proof variables).

The coq.ltac.collect-goals API helps us doing this.

Elpi Tactic split_ll_bis.
Elpi Accumulate lp:{{
  solve (goal Ctx Trigger {{ lp:A /\ lp:B }} Proof []) GL :- !,
    % this triggers the elaboration
    Trigger = {{ conj _ _ }},                   
    % we only take main goals
    coq.ltac.collect-goals Proof GL _ShelvedGL.
  solve _ _ :-
    coq.ltac.fail _ "not a conjunction".
}}.
B is linear: name it _B (discard) or B_ (fresh variable) [elpi.typecheck,elpi,default]
A is linear: name it _A (discard) or A_ (fresh variable) [elpi.typecheck,elpi,default]
Ctx is linear: name it _Ctx (discard) or Ctx_ (fresh variable) [elpi.typecheck,elpi,default]

exists t : Prop, True /\ True /\ t
Proof.

True /\ True /\ ?t

True

True

?t
all: elpi blind. Qed.

At the light of that, refine is simply:

refine T (goal _ RawEv _ Ev _) GS :-
  RawEv = T, coq.ltac.collect-goals Ev GS _.

Now that we know the low level plumbing, we can use refine ;-)

The only detail we still have to explain is what exactly a sealed-goal is. A sealed goal wraps into a single object all the proof variables and the assumptions about them, making this object easy (or better, sound) to pass around.

multi-goal tactics

Since Coq 8.4 tactics can see more than one goal (multi-goal tactics). You can access this feature by using all: goal selector:

  • if the tactic is a regular one, it will be used on each goal independently
  • if the tactic is a multi-goal one, it will receive all goals

In Elpi you can implement a multi-goal tactic by providing a rule for the msolve predicate. Since such a tactic will need to manipulate multiple goals, potentially living in different proof context, it receives a list of sealed-goal, a data type which seals a goal and its proof context.

Elpi Tactic ngoals.
Elpi Accumulate lp:{{

  msolve GL _ :-
    coq.say "#goals =" {std.length GL},
    coq.say GL.

}}.
Elpi Typecheck.

P, Q: Prop

P /\ Q
Proof.
P, Q: Prop

P
P, Q: Prop
Q
#goals = 2
[nabla c0 \ nabla c1 \ seal (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X0 c0 c1) c0 (X1 c0 c1) []), nabla c0 \ nabla c1 \ seal (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X2 c0 c1) c1 (X3 c0 c1) [])]
P, Q: Prop

P
P, Q: Prop
Q
Abort.

This simple tactic prints the number of goals it receives, as well as the list itself. We see something like:

#goals = 2
[nabla c0 \
  nabla c1 \
   seal
    (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X0 c0 c1) c0 
      (X1 c0 c1) []), 
 nabla c0 \
  nabla c1 \
   seal
    (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X2 c0 c1) c1 
      (X3 c0 c1) [])]

nabla binds all proof variables, then seal holds a regular goal, which in turn carries the proof context.

In order to operate inside a goal one can use the coq.ltac.open utility, which postulates all proof variables using pi x\ and loads the proof context using =>.

Operating on multiple goals at the same time is doable, but not easy. In particular the two proof context have to be related in some way.

The following simple multi goal tactic shrinks the list of goals by removing duplicates. As one can see, there is much room for improvement in the same-ctx predicate.

Elpi Tactic undup.
Elpi Accumulate lp:{{

  pred same-goal i:sealed-goal, i:sealed-goal.
  same-goal (nabla G1) (nabla G2) :-
    % TODO: proof variables could be permuted
    pi x\ same-goal (G1 x) (G2 x).
  same-goal (seal (goal Ctx1 _ Ty1 P1 _) as G1)
            (seal (goal Ctx2 _ Ty2 P2 _) as G2) :-
    same-ctx Ctx1 Ctx2,
    % this is an elpi builtin, aka same_term, which does not
    % unify but rather compare two terms without assigning variables
    Ty1 == Ty2,
    P1 = P2.

  pred same-ctx i:goal-ctx, i:goal-ctx.
  same-ctx [] [].
  same-ctx [decl V _ T1|C1] [decl V _ T2|C2] :-
    % TODO: we could compare up to permutation...
    % TODO: we could try to relate def and decl
    T1 == T2,
    same-ctx C1 C2.

  pred undup i:sealed-goal, i:list sealed-goal, o:list sealed-goal.
  undup _ [] [].
  undup G [G1|GN] GN :- same-goal G G1.
  undup G [G1|GN] [G1|GL] :- undup G GN GL.

  msolve [G1|GS] [G1|GL] :-
    % TODO: we could find all duplicates, not just
    % copies of the first goal...
    undup G1 GS GL.

}}.
G2 is linear: name it _G2 (discard) or G2_ (fresh variable) [elpi.typecheck,elpi,default]
G1 is linear: name it _G1 (discard) or G1_ (fresh variable) [elpi.typecheck,elpi,default]
P, Q: Prop
p: P
q: Q

P /\ Q /\ P
Proof.
P, Q: Prop
p: P
q: Q

P
P, Q: Prop
p: P
q: Q
Q
P, Q: Prop
p: P
q: Q
P
(fun (P Q : Prop) (p : P) (q : Q) => conj ?Goal (conj ?Goal0 ?Goal1))
P, Q: Prop
p: P
q: Q

P
P, Q: Prop
p: P
q: Q
Q
(fun (P Q : Prop) (p : P) (q : Q) => conj ?Goal (conj ?Goal0 ?Goal))
P, Q: Prop
p: P
q: Q

P
apply p.
P, Q: Prop
p: P
q: Q

Q
apply q. Qed.

The two calls to show proof display, respectively:

(fun (P Q : Prop) (p : P) (q : Q) =>
 conj ?Goal (conj ?Goal0 ?Goal1))
(fun (P Q : Prop) (p : P) (q : Q) =>
 conj ?Goal (conj ?Goal0 ?Goal))

the proof term is the same but for the fact that after the tactic the first and last missing subterm (incomplete proof tree branch) are represented by the same hole ?Goal0. Indeed by solving one, we can also solve the other.

LCF tacticals

On the notion of sealed-goal it is easy to define the usual LCF combinators, also known as Ltac tacticals. Tacticals usually take in input one or more tactic, here the precise type definition:

typeabbrev tactic (sealed-goal -> (list sealed-goal -> prop)).

A few tacticals can be found in the elpi-ltac.elpi file. For example this is the code of try:

pred try i:tactic, i:sealed-goal, o:list sealed-goal.
try T G GS :- T G GS.
try _ G [G].

Setting arguments for a tactic

As we hinted before, tactic arguments are attached to the goal since they can mention proof variables. So the Ltac code:

intro H; apply H.

has to be seen as 3 steps, starting from a goal G:

  • introduction of H, obtaining G1
  • setting the argument H, obtaining G2
  • calling apply, obtaining G3
Elpi Tactic argpass.
Elpi Accumulate lp:{{

% this directive lets you use short names
shorten coq.ltac.{ open, thenl, all }.

type intro open-tactic. % goal -> list sealed-goal
intro G GL :- refine {{ fun H => _ }} G GL.

type set-arg-n-hyp int -> open-tactic.
set-arg-n-hyp N (goal Ctx _ _ _ _ as G) [SG1] :-
  std.nth N Ctx (decl X _ _),
  coq.ltac.set-goal-arguments [trm X] G (seal G) SG1.

type apply open-tactic.
apply (goal _ _ _ _ [trm T] as G) GL :- refine T G GL.

msolve SG GL :-
  all (thenl [ open intro,
               open (set-arg-n-hyp 0),
               open apply ]) SG GL.

}}.
Elpi Typecheck.

P: Prop

P -> P
Proof. elpi argpass. Qed.

Of course the tactic playing the role of intro could communicate back a datum to be passed to what follows

thenl [ open (tac1 Datum), open (tac2 Datum) ]

but the binder structure of sealed-goal would prevent Datum to mention proof variables, that would otherwise escape the sealing.

The utility set-goal-arguments:

coq.ltac.set-goal-arguments Args G G1 G1wArgs

tries to move Args from the context of G to the one of G1. Relating the two proof contexts is not obvious: you may need to write your own procedure if the two contexts are very distant.

Tactics in terms

Elpi tactics can be used inside terms via the usual ltac:(...) quotation, but can also be exported to the term grammar.

Here we write a simple tactic for default values, which optionally takes a bound to the search depth.

Elpi Tactic default.
Elpi Accumulate lp:{{

  pred default i:term, i:int, o:term.

  default _ 0 _ :- coq.ltac.fail _ "max search depth reached".
  default {{ nat }} _ {{ 46 }}.
  default {{ bool }} _ {{ false }}.
  default {{ list lp:A }} Max {{ cons lp:D nil }} :-
    Max' is Max - 1, default A Max' D.

  solve (goal _ _ T _ [] as G) GL :-
    default T 9999 P,
    refine P G GL.

}}.
Elpi Typecheck.
Elpi Export default.

Definition foo : nat := default.
foo = 46 : nat
Definition bar : list bool := default.
bar = (false :: nil)%list : list bool

The grammar entries for Elpi tactics in terms take an arbitrary number of arguments with the limitation that they are all terms: you can't pass a string or an integer as one would normally do.

Here we use Coq's primitive integers to pass the search depth (in a compact way).

Elpi Accumulate default lp:{{
  solve (goal _ _ T _ [trm (primitive (uint63 Max))] as G) GL :-
    coq.uint63->int Max MaxI,    
    default T MaxI P,
    refine P G GL.
}}.
Elpi Typecheck.

[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Open Scope uint63_scope.
Tactic failure: max search depth reached.
Definition baz : list nat := default 2.
baz = (46%nat :: nil)%list : list nat

That is all folks!