Ltac2 Quickstart

Ltac2 is a new language for writing tactics in Coq. Unlike its predecessor Ltac, Ltac2 supports features such as data types, static typing, and a more readable syntax for metaprogramming. The goal of this document is to introduce the basic features of Ltac2 as an ML-family functional programminig language, and the APIs that would allow you to write tactics by modifying the proof state. Before we start the tutorial, we first require and import the Ltac2 library.

For reasons we will discuss later, if you are eager to try out Ltac2 on an existing Rocq project, you should run the following command right after the Ltac2 import so your existing scripts don't break

Functional Programming with Ltac2

Basics

The main purpose of Ltac2 is a metaprogramming language for constructing Gallina terms, which are terms that we use in our Rocq definitions and proof objects. The definitions of Ltac2 and Gallina live in different namespaces. To write Ltac2 definitions, we use commands that are prefixed Ltac2

The command above binds the Ltac2 variable two to the number 2 of type int. Unlike Ltac, Ltac2 is statically typed. When the type annotation is omitted, the type is inferred.

We can query the type of an Ltac2 term using the command Ltac2 Check, analogous to how we use the Check command to query the type of Gallina terms.

Unsurprisingly, both two and three share the type int. The Ltac2 Eval command allows us to evaluate an Ltac2 expression.

We get the integer 7 from adding up 2, 3, and 2 Note that the + symbol is not part of the syntax of Ltac2 for integer addition. We need to use the Int.add function from the Ltac2 standard library to add up Ltac2 integers. The Int module was made available from the earlier Requrie Import command. We can also import the Int module itself so we don't have to write the Int qualifier for add.

The syntax for defining Ltac2 functions is almost the same as the syntax for Gallina functions. Here are some different ways of defining a function that doubles its input.

We can also use let bindings in our definition.

The Hindley-Milner inference algorithm allows us to write polymorphic functions with few annotations.

Here, the 'a stands for a type parameter, which can be instantiated to the type of the argument of the identity function.

The rec keyword allows us to define recursive functions. Here, we define the factorial function fact over integers, making use of the library functions le, mul, and sub from the Int module of the Ltac2 library, which you can find here.

The rec keyword can also be used in conjunction with the let keyword to define local recursive functions. Let's use let rec to define a more efficient tail-recursive version of fact.

Ltac2, like its predecessor Ltac, does not enforce termination checking.

Evaluate loop 0 (or loop with any argument) at your own risk, as Rocq would get stuck in an infinite loop! In addition to functions and integers, Ltac2 supports built-in product types. The constructor takes the form (a,b). The eliminators fst and snd allows us to extract out the first component a and the second component b respectively.

Recursive data types and records

Like Haskell and OCaml, Ltac2 supports algebraic data types. Let's start by defining a simple type coin, which has two constructors Head and Tail. Note that the constructors must be capitalized.

We can eliminate values of an algebraic data type through pattern matching, which has a syntax that is very similar to match for Gallina terms.

In case you haven't noticed, if you forgot a specific piece of Ltac2 syntax, you can always make an educated guess if you are already familiar with OCaml or Gallina. We can also define recursive data types by including the rec keyword. Here's how we define the nat type for Ltac2. Note that the parentheses around pnat in S (pnat) is not optional.

We can write a recursive function that adds two peano numbers. We name our function padd to disambiguate it from the add we imported from the Int module.

As an exercise, rewrite the definitions of to_int so it converts from a peano number to its integer representation

For the next example, let us consider a binary tree which stores integers.

The leaf constructor Empty takes no argument. The Node constructor takes three arguments, including an int, and its two child nodes. These arguments are separated by comma, which is quite different from Gallina's syntax, but the pattern matching form works the same way regardless.

We can generalize the int_tree definition to the following tree data type, which abstracts the int type with a type parameter 'a

Note that the type arguments to the type constructor tree preceeds the type constructor itself. A tree of booleans, for example, is written as bool tree instead of tree bool.

If your data type is parameterized by multiple type parameters, you need to put them together with parentheses. For example, here's how we define our own pair type

We can recover the projection operators through pattern matching.

Again, thanks to the Hindley-Milner style inference, our functions are automatically polymorphic without any explicit annotations.

A side note: since Pair has only one constructor, we can directly pattern match in function arguments.

A different (and perhaps better) way of defining pairs is to use a record type definition, where we specify the data type by specifying the fields the type contains.

To construct a value of a record type, we specify what the individual fields should be.

Of course, we can always define a constructor to save some typing.

The following ltac2 expression evaluates to the same pair containing 4 and 9

We can project out individual component by appending a record value with .(fieldname)

We can define the following swap function that swaps the first and second components of a pair

The rec keyword also works for record types. Here's how we can define an infinite stream type. Note that the tail is defined as a function that maps a trivial unit input to another stream. We need to use the trivial function arrow to "thunk" the tail since Ltac2 is strict

We can access the actual tail of the list by passing it the unit value ().

We define the sequence of numbers n, n + 1, n + 2, ... as follows

Data types from the standard library

The standard library of Ltac2 already includes some useful data types, including bool and list. We can print out their definitions using the Print Ltac2 Type command.

Both data types come with special syntactic forms,

and library functions.

You can check the definitions of those library functions with the command Print Ltac2

In general, you can find the documentations of the library functions from the reference manual for the standard library by searching the keyword "Ltac2".

Interacting with proof states

Constructing and Matching Gallina Terms

The standard library of Ltac2 exposes APIs that allow the programmer to use Ltac2 to construct Gallina/Rocq terms and manipulate proof states. Let us start by constructing the Gallina term 1 + 2.

In the definition of two_plus_one, we use a special syntax where we write () when a function parameter is expected. This syntax tells Ltac2 that our function takes the unit value () as its input. The constr data type is an opaque ltac2 data type used to represent Gallina terms. To tell Ltac2 that we are defining a Gallina term, we wrap the expression with '(...). To be able to retrieve the term, we need to pass the unit value () to two_plus_one

Why must we define two_plus_one as a function instead of a constant of type constr? In Ltac2, top-level definitions must be a value. Instead of knowing precisely what values are, it is helpful to think of the values as Ltac2 expressions that do not evaluate on their own. For example, the following definitions are valid.

In int_val, the integer value doesn't really compute on its own. In func_val, the function doesn't evaluate/reduce unless we pass it two integer arguments. The following definition is an invalid top-level definition, because its body involves the call to the add function.

The following function definition is invalid, because the lambda is nested in a computation

What about constr? Why is '(1 + 2) not count as a value? It turns out that when we construct Gallina terms, Ltac2 always type checks the term, which may fail.

Therefore, for top-level Ltac2 definitions of Gallina terms, we can only write functions that, if successfully returns, give us back a well-typed Gallina term. However, local definitions or expressions we send to Ltac2 Eval don't subject to the same restriction.

If you don't understand why just yet, you can simply write definitions without thinking about the unit parameter, and if your definition is invalid, Ltac2 will give you an error message to remind you to add a (). Given an Ltac2 variable of type constr, we can use the $var syntax to interpolate the variable inside a Gallina expression we are constructing.

The results in an error as there's no top-level Gallina definition named x.

In fact, Rocq will give a warning that the variable x is unused, as the x in (x * 2) refers to a Gallina variable x, which is not in the same namespace as Ltac2 variables. As an exercise, given the following Gallina definition of x, check the result of the following Ltac2 Eval command and see if the return value is as expected.

The constr type is opaque and therefore we cannot directly examine the ast of a Gallina term by pattern matching a value of type constr. Instead, we use the lazy_match! construct to match constr terms.

The lazy_match! syntactic form takes a Gallina term of type constr. For each branch, we write patterns that involve Gallina terms with the binders prefixed with a question mark. When we don't care what a term is, we can use the wildcard pattern _, as we did in the multiplcation case. The pattern matching does not have to be exhaustive. If we invoke lhs_of on a term that doesn't match any of the patterns, we end up with a Match_failure exception.

We can write more sophisticated functions such as the following, which mirrors the operands of the + operator.

Instead of directly manipulating constr, we can leverage Ltac2 data types for domain-specific problems. We use the Arith data type to represent the arithmetic expressions we wish to manipulate.

We write the following function that converts from constr to Arith.

The mirroring operation can then be carried out on Arith through the match form.

The following function converts the Arith expressions back to Gallina terms

We can then give an alternative definition of mirror_plus, which composes all the functions we have defined so far.

For a function as simple as mirror_plus, our setup for mirror_plus' is an overkill. For bigger projects, leveraging the Ltac2 data type makes it more convenient to analyze and transform Gallina terms.

Writing Tactics

In the previous section, we learned how to construct and match Gallina terms. In this section, we learn how to use Ltac2 to help us write Rocq definitions or proofs. Let's start with the following simple statement.

Using the intros tactic, we can add the hypotheses to our proof context.

The Control module from Ltac2 contains functions that can query and manipulate the proof state. For example, the Control.hyps function allows us to see the list of hypotheses in the context.

The Control.hyps functions returns a list of tuples, containing the name of the hypotheses, its body if it has one, and its type. The Control.refine function takes a computation/thunk that returns a Gallina term, and tries to use that term to complete the goal. Instead of using Ltac2 Eval, we use the ltac2:(...) form, which takes an Ltac2 expression of type unit, which, when executed, can modify the proof state.

Recall the flag we set near the beginning of the tutorial.

By setting the default proof mode to "Classic", Rocq expects the proof script to be written in Ltac. As a consequence, the expression Control.refine (fun _ => 'h0) must be wrapped in ltac2:(...) to remind Rocq that we are writing Ltac2, not Ltac. Without the Set Default ... command, importing Ltac2 will set the proof mode to "Ltac2". As of today, having Ltac2 as the default proof mode is not very desirable, since many tactic libraries (e.g. CoqHammer, mathcomp) are only available in Ltac. More likely, your proof script will break with "Ltac2" being the default proof mode.

A more realistic workflow would involve defining complex tactics in Ltac2, and export the Ltac2 tactic to Ltac1 through FFI. We demonstrate this workflow by defining a naive implementation of the assumption tactic, which completes the goal by searching for a hypothesis that has a matching type. The find_assumption function returns the identifier of the hypothesis whose type matches the goal by composing several library functions. Control.goal gives the type of the goal. List.find takes a boolean predicate and returns the first element of the input list where the predicate holds. Constr.equal checks the alpha-equivalence of two Gallina terms.

Our full tactic is defined as follows, where Control.hyp converts an identifier to a Gallina term, which Control.refine expects as the return value of its input thunk

We can already use myassumption in our proof script, though it is quite verbose to write the ltac2 boilerplate.

The first thing we can do is to wrap myassumption inside an Ltac2 Notation so we don't have to write the trailing parentheses.

In the example, I named the function myassumption' differently from the notation myassumption. It is perfectly fine to shadow the original function name with a notation of the same name.

However, what if we need to refer to the old function, which hasn't been applied to unit? We can always rethunk it as follows.

At this point, we still haven't gotten rid of the ltac2: from our proof script. Without ltac2:(...), Rocq will complain as myassumption is not an Ltac1 tactic.

Instead, we can write an Ltac1 wrapper for myassumption.

We can also expose functions/data from Ltac1 to Ltac2, though the wrapper would become more complicated as we would need to convert from an untyped language to a statically typed language. The reader can refer to the reference manual for details. Finally, I want to point out that the myassumption' function is defined in a way to showcase the strength of Ltac2 as an ML-family language where you can make full use of your functional programming knowledge. An alternative (and perhaps easier) way is to use the special lazy_match! goal with form.

By picking the same variable ?a for both the premise (before the |-) and the goal (after the |-), we ensure that the identifier h has a type that matches the goal.

Sequencing Tactics

Similar to Ltac, Ltac2 uses the semicolon operator to sequentially run two tactics. An idiomatic use of semicolon in Ltac involves running one tactic such as destruct followed by another tactic to discharge multiple subgoals at once.

Here, note that destruct b; reflexivity is not just calling destruct b and reflexivity in sequence. After generating multiple subgoals with destruct b, there's the action of focusing on each generated subgoals and calling reflexivity on each individual goal. In Ltac and Ltac2, the semicolon can be viewed as having the same semantics as the semicolon from ML, which does nothing beyond sequentially chaining two computations. Thus, it is the responsibility of the second tactic to decide how it wants to handle multiple goals. The lazy_match! construct, for example, would simply fail if it directly follows a semicolon with multiple subgoals, unlike its Ltac1 counterpart, which focuses on the subgoals on its own. For example, consider the following alternative definition of myassumption'', which performs the pattern matching before the call to Control.refine

For the example above, focusing on the subgoals might appear to be a more sensible default, however, there are cases where we know in advance that no subgoals will be generated, or we are only interested in running the tactic on specific goals. Thus, Ltac2 gives the choice to the user to decide which behavior is desired. We'll how we can make use of the flexibility shortly. For now, to recover the Ltac1 behavior, we wrap our tactic with Control.enter, which focuses on the subgoals generated by the previous tactic.

Note that myassumption'' works without Control.enter, because Control.refine knows how to handle an unfocused proof state.

An alternative to focusing on the subgoals one by one is to focus on one specific subgoal. The following runfirst tactic uses the Control.focus function to focus on the first goal and execute the tactic it takes as an argument.

What Control.focus i j tac does is focusing on the i through jth subgoals before running tac. By instantiating both i and j to 1, we focus only on the very first goal so the p_assumption tactic successfully discharges the first subgoal but leaves the second one alone.

Basic Exception Handling

Thus far, we have been sloppy with the error handling of our programs. In the definition of myassumption', for example, if no matching hypothesis can be found, one of those API calls/matches that interact with the proof state would fail and the user of our tactic is directly exposed to the internal exceptions that are hard to parse. To provide more useful information to the user of the tactics (which might very well be yourself!), Ltac2 provides a very sophisticated system for exception handling and backtracking. Here, we consider only two functions: Control.zero and Control.plus, which roughly correspond to throw and catch from languages like Java. Consider the following get_elem function, which returns the root element of a tree if it's non-empty, but throws a No_value exception with Control.zero otherwise.

Running get_elem Empty would give us the expected exception

Any exceptions thrown by Control.zero is catchable using Control.plus. Here's how we define a function that tries to call get_elem and returns a default argument when an exception is thrown.

For exceptions that are catastrophic and are not meant to be caught, you can use Control.throw.

Bonus: Advanced FFI for handling tacticals

What's sometimes referred to as tacticals in Ltac1 are simply unit valued functions in Ltac2. One can think of tacticals as nothing more than tactics that may take other tactics as inputs. One such example is the runfirst function we have defined earlier. In this section, we discuss how we can use notations on tacticals and export them to Ltac1. The runfirst function takes a thunk as its input. However, the end user is more likely to pass in a notation rather than a thunk (i.e. myassumption rather than myassumption'). To avoid having to wrap the input notation tac within fun () => tac to recover the explicit thunk, we define the notation for runfirst as follows.

Here, tac is the name we assign to the input tactic which we'd like to apply to the first goal. tactic(6) tells Rocq that tac is a placeholder for an Ltac2 expression. By wrapping around tactic(6) in thunk(...), Rocq automatically wraps around the expression in fun _ => ... so the user doesn't have to write it themself.

How do we make runfirst available in Ltac1? The definition below allows us to use runfirst in Ltac1, and we'll explain how it works shortly.

The ltac2:(arg1 ... argn |- ltac2-expr) form defines an Ltac1 function with n inputs. Inside ltac2-expr, arg1 through argn are variables in scope of type Ltac1.t, which represents an (untyped) Ltac1 expression. Ltac1.t is an opaque type from the Ltac1 module (of the Ltac2 package), and we can either cast them to (typed) Ltac2 expressions through Ltac1.to_constr, Ltac1.to_ident or vice versa through Ltac1.from_constr, Ltac1.from_ident. Here, the tac argument is a tactic, so we don't perform any conversion and simply run it through Ltac1.run and pass the whole Ltac1.run tac expression to the runfirst notation so it is applied to the first goal. Now we can use runfirst together with the Ltac1 tactics from the standard library.