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 the HOAS for Coq terms
Author:
Enrico Tassi
This tutorial focuses on the integration of Elpi within Coq, in particular
it describes how Coq terms are exposed to Elpi programs and how Coq APIs can
be called.
This tutorial assumes the reader is familiar with Elpi and HOAS; if it is not
the case, please take a look at the
Elpi tutorial
first.
The full syntax of Coq terms can be found in
coq-builtin.elpi
together with a detailed documentation of the encoding of contexts and the
APIs one can use to interact with Coq. This tutorial, and the two more
that focus on commands and tactics, are a gentle introduction to all that.
We defer to later quotations and antiquotations: syntactic features that
let one write terms in Coq's native syntax. Here we focus on the abstract
syntax tree of Coq terms.
constant, inductive and constructor are Coq specific
data types that are opaque to Elpi. Still the gref data type lets you
see what these names point to (a constant, and inductive type or a
constructor).
Toplevel input, characters 38-42
GRnat is linear: name it _GRnat (discard) or GRnat_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 87-92
GRplus is linear: name it _GRplus (discard) or GRplus_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 62-64
GRs is linear: name it _GRs (discard) or GRs_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
GRnat = indt «nat»
GRplus = const «Nat.add»
GRs = indc «S»
The coq.env.* family of APIs lets one access the
environment of well typed Coq terms that have a global name.
Definitionx := 2.
Toplevel input, characters 257-258
Bo is linear: name it _Bo (discard) or Bo_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 119-120
Ty is linear: name it _Ty (discard) or Ty_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 261-263
TyC is linear: name it _TyC (discard) or TyC_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
Bo = app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]
C = «x»
GR = const «x»
Ty = global (indt «nat»)
TyC = global (indt «nat»)
An expression like indt «nat» is not a Coq term (or better a type) yet.
The global term constructor turns a gref into an
actual term.
The other binders prod (Coq's forall, AKA Π) and let are similar,
so let's rather focus on fix here.
Toplevel input, characters 74-75
Bo is linear: name it _Bo (discard) or Bo_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
Bo = fix `add` 0
(prod `n` (global (indt «nat»)) c0 \
prod `m` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \
fun `n` (global (indt «nat»)) c1 \
fun `m` (global (indt «nat»)) c2 \
match c1 (fun `n` (global (indt «nat»)) c3 \ global (indt «nat»))
[c2,
fun `p` (global (indt «nat»)) c3 \
app [global (indc «S»), app [c0, c3, c2]]]
C = «Nat.add»
The fix constructor carries a pretty printing hint,
the number of the recursive argument (starting at 0), the type
of the recursive function and finally the body where the recursive
call is represented via a bound variable
typefixname->int->term->(term->term)->term.
A match constructor carries the term being inspected,
the return clause
and a list of branches. Each branch is a Coq function expecting in input
the arguments of the corresponding constructor. The order follows the
order of the constructors in the inductive type declaration.
typematchterm->term->listterm->term.
The return clause is represented as a Coq function expecting in input
the indexes of the inductive type, the inspected term and generating the
type of the branches.
Definitionm (h : 0 = 1 ) P : P 0 -> P 1 :=
match h as e in eq _ x return P 0 -> P x
with eq_refl => fun (p : P 0) => p end.
The returntype of m is: c0 \ c1 \
fun `x` (global (indt «nat»)) c2 \
fun `e`
(app [global (indt «eq»), global (indt «nat»), global (indc «O»), c2])
c3 \ prod `_` (app [c1, global (indc «O»)]) c4 \ app [c1, c2]
Query assignments:
C = «m»
RT = c0 \ c1 \
fun `x` (global (indt «nat»)) c2 \
fun `e`
(app [global (indt «eq»), global (indt «nat»), global (indc «O»), c2])
c3 \ prod `_` (app [c1, global (indc «O»)]) c4 \ app [c1, c2]
The opaque type univ is a universe level variable. Elpi holds a store of
constraints among these variables and provides APIs named coq.univ.* to
impose constraints.
typ «tutorial_coq_elpi_HOAS.6» < typ «tutorial_coq_elpi_HOAS.7»
Cannot enforce tutorial_coq_elpi_HOAS.7 <=
tutorial_coq_elpi_HOAS.6 because
tutorial_coq_elpi_HOAS.6 < tutorial_coq_elpi_HOAS.7
the user is not expected to declare universe constraints by hand
The type checking primitives update the store of constraints
automatically and put Coq universe variables in place of Elpi's unification
variables (U and V below).
Let's play a bit more with universe constraints using the
coq.typecheck API:
Toplevel input, characters 119-119
V is linear: name it _V (discard) or V_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
(id b) is: app [fun `x` (sort (typ X0)) c0 \ c0, sort (typ X1)]
(id a) is illtyped:
Illegal application:
The term "fun x : Type => x" of type "Type -> Type"
cannot be applied to the term
"Type" : "Type"
This term has type "Type@{tutorial_coq_elpi_HOAS.8+1}"
which should be a subtype of "Type@{tutorial_coq_elpi_HOAS.8}".
(universe inconsistency: Cannot enforce tutorial_coq_elpi_HOAS.8 <
tutorial_coq_elpi_HOAS.8 because tutorial_coq_elpi_HOAS.8
= tutorial_coq_elpi_HOAS.8)
after typing (id b) is:
app
[fun `x` (sort (typ «tutorial_coq_elpi_HOAS.8»)) c0 \ c0,
sort (typ «tutorial_coq_elpi_HOAS.9»)] :
sort (typ «tutorial_coq_elpi_HOAS.8»)
ErrMsg = Illegal application:
The term "fun x : Type => x" of type "Type -> Type"
cannot be applied to the term
"Type" : "Type"
This term has type "Type@{tutorial_coq_elpi_HOAS.8+1}"
which should be a subtype of "Type@{tutorial_coq_elpi_HOAS.8}".
(universe inconsistency: Cannot enforce tutorial_coq_elpi_HOAS.8 <
tutorial_coq_elpi_HOAS.8 because tutorial_coq_elpi_HOAS.8
= tutorial_coq_elpi_HOAS.8)
ID = fun `x` (sort (typ «tutorial_coq_elpi_HOAS.8»)) c0 \ c0
The diagnostic data type is used by coq.typecheck to
tell if the term is well typed. The constructor ok signals success, while
error carries an error message. In case of success universe constraints
are added to the store.
Writing Gallina terms as we did so far is surely possible but very verbose
and unhandy. Elpi provides a system of quotations and antiquotations to
let one take advantage of the Coq parser to write terms.
The antiquotation, from Coq to Elpi, is written lp:{{...}} and we have
been using it since the beginning of the tutorial. The quotation from
Elpi to Coq is written {{:coq ...}} or also just {{ ...}} since
the :coq is the default quotation (Coq has no default quotation, hence you always need
to write lp: there).
app
[global (const «Nat.add»),
app [global (indc «S»), global (indc «O»)],
app [global (indc «S»), global (indc «O»)]]
Query assignments:
S = indc «S»
One rule governs bound variables:
Important
if a variable is bound in a language, Coq or Elpi,
then the variable is only visible in that language (not in the other one).
The following example is horrible but proves this point. In real code
you are encouraged to pick appropriate names for your variables, avoiding
gratuitous (visual) clashes.
fun `x` (global (indt «nat»)) c0 \
fun `x` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c1, c0]
A commodity quotation without parentheses let's one quote identifiers
omitting the curly braces.
That is lp:{{ ident }} can be written just lp:ident.
fun `x` (global (indt «nat»)) c0 \
fun `x` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c1, c0]
It is quite frequent to put Coq variables in the scope of an Elpi
unification variable, and this can be done by simply writing
lp:(X a b) which is a shorthand for lp:{{X{{a}}{{b}}}}.
Warning
writing lp:Xab (without parentheses) would result in a
Coq application, not an Elpi one
Let's play a bit with these shorthands:
fun `a` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (const «Nat.add»), c1, c0]
Another commodity quotation lets one access the coqlib
feature introduced in Coq 8.10.
Coqlib gives you an indirection between your code and the actual name
of constants.
Register Coq.Init.Datatypes.nat as my.N.Register Coq.Init.Logic.eq as my.eq.
fun `a` (global (indt «nat»)) c0 \
fun `b` (global (indt «nat»)) c1 \
app [global (indt «eq»), global (indt «nat»), c0, c1]
Note
The (optional) @ in lib:@some.name disables implicit arguments.
The {{:gref..}} quotation lets one build the gref data type, instead of the
term one. It supports lib: as well.
indt «nat»
indt «nat»
The last thing to keep in mind when using quotations is that implicit
arguments are inserted (according to the Arguments setting in Coq)
but not synthesized automatically.
It is the job of the type checker or elaborator to synthesize them.
We shall see more on this in the section on holes.
The context of Elpi (the hypothetical program made of rules loaded
via =>) is taken into account by the Coq APIs. In particular every time
a bound variable is crossed, the programmer must load in the context a
rule attaching to that variable a type. There are a few facilities to
do that, but let's first see what happens if one forgets it.
Bound variable c0 not found in the Coq context:
Mapping from DBL:
Named:
Rel:
Did you forget to load some hypotheses with => ?
This fatal error says that x in (Bo x) is unknown to Coq.
It is
a variable postulated in Elpi, but it's type, nat, was lost. There
is nothing wrong per se in using pix\ as we did if we don't call Coq
APIs under it. But if we do, we have to record the type of x somewhere.
In some sense Elpi's way of traversing a binder is similar to a Zipper.
The context of Elpi must record the part of the Zipper context that is
relevant for binders.
The two predicates decl and def are used
for that purpose:
preddecli:term, o:name, o:term. % Var Name Ty
preddefi:term, o:name, o:term, o:term. % Var Name Ty Bo
where def is used to cross a let.
Query assignments:
Bo = c0 \
app
[global (const «Nat.add»), c0,
app [global (indc «S»), global (indc «O»)]]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \
app
[global (const «Nat.add»), c0,
app [global (indc «S»), global (indc «O»)]]
Ty = global (indt «nat»)
In order to ease this task, Coq-Elpi provides a few commodity macros such as
@pi-decl:
macro @pi-decl NTF:-pix\ decl x NT==>F x.
Note
the precedence of lambda abstraction x\ lets you write the
following code without parentheses for F.
Query assignments:
Bo = c0 \
app
[global (const «Nat.add»), c0,
app [global (indc «S»), global (indc «O»)]]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \
app
[global (const «Nat.add»), c0,
app [global (indc «S»), global (indc «O»)]]
Ty = global (indt «nat»)
Tip
@pi-decl NTyx\ takes arguments in the same order of fun and
prod, while
@pi-def NTyBox\ takes arguments in the same order of let.
The intuition is that Coq's Evar map (AKA sigma or evd), which assigns
typing judgement to evars, is represented with Elpi constraints which carry
the same piece of info.
Naked Elpi unification variables, when passed to Coq's API, are
automatically linked to a Coq evar. We postpone the explanation of the
difference "raw" and "elab" unification variables to the chapter about
tactics, here the second copy of X1 in the evar constraint plays
no role.
Now, what about the typing context?
raw T =
fun `x` (global (indt «nat»)) c0 \
app [global (const «Nat.add»), c0, X0 c0]
Universeconstraints:
UNIVERSES:
{tutorial_coq_elpi_HOAS.13} |=
Set <= tutorial_coq_elpi_HOAS.13
ALGEBRAIC UNIVERSES:
{}
FLEXIBLE UNIVERSES:
SORTS:
α8 := Type
WEAK CONSTRAINTS:
In the value of raw T we can see that the hole in x+_, which occurs under the
binder c0\, is represented by an Elpi unification variable X1 c0, that
means that X1 sees c0 (c0 is in the scope of X1).
The constraint is this time a bit more complex. Let's dissect it:
Here {...} is the set of names (not necessarily minimized) used in the
constraint, while ?- separates the assumptions (the context) from the
conclusion (the suspended goal).
As expected both Elpi's constraint and Coq's evar map record a context
with a variable x (of type nat) which is in the scope of the hole.
Unless one is writing a tactic, Elpi's constraints are just used to
represent the evar map. When a term is assigned to a variable
the corresponding constraint is dropped. When one is writing a tactic,
things are wired up so that assigning a term to an Elpi variable
representing an evar resumes a type checking goal to ensure the term has
the expected type.
We will explain this in detail in the tutorial about tactics.
This encoding of evars is such that the programmer does not need to care
much about them: no need to carry around an assignment/typing map like the
Evar map, no need to declare new variables there, etc. The programmer
can freely call Coq API passing an Elpi term containing holes.
There is one limitation, though. The rest of this tutorial describes it
and introduces a few APIs and options to deal with it.
The limitation is that the automatic declaration and mapping
does not work in all situations. In particular it only works for Elpi
unification variables which are in the pattern fragment, which mean
that they are applied only to distinct names (bound variables).
This is the case for all the {{_}} one writes inside quotations, for
example, but it is not hard to craft a term outside this fragment.
In particular we can use Elpi's substitution (function application) to
put an arbitrary term in place of a bound variable.
Toplevel input, characters 95-95
N is linear: name it _N (discard) or N_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 97-98
Ty is linear: name it _Ty (discard) or Ty_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Flexible term outsidepattern fragment:
X0 (app [global (indc «S»), global (indc «O»)])
This snippet fails hard, with the following message:
Flexible term outside pattern fragment:
X0 (app [global (indc «S»), global (indc «O»)])
Indeed Bo1 contains a term outside the pattern fragment,
the second argument of plus, which is obtained by replacing
c0 with {{1}} in X0 c0.
While programming Coq extensions in Elpi, it may happen that we want to
use a Coq term as a syntax tree (with holes) and we need to apply
substitutions to it but we don't really care about the scope of holes.
We would like these holes to stay {{_}} (a fresh hole which sees the
entire context of bound variables). In some sense, we would like {{_}}
to be a special dummy constant, to be turned into an actual hole on the
fly when needed.
This use case is perfectly legitimate and is supported by all APIs taking
terms in input thanks to the @holes! option.
Toplevel input, characters 63-63
N is linear: name it _N (discard) or N_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 65-66
Ty is linear: name it _Ty (discard) or Ty_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Bo1 before =
app
[global (const «Nat.add»),
app [global (indc «S»), global (indc «O»)],
X0 (app [global (indc «S»), global (indc «O»)])]
Bo1 after =
app
[global (const «Nat.add»),
app [global (indc «S»), global (indc «O»)], X1]
Universeconstraints:
UNIVERSES:
{tutorial_coq_elpi_HOAS.14} |=
Set <= tutorial_coq_elpi_HOAS.14
ALGEBRAIC UNIVERSES:
{}
FLEXIBLE UNIVERSES:
SORTS:
α9 := Type
WEAK CONSTRAINTS:
Note that after the call to coq.typecheck, X0 is assigned the
term _\X1, that means that the offending argument has been pruned
(discarded).
Note
All APIs taking a term support the @holes! option.
In addition to the @holes! option, there is a class of APIs which can
deal with terms outside the pattern fragment. These APIs take in input a term
skeleton. A skeleton is not modified in place, as coq.typecheck
does with its first argument, but is rather elaborated to a term related to it.
In some sense APIs taking a skeleton are more powerful, because they can
modify the structure of the term, eg. insert a coercions, but are less
precise, in the sense that the relation between the input and the output
terms is not straightforward (it's not unification).
Coercionnat2bool n := match n with O => false | _ => true end.Open Scope bool_scope.
Toplevel input, characters 221-223
Bo2 is linear: name it _Bo2 (discard) or Bo2_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 152-152
N is linear: name it _N (discard) or N_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 154-155
Ty is linear: name it _Ty (discard) or Ty_ (fresh variable)
[elpi.linear-variable,elpi.typecheck,elpi,default]
Here Bo2 is obtained by taking Bo1, considering all
unification variables as holes and all {{Type}} levels as fresh
(the are none in this example), and running Coq's elaborator on it.
The result is a term with a similar structure (skeleton), but a coercion
is inserted to make x fit as a boolean value, and a fresh hole X1 is
put in place of the term X0 (app [global (indc «S»), global (indc «O»)])
which is left untouched.
Skeletons and their APIs are described in more details in the tutorial
on commands.
That is all for this tutorial. You can continue by reading the tutorial
about
commands
or the one about
tactics.