Tutorial Ltac2: Quoting

Main contributors

• Gaëtan Gilbert

Summary

Quoting provides syntax to embed one language in another. In particular, Ltac2 provides syntax to embed and to be embedded in Gallina (the language of terms) and Ltac1.

Table of content

• 1. Names (ident / @, reference)
• 2. Quoting: Using Rocq's Terms in Ltac2
  • 2.1 Quoting Terms
  • 2.2 Quoting Terms Without Existential Variables
  • 2.3 Preterms : Internalize without Typechecking
• 3. Ltac2 in Terms
• 4. Quotations as Ltac2 Notations
• 5. Ltac1 and Ltac2

Prerequisites

Needed:

• Basic knowledge of Ltac2

Installation:

• Ltac2 and its core library are available by default with Rocq.

Load Ltac2

Enable "printf" Ltac2 notation

1. Names (ident / @, reference)

The grammar of names may be trivial but it still needs some syntax to produce name constants in Ltac2 expression. Identifiers are of type ident, and can be create using @x (short for ident:(x)) and evaluates to the name "x"

For instance, to refer to an hypothesis H, we can use @H which creates an ident "H" we can then pass to Control.hyp to recover the variable

Note, up to Rocq 9.2, there is a slight printing inconsistency: the evaluated identifier is printed with the @ syntax, but the non evaluated Ltac2 expression is printed with ident:(...):

Ltac2 also has syntax for term references (constants, inductive types, inductive constructors, section variables and hypotheses of the goal context). This corresponds to type Ltac2.Std.reference (short name Std.reference with our current Imports).

Unfortunately automatic printing of such values is currently quite bad: Std.IndRef <abstr>. The easiest way to print it is to use Env.instantiate to turn the reference into a term:

Importantly, names are resolved when the Ltac2 expression is typechecked, not when it is evaluated:

Using & forces the name to be interpreted as a variable name, without checking (we do not check because variables may be dynamically introduced, see & in section 3 of this tutorial):

2. Quoting: Using Rocq's Terms in Ltac2

The language of Rocq terms (Gallina) and the Ltac2 language are not the same language, and do not have the same grammar. For instance, ∀ n, n + 0 = n is a Gallina expression which does not parse as a Ltac2 expression, and fun () ⇒ 0 is a Ltac2 expression which does not parse as a Gallina expression. A Rocq term is not a Ltac2 expression, as is, but it can be turned into a Ltac2 expression we can manipulate, in different ways. Such an operation is call "quoting" (from Rocq to Ltac2).

2.1 Quoting Terms

The most common method to quote a Rocq term, is to '. Its resulting type will be constr, the type of Rocq terms in Ltac2.

A term t is quoted in two steps: 1. The term is internalized when the Ltac2 expression is typechecked. This does several things like name resolution or interpreting notations. See "internalization" through the glossary index in the reference manual. 2. When the Ltac2 expression is evaluated, the internalization of t is typechecked in the current context, returning the elaborated term. See " type inference" through the glossary index in the reference manual. Note that ' does not run typeclass inference. For instance, trying to quote an undefined variable returns an error:

Moreover, because typechecking a term requires a context (which contains the hypotheses), it throws an error if more than one goal is focused. For instance, the following fails as there are two goals after split:

Moreover, this error is "thrown", meaning it cannot be caught by "try" and can only be caught at toplevel with "Fail".

If no goal is focused the section context (empty when there are no sections) is used instead of the goal context.

The converse operation is "unquoting" which consists in turning a Ltac2 constr into a Rocq term, and can be performed with $. For instance, if we match the context for a proof of h : False, we get the associated Ltac2 constr, with Control.hyp, then we recover the Rocq term with $h we can pass to destruct.

As an important technical point, note it is not possible to directly write $(Control.hyp h) or variation of that. It is only possible to unquote variables. The reason is that functions like Control.hyp needs a goal, where $ does not. You hence need a ltac2:() wrapper, c.f. section 3. ' is an notation for open_constr:. The name open_constr comes from the fact that quoted terms can include existential variables. This is very practical to write tactics. For instance, suppose, we have an hypothesis ∀ x : A, B x we want to specialize. We would like to create a new goal of type A, to prove x : A using tactics. We can do so by: 1. Recovering the type ?a by matching the type of the hypothesis 2. Creating a new existential variables with (_ :> $a), 3. Quoting it let e := '(_ :> $a) to get a Ltac2 expression e we can manipulate 4. Specialize the hypothesis h with specialize ($h $e) 5. Following these steps, the existential variable is shelved. Therefore, to create a goal A, we wrap the expression in unshelve. Combined, this gives us the following small tactic:

To refer to an hypothesis H, we use @H

We can also wrap it in a notation, to do the quoting for us

2.2 Quoting Terms Without Existential Variables

It also possible to quote terms without allowing existential variables, using the quotation constr: instead of open_constr:. For instance, quoting a wildcard _ fails for constr::

As for open_constr, the resulting type of constr: is the type constr Try not to confuse the Ltac2 type constr, and the quotation syntax constr:(...). As you may have noticed, the error message above is referring to instances: "Could not find an instance for the following existential variables: ?y : ?T". The reasons is that unlike open_constr:, constr: runs typeclass inference. Another difference is that constr:(...) substitutes all defined evars by their bodies in the returned term. Because defined evars are indistinguishable from their bodies, this difference only matters for performance. The main impact is that it makes recursive term construction using constr:(...) quadratic as the progressively constructed terms are repeatedly traversed to do the evar expansions:

If succ uses open_constr:(...), nat_of_int is linear in n:

but with constr:(...) it is quadratic (n = 5000 is enough to notice the slowdown without taking very long on the author's machine, use a higher number if you have a faster machine).

You can play with the value of n to see the performance curve, for instance 10_000 should take twice the time with open_constr:(...) but four times with constr:(...).

2.3 Preterms : Internalize without Typechecking

In some case, we want to manipulate a Rocq term in Ltac2, but do not want to typecheck it as quoting does. Two main examples are:

• we have more than one goal, and need to postpone typehecking to focus first
• because we want to do typechecking differently, e.g. with a particular expected type

In other words, we want to internalize a term, but postpone typechecking, and trigger it by hand. This is possible, and corresponds to the Ltac2 type preterm, which can be created using the quotation preterm:. For instance, let us quote a term that does not typecheck.

A preterm can then be turned into a value of type constr using Ltac2.Constr.pretype, which runs typechecking like the constr: quotation, or Ltac2.Constr.Pretype.pretype for more control.

As for constr, preterm can be unquoted into Rocq terms using $preterm:x. Typechecking $preterm:x will typecheck the preterm bound to x using the current flags of the surrounding term expression, and the expected type according to the typechecking algorithm. Multiple occurences of $preterm:x are typechecked independently. For instance in the following example the hole for the type of x produces separate existential variables, which are then instantiated by unification to nat and bool.

Preterms also occur naturally when quoting Ltac2 inside a notation definition: the notation variables are bound as Ltac2 variables of type preterm in the Ltac2 expression. Inside the Ltac2 expression they are not bound as term variables:

and not bound with type constr:

but they are bound with type preterm:

Since we used exact in the notation, it rejects unsolved existential variables on the right:

Note that preterms close over (contain a copy of) the Ltac2 bound variables visible when it is created. For instance the following produces "0" not "1":

and the following does not produce a "unbound variable x" error:

and in general functions like the following work as expected:

3. Ltac2 in Terms

We can write a Ltac2 expression inside a Gallina expression:

The ltac2 expression is typechecked when the Gallina term is internalized. See "internalization" through the glossary index in the reference manual. It should have type unit, but other types are tolerated (with a warning). When the Gallina term is typechecked (see "type inference" through the glossary index in the reference manual), a new existential variable is created whose context is the context of the quotation (i.e. the context of the full Gallina expression extended with any local variables) and conclusion if the expected type of the quotation according to the typechecking algorithm. The Ltac2 tactic is then evaluated with that evar as the single focused goal. If there is no expected type (for instance in the above Check), a fresh type evar is also created in the same context to be the conclusion. The term produced by the quotation is the evar, which is typically instantiated by the tactic (for instance by 0 in the above Check). If the tactic fails, it causes typechecking the term to fail:

Ltac2 internalizes terms without awareness of what variables may have been introduced by a previous tactic. For instance:

When we need to refer to such a dynamically introduced variable, we can use the &x syntax:

&x actually expands to ltac2:(Control.refine (fun () ⇒ Control.hyp @x)). We can see it if we print the above definition:

Because goal contexts cannot contain duplicated names, the names of local variables may be mangled when generating the existential variable to run the quoted tactic:

The result prints fun x x0 ⇒ (x0, x): in general name mangling when generating the evar context does not match name mangling done by printing, and it should not be relied upon. When we quote a term inside a Ltac2 expression, it is common to want to refer back to a Ltac2 variable which is bound to a term. We can use the general quotation for this:

but for more convenience we also have the $x syntax:

Note that $x is generally equivalent to ltac2:(refine x) but does not actually expand to it and may have differences. In particular, $x does not need to generate an existential variable to run a tactic, it directly expands to the term bound to Ltac2 variable x.

4. Quotations as Ltac2 Notations

Most (all?) Ltac2 quotations do not need to be primitive (though they often are) and can be written as Ltac2 notations. (Note: this is only the case for quotations embedding some syntax in Ltac2 syntax, not in the other direction. For instance ltac2:(...) in terms currently must be primitive syntax.) For instance we can define a notation equivalent to ident:(...):

or a notation equivalent to ':

In fact even the constr and open_constr notation arguments ("syntactic classes") do not need to be primitive and could be implemented on top of preterm. For instance the following notation provides a short quotation equivalent to constr:(...):

Exercise: define a open_constr_with_tc:(...) quotation equivalent to open_constr:(...) but without skipping typeclass inference. Hint: Ltac2.Constr.Pretype.open_constr_flags_no_tc makes Ltac2.Constr.Pretype.pretype behave like open_constr:(...). Exercise: define a fast_constr:(...) quotation equivalent to constr:(...) but without substituting defined evars, such that using it with nat_of_int is fast. Hint: Ltac2.Constr.Pretype.Flags.set_nf_evars is used to control the evar substitution.

5. Ltac1 and Ltac2

We can embed a Ltac1 expression into Ltac2 using ltac1:(...). This can be practical, for instance, for transitioning from Ltac1 to Ltac2. The resulting Ltac2 expression has type unit, and evaluating it runs the Ltac1 tactic:

Ltac1 tactics quoted into Ltac2 can be quantified over Ltac1 variables using ltac1:(x1 .. xn |- ...). This produces a ltac2 expression of type Ltac1.t → .. → unit, with n Ltac1.t arguments.

Values of type Ltac1.t may be constructed using the APIs in module Ltac2.Ltac1.

(note that in Ltac1 printing terms automatically focuses on each current goal, so it produces no output when there are no goals:)

We can also embed Ltac2 inside Ltac1 using ltac2:(...) which runs the Ltac2 tactic when evaluated:

The Ltac2 expression should have type unit, but other types are tolerated with a warning (the returned value is ignored):

The ltac2 expression may also quantify over variables with the "|-" syntax, and such variables will be bound with type Ltac1.t. Ltac1 syntax does not support directly applying quotations (ltac2:(x |- ...) vx) so we have to let-bind it: