Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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 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.

HOAS for Gallina


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.

Constructor global

Let's start with the gref data type (for global rerence).

type const constant -> gref.
type indt inductive -> gref.
type indc constructor -> gref.

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).

The coq.locate API resolves a string to a gref.

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.

Definition x := 2.

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.

type global gref -> term.

Constructors app and fun

The app term constructor takes a list of terms and builds the (n-ary) application. The first term is the head, while the others are the arguments.

For example app [global (indc «S»), global (indc «O»)] is the representation of 1.

type app   list term -> term.

Let's move to binders!

Definition f := fun x : nat => x.

Query assignments:
Bo = fun `x` (global (indt «nat»)) c0 \ c0
C = «f»

The fun constructor carries a pretty printing hint `x`, the type of the bound variable nat and a function describing the body:

type fun  name -> term -> (term -> term) -> term.

Note

name is just for pretty printing: in spite of carrying a value in the Coq world, it has no content in Elpi (like the unit type)

Elpi terms of type name are just identifiers written between ` (backticks).

Query assignments:
B = X0
T = X1

API such as coq.name-suffix lets one craft a family of names starting from one, eg coq.name-suffix `H` 1 N sets N to `H1`.

Constructors fix and match

The other binders prod (Coq's forall, AKA Π) and let are similar, so let's rather focus on fix here.

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

type fix   name -> 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.

type match term -> term -> list term -> 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.

Definition m (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 return type 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]

Constructor sort

The last term constructor worth discussing is sort.

type sort  universe -> term.
type prop universe.
type typ univ -> universe.

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
Query assignments:
U = typ «tutorial_coq_elpi_HOAS.6»
U1 = typ «tutorial_coq_elpi_HOAS.7»
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.7 tutorial_coq_elpi_HOAS.6} |= tutorial_coq_elpi_HOAS.6 < tutorial_coq_elpi_HOAS.7 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: SORTS: WEAK CONSTRAINTS:

Note

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:

(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»)
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.9 tutorial_coq_elpi_HOAS.8} |= tutorial_coq_elpi_HOAS.9 < tutorial_coq_elpi_HOAS.8 ALGEBRAIC UNIVERSES: {tutorial_coq_elpi_HOAS.9 tutorial_coq_elpi_HOAS.8} FLEXIBLE UNIVERSES: tutorial_coq_elpi_HOAS.9 tutorial_coq_elpi_HOAS.8 SORTS: WEAK CONSTRAINTS:
Query assignments:
A = sort (typ «tutorial_coq_elpi_HOAS.8»)
B = sort (typ «tutorial_coq_elpi_HOAS.9»)
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
T = sort (typ «tutorial_coq_elpi_HOAS.8»)
U = «tutorial_coq_elpi_HOAS.8»
V = «tutorial_coq_elpi_HOAS.9»
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.9 tutorial_coq_elpi_HOAS.8} |= tutorial_coq_elpi_HOAS.9 < tutorial_coq_elpi_HOAS.8 ALGEBRAIC UNIVERSES: {tutorial_coq_elpi_HOAS.9 tutorial_coq_elpi_HOAS.8} FLEXIBLE UNIVERSES: tutorial_coq_elpi_HOAS.9 tutorial_coq_elpi_HOAS.8 SORTS: WEAK CONSTRAINTS:

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.

Quotations and Antiquotations

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»), app [global (indc «S»), global (indc «O»)]]] = app [global (const «Nat.add»), app [global (indc «S»), global (indc «O»)], app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]]

Of course quotations can nest.

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 shorhand for lp:{{ X {{ a }} {{ b }} }}.

Warning

writing lp:X a b (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]
Query assignments:
X = c0 \ 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.

before: fun `ax` (global (indt «nat»)) c0 \ fun `b` (global (indt «nat»)) c1 \ app [global (indt «eq»), X0 c1, c0, c1]
after: fun `ax` (global (indt «nat»)) c0 \ fun `b` (global (indt «nat»)) c1 \ app [global (indt «eq»), global (indt «nat»), c0, c1]
Query assignments:
T = fun `ax` (global (indt «nat»)) c0 \ fun `b` (global (indt «nat»)) c1 \ app [global (indt «eq»), global (indt «nat»), c0, c1]
_uvk_1_ = c0 \ global (indt «nat»)
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.11 tutorial_coq_elpi_HOAS.10} |= tutorial_coq_elpi_HOAS.11 < tutorial_coq_elpi_HOAS.10 Set <= tutorial_coq_elpi_HOAS.11 tutorial_coq_elpi_HOAS.11 <= eq.u0 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: SORTS: α6 := Type WEAK CONSTRAINTS:

The context

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 pi x\ 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:

pred decl i:term, o:name, o:term.         % Var Name Ty
pred def  i: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 N T F :- pi x\ decl x N T => 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 N Ty x\ takes arguments in the same order of fun and prod, while @pi-def N Ty Bo x\ takes arguments in the same order of let.

Holes (implicit arguments)

An "Evar" (Coq slang for existentially quantified meta variable) is represented as a Elpi unification variable and a typing constraint.

raw T = X0
SHELF: FUTURE GOALS STACK:
Coq-Elpi mapping: RAW: ELAB:
--------------------------------
evar (X1) (global (indt «nat»)) (X1) /* suspended on X1 */
EVARS: ?X11==[ |- nat] (internal placeholder) {?e0} ?X10==[ |- => nat] (internal placeholder) SHELF: FUTURE GOALS STACK: ?X11
Coq-Elpi mapping: RAW: ?X11 <-> X1 ELAB: ?X11 <-> X1
Query assignments:
T = X1
_uvk_4_ = X1
Syntactic constraints: evar (X1) (global (indt «nat»)) (X1) /* suspended on X1 */
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.12} |= Set <= tutorial_coq_elpi_HOAS.12 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: SORTS: α7 := Type WEAK CONSTRAINTS:

Before the call to coq.typecheck, coq.sigma.print prints nothing interesting, while after the call it also prints the following syntactic constraint:

evar (X1) (global (indt «nat»)) (X1)  /* suspended on X1 */

which indicates that the hole X1 is linked to a Coq evar and is expected to have type nat.

Now the bijective mapping from Coq evars to Elpi's unification variables is not empty anymore:

Coq-Elpi mapping:
RAW:
?X11 <-> X1
ELAB:
?X11 <-> X1

Note that Coq's evar identifiers are of the form ?X<n>, while the Elpi ones have no leading ?. The Coq Evar map says that ?X11 has type nat:

EVARS:
 ?X11==[ |- nat] (internal placeholder) {?e0}
 ?X10==[ |- => nat] (internal placeholder)

SHELF:
FUTURE GOALS STACK:
 ?X11

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]
{c0 c1} : decl c1 `x` (global (indt «nat»)) ?- evar (X1 c1) (global (indt «nat»)) (X1 c1) /* suspended on X1 */
EVARS: ?X13==[x |- nat] (internal placeholder) {?e0} ?X12==[x |- => nat] (internal placeholder) SHELF: FUTURE GOALS STACK: ?X13
Coq-Elpi mapping: RAW: ?X13 <-> c0 \ X1 c0 ELAB: ?X13 <-> X1
Query assignments:
Bo = c0 \ app [global (const «Nat.add»), c0, X1 c0]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \ app [global (const «Nat.add»), c0, X1 c0]
Ty = global (indt «nat»)
_uvk_9_ = c0 \ X1 c0
Syntactic constraints: {c0 c1} : decl c1 `x` (global (indt «nat»)) ?- evar (X1 c1) (global (indt «nat»)) (X1 c1) /* suspended on X1 */
Universe constraints: 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:

{c0 c1} : decl c1 `x` (global (indt «nat»))
  ?- evar (X1 c1) (global (indt «nat»)) (X1 c1)  /* suspended on X1 */

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).

The mapping between Coq and Elpi is:

Coq-Elpi mapping:
RAW:
?X13 <-> c0 \ X1 c0
ELAB:
?X13 <-> X1

where ?X13 can be found in Coq's sigma:

EVARS:
 ?X13==[x |- nat] (internal placeholder) {?e0}
 ?X12==[x |- => nat] (internal placeholder)

SHELF:
FUTURE GOALS STACK:
 ?X13

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.

Outside the pattern fragment

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 declared 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.

Bo1 (not in pattern fragment) = app [global (const «Nat.add»), app [global (indc «S»), global (indc «O»)], X0 (app [global (indc «S»), global (indc «O»)])]
Flexible term outside pattern 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.

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]
Query assignments:
Bo = c0 \ app [global (const «Nat.add»), c0, X1]
Bo1 = app [global (const «Nat.add»), app [global (indc «S»), global (indc «O»)], X1]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \ app [global (const «Nat.add»), c0, X1]
Ty = global (indt «nat»)
_uvk_15_ = c0 \ X1
Syntactic constraints: evar (X1) (global (indt «nat»)) (X1) /* suspended on X1 */
Universe constraints: 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).

Coercion nat2bool n := match n with O => false | _ => true end.
Open Scope bool_scope.

Query assignments:
Bo = c0 \ app [global (const «andb»), c0, X0 c0]
Bo1 = app [global (const «andb»), app [global (indc «S»), global (indc «O»)], X0 (app [global (indc «S»), global (indc «O»)])]
Bo2 = app [global (const «andb»), app [global (const «nat2bool»), app [global (indc «S»), global (indc «O»)]], X1]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \ app [global (const «andb»), c0, X0 c0]
Ty = global (indt «nat»)
_uvk_21_ = X0
Syntactic constraints: evar (X2) (global (indt «bool»)) X1 /* suspended on X2, X1 */

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.