# The Rewster: Type Preserving Rewrite Rules for the Rocq Prover

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter

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

## To cite this version:

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Rocq Prover. 2025. hal-05294553

HAL Id: hal-05294553

https://inria.hal.science/hal-05294553v1

Preprint submitted on 2 Oct 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Rewster: Type Preserving Rewrite Rules for the Rocq Prover

Extended version of the ITP 2024 paper

Yann Leray¹,²*, Gaëtan Gilbert², Nicolas Tabareau², Théo Winterhalter³

¹Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, F-44000, Nantes, France.

²INRIA Rennes Bretagne Atlantique, LS2N, Nantes, France.

³INRIA Saclay, LMF, Gif-sur-Yvette, France.

*Corresponding author(s). E-mail(s): yann.leray@inria.fr;

## Abstract

In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour. While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as preservation of typing. In this paper, we present an implementation of rewrite rules on top of the Rocq Prover, together with two modular criteria to ensure that the added rewrite rules preserve confluence and typing. These criterion, based on the triangle property for the former and bidirectional type checking for the latter, are formally expressed in PCUIC—the type theory of Rocq recently developed in the MetaRocq project.

**Keywords:** type theory, dependent types, rewrite rules, confluence, type preservation, Rocq
# 1 Introduction

Dependently typed languages are the basis of major proof assistants like Agda [1], Rocq [2] and Lean [3]. In these systems, since general equality is undecidable, it is split into a decidable fragment called *definitional* and the complete but undecidable *propositional* equality. While propositional equality can be extended through axioms, definitional equality is defined upfront and limited in a way that can hinder proof developments and usability. Adding support for user-defined rewrite rules in proof assistants, as recently proposed by Cockx et al. [4], can mitigate these limitations, by allowing users to extend definitional equality in a powerful way through custom reductions. We present here an implementation to support such user-defined rewrite rules over the Rocq Prover. Rewrite rules allow us to write programs which cannot be defined in regular type theories, such as an addition which can reduce on constructors on both sides (usually called “parallel plus”).

Symbol `pplus`: $N \to N \to N$.

Infix `++`: $= pplus$.

Rewrite Rules `pplus_rew` :=

| 0 ++ ?n $\Rightarrow$ ?n | S ?m ++ ?n $\Rightarrow$ S (?m ++ ?n) |

| ?m ++ 0 $\Rightarrow$ ?m | ?m ++ S ?n $\Rightarrow$ S (?m ++ ?n). |

The symbol `pplus` behaves as standard addition, but with additional definitional equalities, that only hold propositionally for standard addition. For instance, `n ++ 0` and `0 ++ n` are both definitionally equal to `n`. This example shows the definition of a function that could already be defined, albeit with fewer definitional properties, but it is also possible to extend the logic of Rocq with new powerful constructions like inductive-recursive types using rewrite rules. As an illustration, consider the definition of (a simple version of) a universe of types:

Axiom `U`: Type.

Symbol `El`: $U \to Type$.

Symbols $(N:U)$ $(\Pi: \forall a:U, (El u \to U) \to U)$.

Symbol `U_rect`: $\forall (P:U \to Type), P N \to (\forall a b, (\forall A:El a, P (b A)) \to P (Pi a b)) \to \forall u, P u$.

Rewrite Rules `U_rect_rew` :=

| `U_rect` ?P ?pN ?pPi `N` $\Rightarrow$ ?pN

| `U_rect` ?P ?pN ?pPi `(Pi ?a ?b)` $\Rightarrow$

?pPi ?a ?b (fun `(A:El ?a)` $\Rightarrow$ `U_rect` ?P ?pN ?pPi `(?b A)`).

Rewrite Rules `El_red` :=

| `El N` $\Rightarrow$ `N`

| `El` `(Pi ?a ?b)` $\Rightarrow \forall (A:El ?a), El (?b A)$.

Without rewrite rules, this construction can be fully postulated with axioms using propositional equality, but in practice neither the elimination principle `U_rect` nor function `El` will compute, which makes the construction much less convenient to use. From this point of view, strictly positive indexed inductive types currently available in Rocq can be seen as one particular class of inductive constructions that have been anticipated, justified and provided natively in the system. Rewrite rules allow users
to go outside this fragment, for instance by defining a non-strictly positive inductive type.<fnref n="1" />

## Problematic examples of rewrite rules

However, contrarily to axioms which can only endanger consistency, the power of rewrite rules needs to be put in check or important metatheoretical properties can be broken. The work of Cockx et al. puts in light that the first property that rewrite rules must verify is confluence, otherwise subject reduction can be broken and type checking quickly becomes undecidable. Evidently, if a symbol b reduces to false by one rule and to true by another, we have contradicted the provable theorem that true ≠ false and we have lost consistency of the type theory. More insidiously, if a symbol T reduces to $N \to Z$ by one rule and to $Z \to N$ by another, we lose the injectivity of function types, a crucial component to ensure subject reduction. To address this, they develop a criterion that can be checked to determine if a rewriting system satisfies confluence, namely the triangle criterion [4]. In this paper, we develop a theory with more expressive patterns and rewrite rules, so we adapt their criterion to extend their proof of confluence in our setting.

To preserve subject reduction of the complete theory, rewrite rules must also verify a second property, type preservation, that is if $t : T$ and $t$ rewrites to $t'$, then $t' : T$. In [4], type preservation of rewrite rules is simply postulated, and one of the main contributions of this paper is to present a criterion to decide type preservation. A simple and intuitive check for type preservation could be to require that the equality induced by the rewrite rule should be well typed when universally quantified ($\forall \vec{x}, p = r$ well typed). There are however problems with this criterion as terms don't have a unique type in Rocq because of the subtyping introduced by universe cumulativity (*Type@{u}* is a subtype of *Type@{v}* when $u \leq_u v$). Let us see a few examples of how rewrite rules may break type preservation in ways that are difficult to notice.

**Example 1** If we consider an identity function on types, which simply returns its argument, cumulativity should mandate that the domain universe be smaller than the codomain universe. However, in the following example with a rewrite rule, this restriction is not enforced.<fnref n="2" />

```
Symbol id@{u v} : Type@{u} → Type@{v}.
Rewrite Rule id_rew := id ?T ⇒ ?T.
Universe a.
Check id Type@{a} : id Type@{a}.
```

The reason is that the naive check only mandates that both universes share a common bigger universe – something which is always verified. Thus, the check doesn't forbid this rule which nonetheless breaks consistency by allowing the existence of a term $U : U$ [6, 7].

<footnote n="1">¹The fact that general non-strictly positive inductive types are unsafe is due to Coquand and Paulin [5], but the argument uses impredicativity.</footnote>

<footnote n="2">²The universe level annotations were added for the comfort of the reader and are not required for the issue to arise.</footnote>
This paper demonstrates that establishing a sound criterion for type checking, in the absence of unique types, requires an asymmetry between both sides of the rewrite rules. Indeed, having a common type is not enough, but the correct criterion rather ensures that the right-hand side of a rewrite rule *checks* against the principal type *inferred* from the pattern on the left-hand side.

Another issue with the naive criterion is that the type of the variables $\vec{x}$ that appear in the pattern might also not be unique, and just testing for one possibility that works is not enough.

**Example 2** Let us consider a symbol which extracts the domains of function types, which can be defined as follows:

```
Symbol dom : Prop → Prop.
Rewrite Rule dom_rew := dom (∀ (x : ?A), ?B) ⇒ ?A.
Eval compute in dom (∀ (x : N), True). (* N : Prop *)
```

The problem here is that no information tells us what sort ?A has in the pattern in general, since the domain of a function type may have any sort (`SProp`, `Prop`, `Type` or even a newly declared sort). Our naive criterion, however, fails to detect the issue because the equality is well typed when both ?A and ?B have type `Prop`, since then both the pattern and the replacement term will have that type, and this problematic rule can then be accepted.

If we want our criterion to accept moderately difficult rewrite rules, including objects with dependent types, we need to accept virtually non-linear rewrite rules like the following:

**Example 3** Let us consider a symbol to implement the type-safe tail function on length-indexed vectors.

```
Symbol vtail : ∀ (n : N), vector (S n) → vector n.
Rewrite Rule vtail_vcons := vtail ?n (vcons ?m ?a ?v) ⇒ ?v.
```

At first glance, the pattern has type `vector ?n` and variable `?v` has type `vector ?m`, so this shouldn't be well typed. However, subpattern `(vcons ?m ?a ?v)` both is inferred to have type `vector (S ?m)` and is constrained to have type `vector (S ?n)`. Therefore, we can deduce that `?n = ?m` and accept this rule.

However, if we use the existing unification algorithm to infer such equalities during pattern type checking, we can face issues since it uses shortcut heuristics which don't always assume the worst.

**Example 4** Consider the following:

```
Inductive Box (b : B) : Type := box. (* box : ∀ (b : B), Box b *)
Symbol I : B → B.
Symbol C : ∀ (b : B), Box b → Box (I b).
Symbol D : ∀ (b : B), Box (I b) → Box b.
Rewrite Rule D_C := D_ (C _ ?b) ⇒ ?b.
```
Rewrite Rule $I_\_rew := I_\_ \Rightarrow false$.

Definition a : Box false := (D false (C _ (box true))).

Eval compute in a. (* box true : Box false *)

The rewrite rule $D\_ (C\_ ?b) \Rightarrow ?b$ looks enticing, if the box is not to be considered as a truncation. However, we don't know the behaviour of $I$ at that point, and as we add rule $I\_ \Rightarrow false$, our first rule loses its type preservation property, so it should in fact not have been accepted in the first place.

The last meta-theoretical property that is not endangered by adding axioms but may break with additional rewrite rules is termination. However, non-termination cannot introduce proofs of $\perp$; these can only come from the declaration of symbols and rules which are inconsistent propositionally from the start [4, Section 6.4]. It does not break subject reduction either, and we can derive a type checker that is valid irrespective of termination, in the sense that if it answers, the answer is correct. Non-termination can at worst result in type checking divergence. Therefore, we can show subject reduction with our criterion without relying on termination.

This paper presents how rewrite rules can be added to PCUIC, the theory of the kernel of Rocq as defined in the MetaRocq project [8, 9] including how they interact with the newly added sort polymorphism. We also extend the work of Cockx et al. [4] by adapting their *triangle criterion* to a richer grammar for patterns and by providing a criterion for type preservation in presence of cumulativity. Rewrite rules, as described in this paper and using the syntax demonstrated in the examples, have been implemented and integrated into the Rocq prover since version 8.20.

**Outline of the paper.** We begin by presenting an extension of PCUIC with *metavariables* in Section 2. We then define rewrite rules in Section 3 before adapting the triangle criterion and proof of confluence in Section 4, and explaining the type preservation criterion in Sections 5 and 6. Finally, we explore the implementation in Section 7 and conclude with related and future work in Sections 8 and 9.

**Extended journal version.** This paper is an extended version of Leray et al. [10] where the syntax of rewrite rules has been extended to support sort polymorphism, as recently introduced in Rocq. Additionally, the adaptation of the confluence criterion presented by Cockx et al. [4] necessary to extend the proof of confluence to our system has been developed in greater detail.

## 2 PCUIC with Metavariables

Before introducing rewrite rules, we present the type theory we will use, which extends the core theory of Rocq with *metavariables*. We start with a brief description of the syntax (Section 2.1), followed by the corresponding typing rules (Section 2.2) before highlighting the role cumulativity plays (Section 2.3).
<table><caption>Fig. 1 The (annotated) syntax of PCUIC, extended with metavariables</caption><tr><td>A, B, P, T, c, t, ...</td><td>::= x</td><td>variable</td></tr><tr><td></td><td>?x{t}</td><td>metavariable</td></tr><tr><td></td><td>u</td><td>universe</td></tr><tr><td></td><td>A@{s; l}</td><td>axiom</td></tr><tr><td></td><td>C@{s; l}</td><td>constructor</td></tr><tr><td></td><td>I@{s; l}</td><td>inductive</td></tr><tr><td></td><td>t t'</td><td>application</td></tr><tr><td></td><td>λ(x : A : u), t</td><td>abstraction</td></tr><tr><td></td><td>∀(x : A : u), (B : u')</td><td>function type</td></tr><tr><td></td><td>case c return P : u with t' case destruction</td><td></td></tr><tr><td></td><td>fix f : T := t</td><td>fixpoint</td></tr><tr><td>u, u'</td><td>::= □<sup>s</sup><sub>l</sub></td><td>universe</td></tr><tr><td>s</td><td>::= SProp | Prop | Type</td><td>ground sorts</td></tr><tr><td></td><td>x<sub>q</sub></td><td>sort variable</td></tr></table>

## 2.1 Syntax

PCUIC, which is the type theory at the core of Rocq, was given a formal description as part of the MetaRocq project [9]. We give its syntax, extended with metavariables, in Fig. 1. It is a dependent type theory featuring inductive types, where inductive elimination is split between fixed points and case analysis.

Following the work of Poiret et al. [11], PCUIC was extended to support so-called *sort polymorphism*, generalising universe level polymorphism [12] to also include sort variables that can be instantiated by **Type**, **Prop** or **SProp**. Universes are thus of the form $\Box_l^s$ where $s$ is either a variable or a ground sort. In the latter case, we will write **Type(l)** for $\Box_l^{\text{Type}}$, **Prop** for $\Box_0^{\text{Prop}}$, and **SProp** for $\Box_0^{\text{SProp}}$. Universe levels are maxima of ground universe levels, each possibly shifted by a natural number: $\max(l_i + k_i)$ with $l_i$ a collection of ground levels and $k_i \in \mathbb{N}$. **Prop** and **SProp** are impredicative, meaning that function types with codomain in $s$ will also live in $s$ as soon as $s \in \{\text{Prop}, \text{SProp}\}$. Additionally, **SProp** has definitional uniqueness of proofs, i.e., any two elements of a type in **SProp** are convertible. Universe levels $l$ are partially ordered with $\leq_\ell$, but when the sort of a universe is **Prop** or **SProp**, its level becomes irrelevant. This defines an ordering $\leq_u$ on universes with $\Box_l^s \leq_u \Box_{l'}^{s'} \iff s = s' \land (s \in \{\text{SProp}, \text{Prop}\} \lor l \leq_\ell l')$. We also order $\Box_u^{\text{Prop}} <_u \Box_{u'}^{\text{Type}}$.

Each element in the environment lives in its own universe context, thus needs a universe instance (containing both sorts and universe levels) to be used in a term: they are denoted by $@\{s; l\}$.

One should note that our $\lambda$-abstractions, function types and cases are heavily annotated; the type annotation on the domains is standard for PCUIC, but the additional universe annotations should be considered as *virtual*, since they are not part of the actual terms. They are simply short-hand notations for the universes given to the associated types in the typing derivation of the term, and are only required for the proof of our type-preservation criterion. They will often be omitted when they aren't useful.
To account for higher-order rewrite rules, the syntax needs to be extended with higher-order variables—henceforth called *metavariables*. A *metavariable* `?x{t}` is meant to live in an extended context, where said context extension is to be instantiated by the context instantiation `t` that the *metavariable* carries. While regular variable substitution will be denoted by `t[τ]`, *metasubstitution*—substitution for *metavariables*—will be denoted by `t{σ}`. Regular substitutions do nothing to *metavariables*, they only propagate to the context instantiation: `(?x{t})[τ] = ?x{t[τ]}`. Dually, *metasubstitutions* do nothing to variables and operate solely on *metavariables* as `(?x{t}){σ} = σ(?x)[t{σ}]`, they also propagate transparently to subterms on all other grammar constructions. Note that *metasubstitutions* need to be defined on all *metavariables* of the substituted term, a condition that will be verified for *metasubstitutions* appearing in rewrite rules.

## 2.2 Typing

The typing judgment of PCUIC is described in Fig. 2. Judgment $\Sigma; \Psi; \Theta; \Gamma \vdash t : T$ (shortened to $\Gamma \vdash t : T$ when $\Sigma, \Psi$ and $\Theta$ can be inferred from the context) states that term $t$ has type $T$ in local context $\Gamma$, *metavariable* context $\Theta$, universe context $\Psi$ and environment $\Sigma$; its rules are standard. The type of universes needs to take into account sorts: $\Box_{\_}^{\text{Prop}}$ and $\Box_{\_}^{\text{SProp}}$ both have type $\Box_{1}^{\text{Type}}$ and $\Box_{l}^{\text{Type}}$ has type $\Box_{l+1}^{\text{Type}}$. For sort variables, the worst case is assumed, thus $\Box_{l}^{x_s}$ has type $\Box_{l+1}^{\text{Type}}$. This is all condensed in the universe successor function $\uparrow_s l$ which equals 1 when $s \in \{\text{Prop}, \text{SProp}\}$ and $l+1$ otherwise. Similarly, the universe of a function type has the sort of its codomain, but its universe level depends on both sorts: $l *_{s}^{s}, l'$ is $\max(l, l')$ if $s = s' \in \{\text{Type}, x_s\}$ and $l'$ otherwise.

Environment $\Sigma$ can contain sort-polymorphic axiom declarations and inductive declarations. An axiom declaration simply gives a name and a type associated with it. An inductive declaration lives in a universe context $\Psi$ and contains a name $I$, a context of parameters $\Gamma_p$, a context of indices $\Gamma_i$ and a list of constructors, each with its name $C_k$, context $\Gamma_k$ and instantiation of the indices $\vec{i}_k$. Note that $\vec{i}_k$ may depend on $\Gamma_p, \Gamma_k$. Rule `CASE` asks for a *scrutinee* $c$ of type $I$ with some instantiation of the parameters $\vec{p}$ and some instantiation of the indices $\vec{t}$, a return type $P$ which depends on a generic instance of the inductive with the given parameters and branches at the return type specialized with the indices of the associated constructor, in the extended context of the constructor.

In order to define typing of *metavariables*, the typing judgment needs to take as input a *metavariable* context $\Theta$. Its elements are of the form $(\Delta_{?x} \vdash ?x : T)$, which reads as “?x is of type $T$ in context extension $\Delta_{?x}$”; which means in turn that the context instantiation associated to ?x must instantiate $\Delta_{?x}$. Technically, the typing rule for *metavariables* (Rule `META`) differs from the rule for variables (Rule `VAR`) in that it additionally checks that $\Gamma \vdash \vec{t} : \Delta_{?x}$, where typing is extended to substitutions pointwise.

Note that we remained abstract in our notion of *guard condition* for fixed points. In practice, fixed points need to recurse on structurally smaller arguments in order to avoid inconsistencies. Moreover to ensure termination, the computation rule for
### Σ

$\Sigma; \Psi; \cdot ; \cdot \vdash T : \Box_l^s$ Axiom
$\vdash \Sigma, (\Psi \vdash A : T)$

$\Sigma; \Psi; \cdot ; \Gamma_p, \Gamma_k \vdash \vec{i}_k : \Gamma_i$ side conditions (positivity, universe size)
$\vdash \Sigma, (\Psi \vdash I : \Gamma_p \rightarrow \Gamma_i \rightarrow \Box_l^s \text{ with } [C_k : (\vec{p} : \Gamma_p) \rightarrow \Gamma_k \rightarrow I \vec{p} \vec{i}_k])$ INDUCTIVE

### Θ

$\vdash \Sigma \qquad \Sigma \vdash_{\text{cstrs}} \Psi$ MCTXEMPTY
$\Sigma; \Psi \vdash \cdot$

$\Sigma; \Psi; \Theta; \Gamma \vdash T : \Box_l^s$ MCTXEXT
$\Sigma; \Psi \vdash \Theta, (\Gamma \vdash ?x : T)$

### Γ

($\Sigma, \Psi, \Theta$ left implicit since they are fixed)

$\Sigma; \Psi \vdash \Theta$ CCTXEMPTY
$\vdash \cdot$

$\Gamma \vdash T : \Box_l^s$ CCTXEXT
$\vdash \Gamma, x : T$

### T

$\vdash \Gamma \qquad (x : T) \in \Gamma$ VAR
$\Gamma \vdash x : T$

$\vdash \Gamma \qquad (\Delta_{?x} \vdash ?x : A) \in \Theta$ $\Gamma \vdash \vec{t} : \Delta_{?x}$ META
$\Gamma \vdash ?x\{\vec{t}\} : A[\vec{t}]$

$\vdash \Gamma \qquad (\Psi \vdash C : T) \in \Sigma \qquad \Sigma \vdash_{\text{cstrs}} \{\vec{s}; \vec{l}\} : \Psi$ ENVVAR
$\Gamma \vdash C@\{\vec{s}; \vec{l}\} : T@\{\vec{s}; \vec{l}\}$

$\vdash \Gamma \qquad \frac{\Gamma \vdash \Box_l^s : \Box_{\uparrow s}^{\text{Type}}}{\Gamma \vdash \Box_l^s} \text{UNIVERSE}$

$\frac{\Gamma \vdash f : \forall (x : A), B \qquad \Gamma \vdash t : A}{\Gamma \vdash f t : B[x := t]}$ APP

$\frac{\Gamma \vdash A : \Box_l^s \qquad \Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda(x : A : \Box_l^s), t : \forall (x : A), B}$ LAMBDA

$\frac{\Gamma \vdash A : \Box_l^s \qquad \Gamma, x : A \vdash B : \Box_{l'}^{s'}}{\Gamma \vdash \forall (x : A : \Box_l^s), (B : \Box_{l'}^{s'} : \Box_{l_*s', l'}^{s_r})}$ FORALL

$\frac{\Gamma \vdash A : \Box_l^s \qquad \Gamma \vdash A \le B \qquad \Gamma \vdash B : \Box_l^s}{\Gamma \vdash t : A \qquad \Gamma \vdash t : B}$ CUMUL

($\Psi \vdash I : \Gamma_p \rightarrow \Gamma_i \rightarrow \Box_l^s$ with $[C_k : (\vec{p} : \Gamma_p) \rightarrow \Gamma_k \rightarrow I \vec{p} \vec{i}_k]) \in \Sigma$

$\Gamma \vdash c : I@\{\vec{s}; \vec{l}\} \vec{p} \vec{i}$ $\Gamma, (\vec{i} : \Gamma_i), (x : I@\{\vec{s}; \vec{l}\} \vec{p} \vec{i}) \vdash P : \Box_{l_r}^{s_r}$

$[\Gamma, (\vec{a} : \Gamma_k[\vec{p}]) \vdash b_k : P[\Gamma_i := \vec{i}_k, x := C_k \vec{p} \vec{a}]_k]$ CASE

$\Gamma \vdash \text{case } c \text{ return } P : \Box_{l_r}^{s_r}$ with $\vec{b}_k : P[\Gamma_i := \vec{i}, x := c]$

$\frac{\Gamma \vdash T : \Box_l^s \qquad \Gamma, f : T \vdash t : T \qquad \Gamma \vdash t \text{ guarded}}{\Gamma \vdash \text{fix } f : T := t : T}$ FIX

<caption>**Fig. 2** Typing judgments in PCUIC with VARIABLES</caption>
$\Gamma \vdash t \to u$

$\overline{\Gamma \vdash (\lambda(x : A), t) a \to t[x := a]}^\beta \qquad \overline{\Gamma \vdash \text{fix } f := t \to t[f := \text{fix } f := t]}^{\text{FIXRED}}$

$$ \frac{(\Psi \vdash I : \Gamma_p \rightarrow \Gamma_i \rightarrow \Box_l^s \text{ with } [C_k : (\vec{p} : \Gamma_p) \rightarrow \Gamma_k \rightarrow I \, \vec{p} \, \vec{i}_k]) \in \Sigma}{\Gamma \vdash \text{ case } C_j \in \{\vec{s}; \vec{l}\} \ \vec{p} \ \vec{a} \text{ return } P \text{ with } \vec{b}_k \rightarrow b_j[\Gamma_j := \vec{a}]} \in \iota $$

$\Gamma \vdash t \leq_{\alpha} u$

$$ \frac{\Sigma; \Psi \vdash \Box_l^s \leq_u \Box_{l'}^{s'}}{\Gamma \vdash \Box_l^s \leq_{\alpha} \Box_{l'}^{s'}} \qquad \frac{\Gamma \vdash T : SProp \qquad \Gamma \vdash t : T \qquad \Gamma \vdash u : T}{\Gamma \vdash t \leq_{\alpha} u} $$

$$ \frac{(\Psi \vdash C : T) \in \Sigma \quad \vec{l} \leq_l \vec{l}'}{\Gamma \vdash C \in \{\vec{s}; \vec{l}\} \leq_{\alpha} C \in \{\vec{s}; \vec{l}'\}} \qquad \frac{\Gamma \vdash f \leq_{\alpha} f' \qquad \Gamma \vdash a \equiv_{\alpha} a'}{\Gamma \vdash f a \leq_{\alpha} f' a'} $$

$$ \frac{\Gamma \vdash A \equiv_{\alpha} A' \qquad \Gamma, (x : A) \vdash B \leq_{\alpha} B'}{\Gamma \vdash \forall (x : A : \Box_l^s), (B : \Box_{l_1}^{s_1}) \leq_{\alpha} \forall (x : A' : \Box_{l'}^{s'}), (B' : \Box_{l_1}^{s_1})} $$

<caption>**Fig. 3** Reduction and cumulativity judgment in PCUIC with metavariables</caption>

fix is typically guarded so that fixed points only unfold when they can consume a constructor. We forego this condition as we do not worry about termination in this paper.

## 2.3 Cumulativity

Our typing judgment contains a cumulativity rule (CUMUL), instead of the more traditional conversion rule. Cumulativity is defined similarly to conversion, except that we allow subtyping on universes: $\Box_l^s \leq_u \Box_{l'}^{s'}$. Formally, cumulativity is defined as the transitive closure $\leq$ of $\to \cup \leftarrow \cup \leq_\alpha$ where $\to$ is reduction, $\leftarrow$ antireduction (the symmetric relation to $\to$) and $\leq_\alpha$ is $\alpha$-cumulativity (defined below). We also define conversion $\equiv$ by replacing $\alpha$-cumulativity with $\alpha$-conversion. Reduction is generated by $\beta$ and $\iota$-reductions, unfolding of fixpoints (Rule FIXRED) and is allowed to happen in any subterm. $\alpha$-cumulativity is roughly $\alpha$-equality with the cumulativity rule on universes explained above, closed by congruence. However, most subterms need to be convertible and not only cumulative in the congruence. Formally, cumulativity $\leq_\alpha$ is defined with the rules described in Fig. 3 and the other congruences where all subterms need to be related with $\equiv_\alpha$, where $t \equiv_\alpha t'$ is defined as $t \leq_\alpha t' \wedge t' \leq_\alpha t$.

Rocq's kernel also supports SProp's proof irrelevance, but MetaRocq's definition of PCUIC does not integrate it because there is currently no proof of correctness with it
<figure><img src="image_3.png" /><figcaption>**Fig. 4** Syntax of patterns *p* and argument patterns *a*, *b*</figcaption></figure>

(even though it is largely believed to be compatible). The rule we give here is mostly for illustrative purposes and does not represent the real presentation with relevance marks [13]. In this paper, we will only try to justify that rewrite rules can still be compatible with the rest of the system, and why any proof featuring the irrelevance rule could be lifted to support rewrite rules.

## 3 Rewrite Rules

A rewrite rule is composed of a left-hand side, called *pattern*, and a right-hand side, called *replacement term*, and written $p \rightsquigarrow r$. When it is applied, a term *t* is *matched* against the pattern *p* to extract subterms at the *holes* of the pattern to form a metasubstitution *σ*, which is then substituted in the replacement term *r*, resulting in reduction *t* → *r*{σ}. As explained in the introduction, restrictions are needed so that the metatheory of PCUIC does not break.

### 3.1 Patterns

The syntax of patterns is described in Fig. 4. As a separation from axioms, that never reduce, we introduce in PCUIC a new class of constants named symbols, which is a specific subclass of axioms on which rewrite rules operate.

Patterns correspond to a subset of terms that need to be *rigid*. Their holes are denoted as *metavariables* (`?x`, also called *pattern variables*) in the pattern; each variable may only appear once in a pattern. Note that, unlike *metavariables*, pattern variables don't carry context instantiations. Thus to see a pattern variable as a term, we have to add the identity instantiation `{|Δ| := Δ}` for Δ the context in which the pattern variable lives. This gives us an injection $p \mapsto p$ from patterns to terms. From now on, we will simply use the change of color to represent this injection.

A pattern needs to be *rigid* to ensure that it unifies (at most) uniquely with any term; this limits where holes may appear, so we introduce the syntactic category of *argument patterns* which allow holes, and will *not* allow regular patterns to be holes, because holes are not rigid. For instance, having a hole at the head of eliminations
<figure><img src="image_4.png" /><figcaption>**Fig. 5** Description of pattern matching</figcaption></figure>

(e.g., pattern `?f?a` against term `(λx f, f x) 0 S`) would be ambiguous (does `?a` match with `0` or `S`?) and would not commute with other reductions (`?f` can match with `S` after reductions), so it must be forbidden. Generally, we can allow holes (equivalently, have argument patterns) anywhere but at the main subterm of an elimination construction, be it an application or a case destruction. Additionally, if part of a pattern coincides with a regular redex, usual reduction takes precedence thus the pattern cannot be matched; we therefore forbid this possibility. Finally, since we don't want to try all rewrite rules at all steps in reduction, we restrict patterns such that the head of their main branch of the pattern needs to be a symbol, which will be the starting point to pattern matching during reduction.

In the end, each rewrite rule induces the following reduction rule:

$$ \frac{(p \rightsquigarrow r) \in \Sigma \quad t \mid p \{\sigma\} \quad \text{REW}}{\Gamma \vdash t \rightarrow r \{\sigma\}} $$

where $t \mid p \{\sigma\}$ denotes the matching of $p$ against a term $t$ as described in the following section.

## 3.2 Pattern Matching

Pattern matching is the operation that tries to match a term $t$ against a pattern $p$, resulting in a metasubstitution $\sigma$ when it succeeds. (We made sure in the previous section that there can be at most one such $\sigma$.) Each pattern constructor can match against the associated term constructor, trying to match recursively, and pattern variables match against any term to fill the metasubstitution. The operation is denoted as
$t|_{p}\{\sigma\}$ and is formally defined in Fig. 5. Actually, pattern matching can also match universes levels against level variables and sort against sort variables, so the resulting $\sigma$ contains in fact a metasubstitution, a universe level substitution and a sort substitution. These last two substitutions are defined transparently on terms, only having effect on the sorts and universe level variables they carry. Pattern matching verifies one crucial property: $\forall p t \sigma, t|_{p}\{\sigma\} \Rightarrow t \equiv_{\alpha} p\{\sigma\}$. This $\alpha$-conversion would be an equality if not for the fact that some technical information is lost by pattern matching, such as names of binders.

Note that patterns are as heavily annotated as terms, but in this case it is required in the normal course of operations. Indeed, during the typing pass, we will need to give a type to all pattern variables and more generally to all argument patterns. This means that all type fields need an annotation to name the sort and universe level of said type. These annotations can however not be used during pattern matching, as they contain no computational content; the sort and universe level that are matched from the virtual annotation of terms can be considered virtual as well, they are also written in gray. These type annotations are necessary to avoid the issue presented in Example 2, where the type of a pattern variable could vary depending on the term being matched.

# 4 Confluence

In this section, we follow the steps taken by the Taming of the Rew [4], and extend it to our more expressive syntax of patterns.

## 4.1 Confluence through the triangle property

### Parallel reduction

Parallel reduction ($\Rightarrow$) [14, 15], defined in Fig. 6, can be seen as a variant of reduction where you are allowed to contract more than one redex, but all in parallel. In practice, this means that $\Rightarrow$ has all congruence rules and all computation rules, but where even redex subterms are allowed to reduce in parallel. Parallel reduction sits between one-step and many-step reduction:

$$ (\rightarrow) \subseteq (\Rightarrow) \subseteq (\rightarrow^*) $$

This has the immediate consequence that confluence of $\Rightarrow$ implies that of $\rightarrow$. Besides this, the reason why we rely on this alternate relation is that it is stable under substitution (if $t \Rightarrow t'$ and $a \Rightarrow a'$ then $t[x := a] \Rightarrow t'[x := a']$), which is not true of regular one-step reduction. Usually, this key property is what allows us to prove in turn the diamond property for parallel reduction, which is a much stronger form of confluence. Our goal is now to adapt the proof to a system with rule REWRITE as a reduction.

### Triangle property

In MetaRocq [9], the diamond property of parallel reduction is proven as a corollary to the triangle property (also called angle property [16], see Fig. 7), which states that
<figure><img src="image_5.png" /><figcaption>**Fig. 6** Parallel reduction for PCUIC</figcaption></figure>

there is for all terms $t$ an “upper-bound” reduct $\rho(t)$, in the sense that every parallel reduction $t \Rightarrow u$ implies $u \Rightarrow \rho(t)$. The idea is that $\rho(t)$ will contract all redexes which appear in $t$, while not contracting any that may appear subsequently. Then, any parallel reduction starting at $t$ contracts some of these redexes, which means that we can construct another parallel reduction step which contracts all remaining redexes in the term. Immediately, we can see that when $t \Rightarrow u$ and $t \Rightarrow v$, we can close the diamond by using $\rho(t)$, thanks to the triangle property. Graphically, this corresponds to grafting two triangles to get a diamond as in Fig. 7.
<figure><img src="image_6.png" /><figcaption>Fig. 7 Triangle and diamond properties</figcaption></figure>

## 4.2 Triangle criterion

To prove the triangle property with rewrite rules, we first need to understand how things go without them to see what criterion is going to allow the proof to go through. First, function $\rho$ is defined structurally as follows:

* If $t$ is a redex ($\beta$ or $\iota$), then $\rho(t)$ is its associated reduct, where all subterms are passed to $\rho$:

- $\rho((\lambda(x : A), t) u) = \rho(t)[x := \rho(u)]$

- $\rho(\text{case } C_j \text{ @}\{\vec{s}; \vec{l}\} \vec{p} \vec{a} \text{ return } P \text{ with } \vec{b}_k) = \rho(b_j)[\Gamma_j := \rho(\vec{a})]$

* otherwise, we recurse in $t$ and keep its head former:

- $\rho(f a) = \rho(f) \rho(a)$ when $f$ is not a lambda

- $\rho(\text{case } c \text{ return } P \text{ with } \vec{b}_k) = \text{case } \rho(c) \text{ return } \rho(P) \text{ with } \rho(\vec{b}_k)$ when $c$ is not an applied constructor

- $\rho(?x\{\vec{t}\}) = ?x\{\rho(\vec{t})\}$

- $\rho(\lambda(x : A), t) = \lambda(x : \rho(A)), \rho(t)$

- $\rho(\forall(x : A), B) = \forall(x : \rho(A)), \rho(t)$

- $\rho(t) = t$ if $t$ is an axiom, constructor, inductive, universe or variable

This makes it so that all redexes in $t$ are found and contracted at once.

With the addition of rewrite rules, we shall suppose them ordered and define $\rho(t)$ when $t$ matches at least one pattern from the set to be $r\{\sigma\}$ where $p \rightsquigarrow r$ is the first rewrite rule where $t$ matches against $p$, and with $t \mid p\{\sigma\}$. We will justify this extension in the exploration of the original proof.

**Theorem 1** With no rewrite rules, for all terms $t$ and $u$ such that $t \Rightarrow u$, we have $u \Rightarrow \rho(t)$

*Proof* The proof goes by induction over $t$. We go over the two clauses in $\rho$'s definition, and then examine which rules were taken to construct $t \Rightarrow u$:

1. $t$ is a redex, and $\rho(t)$ is its reduct. There are two subcases for the last rule used in $t \Rightarrow u$: it is either the computation rule or a congruence rule for an elimination where the last rule for the head is this a congruence rule for the associated constructor.

Let us take the example of a $\beta$-redex : $t = (\lambda(x : A), f) a$
(a) If the last rule is a computation rule, then we have some $f \Rightarrow f'$ and $a \Rightarrow a'$ such that $u = f'[x := a']$. By induction, we then have $f' \Rightarrow \rho(f)$ and $a' \Rightarrow \rho(a)$. Since $\Rightarrow$ is stable under substitution, we can derive $u = f'[x := a'] \Rightarrow \rho(f)[x := \rho(a)] = \rho(t)$.

(b) If the last rule is a congruence rule for application, then the last rule for its head must be a congruence for lambda, and we can find some $A \Rightarrow A'$, $f \Rightarrow f'$ and $a \Rightarrow a'$ such that $u = (\lambda(x : A'), f') a'$. By induction, we then have $f' \Rightarrow \rho(f)$ and $a' \Rightarrow \rho(a)$. Using rule $\beta$, we can derive $u = (\lambda(x : A'), f') a' \Rightarrow \rho(f)[x := \rho(a)] = \rho(t)$.

2. If $t$ has no head redex, then $t \Rightarrow u$ must come from a congruence rule, so we can conclude by induction. $\square$

Starting from this proof, we have to fill in what happens when $t$ is a redex for a rewrite rule, i.e., when $t$ matches the pattern of a declared rewrite rule. Let us consider the first such rewrite rule $p \rightsquigarrow r$, where $t \mid p \{\sigma\}$, and define $\Theta$ to be the set of all pattern variables in $p$. Similarly to the case where $t$ is a usual redex, we discriminate according to the rules that were used to construct the parallel reduction $t \Rightarrow u$ which correspond to the structure of the pattern $p$. There are again two cases: either all rules were congruence rules, or some rules were computation rules (this time, we can't ascertain that only one computation rule happened).

* If all rules are congruence rules, this means that we have both $t$ and $u$ match against the same skeleton $p$, thus $u \mid p \{\sigma'\}$ with also $\sigma \Rightarrow \sigma'$. The goal is to show that $u \Rightarrow \rho(t)$, so it is convenient to have defined $\rho(t) = r\{\rho(\sigma)\}$. This is now equivalent to clause 1 of $\rho$ since we contract a redex and apply $\rho$ to all subterms. This will also allow us to use the same proof idea than before: by induction, $\sigma' \Rightarrow \rho(\sigma)$ and since $\Rightarrow$ is stable under metasubstitutions, $u \Rightarrow r\{\rho(\sigma)\} = \rho(t)$.

* We now consider what to do if one of the rules in $t \Rightarrow u$ is a computation rule. Immediately, this means that a subpattern of $p$ is part of the redex. But we have to remember that one cannot have a hole at the head of an elimination in a pattern. This means that, if the redex does not come from a rewrite rule, it must entirely fit as a subpattern of $p$ (which is proscribed); if it is a rewrite rule redex, then its head symbol at least appears in $p$.

The only possibility is now that $t \Rightarrow u$ can be decomposed as pattern constructor congruences, rewrite rule computation rules and atoms $t_k \Rightarrow u_k$ where $t_k$ is a subterm of an element of $\sigma$. (Roughly, $t = C[p_1\{\sigma_1\}, \dots, p_n\{\sigma_n\}]$ for some term context $C$, rewrite rules $p_k \rightsquigarrow r_k$ and metasubstitutions $\sigma_k$, and $u = C[r_1\{\sigma'_1\}, \dots, r_n\{\sigma'_n\}]$, where elements of $\sigma_k$ are either also of this shape, or eventually subterms of $\sigma$).

To make sense of this, we need to impose a first condition on rewrite rules: the set of rewrite rule patterns in $\Sigma$ shall be closed under pattern unification, such that if $p$ is the unification of $p'$ and $p''$, then it is ordered before these two. In our sketch, since $p$ is the unification of itself with all the patterns used in the reduction $t \Rightarrow u$, this means that we can replace “subterms of $\sigma$” with “elements of $\sigma$ (each used once)”. This is needed because we can prove by induction that the reducts of these elements
reduce to the corresponding elements of $\rho(\sigma)$, but we couldn't relate subterms of $\sigma$
to $\rho(\sigma)$.

In turn, this means that we can factor out $\sigma$ from $t, u$ and $\rho(t)$ as follows: in the
decomposition of $t \Rightarrow u$, replace "elements of $\sigma$" with "metavariables in $\Theta$" (again,
each used once), to get a reduction $t_0 \Rightarrow u$ (in fact, $t_0 = p$) and $\rho(t) = r\{\Theta := \rho(\sigma)\}$
Since again $\Rightarrow$ is stable under metasubstitution, it is enough to show that $u_0 \Rightarrow$
$r\{\Theta}$, so we shall impose it as part of the criterion.

**Definition 1** The triangle condition states the following:

1. For all two rewrite rule patterns $p, p'$ with rules in $\Sigma$, if $p$ and $p'$ can be unified into $p^*$, then there exists a rewrite rule in $\Sigma$ with pattern $p^*$, placed before (in a large sense) the rules with patterns $p$ and $p'$.

2. For all rewrite rules $(p \rightsquigarrow r) \in \Sigma$, assuming that it is the first rule that the associated term $p$ matches against, for all $u$ such that $p \Rightarrow u$, we have $u \Rightarrow r$.

**Theorem 2** For all terms $t$ and $u$ such that $t \Rightarrow u$, we have $u \Rightarrow \rho(t)$

*Proof* The proof goes as before, but with one added case for $t$:

3. $t$ matches some rewrite rule in $\Sigma$. Let $p \rightsquigarrow r$ be the first one in $\Sigma$ that $t$ matches with $t \mid p\{\sigma\}$, thus $\rho(t) = r\{\rho(\sigma)\}$. As we established in the sketch above, thanks to point 1 of the triangle criterion, the only possibilities all imply the existence of a decomposition $u = u_0\{\sigma'\}$ where $p \Rightarrow u_0$ and $\sigma \Rightarrow \sigma'$. By induction, we have $\sigma' \Rightarrow \rho(\sigma)$; by point 2 of the triangle criterion, we have $u_0 \Rightarrow r$. Since $\Rightarrow$ is stable under metasubstitution, $u = u_0\{\sigma'\} \Rightarrow r\{\rho(\sigma)\}$.

□

*Deciding the triangle criterion*

Since there is a finite number of reduction rules that can be used for each former in a
pattern, and since the number of rules in $\Sigma$ is finite, this criterion is decidable. In fact,
Agda already implements this criterion as part of its `--confluence-check` flag [4]
and we intend to do the same for Rocq's implementation of rewrite rules.

**4.3 Compatibility with $\alpha$-cumulativity and irrelevance**

In dependent type theories, the most important use-case for the confluence property
is to establish the completeness of a conversion strategy based on reduction, with the
final goal to prove that conversion enjoys injectivity and non-confusion of type formers
(e.g., $\forall(x: A), B \equiv \forall(x: A'), B' \Longrightarrow A \equiv A' \wedge B \equiv B'$, and $\forall(x: A), B \not\equiv \Box_i^s$) In
Rocq and MetaRocq, this strategy is called "algorithmic cumulativity" (even though
it is not deterministic), and defined as $\to^*; \leq_\alpha; \leftarrow^*$. It satisfies all the properties of
the specification for cumulativity out of the box or through simple inductions, except
for transitivity.
To prove transitivity, we start with $t \to^*; \leq_{\alpha}; \leftarrow^*; \to^*; \leq_{\alpha}; \leftarrow^* u$ and we need to swap around everything until we reach the previous chain. To swap $\leftarrow^*; \to^*$ into $\to^*; \leftarrow^*$, we can use the confluence property established above. We can also prove with a simple induction that $\leq_{\alpha}$ is transitive. It only remains to swap $\leq_{\alpha}; \to$ into $\to^*; \leq_{\alpha}$ and (by symmetry) $\leftarrow; \leq_{\alpha}$ into $\leq_{\alpha}; \leftarrow^*$.

The proof of this swap goes by induction over $\to$. The only case of importance to us is rewrite rule reduction, when there is a rule $p \rightsquigarrow r$ such that $t \mid p \{\sigma\}$. Let us examine which rules appear in the construction $t \leq_{\alpha} u$ that correspond to the pattern constructors of $p$: for each term former, there are only two cases—a congruence rule, or the irrelevance rule. If all the rules used in $t$ that correspond to a pattern constructor in $p$ are congruences, then both $t$ and $u$ match against $p$ and we can swap directly. If any rule is the irrelevance rule, we can't claim this anymore, so we have to make sure that the irrelevance rule cannot be applied.

We can prove that, when a term $t$ matches a pattern $p$, both must have the same relevance. This means that we need to ensure no subpattern of a rewrite rule can be irrelevant, which we can check as a prerequisite to defining a rewrite rule. What's more, if a subpattern has a relevance which depends on a sort variable, we need to ensure that either all subpatterns are relevant or that the whole pattern is irrelevant. This way, if a rewrite rule can happen, then either no subterm is irrelevant and the rule can also apply to any $\alpha$-convertible term, or the whole term is irrelevant and we can ignore this reduction and use the irrelevance rule directly. The exact criterion is then: for a pattern $p$ of relevance $r$, $r \neq$ Irrelevant and all subpatterns of $p$ must either have relevance $r$ or be relevant.

# 5 Criterion for Type Preservation

This section presents a criterion to ensure that rewrite rules preserve typing. For a rewrite rule $p \rightsquigarrow r$, type preservation states that:

$$ \forall \Gamma, t, T, \sigma, \Gamma \vdash t : T \land t \mid p \{\sigma\} \implies \Gamma \vdash r \{\sigma\} : T $$

The idea of the criterion will be to find enough typing structure in $p$ through a bidirectional typing system, so that for every such application of the rewrite rule, we can extract out of $t$ some typing information for $\sigma$ and $T$, such that they can be used for the typing of $r\{\sigma\}$.

The criterion will involve more than the pattern and replacement term of the rewrite rule, adding the type, variable context and universe context of the rule, such that it now looks like $\Psi; \Theta \vdash p \rightsquigarrow r : T$.

## 5.1 Type Inference of Patterns

As mentioned in Section 1, the typing criterion on rewrite rules to ensure subject reduction cannot be solely based on the typing judgment of PCUIC. Actually, what needs to be checked is that the most general type that can be given to a term matching a pattern is a valid type for its replacement in the rewrite rule, when its variables also have the most general type allowed by the pattern.
$\Gamma \vdash_p p \triangleleft A$ ($\Sigma, \Psi, \Theta$ left implicit since they are fixed)

$$ \frac{(\Gamma \vdash ?x : A) \in \Theta}{\Gamma \vdash_p ?x \triangleleft A} \text{ PATVAR} $$

$$ \frac{\Gamma \vdash_p p \triangleright A \qquad \Gamma \vdash_p A \leqslant_p B}{\Gamma \vdash_p p \triangleleft B} \text{ CONV} $$

$\Gamma \vdash_p p \triangleright A$

$$ \frac{(x : A) \in \Gamma}{\Gamma \vdash_p x \triangleright A} \text{ VAR} $$

$$ \frac{(\Psi \vdash C : T) \in \Sigma \qquad \Sigma \vdash_{\text{cstrs}} \{\vec{s}; \vec{l}\} : \Psi}{\Gamma \vdash C @ \{\vec{s}; \vec{l}\} \triangleright T @ \{\vec{s}; \vec{l}\}} \text{ ENVVAR} $$

$\Gamma \vdash_p \Box_l^s \triangleright \Box_{l'sl}^{\text{Type}}$ UNIVERSE

$$ \frac{\Gamma \vdash_p p \triangleright \forall (x : A), B \qquad \Gamma \vdash_p a \triangleleft A}{\Gamma \vdash_p p a \triangleright B[x := a]} \text{ APP} $$

$$ \frac{\Gamma \vdash_p a \triangleleft \Box_l^s \qquad \Gamma, (x : a) \vdash_p p \triangleright B}{\Gamma \vdash_p \lambda(x : a : \Box_l^s), p \triangleright \forall(x : a), B} \text{ LAMBDA} $$

$$ \frac{\Gamma \vdash_p a \triangleleft \Box_l^s \qquad \Gamma, (x : a) \vdash_p b \triangleleft \Box_{l'}^{s'}}{\Gamma \vdash_p \forall (x : a : \Box_l^s), b : \Box_{l'}^{s'} \triangleright \Box_{l'*s'l'}^{s'*}} \text{ FORALL} $$

$$ \frac{(\Psi \vdash I : \Gamma_p \rightarrow \Gamma_i \rightarrow \Box_l^s \text{ with } [C_k : (\vec{p} : \Gamma_p) \rightarrow \Gamma_k \rightarrow I \vec{p} \vec{i}_k]) \in \Sigma \qquad \Gamma \vdash_p p \triangleright I \vec{p} \vec{i} \qquad \Gamma, (\vec{i} : \Gamma_i), (x : I \vec{p} \vec{i}) \vdash_p a \triangleleft \Box_l^s \qquad [\Gamma, (\vec{a} : \Gamma_k[\vec{p}]) \vdash_p b_k \triangleleft a[\Gamma_i := \vec{i}_k, x := C_k \vec{p} \vec{a}]_k]}{\Gamma \vdash_p \text{ case } p \text{ return } a : \Box_l^s \text{ with } \vec{b}_k \triangleright a[\Gamma_i := \vec{i}, x := p]} \text{ CASE} $$

<caption>**Fig. 8 Type inference of patterns**</caption>

To define this formally, we introduce the notion of type inference in a pattern. This notion is based on bidirectional typing as presented for instance by Lennon-Bertrand [17]. Technically, the type of a pattern will be inferred, denoted by $\Gamma \vdash_p p \triangleright T$, while the type of an argument pattern will only be checked, denoted by $\Gamma \vdash_p a \triangleleft T$. The rules for pattern inference are given in Fig. 8.

Most of the rules follow the standard bidirectional discipline. For instance, the type of a variable (VAR) is directly inferred from the local context, and the type of an application (APP) is inferred by inferring the type for the function and checking the type of the argument pattern against the domain of the function.

Let us remark once again that the universe annotations which correspond to the virtual annotations of terms (e.g., the domain in rule FORALL) are needed to check the associated type fields, whereas the usual discipline would have been to infer them and coerce them to universes.
The main specificity with respect to standard bidirectional typing lies in rule PAT-VAR for checking a pattern variable. In our presentation, we consider that $\Theta$ is given and mentions exactly the pattern variables occurring in the pattern. The rule then checks that the type mentioned in $\Theta$ is exactly the one that is checked. Since our criterion needs for pattern variables to have the most general type they can have, we need this rule to be in checking mode. In an algorithmic presentation, $\Theta$ can in fact be constructed solely from the typing of the pattern and can then be considered an output of the typing procedure, along with the inferred type of the whole pattern.

One last crucial rule is CONV, which allows changing bidirectional modes. It makes use of the pattern cumulativity relation $\leq_p$, which will be characterised and defined in Section 6, but can for the moment be approximated with regular term cumulativity (both are binary relations on regular terms).

Using this notion of type inference of patterns, we define the following criterion for subject reduction.

**Definition 2** (Type-preservation criterion) A rewrite rule $\Psi; \Theta \vdash p \rightsquigarrow r : T$ is said to preserve typing in the global environment $\Sigma$ when $\Sigma; \Psi; \Theta; \vdash_p p \triangleright T$ and $\Sigma; \Theta; \vdash r : T$.

## 5.2 Subject Reduction

In this section, we consider a fixed rewrite rule $\Psi_p; \Theta_p \vdash p \rightsquigarrow r : T_p$ that satisfies the type-preservation criterion in environment $\Sigma_0$. We have to show that the rewrite rule preserves typing in all extended environments and all local contexts, which means:

$$ \forall \Sigma \supseteq \Sigma_0, \Gamma, t, T, \sigma, \Gamma \vdash t : T \wedge t \mid p \{\sigma\} \implies \Gamma \vdash r \{\sigma\} : T $$

We first determine the properties that type inference $\vdash_p$ needs to satisfy before proving the implication. Let us fix an environment $\Sigma \supseteq \Sigma_0$ and a local context $\Gamma$.

1. We need to work under environment $\Sigma$ instead of $\Sigma_0$. Fortunately, $\vdash$ satisfies environment weakening and we can verify that $\vdash_p$ also satisfies it, so we can really work under assumptions $\Sigma; \Psi_p; \Theta_p; \vdash_p p \triangleright T_p$ and $\Sigma; \Psi_p; \Theta_p; \vdash r : T_p$.

2. We can use the substitution property of $\vdash$ and the fact that types are well typed to remove all mentions of $r$ in our implication: $\Gamma \vdash r \{\sigma\} : T$ can be proved with $\Gamma \vdash r \{\sigma\} : T_p \{\sigma\} \wedge T_p \{\sigma\} \leq T$ where the first part follows directly from $\Gamma \vdash \sigma : \Theta_p$. Thus, it only remains to prove the following anti-substitution lemma:

$$ \forall t, T, \sigma, \Gamma \vdash t : T \wedge t \mid p \{\sigma\} \implies \Gamma \vdash \sigma : \Theta_p \wedge \Gamma \vdash T_p \{\sigma\} \leq T $$

3. We need $\sigma$ to completely instantiate $\Theta$, so we make use of the fact that $\Theta$ contains exactly one entry per pattern variable of $p$.

4. Since the types in $\Theta$ and $T_p$ can refer to the additional universe annotations in patterns, we need to consider the virtual parts of $t$ and $\sigma$ in the following.

It is well known that the typing judgment of PCUIC satisfies environment weakening [9]. In fact, our extension with metavariables changes nothing to the proof (the
rule on VARIABLES doesn't mention the ENVIRONMENT), so the property still stands in our system. Even better, since our pattern typing judgment resembles regular typing, the same proof can be adapted to work on it, proving that pattern typing also satisfies environment weakening. Let us now prove the anti-substitution lemma.

We first need to introduce more elements and strengthen our property so that the induction can go through. We first split $\Gamma$ into $\Gamma$, $\Delta$ and $\sigma$ into $\sigma_0$, $\sigma$ such that $\Gamma$ is fixed while $\Delta$ is the context extension which corresponds to $\Delta_p$ as we go into the pattern and $\sigma_0$ corresponds to the already matched portion of the pattern, which will affect $\Delta$ and $\Theta_p$ while $\sigma$ corresponds to the currently matched portion of the pattern. The proof goes by induction on the type inference derivation of $p$, with induction predicate:

$$ \Sigma; \Theta_p; \Delta_p \vdash_p p \triangleright T_p \implies \\ \forall \Delta, t, T, \sigma_0, \sigma, \Gamma, \Delta \vdash t : T \wedge t \mid p \{\sigma\} \wedge \Delta_p \{\sigma_0\} \equiv \Delta \implies \\ \Gamma \vdash \sigma : \Theta_p \{\sigma_0\} \wedge T_p \{\sigma_0, \sigma\} \leq T $$

and the corresponding predicate on argument patterns:

$$ \Sigma; \Theta_p; \Delta_p \vdash_p p \triangleleft T_p \implies \\ \forall \Delta, t, T, \sigma_0, \sigma, \Gamma, \Delta \vdash t : T \wedge t \mid p \{\sigma\} \wedge T_p \{\sigma_0, \sigma\} \equiv T \wedge \Delta_p \{\sigma_0\} \equiv \Delta \implies \\ \Gamma \vdash \sigma : \Theta_p \{\sigma_0\} $$

Let us see all cases needed to prove the induction.

* Case $x$:

Hypotheses: $(x : T_p) \in \Delta_p, (x : T_0) \in \Delta, T_0 \leq T, \sigma = \cdot, \Delta_p \{\sigma_0\} \equiv \Delta$

Goal: $\Gamma \vdash \cdot : \Theta_p \{\sigma_0\}$ (empty goal) and $T_p \{\sigma_0\} \leq T$.

Proof: Since $\Delta_p \{\sigma_0\} \equiv \Delta$, we have $T_p \{\sigma_0\} \equiv T_0 \leq T$, so by transitivity we get $T_p \{\sigma_0\} \leq T$.

* Case $C@{?s; ?l}$:

Hypotheses: $(\Psi \vdash C : T_0) \in \Sigma, \Sigma \vdash_{cstrs} \{\vec{s}; \vec{l}\} : \Psi, T_0@{\{\vec{s}; \vec{l}\}} \leq T, \Delta_p \{\sigma_0\} \equiv \Delta, \sigma = [?s := \vec{s}; ?l := \vec{l}], T_p = T_0@{\{?s; ?l\}}$

Goal: $\Gamma \vdash \sigma : \Theta_p \{\sigma_0\}$ (empty goal) and $T_p \{\sigma_0, \sigma\} \leq T$.

Proof: $T_0$ is closed, so $T_p \{\sigma_0, \sigma\} = T_0@{\{?s; ?l\}} \{\sigma_0, \sigma\} = T_0@{\{\vec{s}; \vec{l}\}} \leq T$.

* Case $\Box_{\uparrow s}^s$:

Hypotheses: $\Box_{\uparrow s}^{\text{Type}} \leq T, \sigma = [s := s; ?l := l], T_p = \Box_{\uparrow s}^{\text{Type}} \{\sigma_0\} \equiv \Delta$.

([s := s] is [?s := s] if s = ?s, empty otherwise)

Goal: $\Gamma \vdash \sigma : \Theta_p \{\sigma_0\}$ (empty goal) and $\Box_{\uparrow s}^{\text{Type}} \{\sigma_0, \sigma\} \leq T$.

Proof: By transitivity, we only need $\Box_{\uparrow s}^{\text{Type}} \{\sigma_0, \sigma\} \leq \Box_{\uparrow s}^{\text{Type}}$, so $(\uparrow_s ?l)@{\{s := s; ?l := l\}} \leq l \uparrow_s l$.

We haven't yet defined $\uparrow$. When $s = ?s$, we need to return the lowest possible universe: 0; otherwise, we can return the same as $\uparrow_s ?l$.

* Case $p a$

Hypotheses: $\Delta_p \vdash_p p \triangleright \forall (x : A_p), B_p, \Delta_p \vdash_p a \triangleleft A_p, T_p = B_p[x := a], \Gamma, \Delta \vdash f t : T, \sigma = \sigma_1 + \sigma_2, f \mid p \{\sigma_1\}, t \mid a \{\sigma_2\}, \Delta_p \{\sigma_0\} \equiv \Delta$.
By inversion of typing on an application, there exists A and B such that
$\forall (x : A), B \le T$, $\Gamma, \Delta \vdash f : \forall x : A, B$ and $\Gamma, \Delta \vdash t : A$.

Then, by induction hypothesis on *p*, we get $(\forall x : A_p, B_p)\{\sigma_0, \sigma_1\} \le \forall x : A, B$ and $\Gamma \vdash \sigma_1 : \Theta_p\{\sigma_0\}$.

By the definition of substitution and injectivity of function types for $\le$, $A_p\{\sigma_0, \sigma_1\} \equiv A$ and $B_p\{\sigma_0, \sigma_1\} \le B$. Since $\Delta_p$ does not contain any metavariable in $|\sigma_1|$, $\Delta_p\{\sigma_0, \sigma_1\} \equiv \Delta$. This means we can use the induction hypothesis on *a* and get $\Gamma \vdash \sigma_2 : \Theta_p\{\sigma_0, \sigma_1\}$

Goal: $B_p[x := a]\{\sigma_0, \sigma\} \le B[x := t]$ and $\Gamma \vdash \sigma_1, \sigma_2 : \Theta_p\{\sigma_0\}$. The second goal is immediately proved by concatenating the induction hypotheses.

Proof: by commuting the substitution and metasubstitution,

$$
(B_p[x := a])\{\sigma_0, \sigma\} = B_p\{\sigma_0, \sigma\}[x := a\{\sigma_0, \sigma\}] \equiv B_p\{\sigma_0, \sigma\}[x := t] \le B[x := t]
$$

( *a* contains only metavariables in |*σ*₂| and *t* | *a* {*σ*₂}, so *a*{*σ*₀, *σ*} = *a*{*σ*₂} ≡ *t*)

• Case $\lambda(x : a : \Box_{\exists l}^{?s})$, $p$

Hypotheses: $\Delta_p \vdash_p a \triangleleft \Box_{\exists l}^? s$, $\Delta_p \vdash_p p \triangleright B_p$, $T_p = \forall (x : a), B_p$, $\Gamma, \Delta \vdash \lambda(x : A : \Box_l^s), t : T$, $A \mid a \{\sigma_1\}, t \mid p \{\sigma_2\}, \Delta_p \{\sigma_0\} \equiv \Delta$ with $\sigma = [?q := q; ?u := u]+\sigma_1 + \sigma_2$.

By inversion of typing on a lambda, we get $\forall (x : A), B \le T$, $\Gamma, \Delta \vdash A : \Box_l^s$ and $\Gamma, \Delta, (x : A) \vdash t : B$.

Since $\Delta_p$ does not contain any metavariable in $|\sigma_1|$, $(\Delta_p, x : a)\{\sigma_0, \sigma_1\} \equiv \Delta$, $(x : A)$. This means we can use both induction hypotheses to get $\Gamma \vdash \sigma_1 : \Theta\{\sigma_0\}$ and $\Gamma \vdash \sigma_2 : \Theta\{\sigma_0, \sigma_1\}, B_p\{\sigma_0, \sigma\} \le B$.

Goal: $(\forall (x : a), B_p)\{\sigma_0, \sigma\} \le \forall (x : A), B$ and $\Gamma \vdash \sigma_1, \sigma_2 : \Theta\{\sigma_0\}$. The second goal is immediately proved by concatenating the induction hypotheses.

Proof: *a* only mentions metavariables in $\sigma_1$, so $a\{\sigma\} \equiv A$. We also have $B_p\{\sigma_0, \sigma\} \le B$. By rule PROD for $\le$, we have our result.

• Case $\forall (x : a : \Box_{\exists l}^{?s}), b : \Box_{?l'}^{?s}$

Hypotheses: $\Delta_p \vdash_p a \triangleleft \Box_{\exists l}^? s$, $\Delta_p \vdash_p b \triangleleft \Box_{?l'}^? s$, $T_p = \Box_{?l^* s, ?l'}^{?s'}$, $\Gamma, \Delta \vdash \forall (x : A : \Box_l^s), (B : \Box_{l'}^{s'}) : T, A \mid a \{\sigma_1\}, B \mid b \{\sigma_2\}, \Delta_p \{\sigma_0\} \equiv \Delta$ with $\sigma = [?q := q; ?q' := q'; ?u := u; ?u' := u]+\sigma_1 + \sigma_2$.

By inversion of typing on a function type, we get $\Box_{l^*s, l'}^{s'} \le T$, $\Gamma, \Delta \vdash A : \Box_l^s$ and $\Gamma, \Delta, (x : A) \vdash B : \Box_{l'}^s$.

Since $\Delta_p$ does not contain any metavariable in $|\sigma_1|$, $(\Delta_p, x : a)\{\sigma_0, \sigma_1\} \equiv \Delta$, $(x : A)$. This means we can use both induction hypotheses to get $\Gamma \vdash \sigma_1 : \Theta\{\sigma_0\}$ and $\Gamma \vdash \sigma_2 : \Theta\{\sigma_0, \sigma_1\}$

Goal: $\Box_{?l^*s, ?l'}^{?s'}\{\sigma\} \le \Box_{l^*s, l'}^{s'}$ and $\Gamma \vdash \sigma_1, \sigma_2 : \Theta\{\sigma_0\}$. The second goal is immediately proved by concatenating the induction hypotheses.

Proof: The proof depends on how $?u_{*?q'}^{?q}?u'$ computes, since the result (after substitution) must always be less than what $*$ computes usually. This means that whenever its *q* argument is a variable, it has to return the lowest possible universe: $l_{*?s}^{?s}l' = l'$, otherwise it can return $l *_{s'}^s l'$.

• Case $\mathit{case} p \mathit{return} a : \Box_{\exists l}^{?s}$ with $\vec{b}_k$
Hypotheses:

$$- (\Psi \vdash I : \Gamma_p \rightarrow \Gamma_i \rightarrow \Box_{l_I}^{s_I} \text{ with } [C_k : (\vec{p} : \Gamma_p) \rightarrow \Gamma_k \rightarrow I \vec{p} \vec{i}_k]) \in \Sigma$$

$$- \Delta_p \vdash_p p \triangleright I \vec{q} \vec{j}$$

$$- \Delta_p, (\vec{i} : \Gamma_i), (x : I \vec{q} \vec{i}) \vdash_p a \triangleleft \Box_{l_I}^{?s}$$

$$- [\Delta_p, (\vec{a} : \Gamma_k[\vec{q}]) \vdash_p b_k \triangleleft a[\Gamma_i := \vec{i}_k, x := C_k \vec{q} \vec{a}]]_k$$

$$- T_p = a[\Gamma_i := \vec{j}, x := p]$$

$$- \Gamma, \Delta \vdash \text{ case } c \text{ return } P : \Box_{l_I}^{s_I} \text{ with } \vec{i}_k : T$$

$$- c \mid p \{\sigma_c\}, A \mid a \{\sigma_r\}, t_k \mid b_k \{\sigma_k\}$$

$$- \sigma = [?s := s; ?l := l] + \sigma_c + \sigma_r + \sum \sigma_k$$

$$- \Delta_p \{\sigma_0\} \equiv \Delta$$

By inversion of typing on a case, we get:

$$- P[\Gamma_i := \vec{i}, x := c] \le T$$

$$- \Gamma, \Delta \vdash c : I \vec{p} \vec{i}$$

$$- \Gamma, \Delta, (\vec{i} : \Gamma_i), (x : I \vec{p} \vec{i}) \vdash P : \Box_{l_I}^{s_I}$$

$$- [\Gamma, \Delta, (\vec{a} : \Gamma_k[\vec{p}]) \vdash t_k : P[\Gamma_i := \vec{i}_k, x := C_k \vec{p} \vec{a}]]_k$$

Then, by induction hypothesis on $p$, we get $(I \vec{q} \vec{j})\{\sigma_0, \sigma_c\} \le I \vec{p} \vec{i}$ and $\Gamma \vdash \sigma_c : \Theta_p\{\sigma_0\}$.

By the definition of substitution and injectivity of inductive types for $\le$, $\vec{q}\{\sigma_0, \sigma_c\} \equiv \vec{p}$ and $\vec{j}\{\sigma_0, \sigma_c\} \le \vec{i}$.

On the one hand, this gives us $(\Delta_p, (\vec{i} : \Gamma_i), (x : I \vec{q} \vec{i}))\{\sigma_0, \sigma_c\} \equiv \Delta, (\vec{i} : \Gamma_i), (x : I \vec{p} \vec{i})$ and since $\Box_{l_I}^{?s}\{\sigma_0, \sigma\} = \Box_{l_I}^{s_I}$ we can use the induction hypothesis on $a$ and get $\Gamma \vdash \sigma_r : \Theta_p\{\sigma_0, \sigma_c\}$.

On the other hand, this gives us $(\Delta_p, (\vec{a} : \Gamma_k[\vec{q}]))\{\sigma_0, \sigma_c, \sigma_r\} \equiv \Delta, (\vec{a} : \Gamma_k[\vec{p}])$ and $a[\Gamma_i := \vec{i}_k, x := C_k \vec{q} \vec{a}]\{\sigma_0, \sigma\} \equiv P[\Gamma_i := \vec{i}_k, x := C_k \vec{p} \vec{a}]$ we can use the induction hypothesis on $b_k$ and get $\Gamma \vdash \sigma_k : \Theta_p\{\sigma_0, \sigma_c, \sigma_r\}$.

Goal: $(a[\Gamma_i := \vec{j}, x := p])\{\sigma_0, \sigma\} \le P[\Gamma_i := \vec{i}, x := c]$ and $\Gamma \vdash \sigma_c, \sigma_r, \sum \sigma_k : \Theta\{\sigma_0\}$.

The second goal is immediately proved by concatenating the induction hypotheses.

Proof: Immediate since $\equiv$ is stable under substitution.

* Case ?x:

Hypotheses: $\Gamma, \Delta \vdash t : T$, $\sigma = [?x := t]$, $T_p\{\sigma_0\} \equiv T$, $\Delta_p\{\sigma_0\} \equiv \Delta$

Goal: $\Gamma \vdash (\Delta_p \vdash ?x : T_p)\{\sigma_0, \sigma\}$ which simplifies to $\Gamma, \Delta_p\{\sigma_0, \sigma\} \vdash t : T_p\{\sigma_0, \sigma\}$

Proof: Neither $\Delta_p$ nor $T_p$ mention ?x, so they are respectively convertible to $\Delta$ and $T$ by hypothesis, which proves our goal.

* Case CONV:

Hypotheses: $\Gamma, \Delta \vdash t : T$, $t \mid p\{\sigma\}, T'_p\{\sigma_0\} \equiv T$, $\Delta_p\{\sigma_0\} \equiv \Delta$, $T_p\{\sigma\} \le T$, $T_p \le_p T'_p$, $\Gamma \vdash \sigma : \Theta\{\sigma_0\}$.

Goal: $\Gamma \vdash \sigma : \Theta\{\sigma_0\}$. It is one of our hypotheses, our cumulativity hypotheses are useless for now. In Section 6 however, we present the definition of pattern cumulativity to extract some information from these unused hypotheses. Let us simply note that, by symmetry of $\equiv$ and transitivity, $T_p\{\sigma\} \le T'_p\{\sigma\}$, which we will use alongside $T_p \le_p T'_p$.
*Remark* This whole proof was done without mentioning the ambient $\Psi$ or $\Theta$. In practice, we only use this result with an empty $\Theta$, but the proof goes through whatever value they have.

### General subject reduction

Let us prove that the type system satisfies subject reduction. The proof goes as in MetaRocq [9], by induction over the reduction hypothesis. For all cases but rewrite rule redexes, we can do as usual since we established all required properties, mostly injectivity of type formers in Section 4.3. For rewrite rules, our type preservation property is exactly what is needed for the proof to go through.

## 6 Pattern Cumulativity and Equality Extraction

Currently, our criterion is too limited for our needs. For instance, it doesn't allow us to infer the type of slightly complex rewrite rules on vectors of natural numbers such as

$$ vtail ?n (vcons ?n' ?a ?v) \rightsquigarrow ?v $$

since the pattern has type **vector** ?n while the replacement term has type **vector** ?n'. However, typing ensures that we always have ?n = ?n', so we could extract this equality during pattern typing, in the same way that unification is used to collect constraints during the elaboration of a Rocq term [18]. This way, we can modify the subject reduction criterion to take advantage of these additional conversion hypotheses when checking the type of the right-hand side of the rewrite rule.

We proceed by defining a notion of pattern conversion and cumulativity ($\equiv_p$ and $\leq_p$) that collect the set of equalities $\mathcal{E}$ necessarily satisfied by substituted terms: we replace the binary relation $t \leq_p u$ with the ternary relation $t \leq_p u \triangleright \mathcal{E}$, which satisfies the following property:

$$ \begin{align*} \forall t, u, \mathcal{E}, \Sigma_0; \Theta_p; \Delta_p \vdash_p t &\leq_p u \triangleright \mathcal{E} \\ \forall \Sigma \supseteq \Sigma_0, \Psi, \Theta, \Gamma, \sigma, \Sigma; \Psi; \Theta \vdash \sigma : \Theta_p \wedge \Sigma; \Psi; \Theta \vdash \Delta_p \{\sigma\} \vdash t \{\sigma\} \leq u \{\sigma\} \\ &\implies \forall (\Delta_i \vdash t_i \equiv u_i) \in \mathcal{E}, \Sigma; \Psi; \Theta \vdash \Gamma, \Delta_i \{\sigma\} \vdash t_i \{\sigma\} \equiv u_i \{\sigma\}. \end{align*} $$

Note that we are still very free in the implementation of $\leq_p$ because, as long as we don't claim any equality ($\mathcal{E} = \emptyset$), even the full relation would be sound. However, we must remember that our primary goal is to extract as many enforced equalities as possible.

Our main objective is thus to apply safe inversions of conversion, to make sure that our equalities necessarily hold:

* If $t_1\{\sigma\} \equiv u$ and $t_1 \to^* t_2$, then by inclusion $t_1 \equiv t_2$ and by substitutivity $t_1\{\sigma\} \equiv t_2\{\sigma\}$ and thus $t_2\{\sigma\} \equiv u$. This means that we are allowed to reduce in $\equiv_p$.

* When a term is in weak head normal form, its congruence rule is invertible. This includes function types, universes, $\lambda$-abstractions, inductives, constructors and all weak head neutral terms (whne). Therefore, the general strategy for pattern conversion will be to reduce our arguments to weak head normal form and then to invert the congruence rule of the head constructor.
$$ \frac{\Gamma \vdash t \to^* t' \qquad \Gamma \vdash u \to^* u' \qquad \Gamma \vdash_p t' \leqslant_p u' \triangleright \mathcal{E} \qquad \text{RED}}{\Gamma \vdash_p t \leqslant_p u \triangleright \mathcal{E}} \qquad \frac{C \text{ is injective}}{\Gamma \vdash_p C \leqslant_p C \triangleright} \qquad \text{INJ} $$

$$ \frac{x \in \Gamma}{\Gamma \vdash_p x \leqslant_p x \triangleright} \text{REL} \qquad \frac{\Sigma \vdash s =_s s' \wedge l \leqslant_l l' \text{ possible}}{\Gamma \vdash_p \Box_l^s \leqslant_p \Box_{l'}^{s'} \triangleright [l \leqslant_l l'; s =_s s']} \text{UNIVERSE} $$

$$ \frac{\Gamma \vdash_p A \equiv_p B \triangleright \mathcal{E} \qquad \Gamma, (x : A) \vdash_p t \leqslant_p u \triangleright \mathcal{E}' \qquad \mathcal{B} \in \{\lambda, \forall\}}{\Gamma \vdash_p \mathcal{B}(x : A), t \leqslant_p \mathcal{B}(x : B), u \triangleright \mathcal{E} \cup \mathcal{E}'} \text{LAMBDA/FORALL} $$

$$ \frac{\Gamma \vdash_p f \leqslant_p f' \triangleright \mathcal{E} \qquad \Gamma \vdash_p a \equiv_p a' \triangleright \mathcal{E}' \qquad f, f' \text{ whne}}{\Gamma \vdash_p f a \leqslant_p f' a' \triangleright \mathcal{E} \cup \mathcal{E}'} \text{APP} $$

$$ \frac{\Gamma, \Gamma_i \vdash_p P \equiv_p P' \triangleright \mathcal{E}_r \qquad \Gamma \vdash_p c \equiv_p c' \triangleright \mathcal{E}_c \qquad [\Gamma, \Gamma_k \vdash_p b_k \equiv_p b'_k \triangleright \mathcal{E}_{b,k}]}{\Gamma \vdash_p \text{case } c \text{ return } P \text{ with } \vec{b} \leqslant_p \text{case } c' \text{ return } P' \text{ with } \vec{b}' \triangleright \mathcal{E}_c \cup \mathcal{E}_r \cup \bigcup_i \mathcal{E}_{b,i}} \text{CASE} $$

$$ \overline{\Sigma; \Theta; \Gamma \vdash_p ?x \equiv_p t \triangleright [\Delta \vdash ?x := t]} \text{PATVAR} $$

$$ \frac{t \text{ or } u \text{ contains a pattern variable or a symbol in head position}}{\Sigma; \Theta; \Gamma \vdash_p t \leqslant_p u \triangleright} \text{FAILSAFE} $$

$$ \frac{x \in \Gamma}{x \text{ whne}} \qquad \frac{f \text{ whne}}{f a \text{ whne}} \qquad \frac{c \text{ whne}}{\text{case } c \text{ return } P \text{ with } \vec{b} \text{ whne}} $$

<caption>**Fig. 9** The rules for conversion judgments $\leqslant_p$ and $\equiv_p$ (replace all $\leqslant_p$ with $\equiv_p$ in the rules)</caption>

* Symbols may be equipped with any rule in the future, so the congruence rules of their elimination context (as would-be neutral terms) are not invertible. This means we cannot extract information in this case and should simply accept with no equality (FAILSAFE). This approach is a way to avoid the failure of subject reduction described in Example 4.

* Metavariables may take any (well-typed) value, so the congruence rules of their elimination context (as would-be neutral terms) are not invertible. However, the conversion can be extracted as an equality. To keep the procedure easily decidable, we only keep the equality when the elimination context is empty $(?x\{\Delta := \Delta\} \equiv t)$. Also, if we extract more than one equality for a pattern variable, we discard all but one.
The definition of $t \leq_p u \triangleright \mathcal{E}$ is formally given in Fig. 9. We use this notion of cumulativity on patterns producing equality constraints to extend inference of patterns to also produce a set of equalities: $\vdash_p p \triangleright T_p, \mathcal{E}$.

In the setting we consider, all equations are of the form $\Delta \vdash ?x := a$ and can then be used in the regular typing judgment by adding reduction $?x\{\bar{t}\} \rightarrow a[\Delta := \bar{t}]$ for each $(\Delta \vdash ?x := a) \in \mathcal{E}$ in the definition of cumulativity. We write $\vdash_{\mathcal{E}}$ for the typing judgment where cumulativity is extended with the equalities in $\mathcal{E}$.

**Definition 3** (Extended type-preservation criterion) A rewrite rule $\Psi; \Theta_p \vdash p \rightsquigarrow r$ is said to be type-preserving in the global environment $\Sigma$ when there exists a variable context $\Theta$ and type $T_p$ and set of equalities $\mathcal{E}$ such that $\vdash_p p \triangleright T_p, \mathcal{E}$ and $\vdash_{\mathcal{E}} r : T_p$.

The proof of subject reduction can be extended easily to this setting.

# 7 Implementation

Rewrite rules have been implemented and integrated into the Rocq prover with pull request #18038, they first released in version 8.20 [19]. The criterion for type preservation has been implemented but pull request #19290 is yet to be integrated to the Rocq prover.

Let us describe a more complete example now possible thanks to rewrite rules: exceptions [20]. Previously, one could define an exception as an axiom and merely state how it behaves against other term constructors, now one can do the following:

```
Symbol raise : ∀ (A : Type), A.
Rewrite Rules raise_rew :=
  | raise (∀ (x : ?A), ?B) ?a ⇒ raise ?B@{x := ?a}
  | if raise B as b return ?P then _ else _ ⇒ raise ?P@{b := raise B}
  | match raise N as n return ?P with O ⇒ _ | S ⇒ _ end ⇒ raise ?P@{n := raise N}
  | fst (raise (?A * ?B)) ⇒ raise ?A | snd (raise (?A * ?B)) ⇒ raise ?B.
```

Note that the second and third rules would currently raise a warning complaining about a potential universe inconsistency, since the return predicates `?P` could have a universe level larger than the one `raise` expects, but this issue can only happen if one mentions that level explicitly, and we plan to introduce solutions to make this impossible (and thus make the rules safe) in the future.

A few extensions were made from the theory exposed in this paper, the first of which being the support of the full grammar of Rocq terms, including primitive projections (see the rules on the product type in the example above).

An extension has been made so that users can make some symbols unfold fixpoints. In Rocq, fixpoints are guarded to prevent infinite loops and the guard condition operates on inductive values. This means that fixpoint unfolding may only happen when the guarded argument has a head constructor. However, a user may want to add new values of an inductive type that should behave as a constructor in this regard, for instance an exception as in the example above. To this end, a flag called `unfold{fix} can be given when declaring a symbol:
(* Supersedes the declaration shown previously *)

#[unfold固定] Symbol raise : ∀ (A : Type), A.
(* ... same set of rewrite rules ... *)
Eval compute in raise N + 5. (* raise N *)

In practice, metavariables can be used to bind terms on the left-hand side and mention them in the right-hand side, but they are also convenient to avoid describing explicitly sub-patterns that are “forced” and will be found by the extraction of equalities mechanism described in Section 6. To this end, we have added the _ notation to produce metavariables that are not relevant to the right-hand side, like the two branches of the example above.

In this setting, another extension has been added to the type preservation criterion to mitigate the inference requirements for application and cases: while the theory requires that the pattern infers respectively a function type and an inductive type, it is in fact safe to allow inferring a pattern variable. This way, the user can write a pattern which infers as type an implicit pattern variable when it is expected to check against a function type or an inductive type, and we automatically add an equality between this implicit pattern variable and the function/inductive type with “fresh” pattern variables (respectively for the domain/codomain and for the arguments to the inductive). Since we cannot generate fresh variables during type checking, these additional pattern variables have to be added to the pattern from the start, giving for application a virtual annotation ($p: \forall(x: ?A), ?B$) $a$, with typing rule

$$ \frac{\Sigma; \Theta; \Gamma \vdash p \triangleq \forall(x: ?A), ?B \qquad \Sigma; \Theta; \Gamma \vdash a \triangleq ?A}{\Sigma; \Theta; \Gamma \vdash (p: \forall(x: ?A), ?B) a \triangleright ?B\{x := a\}} $$

# 8 Related Work

Cockx et al. [4] introduce a system for rewrite rules in dependently typed λ-calculus, which forms the foundation for this work. Their system employs simpler rewrite rules (lacking higher-order rules and cumulativity) and doesn’t provide a criterion for type preservation. In this paper, we extend their setting with higher-order rewrite rules in presence of cumulativity and definitional proof irrelevance. We also extend their criterion for ensuring confluence and its proof of correctness. We provide a decidable criterion to ensure type preservation which has been implemented in the Rocq prover. It is important to note that the argument by Cockx et al. regarding the consistency of the theory extended with rewrite rules, under the assumption that these rules are admissible as propositional equalities, also applies to our system. This is because their argument relies on an encoding in extensional type theory, and does not depend on the complexity or richness of the rewrite rules syntax.

In Andromeda 2 [21], users can describe definitional equality by providing equality rules, which can either be extensional or computational. The latter are interpreted as rewrite rules and thus used by Andromeda 2 without further user input [22]. The system checks type preservation in a manner similar to ours, but since their system is more permissive, it has fewer guarantees (such as substitutivity which always holds for us) and thus needs to check equalities before applying a rewrite rule.
Felicissimo [23] introduces a bidirectional system with rewriting, where rewrite rules are also checked to preserve typing. Both systems are close, but our pattern grammar is more expressive, we have fewer constraints on erased arguments (*e.g.*, our virtual universe annotations can't be recovered from the type of the function types) and we extract equalities from the typing of the pattern. The bidirectional approach has some interesting advantages such as the possibility to implement rewrite rules that would typically be non-left-linear. In the case of Rocq it would require a redesign of the syntax and thus it's not clear how to apply these interesting ideas.

Blanqui's decision procedure for type safety in rewrite rules [24] also checks type preservation and extracts equalities in a simpler theory, the λΠ-calculus modulo rewriting, thus without a (cumulative) hierarchy of universes or inductive types. In particular, there is no notion of subtyping and thus no need for bidirectional inference. However, this simpler setting makes it possible to extract more enforced equalities from the pattern.

# 9 Conclusion and Future Work

We introduced and implemented a new framework for users to define their own rewrite rules within the Rocq prover. Additionally, we developed a method to ensure these user-defined rules maintain type safety, guaranteeing the integrity of Rocq's core functionalities like subject reduction and completeness of type checking.

From a practical point of view, our most immediate goal is to implement for Rocq the confluence checker that we described and that has been impelmented for Agda by Jesper Cockx, so that we can improve the safety of rewrite rules. We can also look for a finer criterion by using more permissive proofs of confluence, like the Z method or decreasing diagrams. Another meaningful extension is to define a notion of modular rewrite rules, where users can postulate symbols and rewrite rules for a set of definitions and theorems, and then instantiate these symbols and rules with terms and equalities. If we allow for an instantiation to use propositional equalities, we could justify parallel plus using the standard notion of addition. Generally, modular rewrite rules allow for local postulates, which can be considered as safe if they are instantiated.

**Acknowledgements.** The authors would like to thank Vincent van Oostrom for his useful remarks and advice.

# References

[1] Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory vol. 32. Citeseer, ??? (2007)

[2] The Rocq Development Team: The Rocq Prover. Zenodo (2025). https://doi.org/10.5281/zenodo.15149629

[3] Moura, L., Ullrich, S.: The Lean 4 Theorem Prover and Programming Language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction – CADE 28, pp. 625–635. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_37
[4] Cockx, J., Tabareau, N., Winterhalter, T.: The taming of the rew: A type theory with computational assumptions. Proceedings of the ACM on Programming Languages 5(POPL), 60–16029 (2021) https://doi.org/10.1145/3434341

[5] Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG-88, pp. 50–66. Springer, Berlin, Heidelberg (1990). https://doi.org/10.1007/3-540-52335-9_47

[6] Girard, J.-Y.: Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII (1972)

[7] Hurkens, A.J.C.: A simplification of Girard's paradox. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) Typed Lambda Calculi and Applications, pp. 266–278. Springer, Berlin, Heidelberg (1995). https://doi.org/10.1007/BFb0014058

[8] Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N., Winterhalter, T.: The MetaCoq Project. Journal of Automated Reasoning (2020) https://doi.org/10.1007/s10817-019-09540-0

[9] Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. PACMPL 4(POPL) (2020) https://doi.org/10.1145/3371076

[10] Leray, Y., Gilbert, G., Tabareau, N., Winterhalter, T.: The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In: 15th International Conference on Interactive Theorem Proving (ITP 2024). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, ??? (2024). https://doi.org/10.4230/LIPIcs.ITP.2024.26

[11] Poiret, J., Gilbert, G., Maillard, K., Pédrot, P.-M., Sozeau, M., Tabareau, N., Tanter, É.: All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. Modified Coq with sort polymorphic prelude. 9(POPL), 76–2253762281 (2025) https://doi.org/10.1145/3704912

[12] Sozeau, M., Tabareau, N.: Universe Polymorphism in Coq. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving, pp. 499–514. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_32

[13] Gilbert, G., Cockx, J., Sozeau, M., Tabareau, N.: Definitional proof-irrelevance without K. Proceedings of the ACM on Programming Languages 3(POPL), 3–1328 (2019) https://doi.org/10.1145/3290316

[14] Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics, North holland edn. Studies in Logic and the Foundations of Mathematics, vol. 103. Amsterdam, New York, Oxford (1984)
[15] Takahashi, M.: Parallel reductions in λ-calculus. Journal of Symbolic Computation 7(2), 113–123 (1989) https://doi.org/10.1016/S0747-7171(89)80045-8

[16] van Oostrom, V.: Z; Syntax-Free Developments. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 195, pp. 24–12422. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021). https://doi.org/10.4230/LIPIcs.FSCD.2021.24

[17] Lennon-Bertrand, M.: Complete Bidirectional Typing for the Calculus of Inductive Constructions. In: 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 24–12419. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, ??? (2021). https://doi.org/10.4230/LIPIcs.ITP.2021.24

[18] Ziliani, B., Sozeau, M.: A unification algorithm for Coq featuring universe polymorphism and overloading. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. ICFP 2015, pp. 179–191. Association for Computing Machinery, New York, NY, USA (2015). https://doi.org/10.1145/2784731.2784751

[19] The Coq Development Team: The Coq Proof Assistant. Zenodo (2024). https://doi.org/10.5281/zenodo.14542673

[20] Pédrot, P.-M., Tabareau, N.: Failure is not an option an exceptional type theory. In: ESOP 2018 - 27th European Symposium on Programming. LNCS, vol. 10801, pp. 245–271. Springer, Thessaloniki, Greece (2018). https://doi.org/10.1007/978-3-319-89884-1_9

[21] Bauer, A., Haselwarter, P.G., Petković, A.: Equality Checking for General Type Theories in Andromeda 2. In: Bigatti, A.M., Carette, J., Davenport, J.H., Joswig, M., de Wolff, T. (eds.) Mathematical Software – ICMS 2020, pp. 253–259. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-52200-1_25

[22] Bauer, A., Petković Komel, A.: An extensible equality checking algorithm for dependent type theories. Logical Methods in Computer Science **Volume 18** Issue 1 (2022) https://doi.org/10.46298/lmcs-18(1:17)2022

[23] Felicissimo, T.: Generic bidirectional typing for dependent type theories. In: Weirich, S. (ed.) Programming Languages and Systems, pp. 143–170. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-57262-3_6

[24] Blanqui, F.: Type Safety of Rewrite Rules in Dependent Types. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Schloss-Dagstuhl - Leibniz Zentrum für Informatik, ??? (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.13