# Proxy-based small inversions and their automation

Pierre Corbineau, Basile Gros, Jean-François Monin

► To cite this version:

Pierre Corbineau, Basile Gros, Jean-François Monin. Proxy-based small inversions and their automation. 2026. hal-05469909

HAL Id: hal-05469909

https://hal.science/hal-05469909v1

Preprint submitted on 21 Jan 2026

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 CC BY 4.0 - Attribution - International License
# Proxy-based small inversions and their automation

Pierre Corbineau [x]

Univ. Grenoble Alpes, CNRS, Grenoble INP<fnref n="1" />, VERIMAG, 38000 Grenoble, France

Basile Gros [x]

Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000 Grenoble, France

Jean-François Monin [x]

Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000 Grenoble, France

## Abstract

Inversion reasoning is a frequently used proof-pattern when using proof assistants. It derives premises allowing the construction of an inductive object, by enhancing its elimination principle.

Several implementations of inversion already exist in Rocq, such as the **inversion** tactic or the **Equations library's dependent elimination** tactic. They rely heavily on the use of equality to perform replacement in the proof. In contrast, small inversion uses core mechanisms of type theory such as dependent pattern matching and large elimination in order to perform direct substitutions whenever possible rather than relying on intermediate equalities.

We present a variant of small inversion called *proxy-based small inversion*. We show that it is suitable for both proofs and dependent programming as it generates explicit terms that are intended to be more readable and explainable than those produced by Rocq's **inversion** or Equations' **dependent elimination**. This method consists in mapping an indexed inductive type into simpler inductive types, built in such a manner that the case analysis on objects of these simpler types performs inversion on the corresponding objects of the original inductive type. The creation of the simpler types can be described as a series of transformations on inductive types that are iterated until a suitable form is obtained.

The first contribution in this article is a general presentation of proxy-based small inversions. The second contribution is a definition and illustration of the different transformation steps. The third contribution describes the implementation of those transformations for Rocq inductive types using MetaRocq as a metaprogrammation framework.

**2012 ACM Subject Classification** Theory of computation → Interactive proof systems

**Keywords and phrases** Rocq, Dependent Programming, Inversion, Small Inversions, Metaprogram- mation

**Digital Object Identifier** 10.4230/LIPIcs.CVIT.2016.23

**Supplementary Material**

https://gricadgitlab.univ-grenoble-alpes.fr/proxy-based-small-inversions/types-2025-artifact

## 1 Introduction

Rocq (formerly known as Coq) [20] is an interactive proof assistant, used in particular to prove the correction of software and to verify mathematical proofs. It implements the Calculus of Inductive Constructions (CIC) [22] by allowing the definition of algebraic types and then function and properties on those types. Famous achievements realized in Rocq include the verification of the proof of the Four Color Theorem [9], its use as the basis of the certified C compiler CompCert [18], and more recently it was used to prove the number of steps of the fifth Busy Beaver [15].

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

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

<footnote n="1">¹ Institute of Engineering Univ. Grenoble Alpes</footnote>
## 23:2 Proxy-based small inversions and their automation

Reasoning by inversion [4] [19] is a proof scheme that deduces information about the premises of a hypothesis *H* from its conclusion. It is traditionally used to simplify interactive proofs by case analysis on *H*: only the cases that are compatible with the arguments in the type of *H* are selected and moreover, constraints on those arguments are propagated. In particular, “obviously” impossible situations are removed.

Inversion is most commonly used in Rocq through the application of dedicated tactics in the interactive development of proofs. However, we believe that inversion is also relevant to programming with dependent types as well, especially when the underlying terms are clear and legible enough to be written explicitly.

Several approaches to inversion have been implemented in Rocq, see Sections 2 and 3 for more details. We develop here a method called *proxy-based small inversions*, based on an idea sketched in [12]. We analyze and generalize this idea into a theoretical description of the process. Then we develop a systematic algorithm that implements the generation of intermediate objects that this method requires. This algorithm now covers most situations encountered in practice.

Our algorithm performs successive transformations of the abstract syntax tree (AST) representation of Rocq's functions and inductive types to generate new objects. The MetaRocq framework provide suitable features to carry out this task: obtaining AST representation for existing objects, performing computation on them, and defining new global objects reflected by the resulting ASTs.

The contributions described in this article are then:

- a general presentation of proxy-based small inversions;

- a definition and illustration of the different transformation steps involved in mechanizing this approach, including a formal exposition for specialisation, the most important among those transformations;

- a presentation of the implementation of those transformations for Rocq inductive types using MetaRocq as a metaprogrammation framework.

The rest of this paper is organised as follows. Section 2 reviews existing approaches to inversion, including previous versions of small inversions, without going into technical details. These are covered in Section 3. Our contributions are also clarified in Section 2. Section 4 details proxy-based small inversions and describes the different intermediate objects involved. Section 5 explains the concept of inductive type tranformations and describes the auxiliary tranformations used for generating proxy-based small inversions. Section 6 presents the main and most complex transformation, which is called the specialisation transformation. Our implementation using MetaRocq is discussed in Section 7. We conclude in Section 8.

## 2 Related work

The notion of inversion in Rocq is first discussed in [4], where two so-called naive algorithms are presented and discussed. The first one uses large elimination to generate inversion lemmas, similarly to the elimination lemmas that Rocq generates automatically when defining an inductive type. The second algorithm uses specific equalities to invert a given inductive object. We believe that the *inversion* tactic currently present in Rocq follows a similar approach to this second algorithm. It is extremely versatile and frequently used. However, it is quite complex, more so than what its only published description in [4] suggests. Its proof term generation is unpredictable: it produces subgoals cluttered with a seemingly random number of equality hypotheses and the generated proof-terms have a large size, with reduced readability. This can also be a problem in dependent programming, where inversion
is needed to define some functions. The body of those functions cannot be easily read and understood by a user, especially when importing definitions written by someone else. In addition, common cases in dependent programming lead to unsolvable issues, such as equality between dependent pairs that necessitates UIP. The unpredictability in terms generation also makes proof scripts sensitive to Rocq updates and small changes in the data structures involved in the proof.

The dependent elimination tactic, available in the Equations package [17], can also be used to perform inversion in interactive mode. It follows and improves upon the historical approach of adding constraints in the context of the pattern matching. The algorithm behind Equations is a refinement of the algorithm proposed by Goguen, McBride and McKinna [8] for dependent pattern matching. Dependent elimination uses classes to register and classify the decidability of some types in order to avoid an axiomatic UIP, and only requires it on types where it is needed and not provable. However, the terms still tend to be of large size, leading to difficulties when parsing functions defined with it.

Monin proposed a lightweight approach to inversion, called small inversions in [14] that avoid the aforementioned issues by performing inversion without cluttering the elimination predicate with equality constraints on the indices, using instead custom case-analysis and return types. The absence of equalities also obviates the need for UIP. Small inversions put emphasis on the transparency and small size of the proof term construction, to the cost of the full scope of the inversion tactic and the later dependent elimination. Though this approach has been able to demystify inversion and successfully handle predictability and size blowup that inversion suffered from, it still has modularity issues addressed in [13] in order to scale up to the big inductive relations defined in the CompCert project. The latter technique has also been used in other teams, for instance in the CH₂O project of Krebbers [10].

Some form of this early version of small inversions is implemented and improved within the elaboration mechanism of Rocq, though it remains undocumented. For example, it is triggered when using the refine tactic with dependent match case-analysis, where it can synthesise non-trivial elimination predicates.

In [12], Monin proposed a new approach to small inversions. Over the two pages of this extended abstract, it describes the partitioning of a family of types *R* into a finite disjunction of custom partial inductive types *R*<sub>ψ</sub>, and the definition of a map from *R* to those *R*<sub>ψ</sub>. Inversion is then obtained by applying this map on the premise (*r* : *R* *u*) to invert and then performing an ordinary pattern matching on the result. This approach is comparable to what Wadler calls *views* in the context of functional programming [21]. More precisely we construct a view on *R* based on an *indexed-first* presentation of *R*, following the terminology introduced in [5]). Additionally, this approach is shown to be suitable to a simple but powerful addition allowing us to perform a more advanced kind of inversions called dependent inversions. This heuristic description is accompanied by handcrafted examples.

What we give in this paper is a formal and general presentation of the method sketched in [12] together with its implementation. In order to broaden its scope to the case of multiple and deep patterns, we identify a series of transformations which can be composed in order to end up with the partial inductive types $R_{\psi}$ and the associated auxiliary functions. This analysis allows us to identify corner-cases of our approach and more precisely delimit the scope of our broadened method. The transformations that we have identified are the basis for a modular implementation using MetaRocq. This implementation automates the tedious derivation of the custom partial inductive types $R_{\psi}$ and associated functions for a broad class of inductive definitions.
23:4 Proxy-based small inversions and their automation

The small size of the proof terms created with this method leads to better readability and simpler debugging without specialised tools. This is why we are convinced that small inversions have their niche in the Rocq ecosystem in defining functions for dependent programming that are simple to read and reason about. The examples considered in the current paper are deliberately very basic, for explanatory purposes only. More advanced examples were mentioned in a recent extended abstract [1] and the interested reader can also consult the material provided online.<fnref n="2" />

There is no clear-cut comparison between the scope of those different approaches. In practice, small inversions and dependent elimination may fail in some simple situations where inversion is able to succeed, though the real advantage obtained is debatable (see more details in Section 4.3 below). On the other hand, use cases where inversion fails whereas small inversions succeeds were already identified in [13], and this still holds nowadays for proxy-based small inversions.

To conclude this section, technical details on the use of MetaRocq as a metaprogramming language for our implementation are given in [2].

3 Reasoning and programming using inversion in Rocq

Inversion reasoning typically consists in recovering the premises and constraints used to derive the proof of a given indexed inductive relation whose statement includes specific values for some indices. In the framework of programming with dependent types, by the Curry-Howard isomorphism, inversion consists in recovering the components used to construct a given piece of data whose type includes specific values for some indices. Note that in the context of interactive proof development, inversion is commonly carried out by dedicated tactics, whereas explicit terms are arguably more appropriate in programming.

Those inductive relations or datatypes are defined as inductive types, which are types whose inhabitants are entirely described by a finite set of generating functions, called constructors. Inductive types can represent sets of objects like natural numbers or Boolean values, populating the sorts Type (including Set), or they can be logical propositions, populating the sort Prop. They can be indexed by other types, in particular other inductive types. Those indices are used to constrain the type of a given inductive object, and the different constructors that can generate it.

Inductive types have an “analytic” property of constructors which allows case analysis on the objects populating an inductive type. This property is also the basis of inversion reasoning in Rocq, it is used simultaneously on both the property and its indices.

Non-dependent inversion obtains the arguments and objects used to derive the proof of a given indexed inductive relation.<fnref n="3" /> In addition, dependent inversion obtains the general form (in Rocq: the constructor with its arguments) used to derive the proof of that relation.

As an example, here is the type for a finite set with cardinality *n*, as defined in Rocq's standard library.<fnref n="4" />

Inductive Fin_t : N → Set :=
| F1 : ∀ n : N, Fin_t (S n)
| FS : ∀ n : N, Fin_t n → Fin_t (S n).

<footnote n="2">² https://gricad-gitlab.univ-grenoble-alpes.fr/proxy-based-small-inversions/types-2025-artifact</footnote>

<footnote n="3">³ For simplicity we retain in the sequel the word relation coming from the traditional use of inversion in proofs. This is actually a data type in the example to follow, which is devoted to programming with dependent types.</footnote>

<footnote n="4">⁴ In Rocq, the type's name is *t*, and can be noted *Fin.t* depending on how it was imported. For the clarity of our examples, we have renamed it *Fin_t* here.</footnote>
The type Fin_t is indexed by its cardinality. F1 n represents the first element in a set of n + 1 elements, and FS injects a set of n elements into a set of 1 + n elements.

The other example that we will use sporadically in this article is a “less than or equal to” relation on Peano natural numbers considered in [7] as advantageous compared to that of the standard Rocq library.

Inductive le2 : N → N → Prop :=
| L0 : ∀ m, le2 0 m
| LS : ∀ n m, le2 n m → le2 (S n) (S m).

To illustrate the different ways to invert an indexed inductive type in Rocq, we will use
the previously defined finite enumerated set, and try to define a function Fin_swap that
takes an element from a set of cardinality 2 and returns the other element. Its typing is

Fin_swap : Fin_t 2 → Fin_t 2.

We could as well consider a similar and more general function defined on sets with at least
two elements, of type ∀ n, Fin_t (2+n) → Fin_t (2+n), but the more restrictive typing
above is better suited for our illustrative purposes.

3.1 The destruct tactic

With a basic and naive use of destruct on x : Fin_t 2, we get a goal of Fin_t (S n') for a
generic n' that is not present in the original x. Indeed, Rocq tries to build a term in Fin_t 2
that is the result of a pattern-matching on x, i.e., with the following shape:

match x in Fin_t n return ?P n with
| F1 n' ⇒ ( ?term1 : ?P (S n'))
| FS n' j ⇒ ( ?term2 : ?P (S n'))
end

In this term, the unknown variable ?P is called the elimination predicate<fnref n="5" /> and it should be
chosen such that P 2 = Fin_t 2. The unification algorithm chooses P = Fin_t which means
the branches in the pattern matching should have type P (S n') = Fin_t (S n'). We are left
trying to build term1 and term2 with type Fin_t (S n') where n' is a fresh variable. We did
indeed lose the constraint n' = 1 during the process.

Here, note that the algorithm could have chosen P = λ_ ⇒ Fin_t 2 instead and it
would have succeeded, but this solution cannot be generalized to a Fin_swap of type ∀ n,
Fin_t (2+n) → Fin_t (2+n).

Two options can be considered to perform inversion using dependent case-analysis. The
first is to change the elimination predicate P from the default one used by destruct to a
custom one suitable for inversion reasoning. This is the choice made for the inversion tactic
of Rocq, dependent elimination and for the first version of small inversions [14]. A second
option is to change the object on which destruct is applied, as chosen for proxy-based small
inversions.

3.2 The inversion tactic and Equations' dependent elimination

The Rocq inversion tactic adds equalities and case analyses in the context to constrain
possible values and to manage impossible cases. Equations' dependent elimination follows

<footnote n="5">⁵ Here again, the terminology *elimination predicate* comes from the traditional use of inversion in proofs.</footnote>
23:6 Proxy-based small inversions and their automation

225

226

227

the same approach, but using decidability to reduce UIP needs. They are very versatile and easy to call. Here, the addition of equalities such as $n = 1$ provides the missing link in the elimination predicate, in order to keep the information on the cardinality (2) of $x$.

228

3.3 Introducing elimination proxies

229

230

231

Rather than synthetising ad-hoc elimination predicates to perform direct elimination of the object to be inverted, later methods (such as in [12]) split the inversion process into two separate steps:

232

233

234

■ First, the components of the inverted object are packaged inside an intermediate construct, which we will call the proxy. The proxy type and the proxy mapping function only need to be defined once.

235

236

237

■ Then, the proxy is subjected to a case-analysis with the original intended elimination predicate P. This step only uses the basic Rocq pattern-matching with only minimal elaboration, either as an explicit term or as the result of the *destruct* tactic.

238

239

240

241

242

In this family of small inversion techniques, the repackaging of inversion products into an intermediate construct cannot be currently recognized as structurally smaller by the syntactic guard condition for structural recursion in Rocq. However, in some cases we are able to recover recursion by performing structural induction on an index such as $n$ for $Fin_t n$ rather than on the object in $Fin_t n$.

243

244

245

246

247

Other techniques beyond our scope are needed when the termination argument is not index-structural. To this effect, special small inversions called *small projections* were introduced in the Braga method [11], where we have a specific projection for each component. Additionally, one of the motivations for dependent proxy-based small inversions sketched in [12] was to provide an additional convenient mechanism for reasoning about such recursive functions.

248

4 Proxy-based small inversions

249

250

251

252

253

To summarise our approach, we derive an auxiliary inductive type — called *partial inductive type* — $R_\psi$ for each pattern $\psi$ occurring in conclusions of the type $R$ to be inverted. The constructors of $R_\psi$ mimic the corresponding ones of $R$. Then, in order to invert a term $(r : R \vec{u})$, where the arguments $\vec{u}$ are specific enough, we perform a pattern-matching on a proxy of $r$ of type $R_\psi$, where $R_\psi$ is determined from $\vec{u}$.

254

255

256

257

More precisely, we build a syntactic partition of $R$ into partial inductive types $R_\psi$ depending on the syntactically decidable patterns $\psi$ of one or more of the inductively typed indices of $R$, called *pilot indices*. The partial inductive types $R_\psi$ are systematically derived from $R$ as follows:

258

259

■ The components of the constructors of $R$ are left unchanged in their counterpart in $R_\psi$, including recursive occurrences of $R$; therefore, partial inductive types are not recursive.

260

261

■ Information in the indices that was to be preserved for pattern matching is stored as polymorphic parameters of $R_\psi$ which the elimination predicate does not generalise over. We define the *proxy type* as a function mapping targetted index patterns to the corresponding $R_\psi$. It provides the return type of the *proxy function* to be applied to objects of the original type $R$: the proxy function maps each constructor of $R$ to the corresponding constructor of the respective $R_\psi$. By performing a pattern-matching on the object returned by the proxy function we get an inversion on the proxied object.

262

263

264

265

266

267

268

The separation of an inductive type into partial inductive types — called *specialisation* — can be carried out recursively on previously defined partial inductive types, to allow for
small inversion on multiple indices and with nested patterns.

One of the features of proxy-based small inversions is that once the partial inductive types and proxy function are defined, inversion can be performed as many times as necessary by simple pattern matching on the result of the application of the proxy function to the terms to be inverted (or, in interactive mode, by using the `destruct` tactic) without having to redefine the previously mentioned objects.

## 4.1 Example

For `Fin_t` we have just one index (the cardinality, of type $N$). It is relevant to consider it as a pilot index since, in the possible conclusions of `Fin_t`, it has the constructed shape $S n$.

The first partial inductive type for `Fin_t` selects the cases where the pilot has this shape; as said above, it is parameterised by $n$ and its components are the same as in `Fin_t` so we get:

Inductive $Fin_S (n : N) : Type :=$

| isF1 : Fin_S n

| isFS (x : Fin_t n) : Fin_S n.

Intuitively, `Fin_S` restricts the possible values of the number of elements of `Fin_t` to a successor $S n$; the $x$ component in its second constructor has then the type `Fin_t n`.

In order to define `Fin_proxy_type` below, we also need to consider the complement of this pattern, that is, the case where the cardinality is 0. We call it `Fin_0` and, as there are no constructors of type `Fin_t 0`, there are consistently no constructors for `Fin_0`.

Inductive $Fin_0 : Type := .$

Equivalently, we can reuse a type of the standard Rocq library:

Definition $Fin_0 := Empty_set.$

The proxy type and the proxy itself for `Fin_t` are then:

Definition $Fin_proxy_type (n:N) : Type :=$

match n with 0 ⇒ Fin_0 | S m ⇒ Fin_S m end.

Definition $Fin_proxy (n:N) (x : Fin_t n) : Fin_proxy_type n :=$

match x in Fin_t n' return Fin_proxy_type n' with

| F1 n' ⇒ isF1 n'

| FS n' x ⇒ isFS n' x

end.

Recall that inversion makes sense when we need to analyse some $x$ of type `Fin_t n`, where $n$ is (or reduces to) a constructor applied to arguments, say 0, 1, 2, (S i)... Applying `Fin_proxy` to such an $n$ and $x$ triggers a computation of the corresponding return type, by case analysis on $n$. Then, a pattern-matching on `(Fin_proxy n x)` boils down to a pattern-matching on something of type `Fin_0`, or `Fin_S` applied to a subterm of $n$, so that we get the desired inversion.

Here is how we interactively define `Fin_swap` using proxy-based small inversions. We can also define it directly, as shown below for `Fin_3vo`.

Definition $Fin_swap : Fin_t 2 \to Fin_t 2.$

Proof.
23:8 Proxy-based small inversions and their automation

320

intro x.

321

destruct(Fin_proxy _ x) as [|x'|].

322

– exact (FS F1).

323

– destruct (Fin_proxy _ x') as [ | x''].

324

— exact F1.

325

— destruct (Fin_proxy _ x'').

326

Qed.

328

Note that the last elimination doesn't yield any more proof obligations. The object inverted `x"` has type `Fin_t 0`, which is mapped by the proxy type to `Fin_0`, an empty type.

329

330

## 4.2 Propagation of constraints

331

As a nice consequence of our approach, terms captured by free variables in the course of this pattern-matching are propagated as usual to all occurrences of those variables in the elimination predicate, for free, which explains why additional equalities needed in other inversion techniques are no longer part of the problem. Moreover, such equalities are destined to be eliminated very quickly<fnref n="6" />. As equality elimination is nothing more than a particular pattern-matching in our type theoretic framework, we can say that a small inversion replaces a series of ad hoc pattern-matching steps by a single natural pattern-matching.

332

333

334

335

336

337

338

For example, let us prove $n = 0 \lor n = 1$ from a hypothesis $L : le2 n 1$. Here are the partial inductive types and the proxy type when the pilot index is the second index of `le2`.

339

340

Inductive le2_0 : $\mathbb{N} \to \text{Prop} :=$

341

| L0_0 : le2_0 0.

342

Inductive le2_S (m:$\mathbb{N}$) : $\mathbb{N} \to \text{Prop} :=$

343

| L0_S : le2_S m 0

344

| LS_S : $\forall n$, le2 n m $\to$ le2_S m (S n).

345

346

Definition le2_proxy_type (n m : $\mathbb{N}$) : Prop :=

347

match m with 0 $\Rightarrow$ le2_0 n | S m $\Rightarrow$ le2_S m n end.

348

349

In our exemple, the pilot index is instantiated by `(S 0)`, so that we get `(le2_S 0 n)` as the type of the proxy. We have then two cases. The first case, provided by `(L0_S 0)`, constrains `n` to be 0, and we can prove `0 = 0`. The second case, provided by `(LS_S 0)`, constrains `n` to be the successor of some `n'` with `L' : le2 n' 0`, and we can prove `S n' = 1` by a small inversion on `L'` — with a proxy of type `(le2_0 0)`. No additional equality and rewriting steps has occurred.

350

351

352

353

354

355

356

357

## 4.3 A questionable limitation

358

When inverting objects of type `R`, one needs to consider the possible values taken by the pilot indices in the conclusion of each constructor in the inductive definition of `R`. Our method supports only the situations where the possible values of the pilot are variables or rigid patterns, i.e., terms that are built by possibly nested applications of inductive constructors to variables. More complex situations, where the type of the object to be inverted would,

359

360

361

362

<footnote n="6">⁶ In practice `inversion` is commonly followed by `subst`.</footnote>
after reduction, involve applications of functions which are not constructors, even if they are
injective (e.g., $\lambda n \Rightarrow n + 2$, in contrast with $\lambda n \Rightarrow 2 + n$), are currently not in our scope.

Note that this restriction is not an obstacle to the tactic **inversion**. For instance,
the relation `le2` could be written with the second clause concluding to `le2 (n + 1) (m + 1)`
instead of `le2 (S n) (S m)`. A hypothesis L : `le2 n 1` cannot currently be exploited by a small
inversion for proving `n = 0 ∨ n = 1` with this version of `le2`, whereas **inversion L** succeeds.
However the second goal obtained cannot be easily managed — it requires either additional
algebraic properties of addition, or elementary steps based on injectivity and discrimination;
but all this work is precisely for free when we have a constructor such as `S` instead of a
function such as `_ + 1`. The trouble observed can be interpreted as a symptom that, in some
way, the formalisation used should be questioned. Incidentally, we observe that **dependent
elimination** fails as well on the above goal. In practice, Rocq users spontaneously tend
to use inversion only in the presence of rigid patterns. Hence, at first sight, the advantage
provided by this feature of **inversion** should not be overestimated.

## 4.4 Dependent inversion

An especially interesting use-case of proxy-based small inversions, compared to other inversion methods, seems to be in dependent programming. We get code based on simple pattern matching, albeit on a different type than the original inductive type targeted by an inversion. This allows for easier proofs on functions defined with inversion, and even allows for directly defined functions with dependent pattern matching rather than using interactive mode.

The very point of programming with dependent types is to define functions whose return type depends on their input, which is beyond the scope of the previously described technique simply because the returned *type* of the proxy does not take the inverted object itself into account. To this effect, it is enough to complete the proxy type and the partial inductive definitions used in its definition by an additional argument corresponding to the inverted object. The differences with the previous non-dependent partial inductive types and proxy function are highlighted in red in our example.

Inductive Fin_0 Dep : Fin_t 0 → Type ::= .

Inductive Fin_S dep (n: N): Fin_t (S n) → Type ::=
| isF1 dep : Fin_S dep n F1
| isFS dep x : Fin_S dep n (FS x).

Definition Fin_proxy_type Dep (n:N) : Fin_t n → Type ::=
match n with
| 0 ⇒ Fin_O dep
| S m ⇒ Fin_S dep m
end.

Definition Fin_proxyiser (n:N) (x : Fin_t n) : Fin_proxy_type dep n x :=
match x as x' in Fin_t n' return Fin_proxy_type dep n' x' with
| F1 n' ⇒ isF1 dep n'
| FS n' x ⇒ isFS dep n' x
end.

Then we can define a function mapping each member *x* of a finite set of cardinal 3 to a value
whose type depends on *x*.
23:10 Proxy-based small inversions and their automation

411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429

Definition Fin_3Rect

(P : Fin_t 3 → Type)

(p1 : P F1)

(p2 : P (FS F1))

(p3 : P (FS (FS F1)))

(x : Fin_t 3) : P x :=

match Fin_proxyDep 3 x with

| isF1Dep _ ⇒ p1

| isFSDep _ x ⇒

match Fin_proxyDep 2 x with

| isF1Dep _ ⇒ p2

| isFSDep _ x ⇒

match Fin_proxyDep 1 x with

| isF1Dep _ ⇒ p3

| isFSDep _ x ⇒

match Fin_proxyDep 0 x with end

end end end.

430

5 Transformations and their combination

To facilitate the description and the automation of proxy-based small inversions, we have decomposed the synthesis of the different objects involved into steps called *transformations*, that transform an input inductive type into either a new inductive type or multiple inductive types, while building pieces of the final proxy type and proxy. The transformations we use are, in order of usage :

431

432

433

434

435

1. Derecursivation, transforming recursive components of an inductive type into components having the original inductive type.

436

437

2. Deparameterisation, changing the parameters of the inductive type into indices.

438

3. A special transformation that is applied to make the inversion dependent (see 4.4).

439

4. Specialisation, that creates partial inductive types; this transformation can be repeated several times for nested or multiple patterns on indices.

440

441

5. Parameterisation, transforming indices into parameters whenever possible.

442

The first two transformations allow us to maintain two invariants in the following transform-
ations, that are particularly useful in the specialisation steps: the inductive type considered
does not have any parameter nor does it have any recursive calls. All transformations
except for parameterisation keep the original order of indices in order to respect possible
dependencies.

443

444

445

446

447

Each transformation also produces functions that, composed together, create the proxy
type and proxy functions. One of those functions is a part of the proxy type. Its type is the
arity of the original inductive type. It takes in as arguments the values of the indices of the
original inductive, and outputs the transformed inductive type applied to those arguments. In
the case where multiple inductive types are created, it selects which one to output, according
to the patterns considered.

448

449

450

451

452

453

The other functions perform a similar role for the constructors of the inductive type.
For each constructor of the input inductive type, there is a function that maps it to the
corresponding constructor or constructors created by the transformation. Those are combined
with a proxy0 that performs the initial case analysis into different constructors.

454

455

456

457
Definition proxy_type0 := λ (n : N) ⇒ Fin_t n.

Definition proxy0 :=
  λ (n : N) (r : Fin_t n) ⇒
    match r in Fin_t n' return proxy_type0 n' with
      | F1 n      ⇒ F1 n
      | FS n x   ⇒ FS n x
  end.

Each transformation will substitute Fin_t in proxy_type0, and F1 and FS in proxy0.

The remainder of this section is dedicated to transformations numbered 1, 2, 3 and 5 above, while transformation 4 will be explained later in Section 6. Those transformations leave the structure of the inductive mostly intact, and the proxies generated are trivial, a simple one-to-one mapping from old to new constructors.

## 5.1 Derecursivation

We already remarked that the partial inductive types introduced in our approach are not recursive. Inversion is actually a kind of (somewhat subtle) reasoning by case analysis, it is not concerned with the recursion of inductive types. It is even detrimental to keep recursion while proceeding through specialisation, because of the intricacy of its internal representation.

In Rocq, most references to parameters, arguments, variables etc... are internally represented by bound variables. Recursive occurrences of an inductive in its own definition are also represented with such variables. Internally, derecursivation transforms the bound variables of the recursive occurrences into global reference to the name of the inductive type. On our example this yields:

Inductive Fin_t' : N → Set :=
| F1' : ∀ n : N, Fin_t' (S n)
| FS' : ∀ n : N, Fin_t n → Fin_t' (S n).

The recursive occurrence in the type of FS' becomes a reference to the original inductive Fin_t.

## 5.2 Deparameterisation

The presence of parameters can also cause complications when proceeding through specialisation. Therefore, they are changed into indices and this significantly simplifies later transformation steps.

To illustrate the idea, the deparameterisation of Rocq lists would yield:

Inductive list : Type → Type :=
| nil : ∀ A : Type, list A
| cons : ∀ A : Type, A → list A → list A.

## 5.3 Transformation dedicated to dependent inversion

As seen in 4.4, dependent inversion is obtained by adding to the partial inductive types an index whose type is the original inductive type. In each constructor, this index is instantiated by a term which is an application of the original constructor to its components.
23:12 Proxy-based small inversions and their automation

The proxy type and the proxy functions have to be modified in order to take this new index into account. Apart from that last point, it is entirely possible to treat the addition of dependence as the other transformations. Other transformations (and in particular specialisation) need not be aware of its presence.

5.4 Parameterisation

Inductive types with parameters behave generally better than those with indices instead. When performing case analysis on an inductive object, parameters keep the value given as input, while the case analysis generalises indices to all possible values. It is the reason `destruct` does not properly perform inversion, as was discussed in section 3.1.

There are two reasons we use parameterisation:

- If we transform a polymorphic parameter into an index during deparameterisation, we need to transform it back into a parameter to have a pattern matching on a monomorphic type rather than a polymorphic type.

- If we have indices that come from variables in the patterns of a pilot index, as said earlier we want to transform them into parameters as much as possible.

To be transformable into a parameter, an index must follow two conditions:

1. In the arity of the inductive type, the index type must be only dependent on other parameters.

2. In the conclusion of all constructors, the index value must be a constructor argument. If an index fulfills these conditions, we transform it into a parameter before checking further indices. Otherwise it is skipped. In some cases this means reordering the indices before turning the first one into a parameter.

For example, if we take the second partial inductive type created for the dependent small inversion in `Fin_t`.

Inductive Fin_S Dep : ∀ (n:N), Fin_t (S n) → Type :=
| isF1Dep n : Fin_S Dep n F1
| isFSDep n x : Fin_S Dep n (FS x).

The first index, of type $N$ respects the two conditions mentioned above: it is not dependent, and in the conclusion of both `isF1 Dep` and `isFS Dep` it has the value of the argument $n$ of the corresponding constructor. As such, it can be parameterised.

The second index of type `Fin_t` (`S n`) fails both conditions. It depends on the first index, and it has the value of a constructor in both conclusions.

With the first index begin reparameterised, we get:

Inductive Fin_S Dep (n:N) : Fin_t (S n) → Type :=
| isF1 Dep : Fin_S Dep n F1
| isFS Dep x : Fin_S Dep n (FS x).

Now that the first index is a parameter, the second index does respect the first condition, begin only dependent on a parameter. However, it still fails the second and must therefore stay an index.

6 The specialisation transformation

Specialisation consists in the construction of the partial inductive types, i.e. specialised versions of the original inductive type for relevant patterns of a single pilot index. This
transformation is iterated if we want an inversion piloted by several indices, or using a deep pattern on at least one index. The type of the proxy type is the (parameter-free) arity of the inductive type given as input. The proxy type itself is defined by a case analysis on the pilot index and returns the partial inductive type corresponding to the pattern considered.

In turn, the proxy maps a constructor of the original inductive to the corresponding constructor in one or several of the partial inductive types; if several partial inductive types are concerned, an additional case analysis on the pilot index is performed (see 6.4.1).

## 6.1 Notations and naming convention

We start with some conventions and notations to designate the different components of the original inductive type, thereafter called the *inductive relation*, and of the type of the pilot index, shortened as the *pilot type*.

### 6.1.1 The inductive relation

We consider a parameter-free inductive type Relation.

Inductive Relation : $\forall (\vec{a} : \vec{A}), S :=$

$$ | C_1 : \forall (\vec{x_1} : \vec{X_1}), \text{Relation } \vec{\alpha_1} $$

⋮

$$ | C_i : \forall (\vec{x_i} : \vec{X_i}), \text{Relation } \vec{\alpha_i} $$

567

Its attributes are:

568 ■ its indices $(\vec{a}:\vec{A})$,

569 ■ its sort $S$ that can be Prop or Type; SProp seems to work too, as long as the inversion is used to prove a property in SProp,

570 ■ its constructors $C_i$, with arguments $(\vec{x_i} : \vec{X_i})$,

571 ■ the $\vec{\alpha_i}$ which are terms instantiating the indices $\vec{a}$ in the conclusion of the constructor $C_i$.

572 Finally, the arity of Relation is $\forall (\vec{a}:\vec{A}), S$ and each constructor $C_i$ has the conclusion Relation $\vec{\alpha_i}$.

573 Example: after derecursivation of Fin_t, we want to specialise Fin_t' defined as follows:

574 Inductive Fin_t' : $\forall n:N, Set :=$

575 | F1' (n : N) : Fin_t' (S n)

576 | FS' (n : N) (e:Fin_t n) : Fin_t' (S n).

577

Relation is Fin_t, $\vec{a}$ is (n), $S$ is Set,

580 C₁ is F1, $\vec{x_1}$ is (n), $\vec{\alpha_1}$ is (S n),

581 C₂ is FS, $\vec{x_2}$ is (n,e) and $\vec{\alpha_2}$ is (S n).

582

For the less-or-equal relation on natural numbers we have, after derecursivation and deparameterisation:

583 Inductive le2' : $\forall n m : N, Prop :=$

584 | L0' : $\forall m, le2' 0 m$

585 | LS' : $\forall (n m : N)(l : le2 n m), le2' (S n) (S m)$.

586

Relation is le2', $\vec{a}$ is (n,m), $S$ is Prop,

592 C₁ is L0', $\vec{x_1}$ is (m), $\vec{\alpha_1}$ is (0,m),

593 C₂ is LS', $\vec{x_2}$ is (n,m,1) and $\vec{\alpha_2}$ is (S n, S m).

594
23:14 Proxy-based small inversions and their automation

595

## 6.1.2 The pilot type

The proxy type performs a large elimination on a pilot index of Relation. Its type must then
have an informative sort: Set or Type.

$$
\begin{align*}
& \text{Inductive Pilot } (\vec{q} : \vec{Q}) : \mathcal{T} := \\
& \quad | D_1 : \forall (\vec{y}_1 : \vec{Y}_1), \text{ Pilot } \vec{q} \\
& \quad \vdots \\
& \quad | D_j : \forall (\vec{y}_j : \vec{Y}_j), \text{ Pilot } \vec{q}
\end{align*}
$$

Pilot is the type of the pilot index a_κ that guides the targeted inversion, where κ is the
position of the pilot index in the arity of Relation (see Section 6.1.1). Its attributes are :

604 its parameters $(\vec{q} : \vec{Q})$,

605 no indices (this is a current simplifying hypothesis, that will be discussed in Section 7.4)

606 its sort $\mathcal{T}$ that can be Set or Type,

607 its constructors $D_j$ with arguments $(\vec{y}_j : \vec{Y}_j)$.

The arity of Pilot $\vec{q}$ is then just the sort $\mathcal{T}$.

Both of our previous examples use the Peano natural numbers as their only index. Here
we recall the definition of $\mathbb{N}$ and the corresponding notations as a pilot type.

$$
\texttt{Inductive N: Set} := \texttt{0 : N} | \texttt{S (n:N)} : \texttt{N}.
$$

614 Pilot is $\mathbb{N}$, $\vec{q}$ is $\emptyset$,

615 $D_1$ is $0$, $\vec{y}_1$ is $\emptyset$, $D_2$ is $\mathcal{S}$ and $\vec{y}_2$ is $n$.

6.2 The partial inductive types

617
618
619
The partial inductive types can intuitively be seen as a partition of the original inductive type. Each element with a given shape of the pilot is canonically mapped to an element of the corresponding partial inductive type. This mapping is performed by the proxy function.

To partition the inductive type of the relation, the shapes considered in this work follow
the elimination scheme of Pilot: they are the primitive patterns $\psi j = D_j \vec{y}_j$ formed by the
application of a constructor of the pilot type $D_j$ to as many fresh variables $\vec{y}_j$ as needed to
form an inhabitant of the type Pilot. The partial inductive type corresponding to $\psi j$ is called
Relation\_D_j.

Each constructor $C_i$ has an instantiated pilot $\alpha_{i,\kappa}$ that is said to be *compatible* with the pattern $\psi j$ if one of the two following conditions is true:

1. $\alpha_{i,\kappa} = D_j \overrightarrow{z_j}$, where $\overrightarrow{z_j}$ are terms with free variable in the arguments $\overrightarrow{x_i}$ of $C_i$. We define the substitution $\sigma_j = \{\overrightarrow{y_i} \mapsto \overrightarrow{z_j}\}$ such that

$$
\alpha_{i,\kappa} = D_j \overrightarrow{z_j} = D_j \overrightarrow{y_j} \sigma_j = \psi_j \sigma_j
$$

2. $\alpha_{i,\kappa} = x_{i,\theta}$, where the variable $x_{i,\theta}$ is one of the argument of the constructor $C_i$. We define the substitution $\sigma_j = \{x_{i,\theta} \mapsto D_j \vec{y}_j\}$ such that

$$
\alpha_{i,\kappa} \sigma_j = x_{i,\theta} \sigma_j = D_j \vec{y}_j = \psi_j
$$

The partial inductive type Relation\_D_j is defined by gathering all constructors C_i\_D_j
which mirror a constructor C_i whose instantiated pilot α_{i,κ} is compatible with ψ_j. Its general
form is:

$$
\texttt{Inductive Relation\_D_j: } \forall \vec{a}_{<\kappa} \vec{y}_j, \text{ let } \mathbf{a}_{\kappa} := \psi j \text{ in } \forall \vec{a}_{>\kappa}, \mathbf{S} :=
$$
$$631 \quad | \quad C_{i\_D_j}: \quad \forall \vec{x}_i, \text{ let } \vec{y}_j := \vec{z}_j \quad \begin{array}{@{}c@{}} \text{in} \\ \text{Relation\_D}_j \xrightarrow{\alpha_{i,<\kappa}} \vec{y}_j \end{array} \quad \text{when } \alpha_{i,\kappa} = D_j \vec{z}_j$$

$$633 \quad | \quad C_{i\_D_j}: \quad \forall \vec{x}_{i,<\theta}, \forall \vec{y}_j, \text{ let } x_{i,\theta} := \psi_j \quad \begin{array}{@{}c@{}} \text{in} \\ \text{Relation\_D}_j \xrightarrow{\alpha_{i,<\kappa}} \vec{y}_j \end{array} \quad \forall \vec{x}_{i,>\theta}, \\ 634 \quad | \quad \forall \vec{x}_{i,>\theta}, \forall \vec{y}_j, \text{ let } x_{i,\theta} := \psi_j \quad \begin{array}{@{}c@{}} \text{in} \\ \text{Relation\_D}_j \xrightarrow{\alpha_{i,>\kappa}} \vec{y}_j \end{array} \quad \text{when } \alpha_{i,\kappa} = x_{i,\theta}.$$

It is non-recursive and parameter-free, its indices are the indices of Relation where the pilot index has been replaced by the (possibly empty) sequence of variables of the pattern $\psi_j$, and where the occurrences of the pilot index in subsequent dependent indices have been replaced by $\psi_j$. The let in constructs are necessary if further indices depend on the pilot index.

### 6.2.1 Examples

For Fin_t, described earlier, the only possible inversion patterns are the constructors of the $\mathbb{N}$ type. Here are its partial inductive types:

```
643   Inductive Fin_0 : Type ::=
644   Inductive Fin_S : N → Type ::=
645     | isF1 (n:N) : Fin_S n
646     | isFS (n:N) (x : Fin_t n) : Fin_S n.
647   648
```

The partial inductive types presented here is slightly different from the one presented in section 4, because parameterisation has yet not been performed.

For le2, we choose to consider the second index as the pilot index. The two constructors of le2 each show a different case of the compatibility condition.

```
653   Inductive le2_0 : N → Prop ::=
654   | L0_0 : le2_0 0.
655   Inductive le2_S : N → N → Prop ::=
656     | L0_S (m:N) : le2_S 0 m
657     | LS_S : ∀ n m, le2 n m → le2_S (S n) m.
658   659
```

## 6.3 Proxy type

By construction, the proxy function will be a case analysis, where each branch may return an element from a different partial inductive type. We build the proxy type as a common return type for the case analysis performed by the proxy. It proceeds in turn by case analysis on the pilot, returning the suitable partial inductive type corresponding to basic patterns of the pilot type. The proxy type has the same arity as Relation and is meant to be isomorphic to it.

```
667   Definition Relation_proxy_type: ∀ (\vec{a}:\vec{A}), S :=
668     fun \vec{a} \Rightarrow
669       match \vec{a}' as psi return
670         let \vec{a} \Rightarrow := \vec{a}' \text{ in}
671         let \vec{a}_\kappa := \psi \text{ in}
672         ∀(\vec{a} \Rightarrow : \vec{A} \Rightarrow), S with
673       | D_j \vec{y}_j \Rightarrow
674         let \vec{a} \Rightarrow := \vec{a}' \text{ in}
675         let \vec{a}_\kappa := D_j \vec{q} \vec{y}_j \text{ in}
```
23:16 Proxy-based small inversions and their automation

676 fun ( $\overrightarrow{a}_{>\kappa}: \overrightarrow{A}_{>\kappa}$ ) $\Rightarrow$
677 Relation_D$_j$ $\overrightarrow{a}_{<\kappa}$ $\overrightarrow{y_j}$ $\overrightarrow{a}_{>\kappa}$
678 end.

679 For example, here is the proxy type for Fin_t:

680 Definition Fin_proxy_type (n:N) : Type :=
681 match n with
682 | 0 ⇒ Fin_0
683 | S m ⇒ Fin_S m
684 end.

687 And here is the proxy type for le2.

688 Definition le2_proxy_type (n m : N) : Prop :=
689 match m with
700 | 0 ⇒ le2_0
701 | S m ⇒ le2_S m
702 end.

6.4 Proxy function

695 As explained at the beginning of section 5, the proxy function maps an object of type Relation $\overrightarrow{a}$ to its mirror element in the corresponding partial inductive type. The signature of the proxy is:

699 Relation_proxy($\overrightarrow{a}$ : $\overrightarrow{A}$) : ∀ r : Relation $\overrightarrow{a}$ , Relation_proxy_type $\overrightarrow{a}$ .

700 Initially, it has the value:

701 Definition Relation_proxy_0 ($\overrightarrow{a}$ : $\overrightarrow{A}$) (r : Relation $\overrightarrow{a}$) : Relation_proxy_type $\overrightarrow{a}$ :=
702 match r in Relation $\overrightarrow{a}$ with
703 | C$_i$ $\overrightarrow{x_i}$ ⇒ [C$_i$] $\overrightarrow{x_i}$ end.

704 The proxies generated by the specialisation will replace the [Cᵢ] on the right side of the arrow<fnref n="7" />.

705 The compatibility hypothesis for the constructor Dⱼ can be either of the two following cases:

706 1. When $\alpha_{i,\kappa} = D_j \overrightarrow{z_j}$ the proxy will be the following replacement:

707 [C_i] $\rightsquigarrow$ $\lambda(\overrightarrow{x_i} : \overrightarrow{X_i}) \Rightarrow C_i \_ D_j \overrightarrow{x_i}$

708 2. When $\alpha_{i,\kappa} = x_{i,\theta}$, further case analysis $x_{i,\theta}$ is needed to select the appropriate partial inductive type. This pattern matching proceeds as follows:

710 [C_i] $\rightsquigarrow$ $\lambda(\overrightarrow{x_i} : \overrightarrow{X_i}) \Rightarrow \mathbf{match}$ $x_{i,\theta}$ as $x_{i,\theta'}$ return Relation_proxy_type $\overrightarrow{a}$ {a$_\kappa \mapsto x_{i,\theta'}$} with
| D_j $\overrightarrow{z_j}$ $\Rightarrow$ C_i \_ D_j $x_{i,<\theta}$ $\overrightarrow{z_j}$ $x_{i,>\theta}$

<footnote n="7">⁷ The transformations before specialisation do not change the arguments of the constructors, so we can ignore their effect on the proxy.</footnote>
### 6.4.1 Examples

Fin_t is an example of the first situation: each of its two constructors has a pattern of depth 1, namely the constructor S applied to its argument, which is the variable n. As a reminder, here is the definition of Fin_t:

Inductive Fin_t : N → Set ::=
  | F1 : ∀ n : N, Fin_t (S n)
  | FS : ∀ n : N, Fin_t n → Fin_t (S n).

As a reminder, the code for the initial proxy, before transformations, is:

Definition proxy0 :=
  λ (n : N) (r : Fin_t n) ⇒
    match r in Fin_t n' return proxy_type0 n' with
  | F1 n' ⇒ F1 n
  | FS n x ⇒ FS n x
  end.

In Fin_proxy0 we then substitute the constructors of Fin_t by the following functions:

Fin_proxy_F1 (n:N) : Fin_proxy_type (S n) := isF1 n
Fin_proxy_FS (n:N) (x : Fin_t n) :
  Fin_proxy_type (S n) := isFS n x

Definition Fin_proxy (n:N) (x : Fin_t n) : Fin_proxy_type n :=
match x in Fin_t n' return Fin_proxy_type n' with
| F1 n' ⇒ isF1 n'
| FS n' x ⇒ isFS n' x
end.

In our second example, le2 has two constructors, each presenting a different case.

Inductive le2 : N → N → Prop ::=
  | L0 : ∀ m, le2 0 m
  | LS : ∀ n m, le2 n m → le2 (S n) (S m).

We have chosen the second index to be the pilot index. In the first constructor L0, the pilot index has for value a variable. It is therefore compatible with all constructors of N. Each partial inductive will have a constructor corresponding to L0. The second constructor LS however is only compatible with the pattern (S _).

le2_proxy_L0 (m : N) : le2_proxy_type 0 m :=
  match m with
    | 0 ⇒ L0_0
    | S m' ⇒ L0_S' m end
le2_proxy_LS (n m : N) (l : le2 n m) := LS_S m n l

The completed proxy is then:

Definition le2_proxy {n m} (l : le2 n m) :
  le2_proxy_type n m :=
23:18 Proxy-based small inversions and their automation

764

match l with

765

| LO m ⇒ match m with 0 ⇒ LO_0 | S m ⇒ LO_S m end

766

| LS n m l ⇒ LS_S m n l

767

end.

769

7 Implementation

770

771

772

773

774

The automated creation of intermediate inductive types requires the manipulation of Rocq representations to create and define these new objects and in the Rocq environment. As such, classical automation tools like deep embedding cannot be used. We chose to use MetaRocq because there is a reasonable hope that our code could be later translated in OCaml, since objects are represented in the same way in MetaRocq as in the OCaml source code of Rocq.

775

776

777

Technical details on the architecture of our implementation and on MetaRocq's structures needed are developed in [2]. This section summarises the conclusions of this paper, then we discuss additional aspects of our implementation.

778

7.1 Using MetaRocq

779

780

781

782

783

784

785

786

787

788

789

790

791

792

793

794

795

796

797

798

799

800

801

802

803

MetaRocq [16] was designed in order to formalise and implement the metatheory of Rocq. As we use it here in a very different way, for implementing transformations on Rocq objects, it it worth noticing that MetaRocq turns out to be a suitable tool for our needs. Our implementation is able to automatically generate the necessary definitions for performing small inversions on most situations encountered in practice. This is of course the case of the elementary examples presented in this article, but we can also handle more advanced examples that are generally considered as out of reach of most users, including experienced ones. For instance, we can easily program a map3 function on lists, or reason on list positions defined using dependent types, see these examples explored in the artifact. The main features that we use are the quoting and representation of Rocq objects in the form of ASTs, the definition of new Rocq objects, inductive types and constants, from ASTs, and the sequencing of the actions of extracting, modifying and defining objects provided by the monad TemplateMonad.

Moreover, using MetaRocq (which is defined in Rocq) gives access to the powerful type
checker of Rocq. As an important bonus, we extensively used the ability to define the
intended target code of our approach in Rocq and to get its internal representation in order
to compare it with the AST generated by our tool.

The most difficult part in MetaRocq is the manipulation of deBruijn indices [6], which are
how all bound variables and recursive calls are represented in Rocq and MetaRocq. Indeed,
managing these indices in the specialisation transformation can become a nightmare, at
least without prior precautions. Defining derecursivation and deparameterisation as separate
transformations turned out to be a key decision, because they ensure invariants that make
deBruijn indices management much easier in the subsequent specialisation transformation.
However, once we established a good methodology to deal with these indices, we discovered
that they can be a boon when manipulating MetaRocq representations, especially when
adding new features or as support for corner cases.

804

## 7.2 Detecting specialisation possibilities and chaining them

805

806

In the case of an inductive type that has multiple indices, one might wonder which ones are
interesting to use as a pilot index. We have developed a heuristic to detect a potentially
useful index and specialise upon. This heuristic checks for these conditions to see if an index
can be used as a pilot index:

1. The index has an inductive type (while this might seem necessary at first glance, it could have a type reducible to an inductive type instead, see section 7.4).

2. The inductive type of the index does not include any indices (this point and the following one are also discussed in section 7.4).

3. In the inductive type to invert, the values of the pilot index in the conclusion of the constructors are all either variables or constructors applied to arguments.

4. In the inductive type to invert, the pilot index in the conclusion of the constructors takes at least once the value of a constructor applied to arguments (this insures that useful information can be derived from the separation into partial inductive types).

Using this heuristic, we have developed a left-to-right strategy for specialisation, where the inductive is checked from left to right for potential pilot indices; when a suitable one is found, a specialisation step is applied. Then, this process is repeated on all partial inductive types generated, until no index can be used as a pilot.

7.3 Nameless usage of proxies

Once the new partial inductive types, proxy and proxy type are defined in Rocq using
MetaRocq, it is highly desirable to perform inversion using a single generic name, which
abstracts away the name of each specific proxy. To this effect, we provide a custom typeclass
and a tactic notation that allow for a generic call, leaving Rocq’s internal typeclass resolution
system to select the appropriate instance.

Class Proxy (T:Type) := { proxy_type: Type; invproxy: T → proxy_type }.

Tactic Notation "inv" constr (p) := destruct (invproxy p).

Tactic Notation "inv" constr (p) "as" simple_intropattern (pat) :=
destruct (invproxy p) as pat.

There is a similar typeclass for dependent inversion. In addition to the Rocq objects described earlier, our MetaRocq implementation generates an instance of the typeclass Proxy, so that a call to the tactic inv x on the object x to invert can mimic the use of the inversion x tactic. When programming, the term to use is invproxy x, for example match invproxy x with. Other uses of the proxy and dependent proxy are presented in the artifact.

7.4 Differences with the general method

Proxy-based small inversions as a concept have a larger scope than our implementation. This is mainly because there are opportunities or ways to finely tune partial inductive types in a way that can be beyond the scope of the current generic algorithm. Here are some of the possibilities of proxy-based small inversions that we are aware of and may be implemented in the future:

■ If a pilot index of an inductive type has itself a dependent type, it is sometimes necessary to restrict the pattern matching occurring in the proxy type to the actual constructors that can be used. An additional proxy-based small inversion can be used in turn inside the definition of the proxy type: there, pattern-matching is no longer performed on the pilot, but on a proxy for the pilot itself.
23:20 Proxy-based small inversions and their automation

852

When the pilot index's value reduces to an applicative term of the form $fa_1...$ where f is not a constructor, it is possible to replace it by a fresh variable x and to add an explicit equality constraint $x = fa_1...$ in the partial inductive type considered, mimicking what is performed by the **inversion** tactic.

853

854

855

856

857

If an index **i** has a type described by a computation depending on the value of another index **b**, such as in the arity

858

$$ \forall \mathbf{b:bool}, (\mathbf{if} \mathbf{b} \mathbf{then} \mathbf{N} \mathbf{else} \mathbf{bool}) \rightarrow \mathbf{Type}, $$

859

860

it is possible to perform a first inversion using **b** as a pilot index to force the possible types of **i** before an inversion using **i** as the pilot.

8 Conclusion

861

862

863

864

865

866

867

868

We presented an alternate way to perform inversion on dependent inductive types, using transformations to isolate the information needed in partial inductive types and then leveraging case analysis to select the partial inductive type corresponding to the values of the indices. The Rocq code generated by our tool is very close to and as readable as the one we write by hand, e.g., the one that we have been regularly presenting to students for several years to explain reasoning by inversion [3]. Readability is also particularly welcome when inversion is used in programming functions with dependently typed arguments.

869

870

Readers interested in experimenting with our approach and its current implementation will find the examples of the article and some more in the artifact.

871

872

873

Our approach by successive independent transformations allows flexibility in adding new cases and strategies. For example, in the case of inductive types having many constructors, generating proxies restricted to a few relevant cases seems interesting and feasible.

874

Future work

875

876

The work to come on small inversions will mainly consist in trying to expand the scope of the automation in order to handle our advanced handwritten examples.

877

878

879

880

881

Besides that, now that we have a working prototype, we intend to explore the small inversions in large-scale projects using massive inductive types, like in CompCert [18], the certified C compiler. According to our survey of the use of inversion in CompCert, the large size inductive types used there for defining semantics fall within the scope of our current implementation of proxy-based small inversion.

882

883

We also consider possible applications of on-demand Rocq object creation in other situations where Rocq definitions need to be derived from user-defined objects.

884

References

885

886

887

1. Pierre Corbineau, Basile Gros, and Jean-François Monin. Certified programming with dependent types made simple with proxy-based small inversions. In Pierre Boutry and Loic Pujet, editors, *The Rocqshop 2025*, 2025.

888

889

890

2. Pierre Corbineau, Basile Gros, and Jean-François Monin. Proxy-based small inversions: a case study in metacoq programming. In Adrien Guatto and Marie Kerjean, editors, *JFLA 2025 - 36es Journées Francophones des Langages Applicatifs*, Jan 2025.

891

892

893

3. Pierre Corbineau and Jean-François Monin. Proofs-as-programs for programmers. In Julien Narboux, Walter Neuper, and Pedro Quaresma, editors, *ThEdu 24 - 13th International Workshop on Theorem proving components for Educational software*, July 2024.
894

895

896

897

898

899

900

901

902

903

904

905

906

907

908

909

910

911

912

913

914

915

916

917

918

919

920

921

922

923

924

925

926

927

928

929

930

931

932

933

934

935

936

937

938

939

940

941

942

943

944

945

4 Cristina Cornes and Delphine Terrasse. Automating inversion of inductive predicates in Coq. In Stefano Berardi and Mario Coppo, editors, *Types for Proofs and Programs*, pages 85–104, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg.

5 Pierre-Évariste Dagand and Conor McBride. Transporting functions across ornaments. *Journal of Functional Programming*, 24(2–3):316–383, 2014. doi:10.1017/S0956796814000069.

6 N. G. de Bruijn. Telescopic mappings in typed lambda calculus. *Inf. Comput.*, 91(2):189–204, 1991. doi:10.1016/0890-5401(91)90066-B.

7 Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. *Proc. ACM Program. Lang.*, 3(POPL), January 2019. doi:10.1145/3290316.

8 Healfdene Goguen, Conor McBride, and James McKinna. Eliminating dependent pattern matching. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, *Algebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday*, pages 521–540, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11780274_27.

9 Georges Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In Deepak Kapur, editor, *Computer Mathematics*, pages 333–333, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

10 Robbert Krebbers. *The C Standard Formalized in Coq*. PhD thesis, Radboud University, Nijmegen, 2015.

11 Dominique Larchey-Wendling and Jean-François Monin. *The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq*, chapter 8, pages 305–386. World Scientific Publishing Company, 2021. doi:10.1142/9789811236488_0008.

12 Jean-François Monin. Small inversions for smaller inversions. In *TYPES 2022 Abstracts*, Nantes, June 2022.

13 Jean-François Monin and Xiaomiu Shi. Handcrafted Inversions Made Operational on Operational Semantics. In S. Blazy, C. Paulin, and D. Pichardie, editors, *ITP 2013*, volume 7998 of LNCS, pages 338–353, Rennes, France, July 2013. Springer.

14 Jean-François Monin. Proof Trick: Small Inversions. In Yves Bertot, editor, *Second Coq Workshop*, Edinburgh, United Kingdom, July 2010. URL: https://hal.inria.fr/inria-00489412/en/.

15 mxdys, savask, Nathan Fenner, Justin Blanchard, Mateusz Naściszewski, Konrad Deka, Ijil, mei, Shawn Ligocki, Jason Yuen, Shawn Ligocki, Pavel Kropitz, Chris Xu, Shawn Ligocki, and Dan Briggs. [july 2nd 2024] we have proved "bb(5) = 47,176,870". https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237, July 2024.

16 Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Nielsen, Nicolas Tabareau, and Théo Winterhalter. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. J. ACM, 72(1), January 2025. doi:10.1145/3706056.

17 Matthieu Sozeau and Cyprien Mangin. Equations reloaded: high-level dependently-typed functional programming and proving in Coq. *Proc. ACM Program. Lang.*, 3(ICFP), July 2019. doi:10.1145/3341690.

18 The CompCert Development Team. Main website of the CompCert project. https://compcert.org/, 2024.

19 The Coq Development Team. The Coq reference manual, release 8.19.1, 2024.

20 The Coq Development Team. Main website of the Rocq project. https://rocq-prover.org/, 2025.

21 Philip Wadler. Views: A way for pattern matching to cohabit with data abstraction. In *Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987*, pages 307–313. ACM Press, 1987. doi:10.1145/41625.41653.

22 Benjamin Werner. *Une Théorie des Constructions Inductives*. Theses, Université Paris-Diderot - Paris VII, May 1994. URL: https://theses.hal.science/tel-00196524.