# Translating proofs from an impredicative type system to a predicative one

Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal

► To cite this version:

Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal. Translating proofs from an impredicative type system to a predicative one. 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), 2023, Warsaw, Poland. 10.4230/LIPIcs.CSL.2023.19. hal-03848584v2

HAL Id: hal-03848584

https://inria.hal.science/hal-03848584v2

Submitted on 4 Nov 2023

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Translating Proofs from an Impredicative Type System to a Predicative One

## Thiago Felicissimo ☒

Université Paris-Saclay, INRIA project, Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, 91190 France

## Frédéric Blanqui ☒

Université Paris-Saclay, INRIA project, Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, 91190 France

## Ashish Kumar Barnawal ☒

Indian Institute of Technology Guwahati, Guwahati 781039, Assam, India

## Abstract

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as COQ, MATITA and the HOL family, to proof assistants based on predicative logics like AGDA, whenever impredicativity is not used in an essential way.

In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in AGDA. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases.

During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones.

The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool PREDICATIVIZE and then used to translate semi-automatically many non-trivial developments from MATITA's arithmetic library to AGDA, including Bertrand's Postulate and Fermat's Little Theorem, which were not available in AGDA yet.

**2012 ACM Subject Classification** Theory of computation → Logic; Theory of computation → Type theory; Theory of computation → Equational logic and rewriting

**Keywords and phrases** Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2023.19

**Related Version** Full Version: https://arxiv.org/abs/2211.05700

**Supplementary Material** Software (Source Code): https://github.com/Deducteam/predicativize
archived at swh:1:dir:b2a1f99fe459c3e9a30debb4285eda1419b5d52d

**Acknowledgements** The authors would like to thank François Thiré for the help while developing PREDICATIVIZE, Gilles Dowek for remarks about previous versions of this paper, Jesper Cockx and Vincent Moreau for discussions about universe levels and the anonymous reviewers for the very helpful comments and remarks.

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

© Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal;

licensed under Creative Commons License CC-BY 4.0

31st EACSL Annual Conference on Computer Science Logic (CSL 2023).

Editors: Bartek Klin and Elaine Pimentel; Article No. 19; pp. 19:1–19:19

Leibniz International Proceedings in Informatics

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

LIPICS

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
# 1 Introduction

An important achievement of the research community in logic is the invention of proof assistants. Such tools allow for interactively writing proofs, which are then checked automatically and can then be reused in other developments. Unfortunately, a proof written in a proof assistant cannot be reused in another one, which makes each tool isolated in its own library of proofs. This is specially the case when considering two proof assistants with incompatible logics, as in this case simply translating from one syntax to another would not work. Therefore, in order to share proofs between systems it is very often required to do logical transformations.

One approach to share proofs from a proof assistant *A* to a proof assistant *B* is to define a transformation acting directly on the syntax of *A* and then implement it using the codebase of *A*. However, this code would be highly dependent on the implementation of *A* and can easily become outdated if the codebase of *A* evolves. Moreover, if there is another proof assistant *A'* whose logic is very similar to the one of *A* then this transformation would have to be implemented another time in order to be used with *A*.'

## Dedukti

The logical framework DEDUKTI [3] is a good candidate for a system where multiple logics can be encoded, allowing for logical transformations to be defined uniformly inside DEDUKTI.

Indeed, first, the framework was already shown to be sufficiently expressive to encode the logics of many proof assistants [11]. Moreover, previous works have shown how proofs can be transformed inside DEDUKTI. For instance, Thiré describes in [23] a transformation to translate a proof of Fermat's Little Theorem from the Calculus of Inductive Constructions to Higher Order Logic (HOL), which can then be exported to multiple proof assistants such as HOL, PVS, LEAN, etc. Géran also used Dedukti to export the formalization of Euclid's Elements Book 1 in COQ [5] to several proof assistants [17].

## (Im)Predicativity

One of the challenges in proof interoperability is sharing proofs coming from impredicative proof assistants (the majority of them) to predicative ones such as AGDA. Indeed, impredicativity, which is the ability in a logic to quantify over arbitrary entities, regardless of size considerations, is incompatible with predicative systems, in which each entity can only quantify over smaller ones.

Therefore, it is clear that any proof that uses such characteristic in an essential way cannot be translated to a predicative system. Nevertheless, one can wonder if most proofs written in impredicative systems really need impredicativity and, if not, how one could devise a way for detecting and translating them to predicative systems.

## Our contribution

In this paper, we tackle this problem by proposing an algorithm that tries to do precisely this. This algorithm was implemented on top of the DKCHECK type-checker for DEDUKTI with the tool PREDICATIVIZE, allowing for the translation of proofs semi-automatically inside DEDUKTI. These proofs can then be exported to AGDA, the main proof assistant based on predicative type theory.
This tool has been used to translate many proofs semi-automatically to AGDA, including MATITA’s arithmetic library. It contains many-non trivial proofs, and in particular a proof of Bertrand’s Postulate which was the subject of a whole publication [1] – thanks to our tool, the same hard work did not have to be repeated in order to make it available in AGDA.

## Outline

We start in Section 2 with an introduction to DEDUKTI, before moving to Section 3, where we present informally the problems that appear when translating proofs to predicative systems. We then introduce in Section 4 a predicative universe-polymorphic system, which is a subsystem of AGDA and is used as the target of the translation. This is followed by Section 5, the main one, where we present our algorithm. Section 6 then proposes an (incomplete) unification algorithm for universe levels, which is used by the predicativization algorithm. We then introduce the tool PREDICATIVIZE in Section 7, and describe the translation of MATITA’s library in Section 8. We end with some remarks in Section 9. The proofs not given in the main body of the article can be found in the long version (see link on the first page).

## 2 Dedukti

In this work we use DEDUKTI [3, 11] as the metatheory in which we express the various logic systems and define our proof transformation. Therefore, we start with a quick introduction to this system. The logical framework DEDUKTI has the syntax of the λ-calculus with dependent types (λΠ-calculus).

$$ A, B, M, N ::= x \mid c \mid MN \mid \lambda x : A.M \mid \Pi x : A.B \mid \text{Type} \mid \text{Kind} $$

Here, c ranges in a set of constants C, and x ranges in an infinite set of variables V disjoint from C. We call a type of the form $Πx : A.B$ a dependent product, and we write $A \to B$ when x does not appear free in B. We use s to refer to either Type or Kind.

A context Γ is a finite sequence of entries of the form x : A. A signature Σ is a finite sequence of entries of the form c : A (constant declarations) or c : A := M (definitions). It can be useful to split the signature into a global signature Σ and a local signature Δ defined on top of the global one. The global signature holds the definition of the object logic we are working in, whereas the local one holds axioms and definitions inside the logic. For instance, when working with natural numbers in predicate logic we would have $∧ : Prop \to Prop \to Prop \in \Sigma$, as ∧ is in the definition of predicate logic, but + : Nat → Nat → Nat ∈ Δ, given that the natural numbers and addition are not part of predicate logic, but can be defined on top of it.

The main difference between DEDUKTI and the λΠ-calculus is that we also consider a set $\mathcal{R}$ of rewrite rules, which are pairs of the form $c l_1...l_k \leftrightarrow r$ where $l_1, ..., l_k, r$ are terms. Given a signature $\Sigma$, $\Delta$, we also consider the $\delta$ rules allowing for the unfolding of definitions: we have $c \leftrightarrow M \in \delta$ for each $c : A := M \in \Sigma, \Delta$. We then denote by $\leftrightarrow_{\mathcal{R}}$ the closure by context and substitution of $\mathcal{R}$, and by $\leftrightarrow_{\delta}$ the closure by context of $\delta$. Finally, we write $\leftrightarrow_{\beta \mathcal{R} \delta}$ for $\leftrightarrow_{\beta} \cup \leftrightarrow_{\mathcal{R}} \cup \leftrightarrow_{\delta}$ and $\equiv_{\beta \mathcal{R} \delta}$ for its reflexive, symmetric and transitive closure.

Rewriting allows us to define equality by computation, but not all equalities can be defined like this in a well-behaved way, e.g. the commutativity of some operator. Therefore, we also consider rewriting modulo equations [6]. If $\mathcal{E}$ is a set of pairs of Dedukti terms (written as $M \approx N$), we write $\simeq_{\mathcal{E}}$ for its congruent closure – that is, its reflexive, symmetric and transitive closure by context and substitution.

Because $\mathcal{R}$ and $\mathcal{E}$ are usually kept fixed, in the following we write $\leftrightarrow$ for $\leftrightarrow_{\beta \mathcal{R} \delta}$, $\simeq$ for $\simeq_{\mathcal{E}}$ and $\equiv$ for the reflexive, symmetric and transitive closure of $\leftrightarrow \cup \simeq_{\mathcal{E}}$.
19:4 Translating Proofs from an Impredicative Type System to a Predicative One

<figure><img src="image_4.png" /><figcaption>Figure 1 The DEDUKTI theory which defines the PTS specified by ($S$, $\mathcal{A}$, $\mathcal{R}$).</figcaption></figure>

One very important notion that we will use in this work is that of a *theory*, which is a triple $(\Sigma, \mathcal{R}, \mathcal{E})$ where $\Sigma$ is a global signature and all constants appearing in $\mathcal{R}$ and $\mathcal{E}$ are declared in $\Sigma$. Theories are used to define in DEDUKTI the object logics in which we work (for instance, predicate logic).

The typing rules for DEDUKTI are given in Appendix A, along with some basic metaprop-
erties that we use in the subsequent proofs. We remark in particular that the conversion rule
of the system allows to exchange types which are equivalent modulo $\equiv$, which can use not
only $\beta$ but also $\delta$, $\mathcal{R}$ and $\mathcal{E}$.

2.1 Defining Pure Type Systems in Dedukti

We briefly review how Pure Type Systems (PTSs) [4] can be defined in DEDUKTI [12] (other approaches also exists, such as [14]), as we will need this in the rest of the article. Recall that in PTSs, universes and function types can be specified by a set $\mathcal{S}$ of universes, and two relations $\mathcal{A} \subseteq \mathcal{S}^2$ and $\mathcal{R} \subseteq \mathcal{S}^3$ – which we suppose to be functional relations here, as is usually the case. These specify that, if $(s_1, s_2) \in \mathcal{A}$, then $s_1$ is of type $s_2$, and if $(s_1, s_2, s_3) \in \mathcal{R}$ then when $A : s_1$ and $B : s_2$ we have $\Pi x : A.B : s_3$. Given a PTS specification $(S, \mathcal{A}, \mathcal{R})$, we can define the corresponding PTS with a DEDUKTI theory in the following manner.

We first start with the definition of universes. For each universe $s \in S$, we declare a
DEDUKTI type $U_s : \mathbf{Type}$ holding the types in the universe $s$. We then also declare a function
symbol $Els : U_s \rightarrow \mathbf{Type}$ mapping each member of $U_s$ to the type of its elements. We might
see the elements of $U_s$ as the codes for the types in $s$, and $Els$ as the decoding function,
mapping a code to its true type.

In order to represent the fact that a universe $s_1$ is a member of $s_2$ when $(s_1, s_2) \in \mathcal{A}$ we
add the constant $u_{s_1} : U_{s_2}$. However, now the universe $s_1$ is represented both by $Els_2 u_{s_1}$ and
$U_{s_1}$. Therefore, we add the rewrite rule $Els_2 u_{s_1} \to U_{s_1}$, stating that $u_{s_1}$ decodes to $U_{s_1}$.

Finally, to define dependent functions, for each $(s_1, s_2, s_3) \in \mathcal{R}$ we add a symbol $\pi_{s_1, s_2} : \Pi A : U_{s_1} (Els_1 A \to U_{s_2} \to U_{s_3})$. Intuitively, the type $Els_3 (\pi_{s_1, s_2} A (\lambda x.B))$ should hold the functions from $x : Els_1 A$ to $Els_2 B$, where $x$ might occur in $B$. To make this representation explicit, we add a rewrite rule $\pi_{s_1, s_2} A B \to \Pi x : Els_1 A. Els_2 (B x)$. Because the type of functions from $x : A$ to $B$ is now represented by the framework's function type, the framework's abstraction and application can be used to represent the ones of the encoded system.

In the following, we allow ourselves to write $\pi_{s_1,s_2} A (\lambda x.B)$ informally as $\pi_{s_1,s_2} x : A.B$ in order to improve clarity. When $x \notin FV(B)$, we might also write $A \rightsquigarrow_{s_1,s_2} B$.

3 An informal look at the challenges of proof predicativization

In this informal section we present the problem of proof predicativization and discuss the
challenges that arise through the use of examples. Even though the examples might be
unrealistic, they showcase real problems we found during our first predicativization attempt,
of Fermat’s little theorem library in HOL [23] – some of them being already noted in [13].
We first start by defining the theories **I** and **P**, which we will use to represent the core logics of impredicative and predicative proof assistants. These theories are defined as Pure Type Systems as explained in Subsection 2.1 and are described by the specifications below. Remember that a universe **s** is said to be impredicative when it is closed under dependent products indexed by some bigger sort, that is, for some **s'** with (s, s') ∈ 𝒜 we have (s', s, s) ∈ 𝒜. Therefore, **I** is an impredicative system and **P** is a predicative one.

$$S_I = \{*, \Box\}$$

$$A_I = \{(*, \Box)\}$$

$$R_I = \{(*,*,*), (\Box,*,*), (\Box,\Box,\Box)\}$$

$$S_P = \mathbb{N}$$

$$A_P = \{(n, n + 1) \mid n \in \mathbb{N}\}$$

$$R_P = \{(n, m, \max\{n, m\}) \mid n, m \in \mathbb{N}\}$$

In this setting, the problem of proof predicativization consists in defining a transformation such that, given a local signature $\Delta$ with $\Sigma_I, \Delta$; — well-formed, allows to translate it to a local signature $\Delta'$ with $\Sigma_P, \Delta'$; — well-formed. Stated informally, we would like to translate constants (which represent axioms) and definitions (which also represent proofs) from **I** into **P**. Note in particular that such a transformation is not applied to a single term but to a sequence of constants and definitions, which can be related by dependency — this dependency turns out to be a major issue as we will see. In the following we represent the local signature $\Delta$ in a more readable way as a list of entries **constant** c : A and **definition** c : A := M.

Now that our basic notions are explained, let us dive into proof predicativization. For our first step, consider a very simple development showing that for every type P in * we can build an element of $P \rightsquigarrow_{*,*} P$ — if * is a universe of propositions, then this is just a proof that each proposition in * implies itself.

$$\mathbf{definition} \ thm_1 : E_I_*( \pi_{\Box,*} P : u_*.P \rightsquigarrow_{*,*} P ) := \lambda P : U_*.\lambda p : E_I_0 P.p$$

To translate this simple development, the first idea that comes to mind is to define a mapping on universes: the universe * is mapped to 0 and the universe $\Box$ is mapped to 1. However, because our syntax in Dedukti is heavily annotated, we should only apply this map to the constants $u$ and $U$, which represent the universes, and then try to recalculate the annotations of the other constants $E_I$ and $\pi$ (remember that $\rightsquigarrow$ is just an alias for $\pi$). This would then yield the following local signature, which is indeed valid in **P**.

$$\mathbf{definition} \ thm_1 : E_I_1 (\pi_{1,0} P : u_0.P \rightsquigarrow_{0,0} P) := \lambda P : U_0.\lambda p : E_I_0 P.p$$

This naive approach however quickly fails when considering other cases. For instance, suppose now that one adds the following definition — once again, if * is a universe of propositions, then this is just a proof of the proposition ($\forall P.P \Rightarrow P) \Rightarrow \forall P.P \Rightarrow P$.

$$\mathbf{definition} \ thm_3 : E_I_*( ((\pi_{\Box,*} P : u_*.P \rightsquigarrow_{*,*} P) \rightsquigarrow_{*,*} \pi_{\Box,*} P : u_*.P \rightsquigarrow_{*,*} P) \\ := thm_1 (\pi_{\Box,*} P : u_*.P \rightsquigarrow_{*,*} P)$$

If we try to perform the same syntactic translation as before, we get the following result:

$$\mathbf{definition} \ thm_3 : E_I_1 ((\pi_{1,0} P : u_0.P \rightsquigarrow_{0,0} P) \rightsquigarrow_{1,1} \pi_{1,0} P : u_0.P \rightsquigarrow_{0,0} P) \\ := thm_1 (\pi_{1,0} P : u_0.P \rightsquigarrow_{0,0} P)$$

However, one can verify that this term is not well-typed. Indeed, in the original term one quantifies over all types in * in the term $\pi_{\Box,*} P : u_*.P \rightsquigarrow_{*,*} P$, and because of impredicativity this term stays at *. However, in **P** quantifying over all elements of the universe 0 in $\pi_{1,0} P : u_0.P \rightsquigarrow_{0,0} P$ raises the type to the universe 1. As $thm_1$ expects a term in the universe 0, the term $thm_1 (\pi_{1,0} P : u_0.P \rightsquigarrow_{0,0} P)$ is not well-typed.
19:6 Translating Proofs from an Impredicative Type System to a Predicative One

This suggests that impredicativity introduces a kind of *typical ambiguity*, as it allows us to hide in a single universe * all kinds of bigger types which would have to be placed in bigger universes in a predicative setting. Hence, in order to handle cases like this one, which arise a lot in practice, we should not translate every occurrence of * as 0 naively as we did, but try to compute for each occurrence of * some natural number *i* such that replacing it by *i* would produce a valid result.

Thankfully, performing such kind of transformations is exactly the goal of **UNIVERSO** [24].
This tool allows one to transport typing derivations between two PTS specifications.

To understand how this works, let us come back to the previous example. **UNIVERSO** starts here by replacing all sorts by occurrences of *l*, where *l* is a fresh metavariable representing a natural number.

definition **thm1**: $El_1$ $(\pi_{l_2,l_3} P : u_{l_4} \cdot P \rightsquigarrow_{l_5,l_6} P) := \lambda P : U_{l_7} \cdot \lambda p : El_8 P \cdot p$

definition **thm3**: $El_9$ $((\pi_{l_{10},l_{11}} P : u_{l_{12}} \cdot P \rightsquigarrow_{l_{13},l_{14}} P) \rightsquigarrow_{l_{15},l_{16}} \pi_{l_{17},l_{18}} P : u_{l_{19}} \cdot P \rightsquigarrow_{l_{20},l_{21}} P)$
$:= \mathbf{thm}_1 (\pi_{l_{22},l_{23}} P : u_{l_{24}} \cdot P \rightsquigarrow_{l_{25},l_{26}} P)$

These of course are not valid proofs in **P**, but in the following step **UNIVERSO** typechecks
such development and generates constraints in the process. These constraints are then given
to a SMT solver, which is used to compute for each metavariable *l* a natural number so that
the local signature is valid in **P**. For instance, applying **UNIVERSO** to our previous example
would produce the following valid local signature in **P**.

definition **thm1**: $El_2$ $(\pi_{2,1} P : u_1 \cdot P \rightsquigarrow_{1,1} P)) := \lambda P : U_1 \cdot \lambda p : El_1 P \cdot p$

definition **thm3**: $El_1$ $((\pi_{1,0} P : u_0 \cdot P \rightsquigarrow_{0,0} P) \rightsquigarrow_{1,1} \pi_{1,0} P : u_0 \cdot P \rightsquigarrow_{0,0} P)$
$:= \mathbf{thm}_1 (\pi_{1,0} P : u_0 \cdot P \rightsquigarrow_{0,0} P)$

By using **UNIVERSO** it is possible to go much further than with the naive syntactical
translation. Still, this approach also fails when being employed with real libraries. To
see the reason, consider the following minimum example, in which one uses an element of
$\pi_{\square,*} P : u_* \cdot P \rightsquigarrow_{*,*} P$ twice to build another element of the same type.

definition **thm1**: $El_*$ $(\pi_{\square,*} P : u_* \cdot P \rightsquigarrow_{*,*} P) := \lambda P : U_* \cdot \lambda p : El_* P \cdot p$

definition **thm2**: $El_*$ $(\pi_{\square,*} P : u_* \cdot P \rightsquigarrow_{*,*} P) := \mathbf{thm}_1 (\pi_{\square,*} P : u_* \cdot P \rightsquigarrow_{*,*} P) \mathbf{thm}_1$

If we repeat the same procedure as before, we get the following term, which generates
unsolvable constraints.

definition **thm1**: $El_1$ $(\pi_{l_2,l_3} P : u_{l_4} \cdot P \rightsquigarrow_{l_5,l_6} P) := \lambda P : U_{l_7} \cdot \lambda p : El_8 P \cdot p$

definition **thm2**: $El_9$ $(\pi_{l_{10},l_{11}} P : u_{l_{12}} \cdot P \rightsquigarrow_{l_{13},l_{14}} P) := \mathbf{thm}_1 (\pi_{l_{15},l_{16}} P : u_{l_{17}} \cdot P \rightsquigarrow_{l_{18},l_{19}} P) \mathbf{thm}_1$

This happens because the application $\mathbf{thm}_1 (\pi_{l_{15},l_{16}} P : u_{l_{17}} \cdot P \rightsquigarrow_{l_{18},l_{19}} P) \mathbf{thm}_1$ forces $l_4$ to be both $l_{17}$ and $l_{17} + 1$, which is impossible. This example suggests that impredicativity does not only hide the fact that types are stratified, but also the fact that they can be used at any level of this stratification. For instance, in our example we would like to use $\mathbf{thm}_1$ one time with $l_4 = l_{17}$ and another time with $l_4 = l_{17}+1$. In general, when trying to translate libraries using **UNIVERSO** we found that at very early stages a translated proof or object was already needed at multiple universes at the same time, causing the translation to fail.

Therefore, in order to properly compensate for the lack of impredicativity, our solution uses *universe polymorphism*, a feature in type theory (and also present in AGDA) that allows defining terms that can later be used at multiple universes [18, 21]. Our translation works by
trying to compute for each definition or declaration its most general universe polymorphic type, and using it when translating the subsequent declarations or definitions. To understand how this is done precisely, let us first introduce universe polymorphism, which is the subject of the following section.

## 4 A Universe-Polymorphic Predicative Type System

In this section, we define the Universe-Polymorphic Predicative Type System (or just **UPP**), which enriches the Predicative PTS **P** with prenex universe polymorphism [18, 16]. This is in particular a subsystem of the one underlying the AGDA proof assistant [22]. As usual, we define this system as a **DEDUKTI** theory **UPP** = ($\Sigma_{UPP}$, $\mathcal{R}_{UPP}$, $\mathcal{E}_{UPP}$).

The main change with respect to **P** is that, instead of indexing the constants $El_s$, $U_s$, $u_s$, $\pi_{s_1,s_2}$ externally, we index them inside the framework [2]. To do this, we first introduce a syntax for *universe levels* inside DEDUKTI by the following grammar

$$l, l' ::= i \in \mathcal{I} \mid z \mid s \mid l \mid l \sqcup l'$$

where the constants $z$, $s$ and $\sqcup$ are defined below and $\mathcal{I} \subsetneq \mathcal{V}$ is a set of level variables. We also enforce that level variables can only be substituted by other levels.

$$ \begin{array}{l@{\qquad}l} \mathit{Level} : \mathit{Type} & s : \mathit{Level} \to \mathit{Level} \\ \mathit{z} : \mathit{Level} & \sqcup : \mathit{Level} \to \mathit{Level} \to \mathit{Level} \quad \text{(written infix)} \end{array} $$

The definitions in the theory **P** of $El_s$, $U_s$, $u_s$, $\pi_{s_1,s_2}$ and the related rewrite rules are then replaced by the following ones.<fnref n="1" />

$$ \begin{array}{l@{\qquad}l} \mathit{U} : \mathit{Level} \to \mathit{Type} & \pi : \Pi(i_A i_B : \mathit{Level}) (A : U i_A) (El i_A A \to U i_B) \to U (i_A \sqcup i_B) \\ \mathit{El} : \Pi i : \mathit{Level} \cdot U i \to \mathit{Type} & \mathit{El} i' (u i) \leftrightarrow U i \\ \mathit{u} : \Pi i : \mathit{Level} \cdot U (s i) & \mathit{El} i' (\pi i_A i_B A B) \leftrightarrow \Pi x : \mathit{El} i_A A \cdot \mathit{El} i_B (B x) \end{array} $$

We however still allow ourselves to write $El_i$, $U_i$, $u_i$, $\pi_{i,i'}$ in order to improve clarity. We also reuse the previous convention to write $\pi_{i,i'} A (\lambda x.B)$ as $\pi_{i,i'} x : A.B$, or even $A \rightsquigarrow_{i,i'} B$ when $x \notin \mathit{FV}(B)$.

Now, (prenex) universe polymorphism can be represented directly with the use of the framework's function type [2]. Indeed, if a definition contains free level variables, it can be made universe polymorphic by abstracting over such variables. The following example illustrates this.

**► Example 1.** The universe polymorphic identity function is given by

$$id = \lambda(i : \mathit{Level}) . \lambda(A : U_i) . \lambda(a : El_i A) . a$$

which has type $\Pi i : \mathit{Level} . El_{(s \ i)} (\pi_{(s \ i),i} A : u_i.A \rightsquigarrow_{i,i} A)$. This then allows to use *id* at any universe level: for instance, we can obtain the polymorphic identity function at the level *z* with the application *id z*, which has type $El_{(s \ z)} (\pi_{(s \ z),z} A : u_z.A \rightsquigarrow_{z,z} A)$.

<footnote n="1">¹ Note that in the following rewrite rules we do not need to impose $i'$ to be equal or convertible to $s i$ or $i_A \sqcup i_B$, given that, for well-typed instances of the rule, this is ensured by typing [7, 2, 20, 9].</footnote>
19:8 Translating Proofs from an Impredicative Type System to a Predicative One

Finally, in order to finish our definition we need to specify the definitional equality satisfied by levels, which is the one generated by the following equations [22]. Note that, as stated before, we enforce that $i, i_1, i_2, i_3 \in \mathcal{I}$ can only be replaced by other levels.

$$i_1 \sqcup (i_2 \sqcup i_3) \approx (i_1 \sqcup i_2) \sqcup i_3$$

$$i_1 \sqcup i_2 \approx i_2 \sqcup i_1$$

$$s (i_1 \sqcup i_2) \approx s i_1 \sqcup s i_2$$

$$i \sqcup s i \approx s i$$

$$i \sqcup z \approx i$$

$$i \sqcup i \approx i$$

This definition is justified by the following property. Given a function $\sigma : \mathcal{I} \to \mathbb{N}$, define the interpretation $[[i]]_\sigma$ of a level $i$ by interpreting the symbols $z, s$ and $\sqcup$ as zero, successor and max, and by interpreting each variable $i$ by $\sigma(i)$.

**Proposition 2.** We have $i_1 \simeq i_2$ iff $[[i_1]]_\sigma = [[i_2]]_\sigma$ holds for all $\sigma$.

This also shows that our definition of $\simeq$ agrees with the one used in other works about universe levels [16, 15, 10]. The following basic properties show that $\mapsto$ and $\simeq$ interact well.

**Proposition 3.**

1. $\mapsto$ is confluent

2. If $M \simeq N \mapsto N'$ then, for some $M'$, we have $M \mapsto M' \simeq N'$.

3. If $M \equiv N$ then $M \mapsto * M' \simeq N' * \leftarrow N$.

Using the third property, one can apply known techniques to show that $\mapsto$ satisfies subject reduction [9, 19] (this can also be automatically verified using DKCHECK or LAMBDAPI).

**Proposition 4.** If $\Sigma_{UPP}, \Delta; \Gamma \vdash M : A$ and $M \mapsto M' : A$ then $\Sigma_{UPP}, \Delta; \Gamma \vdash M' : A$.

The third property is also very important from a practical perspective: it shows that in order to check $M \equiv N$ one does not need to use matching modulo $\simeq$.

5 The algorithm

We are now ready to define the (partial) translation of a local signature $\Delta$ to the theory UPP. The idea of the translation is that we traverse the signature $\Delta$ and at each step we try to compute the most general universe polymorphic version of a definition or constant. The result of a previously translated definition or declaration can then be used at multiple levels for translating entries occurring later in the signature. In order to understand all the following steps intuitively, we will make use of a running example.

**Example 5.** The last example of Section 3 corresponds to the local signature

$$\Delta_I = \text{thm}_1 : E_I_* (\pi_{\square,*} P : u_* . P \rightsquigarrow_{*,*} P) := \lambda P : U_* . \lambda p : E_I_* P . p,$$

$$\text{thm}_2 : E_I_* (\pi_{\square,*} P : u_* . P \rightsquigarrow_{*,*} P) := \text{thm}_1 (\pi_{\square,*} P : u_* . P \rightsquigarrow_{*,*} P) \text{thm}_1$$

which is well-formed in the theory I. Let us suppose that the first entry of the signature has already been translated, giving the following signature $\Delta_{\text{thm}_1}$.

$$\Delta_{\text{thm}_1} = \text{thm}_1 : \Pi i : \text{Level}.E_I_{(s \ i)} (\pi_{(s \ i),i} P : u_i . P \rightsquigarrow_{i,i} P) := \lambda i : \text{Level}.\lambda P : U_i . \lambda p : E_I_i P . p$$

Therefore, as a running example, we will translate step by step the second entry $\text{thm}_2$.

Let us start with some basic auxiliary definitions. Given a local signature $\Delta$ such that $\Sigma_{UPP}, \Delta; -$ well-formed and a constant $c$ occurring in $\Delta$, let us define ARITY($c$) as the greatest natural number $k$ such that the type of $c$ is of the form $\Pi i_1 .. i_k : \text{Level}.A$. Informally, it is the number of level arguments that this constant expects. For instance, we have $\text{ARITY}(\text{thm}_1) = 1$.
Using this function, let us define `INSERTMETAS(M)`, by the following equations. This function allows us to insert the fresh level variables that will be used to compute the constraints. We suppose that the inserted variables come from a dedicated subset of level variables $M \subsetneq I$ and that each inserted variable is fresh.

$$ INSERTMETAS(El_s) = El_i $$

$$ INSERTMETAS(Us) = U_i $$

$$ INSERTMETAS(U_s) = U_i $$

$$ INSERTMETAS(\pi_{s1,s2}) = \pi_{i,j} $$

$$ INSERTMETAS(c) = c \ i_1 \dots i_k \text{ where } k = \text{ARITY}(c) \text{ and } c \neq El_s, U_s, u_s, \pi_{s1,s2} $$

$$ INSERTMETAS(M) = M \text{ if } M \text{ is a variable } x \text{ or Type or Kind} $$

$$ INSERTMETAS(\Pi x : A.B) = \Pi x : INSERTMETAS(A).INSERTMETAS(B) $$

$$ INSERTMETAS(\lambda x : A.M) = \lambda x : INSERTMETAS(A).INSERTMETAS(M) $$

$$ INSERTMETAS(MN) = INSERTMETAS(M) INSERTMETAS(N) $$

**► Example 6.** By applying `INSERTMETAS` to the type and body of `thm2` we get

$$ INSERTMETAS(El_*(\pi_{\square,*} P : u_* . P \rightsquigarrow_{*,*} P)) = El_{i_1} (\pi_{i_2, i_3} P : u_{i_4} . P \rightsquigarrow_{i_5, i_6} P) $$

$$ INSERTMETAS(thm_1 (\pi_{\square,*} P : u_* . P \rightsquigarrow_{*,*} P) thm_1) = thm_1 i_7 (\pi_{i_8, i_9} P : u_{i_{10}} . P \rightsquigarrow_{i_{11}, i_{12}} P) (thm_1 i_{13}) $$

**► Remark 7.** Note that because our first step is erasing the universes that appear in the terms, this translation is defined for all PTS local signatures, and not only those in **I**. Therefore, it can be applied to proofs coming from systems featuring much more complex universes hierarchies then **I**, such as the PTS underlying the type systems of COQ and MATITA.

Once the fresh level variables are inserted, the next step is to compute the constraints between levels. To do this, we use an approach similar to [18] and define a bidirectional type checking/inference algorithm.

Figures 2 and 3 define rules for computing constraints required for two terms to be convertible or for a term to be typable, respectively. In these rules, we write $\hat{M}$ for the weak head normal form of $M$ when it exists – thus $(-)$ is a partial function, but becomes total if we suppose the termination of $\to$. As usual, $M \Rightarrow A$ denotes type inference, whereas $M \Leftarrow A$ denotes type checking. We also write $M \Rightarrow_{sort} s$ or $M \Rightarrow \Pi x : A.B$ as a shorthand for $M \Rightarrow A'$ and $\hat{A}' = s$ or $\hat{A}' = \Pi x : A.B$ respectively.

$$ \frac{\begin{array}{c} l, l' \text{ Level} \\ l \equiv? l' \downarrow \{l = l'\} \end{array}}{} \qquad \frac{\begin{array}{c} M = x, c, \text{Type, Kind} \\ M \equiv? M \downarrow \emptyset \end{array}}{} \qquad \frac{\begin{array}{c} M \equiv? M' \downarrow C_1 \\ MN \equiv? M'N' \downarrow C_1 \cup C_2 \end{array}}{} \qquad \frac{\begin{array}{c} \hat{M} \equiv? \hat{N} \equiv? \hat{N}' \downarrow C_2 \\ \hat{A} \equiv? \hat{A}' \downarrow C_1 \qquad \hat{B} \equiv? \hat{B}' \downarrow C_2 \qquad \hat{A} \equiv? \hat{A}' \downarrow C_1 \qquad \hat{M} \equiv? \hat{M}' \downarrow C_2 \\ \Pi x : A.B \equiv? \Pi x : A'.B' \downarrow C_1 \cup C_2 \qquad \lambda x : A.M \equiv? \lambda x : A'.M' \downarrow C_1 \cup C_2 \end{array}}{} $$

**Figure 2** Inference rules for computing constraints for two terms in whnf to be convertible.

Intuitively, these judgments define a conditional typing relation that depends on the constraints being satisfied. This intuition is formalized by the following results.

**► Definition 8.** Given a level substitution $\theta$ (sending level variables to levels) and a set of constraints $C$, containing pairs of levels $l = l'$, we write $\theta \models C$ when for all $l = l' \in C$, $l\theta \simeq l'\theta$.

**► Lemma 9.** If $M \equiv? N \downarrow C$ and $\theta \models C$ then $M\theta \equiv? N\theta$.

Let us write $\vec{i}_X$ for the free level variables in $X$. We also shorten $\vec{i} : Level$ as $\vec{i}$.

**► Lemma 10.** Given a level substitution $\theta$, suppose $\Sigma_{UPP}, \Delta; \vec{i}_{\Gamma\theta}, \Gamma\theta$ well-formed.

- If $\Sigma_{UPP}, \Delta; \Gamma \vdash M \Rightarrow A \downarrow C$ and $\theta \models C$ then $\Sigma_{UPP}, \Delta; \vec{i}_{\Gamma\theta} \cup \vec{i}_{M\theta} \cup \vec{i}_{A\theta}, \Gamma\theta \vdash M\theta : A\theta$

- If $\Sigma_{UPP}, \Delta; \Gamma \vdash M \Leftarrow A \downarrow C$, $\theta \models C$ and $\Sigma_{UPP}, \Delta; \vec{i}_{\Gamma\theta} \cup \vec{i}_{A\theta}, \Gamma\theta \vdash A\theta : s$ then we have $\Sigma_{UPP}, \Delta; \vec{i}_{\Gamma\theta} \cup \vec{i}_{M\theta} \cup \vec{i}_{A\theta}, \Gamma\theta \vdash M\theta : A\theta$
19:10 Translating Proofs from an Impredicative Type System to a Predicative One

$$
\frac{\displaystyle\frac{c : A := M \in \Sigma_{UPP}, \Delta \text{ or } c : A \in \Sigma_{UPP}, \Delta}{\Sigma_{UPP}, \Delta; \Gamma \vdash c \Rightarrow A \downarrow \emptyset} \quad \text{CONS} \quad \displaystyle\frac{x : A \in \Gamma}{\Sigma_{UPP}, \Delta; \Gamma \vdash x \Rightarrow A \downarrow \emptyset} \quad \text{VAR}}{\displaystyle\frac{i \in M}{\Sigma_{UPP}, \Delta; \Gamma \vdash i \Rightarrow \text{Level} \downarrow \emptyset} \quad \text{LVL-VAR}} \quad \text{SORT} \\
\frac{\displaystyle\frac{\Sigma_{UPP}, \Delta; \Gamma \vdash A \Leftarrow \mathbf{Type} \downarrow C_1}{\Sigma_{UPP}, \Delta; \Gamma \vdash \Pi x : A.B \Rightarrow s \downarrow C_1 \cup C_2} \quad \text{PROD}}{\Sigma_{UPP}, \Delta; \Gamma \vdash \lambda x : A.M \Rightarrow \Pi x : A.B \downarrow C_1 \cup C_2 \cup C_3} \quad \text{ABS} \\
\frac{\displaystyle\frac{\Sigma_{UPP}, \Delta; \Gamma \vdash M \Rightarrow \Pi x : A.B \downarrow C_1}{\Sigma_{UPP}, \Delta; \Gamma \vdash MN \Rightarrow B\{N/x\} \downarrow C_1 \cup C_2} \quad \text{APP}}{\Sigma_{UPP}, \Delta; \Gamma \vdash M \Leftarrow B \downarrow C_1 \cup C_2} \quad \text{CHECK}
$$

<caption>Figure 3 Inference rules for computing constraints for a term to be typable.</caption>

► **Example 11.** We can use the rules with our running example. We first calculate $\Sigma_{UPP}, \Delta_{thm_1}; \vdash E_{i_1} (\pi_{i_2,i_3} P : u_{i_4} P \rightsquigarrow i_5, i_6 P) \Rightarrow \mathit{sort} s \downarrow C_1$. Therefore, any substitution $\theta$ with $\theta \models C_1$ applied to the previous term results in a valid type. We then calculate

$$
\Sigma_{UPP}, \Delta_{thm_1}; \vdash \mathit{thm}_1 i_7 (\pi_{i_8,i_9} P : u_{i_{10}}.P \rightsquigarrow_{i_{11},i_{12}} P) (\mathit{thm}_1 i_{13}) \\
\qquad \Leftarrow E_{i_1} (\pi_{i_2,i_3} P : u_{i_4}.P \rightsquigarrow_{i_5,i_6} P) \downarrow C_2
$$

This gives $C_1 \cup C_2 = \{i_8 = s \ i_{10}, \ i_{11} = i_{10}, \ i_{12} = i_{10}, \ i_9 = i_{10} \sqcup i_{12}, \ i_8 \sqcup i_9 = i_7, \ i_{13} = i_{10}, \ i_1 = i_2 \sqcup i_3, \ s \ i_4 = i_2, \ i_5 = i_4, \ i_6 = i_4, \ i_3 = i_5 \sqcup i_6, \ i_4 = i_{10}\}$.

Once the constraints are computed the next step is to solve them. However, as explained in Section 3, we do not want a numerical assignment of level variables that satisfies the constraints, but rather a general symbolic solution which allows the term to be instantiated later at different universe levels. This leads us to use equational unification but, as levels are not purely syntactic entities, one needs to devise a unification algorithm for the equational theory $\simeq$. For now, let us postpone this to the next section and assume we are given a (partial) function `UNIFY` which computes from a set of constraints `C` a unifier $\theta$ – that is, a substitution satisfying $\theta \models C$. We however do not assume that $\theta$ is the most general unifier – as we show later in Theorem 15, such a most general unifier might not exist.

After an unifier $\theta$ is found, the final step is then to apply it.

► **Example 12.** Given the previous computed constraints $C_1 \cup C_2$ we can compute the substitution $\theta$ which sends all variables to $i_4$, except for $i_1, i_2, i_7, i_8$, which are sent to $s i_4$, and verify that $\theta \models C_1 \cup C_2$. By applying $\theta$, and by Lemma 10, we have

$$
\Sigma_{UPP}, \Delta_{thm_1}; i_4 \vdash \mathit{thm}_1 (s i_4) (\pi_{(s i_4),i_4} P : u_{i_4} P \rightsquigarrow_{i_4,i_4} P) (\mathit{thm}_1 i_4) \\
\phantom{\Sigma_{UPP}, \Delta_{thm_1}; i_4 \vdash \mathit{thm}_1 (s i_4) (\pi_{(s i_4),i_4} P : u_{i_4} P \rightsquigarrow_{i_4,i_4} P)} : E_{(s i_4)} (\pi_{(s i_4),i_4} P : u_{i_4} P \rightsquigarrow_{i_4,i_4} P)
$$

Note that in this term, the constant $\mathit{thm}_1$ is used at two different universe levels.

The final algorithm can now be described by the pseudocode in Figure 4. The algorithm might fail at any point when either it is not able to compute the constraints, or if the unification algorithm is not capable of inferring a substitution from the constraints. However, if the algorithm returns, its correctness is guaranteed by the following theorem:

► **Theorem 13.** If $|\Delta|$ is defined, then $\Sigma_{UPP}, |\Delta|; -$ well-formed.
<figure><img src="image_5.png" /><figcaption>**Figure 4** Pseudocode of the predicativization algorithm.</figcaption></figure>

**Proof.** By induction on $\Delta$, the base case being trivial. For the induction step, we have either $\Delta = \Delta'$; $c : A$ or $\Delta = \Delta'$; $c : A := M$. In both cases, if $|\Delta|$ is defined, then so is $|\Delta'|$, and thus by induction hypothesis we have $|\Delta'|$; **well-formed**. We proceed with a case analysis on the entry.

**Definition:** As $\Sigma_{UPP}, |\Delta'|; - \vdash A' \Rightarrow T \downarrow C_1$ and $\theta \models C_1$, by Lemma 10 we get $\Sigma_{UPP}, |\Delta'|; \vec{i}'_A \theta \cup \vec{i}'_T \theta \vdash A' \theta : T \theta$. Because $\hat{T} = s$, we also have $T \theta \hookrightarrow* s$, hence we can derive $\Sigma_{UPP}, |\Delta'|; \vec{i}'_A \theta \cup \vec{i}'_T \theta \vdash A' \theta : s$. By applying the substitution lemma with the substitution sending every variable $i$ in $\vec{i}'_T \theta$ but not in $\vec{i}'_A \theta$ to $z$, we get $\Sigma_{UPP}, |\Delta'|; \vec{i}'_A \theta \vdash A' \theta : s$. Because we also have $\Sigma_{UPP}, |\Delta'|; - \vdash M' \leftarrow A' \downarrow C_2$ and $\theta \models C_2$, by Lemma 10 again we get $\Sigma_{UPP}, |\Delta'|; \vec{i}'_M \theta \cup \vec{i}'_A \theta \vdash M' \theta : A' \theta$. By applying the substitution lemma with the substitution $\tau$, we get $\Sigma_{UPP}, |\Delta'|; \vec{i}' \vdash M' \theta \tau : A' \theta$, where $\vec{i} := \vec{i}'_A \theta$. Finally, by abstracting each free level variable, we get $\Sigma_{UPP}, |\Delta'|; - \vdash \lambda \vec{i} : \text{Level}.M' \theta \tau \vdash \vec{i} : \text{Level}.A' \theta$. Hence, we can derive $\Sigma_{UPP}, |\Delta'|; c : \Pi \vec{i} : \text{Level}.A' \theta := \lambda \vec{i} : \text{Level}.M' \theta \tau; - \text{well-formed}$.

**Constant:** Similar to the previous case.

► **Remark 14.** One could also wonder if the algorithm always terminates and produces a result (be it a valid signature or $\perp$). By supposing strong normalization for **UPP**, and by checking at each step of the rules in Figure 3 that the constraints are consistent, one could show termination of the algorithm by using a similar technique as in [18]. As we do not investigate strong normalization of **UPP** in this paper, we leave termination of the algorithm for future work. However, as we will see in Section 8, when using it in practice we were able to translate many proofs without non-termination issues.

Our algorithm relies on an unspecified function `UNIFY` in order to solve the constraints. In order to fully specify it, we thus present an unification algorithm for $\simeq$ in the next section. As we will discuss, the unification algorithm we propose is not guaranteed to always find a most general unifier whenever there is one. However, note that our predicativization algorithm can in principle be used with any unification algorithm for $\simeq$. Therefore, if we have a better unification algorithm in the future, we do not have the modify the algorithm of Figure 4.
# 6 Solving level constraints

Before addressing the problem of how to solve level constraints, the first natural question that comes to mind is if one can always find a most general unifier (mgu) when the constraints are solvable. The following result answers this negatively.

**Theorem 15.** *Not all solvable problems of unification modulo $\simeq$ over levels have most general unifiers.*

**Proof.** Consider the equation $s i_1 = i_2 \sqcup i_3$, which is a solvable unification problem, and suppose it had a mgu $\theta$. Note that $\theta_1 = i_1 \mapsto z, i_2 \mapsto s z, i_3 \mapsto z$ is also a solution, thus there is some $\tau$ such that $i_3\theta\tau \simeq z$. Therefore, there can be no occurrence of $s$ in $i_3\theta$. By taking $\theta_2 = i_1 \mapsto z, i_2 \mapsto z, i_3 \mapsto s z$ we can show similarly that there can be no occurrence of $s$ in $i_2\theta$. But by taking the substitution $\theta' = \underline{\phantom{z}} \mapsto z$ mapping all variables to $z$, we get $(i_2 \sqcup i_3)\theta\theta' \simeq z$, which cannot be equivalent to $(s i_1)\theta\theta'$. Hence, $s i_1 = i_2 \sqcup i_3$ has no mgu. $\quad \blacksquare$

Therefore, no unification algorithm for $\simeq$ can always produces a mgu. Hence, our algorithm will produce three kinds of results: either it produces a substitution, in which case it is a mgu; or it produces $\perp$, in which case there is no solution to the constraints; or it gets stuck on a set of constraints that it cannot handle. Still, it is not guaranteed to compute a mgu whenever there is one.

Before presenting the algorithm, the first issue we have to address is the fact that levels can have multiple equivalent representations. It would be convenient if we had a syntactical way to compare them. Thankfully, previous works have already addressed this problem.

Let us assume from this point on that level variables in $\mathcal{I}$ admit a total order $<$. Given a strictly increasing sequence of level variables $V = i_1, \dots, i_k$, and an $V$-indexed family of levels $\{l_i\}_{i \in V}$, let $\sqcup_{i \in V} l_i$ denote the term $l_1 \sqcup (l_2 \sqcup \dots (l_{k-1} \sqcup l_k))$. Moreover, given a natural number $k$, let $s^k / l$ be inductively defined by $s^0 / l = l$ and $s^{n+1} / l = s (s^n / l)$.

**Definition 16 (Level normal form).** A level is in normal form when it is of the form $s^k z \sqcup (\sqcup_{i \in V} s^{n_i} i)$ with $n_i \le k$ for all $i$.

Previous works [16, 15, 10] have established that for every level $l$ there is a unique level in normal form, which we refer to as $\hat{l}$, with $l \simeq \hat{l}$ – see for instance Lemma 6.2.5 of [15]. We will not describe explicitly here the algorithm for computing normal forms, as this has already been thoroughly explained in previous works, such as in [16, 10] – we note nevertheless that this procedure is sketched in the proof of Proposition 2.

We also define a notion of normal form for constraints.

**Definition 17.** A constraint $l_1 = l_2$ is said to be in normal form if

1. Both $l_1, l_2$ are in normal form – so we write $l_p = s^{k_p} z \sqcup (\sqcup_{i \in V_p} s^{n_i} i)$ for $p = 1, 2$

2. If $i \in V_1 \cap V_2$, then $n_i^1 = n_i^2$

3. At least one of the numbers in $\{k_1, k_2\} \cup \{n_i^1\}_{i \in V_1} \cup \{n_i^2\}_{i \in V_2}$ is equal to 0

Every constraint can be put in normal form, and for this we can use the algorithm in Figure 5. From the second line on, we use $k^p, n_i^p$ to refer to the indices in the normal forms of $l_1, l_2$. Moreover, the pseudocode should be read imperatively, in the sense that $l_1, l_2, V_1, V_2$ are updated at each step.

Given a set of constraints $C$, let $\hat{C}$ denote the result of putting all constraints of $C$ in normal form by applying the algorithm of Figure 5.

**Lemma 18.** For all substitutions $\theta$, we have $\theta \models C \iff \theta \models \hat{C}$.
let $h_1, h_2 = \hat{h}_1, \hat{h}_2$

for each $i \in V_1 \cap V_2$

if $n_i^1 < n_i^2$ then remove $s^{n_i^1} i$ from $h_1$

else if $n_i^1 > n_i^2$ then remove $s^{n_i^2} i$ from $h_2$

subtract the minimum value of the set $\{k_1, k_2\} \cup \{n_i^1\}_{i \in V_1} \cup \{n_i^2\}_{i \in V_2}$ from all of its elements

**Figure 5** Imperative algorithm for putting a constraint in normal form.

By putting constraints in normal form, we can help our unification algorithm to find a
solution, as shown by the following example.

**► Example 19.** Consider the constraint $i \sqcup s (i \sqcup s j) = j \sqcup s (s i)$ – which, as we will see, cannot be treated by our unification algorithm if it is not normalized first. By first computing the level normal form of each side, we get $s^2 z \sqcup s i \sqcup s^2 j = s^2 z \sqcup s^2 i \sqcup j$. As both variables appear in both sides, we remove from each of the sides the occurrence with the smaller index, giving $s^2 z \sqcup s^2 j = s^2 z \sqcup s^2 i$. Finally, as the minimum among all indices is 2, we subtract this from all of them, giving $z \sqcup j = z \sqcup i$ – a constraint that can be treated by our unification algorithm.

Write $\mathcal{I}(l)$ for the level variables appearing in $l$. Given a substitution $\theta$, we define the sets $dom \theta = \{i \mid i \neq i\theta\}$ and $range \theta = \cup_{i \in dom \theta} \mathcal{I}(i\theta)$, and the substitutions $\hat{\theta} = \{i \mapsto \hat{i\theta}\}_{i \in dom \theta}$, and $\theta\{l/j\} = \{i \mapsto i\theta\{l/j\}\}_{i \in dom \theta}$. Finally, we also define $\mathcal{I}(\theta) = range \theta \cup dom \theta$.

(Trivial) $\{l = l\} \cup C; \theta \rightsquigarrow C; \theta$

(Orient) $\{l = l'\} \cup C; \theta \rightsquigarrow \{l' = l\} \cup C; \theta$

if $l' = z$ or $z \sqcup i$

(Eliminate 1) $\{z \sqcup i = l\} \cup C; \theta \rightsquigarrow \widehat{C\{l/i\}}; \widehat{\theta\{l/i\}}$, $i \mapsto l$

if $i \notin l$

(Eliminate 2) $\{z \sqcup i = l\} \cup C; \theta \rightsquigarrow$

if $s^m i \in l$ with $m = 0$

let $l' = l\{i'/i\}$ in $\widehat{C\{l'/i\}}$; $\widehat{\theta\{l'/i\}}$, $i \mapsto l'$

for some $i' \in \mathcal{I}_{\text{fresh}} \setminus \mathcal{I}(i, l, C, \theta)$

(Decompose) $\{z = z \sqcup (\sqcup_{i \in V} i)\} \cup C; \theta \rightsquigarrow \{z \sqcup i = z\}_{i \in V} \cup C; \theta$

(Clash) $\{z = l\} \cup C; \theta \rightsquigarrow \perp$

if $s^n i \in l$ or $s^n z \in l$ with $n \neq 0$

**Figure 6** Unification algorithm for $\simeq$.

We are now ready to present the unification algorithm, whose rules are given in Figure 6. Steps are represented by rules of the form $C; \theta \rightsquigarrow C'$; $\theta'$, with the pre-conditions that constraints in $C$ are in normal form, $dom \theta$ is disjoint from $range \theta$, the image of $\theta$ contains only levels in normal form, and $dom \theta$ is disjoint from $\mathcal{I}(C)$ – these properties are preserved by each step. In rule (Eliminate 2), $\mathcal{I}_{\text{fresh}} \subsetneq \mathcal{I}$ is an infinite set of fresh level variables. Finally, it may happen that, for some non-empty sets of constraints $C$, no rule applies. This corresponds to the cases in which our algorithm gets stuck and does not produce a solution.

Let us write $\theta_1 \subseteq \theta_2$ when for all $i \in dom \theta_1$, $i\theta_1 = i\theta_2$ and $dom \theta_2 \setminus (dom \theta_1) \subseteq \mathcal{I}_{\text{fresh}}$ – that is, $\theta_2$ extends $\theta_1$ only inside $\mathcal{I}_{\text{fresh}}$.

The following lemma is key in showing the main properties of our algorithm.

**► Lemma 20 (Key lemma).** Suppose $C; \theta \rightsquigarrow C'$; $\theta'$. For all $\tau$, if $\tau \models C$ and $\tau \simeq \tau \circ \theta$ then there is a substitution $\tau'$ with $\tau \subseteq \tau'$ such that (1) $\tau' \models C'$ and (2) $\tau' \simeq \tau' \circ \theta'$. Conversely, for all $\tau$, if $\tau \simeq \tau \circ \theta'$ and $\tau \models C'$, then $\tau \simeq \tau \circ \theta$ and $\tau \models C$.
It is clear that $\rightsquigarrow$ does not always terminate, given that some rules create constraints and in particular that the rule (Orient) can loop. However, it is easy to check that these created constraints can always be eliminated by applying other rules. Indeed, the constraints created by (Decompose) can be eliminated by using (Eliminate 1), and the constraint created by (Orient) can be eliminated either by (Eliminate 1), (Eliminate 2), (Clash) or (Decompose), whose created constraints are eliminated once again using (Eliminate 1). Let $\rightsquigarrow_0$ be the relation that packs all of this into a single reduction, which therefore never creates constraints.

**Lemma 21.** $\rightsquigarrow_0$ terminates.

In the following theorems, we suppose that $\mathcal{I}(C)$ and $\mathcal{I}_{fresh}$ are disjoint.

**Theorem 22.** If $C$; $id \rightsquigarrow_0^* \perp$, then for no $\theta$ we have $\theta \models C$.

**Theorem 23.** If $C$; $id \rightsquigarrow_0^* \emptyset$; $\theta$, then $\theta$ is a most general unifier.

**Proof.** Let $\tau$ be a unifier. We thus have $\tau \models C$. Moreover, we have $\tau \simeq \tau \circ id$. By iterating Lemma 20, we get a substitution $\tau'$ such that $\tau' \simeq \tau' \circ \theta$ and $\tau \subseteq \tau'$. Because $dom \tau' \setminus (dom \tau) \subseteq \mathcal{I}_{fresh}$, which is disjoint from $\mathcal{I}(C)$, we have $i\tau = i\tau'$ for $i \in \mathcal{I}(C)$. Hence, for $i \in \mathcal{I}(C)$ we have $i\tau \simeq i\theta\tau'$, showing that $\tau$ is an instance of $\theta$.

To show that $\theta$ is a unifier, note that $\theta = \theta \circ \theta$ and $\theta \models \emptyset$, hence by iterating Lemma 20 in the inverse direction we get $\theta \models C$. ◀

We have seen that when the algorithm finishes with $\emptyset$; $\theta$, then $\theta$ is a mgu, and when it finishes with $\perp$, then there is no solution to the constraints. However, the algorithm can also get stuck on constraints that it does not know how to solve. In practice, it is very unsatisfying for the unification to get stuck, as this means that the whole predicativization algorithm has to halt. Thus, in order to prevent this, in our implementation we extended the unification with heuristics that are only applied when none of the presented rules applies. Then, whenever the heuristics are applied, the universe polymorphic definition or declaration that is produced might not be the most general one.

# 7 Predicativize, the implementation

In this section we present PREDICATIVIZE, an implementation of our algorithm. It is publicly available at https://github.com/Deducteam/predicativize/.

Our tool is implemented on top of DKCHECK [19], a type-checker for DEDUKTI, and thus does not rely neither on the codebase of AGDA, nor on the codebase of any other proof assistant. Like UNIVERSO [24], our implementation instruments DKCHECK's conversion checking in order to implement the constraint computation algorithm described in Section 5.

Because the currently available type-checkers for DEDUKTI do not implement rewriting modulo for equational theories other than AC (associative commutative), we used Genestier's encoding of levels [16] in order to define the theory UPP in a DKCHECK file.

To see how everything works in practice, we invite the reader to download the code and run make running-example, which translates our running example and produces a DEDUKTI file output/running_example.dk and an AGDA file agda_output/running-example.agda. In order to test the tool with a more realistic example, the reader can also run make test_agda, which translates a proof of Fermat's little theorem from the DEDUKTI encoding of HOL [23] to UPP.

In the following, let us go through some important particularities of how the tool works.
## User added constraints

As we have seen, our tool tries to compute the most general type for a definition or declaration to be typable. However, it is not always desirable to have the most general type, as shown by the following example.

**► Example 24.** Consider the local signature

$$ \Delta = \mathit{Nat} : U_{\square}; \mathit{zero} : E_{\square} \mathit{Nat}; \mathit{succ} : E_{\square} (\mathit{Nat} \rightsquigarrow \square, \square \mathit{Nat}) $$

defining the natural numbers in I. The translation of this signature by our algorithm is

$$ |\Delta| = \mathit{Nat} : \Pi i : \mathit{Level}.U_i; \mathit{zero} : \Pi i : \mathit{Level}.E_i (\mathit{Nat} i); \mathit{succ} : \Pi i j : \mathit{Level}.E_{i \sqcup j} ((\mathit{Nat} i) \rightsquigarrow_{i,j} (\mathit{Nat} j)) $$

However, we normally would like to impose *i* to be equal to *j* in the type of *succ*, or even to impose *Nat* not to be universe polymorphic.

In order to solve this problem, we added to PREDICATIVIZE the possibility of adding constraints by the user, in such a way that we can for instance impose *Nat* to be in $U_z$, or *i* = *j* in the type of the successor. Adding constraints can also be useful to help the unification algorithm.

## Rewrite rules

The algorithm that we presented and proved correct covers two types of entries: definitions and constants. This is enough for translating proofs written in higher-order logic or similar systems, in which every step either poses an axiom or makes a definition or proof.

However, when dealing with full-fledged type theories, such as those implemented by COQ or MATITA, which also feature inductive types, it is customary to use rewrite rules to encode recursion and pattern matching. If we simply ignore these rules when performing the translation, we would run into problems as the entries that appear after may need those rewrite rules to typecheck.

Therefore, our implementation extends the presented algorithm and also translate rewrite rules. In order to do this, we use DKCHECK's subject reduction checker to generate constraints and proceed similarly as in the algorithm. Because this feature is still work in progress, this step can require user intervention in some cases. In this case, the user has to manually add constraints over some symbols to help the translation.

## Agda output

PREDICATIVIZE produces files in UPP, which is a subsystem of the encoding of AGDA. In order to translate these files to AGDA itself, we also integrated in PREDICATIVIZE a translator that performs a simple syntactical translation from the AGDA encoding in DEDUKTI to AGDA. For instance, make test_agda_with_typecheck translates Fermat's Little Theorem proof from HOL to AGDA and typechecks it.

## 8 Translating Matita's arithmetic library to Agda

We now discuss how we used PREDICATIVIZE to translate MATITA's arithmetic library to AGDA. The translation is summarized in Figure 7, where DK[X] stands for the encoding of system X in DEDUKTI.
<figure><img src="image_6.png" /><figcaption>Figure 7 Diagram representing the translation of MATITA’s arithmetic library into AGDA.</figcaption></figure>

MATITA’s arithmetic library was already available in DEDUKTI thanks to KRAJONO [2], a translator from MATITA to the encoding DK[Matita] in DEDUKTI. Therefore, the first step of the translation was already done for us.

Then, using PREDICATIVIZE we translated the library from DK[Matita] to DK[Agda] (which is a supersystem of UPP). As the encoding of MATITA’s recursive functions uses rewrite rules, their translation required some user intervention to add constraints over certain symbols, as mentioned in the previous section. Once this step is done, the library is known to be predicative, as it typechecks in DK[Agda].

We then used PREDICATIVIZE to translate these files to AGDA files. However, because the rewrite rules in the DEDUKTI encoding cannot be translated to AGDA, and given that they are needed for typechecking the proofs, the library does not typecheck directly.

Therefore, to finish our translation we had to define the inductive types and recursive functions manually in AGDA. This step of our translation admittedly requires some time, however the effort is orders of magnitude less than rewriting the whole library in AGDA, specially given that the great majority of the library is made of proofs, whose translations we did not need to change. Note that this manual step is not exclusive to our work as it is also needed in [23].

Defining inductive types also required us to add constraints. For instance, we saw in Example 24 that the successor symbol is translated as *succ* : Πi : Level.El<ι ⊑ j> ((Nat i ) ↪ → i,j (Nat j )), but in order to be able to implement this symbol as a constructor of an inductive type, we need to impose i = j . If one then wishes to align *Nat* with the built-in type of natural numbers in AGDA, we would also have to impose i = z , which would then allow us to replace *Nat* by the built-in type in the result of the translation.

The result of this translation is available at https://github.com/thiagofelicissimo/
matita_lib_in_agda and, as far as we know, contains the very first proofs in AGDA of
Bertrand's Postulate and Fermat's Little Theorem. It also contains a variety of other
interesting results such as the Binomial Law, the Chinese Remainder Theorem, and the
Pigeonhole Principle. Moreover, this library typechecks with AGDA's --safe flag, attesting
that it does not use any unsafe features.

9 Conclusion

We have tackled the problem of sharing proofs with predicative systems, by proposing an
algorithm for it. Our implementation allowed to translate many non-trivial proofs from
MATITA's arithmetic library to AGDA, showing that our algorithm works well in practice.
Our solution uses unification modulo arithmetic equivalence on universe levels. We designed an incomplete algorithm for this problem which is powerful enough for our needs. Still, one can wonder if there is an algorithm which always finds a most general solution when there is one, or if this problem is undecidable. One could improve our algorithm by using ACUI unification to solve constraints not containing s. However, there are problems with most general unifiers that would also not be handled by this extension. AGDA also features an algorithm for solving level variables which uses an approach different from ours, but it does not seem to have been formalized in the literature. Therefore, the question if such an algorithm exists seems to be open.

For future work, we would also like to look at possible ways of making PREDICATIVIZE less dependent on user intervention. In particular, the translation of inductive types and recursive functions involves some considerable manual work. Thus if we want to be able to translate larger libraries, there is definitely a need for automating this step.

References

1 Andrea Asperti and Wilmer Ricciotti. A proof of bertrand's postulate. *Journal of Formalized Reasoning*, 5(1):37-57, 2012.

2 Ali Assaf. *A framework for defining computational higher-order logics*. These, École polytechnique, September 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303.

3 Ali Assaf, Guillaume Burel, Raphaël Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, P Halmagrand, O Hermant, and R Saillard. Dedukti: a logical framework based on the λπ-calculus modulo theory. Unpublished, 2016.

4 H. P. Barendregt. *Lambda Calculi with Types*, pages 117-309. Oxford University Press, Inc., USA, 1993.

5 Michael Beeson, Julien Narboux, and Freek Wiedijk. Proof-checking Euclid. *Annals of Mathematics and Artificial Intelligence*, page 53, January 2019. doi:10.1007/s10472-018-9606-x.

6 F. Blanqui. Rewriting modulo in deduction modulo. In *Proceedings of the 14th International Conference on Rewriting Techniques and Applications*, Lecture Notes in Computer Science 2706, 2003. 15 pages. doi:10.1007/3-540-44881-0_28.

7 F. Blanqui. Definitions by rewriting in the calculus of constructions. *Mathematical Structures in Computer Science*, 15(1):37-92, 2005. doi:10.1017/S0960129504004426.

8 Frédéric Blanqui. *Théorie des types et réécriture. (Type theory and rewriting)*. PhD thesis, University of Paris-Sud, Orsay, France, 2001. URL: https://tel.archives-ouvertes.fr/tel-00105522.

9 Frédéric Blanqui. Type safety of rewrite rules in dependent types. In *5th International Conference on Formal Structures for Computation and Deduction*, 2020.

10 Frédéric Blanqui. Encoding type universes without using matching modulo AC. In *Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction*, Leibniz International Proceedings in Informatics 228, 2022. doi:10.4230/LIPIcs.FSCD.2022.24.

11 Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, *6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)*, volume 195 of *LIPIcs*, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.20.

12 Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In Simona Ronchi Della Rocca, editor, *Typed Lambda Calculi and Applications*, pages 102-117, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.

13 Tristan Delort. Importer les preuves de Logipedia dans Agda. Internship report, Inria Saclay Ile de France, November 2020. URL: https://hal.inria.fr/hal-02985530.
19:18 Translating Proofs from an Impredicative Type System to a Predicative One

14 Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1–25:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.25.

15 Gaspard Ferey. *Higher-Order Confluence and Universe Embedding in the Logical Framework*. These, Université Paris-Saclay, June 2021. URL: https://tel.archives-ouvertes.fr/tel-03418761.

16 Guillaume Genestier. Encoding agda programs using rewriting. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 31:1–31:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.FSCD.2020.31.

17 Yoan Géran. Euclid's elements book 1 in dedukti. URL: https://github.com/Karnaj/sttfa-
geocoq_euclid [cited 2022].

18 Robert Harper and Robert Pollack. Type checking with universes. *Theor. Comput. Sci.*, 89(1):107–136, August 1991. doi:10.1016/0304-3975(90)90108-T.

19 R. Saillard. *Type checking in the Lambda-Pi-calculus modulo: theory and practice*. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.

20 Ronan Saillard. *Type checking in the Lambda-Pi-calculus modulo: theory and practice*. PhD thesis, PhD thesis, Mines ParisTech, France, 2015.

21 Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in coq. In *International Conference on Interactive Theorem Proving*, pages 499–514. Springer, 2014.

22 Agda Development Team. Agda 2.6.2.1 documentation. URL: https://agda.readthedocs.io/en/v2.6.2.1/index.html [cited 2022].

23 François Thiré. Sharing a library between proof assistants: Reaching out to the HOL family. In Frédéric Blanqui and Giselle Reis, editors, *Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice*, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018, volume 274 of EPTCS, pages 57–71, 2018. doi:10.4204/EPTCS.274.5.

24 François Thiré. *Interoperability between proof systems using the logical framework Dedukti*. PhD thesis, ENS Paris-Saclay, 2020.

A Typing rules for Dedukti and basic metaproperties

We recall the following basic metaproperties of DEDUKTI. Proofs can be found in [8, 19].

► **Theorem 25** (Basic metaproperties).

1. *Weakening:* If $\Sigma; \Gamma \vdash M : A, \Gamma \subseteq \Gamma'$ and $\Sigma; \Gamma' \text{ well-formed then } \Sigma; \Gamma' \vdash M : A$

2. *Substitution Lemma:* If $\Sigma; \Gamma, x : B, \Gamma' \vdash M : A$ and $\Sigma; \Gamma \vdash N : B$ then $\Sigma; \Gamma, \Gamma' \{N/x\} \vdash M \{N/x\} : A \{N/x\}$

3. *Well-sortedness:* If $\Sigma; \Gamma \vdash M : A$ then either $A = \mathbf{Kind}$ or $\Sigma; \Gamma \vdash A : s$ for $s = \mathbf{Type}$ or $\mathbf{Kind}$.

4. *Subject reduction of $\delta$:* If $\Sigma; \Gamma \vdash M : A$ and $M \to_{\delta} M'$ then $\Sigma; \Gamma \vdash M' : A$

5. *Subject reduction of $\beta$:* If injectivity of dependent product holds, then $\Sigma; \Gamma \vdash M : A$ and $M \to_{\beta} M'$ implies $\Sigma; \Gamma \vdash M' : A$.

6. *Contexts are well typed:* If $x : A \in \Gamma$ then $\Sigma; \Gamma \vdash A : \mathbf{Type}$

7. *Signatures are well typed:* If $c : A \in \Sigma$ then $\Sigma; - \vdash A : s$ and if $c : A := M \in \Sigma$ then $\Sigma; - \vdash M : A$

8. Inversion of typing: Suppose $\Sigma; \Gamma \vdash M : A$
   $\quad \begin{array}{lcl} \text{- If } M = x & \text{then } x : A' \in \Gamma & \text{and } A \equiv A' \end{array}$
<figure><img src="image_7.png" /><figcaption>Figure 8 Typing rules for DEDUKTI.</figcaption></figure>

- If $M = c$ then $c : A' \in \Sigma$ and $A \equiv A'$

- If $M = \text{Type}$ then $A \equiv \text{Kind}$

- $M = \text{Kind}$ is impossible

- If $M = \Pi x : A_1.A_2$ then $\Sigma; \Gamma, x : A_1 \vdash A_2 : s$ and $s \equiv A$

- If $M = M_1M_2$ then $\Sigma; \Gamma \vdash M_1 : \Pi x : A_1.A_2$, $\Sigma; \Gamma \vdash M_2 : A_1$ and $A_2\{M_2/x\} \equiv A$

- If $M = \lambda x : B.N$ then $\Sigma; \Gamma, x : B \vdash C : s$, $\Sigma; \Gamma, x : B \vdash N : C$ and $A \equiv \Pi x : B.C$