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.
(True * nat)%type
Proof.
split.
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.

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


Lemma test_split : exists t : Prop, True /\ True /\ t.
exists t : Prop, True /\ True /\ t
Proof.
eexists.
True /\ True /\ ?t
repeat elpi split. (* The failure is caught by Ltac's repeat *)
True
True
?t
(* Remark that the last goal is left untouched, since
   it did not match the pattern {{ _ /\ _ }}. *)
all: elpi blind.
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.

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


Lemma test_split2 : exists t : Prop, True /\ True /\ t.
exists t : Prop, True /\ True /\ t
Proof.
eexists.
True /\ True /\ ?t
repeat elpi split2.
True
True
?t
all: elpi blind.
Qed.

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.
P, Q: Prop
H: P -> Q
p: P
Q
Proof.
use (H _).
Using H ?p of type Q
P, Q: Prop
H: P -> Q
p: P
P
use q.
No such hypothesis: q
use p.
Using p of type P
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.
P, Q: Prop
H: P -> Q
p: P
Q
print P, p, (H p).
[trm c0, trm c3, trm (app [c2, c3])]
Abort.

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


Lemma test_assumption  (P Q : Prop) (p : P) (q : Q) : P /\ id Q.
P, Q: Prop
p: P
q: Q
P /\ id Q
Proof.
split.
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
id Q
elpi assumption.
P, Q: Prop
p: P
q: Q
id Q
elpi assumption.
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".
}}.


Lemma test_assumption2  (P Q : Prop) (p : P) (q : Q) : P /\ id Q.
P, Q: Prop
p: P
q: Q
P /\ id Q
Proof.
split.
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".
}}.


Lemma test_assumption3  (P Q : Prop) (p : P) (q : Q) : P /\ id Q.
P, Q: Prop
p: P
q: Q
P /\ id Q
Proof.
split.
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").
}}.


Lemma test_find (P Q : Prop) : (P /\ P) \/ (P /\ Q).
P, Q: Prop
P /\ P \/ P /\ Q
Proof.
elpi find (P).
found P
P, Q: Prop
P /\ P \/ P /\ Q
elpi find (Q /\ _).
Tactic failure: not found.
elpi find (P /\ _).
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").

}}.


Lemma test_set (P Q : Prop) : (P /\ P) \/ (P /\ Q).
P, Q: Prop
P /\ P \/ P /\ Q
Proof.
elpi set "x" (P).
P, Q: Prop
x:= P: Prop
x /\ x \/ x /\ Q
unfold x.
P, Q: Prop
x:= P: Prop
P /\ P \/ P /\ Q
elpi set "x" (Q /\ _).
Tactic failure: not found.
elpi set "x" (P /\ _).
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.

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.

}}.


Lemma test_undup (P Q : Prop) : P /\ Q.
P, Q: Prop
P /\ Q
Proof.
split.
P, Q: Prop
P
P, Q: Prop
Q
all: elpi ngoals.
#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.

}}.
Toplevel input, characters 251-253
G1 is linear: name it _G1 (discard) or G1_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 299-301
G2 is linear: name it _G2 (discard) or G2_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]


Lemma test_undup (P Q : Prop) (p : P) (q : Q) : P /\ Q /\ P.
P, Q: Prop
p: P
q: Q
P /\ Q /\ P
Proof.
repeat split.
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
Q
P, Q: Prop
p: P
q: Q
P
Show Proof.
(fun (P Q : Prop) (p : P) (q : Q) =>
 conj ?Goal (conj ?Goal0 ?Goal1))
all: elpi undup.
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
Q
Show  Proof.
(fun (P Q : Prop) (p : P) (q : Q) =>
 conj ?Goal0 (conj ?Goal ?Goal0))
-
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 ?Goal0 (conj ?Goal ?Goal0))

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.

}}.


Lemma test_argpass (P : Prop) : P -> P.
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.