# Code Generation via Meta-programming in Dependently Typed Proof Assistants

Mathis Bouverot-Dupuis, Yannick Forster

► To cite this version:

Mathis Bouverot-Dupuis, Yannick Forster. Code Generation via Meta-programming in Dependently
Typed Proof Assistants. 2025. hal-05024207v3

HAL Id: hal-05024207

https://hal.science/hal-05024207v3

Preprint submitted on 13 May 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Code Generation via Meta-programming
in Dependently Typed Proof Assistants

(Experience Report)

MATHIS BOUVEROT-DUPUIS YANNICK FORSTER

Dependently typed proof assistants offer powerful meta-programming features, which users can take advantage of to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running example: deriving instances for the **Functor** type class. This example is fairly simple, but sufficiently realistic to highlight recurring difficulties with meta-programming: conceptual limitations of frameworks such as term representation – and in particular binder representation –, meta-language expressiveness, and verifiability as well as current limitations such as API completeness, learning curve, and prover state management, which could in principle be remedied. We conclude with insights regarding features an ideal meta-programming framework should provide.

## 1 Introduction

All proof assistants support user-extensible tactics and code generation through different meta-programming frameworks. Meta-programs are programs which produce or manipulate other programs as data. They can in particular be used to generate boilerplate code, i.e. code that can be mechanically derived from definitions, thereby increasing the productivity of proof assistant users. Common examples are induction principles [41, 69], equality deciders [31, 69], finiteness proofs [20], countability proofs [20], or substitution functions for syntax [67]. Naturally, the default meta-programming language of a proof assistant is its implementation language, and several proof assistants even come with multiple independent meta-programming frameworks. However, we can observe that meta-programming is not wide-spread on the example of boilerplate generation tools which often fall into one of the following: Either proof assistants come with built-in boilerplate generation support (such as induction principles or type class instances) which is widely used. Or tools for generating boilerplate are developed, but not adopted by the community [9, 31, 69]. Lastly, many papers remark that automatic boilerplate generation would be feasible and interesting, but do not carry it out [24, 28, 73, 75]. Furthermore, subcommunities often seem to be split into silos regarding frameworks and we are not aware of scientific comparative work between different frameworks and proof assistants. The notable exception is Dubois de Prisque's PhD thesis [22], using several meta-programming frameworks in Rocq, but not coming with one central example implemented in different frameworks and focusing solely on Rocq.

An additional barrier for adoption is that most frameworks are organically grown and documentation is not accessible to non-experts: pros and cons are often implicitly known by developers but not readily accessible. In fact the situation is so chaotic that, at times, in order to generate boilerplate code authors create ad-hoc meta-programming facilities from scratch [32, 44, 67, 68] instead of taking advantage of existing meta-programming facilities.

On the other hand, the vast choice of meta-programming frameworks also hints that we are at the point where enough evidence is available to evaluate the state of the art and suggest future developments. In this paper, we focus on three major dependently typed proof assistants based on the Calculus of Inductive Constructions (CIC) [16, 56]: Rocq [70], Agda [53, 54], and Lean 4 [48]. We survey their respective meta-programming frameworks: for Rocq we cover OCaml plugins (§ 3), MetaRocq [2, 64] (§ 4), Ltac2 [60] (§ 5), Elpi [25, 69] (§ 6), and furthermore Lean 4's meta-programming API (§ 7)<fnref n="1" /> and Agda's Reflection API [74] (§ 8). In the appendix (§ B), we furthermore explain a novel approach to use Rocq's OCaml API with locally nameless syntax. This means that

<footnote n="1">¹We are not aware of a dedicated publication about meta-programming in Lean 4, but there exists a collaborative book draft [57]. Lean 3's meta-programming was surveyed by Ebner et al. [26].</footnote>
we focus on systems which are designed as proof assistants with consistent meta-theory, rather than dependently typed programming languages, and focus on those with conceptual similarity and shared foundations. In particular, we do not consider Idris [6, 7], HOL-based systems such as Isabelle, HOL4, or HOL light, or LF-based systems such as Beluga, but discuss them in § 9.

We evaluate the different meta-programming frameworks on a simple yet realistic example: automatically deriving instances of the **Functor** type class for a simple family of inductives, covering, amongst many other types, options, lists, and trees. For Rocq we e.g. want to generate the following for the list type:

Fixpoint fmap (A B : Type) (f : A -> B) (l : list A) : list B := match l with [] => [] | x :: l => f x :: map f l end.

Many tasks involving automatic boilerplate generation follow the same model as this example: take an inductive as input and produce a term as output. We choose this example because it is simple enough for code to be readable and explainable, yet complex enough to expose issues that arise in more realistic meta-programs, and makes use of common meta-programming features such as type-class search or the ability to extend the global environment.

Our evaluation criteria are split into *conceptual* criteria, which are inherent to the approach used by the meta-programming framework, and *current* criteria, which are incidental characteristics of the framework and could be changed in the future. *Conceptual* criteria include the expressiveness of the meta-language (especially access to printing, exceptions, non-termination, and mutable state), term representation used (especially of binders), and verifiability of meta-programs. Since this is an experience report, we also comment on learning curve: the author(s) of examples in this paper had no previous contact to most meta-programming frameworks, excluding Ltac2 and OCaml Rocq plugins. *Current* criteria include API completeness, management of the prover state (such as the global or environment, or unification state), and the presence of term quotation.

We do not consider performance issues in this paper: most inductive to term meta-programs run in an order of magnitude of seconds, and only have to be run once per inductive definition. In practice, developments rarely contain many inductive type definitions or very large inductive type definitions. Thus, we deem performance less critical than the aspects discussed here. Performance issues become more critical when implementing proof automation (such as tactics) or more complex meta-programs such as unification algorithms or type checkers (for instance Rocq's verified kernel in MetaRocq [65] or Lean's kernel in Lean4Lean [8]), which are out of the scope of this paper. We also do not consider actual verification of meta-programs, as it is not achievable in most of the frameworks we consider as of today, but still comment on verifiability when relevant.

**Contributions.** (1) A comprehensive survey of the six meta-programming frameworks in Rocq, Agda, and Lean. (2) An overview of their pros and cons. (3) A simple but realistic tool with different implementations for automatically deriving instances of the **Functor** type class covering, amongst other types, options, lists, and trees for Rocq, Agda, and Lean. (4) Suggestions for the development of future frameworks. Our paper can also be seen as a first step towards a suggested Rosetta Stone project for meta-programming in Rocq project, which is stalled [link anonymised].

## 2 Preliminaries

Meta-programs crucially leverage the features provided by the *elaborator* of the proof assistant, such as unification, type checking or inference, and typeclass resolution. They also need to manipulate the *state* of a proof assistant, consisting in the *global environment* (stores global definitions and inductives), *local environment* (stores local variables, and in the case of Rocq also section variables and hypotheses), and *evar-map* (stores information pertaining to unification variables). This manipulation can be implicit or by explicitly threading the three components through programs.

How binders are represented is a key question for meta-programs. De Bruijn indices and locally nameless were both introduced by de Bruijn in his seminal paper [21] and are used in the
implementations of Rocq, Agda, and Lean and consequently in the associated meta-programming frameworks. The notable exception is Coq-Elpi which uses higher-order abstract syntax (HOAS). We give examples for the representation in the respective sections.

Our example is the generation of instances of the following functor type class. In Rocq:

Class Contractor (F : Type -> Type) : Type ::= { fmap {A B} : (A -> B) -> F A -> F B }.

We have already shown the instance for list in the introduction. Our implementation also handles more complex types, for instance using nesting:

Inductive tree (A : Type) : Type ::= Fixpoint fmap (A B : Type) (f : A -> B) (t : tree A) : tree B := | Leaf : tree A match t with Leaf => Leaf | Node : A -> list (tree A) -> tree A. | Node x ts => Node (f x) (List.map (fmap f) ts) end.

In general, inductives can be non-recursive (like *bool*, *option*), recursive (*nat*, *list*), have parameters (*option*, *list*), or have indices (*vector*). For our tool, we support as input inductive types with a single (uniform) parameter and no indices. We do not support mutual recursion for simplicity, but could. For simplicity, the code samples shown in the paper do not handle recursive inductives: the complete implementations do handle the general case. The Lean implementation does not support recursive inductives, see § 7. We use OCaml's syntax for right-associative function application, i.e. `f @ @ g x @ @ h y` for `f (g x (h y))`, even though MetaRocq and Agda use Haskell's `f $ g x $ hy`.

## 3 Rocq Plugin - de Bruijn

The Rocq kernel is implemented in OCaml, and writing an OCaml plugin is historically the most common way of writing Rocq meta-programs [19, 23, 55, 61]. OCaml plugins directly manipulate the kernel representation of terms, which uses de Bruijn indices for variables. For instance the term `λf.λx.λy.f x y` is represented as `λ.λ.λ.2 1 0`.

Figure 1 shows the OCaml code to build the lambda abstractions and case expression of `fmap` for an arbitrary inductive `ind`. Most functions in the API take as input the (global and local) environment `env` and the `evar-map` `sigma` and return the updated `evar-map`. Even if we do not care about the `evar-map`, it has to be threaded. For instance `lambda env sigma "x" T k` builds a lambda abstraction with a binder named `x` and of type `T`; the continuation `k` takes in the new environment (updated with a binding for `x`) and returns the body of the lambda abstraction.

<table><thead><tr><th></th><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><td>Pros</td><td>P1 - Plugins have access to full implementation.</td><td>P2 - OCaml is a mature programming language.</td></tr><tr><td>Cons</td><td>C1 - De Bruijn index arithmetic is difficult.<br>C2 - No term quotations.</td><td>C3 - OCaml plugins are hard to set up.<br>C4 - Cluttered meta-programming API.<br>C5 - Explicit state management.</td></tr></tbody></table>

**P1 - Conceptual.** The main advantage of OCaml plugins is that they allow users to directly access Rocq's implementation (term manipulation functions, unification, and the tactic engine), whereas other meta-languages either duplicate this code or have to manually provide bindings to each useful function. Having direct access guarantees that the meta-programming API is complete: users have access to every customisable aspect of the proof assistant, including the parser and all type-checking and unification flags. Secondly, it ensures the API stays up to date with the latest Rocq features. When new features such as universe polymorphism are added to Rocq, one typically has to wait some time before the various Rocq meta-languages add support for them.

**P2 - Current.** OCaml is a general purpose programming language used in many applications besides Rocq meta-programming and thus enjoys a large ecosystem of packages, as well as robust and well-maintained tools (such as a language server, a code formatter, an optimising compiler, a package manager, etc), which is not the case for Rocq's other meta-languages.

**C1 - Conceptual.** In OCaml plugins, Rocq variables are represented using de Bruijn indices, which require a significant amount of experience to manipulate correctly. Writing explicit indices
and lifting terms was a major source of programming errors when getting started. In the definition of `build_fmap` (figure 1), we had to write de Bruijn indices explicitly and make sure to lift indices when necessary, e.g. in `buildbranch` (figure 1):

```hml
let sigma, arg' = build_arg env sigma (( liftInputs (i + 1) inp) (mkRel 1))
( Vars.lift 1 @@ EConstr.of_constr @@ get_type decl)
in loop env sigma (i + 1) ( lift (ca.cs... - i - 1) arg' :: acc) decls
```

**C2 - Conceptual.** Most meta-languages provide a high-level method to build terms using term quotations, which is a lightweight mechanism allowing one to turn user syntax terms into the internal representation used by the meta-language. Plugins do not provide any quotation mechanism: building terms is thus rather verbose and tedious. In the absence of term quotations, one has to provide fully qualified kernel names, pass all implicit arguments to functions, provide type-class instances by hand (or manually create unification variables to stand in for unknown instances), and explicitly instantiate all universe polymorphic constants and inductives.

**C3 - Current.** Integrating a plugin into a build system currently requires a lot of boilerplate, even when using the modern dune build system for Rocq: one has to include plugin-specific dune stanzas as well as several other build-specific files. This is in stark contrast with most other meta-languages.

**C4 - Current.** The plugin API is hard to use for non-experts. It provides code to accomplish common meta-programming tasks but finding the right function often requires reading their implementation (i.e. reading \*.ml files in addition to \*.mli files), or asking the Rocq developers for help. Fortunately the developers are easy to reach (via online forums) and eager to provide help.

**C5 - Current.** Finally, plugins provide no good solution for managing the prover state: the environment and evar-map are explicitly passed as arguments to and returned from most functions. The resulting code is verbose and obfuscates the core logic of the program. Threading the prover state explicitly is certainly not ideal, however it is not clear yet what is the best approach.

## 4 MetaRocq

The MetaRocq project [2, 64] provides tools for meta-programming for Rocq, in Rocq, and in another subproject has a full specification of Rocq's type theory in Rocq. In principle, these could be developed into a certified meta-programming framework for Rocq, in Rocq. Most importantly for this paper, MetaRocq comes with a monad `TemplateMonad` with bindings to Rocq's elaborator, where such monadic programs can be run using the `MetaCoq Run` command. The barebone meta-programming framework built on top has been used in [1, 3, 4, 18, 22, 29, 30, 41, 65].

Fig. 3 shows the Rocq code for the MetaRocq plugin. The data-structures and low-level APIs exposed by MetaRocq are very similar to those used in OCaml: the MetaRocq plugin is thus very similar to the OCaml plugin using de Bruijn indices (§ 3). The function `mk lambda` corresponds to the OCaml function `lambda`, and the representation of terms is almost identical. The code manages only a local (de Bruijn) context `ctx`: MetaRocq does not have a notion of an evar-map.

<table><thead><tr><th></th><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><th scope="row">Pros</th><td>P1 - Users already know Rocq.<br>P2 - Meta-programs can be formally verified.</td><td>P3 - Significant parts are formally verified.</td></tr><tr><th scope="row">Cons</th><td>C1 - De Bruijn index arithmetic is difficult.<br>C2 - Lack of abstractions to handle effects.</td><td>C3 - Explicit state management.<br>C4 - Missing high level meta-programming features.<br>C5 - Performance issues in some cases.</td></tr></tbody></table>

**P1 - Conceptual.** An appealing aspect of MetaRocq, is the ability to perform meta-programming directly using the host language Rocq, flattening the learning curve significantly.
**P2 - Conceptual.** In addition to useful meta-programming features, MetaRocq includes an extensive formalisation of Rocq's meta-theory, with proofs of key results of theoretical interest. It is possible to formally verify meta-programs by leveraging Rocq's theorem proving features in combination with the numerous lemmas already present in MetaRocq. Note however that verifying meta-programs which use high-level meta-programming features (such as unification or type-inference) through the `TemplateMonad` is still an active research area.

**P3 - Current.** Most of the functions provided by MetaRocq are formally verified with respect to Rocq's meta-theory, including reduction and type-checking, providing strong correctness guarantees: this is used to build a certified extraction procedure by Forster et al. [29]. Formal verification is very appealing considering the complexity inherent to implementing proof assistants; note however that verified implementations are often quite basic and do not benefit from the same optimisations and clever heuristics (for instance reduction using explicit substitutions or abstract machines) as the equivalent code in Rocq's OCaml implementation.

**C1 - Conceptual.** MetaRocq implements binders using de Bruijn, which has the same drawbacks we explained in § 3. On the upside many term manipulation functions are formally verified, but we found bugs related to de Bruijn indices in unverified MetaRocq functions during this project.

**C2 - Conceptual.** Rocq does not provide abstractions to handle effects such as printing, exceptions or non-termination, so writing non-trivial programs quickly becomes tedious. Herbelin's reduction-effects plugin [34] allows to print values, but is currently only suitable for debugging. Moreover, writing partial or possibly non-terminating programs is impractical in Rocq. Common solutions include disabling the guard-checker or using step-indexing. MetaRocq uses monads to somewhat mitigate these issues, but in our experience this was still a major point of friction.

MetaRocq relies crucially on *monads* to handle effects, most notably the `TemplateMonad`. There does not seem to be a consensus on how to implement monads in Rocq: a promising attempt is the Monae library [62] which formalises monads in the style of Rocq's Mathematical-Components library using the Hierarchy Builder tool [14]. MetaRocq rolls its own monad library, following a simpler design called *semi-bundled* type-classes, which is a standard way of implementing monadic effects and is used successfully in languages such as Haskell and in Lean's mathematical library [46]. However, contrary to Haskell and Lean, monadic programs in Rocq are very hard to debug: programming errors often lead to implicit argument resolution failing with incomprehensible error messages.

**C3 - Current.** State management in MetaRocq is explicit: the global environment and local context have to be threaded manually, and this issue will only worsen as more state (such as the `evar-map`) is added. Rocq being a pure language, the obvious solution is to use monads to hide the state, but as discussed above there is currently no satisfactory implementation of monads in Rocq.

**C4 - Current.** MetaRocq provides no access to e.g. unification, type inference, type-class resolution. Indeed, MetaRocq only re-implements Rocq's kernel, and bindings to the upper levels of Rocq's implementation are incomplete: many functions are missing entirely or lack vital flags and inputs. For instance typeclass resolution does not take a local environment as input: thus only global instances are considered, and there is no way to provide local instances. Another example is that it is impossible to define a new universe polymorphic constant (only monomorphic constants are handled), although it is possible to define both monomorphic and universe polymorphic inductives.

**C5 - Current.** Performance of impure MetaRocq programs (i.e. programs in the `TemplateMonad`) can be quite poor: we noticed slowdowns of up to two orders of magnitude on small programs, and conjecture that this extends to larger programs. The best practice is to write meta-program without using the `TemplateMonad`, effectively pushing effects to the edges of the program. Designing programs this way is generally accepted as good practice in pure programming languages; however in this case, effects include pervasive operations such as calling into Rocq's high level meta-programming API (for instance to perform unification or type-class resolution) or quoting terms, making overall
performance low. Another issue is that accessing the declaration corresponding to a definition or inductive might require unquoting, reduction through the `TemplateMonad`, and quoting again.

## 5 Ltac2

Until now we have built `fmap` by assembling small terms into larger ones, directly manipulating the representation of terms. An alternate approach, following the Curry-Howard correspondence, is to use tactics to produce a proof term `fmap :forall A B, (A -> B) -> F A -> F B`. For instance the elaborator of Idris 1 [6] uses tacticsto transform concrete syntax into abstract syntax. For example, to use Ltac2 tactics to define `fmap` for option one writes:

```
Definition fmap :forall A B, (A -> B) -> option A -> option B.
    intros A B f x. destruct x.
    { (* Some *) intros y. constructor 0. exact (f y). } { (* None *) constructor 1. } Defined.
```

Here low-level details such as binder representation are taken care of by dedicated tactics such as `intros` and there is no need anymore to handle the internal representation of terms. This observation remains true when generalising to arbitrary inductives: figure 4 shows the code for the Ltac2 plugin (the at symbol, as in `@x`, is used to construct Ltac2 identifiers). A quirk of the Ltac2 API is that introducing variables with fresh identifiers is slightly awkward: while most introduction tactics have the ability to generate fresh identifiers, they do not return the generated identifiers to the caller, and it is thus impossible to refer to the introduced identifiers in subsequent code. To circumvent this we wrote a custom introduction tactic `n_intro` which handles fresh name generation.

Another point of friction is that many functions require multiple flags to control their behavior, and default flags were more often than not incompatible with our needs. Explicit flags as in figure 4 are complicated due to missing documentation. E.g. `Std.case false (Control.hyp @x, NoBindings)` simply performs case analysis on the local variable `x`, and `constructor_n false i NoBindings` applies the i-th constructor when the goal is of inductive type. Chaining tactics is done using `Control.dispatch [t_1 ; ... ; t_n]`, which applies tactic `t_i` to the i-th open goal.

<table><thead><tr><th></th><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><td><strong>Pros</strong></td><td>P1 - Tactics provide a nice API to build terms.</td><td>P2 - Implicit state management.</td></tr><tr><td><strong>Cons</strong></td><td>C1 - Tactics are hard to reason about.<br>C2 - Implicit backtracking.</td><td>C3 - Ltac2 is missing many basic language features.<br>C4 - Weak meta-programming API.</td></tr></tbody></table>

**P1 - Conceptual.** Using tactics, the core logic to build `fmap` for arbitrary inductives is both concise and easy to understand: based on our experience, tactics provide a nice interface not only for constructing proofs, but also for constructing terms. In fact, we argue tactic programming combines aspects of locally nameless and top-down term construction. When using tactics, free variables are represented using names, in the same way as local hypotheses. The tactic `intro x` removes the outermost binder in the goal and replaces all occurrences of `de Bruijn index 0` with named variable `x`; conversely, the tactic `revert x` replaces all occurrences of named variable `x` in the goal with `de Bruijn index 0` and adds a binder. Tactics generally maintain the same invariant as locally nameless: free variables are represented using names, while bound variables use `de Bruijn` indices. Most importantly, users do not have to care about such considerations at all: Ltac2 does provide ways to access the underlying representation of terms, but at no point is this needed in our code. Additionally, in the same way that tactic-based backward reasoning provides a pleasant alternative to forward reasoning, tactics allow one to build terms top-down instead of the usual bottom-up approach. We found it to be well suited for building `fmap` in our code, and conjecture this is due to top-down term construction being closer to how one describes terms informally.
**P2 - Current.** Ltac2 does not explicitly expose the prover state. Information about global constants, local variables and unification variables can be queried when needed. However interacting with the prover state was rather difficult in our opinion and could be improved, as discussed in C5.

**C1 - Conceptual.** Reasoning about tactic programs is inherently more difficult than reasoning about equivalent direct style programs. We are not aware of existing work on reasoning about tactics. Since tactics can be seen as monadic programs, using a tailored program logic is conceivable.

**C2 - Conceptual.** A unique characteristic of tactics is *implicit backtracking*, as described by Spiewack [66]. Tactics produce a lazy stream of successes, optionally followed by a single failure. For instance the constructor tactic tries to apply the first constructor of an inductive; if the following tactic fails, the proof engine backtracks up to constructor, which is asked for a second success, until all constructors have been tried. Such lightweight backtracking is useful for proof construction, but not for us, and we even argue that implicit backtracking could be harmful in the context of generating terms with computational content, as it decreases predictability.

**C3 - Current.** Ltac2 is missing many convenience features at the language level, such as syntactic sugar or a proper printing mechanism. Its standard library is barebone, and documentation and learning resources are scarce. The language is however under active development.

**C4 - Current.** Ltac2 is far from a full meta-programming language: many conceptually simple tasks are difficult or outright impossible. Extending the global environment is impossible, declaring new unification variables or local variables is difficult, and building terms in a traditional way by assembling subterms into larger terms is impractical. In general the low-level API to manipulate the internal representation of terms lacks many features, and most high-level facilities (including unification, term quotations, and most of the OCaml API re-exported by Ltac2) do not support terms containing free de Bruijn indices. Moreover, switching between tactic mode and direct term manipulation is hard to perform: in our case it was necessary (for technical reasons related to Rocq's guard checker) to normalise the term built by `build_fmap`, which was awkward to implement.

## 6 Elpi

Elpi is a logic programming language based on λProlog [50] which can be used as a meta-programming language for Rocq [12, 17, 22, 31, 45, 63, 69]. Elpi is notably used to implement Hierarchy Builder [14] -a tool used to structure Rocq's Mathematical Components library [13] -, a type-checker and elaborator for the Calculus of Inductive Constructions [33], and of a type-class resolution algorithm for Rocq [27].

Figure 5 shows the Elpi code to build the `fmap` function for an arbitrary inductive I. An Elpi program is composed of predicates, which relate input(s) to output(s): `pred build-fmap i:inductive`, `o:term` declares the predicate `build-fmap` with one input (the inductive we are mapping over) and one output (the `fmap` n). Predicates are then endowed with a set of rules: for instance `build-fmap I T :- p` adds a rule with conclusion `build-fmap I T` and premise p. Elpi code makes heavy use of term quotations: `{ ... }` quotes Rocq code into Elpi, and `lpe(...)` quotes Elpi code into Rocq.

Back-ticks, as in `x'`, provide syntactic sugar to build identifiers for local variables. These variables are tracked in a local context: `@pi-decl 'x' T k` adds a variable with name `x` and type `T` to the local context, and runs continuation `k` in this extended context. In the code above, continuations are in fact simply lambda abstractions `λx.t`, written `x\t` in Elpi.

<table><thead><tr><th></th><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><th>Pros</th><td>P1 - Higher-order abstract syntax.</td><td>P2 - Powerful quoting and unquoting mechanism.</td></tr><tr><th>Cons</th><td>C1 - Paradigm shift (logic programming).</td><td>C2 - Many trivial bugs are caught only at runtime.<br>C3 - Limited representations for structured data.</td></tr></tbody></table>
**P1 - Conceptual.** A key feature of Elpi is the binder representation it uses for terms, called higher order abstract syntax (HOAS) and due to Pfenning and Elliott [58]: Rocq functions and products are represented using Elpi lambda abstractions. For instance the Rocq function `fun x : nat => x` is represented in Elpi as `fun `x` (global (indt nat?)) c\c`, where `fun` is a constructor with three arguments (binder name, binder type and body). Meta-programming using HOAS does not require dealing with index arithmetic or lifting terms, and the Elpi type-checker helps catch many easy mistakes when building terms (for instance making it impossible to construct ill-scoped terms).

**P2 - Current.** Elpi has support for quoting Rocq expressions into their Elpi representation and vice-versa, most importantly supporting open terms. This is not the case in most meta-languages which support quoting (Lean being a notable exception). Moreover, Rocq unification variables correspond almost one to one with Elpi unification variables, allowing meta-programs to trigger Rocq's unification simply by using Elpi's built-in unification.

**C1 - Conceptual.** Elpi is a logic programming language, which is a paradigm shift compared to dependently-typed proof assistants. As a consequence, it comes with a steep learning curve. In our experience, switching to a new programming paradigm is mainly an issue for beginners: experienced users can be very productive using Elpi.

A strong argument in favor of logic programming is that it enables HOAS. In fact a higher-order binder representation in a proof assistant requires switching off the strict positivity condition on inductives. We did not investigate parametric higher-order abstract syntax [11]. Even in general purpose languages such as OCaml in which it is possible to define a HOAS term grammar, basic term manipulations (such as counting the number of variables in a term) are impossible.

**C2 - Current.** We experienced friction points due to the Elpi type-checker not catching enough errors. A common example is that misspelling the name of a predicate (i.e. of a global constant) does neither lead to a type-checking nor to a runtime error but to unexpected runtime behavior: the predicate is treated as unsatisfiable, since indeed there are no program clauses associated to it. At the time of writing, an improved version of the Elpi type-checker is being developed.

**C3 - Current.** On the language level, Elpi provides limited options for representing structured data. There are no ML-style records; in fact it is common for Elpi functions to have more than half a dozen input and output parameters. Sum types are available, but only open sums: one can add more constructors at any point in the program. This enables clever programming patterns, but prevents the type-checker from checking that programs handle all constructors.

# 7 Lean

The entire elaborator of Lean 4 (which includes parsing, unification, type-inference and type-class resolution) is implemented in Lean itself [49] – self-hosting the kernel is subject to active research, see the Lean4Lean project by Carneiro [8] – and meta-programs are simply Lean programs which have access to the Lean implementation. Lean's meta-programming features are used in the Lean mathematical library [46] as well as in many other projects [5, 42, 43, 51], and most of the implementation of Lean's elaborator can be considered meta-programming.

Figure 6 shows the code for the Lean version. In Lean, binders are represented using the locally-nameless style: bound variables use de Bruijn indices, and free variables are named. The function `withLocalDecl` extends the local context with a new named variable, and `mkLambdaFVars` replaces free (named) variables with bound (de Bruijn) variables in a term. Back-ticks, as in ``\A```, provide syntax sugar to construct names of global constants or local variables. Notice the return type `MetaM Expr` of `build_fmap` and the use of `do` notation: the code shown in figure 6 runs in the `MetaM` monad, which provides implicit access to the global environment, local context, and meta-variable context.
<table><thead><tr><th></th><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><td><strong>Pros</strong></td><td>P1 - Users already know Lean.<br>P2 - Access to complete Lean implementation.<br>P3 - Locally-nameless API is nice to build terms.</td><td>P4 - Implicit state management using monads.</td></tr><tr><td><strong>Cons</strong></td><td>C1 - No first-class fixpoints or pattern matching.</td><td></td></tr></tbody></table>

*P1 - Conceptual.* Meta-programming is done directly in Lean: this has the benefit of relieving the user from learning a new DSL, but goes much further as explained in the next paragraph.

*P2 - Conceptual.* Meta-programs can access the entire API of the Lean implementation without the need for developers to manually expose bindings to every useful API function. This also avoids duplicating data-structures for syntax the local context, global environment, etc. and to seamlessly access other useful parts of the implementation which would typically not be part of a meta-programming language, e.g. related to the *concrete* syntax of terms such as the parser. We also note that support for instrumenting the parser to implement various notations, macros, and embedded CSL is particularly good. In fact Lean macros are so powerful that they allow some form of basic meta-programming. We refer the reader to the work by Ullrich and de Moura [71] for an overview of Lean's macro system.

*P3 - Conceptual.* Local variables are internally represented as locally nameless and the user has to maintain a local context (accessible via a reader monad) which performs the necessary bookkeeping for free variables (type information, name, etc). We found this to be pleasant to use.

*P4 - Current.* Lean is a pure language, and modifying prover state is done using a small hierarchy of monads: this provides the lightweight programming experience of implicit state, while keeping some level of control over which effects a meta-program can perform. A meta-program in *CoreM* can access the global environment but may not assign meta-variables, while a more powerful meta-program in *MetaM* has access to the global environment, local context, and *metavariable* context. The good monadic programming experience is partly due to Lean's excellent support for monadic programming at the language level, as described by Ullrich and de Moura [72].

*C1 - Conceptual.* Lean's abstract term syntax has no first-class fixpoints or case expressions (as for instance in Rocq): instead, *concrete syntax* fixpoints and case expressions are compiled to primitive recursors, which are represented as global constants with special reduction rules.

Benefits include having a simpler meta theory and no need for a guard checker in the kernel. However, we perceived this a severe limitation for meta-programming.

For instance a case expression on an *option* is represented as an application of the `--option.casesOn` primitive recursor. The fixpoint and pattern matching compiler cannot be used because it only accepts *concrete syntax* as input. Meta-programs can thus only build recursive functions using *primitive recursors*. In practice recursors for nested inductives quickly become unwieldy. Generating concrete syntax (instead of abstract syntax) solves this particular issue with fixpoints and case expressions, but concrete syntax is very difficult to manipulate, and most functions in the Lean meta-programming API (such as unification or type inference) do not work with concrete syntax. Due to these difficulties, our Lean implementation does not support recursive inductives such as lists. The problems could be mitigated by improving the API to have more support for the generation of recursive functions also with unification and type inference.

## 8 Agda

Meta-programming in Agda is done directly in Agda, using the *Reflection* API [74]: meta-programs are written in Agda, and interact with the elaborator and kernel via the type-checking monad $\tau_c$.

Figure 7 shows the code for the Agda plugin.
<table><thead><tr><th></th><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><td><strong>Pros</strong></td><td>P1 - Users already know Agda.</td><td>P2 - Implicit state management using monads.</td></tr><tr><td><strong>Cons</strong></td><td>C1 - De Bruijn index arithmetic is difficult.<br>C2 - Difficult to manipulate term representation.</td><td>C3 - Type-class search is hard to control.<br>C4 - Performance issues in some cases.<br>C5 - Weak notation system and parser.</td></tr></tbody></table>

**P1 - Conceptual.** Agda meta-programs are simply Agda programs with a return type in the typechecking monad $\mathcal{T}C$: this has the benefit that users do not need to learn a new programming language. MetaRocq uses the same approach based around a monad (the MetaRocq equivalent of the type-checking monad is the *TemplateMonad*), however in Agda's case the type-checking monad also contains the prover state, whereas in MetaRocq the state is threaded explicitly.

**P2 - Current.** The prover state is hidden in the $\mathcal{T}C$ monad: there is no need to thread it explicitly. We found monadic programming in Agda to be a lightweight and enjoyable programming experience, thanks to an extensive monad library based on type-classes (agda-stdlib-classes [15]).

**C1 - Conceptual.** Agda implements binders in terms using de Bruijn indices, which has the same drawbacks we explained in § 3. Additionally, we note that the API to manipulate the local (de Bruijn) context is currently awkward to use: for instance some functions expect the context in reverse order (last to first), and some expect it in normal order (first to last).

**C2 - Conceptual.** The internal representation of terms is quite restrictive. First, let bindings (as well as where clauses) are not represented in the abstract syntax, but are instead inlined during type-checking: meta-programs cannot make use of such features when building terms. Second, terms are always beta-normal, making it difficult to build a term corresponding to a function application. Implementing substitution on this representation of terms is quite delicate, and in fact there is no substitution function available in the meta-programming API.

**C3 - Current.** Agda's type-class resolution is weaker than in Rocq or Lean. Historically, Agda did not allow overlapping instances and instance search was not backtracking. These features are now supported, but recursive instances can still cause type-class resolution to loop. This is because instance search is implemented using a depth-first search, whereas one would need breadth-first search to avoid looping. In our case a crucial typeclass instance (for the composition of functors) is recursive: we had to cap instance search at a very low depth to get acceptable type-checking times. This workaround would not scale to real-world applications. Additionally, although Agda has the concept of local type-class instances, using local instances via the meta-programming API is not directly supported and requires awkward workarounds.

**C4 - Current.** Performance of meta-programs in the type-checking monad $\mathcal{T}C$ can be poor: we noticed significant slowdowns compared to equivalent pure code on small examples, but providing larger benchmarks is outside the scope of this study.

**C5 - Current.** Agda's support for custom notations seems inferior. For instance there is no syntax sugar for lists (such as `[1; 2; 3; 4]` in Rocq); it is not possible to provide such a notation using Agda's notation system due to notation clashes, and there is no list built-in list notation. Controlling the precedence levels of notations is difficult, leading to many unnecessary parentheses.

## 9 Related Work

Dubois de Prisque [22] compares Ltac1, Ltac2, MetaRocq, and Elpi as meta-programming languages in tutorial style through different examples. In conclusion, Ltac1 lacks a clear semantics and static typing, and tactics not being allowed to have side effects and return a value leads to ubiquitous, hard to read CPS translations. Ltac2 solves many of the issues of Ltac1, but manipulating the low-level term representation is difficult (many things were even impossible at the time the thesis was written).
MetaRocq allows to manipulate the low-level term representation, and might allow formally proving correctness of the meta-programs. However, de Bruijn arithmetic and lack of proper abstractions for effects (in particular mutual state and non-terminating functions) is criticised. For Elpi, Dubois de Prisque lauds the benefits of HOAS and remarks that term quotations are beneficial. However, HOAS seems to be difficult for term to term transformations when the structure of the output is very different from that of the input. Writing tactics was reported as tedious, which however could be a problem related to how Elpi represents the proof context, i.e. might not be conceptual.

HOL-based proof assistants come with meta-programming support in their host language. HOL4 and HOL light might offer the most natural experience, since proving happens just in an OCaml session. Isabelle allows meta-programming in Standard ML. Beluga is a proof assistant for the mechanisation of meta-theory based on contextual modal type theory. There is a lot of ongoing work on how to make quotation native in contextual modal type theory and thus allow certifiable meta-programming [35–39, 59]. The concerns of this setting are somewhat orthogonal to ours: They try to understand the foundations of meta-programming by extending type theory, whereas we focus on power and usability of frameworks that are built on top of type theory.

# 10 Conclusion

We now synthesise the pros and cons of §§ 3 to 8 into insights.

**Conceptual.** Binder representation was a recurring issue in this paper. Meta-programs involve manipulating terms as data, and as such it must be easy to construct and inspect the structure of terms, including binders. In particular, we note that our de Bruijn based implementations used arithmetic on indices, which lead to frequent mistakes and bugs. The locally-nameless representation simplifies writing correct code, but comes with minor efficiency considerations. Finding the best binder representation for meta-programming is still an open problem.

Term quotations allow to use user syntax directly when constructing and pattern matching on terms, thereby removing the need to spell out fully qualified constant names, implicit arguments, type-class instances, or universe levels. Additionally, term quotations allow some amount of type-checking at compile time (such as scope analysis) which allows one to catch errors earlier. Quasiquotations (i.e. the ability to nest anti-quotations and quotations) and the ability to quote open terms are especially useful, but are currently only supported in Lean and Elpi.

Recursive function generation is crucial, which became especially apparent for the example in Lean 4, where the need to fall back on primitive recursors prevented us from implementing a plugin with the same features as in the other systems: recursive types such as lists are not supported. Thus, a meta-programming framework must expose powerful tools for this generation, with unification and type inference support, even if recursive functions are not native to the kernel.

State is inherent to meta-programs, which can read and modify the global environment, local environment, and unification state. A good meta-programming framework must more generally provide good abstractions to deal with various kinds of effects, such as printing, exceptions, non-termination, and (prover) state. Lean and Agda handle printing using an IO monad and generally provide good monad libraries, while Rocq only provides ad hoc printing using the reduction-effects plugin [34] and does not have a satisfactory monad library (see § 4).

Verifiability is a desirable property of frameworks. Ideally formal verification is possible. Verification is not so attractive for users of meta-programs because properties such as well-typedness can be checked a posteriori by the kernel, but implementors of meta-programs might be interested in (partial) correctness guarantees. Indeed, formal specifications can partly replace documentation – which is lacking for all considered frameworks anyways – and can help in writing correct meta-programs, which is far from an easy task considering the complexity of the underlying systems.
**Current.** *The learning curve* of a meta-programming framework is crucial, and writing meta-programs in a different language than that of the underlying proof assistant leads to a steeper curve. Learning Elpi was especially challenging due to the paradigm shift to logical programming.

A proper meta-programming language requires adequate tooling, such as a language server, a documentation generator, a package manager, an optimising compiler or an efficient interpreter, and a good integration with the proof assistant's build system. Most of these tools come for free when the meta-language is the proof assistant itself or an already established programming language (such as OCaml), but require significant engineering work in the case of a DSL (e.g. Elpi or Ltac2).

Precise performance considerations are outside the scope of this paper, although we did comment on performance when relevant. We argue that meta-programming should prioritise usability over performance when possible. Performance is however an important issue when considering tactic programming or more complex meta-programs such as unification algorithms and type-checkers.

**Summary.** Conceptually, two meta-programming approaches emerge. Meta-programming directly in the proof assistant or using a domain specific language (DSL).

The first option allows the possibility of verifying meta-programs, which is relevant for authors of meta-programs. Verifying meta-programs requires both a specification of the basic meta-programming operations provided by the framework, and adequate means to use these basic specifications in order to derive guarantees about complex meta-programs. We note that one can not realistically expect to prove that the meta-programming framework fulfills its specification, as this would amount to proving the correctness of the entire elaborator and kernel of the underlying proof assistant. A more realistic approach is to interface with two implementation of elaborator and kernel: a naive but verified implementation à la MetaRocq [65], and an efficient but unverified implementation. The second option does not allow certifying meta-programs, but enables using domain-specific programming language features. Elpi is an example of such a DSL: logic programming is a valuable tool for working with syntax and binders. Using Elpi is warranted by the fact that one can not directly use logic programming in Rocq. In both cases, one needs a feature-complete meta-programming API, which stays up to date with the evolution of the proof assistant. As implementors of a meta-programming framework, bootstrapping the proof assistant gives a feature-complete API for free, but requires significant work a priori (for instance Lean 4's elaborator is bootstrapped). An alternate approach, which MetaRocq and Agda follow, is to do meta-programming directly in the proof assistant, without bootstrapping. Interfacing with the elaborator and kernel is done using a meta-programming monad, which from a user's point of view is very similar to bootstrapping, but requires more work from the implementors.

# 11 Future Work

A natural direction for future work is to extend this study to other dependently typed programming languages – such as Idris – or other proof assistants, e.g. from the HOL family or Beluga. We also want to study term to term transformations, where we expect most of our results to carry over, although Dubois de Prisque remarks that HOAS can cause issues for these transformations [22]. Surveying tactic frameworks might also provide valuable insights. There are however far less tactic-than meta-programming frameworks, thus a survey would amount to comparing proof assistants.

An orthogonal direction is to extend one of the implementations into a standalone tool, and derive Function instances for more general types, such as inductives with several parameters or non-uniform parameters, following the ideas of Laurent et al. [40].

Central future work is to develop a meta-programming framework based on our insights, potentially in parallel for different proof assistants. We believe that a key insight is that meta-programs are inherently effectful programs, which have access both to generic effects such as failure and non-termination, and to domain specific effects such as the ability to read and modify the global
environment, local context and evar-map. We also argue that, considering the complexity of the underlying systems, verifying meta-programs is of great interest for implementors of meta-programs. These ideas hint at the possibility of using powerful verification techniques to ease reasoning about meta-programs: one can use specialised program logics tailored to domain specific effects, and in particular separation logic to handle the evar-map, building on ideas from Nigron and Dagand [52] and Vistrup et al. [76].

## References

[1] Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Z. Weaver. 2016. CertiCoq: A verified compiler for Coq. https://apisemanticscholar.org/CorpusID:9607775

[2] Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. In *ITP 2018*. 20–39. doi:10.1007/978-3-319-94821-8_2

[3] Abhishek Anand, Anvay Grover, John Li, Greg Morrisett, Randy Pollack, Olivier Savary Belanger, Matthew Weaver, Andrew Appel, Yannick Forster, Joomy Korkut, Zoe Paraskevopoulou, Kathrin Stark, and Matthieu Sozeau. 2025. CertiCoq: A verified compiler for Coq (GitHub repository). (2025). https://github.com/CertiCoq/certicoq accessed Feb 18th 2025.

[4] Danił Annenkov, Jakob Botsch Nielsen, and Bas Spitters. 2020. ConCert: a smart contract certification framework in Coq. In *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020*, Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, 21–228. doi:10.1145/3372885.3373829

[5] Anne Baanen. 2020. A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). In *Automated Reasoning*, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham, 21–27.

[6] Edwin C. Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. *J. Funct. Program*. 23, 5 (2013), 552–593. doi:10.1017/S095679681300018X

[7] Edwin C. Brady. 2021. Idris 2: Quantitative Type Theory in Practice. In *35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference) (LIPIcs, Vol. 194)*, Anders Møller and Manu Sridharan (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 9:1–9:26. doi:10.4230/LIPICS.ECOOP.2021.9

[8] Mario Carneiro. 2024. Lean4Lean: Towards a Verified Typechecker for Lean, in Lean. arXiv:2403.14064 [cs.PL] https://arxiv.org/abs/2403.14064

[9] Tej Chajed. 2021. Record Updates in Coq. In *CoqPL 2021: The Seventh International Workshop on Coq for Programming Languages*. https://popl21.sigplan.org/details/CoqPL-2021-papers/3/Record-Updates-in-Coq Extended Abstract.

[10] Arthur Charguéraud. 2012. The Locally Nameless Representation. *Journal of Automated Reasoning* - JAR 49 (10 2012), 1–46. doi:10.1007/s10817-011-9225-2

[11] Adam Chlipala. 2008. Parametric higher-order abstract syntax for mechanized semantics. *SIGPLAN Not*. 43, 9 (Sept. 2008), 143–156. doi:10.1145/1411203.1411226

[12] Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2023. Trocq: Proof Transfer for Free, With or Without Univalence. CoRR abs/2310.14022 (2023). doi:10.48550/ARXIV.2310.14022 arXiv:2310.14022

[13] Cyril Cohen, Pierre Roux, Enrico Tassi, Kazuhiko Sakaguchi, affeldt aist, Laurent Théry, Erik Martin-Dorel, Georges Gonthier, Assia Mahboubi, Christian Doczkal, Florent Hivert, Yves Bertot, Maxime Dénès, Anton Trunov, jouvelot, Emilio Jesús Gallego Arias, Pierre-Marie Pédrot, Evgeniy Moiseenko, Jasper Hugunin, Pierre-Yves Strub, antonio nikishaev, KimayaBedarkar, YOSHIHIRO Imai, Pierre PomCo, Julin S, Jason Gross, Hugo Herbelin, Alex Gryzlov, Gabriel Taumaturgo, and Mireia G. Bedmar. 2024. *math-comp/math-comp: The Mathematical Components Library 2.3.0*. doi:10.5281/zenodo.14237175

[14] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. 2020. Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). In *5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference) (LIPIcs, Vol. 167)*, Zena M. Ariola (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 34:1–34:21. doi:10.4230/LIPICS.FSCD.2020.34

[15] Agda Community. [n. d.]. *agda-stdlib-classes*. https://github.com/agda/agda-stdlib-classes

[16] Thierry Coquand and Gérard P Huet. 1988. The Calculus of Constructions. *Information and Computation* 76, 2/3 (1988), 95–120. doi:10.1016/0890-5401(88)90005-3

[17] Enzo Crance. 2023. *Méta-programmation pour le transfert de preuve en théorie des types dépendants*. Theses. Nantes Université. https://theses.hal.science/tel-04719004

[18] Adrian Dapprich. 2021. Autosubst MetaCoq. https://github.com/uds-psl/autosubst-metacoq

[19] Adrian Dapprich. 2021. Generating Infrastructural Code for Terms with Binders using MetaCoq. Bachelor's thesis, Saarland University.
[20] Arthur Azevedo de Amorim. 2020. Deriving Instances with Dependent Types. In Proceedings of the Sixth International Workshop on Coq for Programming Languages (CoqPL 2020) (New Orleans, Louisiana, USA). https://popl20.sigplan.org/details/CoqPL-2020-papers/1/Deriving-Instances-with-Dependent-Types

[21] N.G de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5 (1972), 381-392. doi:10.1016/1385-7258(72)90034-0

[22] Louise Dubois de Prisque. 2024. Prétraitement compositionnel en Coq. (Compositional preprocessing in Coq). Ph. D. Dissertation. University of Paris-Saclay, France. https://tel.archives-ouvertes.fr/tel-04696909

[23] Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. 2022. A drag-and-drop proof tactic. In CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, Andrei Popescu and Steve Zdancewic (Eds.). ACM, 197-209. doi:10.1145/3497775.3503692

[24] Catherine Dubois, Nicolas Magaud, and Alain Giorgetti. 2022. Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. In 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France (LIPICS, Vol. 269), Delia Kesner and Pierre-Marie Pédrot (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 11:1-11:19. doi:10.4230/LIPICS TYPES.2022.11

[25] Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. 2015. ELPI: Fast, Embeddable, λProlog Interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9450), Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.). Springer, 460-468. doi:10.1007/978-3-662-48899-7_32

[26] Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017. A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1, ICFP, Article 34 (Aug. 2017), 29 pages. doi:10.1145/3110278

[27] Davide Fissore and Enrico Tassi. 2023. A new Type-Class solver for Coq in Elpi. In The Coq Workshop 2023. Bialystok, Poland. https://inria.hal.science/hal-04467855

[28] João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling. 2015. Pi-Ware: Hardware Description and Verification in Agda. In 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia (LIPICS, Vol. 69), Tarmo Uustalu (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 9:1-9:27. doi:10.4230/LIPICS. TYPES.2015.9

[29] Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. 2024. Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. 8, PLDI, Article 149 (June 2024), 24 pages. doi:10.1145/3656379

[30] Yannick Forster and Kathrin Stark. 2020. Coq à la carte: a practical approach to modular syntax with binders. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, 186-200. doi:10.1145/3372885.3373817

[31] Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi. 2023. Practical and sound equality tests, automatically - Deriving eqType instances for Jasmin's data types with Coq-Elpi. In CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs). ACM, Boston MA USA, France, 167-181. doi:10.1145/3573105.3575683

[32] Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala. 2022. Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. In 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel (LIPICS, Vol. 237), June Andronick and Leonardo de Moura (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 18:1-18:18. doi:10.4230/LIPICS.ITP.2022.18

[33] Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. 2019. Implementing Type Theory in Higher Order Constraint Logic Programming. Mathematical Structures in Computer Science 29, 8 (March 2019), 1125-1150. https://inria.hal.science/hal-01410567

[34] Hugo Herbelin. [n. d.]. reduction-effects. https://github.com/coq-community/reduction-effects

[35] Jason Z. S. Hu and Brigitte Pientka. 2024. A Layered Approach to Intensional Analysis in Type Theory. ACM Trans. Program. Lang. Syst. 46, 4 (2024), 15:1-15:43. doi:10.1145/3707203

[36] Jason Z. S. Hu and Brigitte Pientka. 2024. Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. In Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 14576), Stephanie Weirich (Ed.). Springer, 52-82. doi:10.1007/978-3-031-57262-3_3

[37] Jason Z. S. Hu and Brigitte Pientka. 2025. A Dependent Type Theory for Meta-programming with Intensional Analysis. Proc. ACM Program. Lang. 9, POPL (2025), 416-445. doi:10.1145/3704851

[38] Jason Z. S. Hu, Brigitte Pientka, and Ulrich Schöpp. 2022. A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types. ACM Trans. Comput. Log. 23, 4 (2022), 25:1-25:36. doi:10.1145/3545115
[39] Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka. 2022. Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself. Proc. ACM Program. Lang. 6, POPL (2022), 1-27. doi:10.1145/3498700

[40] Théo Laurent, Meven Lennon-Bertrand, and Kenji Maillard. 2024. Definitional Functionality for Dependent (Sub)Types. In Lecture Notes in Computer Science. 302-331. doi:10.1007/978-3-031-57262-3_13

[41] Bohdan Liesnikov, Marcel Ullrich, and Yannick Forster. 2020. Generating induction principles and subterm relations for inductive types using MetaCoq. CoRR abs/2006.15135 (2020). arXiv:2006.15135 https://arxiv.org/abs/2006.15135

[42] Jannis Limperg. 2021. A novice-friendly induction tactic for lean. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (Virtual, Denmark) (CPP 2021). Association for Computing Machinery, New York, NY, USA, 199-211. doi:10.1145/3437992.3439928

[43] Jannis Limperg and Asta Halkjær From. 2023. Aesop: White-Box Best-First Proof Search for Lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (Boston, MA, USA) (CPP 2023). Association for Computing Machinery, New York, NY, USA, 253-266. doi:10.1145/3573105.3575671

[44] Nicolas Magaud. 2023. Towards Automatic Transformations of Coq Proof Scripts. In Proceedings 14th International Conference on Automated Deduction in Geometry, ADG 2023, Belgrade, Serbia, 20-22th September 2023 (EPTCS, Vol. 398), Pedro Quaresma and Zoltán Kovács (Eds.). 4-10. doi:10.4204/EPTCS.398.4

[45] Matteo Manighetti, Dale Miller, and Alberto Momigliano. 2021. Two Applications of Logic Programming to Coq. In 26th International Conference on Types for Proofs and Programs (TYPES 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 188), Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 10:1-10:19. doi:10.4230/LIPIcs.TYPES.2020.10

[46] The mathlib Community. 2020. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). Association for Computing Machinery, New York, NY, USA, 367-381. doi:10.1145/3372885.3373824

[47] Conor McBride and James McKinna. 2004. Functional pearl: i am not a number-i am a free variable. In Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell (Snowbird, Utah, USA) (Haskell '04). Association for Computing Machinery, New York, NY, USA, 1-9. doi:10.1145/1017472.1017477

[48] Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Lecture Notes in Computer Science. 625-635. doi:10.1007/978-3-030-79876-5_37

[49] Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28, André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 625-635.

[50] Gopalan Nadathur and Dale Miller. 1988. An Overview of Lambda Prolog. Technical Report. USA.

[51] Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. 2023. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bialystok, Poland (LIPIcs, Vol. 268), Adam Naumowicz and René Thiemann (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 24:1-24:20. doi:10.4230/LIPICS.ITP.2023.24

[52] Pierre Nigon and Pierre-Évariste Dagand. 2021. Reaching for the Star: Tale of a Monad in Coq. In Leibniz International Proceedings in Informatics (LIPIcs) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193). Schloss Dagstuhl, Rome, Italy, 29:1-29:19. doi:10.4230/LIPIcs.ITP.2021.29

[53] Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Vol. 32. Chalmers University of Technology.

[54] Ulf Norell, Nils Anders Danielsson, Jesper Cockx, and Andreas Abel. [n. d.]. Agda Wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php.

[55] Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos. 2022. Computing correctly with inductive relations. In PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, Ranjit Jhala and Isil Dillig (Eds.). ACM, 966-980. doi:10.1145/3519939.3523707

[56] Christine Paulin-Mohring. 1993. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications. Springer, 328-345. doi:10.1007/BFb0037116

[57] Arthur Paulino, D Testa, E Ayers, H Böving, J Limperg, S Gadgil, and S Bhat. 2024. Metaprogramming in Lean 4. Online Book. https://github.com/arthurpaulino/lean4-metaprogramming-book (2024).

[58] F. Pfenning and C. Elliott. 1988. Higher-order abstract syntax. SIGPLAN Not. 23, 7 (June 1988), 199-208. doi:10.1145/960116.54010

[59] Brigitte Pientka. 2025. A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract). In Proceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2025, Denver, CO, USA, 21 January 2025, Guillaume Allais and Yanhong Annie Liu (Eds.). ACM, 10-11. doi:10.1145/3704253.3706136

[60] Pierre-Marie Pédrot. 2019. Ltac2: Tactical Warfare. In The 5th International Workshop on Coq for Programming Languages (CoqPL 2019). https://popl19.sigplan.org/details/CoqPL-2019/8/Ltac2-Tactical-Warfare Talk at CoqPL 2019, affiliated
with POPL 2019.

[61] Talia Ringer. 2021. *Proof Repair*. Ph. D. Dissertation. University of Washington, USA. https://hdl.handle.net/1773/47429

[62] Ayumu Saito and Reynald Affeldt. 2022. Towards a Practical Library for Monadic Equational Reasoning in Coq. In *Mathematics of Program Construction*, Ekaterina Komendantskaya (Ed.). Springer International Publishing, Cham, 151–177.

[63] Kazuhiko Sakaguchi. 2022. Reflexive Tactics for Algebra, Revisited. In *13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel (LIPIcs, Vol. 237)*, June Andronick and Leonardo de Moura (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 29:1–29:22. doi:10.4230/LIPICS.ITP.2022.29

[64] Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2020. The MetaCoq Project. *Journal of Automated Reasoning* (Feb. 2020). doi:10.1007/s10817-019-09540-0

[65] Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2019. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. *Proc. ACM Program. Lang.* 4, POPL, Article 8 (Dec. 2019), 28 pages. doi:10.1145/3371076

[66] Arnaud Spiwack. 2010. An abstract type for constructing tactics in Coq. In *Proof Search in Type Theory*. Edinburgh, United Kingdom. https://inria.hal.science/inria-00502500

[67] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. 2019. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*, Assia Mahboubi and Magnus O. Myreen (Eds.). ACM, 166–180. doi:10.1145/3293880.3294101

[68] Carst Tankink, Herman Geuvers, James McKinna, and Freek Wiedijk. 2010. Proviola: A Tool for Proof Re-animation. *CoRR* abs/1005.2672 (2010). arXiv:1005.2672 http://arxiv.org/abs/1005.2672

[69] Enrico Tassi. 2019. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In *10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 141)*, John Harrison, John O'Leary, and Andrew Tolmach (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 29:1–29:18. doi:10.4230/LIPIcs.ITP.2019.29

[70] The Coq Development Team. 2024. *The Coq Proof Assistant*. doi:10.5281/zenodo.14542673

[71] Sebastian Ullrich and Leonardo de Moura. 2020. Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. In *Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II* (Paris, France). Springer-Verlag, Berlin, Heidelberg, 167–182. doi:10.1007/978-3-030-51054-1_10

[72] Sebastian Ullrich and Leonardo de Moura. 2022. 'do' unchained: embracing local imperativity in a purely functional language (functional pearl). *Proc. ACM Program. Lang.* 6, ICFP, Article 109 (Aug. 2022), 28 pages. doi:10.1145/3547640

[73] Cas van der Rest and Wouter Swierstra. 2022. A completely unique account of enumeration. *Proc. ACM Program. Lang.* 6, ICFP (2022), 411–437. doi:10.1145/3547636

[74] Paul van der Walt and Wouter Swierstra. 2012. Engineering Proof by Reflection in Agda. In *International Symposium on Implementation and Application of Functional Languages*. https://apisemanticscholar.org/CorpusID:18658569

[75] Marcell van Geest and Wouter Swierstra. 2017. Generic packet descriptions: verified parsing and pretty printing of low-level data. In *Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2017, Oxford, UK, September 3, 2017*, Sam Lindley and Brent A. Yorgey (Eds.). ACM, 30–40. doi:10.1145/3122975.3122979

[76] Max Vistrup, Michael Sammler, and Ralf Jung. 2025. Program Logics à la Carte. *Proc. ACM Program. Lang.* 9, POPL, Article 11 (Jan. 2025), 32 pages. doi:10.1145/3704847
## A Rocq Plugin - de Bruijn code

``` OCaml
let build_fmap env sigma ind : Evd.evar_map * EConstr.t =
(* Construct the lambda abstractions. *)
lambda env sigma "a" ta @@ fun env ->
lambda env sigma "b" tb @@ fun env ->
lambda env sigma "f" (arr (mkRel 2) (mkRel 1)) @@ fun env ->
lambda env sigma "x" (apply_ind env ind @@ mkRel 3) @@ fun env ->
let inp = { a = 4; b = 3; f = 2; x = 1 } in
(* Construct the case return clause. *)
let sigma, case_return =
  lambda env sigma "_" (apply_ind env ind @@ mkRel inp.a) @@ fun env ->
  (sigma, apply_ind env ind @@ mkRel (1 + inp.b))
in
(* Construct the case branches. *)
let rec loop sigma acc ctrs_a ctrs_b =
  match (ctrs_a, ctrs_b) with
  | [], [] -> (sigma, Array.of_list @@ List.rev acc)
  | ca :: ctrs_a, cb :: ctrs_b ->
    let sigma, branch = buildahan env sigma inp ca cb in
    loop sigma (branch :: acc) ctrs_a ctrs_b
  | _ -> Log.error "build_fmap : different lengths"
in
let sigma, branches =
  loop sigma [] (constructors env ind @@ mkRel inp.a) (constructors env ind @@ mkRel inp.b)
in
(* Finally construct the case expression. *)
( sigma
, Inductiveops.Simple_make_case_or_project env sigma
  (Inductiveops.make_case_info env ind Constr(regularStyle)
   (case_return, ERelevance.relevant)
   Constr.NoInvert (mkRel inp.x) branches )
let buildahan env sigma inp ca cb : Evd.evar_map * EConstr.t =
(* Arguments are processed from outermost to innermost. *)
let rec loop env sigma i acc decls =
  match decls with
  | [] -> (sigma, acc)
  | decl :: decls ->
    let env = Environ.push_rel decl env in
    let sigma, arg' =
      (* Call build_arg at a depth which is consistent with the local context
         of the environment, and lift the result to bring it at depth [n]. *)
      build_arg env sigma
        (liftInputs (i + 1) inp)
        (mkRel 1)
        (Vars.lift 1 @@ EConstr.of_constr @@ get_type decl)
    in
    loop env sigma (i + 1) (lift (ca.cs - i - 1) arg' :: acc) decls
in
let sigma, args' =
  loop env sigma 0 [] (List.rev @@ EConstr.to_rel_context sigma ca.cs_args)
in
(* Apply the constructor to the arguments. *)
let body = mkApp (mkConstructU cb.cs_cstr,
  Array.of_list (mkRel (ca.cs_args + inp.b) :: List.rev args'))
in
(* Bind the constructor arguments. *)
let branch =
  it_mklambda body @@ List.map
    (function LocalAssum (b, ty) | LocalDef (b,_, ty) -> (b, ty))
    ca.cs_args
in
```
(sigma, branch)

<caption>Fig. 1. OCaml code for `build_fmap` and `buildazine`.</caption>
## B Rocq Plugin - Locally Nameless

``` OCaml
let build_fmap env sigma ind : Evd.evar_map * EConstr.t =
(* Abstract over the input variables. *)
namedLambda env sigma "a" ta @@ fun env sigma a ->
namedLambda env sigma "b" tb @@ fun env sigma b ->
namedLambda env sigma "f" (mkArrowR (mkVar a) (mkVar b)) @@ fun env sigma f ->
namedLambda env sigma "x" (apply_ind env ind @@ mkVar a) @@ fun env sigma x ->
(* Construct the case return clause. *)
let sigma, case_return =
  namedLambda env sigma "_" (apply_ind env ind @@ mkVar a) @@ fun env sigma _ ->
  (sigma, apply_ind env ind @@ mkVar b)
in
(* Construct the case branches. *)
let rec loop sigma acc ctrs_a ctrs_b =
  match (ctrs_a, ctrs_b) with
  | [], [] -> (sigma, Array.of_list @@ List.rev acc)
  | ca :: ctrs_a, cb :: ctrs_b ->
    let sigma, branch = buildahan env sigma { fmap; a; b; f; _x = x } ca cb in
    loop sigma (branch :: acc) ctrs_a ctrs_b
  | _ -> Log.error "build_map : different lengths"
in
let sigma, branches = loop sigma [] (constructors env @@ mkVar a) (constructors env @@ mkVar b) in
(* Finally construct the case expression. *)
( sigma
, Inductiveops.simple_make_case_or_project env sigma
  (Inductiveops.make_case_info env ind Constr(regularStyle)
   (case_return, ERelevance.relevant)
   Constr.NoInvert (mkVar x) branches )
let buildahan env sigma inp ca cb : Evd.evar_map * EConstr.t =
(* Bind the arguments of the constructor. *)
namedLambdaContext env sigma ca.cs_args @@ fun env sigma args ->
(* Map the correct function over each argument. *)
let arg_tys = List.map Declaration.get_type ca.cs_args in
let rec loop sigma acc args arg_tys =
  match (args, arg_tys) with
  | [], [] -> (sigma, acc)
  | arg :: args, ty :: arg_tys ->
    let sigma, arg' = build_arg env sigma inp arg ty in
    loop sigma (arg' :: acc) args arg_tys
  | _ -> Log.error "buildahan : length mismatch"
in
let sigma, args' = loop sigma [] (List.map mkVar args) arg_tys in
(* Apply the constructor to the arguments. *)
 sigma, mkApp (mkConstructU cb.cs_cstr, Array.of_list (mkVar inp.b :: args')))
```

<caption>Fig. 2. OCaml code for `build_fmap` and `build, locally-nameless version.</caption>

De Bruijn indices are arguably the most common binder representation in implementations of dependently-typed proof assistants (Rocq, Agda, and Idris all use de Bruijn indices internally), however an alternative is locally nameless, in which bound variables are represented using de Bruijn indices, but free variables are named. For instance the term $\lambda x.\lambda y.f x y$ (which has one free variable $f$) is represented in locally nameless as $\lambda.\lambda.f 1 0$. Maintaining the locally nameless invariant as terms are traversed requires some amount of bookkeeping from the user, but crucially all index arithmetic and lifting is performed by the API. We refer the reader to the paper by McBride and McKinna [47] for an introduction to programming with locally nameless. The work of Charguéraud [10] provides a more formal perspective on locally-nameless.

Rocq already has most of the infrastructure needed for locally nameless: indeed, section variables and local hypotheses are represented using named variables instead of indices. We can reuse these named variables to represent free variables. Named variables have good support in the OCaml implementation: they have their own named local context, and most functions which take as
input the global environment and local context – such as unification or type-class search – also support the named local context. Using named variables, we can implement a small library of term manipulation functions in the locally nameless style, and use it to improve the plugin of the previous section by removing the friction points related to index manipulation.

Figure 2 shows the corresponding code. The `lambda` function has been replaced by `namedLambda`:

```
namedLambda (env : Environ.env) (sigma : Evd.evar_map) (name : string) (ty : EConstr.t)
    (mk_body : Environ.env -> Evd.evar_map -> Names variable -> Evd.evar_map * EConstr.t) :
    Evd.evar_map * EConstr.t
```

The most notable difference is that `namedLambda` passes a fresh named variable `x` to the continuation `mk_body`. The continuation builds a term in which `x` is free, and `namedLambda` subsequently replaces all occurrences of `x` in the body by de Bruijn index 1 (de Bruijn indices start at 1 in plugins). Additionally, when referring to a variable `x` we use `mkVar` `x` instead of writing down the exact de Bruijn index of `x`.

The switch to locally nameless is the only difference between the plugin of § 3 and this version; we concentrate on the pros and cons that come with locally nameless.

<table><thead><tr><th>Conceptual</th><th>Current</th></tr></thead><tbody><tr><td><strong>Pros</strong> P1 - Locally-nameless provides a nice API to build P2 - Locally-nameless is easy to add to Rocq. terms.</td><td></td></tr><tr><td><strong>Cons</strong> C1 - Locally-nameless is less efficient than de Bruijn.</td><td></td></tr></tbody></table>

**P1 - Conceptual.** We found programming using locally-nameless to be much easier than using de Bruijn indices. Using locally-nameless, one never has to write exact de Bruijn indices, to perform index arithmetic or to lift terms. For instance, compare the first lines of `build_fmap` using de Bruijn indices (in figure 1):

```
lambda env sigma "a" ta @@ fun env ->
lambda env sigma "b" tb @@ fun env ->
lambda env sigma "f" (arr (mkRel 2) (mkRel 1)) @@ fun env ->
lambda env sigma "x" (apply_ind env ind @@ mkRel 3) @@ fun env ->
```

And using a locally-nameless style (in figure 2):

```
namedLambda env sigma "a" ta @@ fun env sigma a ->
namedLambda env sigma "b" tb @@ fun env sigma b ->
namedLambda env sigma "f" (mkArrowR (mkVar a) (mkVar b)) @@ fun env sigma f ->
namedLambda env sigma "x" (apply_ind env ind @@ mkVar a) @@ fun env sigma x ->
```

**P2 - Current.** Locally-nameless integrates well with Rocq's internal API: even intermediate terms which contain named (free) variables are compatible with Rocq's infrastructure, and can be passed for instance to unification or type-checking. The fact that Rocq has such good support for named variables out of the box made it very easy to use a locally-nameless style. Without such good support, we would need to implement a separate representation for terms, and to convert back and forth between these two representations.

**C1 - Conceptual.** The locally nameless binder representation requires very frequent substitution of named variables with de Bruijn indices, and vice versa; although this is hidden from the user, it does have an impact on performance. Measuring the precise cost of these substitutions in practice is outside the scope of this study, but we did not notice a significant performance degradation in our case. If it becomes an issue, one can use a pure de Bruijn representation in performance-critical sections, breaking the locally nameless invariant locally, while still enjoying locally nameless in the rest of the code. This is exactly what the implementation of Lean 4 does, in addition to some simple caching optimisations to improve the performance of substitutions in common cases. Implementing these optimisations in Rocq is not as straightforward as one would hope, and has not been done in this study.

**Locally nameless in other frameworks.** One could also imagine using MetaRocq's implementation to work with locally nameless. However, unfortunately most of the API does not work well with
named variables because they do not occur in closed terms checked by the kernel, and thus MetaRocq does not even have a notion of named local context. Following a locally nameless discipline would require one to either convert terms to a pure de Bruijn representation on the fly when calling MetaRocq functions, or add support for named variables throughout the entirety of MetaRocq, requiring significant engineering effort.

## C MetaRocq code

```
Definition build_fmap ctx ind ind_body : term :=
(* Abstract over the input parameters. *)
mk lambda ctx "A" (tSort @@ sType fresh_universe) @@ fun ctx @>
mk lambda ctx "B" (tSort @@ sType fresh_universe) @@ fun ctx @>
mk lambda ctx "f" (mkArrow (tRel 1) (tRel 0)) @@ fun ctx @>
mk lambda ctx "x" (tApp (tInd ind[]) [tRel 2]) @@ fun ctx @>
let inp := { fmap := 4 ; A := 3 ; B := 2 ; f := 1 ; x := 0 } in
(* Construct the case information. *)
let ci := { ci_ind := ind ; ci_npar := 1 ; ci_relevance := Relevant } in
(* Construct the case predicate. *)
let pred :=
{ | pinst := []
; pparams := [tRel inp.(A)]
; pcontext := [[| binder_name := nNamed "x" ; binder_relevance := Relevant ]]]
; preturn := tApp (tInd ind[]) [tRel (inp.(B) + 1) ] ]
in
(* Construct the branches. *)
let branches := mapi (buildahan ctx ind inp) ind_body.(ind_actors) in
tCase ci pred (tRel inp.(x)) branches.

Definition buildahan ctx ind inp ctor_idx ctor : branch term :=
(* Get the context of the constructor. *)
let bcontext := List.map decl_name ctor.(cstr_args) in
let n := List.length bcontext in
(* Get the types of the arguments of the constructor at type [A]. *)
let arg tys := cstr_args_at ctor (tInd ind[]) [tRel inp.(A)] in
(* Process the arguments one by one, starting from the outermost one. *)
let loop := fix loop ctx i acc decls :=
match decls with
| [] => List.rev acc
| d :: decls =>
let ctx := d :: ctx in
(* We call build_arg at a depth which is consistent with the local context,
and we lift the result to bring it at depth [n]. *)
let mapped_arg := build_arg ctx (liftInputs (i + 1) inp) (tRel 0) (lift0 1 d.(decl_type)) in
loop ctx (i + 1) (lift0 (n - i - 1) mapped_arg :: acc) decls
go
in
(* The mapped arguments are at depth [n]. *)
let mapped_args := loop ctx 0 [] (List.rev arg tys) in
(* Apply the constructor to the mapped arguments. *)
let bbody := tApp (tConstruct ind ctor_idx[]) @@ tRel (inp.(B) + n) :: mapped_args in
(* Assemble the branch's context and body. *)
mkahan bcontext bbody.
```

<caption>Fig. 3. MetaRocq code for build_fmap and buildahan.</caption>
## D Ltac2 code

```c
(* Expects a goal of the form [forall A B, (A -> B) -> F A -> F B]. *)
Ltac2 build_fmap F : unit :=
  (* intro *)
  intro @A ; intro @B ; intro @f ; intro @x ;
  (* destruct *)
  Std.case false (Control.hyp @x, NoBindings) ;
  (* Build each branch. *)
  let n_actors := ... in
  Control.dispatch (List.init n_actors (buildahan F @A @B @f)).
```

```c
(* Expects a goal of the form [forall arg_1 ... arg_n, F B]. *)
Ltac2 buildahan F a b f i () : unit :=
  (* Introduce the arguments with fresh names. *)
  let n_args := ... in
  let args := n_intro n_args in
  (* Apply constructor [i]. *)
  constructor_n false i NoBindings ;
  (* Process each argument separately. *)
  Control.dispatch (List.map (build_arg a b f) args).
```

<caption>Fig. 4. Ltac2 code for build_fmap and buildahan.</caption>

## E Elpi code

```c
pred build-fmap i:inductive, o:term.
build-fmap I {{ fun (A B : Type) (f : A -> B) (x : lp:(FI A)) => lp:(M A B f x) }}
  :-
    % Declare FI
    (pi x\ coq.mk-app { coq.env.global (indt I) } [x] (FI x)),
    % Bind the parameters.
    @pi-decl `A` {{ Type }} a\
    @pi-decl `B` {{ Type }} b\
    @pi-decl `f` {{ lp:a -> lp:b }} f\
    @pi-decl `x` (FI a) x\
    % Build the inner match.
    coq.build-match x (FI a) (~~N~~N~~r\ r = FI b)
    (build-branch I a b f) (M a b f x).
```

```c
pred build-branch i:inductive, i:term, i:term, i:term, i:term, i:term, i:list term, i:list term, o:term.
build-branch I A B F CA _Args ArgSTy Branch :-
  % Process each argument.
  std.map2 Arg ArgSTy (build-arg I A B F) MappedArgs,
  % Change A with B in the constructor.
  (copy A B => copy CA CB),
  % Apply the constructor to the new arguments.
  coq.mk-app CB MappedArgs Branch.
```

<caption>Fig. 5. Elpi code for build-fmap and build-branch.</caption>
## F Lean code

``` Lean
def buildFmap ind : MetaM Expr := do
  -- Declare the input parameters.
  withLocalDecl `A .implicit (.sort ...) fun A => do
  withLocalDecl `B .implicit (.sort ...) fun B => do
  withLocalDecl `f .default (← mkArrow A B) fun f => do
  withLocalDecl `x .default (← apply_ind ind A) fun x => do
  -- Construct the case return type.
  let ret_type := Expr.lam `_ (← apply_ind ind A) (← apply_ind ind B) .default
  -- Construct the case branches.
  let branches ← ind.actors.toArray.mapM fun ctr => do
    let info ← getConstInfoCtor ctr
    buildBranch A B f info
  -- Construct the case expression.
  let cases_func ← freshConstant (← getConstInfo @@ .str ind.name "casesOn")
  let body := mkAppN cases_func @@ Array.append #[A, ret_type, x] branches
  -- Bind the input parameters.
  mkLambdaFVars #[A, B, f, x] body

def buildBranch A B f ctr : MetaM Expr := do
  -- Get the arguments of the constructor applied to A.
  let ctrTy ← instantiateTypeLevelParams (ConstantInfo.ctorInfo ctr) [...]
 forallTelescope (← instantiateForall ctrTy #[A]) fun args _ => do
    -- Map over each argument of the constructor.
    let mapped_args ← args.mapM (buildArg A B f)
    -- Apply the constructor to the new arguments.
    let freshCtor ← freshConstant @@ .ctorInfo ctr
    let body := mkAppN freshCtor @@ Array.append #[B] mapped_args
    -- Abstract with respect to the arguments.
    instantiateMVars =<< mkLambdaFVars args body
```

<caption>Fig. 6. Lean code for `buildFmap` and `buildBranch`.</caption>

For simplicity we assume that all arguments of `option` and its constructors are explicit, and do not show how to handle universe polymorphism (we use ellipses `...` in the code above).
## G Agda code

```hkl
build-fmap : Name -> Name -> TC (List Clause)
build-fmap ind func = do
  ind-def <- getDefinition ind
  ctors <-
    case ind-def of \
      ( (data-type npars ctors) -> return ctors
      ; _ -> typeError ... )
    mapM (build-clause ind func) ctors

build-clause : Name -> Name -> Name -> TC Clause
build-clause ind func ctor = do
  -- Bind the input arguments.
  let inp = record { ind = ind ; func = func ; a = 4 ; A = 3 ; b = 2 ; B = 1 ; f = 0 }
    inp-tele =
      ("a", hArg (quoteTerm Level)) ::
      ("A", hArg (agda-sort @@ Sort.set @@ var 0 [])) ::
      ("b", hArg (quoteTerm Level)) ::
      ("B", hArg (agda-sort @@ Sort.set @@ var 0 [])) ::
      ("f", vArg (pi (vArg @@ var 2 [])) @@ abs "_" @@ var 1 [])) :: []
inContext (List.reverse inp-tele) @ do
  -- Fetch the type of the constructor at parameter [A].
  ctor-ty <- inferType (con ctor (hArg (var (Inputs.a inp)) []) :: hArg (var (Inputs.A inp)) []) :: [])
  -- Get the types of the arguments of the constructor.
  let (args-tele,_) = pi-telescope ctor-ty
    n-args = List.length args-tele
  inContext (List.reverse @@ inp-tele ++ args-tele) @ do
    let inp = lift-inputs n-args inp
      -- Transform each argument as needed.
    mapped-args <-
      mapM (\(i,_, ty)) -> build-arg inp i @@ Arg.map (weaken (i + 1)) ty
        (List.zip (downFrom n-args) args-tele)
  -- Build the clause.
  let args-patt =
    List.zipWith
      (\(_, arg info_) i -> arg info (Pattern.var i))
      args-tele (downFrom n-args)
    patt =
      hArg (Pattern.var @@ Inputs.a inp) ::
      hArg (Pattern.var @@ Inputs.A inp) ::
      hArg (Pattern.var @@ Inputs.B inp) ::
      hArg (Pattern.var @@ Inputs.B inp) ::
      vArg (Pattern.var @@ Inputs.f inp) ::
      vArg (Pattern.con ctor args-patt) :: []
    body = con ctor (hArg (var (Inputs.b inp))’) :: hArg (var (Inputs.B inp)) :: mapped-args)
    Clause.clause (inp-tele ++ args-tele) patt body
```

<caption>Fig. 7. Agda code for build-fmap and build-clause.</caption>

## H On recursive inductives

Recall the definition of trees, which is both recursive and nested:

```
Inductive tree (A : Type) : Type :=
  | Leaf : tree A
  | Node : A -> list (tree A) -> tree A.
```

```
Fixpoint fmap (A B : Type) (f : A -> B) (t : tree A) : tree B :=
  match t with Leaf => Leaf
    | Node x ts => Node (f x) (List.map (fmap f) ts) end.
```

In the case of `Node` in the example above, we applied `f` to the first argument `x`, and `List.map (fmap f)` to the second argument `ts`. In general, there are various ways to disambiguate what function to apply. The canonical way is to do type-based disambiguation. An alternative is to use type class inference of the proof assistant, which is what we do in our implementation.
For instance, we define the branch as `Node (fmap f x) (fmap f ts)` in the example above, and let typeclass resolution determine which functor we are mapping over. To be able to do so, we need to use the identity functor for `x` and for `ts` the composition of the `list` and `tree` functors.

Consequently, we globally declare

```
Instance functor_id : Functor (fun T => T) := ...
Instance functor_comp (F G : Type -> Type) `(Functor F) `(Functor G) : Functor (fun T => G (F T)) := ...
```

Naively using the typeclass approach may fail in the case of recursive inductives such as `tree` or `list`. For instance in the `tree` example, typeclass resolution will fail to find a `Functor` instance for `fmap f ts` (because there is no instance of `Functor tree` in scope). We can solve this issue by using a local typeclass instance. In the case of `tree`:

```
Fixpoint fmap {A B : Type} (f : A -> B) (t : tree A) : tree B :=
  let _ := Build_Functor tree fmap in
  match t with Leaf => Leaf | Node x ts => Node (fmap f x) (fmap f ts) end.
```

Typeclass resolution will now consider the local instance `_ : Functor tree` when elaborating `fmap f ts`. Note that this stretches the limits of what the guard checker/termination checker is capable of accepting: we had to disable Agda's termination checker, and in the case of Rocq we had to help the guard checker by normalizing `fmap` before adding it to the global environment.

We do not expect alternative approaches to this problem to alter the conclusions of this experience report.