\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

From Ltac2 Require Import Ltac2.: [Loading ML file ltac2_plugin.cmxs ... done]

Ltac2¶

The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:

has often unclear semantics
is very non-uniform due to organic growth
lacks expressivity (data structures, combinators, types, ...)
is slow
is error-prone and fragile
has an intricate implementation

Following the need of users who are developing huge projects relying critically on Ltac, we believe that we should offer a proper modern language that features at least the following:

at least informal, predictable semantics
a type system
standard programming facilities (e.g., datatypes)

This new language, called Ltac2, is described in this chapter. It is still experimental but we nonetheless encourage users to start testing it, especially wherever an advanced tactic language is needed. The previous implementation of Ltac, described in the previous chapter, will be referred to as Ltac1.

General design¶

There are various alternatives to Ltac1, such as Mtac or Rtac for instance. While those alternatives can be quite different from Ltac1, we designed Ltac2 to be as close as reasonably possible to Ltac1, while fixing the aforementioned defects.

In particular, Ltac2 is:

a member of the ML family of languages, i.e.
- a call-by-value functional language
- with effects
- together with the Hindley-Milner type system
a language featuring meta-programming facilities for the manipulation of Coq-side terms
a language featuring notation facilities to help write palatable scripts

We describe more in details each point in the remainder of this document.

ML component¶

Overview¶

Ltac2 is a member of the ML family of languages, in the sense that it is an effectful call-by-value functional language, with static typing à la Hindley-Milner (see [DM82]). It is commonly accepted that ML constitutes a sweet spot in PL design, as it is relatively expressive while not being either too lax (unlike dynamic typing) nor too strict (unlike, say, dependent types).

The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it naturally fits in the ML lineage, just as the historical ML was designed as the tactic language for the LCF prover. It can also be seen as a general-purpose language, by simply forgetting about the Coq-specific features.

Sticking to a standard ML type system can be considered somewhat weak for a meta-language designed to manipulate Coq terms. In particular, there is no way to statically guarantee that a Coq term resulting from an Ltac2 computation will be well-typed. This is actually a design choice, motivated by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are provided with an ill-typed term.

The language is naturally effectful as it manipulates the global state of the proof engine. This allows to think of proof-modifying primitives as effects in a straightforward way. Semantically, proof manipulation lives in a monad, which allows to ensure that Ltac2 satisfies the same equations as a generic ML with unspecified effects would do, e.g. function reduction is substitution by a value.

Type Syntax¶

At the level of terms, we simply elaborate on Ltac1 syntax, which is quite close to OCaml. Types follow the simply-typed syntax of OCaml.

The non-terminal lident designates identifiers starting with a lowercase.

ltac2_type       ::=  ( ltac2_type, ... , ltac2_type ) ltac2_typeconst
                      ( ltac2_type * ... * ltac2_type )
                      ltac2_type -> ltac2_type
                      ltac2_typevar
ltac2_typeconst  ::=  ( modpath . )* lident
ltac2_typevar    ::=  'lident
ltac2_typeparams ::=  ( ltac2_typevar, ... , ltac2_typevar )

The set of base types can be extended thanks to the usual ML type declarations such as algebraic datatypes and records.

Built-in types include:

int, machine integers (size not specified, in practice inherited from OCaml)
string, mutable strings
'a array, mutable arrays
exn, exceptions
constr, kernel-side terms
pattern, term patterns
ident, well-formed identifiers

Type declarations¶

One can define new types with the following commands.

Command Ltac2 Type ltac2_typeparams? lident¶: This command defines an abstract type. It has no use for the end user and is dedicated to types representing data coming from the OCaml world.

Variant Ltac2 Type rec? ltac2_typeparams? lident := ltac2_typedef

This command defines a type with a manifest. There are four possible kinds of such definitions: alias, variant, record and open variant types.

ltac2_typedef        ::=  ltac2_type
                          [ ltac2_constructordef | ... | ltac2_constructordef ]
                          { ltac2_fielddef ; ... ; ltac2_fielddef }
                          [ .. ]
ltac2_constructordef ::=  uident [ ( ltac2_type , ... , ltac2_type ) ]
ltac2_fielddef       ::=  [ mutable ] ident : ltac2_type

Aliases are just a name for a given type expression and are transparently unfoldable to it. They cannot be recursive. The non-terminal uident designates identifiers starting with an uppercase.

Variants are sum types defined by constructors and eliminated by pattern-matching. They can be recursive, but the rec flag must be explicitly set. Pattern matching must be exhaustive.

Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the rec flag is set.

Variant Ltac2 Type ltac2_typeparams? ltac2_qualid ::= [ ltac2_constructordef ]: Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example is the standard exn type. Pattern matching on open variants must always include a catch-all clause. They can be extended with this command.

Term Syntax¶

The syntax of the functional fragment is very close to the one of Ltac1, except that it adds a true pattern-matching feature, as well as a few standard constructs from ML.

ltac2_var         ::=  lident
ltac2_qualid      ::=  ( modpath . )* lident
ltac2_constructor ::=  uident
ltac2_term        ::=  ltac2_qualid
                       ltac2_constructor
                       ltac2_term ltac2_term ... ltac2_term
                       fun ltac2_var => ltac2_term
                       let ltac2_var := ltac2_term in ltac2_term
                       let rec ltac2_var := ltac2_term in ltac2_term
                       match ltac2_term with ltac2_branch ... ltac2_branch end
                       int
                       string
                       ltac2_term ; ltac2_term
                       [| ltac2_term ; ... ; ltac2_term |]
                       ( ltac2_term , ... , ltac2_term )
                       { ltac2_field ltac2_field ... ltac2_field }
                       ltac2_term . ( ltac2_qualid )
                       ltac2_term . ( ltac2_qualid ) := ltac2_term
                       [; ltac2_term ; ... ; ltac2_term ]
                       ltac2_term :: ltac2_term
                       ...
ltac2_branch      ::=  ltac2_pattern => ltac2_term
ltac2_pattern     ::=  ltac2_var
                       _
                       ( ltac2_pattern , ... , ltac2_pattern )
                       ltac2_constructor ltac2_pattern ... ltac2_pattern
                       [ ]
                       ltac2_pattern :: ltac2_pattern
ltac2_field       ::=  ltac2_qualid := ltac2_term

In practice, there is some additional syntactic sugar that allows e.g. to bind a variable and match on it at the same time, in the usual ML style.

There is dedicated syntax for list and array literals.

Note

For now, deep pattern matching is not implemented.

Ltac Definitions¶

Command Ltac2 mutable? rec? lident := ltac2_term¶

This command defines a new global Ltac2 value.

For semantic reasons, the body of the Ltac2 definition must be a syntactical value, that is, a function, a constant or a pure constructor recursively applied to values.

If rec is set, the tactic is expanded into a recursive binding.

If mutable is set, the definition can be redefined at a later stage (see below).

Command Ltac2 Set qualid := ltac2_term¶: This command redefines a previous mutable definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like.

Reduction¶

We use the usual ML call-by-value reduction, with an otherwise unspecified evaluation order. This is a design choice making it compatible with OCaml, if ever we implement native compilation. The expected equations are as follows:

(fun x => t) V ≡ t{x := V} (βv)

let x := V in t ≡ t{x := V} (let)

match C V₀ ... Vₙ with ... | C x₀ ... xₙ  => t | ... end ≡ t {xᵢ := Vᵢ} (ι)

(t any term, V values, C constructor)

Note that call-by-value reduction is already a departure from Ltac1 which uses heuristics to decide when to evaluate an expression. For instance, the following expressions do not evaluate the same way in Ltac1.

foo (idtac; let x := 0 in bar)

foo (let x := 0 in bar)

Instead of relying on the idtac idiom, we would now require an explicit thunk to not compute the argument, and foo would have e.g. type (unit -> unit) -> unit.

foo (fun () => let x := 0 in bar)

Typing¶

Typing is strict and follows the Hindley-Milner system. Unlike Ltac1, there are no type casts at runtime, and one has to resort to conversion functions. See notations though to make things more palatable.

In this setting, all the usual argument-free tactics have type unit -> unit, but one can return a value of type t thanks to terms of type unit -> t, or take additional arguments.

Effects¶

Effects in Ltac2 are straightforward, except that instead of using the standard IO monad as the ambient effectful world, Ltac2 is has a tactic monad.

Note that the order of evaluation of application is not specified and is implementation-dependent, as in OCaml.

We recall that the Proofview.tactic monad is essentially a IO monad together with backtracking state representing the proof state.

Intuitively a thunk of type unit -> 'a can do the following:

It can perform non-backtracking IO like printing and setting mutable variables
It can fail in a non-recoverable way
It can use first-class backtracking. One way to think about this is that thunks are isomorphic to this type: (unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a))) i.e. thunks can produce a lazy list of results where each tail is waiting for a continuation exception.
It can access a backtracking proof state, consisting among other things of the current evar assignation and the list of goals under focus.

We now describe more thoroughly the various effects in Ltac2.

Standard IO¶

The Ltac2 language features non-backtracking IO, notably mutable data and printing operations.

Mutable fields of records can be modified using the set syntax. Likewise, built-in types like string and array feature imperative assignment. See modules String and Array respectively.

A few printing primitives are provided in the Message module, allowing to display information to the user.

Fatal errors¶

The Ltac2 language provides non-backtracking exceptions, also known as panics, through the following primitive in module Control:

val throw : exn -> 'a

Unlike backtracking exceptions from the next section, this kind of error is never caught by backtracking primitives, that is, throwing an exception destroys the stack. This is codified by the following equation, where E is an evaluation context:

E[throw e] ≡ throw e

(e value)

There is currently no way to catch such an exception, which is a deliberate design choice. Eventually there might be a way to catch it and destroy all backtrack and return values.

Backtracking¶

In Ltac2, we have the following backtracking primitives, defined in the Control module:

Ltac2 Type 'a result := [ Val ('a) | Err (exn) ].

val zero : exn -> 'a
val plus : (unit -> 'a) -> (exn -> 'a) -> 'a
val case : (unit -> 'a) -> ('a * (exn -> 'a)) result

If one views thunks as lazy lists, then zero is the empty list and plus is list concatenation, while case is pattern-matching.

The backtracking is first-class, i.e. one can write plus (fun () => "x") (fun _ => "y") : string producing a backtracking string.

These operations are expected to satisfy a few equations, most notably that they form a monoid compatible with sequentialization.:

plus t zero ≡ t ()
plus (fun () => zero e) f ≡ f e
plus (plus t f) g ≡ plus t (fun e => plus (f e) g)

case (fun () => zero e) ≡ Err e
case (fun () => plus (fun () => t) f) ≡ Val (t,f)

let x := zero e in u ≡ zero e
let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u)

(t, u, f, g, e values)

Goals¶

A goal is given by the data of its conclusion and hypotheses, i.e. it can be represented as [Γ ⊢ A].

The tactic monad naturally operates over the whole proofview, which may represent several goals, including none. Thus, there is no such thing as the current goal. Goals are naturally ordered, though.

It is natural to do the same in Ltac2, but we must provide a way to get access to a given goal. This is the role of the enter primitive, which applies a tactic to each currently focused goal in turn:

val enter : (unit -> unit) -> unit

It is guaranteed that when evaluating enter f, f is called with exactly one goal under focus. Note that f may be called several times, or never, depending on the number of goals under focus before the call to enter.

Accessing the goal data is then implicit in the Ltac2 primitives, and may panic if the invariants are not respected. The two essential functions for observing goals are given below.:

val hyp : ident -> constr
val goal : unit -> constr

The two above functions panic if there is not exactly one goal under focus. In addition, hyp may also fail if there is no hypothesis with the corresponding name.

Meta-programming¶

Overview¶

One of the major implementation issues of Ltac1 is the fact that it is never clear whether an object refers to the object world or the meta-world. This is an incredible source of slowness, as the interpretation must be aware of bound variables and must use heuristics to decide whether a variable is a proper one or referring to something in the Ltac context.

Likewise, in Ltac1, constr parsing is implicit, so that foo 0 is not foo applied to the Ltac integer expression 0 (Ltac does have a notion of integers, though it is not first-class), but rather the Coq term Datatypes.O.

The implicit parsing is confusing to users and often gives unexpected results. Ltac2 makes these explicit using quoting and unquoting notation, although there are notations to do it in a short and elegant way so as not to be too cumbersome to the user.

Generic Syntax for Quotations¶

In general, quotations can be introduced in terms using the following syntax, where quotentry is some parsing entry.

ltac2_term += ident : ( quotentry )

Built-in quotations¶

The current implementation recognizes the following built-in quotations:

ident, which parses identifiers (type Init.ident).
constr, which parses Coq terms and produces an-evar free term at runtime (type Init.constr).
open_constr, which parses Coq terms and produces a term potentially with holes at runtime (type Init.constr as well).
pattern, which parses Coq patterns and produces a pattern used for term matching (type Init.pattern).
reference, which parses either a qualid or &ident. Qualified names are globalized at internalization into the corresponding global reference, while &id is turned into Std.VarRef id. This produces at runtime a Std.reference. There shall be no white space between the ampersand symbol (&) and the identifier (ident).

The following syntactic sugar is provided for two common cases.

@id is the same as ident:(id)
't is the same as open_constr:(t)

Strict vs. non-strict mode¶

Depending on the context, quotation-producing terms (i.e. constr or open_constr) are not internalized in the same way. There are two possible modes, the strict and the non-strict mode.

In strict mode, all simple identifiers appearing in a term quotation are required to be resolvable statically. That is, they must be the short name of a declaration which is defined globally, excluding section variables and hypotheses. If this doesn't hold, internalization will fail. To work around this error, one has to specifically use the & notation.
In non-strict mode, any simple identifier appearing in a term quotation which is not bound in the global context is turned into a dynamic reference to a hypothesis. That is to say, internalization will succeed, but the evaluation of the term at runtime will fail if there is no such variable in the dynamic context.

Strict mode is enforced by default, such as for all Ltac2 definitions. Non-strict mode is only set when evaluating Ltac2 snippets in interactive proof mode. The rationale is that it is cumbersome to explicitly add & interactively, while it is expected that global tactics enforce more invariants on their code.

Term Antiquotations¶

Syntax¶

One can also insert Ltac2 code into Coq terms, similarly to what is possible in Ltac1.

term += ltac2:( ltac2_term )

Antiquoted terms are expected to have type unit, as they are only evaluated for their side-effects.

Semantics¶

A quoted Coq term is interpreted in two phases, internalization and evaluation.

Internalization is part of the static semantics, that is, it is done at Ltac2 typing time.
Evaluation is part of the dynamic semantics, that is, it is done when a term gets effectively computed by Ltac2.

Note that typing of Coq terms is a dynamic process occurring at Ltac2 evaluation time, and not at Ltac2 typing time.

Static semantics¶

During internalization, Coq variables are resolved and antiquotations are type-checked as Ltac2 terms, effectively producing a glob_constr in Coq implementation terminology. Note that although it went through the type-checking of Ltac2, the resulting term has not been fully computed and is potentially ill-typed as a runtime Coq term.

Example

The following term is valid (with type unit -> constr), but will fail at runtime:

Ltac2 myconstr () := constr:(nat -> 0).

Term antiquotations are type-checked in the enclosing Ltac2 typing context of the corresponding term expression.

Example

The following will type-check, with type constr.

let x := '0 in constr:(1 + ltac2:(exact x))

Beware that the typing environment of antiquotations is not expanded by the Coq binders from the term.

Example

The following Ltac2 expression will not type-check:
`constr:(fun x : nat => ltac2:(exact x))`
`(* Error: Unbound variable 'x' *)`

There is a simple reason for that, which is that the following expression would not make sense in general.

constr:(fun x : nat => ltac2:(clear @x; exact x))

Indeed, a hypothesis can suddenly disappear from the runtime context if some other tactic pulls the rug from under you.

Rather, the tactic writer has to resort to the dynamic goal environment, and must write instead explicitly that she is accessing a hypothesis, typically as follows.

constr:(fun x : nat => ltac2:(exact (hyp @x)))

This pattern is so common that we provide dedicated Ltac2 and Coq term notations for it.

&x as an Ltac2 expression expands to hyp @x.
&x as a Coq constr expression expands to ltac2:(Control.refine (fun () => hyp @x)).

In the special case where Ltac2 antiquotations appear inside a Coq term notation, the notation variables are systematically bound in the body of the tactic expression with type Ltac2.Init.preterm. Such a type represents untyped syntactic Coq expressions, which can by typed in the current context using the Ltac2.Constr.pretype function.

Example

The following notation is essentially the identity.

Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing).: Setting notation at level 0.

Dynamic semantics¶

During evaluation, a quoted term is fully evaluated to a kernel term, and is in particular type-checked in the current environment.

Evaluation of a quoted term goes as follows.

The quoted term is first evaluated by the pretyper.
Antiquotations are then evaluated in a context where there is exactly one goal under focus, with the hypotheses coming from the current environment extended with the bound variables of the term, and the resulting term is fed into the quoted term.

Relative orders of evaluation of antiquotations and quoted term are not specified.

For instance, in the following example, tac will be evaluated in a context with exactly one goal under focus, whose last hypothesis is H : nat. The whole expression will thus evaluate to the term fun H : nat => H.

let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))

Many standard tactics perform type-checking of their argument before going further. It is your duty to ensure that terms are well-typed when calling such tactics. Failure to do so will result in non-recoverable exceptions.

Trivial Term Antiquotations

It is possible to refer to a variable of type constr in the Ltac2 environment through a specific syntax consistent with the antiquotations presented in the notation section.

term += $lident

In a Coq term, writing $x is semantically equivalent to ltac2:(Control.refine (fun () => x)), up to re-typechecking. It allows to insert in a concise way an Ltac2 variable of type constr into a Coq term.

Match over terms¶

Ltac2 features a construction similar to Ltac1 match over terms, although in a less hard-wired way.

ltac2_term     ::=  match! ltac2_term with constrmatching .. constrmatching end
                    lazy_match! ltac2_term with constrmatching .. constrmatching end
                    multi_match! ltac2_term with constrmatching .. constrmatching end
constrmatching ::=  | constrpattern => ltac2_term
constrpattern  ::=  term
                    context  [ term ]
                    context lident [ term ]

This construction is not primitive and is desugared at parsing time into calls to term matching functions from the Pattern module. Internally, it is implemented thanks to a specific scope accepting the constrmatching syntax.

Variables from the constrpattern are statically bound in the body of the branch, to values of type constr for the variables from the term pattern and to a value of type Pattern.context for the variable lident.

Note that unlike Ltac, only lowercase identifiers are valid as Ltac2 bindings, so that there will be a syntax error if one of the bound variables starts with an uppercase character.

The semantics of this construction is otherwise the same as the corresponding one from Ltac1, except that it requires the goal to be focused.

Match over goals¶

Similarly, there is a way to match over goals in an elegant way, which is just a notation desugared at parsing time.

ltac2_term   ::=  match! [ reverse ] goal with goalmatching ... goalmatching end
                  lazy_match! [ reverse ] goal with goalmatching ... goalmatching end
                  multi_match! [ reverse ] goal with goalmatching ... goalmatching end
goalmatching ::=  | [ hypmatching ... hypmatching |- constrpattern ] => ltac2_term
hypmatching  ::=  lident : constrpattern
                  _ : constrpattern

Variables from hypmatching and constrpattern are bound in the body of the branch. Their types are:

constr for pattern variables appearing in a term
Pattern.context for variables binding a context
ident for variables binding a hypothesis name.

The same identifier caveat as in the case of matching over constr applies, and this features has the same semantics as in Ltac1. In particular, a reverse flag can be specified to match hypotheses from the more recently introduced to the least recently introduced one.

Notations¶

Notations are the crux of the usability of Ltac1. We should be able to recover a feeling similar to the old implementation by using and abusing notations.

Scopes¶

A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression.

ltac2_scope ::= stringintlident (ltac2_scope+,)¶

A few scopes contain antiquotation features. For the sake of uniformity, all antiquotations are introduced by the syntax $lident.

The following scopes are built-in.

constr:
- parses c = term and produces constr:(c)
This scope can be parameterized by a list of delimiting keys of interpretation scopes (as described in Local interpretation rules for notations), describing how to interpret the parsed term. For instance, constr(A, B) parses c = term and produces constr:(c%A%B).
ident:
- parses id = ident and produces ident:(id)
- parses $(x = ident) and produces the variable x
list0(ltac2_scope):
- if ltac2_scope parses quotentry, then it parses (quotentry₀, ..., quotentry_n) and produces [quotentry₀; ...; quotentry_n].
list0(ltac2_scope, sep = string_sep):
- if ltac2_scope parses quotentry, then it parses (quotentry₀ string_sep ... string_sep quotentry_n) and produce [quotentry₀; ...; quotentry_n].
list1: same as list0 (with or without separator) but parses quotentry+ instead of quotentry*.
opt(ltac2_scope)
- if ltac2_scope parses quotentry, parses quotentry? and produces either None or Some x where x is the parsed expression.
self:
- parses a Ltac2 expression at the current level and returns it as is.
next:
- parses a Ltac2 expression at the next level and returns it as is.
tactic(n = int):
- parses a Ltac2 expression at the provided level n and returns it as is.
thunk(ltac2_scope):
- parses the same as scope, and if e is the parsed expression, returns fun () => e.
STRING:
- parses the corresponding string as an identifier and returns ().
keyword(s = string):
- parses the string s as a keyword and returns ().
terminal(s = string):
- parses the string s as a keyword, if it is already a keyword, otherwise as an ident. Returns ().
seq(ltac2_scope₁, ..., ltac2_scope₂):
- parses scope₁, ..., scope_n in this order, and produces a tuple made out of the parsed values in the same order. As an optimization, all subscopes of the form STRING are left out of the returned tuple, instead of returning a useless unit value. It is forbidden for the various subscopes to refer to the global entry using self or next.

A few other specific scopes exist to handle Ltac1-like syntax, but their use is discouraged and they are thus not documented.

For now there is no way to declare new scopes from Ltac2 side, but this is planned.

Notations¶

The Ltac2 parser can be extended with syntactic notations.

Command Ltac2 Notation lident (ltac2_scope)string+ : int? := ltac2_term¶: A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded to the provided body where every token from the notation is let-bound to the corresponding generated expression.

Example

Assume we perform:

Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids.

Then the following expression

let y := @X in foo (nat -> nat) x $y

will expand at parsing time to

let y := @X in let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids

Beware that the order of evaluation of multiple let-bindings is not specified, so that you may have to resort to thunking to ensure that side-effects are performed at the right time.

Abbreviations¶

Variant Ltac2 Notation lident := ltac2_term

This command introduces a special kind of notation, called an abbreviation, that is designed so that it does not add any parsing rules. It is similar in spirit to Coq abbreviations, insofar as its main purpose is to give an absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition.

The abbreviation can then be manipulated just as a normal Ltac2 definition, except that it is expanded at internalization time into the given expression. Furthermore, in order to make this kind of construction useful in practice in an effectful language such as Ltac2, any syntactic argument to an abbreviation is thunked on-the-fly during its expansion.

For instance, suppose that we define the following.

Ltac2 Notation foo := fun x => x ().

Then we have the following expansion at internalization time.

foo 0 ↦ (fun x => x ()) (fun _ => 0)

Note that abbreviations are not typechecked at all, and may result in typing errors after expansion.

Evaluation¶

Ltac2 features a toplevel loop that can be used to evaluate expressions.

Command Ltac2 Eval ltac2_term¶: This command evaluates the term in the current proof if there is one, or in the global environment otherwise, and displays the resulting value to the user together with its type. This command is pure in the sense that it does not modify the state of the proof, and in particular all side-effects are discarded.

Debug¶

Flag Ltac2 Backtrace¶: When this flag is set, toplevel failures will be printed with a backtrace.

Compatibility layer with Ltac1¶

Ltac1 from Ltac2¶

Simple API¶

One can call Ltac1 code from Ltac2 by using the ltac1 quotation. It parses a Ltac1 expression, and semantics of this quotation is the evaluation of the corresponding code for its side effects. In particular, it cannot return values, and the quotation has type unit.

ltac2_term ::=  ltac1 : ( ltac_expr )

Ltac1 cannot implicitly access variables from the Ltac2 scope, but this can be done with an explicit annotation on the ltac1 quotation.

ltac2_term ::=  ltac1 : ( ident ... ident |- ltac_expr )

The return type of this expression is a function of the same arity as the number of identifiers, with arguments of type Ltac2.Ltac1.t (see below). This syntax will bind the variables in the quoted Ltac1 code as if they had been bound from Ltac1 itself. Similarly, the arguments applied to the quotation will be passed at runtime to the Ltac1 code.

Low-level API¶

There exists a lower-level FFI into Ltac1 that is not recommended for daily use, which is available in the Ltac2.Ltac1 module. This API allows to directly manipulate dynamically-typed Ltac1 values, either through the function calls, or using the ltac1val quotation. The latter parses the same as ltac1, but has type Ltac2.Ltac1.t instead of unit, and dynamically behaves as an Ltac1 thunk, i.e. ltac1val:(foo) corresponds to the tactic closure that Ltac1 would generate from idtac; foo.

Due to intricate dynamic semantics, understanding when Ltac1 value quotations focus is very hard. This is why some functions return a continuation-passing style value, as it can dispatch dynamically between focused and unfocused behaviour.

The same mechanism for explicit binding of variables as described in the previous section applies.

Ltac2 from Ltac1¶

Same as above by switching Ltac1 by Ltac2 and using the ltac2 quotation instead.

ltac_expr ::=  ltac2 : ( ltac2_term )
               ltac2 : ( ident ... ident |- ltac2_term )

The typing rules are dual, that is, the optional identifiers are bound with type Ltac2.Ltac1.t in the Ltac2 expression, which is expected to have type unit. The value returned by this quotation is an Ltac1 function with the same arity as the number of bound variables.

Note that when no variables are bound, the inner tactic expression is evaluated eagerly, if one wants to use it as an argument to a Ltac1 function, one has to resort to the good old idtac; ltac2:(foo) trick. For instance, the code below will fail immediately and won't print anything.

From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".

Ltac mytac tac := idtac "I am being evaluated"; tac.: mytac is defined
Goal True.: 1 subgoal ============================ True
Proof.
Fail mytac ltac2:(fail).: The command has indeed failed with message: Uncaught Ltac2 exception: Tactic_failure (None)
Fail mytac ltac:(idtac; ltac2:(fail)).: I am being evaluated The command has indeed failed with message: Uncaught Ltac2 exception: Tactic_failure (None)

In any case, the value returned by the fully applied quotation is an unspecified dummy Ltac1 closure and should not be further used.

Transition from Ltac1¶

Owing to the use of a lot of notations, the transition should not be too difficult. In particular, it should be possible to do it incrementally. That said, we do not guarantee you it is going to be a blissful walk either. Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq will help you.

We list the major changes and the transition strategies hereafter.

Syntax changes¶

Due to conflicts, a few syntactic rules have changed.

The dispatch tactical tac; [foo|bar] is now written tac > [foo|bar].
Levels of a few operators have been revised. Some tacticals now parse as if they were normal functions. Parentheses are now required around complex arguments, such as abstractions. The tacticals affected are: try, repeat, do, once, progress, time, abstract.
idtac is no more. Either use () if you expect nothing to happen, (fun () => ()) if you want a thunk (see next section), or use printing primitives from the Message module if you want to display something.

Tactic delay¶

Tactics are not magically delayed anymore, neither as functions nor as arguments. It is your responsibility to thunk them beforehand and apply them at the call site.

A typical example of a delayed function:

Ltac foo := blah.

becomes

Ltac2 foo () := blah.

All subsequent calls to foo must be applied to perform the same effect as before.

Likewise, for arguments:

Ltac bar tac := tac; tac; tac.

becomes

Ltac2 bar tac := tac (); tac (); tac ().

We recommend the use of syntactic notations to ease the transition. For instance, the first example can alternatively be written as:

Ltac2 foo0 () := blah. Ltac2 Notation foo := foo0 ().

This allows to keep the subsequent calls to the tactic as-is, as the expression foo will be implicitly expanded everywhere into foo0 (). Such a trick also works for arguments, as arguments of syntactic notations are implicitly thunked. The second example could thus be written as follows.

Ltac2 bar0 tac := tac (); tac (); tac (). Ltac2 Notation bar := bar0.

Variable binding¶

Ltac1 relies on complex dynamic trickery to be able to tell apart bound variables from terms, hypotheses, etc. There is no such thing in Ltac2, as variables are recognized statically and other constructions do not live in the same syntactic world. Due to the abuse of quotations, it can sometimes be complicated to know what a mere identifier represents in a tactic expression. We recommend tracking the context and letting the compiler print typing errors to understand what is going on.

We list below the typical changes one has to perform depending on the static errors produced by the typechecker.

In Ltac expressions¶

Error Unbound valueconstructor X¶

if X is meant to be a term from the current stactic environment, replace the problematic use by 'X.
if X is meant to be a hypothesis from the goal context, replace the problematic use by &X.

In quotations¶

Error The reference X was not found in the current environment¶

if X is meant to be a tactic expression bound by a Ltac2 let or function, replace the problematic use by $X.
if X is meant to be a hypothesis from the goal context, replace the problematic use by &X.

Exception catching¶

Ltac2 features a proper exception-catching mechanism. For this reason, the Ltac1 mechanism relying on fail taking integers, and tacticals decreasing it, has been removed. Now exceptions are preserved by all tacticals, and it is your duty to catch them and re-raise them as needed.