Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. 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 commands

Author: Enrico Tassi

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 commands

Let's create a simple command, called "hello", which prints "Hello" followed by the arguments we pass to it:

[Loading ML file coq-elpi.elpi ... done]
Elpi Command hello. Elpi Accumulate lp:{{ % main is, well, the entry point main Arguments :- coq.say "Hello" Arguments. }}. Elpi Typecheck.

The program declaration is made of 3 parts.

The first one Elpi Command hello. sets the current program to hello. Since it is declared as a Command 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 postpone the description of data bases to a dedicated section.

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.

We can now run our program!

Hello [str world!]

You should see the following output (hover the bubble next to the code if you are reading this online):

Hello [str world!]

The string "world!" we passed to the command is received by the code as (str "world!").


coq.say won't print quotes around strings

Command arguments

Let's pass different kind of arguments to hello:

Hello [int 46]
Hello [str there]

This time we passed to the command a number and an identifier. Identifiers are received as strings, and can contain dots, but no spaces.

Hello [str my, str friend]
Hello [str this.is.a.qualified.name]

Indeed the first invocation passes two arguments, of type string, while the second a single one, again a string containing dots.

There are a few more types of arguments a command can receive:

  • terms, delimited by ( and )
  • toplevel declarations, like Inductive .., Definition .., etc.. which are introduced by their characterizing keyword.

Let's try with a term.

Hello [trm (app [global (indt «eq»), global (indt «nat»), global (indc «O»), app [global (indc «S»), global (indc «O»)]])]

Since Coq-Elpi 1.15, terms are received in elaborated form, meaning that the elaborator of Coq is used to pre-process them. In the example above the type argument to eq has been synthesized to be nat.

Hello [const-decl test (some (app [global (indt «eq»), global (indt «nat»), global (indc «O»), app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))]
Hello [indt-decl (record test (sort (typ «Set»)) Build_test (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ field [coercion off, canonical tt] f2 (app [global (indt «eq»), global (indt «nat»), c0, app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))]

Global declarations are received in elaborated form as well. In the case of Definition test the optional body (would be none for an Axiom declaration) is present while the omitted type is inferred (to be Prop).

In the case of the Record declaration remark that each field has a few attributes, like being a coercions (the :> in Coq's syntax). Also note that the type of the record (which was omitted) defaults to Type. Finally note that the type of the second field sees c0 (the value of the first field).

See the argument data type for a detailed decription of all the arguments a command can receive.

Processing raw arguments

It is sometimes useful to receive arguments in raw format, so that no elaboration has been performed. This can be achieved by using the #[arguments(raw)] attributed when the command is declared.

Then, thre are two ways to process term arguments: typechecking and elaboration.

#[arguments(raw)] Elpi Command check_arg.
Elpi Accumulate lp:{{

  main [trm T] :-
    std.assert-ok! (coq.typecheck T Ty) "argument illtyped",
    coq.say "The type of" T "is" Ty.

Elpi Typecheck.

The type of app [global (indt «eq»), global (indt «nat»), app [global (indc «S»), global (indc «O»)], global (indc «O»)] is sort prop
argument illtyped: Illegal application: The term "@eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "nat" : "Type" "1" : "nat" "true" : "bool" The 3rd term has type "bool" which should be a subtype of "nat".

The command check_arg receives a term T and type checks it, then it prints the term and its type.

The coq.typecheck API has 3 arguments: a term, its type and a diagnostic which can either be ok or (error Message). The assert-ok! combinator checks if the diagnostic is ok, and if not it prints the error message and bails out.

The first invocation succeeds while the second one fails and prints the type checking error (given by Coq) following the string passed to std.assert-ok!.

Coercion bool2nat (b : bool) := if b then 1 else 0.
argument illtyped: Illegal application: The term "@eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "nat" : "Type" "1" : "nat" "true" : "bool" The 3rd term has type "bool" which should be a subtype of "nat".
1 = true : Prop

The command still fails even if we told Coq how to inject booleans values into the natural numbers. Indeed the Check commands works.

The call to coq.typecheck modifies the term in place, it can assign implicit arguments (like the type parameter of eq) but it cannot modify the structure of the term. To do so, one has to use the coq.elaborate-skeleton API.

Elpi Command elaborate_arg.
Elpi Accumulate lp:{{

  main [trm T] :-
    std.assert-ok! (coq.elaborate-skeleton T Ty T1) "illtyped arg",
    coq.say "T=" T,
    coq.say "T1=" T1,
    coq.say "Ty=" Ty.

Elpi Typecheck.

T= app [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], global (indc «true»)]
T1= app [global (indt «eq»), global (indt «nat»), app [global (indc «S»), global (indc «O»)], app [global (const «bool2nat»), global (indc «true»)]]
Ty= sort prop

Remark how T is not touched by the call to this API, and how T1 is a copy of T where the hole after eq is synthesized and the value true injected to nat by using bool2nat.

It is also possible to manipulate term arguments before typechecking them, but note that all the considerations on holes in the tutorial about the HOAS representation of Coq terms apply here. An example of tool taking advantage of this possibility is Hierarchy Builder: the declarations it receives would not typecheck in the current context, but do once the context is temporarily augmented with ad-hoc canonical structure instances.


Synthesizing a term

Synthesizing a term typically involves reading an existing declaration and writing a new one. The relevant APIs are in the coq.env.* namespace and are named after the global refence they manipulate, eg coq.env.const for reading and coq.env.add-const for writing.

Here we implement a little command that given an inductive type name generates a term of type nat whose value is the number of constructors of the given inductive type.

Elpi Command constructors_num.

Elpi Accumulate lp:{{

pred int->nat i:int, o:term.
int->nat 0 {{ 0 }}.
int->nat N {{ S lp:X }} :- M is N - 1, int->nat M X.

main [str IndName, str Name] :-
  std.assert! (coq.locate IndName (indt GR)) "not an inductive type",
  coq.env.indt GR _ _ _ _ Kn _,      % the names of the constructors
  std.length Kn N,                   % count them
  int->nat N Nnat,                   % turn the integer into a nat
  coq.env.add-const Name Nnat _ _ _. % save it

Elpi Typecheck.

Elpi constructors_num bool nK_bool.
nK_bool = 2 : nat
Elpi constructors_num False nK_False.
nK_False = 0 : nat
not an inductive type: coq.locate plus (indt X0)
Global reference not found: not_there

The command starts by locating the first argument and asserting it points to an inductive type. This line is idiomatic: coq.locate aborts if the string cannot be located, and if it relates it to a gref which is not indt (for example const plus) assert! aborts with the given error message.

coq.env.indt lets one access all the details of an inductive type, here we just use the list of constructors. The twin API coq.env.indt-decl lets one access the declaration of the inductive in HOAS form, which might be easier to manipulate in other situations, like the next example.

Then the program crafts a natural number and declares a constant for it.

Abstracting an inductive

For the sake of introducing copy, the swiss army knife of λProlog, we write a command which takes an inductive type declaration and builds a new one abstracting the former one on a given term. The new inductive has a parameter in place of the occurrences of that term.

Elpi Command abstract.

Elpi Accumulate lp:{{

  % a renaming function which adds a ' to an ident (a string)
  pred prime i:id, o:id.
  prime S S1 :- S1 is S ^ "'".

  main [str Ind, trm Param] :-

    % the term to be abstracted out, P of type PTy
      (coq.elaborate-skeleton Param PTy P)
      "illtyped parameter",

    % fetch the old declaration
    std.assert! (coq.locate Ind (indt I)) "not an inductive type",
    coq.env.indt-decl I Decl,

    % let's start to craft the new declaration by putting a
    % parameter A which has the type of P
    NewDecl = parameter "A" explicit PTy Decl',

    % let's make a copy, capturing all occurrences of P with a
    % (which stands for the parameter)
    (pi a\ copy P a => copy-indt-decl Decl (Decl' a)),

    % to avoid name clashes, we rename the type and its constructors
    % (we don't need to rename the parameters)
    coq.rename-indt-decl (=) prime prime NewDecl DeclRenamed,

    % we type check the inductive declaration, since abstracting
    % random terms may lead to illtyped declarations (type theory
    % is hard)
      (coq.typecheck-indt-decl DeclRenamed)
      "can't be abstracted",

    coq.env.add-indt DeclRenamed _.

Elpi Typecheck.

Inductive tree := leaf | node : tree -> option nat -> tree -> tree.

Elpi abstract tree (option nat).
Inductive tree' (A : Set) : Set := leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. Arguments tree' A%type_scope Arguments leaf' A%type_scope Arguments node' A%type_scope _ _ _

As expected tree' has a parameter A.

Now let's focus on copy. The standard coq library (loaded by the command template) contains a definition of copy for terms and declarations.

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 P a

which, at run time, looks like

copy (app [global (indt «option»), global (indt «nat»)]) c0

and that rule masks the one for app when the sub-term being copied is exactly option nat. The API copy-indt-decl copies an inductive declaration and calls copy on all the terms it contains (e.g. the type of the constructors).

The copy predicate is very flexible, but sometimes one needs to collect some data along the way. The sibling API fold-map lets one do that.

An excerpt:

fold-map (fun N T F) A (fun N T1 F1) A2 :-
  fold-map T A T1 A1, pi x\ fold-map (F x) A1 (F1 x) A2.

For example one can use fold-map to collect into a list all the occurrences of inductive type constructors in a given term, then use the list to postulate the right number of binders for them, and finally use copy to capture them.

Using DBs to store data across calls

A Db can be created with the command:

Elpi Db name.db lp:{{ some code. }}.

and a Db can be later extended via Elpi Accumulate. As a convention, we like Db names to end in a .db suffix.

A Db is pretty much like a regular program but can be shared among other programs and is accumulated by name. Since is a Db is accumulated when a program runs the current contents of the Db are used. Moreover the Db can be extended by Elpi programs themselves thanks to the API coq.elpi.accumulate, enabling code to save a state which is then visible at subsequent runs.

The initial contents of a Db, some code in the example above, is usually just the type declaration for the predicates part of the Db, and maybe a few default rules. Let's define a Db.

Elpi Db age.db lp:{{

  % A typical Db is made of one main predicate
  pred age o:string, o:int.

  % the Db is empty for now, we put a rule giving a
  % descriptive error and we name that rule "age.fail".
  :name "age.fail"
  age Name _ :- coq.error "I don't know who" Name "is!".


Elpi rules can be given a name via the :name attribute. Named rules serve as anchor-points for new rules when added to the Db.

Let's define a Command that makes use of a Db.

Elpi Command age.
Elpi Accumulate Db age.db.  (* we accumulate the Db *)
Elpi Accumulate lp:{{

  main [str Name] :-
    age Name A,
    coq.say Name "is" A "years old".

Elpi Typecheck. 

I don't know who bob is!

Let's put some data in the Db. Given that the Db contains a catch-all rule, we need the new ones to be put before it.

Elpi Accumulate age.db lp:{{

  :before "age.fail"     % we place this rule before the catch all
  age "bob" 24.


bob is 24 years old

Extending data bases this way is fine, but requires the user of our command to be familiar with Elpi's syntax, which is not very nice. Instead, we can write a new program that uses the coq.elpi.accumulate API to extend the Db.

Elpi Command set_age.
Elpi Accumulate Db age.db.
Elpi Accumulate lp:{{
  main [str Name, int Age] :-
    TheNewRule = age Name Age,
    coq.elpi.accumulate _ "age.db"
      (clause _ (before "age.fail") TheNewRule).

Elpi Typecheck.

Elpi set_age "alice" 21.
alice is 21 years old

Additions to a Db are a Coq object, a bit like a Notation or a Type Class instance: these object live inside a Coq module (or a Coq file) and become active when that module is Imported.

Deciding to which Coq module these extra rules belong is important and coq.elpi.accumulate provides a few options to tune that. Here we passed _, that uses the default setting. See the scope and clause data types for more info.

Inspecting a Db

So far we did query a Db but sometimes one needs to inspect the whole contents.

Elpi Command print_all_ages.
Elpi Accumulate Db age.db.
Elpi Accumulate lp:{{

  :before "age.fail"
  age _ _ :- !, fail. % softly

  main [] :-
    std.findall (age _ _) Rules,
    std.forall Rules print-rule.

  pred print-rule i:prop.
  print-rule (age P N) :- coq.say P "is" N "years old".

Elpi Typecheck.
bob is 24 years old
alice is 21 years old

The std.findall predicate gathers in a list all solutions to a query, while std.forall iterates a predicate over a list. It is important to notice that coq.error is a fatal error which aborts an Elpi program. Here we shadow the catch all clause with a regular failure so that std.findall can complete to list all the results.

Polishing a command

The details do make the difference, some times.


Elpi programs can be prefixed with attributes, like #[local]. Attributes are not passed as arguments but rather as a rule in the context, a bit like the option @holes! we have seen before.

Elpi Command attr.
Elpi Accumulate lp:{{

  main _ :-
    attributes A, % we fetch the list of attributes from the context
    coq.say A.


[attribute elpi.loc (leaf-loc File "(stdin)", line 10, column 31, character 175:), attribute this (leaf-str ), attribute more (node [attribute stuff (leaf-str 33)])]

The first attribute, elpi.loc is always present and corresponds to the location in the source file of the command. Then we find an attribute for "this" holding the emptry string and an attribute for "more.stuff" holding the string "33".

Attributes are usually validated (parsed) and turned into regular options using coq.parse-attributes and a description of their types using the attribute-type data type:

Elpi Command parse_attr.
Elpi Accumulate lp:{{

  pred some-code.
  some-code :-
    get-option "more.stuff" N, get-option "this" B, coq.say N B.

  main _ :-
    attributes A,
    coq.parse-attributes A [
      att "this" bool,
      att "more.stuff" int,
    ] Opts,
    coq.say "options=" Opts,
    Opts => some-code.


options= [get-option elpi.loc File "(stdin)", line 19, column 31, character 358:, get-option this tt, get-option more.stuff 33]
33 tt
Attribute unknown is not supported

Note that get-option links a string with a datum of type any, which means no type checking is performed on it. It is recommended to wrap calls to get-option into other predicates typed in a more precise way. Eg:

pred get-my-option o:int.
get-my-option I :- get-option "my-option-name" I.

Extending the command grammar

Elpi programs can be exported as regular Coq commands, so that the final user does not need to type Elpi to invoke them.

Elpi Command Say.
Elpi Accumulate lp:{{ main [str S] :- coq.say S. }}.
Elpi Typecheck.

Elpi Export Say. (* extend the Coq command grammar *)

That is all folks!

Not yet...

Coq offers no equivalent of Tactic Notation for commands. Still Elpi commands accept any symbol or keyword as strings. It is up to the programmer to catch and report parse errors.

Elpi Command Go.
Elpi Accumulate lp:{{
  main [str Src, str "=>", str Tgt, str "/", str F] :- !,
    coq.say "going from" Src "to" Tgt "via" F.
  main _ :-
    coq.error "Parse error! Use: go <from> => <to> / <via>".
Elpi Typecheck.
Elpi Export Go.

going from source to target via plane
Parse error! Use: go <from> => <to> / <via>

Reporting errors

Last, (good) Elpi programs should fail reporting intellegible error messages, as the previous one.

Elpi Command bad.
Elpi Accumulate lp:{{ main []. }}.
Elpi Typecheck.
Elpi Export bad.

The elpi tactic/command bad failed without giving a specific error message. Please report this inconvenience to the authors of the program.

If they just fail, they produce the following generic error:

The elpi tactic/command bad failed without giving a
specific error message. Please report this
inconvenience to the authors of the program.

You should use the coq.error API or the assert! one to abort a program. There is a dedicated coq.ltac.fail API to abort tactics.

Warnings can be reported using the coq.warning which lets you pick a name and category. In turn these can be used to disable or make fatal your warnings (as any other Coq warning).

This is really the end, unless you want to learn more about writing tactics in Elpi, in that case look at that tutorial ;-)