the system. For instance, in rules for constrained inference such as `infer Prod`, the induction hypothesis gives some $Σ$; $Γ ⊢ t : T$, and we must use validity and subject reduction to ensure that `Prod` na A B, a reduct of T, is a well-formed type.

### 3.3.3 Completeness: Undirected Typing Implies Bidirectional Typing.
In the other direction of the equivalence (PCUIC: `BDFromPCUIC`), we cannot keep the structure of the undirected proof. Indeed, Rule `type_Cumul` can appear at any place in such an undirected proof, which is not allowed in a bidirectional derivation. Thus, the aim here is to ensure that computation can be moved in the typing derivation to places where it is allowed in the bidirectional system. More precisely, we show that uses of cumulativity via Rule `type_Cumul` can be commuted down with the other rules.

**Theorem** `typing inferring Σ Γ t T : wf Σ → Σ ; Γ ⊢ t : T → ∃ T' , Σ ; Γ ⊢ t ▷ T' × Σ ; Γ ⊢ T' ≤ T`.

Let us for instance consider the case of a cumulativity rule on the function in `type_App`, i.e., suppose we have $Σ$; $Γ ⊢ f : T$ and $Σ$; $Γ ⊢ T ≤_a tProd$ na A B and $Σ$; $Γ ⊢ u : A$, so that $Σ$; $Γ ⊢ tApp f u : B\{0 := u\}$. First, the cumulativity can be broken down into a reduction to a product type $Σ$; $Γ ⊢ T ↝ tProd$ na' A' B' and two cumulativities $Σ$; $Γ ⊢ A' ≈_a A$ and $Σ$; $Γ , : na A ⊢ B' ≤_a B$, respectively between domains and codomains. This key point is a strong form of injectivity for type constructor `tProd`, and its proof relies crucially upon confluence. To show that the cumulativity rule can indeed be commuted with `type_App`, we need to show that the three components of the considered cumulativity rule can be integrated into the premises of `infer App`. The reduction is incorporated into the constrained inference premise of `infer App`, the conversion on domains goes into the checking premise, and the cumulativity on codomains is propagated further down.

### 3.3.4 Reaping the Benefits of the Equivalence.
In the end, composing completeness with correctness gives a form of "normalization" of typing derivations to somewhat canonical ones, where computation is delayed as long as possible and is used only in a principled way. More precisely, the structure of a derivation is completely fixed by the term, but because we do not fix a strategy for reduction (see e.g., Rule `infer Prod` in Fig. 7) we can potentially have derivations that have the same structure but differ in how much they reduce types.

The structure of these canonical derivations entails that they have better properties than the undirected ones, and the possibility to obtain one from any undirected derivation consequently ensure meta-theoretical properties of the undirected system that would be much harder to obtain directly.

The first is principality of typing, a version of type uniqueness relaxed to account for cumulativity.<fnref n="17" /> A caveat here: as already mentioned, since we do not impose a reduction strategy in constrained inference, inferred types are not unique up to equality, i.e., inference is not a functional relation. However, we show in (PCUIC: `BDUnique`) that two inferred types $T$ and $T'$ for a given term $t$ can always be reduced to a common reduct $T''$, implying in particular that $T$ and $T'$ are always convertible. As a consequence, any typeable term $t$ has a principal type— one that is minimal with respect to cumulativity amongst all types for $t$—namely (any of) its inferred type.

**Theorem** `inferring_unique Σ Γ t T`:
wf Σ → wf_local Σ Γ → Σ ; Γ ⊢ t ▷ T → Σ ; Γ ⊢ t ▷ T' → ∃ T'', Σ ; Γ ⊢ T ↝ T'' × Σ ; Γ ⊢ T' ↝ T''.

**Corollary** `inferring_unique' Σ Γ t T T`:
wf Σ → wf_local Σ Γ → Σ ; Γ ⊢ t ▷ T → Σ ; Γ ⊢ t ▷ T' → Σ ; Γ ⊢ T ≈_s T'.

This property is crucial for the work on erasure, as it ensures we can unambiguously assign ‘its’ sort to a term, so erasing all terms whose sort is `tProp` is properly defined. While it was already

<footnote n="17">¹⁷Or, more generally, subtyping.</footnote>
Fixpoint lsp₀ (fuel:N) (s : VSet) (x z : V) : option Z :=
  let base := if V.eq_dec x z then Some 0 else None in
  match fuel with
  | 0 ⇒ base
  | S fuel ⇒
    match mem x s with
    | true ⇒ let ds := map (fun ' (n, y) ⇒ Some n + lsp₀ fuel (remove x s) y z) (succs x) in
        fold_left max ds base
    | false ⇒ base
  end
end.

Definition lsp s := lsp₀ (cardinal s) s.

where `succs x` computes the list of edges with source `x`. Note that the function goes to option `Z` because there may not be any path between `x` and `y`. Thus, the constructor `None` of option `Z` corresponds to $-\infty$ when extending addition, maximum, and comparison to option `Z`.

We then show that `lsp s x y` is equal to the maximum of weights of simple paths from `x` to `y`.

Lemma lsp_spec_le s x y (p : SPath s x y) : Some (weight p) ≤ lsp s x y.

Lemma lsp_spec_eq s x y n : lsp s x y = Some n → ∃ p : SPath s x y, weight p = n.

With this notion of `lsp`, we can prove that acyclicity is equivalent to the existence of a correct labeling, by showing that acyclicity implies that the weight of the longest simple reflexive path on `x` is 0. This allows us to derive the fact that the labeling induced by the weight of the longest simple path from the root is correct when the graph is acyclic.

Lemma acyclic_lsp s x : acyclic G → lsp s x x = Some 0.

Lemma lsp correctness : acyclic G → correct_labeling (fun x ⇒ option_get 0 (lsp V (s G) x)).

Conversely, we can show that the property of a correct labeling extends to paths, from which we directly conclude that the existence of a correct labeling implies acyclicity of the graph.

Lemma correct_labeling_PathOf l : correct_labeling l →

V x y (p : PathOf G x y), x + weight p ≤ l y.

Lemma acyclic_labeling l : correct_labeling l → acyclic G.

In particular, it gives us a decision procedure to check that a graph is acyclic, by simply checking that `lsp V x x` is 0 for every node `x` in the graph (see §6.2.3). To conclude, we just need to remark that the existence of a correct labeling is equivalent to the existence of a valuation that satisfies the constraints of the graph.

## 4.2 Conversion: Algorithmic presentation with equality and reduction

The specification of cumulativity and conversion of §3.3 is quite far from a decision procedure. First, the transitivity rule `cumul_Trans` can be applied at any time, making an intermediate term appear out of thin air. Second, when looking at conversion, the symmetry rule can always be applied twice, without any progress in the comparison. Finally, when comparing inductive types and constructors, for instance `mkApps` (`tInd` i u) args and `mkApps` (`tInd` i u') args', several rules can be applied and in particular `cumul_Ind` which compares them up to cumulativity and `cumul_App` which compares them as standard constants. Thus, we have some kind of critical pairs in the definition of a cumulativity derivation.
proven before bidirectional typing was added to META-CoQ, the proof was quite involved. And indeed, for some time only a weaker version could be obtained, asserting that if a term had two different types $\Gamma$ and $\Gamma'$ then there existed a third one $\Gamma''$ smaller than both $\Gamma$ and $\Gamma'$.

Another valuable property is strengthening (PCUIC: BDStrengthening) which says that if $\Sigma; \Gamma \vdash t : \Gamma$ and $\Delta$ is a well-formed sub-context of $\Gamma$ containing all variables of $t$, then $t$ is still well typed in the smaller $\Delta$. Although it is not directly used in the rest of the development as of now, it should be a useful stepping stone for proving correctness of various optimizations and tactics. Strengthening is difficult to prove in the undirected setting because a *type_Cumul* rule might introduce a type using arbitrary variables, the whole point of a proof being to show this kind of types can be avoided. In the bidirectional setting, the proof is much simpler as a derivation naturally only uses allowed variables, so that strengthening can be proven by a direct induction.

## 3.4 Fixing Cumulativity for Pattern Matching on Cumulative Inductive Types

*Representing pattern matching.* CoQ's typing rule for `match` is notoriously difficult and obscure, as it has to account for the full generality of inductive types and dependent elimination. In all generality, a pattern-matching node in CoQ's kernel language is presented to the user with the following syntax:<fnref n="18" />

```
match s in I ... x₁ ... as s' return P with
  | c₁ y₁ ... yₙ₁ ⇒ b₁
  ...
  | cₖ y₁ ... yₙₖ ⇒ bₖ
end
```

The `scrutinee s` is the value being matched, which should be of an inductive type `I`, `P` is the return type of the whole pattern matching, and `b₁` to `bₖ` are the branches, one per constructor. The return type `P` can depend on both the indices of the inductive type `I` and the `scrutinee`, corresponding respectively to the `in` and `as` clauses, introducing variables that `P` can use. Similarly, branch `b₁` binds the variables `y₁` to `yₙ₁`, corresponding to the arguments of the constructor.

Historically, these binders had been respectively represented as iterated $\Pi$-types and $\lambda$-abstractions. This is the natural way they are specified in a setting with eliminators, and was kept when transitioning from those to pattern matching in CoQ 6.1. This meant that, contrarily to this user-facing syntax, `P` was actually internally represented as some iterated product type

```
tProd x₁ x₁ ... (tProd xₙ xₙ (tProd s' (mkApps I ([A₁; ... ; Aₙ]+[x₁; ... ; xₙ]+[s']))) P)...
```

and similarly for branches.

*The completeness issue.* Our work on the proof of completeness of the type checker (§3.3.3) led to the discovery of a bug not only in our formalization, but also in the kernel of CoQ.<fnref n="19" /> This bug affected cumulative inductive types from their introduction in CoQ 8.11 until its discovery and fix in CoQ 8.14. It came from an incorrect implementation of the pen and paper development [Timany and Sozeau 2017] which used eliminators rather than pattern matching. This incompleteness in the implementation in turn led to a subject reduction failure: the kernel was unable to recognize that the reduct of a well-typed term was well typed. An example of this is given in Appendix.

In brief, the issue was that the representation of binders using $\Pi$-types and $\lambda$-abstractions led to a comparison of domain types that was wrongly using conversion (as is natural for product types in equivariant cumulativity, see §2.3.4). However, the correct cumulativity check for pattern matching on cumulative inductive types permits the inferred type of the `scrutinee` to be strictly

<footnote n="18">¹⁸See the reference manual.</footnote>

<footnote n="19">¹⁹A precise description of the problem in the kernel is given in issue #13495 in the CoQ bug tracker on GitHub.</footnote>
Inductive "Σ; Γ ⊢ _ ↝ _": term → term → Type :=
| red beta : ∀ na t b a,
   Σ ; Γ ⊢ tApp (tLambda na t b) a ↝ b {0 := a}
| red iota : ∀ ci c u args p brs br,
   nth_error brs c = Some br → #|args| = ci.(ci_npar) + context_assumptions br.(bcontext) →
   Σ ; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ↝ iota_red ci p args br
| ... (** Other computation rules are similar *)
| abs red_1 : ∀ na ty ty' t,
   Σ ; Γ ⊢ ty ↝ ty' → Σ ; Γ ⊢ tLambda na ty t ↝ tLambda na ty' t
| abs red_r : ∀ na ty t t',
   Σ ; Γ , na : ty ⊢ t ↝ t' → Σ ; Γ ⊢ tLambda na ty t ↝ tLambda na ty' t
| ... (** Other congruence rules are similar **)

Inductive "Σ ⊢ _ ≤<sup>R1e</sup><sub>napp</sub> _": term → term → Type :=
| eq_Rel : ∀ n,
   Σ ⊢ tRel n ≤<sup>R1e</sup><sub>napp</sub> tRel n
| eq_Sort : ∀ s s',
   R1e s s' → Σ ⊢ tSort s ≤<sup>R1e</sup><sub>napp</sub> tSort s'
| eq_Lambda : ∀ na na' ty ty' t t',
   eq_binder_annot na na' → Σ ⊢ ty ≤<sup>Re</sup><sub>0</sub> ty' → Σ ⊢ t ≤<sup>R1e</sup><sub>0</sub> t' →
   Σ ⊢ tLambda na ty t ≤<sup>R1e</sup><sub>napp</sub> tLambda na' ty' t'
| eq_App : ∀ t t' u u',
   Σ ⊢ t ≤<sup>sR1e</sup><sub>Snapp</sub> t' → Σ ⊢ u ≤<sup>Re</sup><sub>0</sub> u' →
   Σ ⊢ tApp t u ≤<sup>R1e</sup><sub>napp</sub> tApp t' u'
| eq_Ind : ∀ i u u',
   R_global_instance Σ Re R1e (IndRef i) napp u u' →
   Σ ⊢ tInd i u ≤<sup>R1e</sup><sub>napp</sub> tInd i u'
| ... (** Other cumulativity and congruence rules are similar **)

<caption>Fig. 5. Single step reduction and syntactical equality up to universes (excerpt)</caption>

To remedy this issue, it is common to decide conversion by using reduction instead. The idea
is that two terms are convertible if and only if they can both be reduced to the same term. In the
presence of universe polymorphism and cumulativity, the notion of “same term” needs to be relaxed
to syntactical equality up to universes.

In this section we define an algorithmic notion of cumulativity based on reduction and show
that it is indeed equivalent to cumulativity defined in §3.3 and given in full in Figs. 19 and 20. The
main technical ingredient of the proof is confluence of reduction.

4.2.1 Reduction and Syntactic Equality up to Universes. Single step reduction of PCUIC terms is defined in Fig. 5, and written Σ ; Γ ⊢ t ↝ u. We only show representative cases, as the definition shares a lot with the definition of cumulativity. Basically, reduction corresponds to the computation and congruence rules of cumulativity. For computation rules, they are literally the same, as the reader can check on red beta and red iota. Congruence rules however are slightly different because we do not want the reduction to be parallel, as we are defining one-step reduction, so we need a rule per argument of a constructor. For instance, in the case of tLambda, there are two rules: abs_red_1 which reduces the type annotation, and abs_red_r which reduces the body of the lambda.
smaller than the expected type of the argument of the return type. Thus, using a generic encoding of the return type as a Π-type was incorrect.

*The change in CoQ.* The easy fix, which simply replaced conversion by cumulativity in this particular function, was quickly implemented once the issue was found.<fnref n="20" />

However, the more principled solution in the long run was to change the case representation to store the parameters and universe instance separately from the return predicate and branches, completely removing the usage of Π and λ binders that caused the issue in the first place. In this new representation, corresponding to the typing rules given in §2.5, the return type P is directly represented as a term, implicitly well defined in an extended context which is computed from the information stored in the pattern-matching node. This representation of cases, is more efficient, as the context of the predicate and branches no longer need to be stored, since they can canonically be derived from the inductive declaration and the stored parameters and universe instance. Only the user-specified binding annotations for these contexts are kept for pretty-printing.

This change had already been proposed by Herbelin,<fnref n="21" /> but was only finally implemented in CoQ's kernel by Pédrot<fnref n="22" /> for CoQ 8.14, following our discovery of the bug. The kernel representation moreover becomes closer to user syntax in which the types in these contexts are never displayed. This also fixes unintuitive behaviors of occurrence selection in tactics, since before the change tactics could find occurrences in parts of the term that the user couldn't see, namely the type of binders that were removed. Overall, the typing rule for match becomes simpler and closer to its bidirectional version, making explicit the flow of information between the inferred type of the scrutinee and the stored parameters and universe instance.

# 4 METATHEORY OF PCUIC

To implement a type checker for PCUIC and prove it correct, it is necessary to also formalize most of its metatheory. Indeed, the certified checker relies for instance on *confluence*, *subject reduction*, and *strong normalization* of the reduction.

In this section, we explain how confluence of the conversion can be derived using the Tait-Martin-Löf-Takahashi methodology [Takahashi 1989] extended to cover not only β-reduction, but also pattern-matching, (co)fixpoints and let-bindings. In particular, parallel reduction in our setting can also reduce contexts. From this confluence proof, we derive many important properties, such as *validity* (the fact that the type in a typing derivation can itself be typed, sometimes called presupposition), as well as *subject reduction* and *canonicity*.

As already mentioned in the introduction, because of Gödel's second incompleteness theorem, strong normalization (SN) of PCUIC cannot be proven inside CoQ. Barras [2012] went as far as possible in this direction, showing that one can prove in CoQ, for the Calculus of Constructions extended with natural numbers and a sized-typing discipline, both a relative consistency proof with Intuitionistic Zermelo-Fraenkel Set Theory with Grothendieck universes, and SN using a reducibility candidates technique. The generalization of this method to the full CIC remains a research problem. Alternatively, Abel et al. [2018a] prove SN for a (predicative) restriction of the same system in AGDA extended with inductive-recursive types, whose logical strength is a priori much higher. We see these rather strong results as evidence that it is consistent to *assume strong normalization* for PCUIC, and use it to derive consistency of PCUIC and standardization theorems which are useful for erasure.

<footnote n="20">²⁰In CoQ PR #13501.</footnote>

<footnote n="21">²¹In the CoQ enhancement proposal #34.</footnote>

<footnote n="22">²²In CoQ PR #13563.</footnote>
<figure><img src="image_1.png" /><figcaption>Fig. 6. Algorithmic cumulativity</figcaption></figure>

From this single step reduction, general reduction is simply defined as its reflexive and transitive closure.

Notation $\Sigma; \Gamma \vdash t \stackrel{\sim}{\to}^* u := \mathrm{clos\_refl\_trans}(\mathrm{fun}\ t\ u: \mathrm{term} \Rightarrow \Sigma; \Gamma \vdash t \stackrel{\sim}{\to} u)$.

The fundamental property that reduction satisfies is confluence. Its proof is involved and requires several auxiliary notions, so we defer its explanation to § 5. However, let us just state the relevant result for this section: reduction is confluent on well-scoped terms (that is terms whose variables are bound in the local context Γ).

Lemma red_confluence Γ (t : open_term Γ) uv :
$$ \Sigma; \Gamma \vdash t \stackrel{\sim}{\to}^* u \to \Sigma; \Gamma \vdash t \stackrel{\sim}{\to}^* v \to \{v' \& \Sigma; \Gamma \vdash u \stackrel{\sim}{\to}^* v' + \Sigma; \Gamma \vdash v \stackrel{\sim}{\to}^* v'\}. $$

Syntactic equality up to universes is also defined in Fig. 5, and written $\Sigma \vdash t \stackrel{\leq}{\leq}^{R1e}_{n_{app}} u$. Basically, it contains the cumulativity and congruence rules of cumulativity. Note that syntactical equality does not depend on a local context because variables are compared syntactically (Rule eq_Rel), but it depends on a relation R1e comparing universes and a natural number n_app. The index R1e is used in the exact same way as for cumulativity, to compare universes and inductive types up to cumulativity. The index n_app deserves more explanation.

Because we want the algorithmic specification to be closer to a decision procedure, we do not want to have the critical pairs that we have for the specification of cumulativity/conversion. This means that to compare mkApps (tInd i u) args and mkApps (tInd i u') args' we always want to use congruence of application (Rule eq_App). As such, the congruence rule eq_Ind for tInd needs to account for cumulativity. However, we have an issue here because the cumulativity rule only applies to fully applied inductive types. This is why we need to store the number of applications that we have traversed during the syntactic equality check: this is the exact purpose of the n_app index.

Indeed, Rule eq_App increments the index in the premise of the applied functions (here $\Sigma \vdash t \stackrel{\leq}{\leq}^{SRel}_{Sn_{app}} t'$). Note that the index is reset to 0 for the premise on the arguments of the application.

Using this information, the predicate R_global_instance decides if two applications of a polymorphic cumulative inductive type are in the cumulativity relation. For this to hold, n_app should match the arity of the reference, u and u' should have equal lengths and the universe constraints corresponding to the variance relations declared for the reference's universe arguments applied to u, u' should hold in the universe context.

For other congruence rules, such as eq_Lambda, n_app is reset to 0 in the premise to account for the fact that we are not under an n-ary application.

It is not difficult to show that syntactical equality up to universes is reflexive, symmetric and transitive as soon as the relations Re and R1e comparing universes are as well.
## 4.1 Accessibility and Well-Founded Induction

In our development, we heavily rely on well-foundedness, both to state and use normalization, and to define functions by well-founded induction when structural induction as available natively in CoQ's guard checking is not enough.

While well-foundedness of a relation is classically stated as the absence of infinite descending chain, this negative statement is too weak in a constructive setting. Instead, we use the usual constructive reformulation [Paulson 1986], which says that all descending paths are finite. This is expressed using the accessibility predicate Acc associated with a relation, defined as follows:

Inductive Acc (A : Type) (R : A → A → Prop) (x : A) : Prop :=
| Acc_intro : (∀ y : A, R y x → Acc R y) → Acc R x.

In words, an element x of A is accessible whenever all R-smaller elements are themselves accessible. A relation R : A → A → Prop is well founded whenever every element of A is accessible, i.e., whenever ∀ a : A, Acc R a. However, accessibility is more precise, as it is ‘local’ in the sense that it asserts a property of a single element of a type.

This inductive accessibility predicate directly translates to well-founded recursion: its eliminator says that to define a function f on an accessible x : A, one can access recursive calls on all R-smaller elements. Crucially, while accessibility is a Prop-valued relation, CoQ's subsingleton criterion allows to eliminate it into the Type sort. This means we can define functions by well-founded recursion, but have this proof of termination erased during extraction, providing an extracted function which is guaranteed to terminate<fnref n="23" /> but does not compute an uninformative proof of accessibility, avoiding a huge performance loss.

## 4.2 Substitution and Weakening

The implemented calculus uses standard de Bruijn lifting and (parallel) substitution operations. As a first step towards formalizing the metatheory of PCUIC, we need to show that reduction, cumulativity and typing are all closed by lifting (a property usually called weakening or thinning) and substitution operations.

Working with this traditional presentation of de Bruijn indices goes a long way, however we hit a difficulty when formalizing more complex operations on syntax, such as parallel reduction for proving confluence. To alleviate the difficulties associated with reasoning on the primitive operations, we provide a version of the σ-calculus operations [Abadi et al. 1991; Schäfer et al. 2015] on terms.

The σ-calculus operations enjoy a rich, clean and decidable equational theory, equivalent to an explicit substitution calculus, and are able to express complex commutations neatly—compared to the tricky lifting and substitution lemmas of “traditional” de Bruijn representations.

### 4.2.1 The σ-calculus

The two primitives of the σ-calculus correspond to generalizations of lifting and substitution to an infinitary setting whose corresponding types are:

Definition renaming := N → N.

Definition substitution := N → term.

Renaming corresponds to a generalization of lifting where the action of a renaming f, written rename f, on a de Bruijn variable tRel n is defined by tRel (f n). Similarly, the action of an infinitary substitution σ, written _-[σ] and called instantiation, on a de Bruijn variable tRel n is defined by σ n. In both cases, this action on variables is lifted to arbitrary terms by congruence.

<footnote n="23">²³To be precise, this only applies to inputs that satisfy potentially erased preconditions. For instance, our weak-head reduction machine is only guaranteed to terminate on well-typed terms.</footnote>
### 4.2.2 Algorithmic cumulativity and its properties.
Algorithmic cumulativity between two terms is defined as the fact that these two terms reduce to terms that are syntactically equal up to universes (see Fig. 6).

We now turn to the proof that this algorithmic presentation of cumulativity is equivalent to the abstract specification. Thus, algorithmic cumulativity provides a crucial intermediate point between the abstract specification and the concrete implementation of cumulativity/conversion.

To show that algorithmic cumulativity implies the abstract specification, we only have to show that all the rules of reduction and syntactic equality up to universes are admissible rules of the abstract specification.

For reduction, this is fairly straightforward, as the computation rules are literally the same, the only remaining work is to use reflexivity of the abstract specification to be able to encode the non-parallel congruence rule of reduction.

**Proposition red cumulSpec Γ t u : Σ ; Γ ⊢ t ↦→ u → Σ ; Γ ⊢ t ≈_s u.**

The proof that the rules of syntactic equality up to universes are admissible requires to state a more general lemma that essentially checks that the $n_{app}$ index of syntactic equality is computing the number of applications in the right way.

**Proposition eq\_term\_upto\_univ\_cumulSpec (Γ : context) {Re R1e} t u args args' :**

$$ \Sigma \vdash t \leq_{\#|args|}^{R1e} u \rightarrow \text{All2 (fun t u \Rightarrow \Sigma; \Gamma \vdash t \leq_s^{Re} u) args args'} \rightarrow $$

$$ \Sigma ; \Gamma \vdash \text{mkApps t args} \leq_s^{R1e} \text{mkApps u args'.} $$

Then, the fact that syntactic equality up to universes implies the abstract specification of cumulativity is a direct consequence, when args and args' are the empty list.

From this, we can conclude directly that algorithmic cumulativity is correct, using transitivity of the abstract specification.

**Proposition cumulAlgo\_cumulSpec R1e Γ (t u : term) : Σ ; Γ ⊢ t ≤_a^{R1e} u → Σ ; Γ ⊢ t ≤_s^{R1e} u.**

For the opposite direction, the situation is more complicated as we need to show that some rules, such as reflexivity, transitivity or symmetry, which are not at all present in the definition of algorithmic cumulativity, are nevertheless admissible. As already mentioned, this strongly relies on the fact the reduction is confluent, but only on well-scoped terms (see § 5.3 for a counter-example of unconditional confluence). This means that completeness of algorithmic cumulativity only holds for well-scoped terms, but not for arbitrary ill-scoped terms. Fortunately, type checking only calls cumulativity checking on well-typed terms, which are in particular well scoped, so this conditional completeness is enough for our purpose.

To understand why confluence is a key property, consider three (well-scoped in Γ) terms t, u and v, such that $\Sigma ; \Gamma \vdash t \leq_a^{R1e} u$ and $\Sigma ; \Gamma \vdash u \leq_a^{R1e} v$. It may be the case that this holds because $\Sigma ; \Gamma \vdash u \rightsquigarrow t$ and $\Sigma ; \Gamma \vdash u \rightsquigarrow v$. But then, as the reduction is not deterministic, there is no reason for t and v to be syntactically equal (up to universes) (for instance, one reduction could use Rule `cumul_red_1` while the other could come from Rule `cumul_red_r`), so the only sensible way to show transitivity in this case is to have confluence and get a common reduct $\rho(u)$ from t and v. This way, in our example $\Sigma ; \Gamma \vdash t \leq_a^{R1e} v$ holds by using Rules `cumul_red_1`, `cumul_red_r` and reflexivity on $\rho(u)$.

In fact, we have been able to show that this particular situation generalizes to the arbitrary case, so that confluence of reduction is enough to deduce transitivity of algorithmic cumulativity (on well-scoped terms). Beyond confluence, we also need that reduction and syntactic equality up to universes behave well with respect to each other. More precisely, we show that the latter is a simulation with respect to the former:
Class GuardCheckerCorrect := {
  guard_red b Σ Γ mfix mfix' idx :
    Σ ; Γ ⊢ tFixCoFix b mfix idx ↦→ tFixCoFix b mfix' idx →
  guard b Σ Γ mfix → guard b Σ Γ mfix' ;
  guard_extendsb Σ Σ' Γ mfix :
    extends Σ Σ' →
    guard b Σ Γ mfix → guard b Σ' Γ mfix ;
  guard_inst b Σ Γ Δ mfix σ :
    Σ ; Γ ⊢ σ : Δ →
    guard b Σ Δ mfix → guard b Σ Γ (inst_mfix mfix σ ) ;
  guard_renamb P Σ Γ Δ mfix f :
    renaming P Γ Δ f →
    guard b Σ Δ mfix → guard b Σ Γ (rename_mfix mfix f ) }.

<caption>Fig. 8. Correctness of the guard checker with respect to the calculus (excerpt)</caption>

In the σ -calculus, a renaming can be turned into a substitution by post-composition with the variable constructor tRel, both having the same action on terms. Moreover, the theory enjoys nice properties such as the fact that the action of renaming commutes with composition. This lets us prove stability of typing under a closed renaming (that is, when the renaming maps each variable in the source context to one with the same type in the target context) and under instantiation with a well-typed substitution (where well-typedness of a substitution is defined pointwise on the context with the additional check that let-binding are preserved).

Lemma typing_rename Σ Γ Δ f t A :
wf Σ → wf_local Σ Δ →
renaming_closed Γ Δ f →
Σ ; Γ ⊢ t : A →
Σ ; Δ ⊢ rename f t : rename f A .

Lemma typing_inst Σ Γ Δ σ t A :
wf Σ → wf_local Σ Δ →
Σ ; Δ ⊢ σ : Γ →
Σ ; Γ ⊢ t : A →
Σ ; Δ ⊢ t.[σ] : A.[σ].

The **weakening** and **substitution** theorems, formulated without the **σ**-calculus primitives, are direct consequences of their more abstract counterparts, but more directly usable. The global environment also induces a form of weakening by the addition of new inductive or constant declarations (PCUIC: **WeakeningEnv**), simpler from the point of view of typing but trickier w.r.t. universe instantiation (PCUIC: **UnivSubstitutionTyp**). Still, in both cases we show that typing is also stable by these operations.

4.2.2 Correctness of the Guard Checker. Stability of typing under renaming and substitution actually depends on correctness properties of the guard condition. Indeed, for those metatheoretical properties to hold, the guard condition needs to satisfy corresponding stability properties. This can be seen as a guideline on how to implement a guard condition properly. Indeed, we want the guard condition to imply normalization of the theory, but we also want it not to break subject reduction for instance.

The class GuardCheckerCorrect (Fig. 8) summarizes the properties that a guard condition needs to satisfy to preserve good metatheoretical properties. It says that the guard condition must be stable by reduction, context extension, instantiation and renaming. There are also conditions of stability by α -renaming, cumulativity (at the level of contexts) and universe substitution, but those condition are mainly technical.
Lemma red<sub>1</sub>_eq_term_upto_univ_l {ΣΣ' : global_env} Re Rle n<sub>app</sub> Γ u v u':

$$ \Sigma' \vdash u \leq_{\text{napp}}^{\text{Rle}} u' \rightarrow \Sigma; \Gamma \vdash u \rightsquigarrow v \rightarrow \exists v', \Sigma; \Gamma \vdash u' \rightsquigarrow v' \times \Sigma' \vdash v \leq_{\text{napp}}^{\text{Rle}} v'. $$

For the rest of the rules of the abstract specification of cumulativity, things are a bit simpler. Computation rules are directly mimicked by the corresponding rules for the reduction, and cumulativity rules are directly related to corresponding rules for the syntactic equality up to universes. Finally, congruence rules are obtained by using corresponding congruence rules for both reduction and syntactic equality up to universes. Of course, to prove that all those rules are admissible, there is a fair amount of bureaucratic proof obligations popping up, but they are not particularly informative and we refer the curious reader to the formalization for details.

Armed with all those admissible rules, it is now easy to prove completeness of algorithmic cumulativity.

Proposition cumulSpec cumulAlgo Rle Γ (t u : open_term Γ) : Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Rle</sup> u → Σ ; Γ ⊢ t ≤<sub>d</sub><sup>Rle</sup> u.

## 4.3 Bidirectional Typing

The last step to go from the abstract specification to an algorithmic specification is to deal with typing derivations (§3.5). We will call them undirected when needing to distinguish it from the other judgments we are about to introduce.

The main difficulty here is Rule type_Cumul. Indeed, similarly to transitivity for cumulativity, it can be used at any point in a typing derivation and involve an arbitrary type that cannot be “invented” by an algorithm. However, we cannot completely remove the rule, as we still need to retain the possibility to use computation on types inside derivation trees. Instead, we distribute computation in two ways: we keep the possibility to use cumulativity between types, at specific places where both types are known; and we allow reduction in order to expose the head constructor of a type.

The structure of this judgement system is directly inspired by the actual kernel. In particular, we introduce a separation between the checking judgement, which expects a type as input, and the inference one, which instead outputs a type. This separation is the characteristic of so-called bidirectional typing algorithms, see the survey by Dunfield and Krishnaswami [2021] for an overview, and so this is also the name we adopt for this judgement.<fnref n="19" />

Moreover, the kernel of Coq maintains the invariant that inputs to the type checker are always well formed—apart, of course, for the term whose typing is under scrutiny. Conversely, outputs of type inference, and in particular inferred types, are always well formed. Those principles manifest in the proof of equivalence between the bidirectional and undirected system, as we will explain in §4.3.2.

Standalone work [Lennon-Bertrand 2021, 2022], centered mainly around bidirectional typing in the context of CIC/PCUIC, has already appeared. We present here the most interesting points for META-Coq, but more details and general intuitions can be found in those works.

### 4.3.1 The Bidirectional Typing Judgement.
Some rules of the bidirectional typing judgment are presented in Fig. 7. They are at the same time quite similar to the rules of §3.5 but with subtle albeit important differences, let us go through those.

<footnote n="19">¹⁹The literature on bidirectional dependent typing [Graitzer et al. 2019; McBride 2018; Norell 2007] often focuses on the setting where destructor forms, such as application, infer, but constructor forms, such as λ-abstractions, can only check. This is however not our approach here: instead, our terms pack enough information to always infer types, as this is the path taken by Coq’s kernel. Still, given the importance of the infer/check distinction, we still feel our presentation belongs to the bidirectional world.</footnote>
Inductive Γ, _ ⇒ Δ, _ : term → term → Type :=

| pred_beta na t₀ t₁ b₀ b₁ a₀ a₁ :

Γ, t₀ ⇒ Δ, t₁ → (Γ, na : t₀), b₀ ⇒ (Δ, na : t₁), b₁ → Γ, a₀ ⇒ Δ, a₁ →

Γ, tApp (tLambda na t₀ b₀) a₀ ⇒ Δ, b₁ {0 := a₁}

| pred_zeta na d₀ d₁ t₀ t₁ b₀ b₁ :

Γ, t₀ ⇒ Δ, t₁ → Γ, d₀ ⇒ Δ, d₁ → (Γ, na := d₀ : t₀), b₀ ⇒ (Δ, na := d₁ : t₁), b₁ →

Γ, tLetIn na d₀ t₀ b₀ ⇒ Δ, b₁ {0 := d₁}

| pred_rel_def_unfold i body :

Γ ⇒ ctx Δ → option_map decl_body (nth_error Δ i) = Some (Some body) →

Γ, tRel i ⇒ Δ, lift₀ (S i) body

| pred_rel_refl i :

Γ ⇒ ctx Γ' → Γ, tRel i ⇒ Γ', tRel i

| pred_delta c decl body (isdecl : declared constant Σ c decl) u :

Γ ⇒ ctx Δ → decl.(cst_body) = Some body → Γ, tConst c u ⇒ Δ, body@[u]

| pred_app M₀ M₁ N₀ N₁ :

Γ, M₀ ⇒ Δ, M₁ → Γ, N₀ ⇒ Δ, N₁ → Γ, tApp M₀ N₀ ⇒ Δ, tApp M₁ N₁

(* other cases are omitted *)

Inductive Γ,_,− ⇒ subst Γ',_,− : list term → context → list term → context → Type :=

| psubst_empty : Γ, [], [] ⇒ subst Γ', [], []

| psubstₐ Δ Δ' s s' na na' t t' T T' :

Γ, s, Δ ⇒ subst Γ', s', Δ' → (Γ ++ Δ), T ⇒ (Γ' ++ Δ'), T' → Γ, t ⇒ Γ', t' →

Γ, (t :: s), (Δ, na : T) ⇒ subst Γ', (t' :: s'), (Δ', na' : T)

| psubst₉ Δ Δ' s s' na na' t t' T T' :

Γ, s, Δ ⇒ subst Γ', s', Δ' → (Γ ++ Δ), T ⇒ (Γ' ++ Δ'), T' → Γ, (subst₀ s t) ⇒ Γ', (subst₀ s' t') →

Γ, (subst₀ s t :: s), (Δ, na := t : T) ⇒ subst Γ', (subst₀ s' t' :: s'), (Δ', na' := t' : T').

<caption>Fig. 9. Definition of *parallel reduction* (assuming a global environment Σ)</caption>

## 4.3 Confluence

Following the Tait-Martin Löf method [Takahashi 1989], we define *parallel reduction* for PCUIC, written as Γ, t ⇒ Δ, t', in Fig. 9. This reduction is just a variant of reduction Σ ; Γ ⊢ t ↛ t' where already present redexes can all be reduced together in one single step. Note that the global environment Σ is a parameter of the reduction and not an index because it is fixed during the reduction. Note that a β-redex can be reduced or not, depending on whether the reduction rule pred_beta or congruence rule pred_app is used. We also add a reflexivity rule for atoms (variables which may not be reduced, universes, inductive types and constructors), thus ensuring that parallel reduction is reflexive.

4.3.1 *Well-Scoped Terms.* The correct representation of pattern matching for cumulative inductive types (§3.4) introduces a subtle issue which has to do with confluence. The term

tCase ... (tApp (tConstruct <T> 0 [] ) (tInd <N> []))

[( { decl_name := { | binder_name := "x"; binder_relevance := Relevant } |; decl_body := Some (tRel 0); ... |}, tRel 0) ]
Inductive "Σ ; Γ ⊢ _ ▷ _" : term → term → Type :=

| infer_Rel n decl :

nth_error Γ n = Some decl →

Σ; Γ ⊢ tRel n ▷ lift₀ (S n) (decl_type decl)

| infer_Sorts s :

wf_universe Σ s →

Σ; Γ ⊢ tSort s ▷ tSort (Universe.super s)

| infer_Lambda na A t s B :

Σ; Γ ⊢ A ▷ □ s →

Σ; Γ, na : A ⊢ t ▷ B →

Σ; Γ ⊢ tLambda na A t ▷ tProd na A B

| infer_App t na A B u :

Σ; Γ ⊢ t ▷ Π (na,A,B) →

Σ; Γ ⊢ u ◁ A →

Σ; Γ ⊢ tApp t u ▷ B{0 := u}

| ... (**Other inference rules are similar**)

with "Σ ; Γ ⊢ _ ▷ Π ( _ , _ , _ )" : term → aname → term → term → Type :=

| inferProd_Prod t T na A B :

Σ; Γ ⊢ t ▷ T →

Σ; Γ ⊢ T ↝ tProd na A B →

Σ; Γ ⊢ t ▷ Π (na,A,B)

with ... (**Other constrained inference judgments are similar**)

with "Σ ; Γ ⊢ _ ◁ _" : term → term → Type :=

| check_Cumul t T T' :

Σ; Γ ⊢ t ▷ T →

Σ; Γ ⊢ T ≲ a T' →

Σ; Γ ⊢ t ◁ T'.

<caption>Fig. 7. Bidirectional typing rules (excerpt)</caption>

First, it is an important feature of PCUIC that terms contain enough information to always infer a type—this is not true of e.g., MLTT as implemented in AGDA. In particular, our λ-abstractions are always annotated with their types. This is reflected here by the fact that each typing rule from § 3.5—apart from type_Cumul that we will treat separately later—gives rise to a type inference rule. Rules for variables, sorts, abstractions and application should be enough to give a feel of how we adapt § 3.5. We write inference Σ ; Γ ⊢ t ▷ T, and think of T as an output, even though the relation is not a function.

None of the rules for inference, however, play the role that Rule type_Cumul plays in undirected typing. This is why we define, mutually with inference, other inductive judgments. Together, those rules will cover what can be achieved in undirected typing using Rule type_Cumul, but in a more controlled way.

The first of these judgments is checking, written Σ ; Γ ⊢ t ◁ T. This gives the full power of (algorithmic) cumulativity to compare the type inferred for t and the type T, but the price to pay is that the type T should be considered an input, and not an output as in inference. Thus, care is taken that this
corresponds to match @C N with @C X (x := X) ⇒ x end but the new PCUIC representation now also allows let Y := N in match @C N with @C X (x := Y) ⇒ x end which breaks confluence. The root of the problem comes from the fact that the reduction rule for pattern matching implicitly assumes that the contexts of the branches are well formed, i.e., have the right number of binders. On terms where this is not the case, we can encounter the pathological behavior above.

Thus, we need a property on untyped terms that is enough to regain confluence. A sufficient property is well scoping, which in the case where the term is a pattern-matching node ensures that contexts are properly closed, and forbids the ill-scoped example above. Under this restriction, reduction and substitution properly commute, and confluence is recovered. In what follows, we implicitly assume that all terms are well scoped, although in the Coq formalization, this introduces a significant amount of additional assumption in the theorems and definitions. For instance, this is the technical reason why transitivity of conversion is only allowed to go through a well-scoped term (§2.3.1), as this ensures we can use our confluence property on well-scoped terms.

### 4.3.2 Dealing with Dependent Let-Bindings.
Note that because of let-bindings, we need to take the context explicitly into account during the reduction. This is obtained by adding the `All2_local_env` (`on Decl pred₁`) Γ Γ' predicate in the premises of basic parallel reduction steps (such as the rule `pred_rel_def_unfold` for instance) in order to allow for parallel reduction in the context too.

Thanks to the generalization to contexts, we can prove a strong substitution lemma which says that the parallel reduction satisfies the property that the reductions performed on two terms M and N can also be done in one step on M where its first de Bruijn variable is substituted by N', where N reduces to N' in parallel as well.

**Lemma** `substitution_pred₁ Γ Δ M M' na A A' N N' : wf Σ →`
`Γ, N ⇒ Δ, N' →`
`(Γ, na : A), M ⇒ (Δ, na : A'), M' →`
`Γ, M{0 := N} ⇒ Δ, M'{0 := N'}.`

We actually need a generalized version of this lemma for well-typed substitutions: $Γ ⊢ s : Δ$, where $Δ$ is the context we are substituting into and $Γ$ represents the variables needed to type the substitution $s$. However, as we are doing things in parallel, we need a notion of parallel substitution. To account for let-ins correctly, we need these well-typed substitutions to coherently *preserve* the definiens of local definitions. The parallel substitution structure $Γ, Δ, s ≡^{subst} Γ', Δ', t'$ represents two substitutions $s$ and $t$ typed respectively in $Γ$ and $Γ'$ and instantiating respectively contexts $Δ$ and $Δ'$ (Fig. 9).

Rule `psubstₐ` simply ensures that the two terms $t$ and $t'$ are in the parallel reduction relation, to instantiate two assumptions, the `psubstₐ` rule rather *forces* the substitution to be equal to the appropriately substituted bodies of let-ins. This still allows the reduction of the substituted versions of let-in definiens in the contexts. While types themselves do not participate in reduction, it is essential to also allow their reduction, to get context conversion (of type annotations, not bodies) at the same time as substitution: a context conversion, when restricted to type annotations, is a substitution by the identity. We use mathematical notation rather than Coq for the following theorems to allow for more visual statements.

**THEOREM 4.1 (PARALLEL SUBSTITUTION).** *The stability by substitution of parallel reduction extends to parallel substitution in the following way:*

`Γ, Δ, s ≡^{subst} Γ', Δ', t →`
`(Γ ++ Δ ++ Γ'), M ⇒ (Γ₁ ++ Δ₁ ++ Γ'₁), N →`
`(Γ ++ Γ'[s]), (subst s #|Γ'| M) ⇒ (Γ₁ ++ Γ'₁[s]), (subst s' #|Γ'| N)`
judgment is used only in places where no type has to be invented. For instance, in Rule `infer_App`, the argument can be checked against the domain that has been previously inferred for the function. More generally, checking is only used with a type known from previous hypotheses.

The last kind of judgments we call constrained inference, and it is itself divided into three judgments respectively for sorts, product types and inductive types. These stand between inference and checking. They are similar to inference as they output rather than take an input. But they are similar to checking as they constrain the type to have a certain shape: it should respectively be a sort, a product, or an inductive type (applied to a list of arguments). In Fig. 7 we for instance show constrained inference for products, written $Σ; Γ ⊢ t ⊢ Π$ (na,A,B), and its use in Rule `infer_App` to check whether the function inhabits a product type, and if so output a domain type used to further check the argument. Constrained inference for (co)inductive types is similarly used in destructors (pattern-matching and projections) to see whether the destructed term's type has the right shape. Finally, constrained inference for sorts is used in all places where we want to verify that a term is a type, but do not know what its universe level should be, as for instance in Rule `infer_Lambda`.

### 4.3.2 Correctness: Bidirectional Typing Implies Undirected Typing.
For the first direction of the equivalence between the two forms of typing (PCUIC: `BDToPCUIC`), a bidirectional derivation can be directly erased to an undirected one: inference rules are mapped to their undirected counterparts, and the rules for constrained inference and checking are subsumed by the more flexible `type_Cumul`.

**Theorem** `inferring_typing` $Σ Γ t T :$ `wf Σ → wf_local Σ Γ → Σ; Γ ⊢ t ▷ T → Σ; Γ ⊢ t : T.`

There is however one subtlety: the bidirectional judgment follows the information flow of the algorithm, which never re-checks inputs to be valid, as this invariant is maintained throughout the recursive calls. Thus, the bidirectional derivations lack information that is required in the undirected one. For instance, Rule `check_Cumul` in Fig. 7 does not require the target $T'$ to be a well-formed type, while Rule `type_Cumul` in §3.5 does. Similarly, Rule `infer_Rel` does not demand the context to be well formed, contrarily to Rule `type_Rel`.

Thus, the bulk of the work to prove the correctness theorem `inferring_typing` above is to derive the extra hypotheses of the undirected rules, effectively ensuring that the well-formation invariant of the algorithm is maintained. This appears in the statement, as the fact that $Σ; Γ ⊢ t ▷ T$ implies $Σ; Γ ⊢ t : T$ only when $Γ$ is well formed. This relies in turn on important meta-theoretical properties of the system. For instance, in rules for constrained inference such as `inferProdProd`, the induction hypothesis gives some $Σ; Γ ⊢ t : T$, and we must use validity and subject reduction to ensure that `tProd na A B`, a reduct of $T$, is a well-formed type.

### 4.3.3 Completeness: Undirected Typing Implies Bidirectional Typing.
In the other direction of the equivalence (PCUIC: `BDFromPCUIC`), we cannot keep the structure of the undirected proof. Indeed, Rule `type_Cumul` can appear at any place in such an undirected proof, which is not allowed in a bidirectional derivation. Thus, the aim here is to ensure that computation can be moved in the typing derivation to places where it is allowed in the bidirectional system. More precisely, we show that uses of cumulativity via Rule `type_Cumul` can be commuted down with the other rules.

**Theorem** `typing inferring` $Σ Γ t T :$ `wf Σ → Σ; Γ ⊢ t : T → ∃ T', Σ; Γ ⊢ t ▷ T' × Σ; Γ ⊢ T' ≤_a T.`

Let us for instance consider the case of a cumulativity rule on the function in `type_App`, i.e., suppose we have $Σ; Γ ⊢ f : T$ and $Σ; Γ ⊢ T ≤_a tProd na A B$ and $Σ; Γ ⊢ u : A$, so that $Σ; Γ ⊢ tApp f u : B\{0 := u\}$. First, the cumulativity can be broken down into a reduction to a product type $Σ; Γ ⊢ T ↝ tProd na' A' B'$ and two cumulativities $Σ; Γ ⊢ A' ≈_a A$ and $Σ; Γ : na A ⊢ B' ≤_a B$, respectively between domains and codomains. This key point is a strong form of injectivity for type constructor `tProd`, and its proof relies crucially upon confluence. To show that the cumulativity rule can indeed be commuted with
Fixpoint $\rho \Gamma t: term :=$
match t with
| tApp (tLambda na T b) u $\Rightarrow$ (\rho (na : (\rho \Gamma T) :: \Gamma) b) {0 := \rho \Gamma u}
| tLetIn na d t b $\Rightarrow$ (\rho (na := (\rho \Gamma d) : (\rho \Gamma t) :: \Gamma) b) {0:=\rho \Gamma d}
| tRel i $\Rightarrow$
match option_map decl_body (nth_error \Gamma i) with
| Some (Some body) $\Rightarrow$ (lift₀ (S i) body)
| Some None $\Rightarrow$ tRel i
| None $\Rightarrow$ tRel i
end
end

| tApp t u $\Rightarrow$ tApp (\rho \Gamma t) (\rho \Gamma u)
| tLambda na t u $\Rightarrow$ tLambda na (\rho \Gamma t) (\rho (na : (\rho \Gamma t) :: \Gamma) u)
| tProd na t u $\Rightarrow$ tProd na (\rho \Gamma t) (\rho (na : (\rho \Gamma t) :: \Gamma) u)
| tVar i $\Rightarrow$ tVar i
(* other cases are similar *)
end.

<caption>Fig. 10. Definition of the optimal reduction function $\rho$</caption>

**4.3.3 The Triangle Method.** Parallel reduction induces a relation which is larger than one-step reduction, but smaller than the reflexive transitive closure of one-step reduction.

$$ \rightarrow \subseteq \Rightarrow \subseteq \rightarrow^{*} $$

Therefore, confluence of parallel reduction is equivalent to confluence of one-step reduction.

But what is crucial for parallel reduction is that it satisfies the property that there is an *optimal reduced term* $\rho t$ for every term $t$ (Smolka [2015] provides a detailed exposition of this). Technically, this term is defined by well-founded recursion (§4.1) and views (§5.1), performing as many reductions as possible during its traversal, but for simplicity we here include a simplified description using a fixpoint on the syntax, (see Fig. 10). This definition is extended on contexts pointwise. The fact that it is optimal is expressed by the *triangle property* (for readability, we express the following two properties using commutative diagrams).

**THEOREM 4.2 (TRIANGLE PROPERTY).** For every term $t$ and context $\Gamma$, we have $\Gamma, t \Rightarrow \rho \Gamma, \rho (\rho \Gamma) t$ and for every $\Delta, u$ such that $\Gamma, t \Rightarrow \Delta, u$, the following triangle commutes

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

Note that the optimal reduction needs to be computed in the optimally reduced context, because parallel reduction also reduces terms in the context.

Parallel reduction is confluent because it is confluent in exactly one step, by using the *triangle property* twice.

**COROLLARY 4.2.1 (CONFLUENCE OF PARALLEL REDUCTION).** Parallel reduction is confluent.

<figure><img src="image_4.png" /></figure>
`type_App`, we need to show that the three components of the considered cumulativity rule can be integrated into the premises of `infer_App`. The reduction is incorporated into the constrained inference premise of `infer_App`, the conversion on domains goes into the checking premise, and the cumulativity on codomains is propagated further down.

### 4.3.4 Reaping the Benefits of the Equivalence.
In the end, composing completeness with correctness gives a form of "normalization" of typing derivations to somewhat canonical ones, where computation is delayed as long as possible and is used only in a principled way. More precisely, the structure of a derivation is completely fixed by the term, but because we do not fix a strategy for reduction (see e.g., Rule `infer product` in Fig. 7) we can potentially have derivations that have the same structure but differ in how much they reduce types.

The structure of these canonical derivations entails that they have better properties than the undirected ones, and the possibility to obtain one from any undirected derivation consequently ensure meta-theoretical properties of the undirected system that would be much harder to obtain directly.

The first is principality of typing, a version of type uniqueness relaxed to account for cumulativity.<fnref n="20" /> A caveat here: as already mentioned, since we do not impose a reduction strategy in constrained inference, inferred types are not unique up to equality, i.e., inference is not a functional relation. However, we show in (PCUIC: BDUnique) that two inferred types $\Gamma$ and $\Gamma'$ for a given term $t$ can always be reduced to a common reduct $\Gamma'$, implying in particular that $\Gamma$ and $\Gamma'$ are always convertible. As a consequence, any typeable term $t$ has a principal type— one that is minimal with respect to cumulativity amongst all types for $t$—namely (any of) its inferred types.

**Theorem inferring_unique** $\Sigma \Gamma t \Gamma'$:

$$ 
\begin{align*}
wf_{\Sigma} &\rightarrow wf_{\text{local}} \Sigma \Gamma \rightarrow \Sigma; \Gamma \vdash t \rightarrow \Gamma \rightarrow t \rightarrow \Sigma; \Gamma \vdash t \rightarrow \Gamma' \rightarrow \\
&\exists \Gamma'', \Sigma; \Gamma \vdash \Gamma \rightarrow \Gamma'' \times \Sigma; \Gamma \vdash \Gamma' \rightarrow \Gamma''
\end{align*}
$$

**Corollary inferring_unique** $\Sigma \Gamma t \Gamma'$:

$$ 
wf_{\Sigma} \rightarrow wf_{\text{local}} \Sigma \Gamma \rightarrow \Sigma; \Gamma \vdash t \rightarrow \Gamma \rightarrow t \rightarrow \Sigma; \Gamma \vdash t \rightarrow \Gamma' \rightarrow \Sigma; \Gamma \vdash t \approx_{s} \Gamma'.
$$

This property is crucial for the work on erasure, as it ensures we can unambiguously assign 'its' sort to a term, so erasing all terms whose sort is `tProp` is properly defined. While it was already proven before bidirectional typing was added to `METACOQ`, the proof was quite involved. And indeed, for some time only a weaker version could be obtained, asserting that if a term had two different types $\Gamma$ and $\Gamma'$ then there existed a third one $\Gamma''$ smaller than both $\Gamma$ and $\Gamma'$.

Another valuable property is strengthening (PCUIC: BDStrengthening) which says that if $\Sigma; \Gamma \vdash t : \Gamma$ and $\Delta$ is a well-formed sub-context of $\Gamma$ containing all variables of $t$, then $t$ is still well typed in the smaller $\Delta$. Although it is not directly used in the rest of the development as of now, it should be a useful stepping stone for proving correctness of various optimizations and tactics. Strengthening is difficult to prove in the undirected setting because a `type_Cumul` rule might introduce a type using arbitrary variables, the whole point of a proof being to show this kind of types can be avoided. In the bidirectional setting, the proof is much simpler as a derivation naturally only uses allowed variables, so that strengthening can be proven by a direct induction.

## 4.4 Fixing Cumulativity for Pattern Matching on Cumulative Inductive Types

*Representing pattern matching.* Coq's typing rule for `match` is notoriously difficult and obscure, as it has to account for the full generality of inductive types and dependent elimination. In all

<footnote n="20">²⁰Or, more generally, subtyping.</footnote>
It is easy to get confluence of the transitive closure of one-step reduction from confluence of parallel reduction by forgetting the target contexts.

Once confluence is proven, we can show the no-confusion properties of type constructors: dependent products, (co-)inductive types and sorts are injective with respect to cumulativity and different from each other. The proofs are standard. For example, if two products are in the cumulativity relation, then they are reducible to two products in the syntactical equality up to universes $Σ \vdash t \vdash \tau$ na $T \cup \leq_0^{Re} t \vdash \tau$ na $T' \cup \leq_0^{Re} t'$ and $Σ \vdash U \vdash \tau$ na $U \cup \leq_0^{Re} U$. The cases of syntactical equality outside the diagonal give us the proofs that e.g., sorts and inductive types are incomparable.

### 4.3.4 Context Conversion and Cumulativity.
Due to the complex interaction with the reduction of let-in definitions that can be present in the context, it is not possible to get full stability by context conversion of cumulativity and typing directly from the substitution lemma.

However, once confluence is proven, we can prove that for two contexts $Γ$ and $Δ$, if $Γ \leadsto Δ$ (where the notion of reductions of contexts is the pointwise extension of one-step reduction) and $Σ \vdash Γ \vdash U$ then there exists a common reduct of $t$ and $u$ in the context $Δ$. From this, we derive a confluence lemma for contexts: convertible contexts have a common reduct. This is the crucial property to show that cumulativity (hence typing) is preserved by context conversion. Actually, we show an even stronger version where we weaken the assumption to context cumulativity (defined pointwise, like conversion).

**Lemma** ws.cumul_pb ws.cumul_ctx {pb pb'} {Γ Γ'} {T U} :
$$Σ \vdash Γ' \leq [pb'] Γ \rightarrow$$
$$Σ \vdash Γ \vdash T \leq [pb] U \rightarrow$$
$$Σ \vdash Γ' \vdash T \leq [pb] U.$$

As contexts are on the left of the turnstile, context cumulativity has a contravariant action on cumulativity and typing: if a judgement holds in the larger context, then it also holds in the more precise one. We can derive a context conversion lemma as a specialization of this lemma where pb := Conv. The generality of this lemma is necessary in the subject reduction proof below: in presence of cumulative inductive types we will indeed need to move an hypothetical judgment from a larger context, coming from the type-checking of a case analysis to a smaller context corresponding to the scrutinee.

## 4.4 Subject Reduction

The subject reduction property is standard for the Pure Type System fragment of PCUIC: it follows the usual schema of induction on the typing derivation and inversion of the one-step reduction of the subject of the typing judgment. As we use untyped conversion, the case of the conversion rule is trivial, following directly by induction, and we can use the no-confusion properties of type constructors for elimination rules. In contrast, no direct subject reduction proof is known in presence of typed conversion [Abel et al. 2018a], as injectivity of type constructors cannot be proved directly in this formulation.

The meat and originality of our proof is to deal with case analysis on cumulative inductive families in all their generality. The paper proofs of Timany and Sozeau [2017, 2018] did not include a type preservation proof: they are concerned with a consistency proof of a variant of the system with typed conversion rules using a set-theoretical model, for the more elementary eliminator presentation of cumulative inductive types. Here we show that “real-world” mutual cumulative inductive families, with parameters, indices and let-bindings appearing anywhere, together with the rather complex case analysis construct, are behaving correctly with respect to reduction.
generality, a pattern-matching node in CoQ's kernel language is presented to the user with the following syntax:<fnref n="21" />

```
match s in I ... x₁ ... as s' return P with
  | c₁ y₁ ... yn₁ ⇒ b₁
  ...
  | cₖ y₁ ... ynₖ ⇒ bₖ
end
```

The scrutinee s is the value being matched, which should be of an inductive type I, P is the return type of the whole pattern matching, and b₁ to bₖ are the branches, one per constructor. The return type P can depend on both the indices of the inductive type I and the scrutinee, corresponding respectively to the in and as clauses, introducing variables that P can use. Similarly, branch bi binds the variables y₁ to ynᵢ, corresponding to the arguments of the constructor.

Historically, these binders had been respectively represented as iterated Π-types and λ-abstractions. This is the natural way they are specified in a setting with eliminators, and was kept when transitioning from those to pattern matching in CoQ 6.1. This meant that, contrarily to this user-facing syntax, P was actually internally represented as some iterated product type

```
tProd x₁ x₁ ... (tProd xₙ xₙ (tProd s' (mkApps I ([A₁; ... ; Aₙ]+[X₁; ... ; Xₙ]+[s']))) P)...
```

and similarly for branches.

**The completeness issue.** Our work on the proof of completeness of the type checker (§4.3.3) led to the discovery of a bug not only in our formalization, but also in the kernel of CoQ.<fnref n="22" /> This bug affected cumulative inductive types from their introduction in CoQ 8.11 until its discovery and fix in CoQ 8.14. It came from an incorrect implementation of the pen and paper development [Timany and Sozeau 2017] which used eliminators rather than pattern matching. This incompleteness in the implementation in turn led to a subject reduction failure: the kernel was unable to recognize that the reduct of a well-typed term was well typed. An example of this is given in Appendix.

In brief, the issue was that the representation of binders using Π-types and λ-abstractions led to a comparison of domain types that was wrongly using conversion (as is natural for product types in equivariant cumulativity, see §3.3.4). However, the correct cumulativity check for pattern matching on cumulative inductive types permits the inferred type of the scrutinee to be strictly smaller than the expected type of the argument of the return type. Thus, using a generic encoding of the return type as a Π-type was incorrect.

**The change in CoQ.** The easy fix, which simply replaced conversion by cumulativity in this particular function, was quickly implemented once the issue was found.<fnref n="23" />

However, the more principled solution in the long run was to change the case representation to store the parameters and universe instance separately from the return predicate and branches, completely removing the usage of Π and λ binders that caused the issue in the first place. In this new representation, corresponding to the typing rules given in §3.5, the return type P is directly represented as a term, implicitly well defined in an extended context which is computed from the information stored in the pattern-matching node. This representation of cases is more efficient, as the context of the predicate and branches no longer need to be stored, since they can canonically be derived from the inductive declaration and the stored parameters and universe instance. The user-specified binding annotations for these contexts are kept only for pretty-printing.

<footnote n="21">²¹See the reference manual.</footnote>

<footnote n="22">²²A precise description of the problem in the kernel is given in issue #13495 in the CoQ bug tracker on GitHub.</footnote>

<footnote n="23">²³In CoQ PR #13501.</footnote>
Without going into too many details the gist of the proof is as follows. Consider the most interesting case of a term `tCase ci (mkApps (tConstruct ind c u) args) p brs` performing a case analysis on a polymorphic datatype where the scrutinee is already a constructor application, hence a *l*-reduction can be performed. In that case, assuming (among other hypotheses) that

$$ \Sigma; \Gamma \vdash mkApps (tConstruct ind c u) args : mkApps (tInd ci (puinst p)) (pparams p ++ indices) $$

we need to show that

$$ \begin{align*} \Sigma; \Gamma \vdash \text{iota\_red} (\text{ci\_npar ci}) p &\text{ args br :} \\ &mkApps (\text{it\_mkLambda\_or\_LetIn} (\text{case\_predicate\_context ci mdecl idecl p}) (\text{preturn p})) \\ &\quad (\text{indices ++ } [\text{mkApps} (tConstruct ind c u) args]) \end{align*} $$

Here `br` is the branch corresponding to constructor `c`, which by typing must exist. The `ci` and `ind` information also have to match thanks to the case typing rule. The difficulty lies first in the relationship between the universes `u` of the actual constructor and `puinst p`, the universes that have been used to type-check the case originally. Due to cumulativity, we can have arbitrary relations between these two universe instances, including *no relationship* at all, in case a universe level is actually irrelevant. By validity and inversion lemmas, we can however show that `args` can be split into a list of parameters `pars` and actual arguments to the constructor `cargs` and that the parameters are convertible to `pparams p`. While they are convertible, they cannot be proven to be a well-typed instance of `ind_params mdecl` instantiated at (`puinst p`). However, the invariants on cumulative inductive types in § 2.6.2 ensure that the type of the vector of arguments `args` is a pointwise subtype of the type of the vector of arguments instantiated at (`puinst p`), in a context of parameters at level `u`. This is the key property to ensure that the branch that is selected, which was originally typed with an argument context at levels (`puinst p`) can indeed be instantiated with the actual arguments at level `u` as they are “smaller” according to the subtyping relation, making the reduction type-preserving.

**Positive Coinductive Types.** The subject reduction theorem holds because the case rule is disallowed on coinductive types. Indeed, subject reduction fails for dependent pattern matching on cofixpoints in `Coq`. This is an explicit design decision: when Giménez [1996] introduced coinductive types in `Coq`, he faced the problem that his presentation could either provide type preservation or decidability of type checking, but not both at the same time. It is known today how to fix the situation, either by forcing the use of co-pattern-matching and “Mendler-style” presentations of coinductives [Abel et al. 2013] or by restricting the dependent elimination of coinductive “values” to “pure” predicates, as they should rather be seen as computations [Pédrot and Tabareau 2017]. We plan to study the latter treatment in future work.

**Negative Coinductive Types.** Since `Coq 8.5` [The Coq Development Team 2016], there is an alternative presentation of coinductive types using primitive projections. A coinductive record type is defined together with its projections, and pattern matching is disallowed on these types. In this case, subject reduction holds for the projection reductions thanks to the restricted shape a projection's type can take, as projection types are derived from constructor argument types. Take non-zero streams for example:

**Set Primitive Projections.**

`CoInductive NZStream: Type := mkNZStream { head : N; tail : NZStream; head_nz : head ≠ 0 }.`

Its projections have type:

`head : NZStream → N; tail : NZStream → NZStream; head_nz : V (s : NZStream), head s ≠ 0`
This change had already been proposed by Herbelin,<fnref n="24" /> but was only finally implemented in CoQ's kernel by Pédrot<fnref n="25" /> for CoQ 8.14, following our discovery of the bug. The kernel representation moreover becomes closer to user syntax in which the types in these contexts are never displayed. This also fixes unintuitive behaviors of occurrence selection in tactics, since before the change tactics could find occurrences in parts of the term that the user couldn't see, namely the type of binders that were removed. Overall, the typing rule for match becomes simpler and closer to its bidirectional version, making explicit the flow of information between the inferred type of the scrutinee and the stored parameters and universe instance.

# 5 METATHEORY OF PCUIC

To implement a type checker for PCUIC and prove it correct, it is necessary to also formalize most of its metatheory. Indeed, the certified checker for CoQ relies for instance on confluence, subject reduction, and strong normalization of the reduction.

In this section, we explain how confluence of the conversion can be derived using the Tait-Martin-Löf-Takahashi methodology [Takahashi 1989] extended to cover not only $\beta$-reduction, but also pattern-matching, (co)fixpoints and let-bindings. In particular, parallel reduction in our setting can also reduce contexts. From this confluence proof, we derive many important properties, such as validity (the fact that the type in a typing derivation can itself be typed, sometimes called presupposition), as well as subject reduction and canonicity.

As already mentioned in the introduction, because of Gödel's second incompleteness theorem, strong normalization (SN) of PCUIC cannot be proven inside CoQ. Barras [2012] went as far as possible in this direction, showing that one can prove in CoQ, for the Calculus of Constructions extended with natural numbers and a sized-typing discipline, both a relative consistency proof with Intuitionistic Zermelo-Fraenkel Set Theory with Grothendieck universes, and SN using a reducibility candidates technique. The generalization of this method to the full CIC remains a research problem. Alternatively, Abel et al. [2018] prove SN for a (predicative) restriction of the same system in AGDA extended with inductive-recursive types, whose logical strength is a priori much higher. We see these rather strong results as evidence that it is consistent to assume strong normalization for PCUIC, and use it to derive consistency of PCUIC and standardization theorems which are useful for erasure.

## 5.1 Accessibility and Well-Founded Induction

In our development, we heavily rely on well-foundedness, both to state and use normalization, and to define functions by well-founded induction when structural induction as available natively in CoQ's guard checking is not enough.

While well-foundedness of a relation is classically stated as the absence of infinite descending chains, this negative statement is too weak in a constructive setting. Instead, we use the usual constructive reformulation [Paulson 1986], which says that all descending paths are finite. This is expressed using the accessibility predicate Acc associated with a relation, defined as follows:

Inductive Acc (A : Type) (R : A → A → Prop) (x : A) : Prop :=

Acc_intro : (V y : A, R y x → Acc R y) → Acc R x.

In words, an element x of A is accessible whenever all R-smaller elements are themselves accessible. A relation R : A → A → Prop is well founded whenever every element of A is accessible, i.e., whenever $\forall a : A, \text{Acc R a}$. However, accessibility is more precise, as it is 'local' in the sense that it asserts a property of a single element of a type.

<footnote n="24">²⁴In the CoQ enhancement proposal #34.</footnote>

<footnote n="25">²⁵In CoQ PR #13563</footnote>
One can see that in `head_nz`'s type, the `head` reference characteristic of dependent records is replaced by the corresponding projection of the record argument of the projection. This is actually the case for all occurrences of the record variable in the type of a projection: they are always projected. This invariant is crucial for the subject reduction proof, and is clearly not enforced for general dependent pattern matching where the eliminated variable can appear anywhere in the result type. To see why, consider the reduction of `head_nz ones : head ones ≠ 0` where ones is a cofixpoint expression producing an infinite stream of 1. When we reduce this expression we get to a proof of `1 ≠ 0` defined inside ones. The crucial property to show for type preservation is then that `head ones` is convertible to 1. This holds because we known that the record is a cofixpoint in this case as we just applied a projection on cofix reduction rule, so we can use the `cumul_cofix proj` rule to synchronize the two types. With the general pattern-matching construct we do not have such an invariant, so cofixpoint unfolding in the type expressions either have to be made unrestricted which leads to non-terminating type checking, or type preservation fails.

## 4.5 Strong Normalization

As we already said in the abstract, there is no hope to prove strong normalization of PCUIC inside Coq. We thus take as an assumption that we will use to prove our type checker terminating. Currently, this assumption is implemented in the form of an axiom. While strong normalization is often stated as the absence of infinite reduction paths, we here state it in a more constructive manner to be able to use it in the definition of the type checker. We say that every well-typed term is accessible for the opposite of reduction (§4.1). In other words all reduction paths starting from a given well-typed term are finite.

First, we specify the transitive closure of the opposite of the reduction—which we call coreduction— as the following inductive type `cored`:

Inductive `cored Σ Γ : term → term → Prop :=`
| `cored₁ : ∀ u v, Σ ; Γ ⊢ u ↦ v → cored Σ Γ v u
| `cored_trans : ∀ u v w, cored Σ Γ v u → Σ ; Γ ⊢ v ↦ w → cored Σ Γ w u.

Then, the *axiom of normalization* corresponds to the proposition that every well-typed term of PCUIC is accessible for `cored`. Note that this axiom is only taken to hold in a well-formed global environment, as an ill-formed environment can contain non-positive inductive types which would let one define non-normalizing terms.

Axiom normalization : ∀ Σ Γ t,
wf_ext Σ →
welltyped Σ Γ t →
Acc (cored Σ Γ) t.

The reduction order is reversed because a term should reduce to a smaller term for the order. So the axiom *normalization* means that the relation `cored` is well founded for well-typed terms, which corresponds to strong normalization of PCUIC.

## 4.6 Weak Call-by-Value Standardization

Reduction in PCUIC does not commit to a reduction order and can go under arbitrary binders. When extracting code to a programming language, it is important that the evaluation in the programming language can compute the same values as reduction in PCUIC. In this section, we prepare such a result to be later used in the correctness proof of type and proof erasure (§6), the first phase of an anticipated future verified extraction process. Precisely, we prove that whenever $Σ ; [] ⊢ t ↦* v$
This inductive accessibility predicate directly translates to well-founded recursion: its eliminator says that to define a function $f$ on an accessible $x : A$, one can access recursive calls on all R-smaller elements. Crucially, while accessibility is a *Prop*-valued relation, CoQ's subsingleton criterion allows to eliminate it into the *Type* sort. This means we can define functions by well-founded recursion, but have this proof of termination erased during extraction, providing an extracted function which is guaranteed to terminate<fnref n="26" /> but does not compute an uninformative proof of accessibility, avoiding a huge performance loss.

## 5.2 Substitution and Weakening

The implemented calculus uses standard de Bruijn lifting and (parallel) substitution operations. As a first step towards formalizing the metatheory of PCUIC, we need to show that reduction, cumulativity and typing are all closed by lifting (a property usually called weakening or thinning) and substitution operations.

Working with this traditional presentation of de Bruijn indices goes a long way, however we hit a difficulty when formalizing more complex operations on syntax, such as parallel reduction for proving confluence. To alleviate the difficulties associated with reasoning on the primitive operations, we provide a version of the $\sigma$-calculus operations [Abadi et al. 1991; Schäfer et al. 2015] on terms.

The $\sigma$-calculus operations enjoy a rich, clean and decidable equational theory, equivalent to an explicit substitution calculus, and are able to express complex commutations neatly—compared to the tricky lifting and substitution lemmas of “traditional” de Bruijn representations.

### 5.2.1 The $\sigma$-calculus.
The two primitives of the $\sigma$-calculus correspond to generalizations of lifting and substitution to an infinitary setting whose corresponding types are:

Definition renaming := $N \to N$.

Definition substitution := $N \to \text{term}$.

Renaming corresponds to a generalization of lifting where the action of a renaming $f$, written `rename f`, on a de Bruijn variable `tRel n` is defined by `tRel(f n)`. Similarly, the action of an infinitary substitution $\sigma$, written `$_{f}[\sigma]$` and called `instantiation`, on a de Bruijn variable `tRel n` is defined by $\sigma n$. In both cases, this action on variables is lifted to arbitrary terms by congruence.

In the $\sigma$-calculus, a renaming can be turned into a substitution by post-composition with the variable constructor `tRel`, both having the same action on terms. Moreover, the theory enjoys nice properties such as the fact that the action of renaming commutes with composition. This lets us prove stability of typing under a closed renaming (that is, when the renaming maps each variable in the source context to one with the same type in the target context) and under instantiation with a well-typed substitution (where well-typedness of a substitution is defined pointwise on the context with the additional check that let-bindings are preserved).

**Lemma** typing_rename $\Sigma \Gamma \Delta f t A$:
wf $\Sigma \to$ wf_local $\Sigma \Delta \to$
renaming_closed $\Gamma \Delta f \to$
$\Sigma; \Gamma \vdash t : A \to$
$\Sigma; \Delta \vdash rename f t : rename f A$.

**Lemma** typing_inst $\Sigma \Gamma \Delta \sigma t A$:
wf $\Sigma \to$ wf_local $\Sigma \Delta \to$
$\Sigma; \Delta \vdash \sigma : \Gamma \to$
$\Sigma; \Gamma \vdash t : A \to$
$\Sigma; \Delta \vdash t.[\sigma] : A.[\sigma]$.

The **weakening** and **substitution** theorems, formulated without the $\sigma$-calculus primitives, are direct consequences of their more abstract counterparts, but more directly usable. The global environment also induces a form of weakening by the addition of new inductive or constant

<footnote n="26">²⁶To be precise, this only applies to inputs that satisfy potentially erased preconditions. For instance, our weak-head reduction machine is only guaranteed to terminate on well-typed terms.</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 11. Weak call-by-value reduction (excerpt)</figcaption></figure>

where v is irreducible, then this value can actually be found using weak call-by-value evaluation (up to some remaining silent reduction under binders).

The terminology “evaluation” here refers to a one-shot inductive definition of big-step evaluation, i.e., without relying on one step reduction and reflexive transitive closure, whereas “call-by-value” means that arguments are always fully evaluated before a function or fixpoint application, and “weak” refers to the fact that abstraction and fixpoint are treated as values, without evaluating their bodies first.

We prove the result for closed terms and use the strong normalization assumption in the proof to obtain a simple proof. We remark however that this choice is solely for proof engineering reasons—more general results with less assumptions are possible, but at the cost of significantly more complicated proof methods.

We first define a one-step weak call-by-value reduction predicate $\Sigma \vdash t \leadsto_{wcbv} t'$, $t'$ in Figure 11, which is a restriction of $\Sigma; \Gamma \vdash t \leadsto t'$ for closed terms t. Since we only care about closed terms in this section, there is no need for a context $\Gamma$ in the definition of the weak call-by-value reduction, since weak call-by-value reduction ensures that reduction of closed term will never have to consider open terms. Weak call-by-value reduction relies on the notion of value (Figure 12), which characterizes closed terms that are irreducible. We do not consider global definitions without bodies (i.e., axioms) in the definition, and thus our results only apply to axiom-free global environments.

**Definition axiom_free** $\Sigma := \forall c \ decl$, $decl$ constant $\Sigma c \ decl \to cst\_body$ decl $\neq$ None.

A natural first step to prove the standardization theorem is to prove a *progress theorem* for weak call-by-value reduction, as usual by induction on the typing derivation:

**Lemma progress** : $\forall \Sigma t T, \mathrm{wf} \Sigma \to \mathrm{axiom\_free} \Sigma \to \Sigma; [] \vdash t : T \to \{t' \& \Sigma \vdash t \leadsto_{wcbv} t'\} + (\mathrm{value} \ \Sigma t).$
Class GuardCheckerCorrect := {
  guard_red b Σ Γ mfix mfix' idx :
    Σ ; Γ ⊢ tFixCoFix b mfix idx ↦→ tFixCoFix b mfix' idx →
  guard b Σ Γ mfix → guard b Σ Γ mfix' ;
  guard_extend s b Σ Σ' Γ mfix :
    extends Σ Σ' →
    guard b Σ Γ mfix → guard b Σ' Γ mfix ;
  guard_inst b Σ Γ Δ mfix σ :
    Σ ; Γ ⊢ σ : Δ →
    guard b Σ Δ mfix → guard b Σ Γ (inst_mfix mfix σ ) ;
  guard_rename b P Σ Γ Δ mfix f :
    renaming P Γ Δ f →
    guard b Σ Δ mfix → guard b Σ Γ (rename_mfix mfix f ) }.

<caption>Fig. 8. Correctness of the guard checker with respect to the calculus (excerpt)</caption>

declarations (PCUIC: WeakeningEnv), simpler from the point of view of typing but trickier w.r.t.
universe instantiation (PCUIC: UnivSubstitutionTyp). Still, in both cases we show that typing is
also stable by these operations.

5.2.2 Correctness of the Guard Checker. Stability of typing under renaming and substitution actually depends on correctness properties of the guard condition. Indeed, for those metatheoretical properties to hold, the guard condition needs to satisfy corresponding stability properties. This can be seen as a guideline on how to implement a guard condition properly. Indeed, we want the guard condition to imply normalization of the theory, but we also want it not to break subject reduction for instance.

The class GuardCheckerCorrect (Fig. 8) summarizes the properties that a guard condition needs to satisfy to preserve good metatheoretical properties. It says that the guard condition must be stable by reduction, context extension, instantiation and renaming. There are also conditions of stability by α-renaming, cumulativity (at the level of contexts) and universe substitution, but those conditions are mainly technical.

5.3 Confluence

Following the Tait-Martin Löf method [Takahashi 1989], we define *parallel reduction* for PCUIC,
written as Γ,t ⇒ Δ,t', in Fig. 9. This reduction is just a variant of reduction Σ; Γ ⊢ t ↦→ t' where
already present redexes can all be reduced together in one single step. Note that the global environ-
ment Σ is a parameter of the reduction and not an index because it is fixed during the reduction.
Note that a β-redex can be reduced or not, depending on whether the reduction rule pred beta or
congruence rule pred app is used. We also add a reflexivity rule for atoms (variables which may
not be reduced, universes, inductive types and constructors), thus ensuring that parallel reduction
is reflexive.

5.3.1 *Well-Scoped Terms.* The correct representation of pattern matching for cumulative inductive types (§ 4.4) introduces a subtle issue which has to do with confluence. The term

tCase ... (tApp (tConstruct <T> 0 [] ) (tInd <N> [] ))
[ ( { decl_name := { binder_name := "x"; binder_relevance := Relevant };
  decl_body := Some (tRel 0); ... },
  tRel 0) ]
<figure><img src="image_6.png" /><figcaption>Fig. 12. Weak call-by-value values</figcaption></figure>

The standardization result actually talks about a weak call-by-value evaluation predicate $\Sigma \vdash t \triangleright v$. Since it is entirely standard to derive the definition from the definition of reduction, we omit it in the paper and refer the reader to the Coq code. Standardization relies on auxiliary results such as the fact that weak call-by-value reduction steps do not change the value under evaluation; that evaluation is included in the reflexive transitive closure of reduction; and also that subject reduction applies to evaluation. Furthermore, it relies on the fact that results of evaluation are values, and values evaluate to themselves.

From those auxiliary lemmas, it is easy to conclude that strongly normalizing terms are weakly normalizing, in the sense that they evaluate to a value.

Lemma $SN\_to\_WN: \forall \Sigma A t, \mathrm{wf}\ \Sigma \rightarrow \mathrm{axiom\_free}\ \Sigma \rightarrow \mathrm{Acc}(\mathrm{cored}\ \Sigma \;) t \rightarrow \Sigma; [] \vdash t : A \rightarrow \{v \ \& \ \Sigma \vdash t \searrow v\}$.

The proof is by induction on the assumption that $t$ is strongly normalizing. We use progress to either obtain $t'$ such that $\Sigma \vdash t \leadsto_{\mathrm{webv}} t'$ or have that $t$ is a value. In the first case, there is $v$ such that $\Sigma \vdash t' \triangleright v$ by induction hypothesis, and we can use that a reduction step preserves evaluation to conclude. In the second case, we can pick $v$ as $t$.

By using the axiom that every well typed term is normalizing we can then deduce weak normalization and finally deduce weak-call by-value standardization. This theorem states that if a term $t$ reduces to a non reducible terms, then this term can also be reached by first evaluating $t$ to a value $v$' using call-by-value big step evaluation in an empty context, written $\Sigma \vdash t \searrow t'$. And then performing the potentially remaining deep reductions (reductions under binders that cannot be performed by weak call-by-value reduction).

Lemma `webv_standardization`: $\forall \Sigma T t v, \mathrm{wf}\ \Sigma \rightarrow \mathrm{axiom\_free}\ \Sigma \rightarrow \Sigma; [] \vdash t : T \rightarrow \Sigma; [] \vdash t \leadsto v \rightarrow \neg \{t' \ \& \ \Sigma; [] \vdash v \leadsto t'\} \rightarrow$
Inductive Γ, _ ⇒ Δ, _ : term → term → Type :=

| pred desugar na t0 t1 b0 b1 a0 a1 :

Γ, t0 ⇒ Δ, t1 → (Γ, na : t0), b0 ⇒ (Δ, na : t1), b1 → Γ, a0 ⇒ Δ, a1 →

Γ, tApp (tLambda na t0 b0) a0 ⇒ Δ, b1 {0 := a1}

| pred desugar na d0 d1 t0 t1 b0 b1 :

Γ, t0 ⇒ Δ, t1 → Γ, d0 ⇒ Δ, d1 → (Γ, na := d0 : t0), b0 ⇒ (Δ, na := d1 : t1), b1 →

Γ, tLetIn na d0 t0 b0 ⇒ Δ, b1 {0 := d1}

| pred rel_def_unfold i body :

Γ ⇒ ctx Δ → option_map decl_body (nth_error Δ i) = Some (Some body) →

Γ, tRel i ⇒ Δ, lift0 (S i) body

| pred rel refl i :

Γ ⇒ ctx Γ' → Γ, tRel i ⇒ Γ', tRel i

| pred delta c decl body (isdecl : declaredoes declared c decl) u :

Γ ⇒ ctx Δ → decl.(cst_body) = Some body → Γ, tConst c u ⇒ Δ, body@[u]

| pred app M0 M1 N0 N1 :

Γ, M0 ⇒ Δ, M1 → Γ, N0 ⇒ Δ, N1 → Γ, tApp M0 N0 ⇒ Δ, tApp M1 N1

(* other cases are omitted *)

Inductive Γ,_,− ⇒ subst Γ',_,− : list term → context → list term → context → Type :=

| psubst_empty : Γ, [], [] ⇒ subst Γ', [], []

| psubst a Δ Δ' s s' na na' t t' T T' :

Γ, s, Δ ⇒ subst Γ', s', Δ' → (Γ ++ Δ), T ⇒ (Γ' ++ Δ'), T' → Γ, t ⇒ Γ', t' →

Γ, (t :: s), (Δ, na : T) ⇒ subst Γ', (t' :: s'), (Δ', na' : T')

| psubst d Δ Δ' s s' na na' t t' T T' :

Γ, s, Δ ⇒ subst Γ', s', Δ' → (Γ ++ Δ), T ⇒ (Γ' ++ Δ'), T' → Γ, (subst0 s t) ⇒ Γ', (subst0 s' t') →

Γ, (subst0 s t :: s), (Δ, na := t : T) ⇒ subst Γ', (subst0 s' t' :: s'), (Δ', na' := t' : T').

<caption>Fig. 9. Definition of *parallel reduction* (assuming a global environment Σ)</caption>

corresponds to match @C N with @C X (x := X) ⇒ x end but the new PCUIC representation now also
allows let Y := N in match @C N with @C X (x := Y) ⇒ x end which breaks confluence. The root of the
problem comes from the fact that the reduction rule for pattern matching implicitly assumes that
the contexts of the branches are well formed, i.e., have the right number of binders. On terms where
this is not the case, we can encounter the pathological behavior above.

Thus, we need a property on untyped terms that is enough to regain confluence. A sufficient
property is well scoping, which in the case where the term is a pattern-matching node ensures
that contexts are properly closed, and forbids the ill-scoped example above. Under this restriction,
reduction and substitution properly commute, and confluence is recovered. In what follows, we
implicitly assume that all terms are well scoped, although in the Coq formalization, this introduces
a significant amount of additional assumptions in the theorems and definitions. For instance, this is
the technical reason why transitivity of conversion is only allowed to go through a well-scoped
term (§3.3.1), as this ensures we can use our confluence property on well-scoped terms. We decided
against switching to intrinsically well-scoped syntax as it would be highly non-trivial: there are
complex *n*-ary binding constructs for cases and (co-)fixpoints in particular, and it would require
duplicating the whole development around environments. Besides, it would clutter our already
Inductive whne Σ (Γ : context) : term → Type :=
whne_rel i : option_map decl_body (nth_error Γ i) = Some None → whne Σ Γ (tRel i)
whne_const c u decl : lookup_env Σ c = Some (ConstantDecl decl) → decl.(cst_body) = None →
whne Σ Γ (tConst c u)
whne_app f v : whne Σ Γ f → whne Σ Γ (tApp f v)
whne fixed mfix idx args d arg :
nth_error mfix idx = Some d → nth_error args (rarg d) = Some arg →
whne Γ arg → whne Γ (mkApps (tFix mfix idx) args)
whne_case i p c brs : whne Σ Γ c → whne Σ Γ (tCase i p c brs)
whne Project : whne Σ Γ c → whne Σ Γ (tProj p c)

Inductive whnf Σ (Γ : context) : term → Type :=
whnf_ne t : whne Σ Γ t → whnf Σ Γ t
whnf_sort s : whnf Σ Γ (tSort s)
whnfProd na A B : whnf Σ Γ (tProd na A B)
whnf_lam na A B : whnf Σ Γ (tLambda na A B)
whnf_cstrapp i n u v : whnf Σ Γ (mkApps (tConstruct i n u) v)
whnf_indapp i u v : whnf Σ Γ (mkApps (tInd i u) v)
whnf fixed mfix idx args :
(∃ d, nth_error mfix idx = Some d ∧ nth_error args (rarg d) = None) ∨ (nth_error mfix idx = None)
→ whnf Γ (mkApps (tFix mfix idx) args)
whnf_cofixed mfix idx v : whnf Σ Γ (mkApps (tCoFix mfix idx) v).

<caption>Fig. 13. Definition of weak-head normal forms in PCUIC</caption>

{v' & Σ ⊢ t ⇝ v' * Σ ; [] ⊢ v' ↝ v}.

To show this, we use weak normalization for t to obtain v' such that Σ ⊢ t ⊲ v'. Because evaluation
entails reduction, we also have that Σ ; [] ⊢ t ↝* v'. By the assumption that t also reduces to v and
confluence, we obtain v'' such that Σ ; [] ⊢ v ↝* v'' and Σ ; [] ⊢ v' ↝* v''. Since v is irreducible, we
know that in fact v = v''.

4.7 Canonicity

Canonicity for PCUIC states that any non-reducible inhabitant of an (co-)inductive type is an applied
constructor or a cofixpoint. The proof goes in two steps, first we show that any non-reducible
term is in weak-head normal form. A weak-head normal form (Fig. 13) is either a term starting
with a constructor (a type constructor, a lambda abstraction, a constructor of an inductive type), a
partially applied fixpoint, any cofixpoint, or a neutral term (whne). A neutral term is either a variable
(not associated to a let-in construct), an axiom (i.e., a constant with no body) or a destructor (an
application, a fixpoint, a pattern matching or a projection) whose evaluation is blocked on a neutral
term. We can reuse the progress lemma of § 4.6 to derive the following lemma which states that
weak-head normal forms describe all stuck terms.

Lemma whnf_progress : ∀ Σ t T,
axiom_free Σ → wf Σ →
Σ ; [] ⊢ t : T →
¬ { t' & Σ ; [] ⊢ t ↝ t' } →
whnf Σ [] t.
complex technical statements and proofs with manipulations of coercions due to the explicit
weakenings and type-level arithmetic on context lengths this necessarily introduces.

5.3.2 *Dealing with Dependent Let-Bindings.* Note that because of let-bindings, we need to take the context explicitly into account during the reduction. This is obtained by adding the `All2_local_env` (`on Decl pred₁`) `Γ Γ'` predicate in the premises of basic parallel reduction steps (such as the rule `pred_rel_def_unfold` for instance) in order to allow for parallel reduction in the context too.

Thanks to the generalization to contexts, we can prove a strong substitution lemma which says that the parallel reduction satisfies the property that the reductions performed on two terms M and N can also be done in one step on M where its first de Bruijn variable is substituted by N', where N reduces to N' in parallel as well.

**Lemma** *substitution Γ Δ M M' na A A' N N' : wf Σ →*
*Γ, N ⇒ Δ, N' →*
*(Γ, na : A) M ⇒ (Δ, na : A') , M' →*
*Γ, M {0 := N} ⇒ Δ, M' {0 := N}.*

We actually need a generalized version of this lemma for well-typed substitutions: $\Gamma \vdash s : \Delta$, where $\Delta$ is the context we are substituting into and $\Gamma$ represents the variables needed to type the substitution $s$. However, as we are doing things in parallel, we need a notion of parallel substitution. To account for let-ins correctly, we need these well-typed substitutions to coherently *preserve* the body of local definitions. The parallel substitution structure $\Gamma, \Delta, s \Rightarrow^{\text{subst}} \Gamma', \Delta', t'$ represents two substitutions $s$ and $t$ typed respectively in $\Gamma$ and $\Gamma'$ and instantiating respectively contexts $\Delta$ and $\Delta'$ (Fig. 9).

Rule `psubst_d` simply ensures that the two terms `t` and `t'` are in the parallel reduction relation, to instantiate two assumptions, the `psubst_d` rule rather *forces* the substitution to be equal to the appropriately substituted bodies of let-ins. This still allows the reduction of the substituted versions of let-in bodies in the contexts. While types themselves do not participate in reduction, it is essential to also allow their reduction, to get context conversion (of type annotations, not bodies) at the same time as substitution: a context conversion, when restricted to type annotations, is a substitution by the identity. We use mathematical notation rather than Coq for the following theorems to allow for more visual statements.

**THEOREM 5.1 (PARALLEL SUBSTITUTION).** *The stability by substitution of parallel reduction extends to parallel substitution in the following way:*

$$
\begin{align*}
(\Gamma, \Delta), s &\Rightarrow^{\text{subst}} (\Gamma_1, \Delta_1), s' \rightarrow \\
(\Gamma + \Delta \quad &\Rightarrow \quad \Gamma'), M \Rightarrow (\Gamma_1 + \Delta_1 \quad \Rightarrow \quad \Gamma'_1), N \rightarrow \\
& (\Gamma + \Gamma'[s]), (\text{subst } s \#|\Gamma'| M) \Rightarrow (\Gamma_1 + \Gamma'_1[s]), (\text{subst } s' \#|\Gamma'_1| N)
\end{align*}
$$

5.3.3 *The Triangle Method.* Parallel reduction induces a relation which is larger than one-step reduction, but smaller than the reflexive transitive closure of one-step reduction.

$$
\rightarrow \subseteq \Rightarrow \subseteq \rightarrow^{*}
$$

Therefore, confluence of parallel reduction is equivalent to confluence of one-step reduction.

But what is crucial for parallel reduction is that it satisfies the property that there is an *optimal reduced* term $\rho$ t for every term t (Smolka [2015] provides a detailed exposition of this). Technically, this term is defined by well-founded recursion (§5.1) and views (§6.1), performing as many reductions as possible during its traversal, but for simplicity we here include a simplified description using a fixpoint on the syntax, (see Fig. 10). This definition is extended on contexts pointwise. The fact that it is optimal is expressed by the *triangle property* (for readability, we express the following two properties using commutative diagrams).
From this, we can formulate a classification theorem by proving that no neutral terms can exist in an empty context, and then analyzing the potential whnf inhabitants of an inductive type (the definition `construct_cofix_discr` (head t) just says that the head of t is either a constructor or a cofixpoint).

**Theorem classification:** $\forall \Sigma t i u \text{ args,}$
$$ \begin{aligned} \text{axiom_free } \Sigma &\rightarrow \text{wf } \Sigma \rightarrow \\ &\neg \{t' \& \Sigma; [] \vdash t \leadsto t'\} \rightarrow \\ \Sigma; [] \vdash t : \text{mkApps} (\text{tInd } i u) \text{ args} &\rightarrow \\ \text{construct_cofix_discr} (\text{head } t). \end{aligned} $$

Finally, thanks to normalization and subject reduction, we can show the usual canonicity statement for PCUIC, saying that any closed inhabitant of an inductive type is convertible to a fully applied constructor, and any closed inhabitant of a coinductive type is convertible either to a fully applied constructor or to a cofixpoint.

**Lemma pcuic_canonicity:** $\forall \Sigma t i u \text{ args,}$
$$ \begin{aligned} \text{axiom_free } \Sigma &\rightarrow \text{wf } \Sigma \rightarrow \\ \Sigma; [] \vdash t : \text{mkApps} (\text{tInd } i u) \text{ args} &\rightarrow \\ \{t' : \text{term } \& \Sigma; [] \vdash t' : \text{mkApps} (\text{tInd } i u) \text{ args} \times \Sigma; [] \vdash t \approx_s t' \times \text{construct_cofix_discr} (\text{head } t')\}. \end{aligned} $$

## 4.8 Consistency

Using canonicity, it is easy to derive the following consistency result for PCUIC. As is standard, consistency is stated as the fact that the empty type cannot be inhabited in the empty context. Because our definition of PCUIC is parametrized by a global environment our statement needs to postulate that this global environment contains the empty type to be able to state the result. $\perp_{oib}$ correspond to the `one_inductive_body` in `tProp` with no parameter or constructor, and $\perp_{mib}$ is the `mutual_inductive_body` consisting only of $\perp_{oib}$.

**Theorem pcuic_consistent:** $\forall \Sigma t \perp_{pcuic},$
$$ \begin{aligned} \text{declared_inductive } \Sigma &\perp_{pcuic} \perp_{mib} \perp_{oib} \rightarrow \\ \text{wf_ext } \Sigma &\rightarrow \text{axiom_free } \Sigma \rightarrow \\ \Sigma; [] \vdash t : \text{tInd} \perp_{pcuic} [] &\rightarrow \perp. \end{aligned} $$

Technically speaking, this theorem is actually a relative consistency result, as it shows consistency of PCUIC (the formalized theory) for strongly normalizing terms assuming consistency of CoQ (the proof assistant).

## 5 A SOUND AND COMPLETE CHECKER FOR PCUIC

We now turn to the definition of a type checker for PCUIC and a proof that it is sound and complete with respect to the specification given in §2. In order to define this type checker, all properties involved in typing judgments must be replaced by actual decision procedures. To make our type checker more modular and independent of a specific implementation, we parametrize type checking by an abstract notion of environment on which only basic decision procedures are postulated. This allows us to define a generic type checker that can be later optimized, by optimizing these basic decision procedures. For instance, the most direct venue for optimization is the decision procedure for consistency of the universe hierarchy.

After giving some technical insights and presenting the abstract interface of an environment used for type checking, we present the generic conversion/cumulativity checking algorithm and type inference. We then discuss a slightly optimized implementation of the abstract environment and finally analyze the performance of the safe checker compared to the one of CoQ.
Fixpoint $\rho \Gamma t: term :=$
match t with
| tApp (tLambda na T b) u $\Rightarrow$ (\rho (na : (\rho \Gamma T) :: \Gamma) b) {0 := \rho \Gamma u}
| tLetIn na d t b $\Rightarrow$ (\rho (na := (\rho \Gamma d) : (\rho \Gamma t) :: \Gamma) b) {0:=\rho \Gamma d}
| tRel i $\Rightarrow$
match option_map decl_body (nth_error \Gamma i) with
| Some (Some body) $\Rightarrow$ (lift₀ (S i) body)
| Some None $\Rightarrow$ tRel i
| None $\Rightarrow$ tRel i
end

| tApp t u $\Rightarrow$ tApp (\rho \Gamma t) (\rho \Gamma u)
| tLambda na t u $\Rightarrow$ tLambda na (\rho \Gamma t) (\rho (na : (\rho \Gamma t) :: \Gamma) u)
| tProd na t u $\Rightarrow$ tProd na (\rho \Gamma t) (\rho (na : (\rho \Gamma t) :: \Gamma) u)
| tVar i $\Rightarrow$ tVar i
(* other cases are similar *)
end.

<caption>Fig. 10. Definition of the optimal reduction function $\rho$</caption>

**THEOREM 5.2 (TRIANGLE PROPERTY).** For every term $t$ and context $\Gamma$, we have $\Gamma, t \Rightarrow \rho \Gamma, \rho (\rho \Gamma) t$ and for every $\Delta, u$ such that $\Gamma, t \Rightarrow \Delta, u$, the following triangle commutes

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

Note that the optimal reduction needs to be computed in the optimally reduced context, because parallel reduction also reduces terms in the context.

Parallel reduction is confluent because it is confluent in exactly one step, by using the *triangle* property twice.

**COROLLARY 5.2.1 (CONFLUENCE OF PARALLEL REDUCTION).** *Parallel reduction is confluent.*

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

It is easy to get *confluence* of the transitive closure of one-step reduction from confluence of parallel reduction by forgetting the target contexts.

Once confluence is proven, we can show the no-confusion properties of type constructors: dependent products, (co-)inductive types and sorts are injective with respect to cumulativity and different from each other. The proofs are standard. For example, if two products are in the cumulativity relation, then they are reducible to two products in the syntactical equality up to universes $\Sigma \vdash tProd na T \Upsilon \leq_0^{\text{Re}} tProd na' T' U'$, which by a direct inversion gives us that $\Sigma \vdash T \leq_0^{\text{Re}} T'$ and $\Sigma \vdash U \leq_0^{\text{Re}} U'$. The cases of syntactical equality outside the diagonal give us the proofs that e.g., sorts and inductive types are incomparable.
## 5.1 Technical Insight

Before we delve into the definition of our type checker, let us address some technical points that are either needed as preliminaries or that give insight to the methods that we use for our formalization that are not directly related to our problem at hand.

5.1.1 *Enforcing computational irrelevance.* Because we want to ultimately obtain a type checker that can be extracted and run efficiently, we are very careful to separate the relevant content used by the algorithm from the computationally irrelevant content pertaining to the invariants it maintains. For this we use the facilities offered by the sort *Prop* of *CoQ*, whose inhabitants are erased at extraction time. However, most predicates and relations from the previous sections (for instance typing) are defined in sort *Type*, in order to avoid having to struggle with the dichotomy between relevant and irrelevant while doing the meta-theoretic proofs. Throughout this section, we thus make extensive use of *squashing* of a type `X` into *Prop*, written `||X||`, to make relevant content irrelevant.

5.1.2 *EQUATIONS.* In order to ease the use of the techniques described in this section, we heavily rely on the *EQUATIONS* [Sozeau and Mangin 2019] plugin for *CoQ*. This plugin provides notations and mechanisms to help with the definition of complex, non-structural recursive definitions. In particular, it has built-in support for definitions by well-founded induction (see §4.1). Moreover, its *obligation* mechanism, which lets users leave holes in the definition of functions and fill them later in proof mode, is crucial to be able to write complex proof-carrying code.

5.1.3 *Views.* When manipulating datatypes, typically terms, we often wish to inspect them in a way that is not expressible directly by pattern matching. For instance, when considering reduction we want to distinguish exactly three cases: the term is either a `λ`-abstraction applied to a list of arguments (i.e., of the form `mkApps (tLambda na A t) 1`), a fixpoint applied to a list of arguments, or any other term.

To express these custom case distinctions, we rely on *views*, originally introduced by *Wadler* [1985] and later rephrased in the setting of dependent types by *McBride and McKinna* [2004]. Examples of such views are given in PCUIC: *Views*, such as `fix Lambda App view`, corresponding to the case distinction we outlined above:

```
Inductive fixoglba_app_view: term → term → Type :=
| fixoglba_app_fix mfix i l a : fixoglba_app_view (mkApps (tFix mfix i) 1) a
| fixoglba_app...lambda na ty b l a : fixoglba_app_view (mkApps (tLambda na ty b) 1) a
| fixoglba_app_other t a : ¬ isFixLambda_app (tApp t a) → fixoglba_app_view t a.
```

Compared to the non-dependent case, however, our views are richer: they not only allow for a convenient case distinction, but embed, either in their indexed type (as for the first two constructors) or extra arguments (as in the last constructor), the meaning of this case distinction. This way, a pattern-matching on a view gives us the logical information corresponding to the case distinction we apply. Another important benefit of this technique is that we get one proof obligation for each case of the view. In a setting where the "default" view case typically corresponds to more than 10 branches in a regular pattern matching, this is important to keep proofs manageable: we get only one obligation to solve instead of 10 very similar ones.

5.1.4 *Open Recursion.* In order to implement our type checker, we define several functions mutually, involving complex termination measures. Mutually defined fixpoints are painful to reason about so we lighten our burden by using a technique called *open recursion*. The idea is quite simple: instead of defining a function directly as a (mutual) fixpoint, we define the associated *functional* and then we take the corresponding fixed point. Concretely, the function takes an extra argument which is a
5.3.4 Context Conversion and Cumulativity. Due to the complex interaction with the reduction of let-in definitions that can be present in the context, it is not possible to get full stability by context conversion of cumulativity and typing directly from the substitution lemma.

However, once confluence is proven, we can prove that for two contexts Γ and Δ, if Γ ↛ Δ (where the notion of reductions of contexts is the pointwise extension of one-step reduction) and Σ ; Γ ⊢ t ↛ u then there exists a common reduct of t and u in the context Δ. We define algorithmic cumulativity as the relation Σ ; Γ ⊢ T ≤=[R1e] T' with R1e deciding if universes are compared for inclusion or equality as usual. It is the standard PTS-style cumulativity relation: both types must reduce to syntactically equal terms up-to universes, according to the R1e relation. Algorithmic context cumulativity is defined by pointwise algorithmic cumulativity and is denoted by Σ ⊢ Γ' ≤=[R1e] Γ. From the context reduction lemma above, we derive a confluence lemma for contexts: algorithmically convertible contexts have a common reduct. This is the crucial property to show that cumulativity (hence typing) is preserved by context conversion. Actually, we show an even stronger version where we weaken the assumption to context cumulativity.

Lemma ws_cumul_pb_WS_cumul_ctx {R1e R1e'} {Γ Γ'} {T U} :
Σ ⊢ Γ' ≤=[R1e'] Γ →
Σ ; Γ ⊢ T ≤=[R1e] U →
Σ ; Γ' ⊢ T ≤=[R1e] U.

As contexts are on the left of the turnstile, context cumulativity has a contravariant action on cumulativity and typing: if a judgement holds in the larger context, then it also holds in the more precise one. We can derive a context conversion lemma as a specialization of this lemma where R1e' := eq_universe (global_ext_constraints Σ). The generality of this lemma is necessary in the subject reduction proof below: in presence of cumulative inductive types we will indeed need to move a hypothetical judgment from a larger context, coming from the type-checking of a case analysis to a smaller context corresponding to the scrutinee.

5.4 Subject Reduction

The subject reduction property is standard for the Pure Type System fragment of PCUIC: it follows
the usual schema of induction on the typing derivation and inversion of the one-step reduction
of the subject of the typing judgment. As we use untyped conversion, the case of the conversion
rule is trivial, following directly by induction, and we can use the no-confusion properties of
type constructors for elimination rules. In contrast, no direct subject reduction proof is known
in presence of typed conversion [Abel et al. 2018], as injectivity of type constructors cannot be
proved directly in this formulation. This is a standard issue with formulations of dependent type
theory, see, e.g., the work of Harper and Pfenning [2005] for a study of this issue in the simpler
setting of the Logical Framework.

The meat and originality of our proof is to deal with case analysis on cumulative inductive families in all their generality. The paper proofs of Timany and Sozeau [2017, 2018] did not include a type preservation proof: they are concerned with a consistency proof of a variant of the system with typed conversion rules using a set-theoretical model, for the more elementary eliminator presentation of cumulative inductive types. Here we show that “real-world” mutual cumulative inductive families, with parameters, indices and let-bindings appearing anywhere, together with the rather complex case analysis construct, are behaving correctly with respect to reduction.

Without going into too many details the gist of the proof is as follows. Consider the most interest-
ing case of a term tCase ci (mkApps (tConstruct ind c u) args) p brs performing a case analysis on a
polymorphic datatype where the scrutinee is already a constructor application, hence a l-reduction
can be performed. In that case, assuming (among other hypotheses) that
function to perform the recursive calls, and this function is guarded to only be called on smaller arguments w.r.t. to a previously chosen relation.

Taking a silly example on purpose, we could define functions that test whether a natural number is odd or even as follows:

Fixpoint even (n : N) : B :=
match n with
  | 0 ⇒ true
  | S n ⇒ odd n
end

with odd (n : N) : B :=
match n with
  | 0 ⇒ false
  | S n ⇒ even n
end.

The same example in open recursion, using Inductive mode := Even | Odd to distinguish between the two functions even and odd, looks as follows:

Equations _even n
  (aux : mode → ∀ m, m < n → B) : B :=
    _even 0 aux := true;
    _even (S n) aux := aux Odd n _.

Equations _odd n
  (aux : mode → ∀ m, m < n → B) : B :=
    _odd 0 aux := false;
    _odd (S n) aux := aux Even n _.

We first define _even and _odd which are functions that are not even recursive yet, but take as argument aux to represent recursive calls. This is where the mode comes into play, it lets one choose which function to call recursively. Here we use EQUATIONS to infer automatically the proof that n < S n. Then we can actually perform (well-founded) recursion to *close the loop* by using a function even_orOdd which uses itself as aux.

Equations even_orOdd (M : mode) (n : N) : B by wf n lt :=
  even_orOdd Even n := _even n even_orOdd;
  even_orOdd Odd n := _odd n even_orOdd.

Definition even := even_orOdd Even.
Definition odd := even_orOdd Odd.

While on such an example, it might not appear very interesting, in our case this lets us define all components of a mutual recursive block in isolation and prove things about them without having to worry about recursion or the interaction with the other functions beyond the specification (*i.e.*, the type) of the aux function.

### 5.1.5 Monadic-Style Code.
When writing a type checker, we implement several decision procedures that may additionally return extra information such as a type in the case of type inference. In our case we moreover chose a proof-carrying code approach so that these procedures are correct by construction.

In the simple case with no extra returned information, to decide a property P we could be using the type `{P}` + `{¬P}` of informative booleans, *i.e.*, constructive proofs that P holds or not. But since we also want to be able to return error messages, we use result types that can also raise errors of the form:

Inductive info_result A E :=
  | Success (a : A)
  | Error (e : E) (h : ¬A).

If our goal is to decide proposition P then `info_result P E` will do. But if we want to return extra information as is the case for type inference, then we simply use a Σ-type. Thus, the type of `infer` looks like the following:

`infer : ∀ Σ Γ t, info_result {A & || Σ ; Γ ⊢ t ▷ A ||} typing_error`

meaning it either returns a type together with a (squashed) proof that it is indeed a type for `t`, or it returns an error message together with a proof that there doesn't exist any type for `t`.
$\Sigma; \Gamma \vdash mkApps (tConstruct ind c u) args : mkApps (tInd ci (puinst p)) (pparams p ++ indices)$

we need to show that

$\Sigma; \Gamma \vdash iota\_red (ci\_npar ci) p args br :$
$mkApps (it\_mkLambda\_or\_LetIn (case\_predicate\_context ci mdecl idecl p) (preturn p))$
$(indices ++ [mkApps (tConstruct ind c u) args])$

Here *br* is the branch corresponding to constructor *c*, which by typing must exist. The *ci* and *ind* information also have to match thanks to the case typing rule. The difficulty lies first in the relationship between the universes *u* of the actual constructor and *puinst p*, the universes that have been used to type-check the case originally. Due to cumulativity, we can have arbitrary relations between these two universe instances, including *no relationship* at all, in case a universe level is actually irrelevant. By validity and inversion lemmas, we can however show that *args* can be split into a list of parameters *pars* and actual arguments to the constructor *cargs* and that the parameters are convertible to *pparams p*. While they are convertible, they cannot be proven to be a well-typed instance of *ind_params mdecl* instantiated at (*puinst p*). However, the invariants on cumulative inductive types in § 3.6.2 ensure that the type of the vector of arguments *args* is a pointwise subtype of the type of the vector of arguments instantiated at (*puinst p*), in a context of parameters at level *u*. This is the key property to ensure that the branch that is selected, which was originally typed with an argument context at levels (*puinst p*) can indeed be instantiated with the actual arguments at level *u* as they are “smaller” according to the subtyping relation, making the reduction type-preserving.

*Positive Coinductive Types.* The subject reduction theorem holds because the case rule is disallowed on coinductive types. Indeed, subject reduction fails for dependent pattern matching on cofixpoints in Coq. This is an explicit design decision: when Giménez [1996] introduced coinductive types in Coq, he faced the problem that his presentation could either provide type preservation or decidability of type checking, but not both at the same time. It is known today how to fix the situation, either by forcing the use of co-pattern-matching and “Mendler-style” presentations of coinductives [Abel et al. 2013] or by restricting the dependent elimination of coinductive “values” to “pure” predicates, as they should rather be seen as computations [Pédrot and Tabareau 2017]. We plan to study the latter treatment in future work.

*Negative Coinductive Types.* Since Coq 8.5 [The Coq Development Team 2016], there is an alternative presentation of coinductive types using primitive projections. A coinductive record type is defined together with its projections, and pattern matching is disallowed on these types. In this case, subject reduction holds for the projection reductions thanks to the restricted shape a projection's type can take, as projection types are derived from constructor argument types. Take non-zero streams for example:

Set Primitive Projections.

CoInductive NZStream : Type := mkNZStream { head : N; tail : NZStream; head_nz : head ≠ 0 }.

Its projections have type:

head : NZStream → N; tail : NZStream → NZStream; head_nz : V (s : NZStream), head s ≠ 0

One can see that in `head_nz`'s type, the `head` reference characteristic of dependent records is replaced by the corresponding projection of the record argument of the projection. This is actually the case for all occurrences of the record variable in the type of a projection: they are always projected. This invariant is crucial for the subject reduction proof, and is clearly not enforced for general dependent pattern matching where the eliminated variable can appear anywhere in the result type. To see why, consider the reduction of `head_nz` ones : head ones ≠ 0 where ones is a cofixpoint expression
When writing such correct-by-construction decision procedures, we also have to examine results of recursive calls that might carry errors that need to be propagated. For this purpose we wish to adopt a monadic style. There is one caveat here: because of the `¬ A` proof in the error branch, `info_result` does not form a monad. But it almost does! `Success` acts as the return of the monad and for bind we use the following handy notation.

Notation "x ← r ; k" := match r with Success a ⇒ k | Error e h ⇒ Error e _ end.

The trick comes from the underscore in the notation: we are leaving a hole for the new proof we cannot produce in full generality. Let us see how it works in practice by looking at (a simplified version of) the abstraction case of `infer`:

infer Γ (tLambda na A t) :=
'(B ; hB) ← infer (Γ , na : A) t ;
Success (tProd na A B ; _)

We recursively call `infer` on the body of the abstraction, and in case it succeeds with type `B` together with correctness proof `hB`, we can return a new success with `tProd na A B` for the type. When unfolding the notations, two underscores appear:

infer Γ (tLambda na A t) :=
match infer (Γ , na : A) t with
| Success (B ; hB) ⇒ Success (tProd na A B ; _)
| Error e h ⇒ Error e _
end

They are handled by the obligation mechanism of EQUATIONS and proven interactively.

## 5.2 Abstract Computational Environment

In the specification of the type system for PCUIC, a particular choice has been made for the representation of the global environment. Namely, we use the type `global_env` containing pairs of a set of universe constraints and a list of declarations, which is appropriate for a formal specification but is inefficient as a data structure. To avoid being devoted to a particular choice of representation, we parametrize the definition of the type checker by an abstract implementation of the global environment `abs_env_impl`, and a relation `~` to connect the implementation to the specification.

### 5.2.1 Interface.
Fig. 14 describes the set of operations and decision procedures that must come with the abstract interface of a global environment. The interface is parametrized by two types, `abs_env_impl` and `abs_env_ext_impl`, corresponding respectively to the concrete representation of a global environment and a global environment extended with a polymorphic universe declaration. There are four operations to build new environments. Because we want to maintain that all environments that are manipulated are well formed, those operations are prefixed by premises that guarantee their validity. The function `abs_env_init` creates an empty environment with valid initial universe constraints and no declarations. The function `abs_env_add}s a d e c l` adds a valid new declaration to an already existing environment. Note here how the validity premise is stated. Because we cannot state it directly on the abstract environment, we instead assume that the declaration is valid (using `on_global_decls`) in any global environment in relation with the abstract environment. Similarly, there is an operation `abs_env_add_udecl` to add valid universe declarations. Finally, there is also an operation `abs_pop_decls` to remove the last declaration in an abstract environment. This operation is used during erasure in order to remove propositions from the environment, in order to keep only relevant content in it (§ 6.4).
producing an infinite stream of 1. When we reduce this expression we get to a proof of $1 \neq 0$ defined inside ones. The crucial property to show for type preservation is then that head ones is convertible to 1. This holds because we know that the record is a cofixpoint in this case as we just applied a projection on cofix reduction rule, so we can use the `cumul_cofix proj` rule to synchronize the two types. With the general pattern-matching construct we do not have such an invariant, so cofixpoint unfolding in the type expressions either has to be made unrestricted which leads to non-terminating type checking, or type preservation fails.

## 5.5 Strong Normalization

As we already said in the abstract, there is no hope to prove strong normalization of PCUIC inside Coq. We thus take it as an assumption that we will use to prove our type checker terminating. Currently, this assumption is implemented in the form of an axiom. While strong normalization is often stated as the absence of infinite reduction paths, here we state it in a more constructive manner to be able to use it in the definition of the type checker. We say that every well-typed term is accessible for the opposite of reduction (§5.1). In other words all reduction paths starting from a given well-typed term are finite.

First, we specify the transitive closure of the opposite of the reduction—which we call coreduction— as the following inductive type cored:

```
Inductive cored Σ Γ : term → term → Prop :=
| cored₁ : ∀ u v, Σ ; Γ ⊢ u ↝ v → cored Σ Γ v u
| cored_trans : ∀ u v w, cored Σ Γ v u → Σ ; Γ ⊢ v ↝ w → cored Σ Γ w u.
```

Then, the axiom of normalization corresponds to the proposition that every well-typed term of PCUIC is accessible for cored. Note that this axiom is only taken to hold in a well-formed global environment, as an ill-formed environment can contain non-positive inductive types which would let one define non-normalizing terms.

```
Axiom normalization : ∀ Σ Γ t,
  wf_ext Σ →
  welltyped Σ Γ t →
  Acc (cored Σ Γ) t.
```

The reduction order is reversed because a term should reduce to a smaller term for the order. So the axiom normalization means that the relation cored is well founded for well-typed terms, which corresponds to strong normalization of PCUIC.

## 5.6 Weak Call-by-Value Standardization

Reduction in PCUIC does not commit to a reduction order and can go under arbitrary binders. When extracting code to a programming language, it is important that the evaluation in the programming language can compute the same values as reduction in PCUIC. In this section, we prepare such a result to be later used in the correctness proof of type and proof erasure (§7), the first phase of an anticipated future verified extraction process. Precisely, we prove that whenever $Σ ; [] ⊢ t ↝* v$ where v is irreducible, then this value can actually be found using weak call-by-value evaluation (up to some remaining silent reduction under binders).

The terminology “evaluation” here refers to a one-shot inductive definition of big-step evaluation, i.e., without relying on one step reduction and reflexive transitive closure, whereas “call-by-value” means that arguments are always fully evaluated before a function or fixpoint application, and “weak” refers to the fact that abstraction and fixpoint are treated as values, without evaluating their bodies first.
Class abs_env_struct (abs_env_impl abs_env_ext_impl : Type ) := {
    (* Relations that connect an abstract to a concrete environment *)
    ~ : abs_env_impl → global_env → Prop;
    ~ext : abs_env_ext_impl → global_env_ext → Prop;

    (* Operations on the environment *)
    abs_env_init cs : on_global_univs cs → abs_env_impl;
    abs_env_add decl X kn decl :
        (V Σ, X ~ Σ → || on_global_decls Σ kn decl ||) → abs_env_impl;
    abs_env_add_udecl X udecl :
        (V Σ, X ~ Σ → || on_udecl Σ.(universes) udecl ||) → abs_env_ext_impl;
    abs_pop_decls : abs_env_impl → abs_env_impl;

    (* Queries on the environment *)
    abs_env_lookup : abs_env_ext_impl → kername → option globaldecl;

    (* Primitive decision procedures *)
    abs_env_level_mem : abs_env_ext_impl → Level → B;
    abs_env_leqb_level_n : abs_env_ext_impl → Z → Level → Level → B;
    abs_env_is_consistent : abs_env_impl → LevelSet * UnivConstraintSet → B;
    abs_env-guard : abs_env_ext_impl → FixOrCoFix → context → mfixpoint term → B}.

<caption>Fig. 14. Definition of an abstract global environment</caption>

The interface also has one query function abs_env_lookup that (optionally) returns the global declaration associated to a given name, when the name is declared. This is the only direct access to the abstract environment.

Finally, there are three decision procedures on universes and an abstract version of the guard condition (abs_env-guard). The functions abs_env_level_mem checks that a level belongs to the extended global environment. The functions abs_env_leqb_level_n takes an integer z and two levels 1 and 1' and checks whether 1 + z ≤ 1' holds in the extended global environment. Finally, the function abs_env_is_consistent checks that extending the current set of universes and constraints with additional ones remains consistent.

5.2.2 Properties. Fig. 15 shows the properties that a given implementation of an abstract environ-
ment interface must fulfill. The first set of properties is about the connection to a global environment.
Every abstract environment must be in relation to exactly one well-formed global environment
(and similarly for the version extended with polymorphic universe constraints). Note here the
use of the squash operator to prevent computational access to the concrete global environment.
The correctness properties of operations and queries of the abstract environment are stated using
direct correspondence with the specification. Finally, the statement of correctness of decision
procedures is done in a similar way, with potentially additional hypotheses to clarify when the
correctness property should hold. For instance, correctness of abs_env_is_consistent is stated as
an equivalence with a validity predicate<fnref n="24" /> under the assumption that the constraints in udecl that
are checked are about levels that appear either in udecl or are already in the environment, stated
using the declared_cstrLevels predicate. The validity predicate itself states that any valuation

<footnote n="24">²⁴Note that we are using boolean reflection to consider decision procedures as a particular form of predicates.</footnote>
Class abs_envProp (abs_env_impl abs_env_ext_impl: Type): Prop := {
(* connection to an global environment (similar definition for abs_env_ext_impl) *)
abs_env_∃X : || {Σ & X ~ Σ} ||;
abs_envWF X Σ : X ~ Σ → || WF Σ ||;
abs_env_irr X Σ Σ' : X ~ Σ → X ~ Σ' → Σ = Σ';

(* correctness properties of operations (excerpt) *)
abs_env_add_udecl_correct X Σ udecl H :
(X ~ Σ.1 ∧ Σ.2 = udecl) ↔ abs_env_add_udecl X udecl H ~ext Σ;

(* correctness property of queries *)
abs_env_lookup_correct X Σ kn decl : X ~ext Σ →
(kn, decl) ∈ declarations Σ ↔ abs_env_lookup X kn = Some decl ;

(* correctness properties of decision procedures *)
abs_env_level_mem_correct X Σ 1 : X ~ext Σ →
1 ∈ levels Σ ↔ abs_env_level_mem X 1 ;
abs_env_leqb_level_n_correct X Σ n 1 l' :
X ~ext Σ → l ∈ levels Σ → l' ∈ levels Σ →
(∀ v : valuation, satisfies v Σ → val v 1 + n ≤ val v l') ↔ abs_env_leqb_level_n X n 1 l' ;
abs_env_is_consistent_correct X Σ udecl :
X ~ Σ → For_all (declared_cstrLevels (udecl.1 ∪ levels Σ)) udecl.2 →
(∀ v, satisfies v Σ → ∃ v', satisfies v' udecl ∧ For_all (fun l ⇒ val v l = val v' l) (levels Σ))
↔ abs_env_is_consistent X udecl ;
abs_env-guard correct X Σ fix_cofix Γ mfix : X ~ext Σ →
guard fix_cofix Σ Γ mfix ↔ abs_env-guard X fix_cofix Γ mfix }.

<caption>Fig. 15. Properties of the abstract global environment (excerpt)</caption>

valid for the environment can be extended to a valuation that also validates the constraints in udecl.
The correctness properties of other decision procedures is stated in the same way.

5.2.3 Reference Implementation. To show that our primitive decision procedures are indeed dealing with decidable properties, we provide a reference implementation that directly reuses the notion of well-formed global environment and just implements naïve decision procedures on top of it.

Record reference_impl := {
reference_impl_env : global_env;
reference_implWF : || WF reference_impl_env ||}.

The correct implementation of all operations and queries is direct. As for decision procedures, the
only non-direct part are constraints and consistency checking. Indeed, for those, the specification
as the existence of a correct valuation is not obviously decidable.

Fortunately, in § 3.1 we have developed an equivalent description not using the existence of a
valuation but rather acyclicity of a corresponding graph of constraints. Concretely, the equivalence
between the two notions is proven by mediating with the lsp function, computing the length of a
shortest simple path in a graph. Namely, to know that a graph is acyclic, we simply have to check
that lsp V x x is 0 for every node x in the graph. We can express this in CoQ as a boolean decision
procedure:
section, there is no need for a context $\Gamma$ in the definition of the weak call-by-value reduction, since weak call-by-value reduction ensures that reduction of closed term will never have to consider open terms. Weak call-by-value reduction relies on the notion of *value* (Figure 12), which characterizes closed terms that are irreducible. We do not consider global definitions without bodies (i.e., axioms) in the definition, and thus our results only apply to *axiom-free global environments*. Axioms could become stuck terms during evaluation, but we actually want to show that there are no stuck terms appearing during weak-call-by-value evaluation.

**Definition axiom_free Σ := ∀ c decl, declaredConstant Σ c decl → cst_body decl ≠ None.**

A natural first step to prove the standardization theorem is to prove a *progress theorem* for weak call-by-value reduction, as usual by induction on the typing derivation:

**Lemma progress : ∀ Σ t T, wf Σ → axiom_free Σ →**
$$Σ; [] ⊢ t : T → \\ \{t' & Σ ⊢ t ↦→< wcbv t' } + (value Σ t).$$

The standardization result actually talks about a *weak call-by-value evaluation predicate* $Σ ⊢ t ⇝ v$. Since it is entirely standard to derive the definition from the definition of reduction, we omit it in the paper and refer the reader to the Coq code. Standardization relies on auxiliary results such as the fact that weak call-by-value reduction steps do not change the value under evaluation; that evaluation is included in the reflexive transitive closure of reduction; and also that subject reduction applies to evaluation. Furthermore, it relies on the fact that results of evaluation are values, and values evaluate to themselves.

From those auxiliary lemmas, it is easy to conclude that *strongly normalizing terms are evaluating to a value w.r.t. weak call-by-value evaluation*, in the sense that they evaluate to a value.

**Lemma SN_to_WN : ∀ Σ A t, wf Σ → axiom_free Σ →**
**Acc (cored Σ[]) t →**
$$Σ; [] ⊢ t : A → \\ \{v & Σ ⊢ t ⇝ v\}.$$

The proof is by induction on the assumption that $t$ is strongly normalizing. We use *progress* to either obtain $t'$ such that $Σ ⊢ t ↦→< wcbv t'$ or have that $t$ is a value. In the first case, there is $v$ such that $Σ ⊢ t ⇝ v$ by induction hypothesis, and we can use that a reduction step preserves evaluation to conclude. In the second case, we can pick $v$ as $t$.

By using the axiom that every well-typed term is normalizing we can then deduce *weak-call by-value standardization*. This theorem states that if a term $t$ reduces to a non reducible term in the empty context, then this term can also be reached by first evaluating $t$ to a value $v'$ using call-by-value big step evaluation and then performing the potentially remaining deep reductions (reductions under binders that cannot be performed by weak call-by-value reduction).

**Lemma wcbv_standardization : ∀ Σ T t v, wf Σ → axiom_free Σ →**
$$Σ; [] ⊢ t : T → \\ Σ; [] ⊢ t ↦→< v → \\ ¬ {t' & Σ; [] ⊢ v ↦→ t'} → \\ \{v' & Σ ⊢ t ⇝ v' * Σ; [] ⊢ v' ↦→< v'\}.$$

To show this, we use strong normalization and $SN_{to\_WN}$ for $t$ to obtain $v'$ such that $Σ ⊢ t ⇝ v'$. Because evaluation entails reduction, we also have that $Σ; [] ⊢ t ↦→< v'$.
By the assumption that $t$ also reduces to $v$ and confluence, we obtain $v''$ such that $Σ; [] ⊢ v ↦→< v''$ and $Σ; [] ⊢ v' ↦→< v''$.
Since $v$ is irreducible, we know that in fact $v = v''$.
Definition is_acyclic (G : RootedGraph) : B ::= for_all (fun x ⇒ match lsp V x x with | Some 0 ⇒ true | _ ⇒ false end) V.

This `is_acyclic` procedure can be directly used to implement `abs_env_is_consistent`.

To implement the decision procedure checking a constraint between levels, we use a rephrasing using labeling on graph.

Definition leqVertices n x y := V l, correct_labeling l → l x + n ≤ l y.

This characterization is not a *priori* decidable as there is potentially an infinite number of such correct_labeling. However, using lsp again, we can prove that when the graph is acyclic, this property can just be tested on one correct labeling, namely the one induced by lsp.

Lemma leqVertices_charact n x y {In y V} : leqVertices G n x y ↔ Some n ≤ lsp G x y.

Using this, we can characterize the statement “x+n is smaller than y” by either y is in the graph of constraints and lsp G x y is bigger than n, or y is constraint free, and in that case, n must be 0 and x must be at distance 0 from Set (which is the source s G of the graph).

Definition leqbVertices n x y : B ::= if mem y V then le_dec (Some n) (lsp G x y) else N.eqb n 0 && (eq_dec x y || le_dec (Some 0) (lsp G x (s G))).

Because all the (in)equalities involved in the definition are decidable, this gives rise to a boolean decision procedure for constraint checking.

### 5.2.4 More efficient implementations.
Beyond this naïve implementation, we additionally provide a more efficient representation of the environment to perform lookups by using *AVL trees* (a.k.a. self-balancing binary search tree) in the file PCUIC: WfEnvImpl. This representation allows additions, removals and lookups in the environment in $O(\log n)$.

But the main venue for optimization is of course the decision procedure for consistency. We could for instance use the algorithm proposed by Bender et al. [2015], as recently formalized by Guéneau et al. [2019] (in the particular case where there is no constraint of the form $\le$) to check the acyclicity of the graph. Similarly, we could experiment with the proposal of Bezem and Coquand [2022] using join-semilattices.

Note that the performance of the acyclicity checking algorithm is currently a performance bottleneck in Coq too, and our formalization offers the possibility to experiment with more efficient consistency checking and first prove it is correct before deploying it in an official release of Coq.

## 5.3 Conversion and Cumulativity Without Fuel

Being able to decide conversion and cumulativity is essential for defining a type checker and relies on a lot of the meta-theory. The definition of the conversion algorithm is optimized to be more efficient than just comparing the normal forms up to cumulativity. It has been designed so that it mimics the conversion algorithm implemented in Coq which consists of

(1) first weak-head reducing the two terms without $\delta$-reductions (i.e., without unfolding definitions);

(2) then comparing their heads, and if they match comparing the subterms recursively;

(3) if they do not match, checking if some computation (pattern-matching or fixpoint) or even the whole term is blocked by a definition that could unfold to a value, unfolding this definition and comparing again.

From this we can already identify a few requirements. First, weak-head reduction has to be defined as an algorithm, which in turn needs normalization (§4.5) to be proven terminating. Furthermore, as normalization can only be assumed for well-typed terms, the conversion algorithm is only defined
Inductive whne Σ (Γ : context) : term → Type :=
whne_rel i : option_map decl_body (nth_error Γ i) = Some None → whne Σ Γ (tRel i)
whne_const c u decl : lookup_env Σ c = Some (ConstantDecl decl) → decl.(cst_body) = None →
whne Σ Γ (tConst c u)
whne_app f v : whne Σ Γ f → whne Σ Γ (tApp f v)
whne fixed mfix idx args d arg :
nth_error mfix idx = Some d → nth_error args (rarg d) = Some arg →
whne Γ arg → whne Γ (mkApps (tFix mfix idx) args)
whne_case i p c brs : whne Σ Γ c → whne Σ Γ (tCase i p c brs)
whne Project : whne Σ Γ c → whne Σ Γ (tProj p c)

Inductive whnf Σ (Γ : context) : term → Type :=
whnf_ne t : whne Σ Γ t → whnf Σ Γ t
whnf_sort s : whnf Σ Γ (tSort s)
whnfProduct na B : whnf Σ Γ (tProduct na B)
whnf_lam na B : whnf Σ Γ (tLambda na B)
whnf_cstrapp i n u v : whnf Σ Γ (mkApps (tConstruct i n u) v)
whnf_indapp i u v : whnf Σ Γ (mkApps (tInd i u) v)
whnf fixed mfix idx args :
(∃ d, nth_error mfix idx = Some d ∧ nth_error args (rarg d) = None) ∨ (nth_error mfix idx = None)
→ whnf Γ (mkApps (tFix mfix idx) args)
whnf_cofixed mfix idx v : whnf Σ Γ (mkApps (tCofix mfix idx) v).

<caption>Fig. 13. Definition of weak-head normal forms in PCUIC</caption>

5.7 Canonicity

Canonicity for PCUIC states that any non-reducible inhabitant of an (co-)inductive type is an
applied constructor or a cofixpoint. The proof goes in two steps, first we show that any non-
reducible term is in weak-head normal form. A weak-head normal form (Fig. 13) is either a
term starting with a constructor (a type constructor, a lambda abstraction, a constructor of an
inductive type), a partially applied fixpoint, any cofixpoint, or a neutral term (whne). A neu-
tral term is either a variable (not associated to a let-in construct), an axiom (i.e., a constant
with no body) or a destructor (an application, a fixpoint, a pattern matching or a projection)
whose evaluation is blocked on a neutral term. We can reuse the progress lemma of § 5.6 to de-
rive the following lemma which states that weak-head normal forms describe all stuck terms.

Lemma whnf_progress : ∀ Σ t T,
  axiom_free Σ → wf Σ →
  Σ ; [] ⊢ t : T →
  ¬ { t' & Σ ; [] ⊢ t ↝ t' } →
  whnf Σ [] t.

From this, we can formulate a classification theorem by proving that no neutral terms can exist
in an empty context, and then analyzing the potential whnf inhabitants of an inductive type (the
definition construct_cofix_discr (head t) just says that the head of t is either a constructor or a
cofixpoint).
on well-typed terms. This means that we need to know that the term obtained after reduction is still well typed, which is guaranteed by subject reduction (§4.4). Finally, when reducing a term during conversion, we sometimes need to focus on subterms to reduce them to constructors. This is the case for pattern matching but also for fixpoints that only unfold when their recursive argument is a constructor to preserve termination. As the argument is not itself a subterm of the fixpoint, we use the more general notion of position inside the original term to ensure termination. We now describe all these points in more details, leading up to the definition of a decision algorithm for conversion and cumulativity.

### 5.3.1 Term positions.
A position in a term can be seen as a path from the root the desired subterm. As our terms have structure this path is described by a sequence of choices one makes at each node. For instance `app_l` goes left in an application `tApp u v` and point to `u`.

**Inductive choice :=**

| app_l | app_r | case_par (n : N) | case_preturn | case_c | case_brsbody (n : N) | proj_c | fix_mfixTy (n : N) | fix_mfix.bd (n : N) | cofix_mfix Ty (n : N) | cofix_mfixbd (n : N) | lam Ty | lam_tm | prod_l | prod_r | let bd | let Ty | let_in.

**Definition position := list choice.**

Of course, choosing `app_l` when the term is `tLambda` does not make sense. We thus **define a boolean predicate validpos t p** that checks that the position `p` is valid in term `t`. This lets us define the type of valid positions in a term:

**Definition pos (t : term) :=** `{p : position | validpos t p = true}`.

As advertised, the goal of these positions is to help in the termination proof of our reduction machine and our cumulativity checker. We thus define an order on positions as below:

**Inductive positionR : position → position → Prop :=**

| positionR_app_lrpq : positionR (app_r :: p) (app_l :: q)

| positionR_deeCPq : positionR p q → positionR (c :: p) (c :: q)

| positionR_rootcp : positionR (c :: p) [].

The idea is that going deeper inside a term, always yields a smaller position, but crucially going on the right of an application node is smaller than going left. This last point is what lets us inspect and reduce the argument of a fixpoint after inspecting the fixpoint itself.

This order in itself is not well founded, as one could go arbitrarily deep. It becomes well founded when restricted to positions in the same term:

**Definition posR {t} (p : pos t) : Prop :=** positionR p.π₁ q.π₁.

**Lemma posR_Acc : ∀ t p, Acc (@posR t) p.**

In the reduction and cumulativity algorithms, instead of always carrying around the whole term together with a position, we adopt the equivalent approach of having the term currently under scrutiny, together with its evaluation context: the whole term with a hole. We represent those using **stacks**, defined as follows in a dual manner to positions.

**Variant stack_entry : Type :=**

| App_l (v : term)

| App_r (u : term)

| Prod_l (na : aname) (B : term)

| Prod_r (na : aname) (A : term)

| Lambda Ty (na : aname) (b : term)
**Theorem classification:** $\forall \Sigma \ t \ i \ u \ args$, 
$\qquad axiom_free \Sigma \rightarrow wf \Sigma \rightarrow$ 
$\qquad \neg \{t' \ \& \ \Sigma; \ [] \vdash t \leadsto t'\} \rightarrow$ 
$\qquad \Sigma; \ [] \vdash t \ : \ mkApps (tInd i u) \ args \rightarrow$ 
$\qquad construct_cofix_discr (head t)$.

Finally, thanks to normalization and subject reduction, we can show the usual canonicity statement for PCUIC, saying that any closed inhabitant of an inductive type is convertible to a fully applied constructor, and any closed inhabitant of a coinductive type is convertible either to a fully applied constructor or to a cofixpoint.

**Lemma pcuic_canonicity:** $\forall \Sigma \ t \ i \ u \ args$, 
$\qquad axiom_free \Sigma \rightarrow wf \Sigma \rightarrow$ 
$\qquad \Sigma; \ [] \vdash t \ : \ mkApps (tInd i u) \ args \rightarrow$ 
$\qquad \{t':term \ \& \ \Sigma; \ [] \vdash t' \ : \ mkApps (tInd i u) \ args \times \Sigma; \ [] \vdash t \ \approx_s \ t' \ \times \ construct_cofix_discr (head t')\}$.

## 5.8 Consistency

Using canonicity, it is easy to derive the following consistency result for PCUIC. As is standard, consistency is stated as the fact that the empty type cannot be inhabited in the empty context. Because our definition of PCUIC is parametrized by a global environment our statement needs to postulate that this global environment contains the empty type to be able to state the result. $\perp_{oib}$ correspond to the one_inductive_body in tProp with no parameter or constructor, and $\perp_{mib}$ is the mutual_inductive_body consisting only of $\perp_{oib}$.

**Theorem pcuic_consistent:** $\forall \Sigma \ t \ \perp_{pcuic}$, 
$\qquad declared_inductive \ \Sigma \ \perp_{pcuic} \ \perp_{mib} \ \perp_{oib} \rightarrow$ 
$\qquad wf_ext \ \Sigma \rightarrow axiom_free \ \Sigma \rightarrow$ 
$\qquad \Sigma; \ [] \vdash t \ : \ tInd \ \perp_{pcuic} \ [] \rightarrow \perp$.

Technically speaking, this theorem is a consistency result relying crucially on the soundness of the surrounding logic of CoQ (the proof assistant) and the adequate formulation of PCUIC (the formalized theory) for which we assume strong normalization.

## 6 A SOUND AND COMPLETE CHECKER FOR PCUIC

We now turn to the definition of a type checker for PCUIC and a proof that it is sound and complete with respect to the specification given in § 3. In order to define this type checker, all properties involved in typing judgments must be replaced by actual decision procedures. To make our type checker more modular and independent of a specific implementation, we parametrize type checking by an abstract notion of environment on which only basic decision procedures are postulated. This allows us to define a generic type checker that can be later optimized, by optimizing these basic decision procedures. For instance, the most direct venue for optimization is the decision procedure for consistency of the universe hierarchy.

After giving some technical insights and presenting the abstract interface of an environment used for type checking, we present the generic conversion/cumulativity checking algorithm and type inference. We then discuss a slightly optimized implementation of the abstract environment and finally analyze the performance of the safe checker compared to the one of CoQ.
| Lambda BD (na : aname) (A : term)
(* ... other cases are similar, reflecting the constructors of choice *)

Definition stack := list stack_entry.

A stack is composed of a list of nodes with a hole. The hole might for instance appear in one of the branches of a pattern matching as expressed by `branches_hole` or inside the motive as described by a `predicate_hole`.

From a stack $\pi$, one can do two things: (i) plug a term $t$ in its hole, written $zip t \pi$; (ii) recover the position associated to its hole: `stack_position \pi`.

### 5.3.2 Weak-Head Normalization Using a Stack Machine.
We are now equipped enough to define weak-head reduction, that is a reduction algorithm which produces a term in weak-head normal form as described in Fig. 13. As we often need to inspect subterms of an expression, the basic input of the algorithm is not just a term but a term under focus as well as its surrounding context, which we called stack in §5.3.1. A reduction step amounts to either reducing the whole expression (term and stack, zipped together with the function `zip`) or focusing on a subterm, and sometimes looking things up on the stack. To prove termination, we use a (dependent) lexicographical order on first coreduction of the whole expression, and then the position order for the positions corresponding to the stacks:

Definition R_aux $\Gamma$ :=
dlexprod (cored $\Sigma \Gamma$) (@posR).

Definition R $\Gamma$ (u v : term $\ast$ stack) :=
R_aux $\Gamma$ (zip u ; stack_pos (fst u) (snd u)) (zip v ; stack_pos (fst v) (snd v)).

We can then define our algorithm by well-founded induction on $\mathbb{R}$. For this, we start by defining a function `reduce_stack` in open-recursion style (§ 5.1). It takes as argument a term $t$, a stack $\pi$ such that the whole expression is well typed (`welltyped $\Sigma \Gamma$ (zip (t, $\pi$))`), as well as a function corresponding to recursive calls that can only be applied on pairs that are smaller than $(t, \pi)$ for $\mathbb{R}$. It returns a new pair $(t', \pi')$ together with a proof that $(t', \pi')$ is smaller than or equal to $(t, \pi)$ for $\mathbb{R}$ so that one can conclude that the resulting whole expression is indeed a reduct of the original one, possibly in zero steps. Additionally, it also provides some technical invariants to ensure that the produced terms are in weak-head normal form.

We can then close the open recursion and obtain a `reduce_term` function that we prove sound, which is expressed by saying that it indeed computes a term that is in the transitive closure of one-step reduction ($\rightsquigarrow$):

Theorem `reduce_term{sound} X` :
$\forall \Gamma t (h : \forall \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \text{welltyped } \Sigma \Gamma t) \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \| \Sigma ; \Gamma \vdash t \rightsquigarrow * \text{ reduce\_term } \Gamma t h \|$.

Note that the theorem is quantified over any abstract environment $X$, and properties mentioning a concrete environment $\Sigma$, such as typing, are stated by quantifying over any concrete environment in relation with $X$. Similarly, we can prove that the reduction is complete, which is expressed by saying that the produced term is in weak-head normal form (Fig. 13):

Theorem `reduce\_term\_complete X` :
$\forall \Gamma t (h : \forall \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \text{welltyped } \Sigma \Gamma t) \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \| \text{whnf } \Sigma \Gamma (\text{reduce\_term } \Gamma t h) \|$.
## 6.1 Technical Insight

Before we delve into the definition of our type checker, let us address some technical points that are either needed as preliminaries or that give insight to the methods that we use for our formalization that are not directly related to our problem at hand.

6.1.1 *Enforcing computational irrelevance.* Because we want to ultimately obtain a type checker that can be extracted and run efficiently, we are very careful to separate the relevant content used by the algorithm from the computationally irrelevant content pertaining to the invariants it maintains. For this we use the facilities offered by the sort *Prop* of *Coq*, whose inhabitants are erased at extraction time. However, most predicates and relations from the previous sections (for instance typing) are defined in sort *Type*, in order to avoid having to struggle with the dichotomy between relevant and irrelevant while doing the meta-theoretic proofs. Throughout this section, we thus make extensive use of *squashing* of a type `X` into *Prop*, written `||X||`, to make relevant content irrelevant.

6.1.2 *EQUATIONS.* In order to ease the use of the techniques described in this section, we heavily rely on the *EQUATIONS* [Sozeau and Mangin 2019] plugin for *Coq*. This plugin provides notations and mechanisms to help with the definition of complex, non-structural recursive definitions. In particular, it has built-in support for definitions by well-founded induction (see §5.1). Moreover, its *obligation* mechanism, which lets users leave holes in the definition of functions and fill them later in proof mode, is crucial to be able to write complex proof-carrying code.

6.1.3 *Views.* When manipulating datatypes, typically terms, we often wish to inspect them in a way that is not expressible directly by pattern matching. For instance, when considering reduction we want to distinguish exactly three cases: the term is either a `λ`-abstraction applied to a list of arguments (i.e., of the form `mkApps (tLambda na A t) 1`), a fixpoint applied to a list of arguments, or any other term.

To express these custom case distinctions, we rely on *views*, originally introduced by *Wadler* [1985] and later rephrased in the setting of dependent types by *McBride and McKinna* [2004]. Examples of such views are given in PCUIC: *Views*, such as `fix Lambda app view`, corresponding to the case distinction we outlined above:

```
Inductive fixoglba_app_view : term → term → Type :=
| fixoglba_app_fix mfix i l a : fixoglba_app_view (mkApps (tFix mfix i) 1) a
| fixoglba_app...lambda na ty b l a : fixoglba_app_view (mkApps (tLambda na ty b) 1) a
| fixoglba_app_other t a : ¬ isFixLambda_app (tApp t a) → fixoglba_app_view t a.
```

Compared to the non-dependent case, however, our views are richer: they not only allow for a convenient case distinction, but embed, either in their indexed type (as for the first two constructors) or extra arguments (as in the last constructor), the meaning of this case distinction. This way, a pattern-matching on a view gives us the logical information corresponding to the case distinction we apply. Another important benefit of this technique is that we get one proof obligation for each case of the view. In a setting where the "default" view case typically corresponds to more than 10 branches in a regular pattern matching, this is important to keep proofs manageable: we get only one obligation to solve instead of 10 very similar ones.

6.1.4 *Open Recursion.* In order to implement our type checker, we define several functions mutually, involving complex termination measures. Mutually defined fixpoints are painful to reason about so we lighten our burden by using a technique called *open recursion*. The idea is quite simple: instead of defining a function directly as a (mutual) fixpoint, we define the associated *functional* and then we take the corresponding fixed point. Concretely, the function takes an extra argument which is a
5.3.3 *Safe Conversion.* We define *safe conversion and cumulativity* while proving it sound and complete by having it return either a conversion or cumulativity proof for its inputs, or an error message together with a proof of the negation of conversion or cumulativity, using the monadic style explained in §5.1.

At the beginning of the section, we hinted at the fact that our conversion and cumulativity checker proceeds in different phases. We record the current phase using what we call *state*, defined below.

Inductive state := Reduction | Term | Arg s | Fallback.

Initially, we are in *Reduction* mode in which we start by weak-head reducing both terms (except for *δ*-reduction, meaning we do not unfold any definition). In this phase we also decompose each term into a term and a stack, moving all applications nodes to the stack and consuming them when possible, as we described in §5.3.2.

We then move to the *Term* phase where we inspect the two terms below their respective stacks. Essentially in this phase we check whether the two terms have the same head, in which case we compare the subterms recursively (back to phase *Reduction*). For instance, when comparing two *λ*-abstractions, this is sufficient and we can directly raise an error message if subterm comparison fails. The proof of completeness ensures that we are not missing a case. It exploits properties of injectivity of weak-head normal forms (shown in PCUIC: *Conversion* and PCUIC: *ConvCumInversion*), which follow from confluence. There are still some special cases to consider. For instance, when comparing two constants, we first check whether they happen to be instances of the exact same constant (i.e., the same global reference with equal universe instances), but in case they are not, it does not necessarily mean that the terms are different. We then unfold one of the constants and resume comparison from the *Reduction* phase. We need to do similar things for pattern matching, (co)fixpoints and projections.

When the previous phase succeeds (i.e., when the two terms have the same head and convertible subterms), we proceed to verify that the applications present on top of the two stacks are themselves pointwise convertible. This *Arg s* phase simply looks through the two stacks and compares the application arguments (in *Reduction* mode). If this succeeds, we can conclude the whole terms are indeed in the conversion or cumulativity relation.

In the *Term* phase we may however end up with two terms with different heads. Once again, this does not mean that they are not in the cumulativity relation. We end up in the *Fallback* case in which we check whether one of the terms could be further reduced by unfolding a constant. This happens when the term is itself a constant, but also when it is a pattern matching or projection applied to a stuck term, or a fixpoint whose recursive argument is stuck. In those cases we reduce the argument to weak-head normal form (including *δ*-reductions) and check whether we can make progress (e.g., it is a constructor for pattern matching). If progress can be made, we go back to the *Term* phase (no need to go through *Reduction* again as the terms are still in weak-head normal form). In case no progress can be made on either side, as a last resort we compare the terms syntactically. This is needed for heads like sorts or variables that have not been considered before, as well as for all neutral expressions (i.e., stuck terms).

These phases are defined respectively in open recursion through the functions _isconv_red, _isconvProg, _isconv_args, and _isconv_fallback_. They are combined together into isconv_full which involves an order slightly more complicated than for reduction as the phase (state) is also taken into account. We also call this order R and show it is well founded.

Finally, starting from empty stacks, we define *conversion checking for well-typed terms*, named `isconv_term`, and show it sound and complete. Again, the theorems are stated for any abstract environment X.
function to perform the recursive calls, and this function is guarded to only be called on smaller arguments w.r.t. to a previously chosen relation.

Taking a silly example on purpose, we could define functions that test whether a natural number is odd or even as follows:

Fixpoint even (n : N) : B :=
match n with
| 0 = true
| S n = odd n
end

with odd (n : N) : B :=
match n with
| 0 = false
| S n = even n
end.

The same example in open recursion, using Inductive mode := Even | Odd to distinguish between the two functions even and odd, looks as follows:

Equations _even n
(aux : mode → ∀ m, m < n → B ) : B :=
 _even 0 aux := true ;
 _even (S n) aux := aux Odd n _.

Equations _odd n
(aux : mode → ∀ m, m < n → B ) : B :=
 _odd 0 aux := false ;
 _odd (S n) aux := aux Even n _.

We first define _even and _odd which are functions that are not even recursive yet, but take as argument aux to represent recursive calls. This is where the mode comes into play, it lets one choose which function to call recursively. Here we use EQUATIONS to infer automatically the proof that n < S n. Then we can actually perform (well-founded) recursion to *close the loop* by using a function even_orOdd which uses itself as aux.

Equations even_or_odd (M : mode) (n : N) : B by wf n lt :=
even_or_odd Even n := _even n even_or_odd ;
even_or_odd Odd n := _odd n even_or_odd .

Definition even := even_or_odd Even.
Definition odd := even_or_odd Odd.

While on such an example, it might not appear very interesting, in our case this lets us define all components of a mutual recursive block in isolation and prove things about them without having to worry about recursion or the interaction with the other functions beyond the specification (*i.e.*, the type) of the aux function.

### 6.1.5 Monadic-Style Code.
When writing a type checker, we implement several decision procedures that may additionally return extra information such as a type in the case of type inference. In our case we moreover chose a proof-carrying code approach so that these procedures are correct by construction.

In the simple case with no extra returned information, to decide a property P we could be using the type {P} + {¬P} of informative booleans, i.e., constructive proofs that P holds or not. But since we also want to be able to return error messages, we use result types that can also raise errors of the form:

Inductive info_result A E :=
| Success (a : A)
| Error (e : E) (h : ¬ A).

If our goal is to decide proposition P then info_result P E will do. But if we want to return extra information as is the case for type inference, then we simply use a Σ-type. Thus, the type of infer looks like the following:

infer : ∀ Σ Γ t, info_result {A & || Σ ; Γ ⊢ t ▷ A ||} typing_error

meaning it either returns a type together with a (squashed) proof that it is indeed a type for t, or it returns an error message together with a proof that there doesn't exist any type for t.

When writing such correct-by-construction decision procedures, we also have to examine results of recursive calls that might carry errors that need to be propagated. For this purpose we wish
**Theorem isconv_term{sound} X:**
$$ \forall \Sigma (wf\Sigma : X \sim_{ext} \Sigma) \Gamma Rle t_1 h1 t2 h2, \\ \qquad isconv_term \Gamma Rle t_1 h1 t2 h2 = ConvSuccess \rightarrow \|\Sigma; \Gamma \vdash t_1 \leq_s^{Rle} t2 \|. $$

**Theorem isconv\_term\_complete X:**
$$ \forall \Sigma (wf\Sigma : X \sim_{ext} \Sigma) \Gamma Rle t_1 h1 t2 h2 e, \\ \qquad isconv\_term \Gamma Rle t_1 h1 t2 h2 = ConvError e \rightarrow \neg \|\Sigma; \Gamma \vdash t_1 \leq_s^{Rle} t2 \|. $$

## 5.4 A Typechecking Algorithm for PCUIC

Given the work already done in §3.3, the definition of a *type checking algorithm* itself is quite straightforward: it closely follows the structure laid out by the mutually defined bidirectional judgments, and poses no termination issue—as opposed to conversion—since the type checker operates by a simple induction on the structure of the term. Actually, rather than a type checker, the main function we define is *type inference*,<fnref n="25" /> from which we can easily define type checking. In more details, the function takes a term `t` in well-formed environment `Σ` and context `Γ`, and returns a type together with a derivation of `Σ`; `Γ ⊢ t > A`, the inductively defined inference judgment, so the function is correct by construction. We cannot separate the definition from the correctness proof, since the conversion checker that is called as a sub-routine expects a well-typed term as input in order to be terminating. We do not detail the definition of type inference here, as it follows scrupulously the bidirectional representation, we just need to replace propositional assumptions, such as convertibility or universe constraints, by the corresponding decision procedures.

We also provide a retyping algorithm, which takes a term and a proof that this term is well typed and computationally infers an explicit type for it. This is an optimized version of type inference where many conversion and type-checking tests can be elided, because we know they are valid thanks to the assumption that the initial term is well typed. For instance, to retype an application `tApp t u`, it is only necessary to retype `t` and get a type `tProd na A B`, and we can directly return `B{0 := u}`, as we know that `u` checks against `A` since the term is well typed. This retyping algorithm is used by extraction, to detect types and proofs in the term that can be erased.

Finally, we define a *function checking well-formedness of an environment*, by iteratively checking each constant or inductive declaration as specified in §2.6.

## 6 TYPE AND PROOF ERASURE FOR PCUIC

One of the key features of the CoQ proof assistant is extraction [Letouzey 2004], used for instance in the CompCert compiler [Leroy 2006]. The current implementation of extraction [Letouzey 2002] consists of a general procedure to erase types and proofs and several different mechanisms to extract these erased terms into industrial programming languages like OCaml, Haskell, or Scheme. We verify the type and proof erasure procedure for PCUIC with respect to big-step call-by-value evaluation as introduced in §4.6. In future work, we plan to also verify CoQ's extraction mechanism to OCaml and other languages. Already Letouzey's work [Letouzey 2004] separates the erasure to pure, untyped λ-calculus (equivalent to ours) from the MiniML extraction that is actually implemented by extraction (inserting `Obj.magic` to embed untyped terms and applying optimizations).

In this section, we first introduce the target calculus of erasure, which is a simplified version of PCUIC with one extra constructor □ denoting erased terms. We then define an erasure function $\mathcal{E}$, using the retyping algorithm from §5.4. Following Letouzey [2004], we introduce an erasure relation extending the erasure function, prove its correctness and deduce the strongest possible correctness

<footnote n="25">²⁵Which is decidable due to our Church-style syntax, i.e., using annotated abstractions, as opposed to a Curry-style one.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 14. Definition of an abstract global environment</figcaption></figure>

to adopt a monadic style. There is one caveat here: because of the $\neg A$ proof in the error branch, `info_result` does not form a monad. But it almost does! `Success` acts as the return of the monad and for bind we use the following handy notation.

Notation "x $\leftarrow$ r ; k" := match r with Success a $\Rightarrow$ k | Error e h $\Rightarrow$ Error e _end.

The trick comes from the underscore in the notation: we are leaving a hole for the new proof we
cannot produce in full generality. Let us see how it works in practice by looking at (a simplified
version of) the abstraction case of infer:

infer Γ (tLambda na A t) :=
'(B ; hB) $\leftarrow$ infer (Γ, na : A) t ;
Success (tProd na AB; _)

We recursively call infer on the body of the abstraction, and in case it succeeds with type B
therefore together with correctness proof hB, we can return a new success with tProd na A B for the type.
When unfolding the notations, two underscores appear:

infer Γ (tLambda na A t) :=
match infer (Γ, na : A) t with
| Success (B ; hB) ⇒ Success (tProd na A B; _)
| Error e h ⇒ Error e _
end

They are handled by the obligation mechanism of EQUATIONS and proven interactively.
<figure><img src="image_7.png" /><figcaption>Fig. 16. Syntax of $\lambda_{\square}$</figcaption></figure>

result for the erasure function: if a program of first-order inductive type (i.e., an inductive type containing no proofs or functions) evaluates to a value, its erasure evaluates to the same value. As a corollary, we also get that in case the return type of a function $f$ is a first-order inductive type, $f$ can be erased separately to some function which will evaluate to the same value as $f$ once applied to enough arguments.

Note that, like in the extraction currently implemented in Coq, the rule $Prop \le Type$ has to be disabled for type checking (using the flag structure explained at the end of §2.5) to ensure that erasability is stable by expansion.

## 6.1 The Target Calculus $\lambda_{\square}$

The target of the type and proof erasure procedure is $\lambda_{\square}$, an untyped $\lambda$-calculus. $\lambda_{\square}$ is syntactically similar to PCUIC (see syntax in Fig. 16). It has the same constructors, but subterms which can only contain types are left out (because they would be erased anyway). Furthermore, $\lambda_{\square}$ has an additional constructor $\square$ denoting computationally meaningless content which was erased. Technically, the code shares the same syntax as that for PCUIC, but inside a different module. To avoid confusion and the additional complexity of considering modules, we have taken the liberty to prefix every term with 'E.' in the definition.

The weak call-by-value (big-step) evaluation relation for $\lambda_{\square}$ is defined like for PCUIC (see §4.6), with three amendments:<fnref n="26" />

(1) If $\Sigma \vdash a \Downarrow \square$ then $\Sigma \vdash E.tApp a t \Downarrow \square$.

(2) If $\Sigma \vdash a \Downarrow \square$ and $\Sigma \vdash t \square \dots \square \Downarrow v$ then $\Sigma \vdash E.tCase (i, p) a [(n,t)] \Downarrow v$. $n$ times

(3) The $E.tFix$ rule is similarly extended to also apply if the principal argument evaluates to $\square$. Intuitively, the first rule corresponds to the fact that applying a type or a proof to an argument will be a type or proof. The second rule corresponds to the fact that if a case analysis is not erased to $\square$, this is because it returns something computational, and consequently the case analysis on the proof which was erased to $\square$ has to come from a subsingleton elimination (§2.6.3). Due to this, the rule actually covers all possible eliminations from $tProp$ to produce a computational value. This will be explicit in the proof of correctness of erasure (§6.3). The third rule allows the unfolding of fixpoints computing a value by recursion on proofs.

<footnote n="26">²⁶We present only the changes for big-step evaluation.</footnote>
## 6.2 Abstract Computational Environment

In the specification of the type system for PCUIC, a particular choice has been made for the representation of the global environment. Namely, we use the type `global_env` containing pairs of a set of universe constraints and a list of declarations, which is appropriate for a formal specification but is inefficient as a data structure. To avoid being devoted to a particular choice of representation, we parametrize the definition of the type checker by an abstract implementation of the global environment `abs_env_impl`, and a relation $\sim$ to connect the implementation to the specification.

6.2.1 *Interface*. Fig. 14 describes the set of operations and decision procedures that must come with the abstract interface of a global environment. The interface is parametrized by two types, `abs_env_impl` and `abs_env_ext_impl`, corresponding respectively to the concrete representation of a global environment and a global environment extended with a polymorphic universe declaration. There are four operations to build new environments. Because we want to maintain that all environments that are manipulated are well formed, those operations are prefixed by premises that guarantee their validity. The function `abs_env_init` creates an empty environment with valid initial universe constraints and no declarations. The function `abs_env_add Decl` adds a valid new declaration to an already existing environment. Note here how the validity premise is stated. Because we cannot state it directly on the abstract environment, we instead assume that the declaration is valid (using `on_globaldecls`) in any global environment in relation with the abstract environment. Similarly, there is an operation `abs_env_add U UDecl` to add valid universe declarations. Finally, there is also an operation `abs_pop Decl` to remove the last declaration in an abstract environment. This operation is used during erasure in order to remove propositions from the environment, in order to keep only relevant content in it (§ 7.4).

The interface also has one query function `abs_env_lookup` that (optionally) returns the global declaration associated to a given name, when the name is declared. This is the only direct access to the abstract environment.

Finally, there are three decision procedures on universes and an abstract version of the guard condition (`abs_env-guard`). The function `abs_env_level_mem` checks that a level belongs to the extended global environment. The function `abs_env_leqb_level_n` takes an integer $z$ and two levels $1$ and $1'$ and checks whether $1 + z \le 1'$ holds in the extended global environment. Finally, the function `abs_env_is_consistent` checks that extending the current set of universes and constraints with additional ones remains consistent.

6.2.2 *Properties*. Fig. 15 shows the properties that a given implementation of the abstract environment interface must fulfill. The first set of properties is about the connection to a global environment. Every abstract environment must be in relation to exactly one well-formed global environment (and similarly for the version extended with polymorphic universe constraints). Note here the use of the squash operator to prevent computational access to the concrete global environment. The correctness properties of operations and queries of the abstract environment are stated using direct correspondence with the specification. Finally, the statement of correctness of decision procedures is done in a similar way, with potentially additional hypotheses to clarify when the correctness property should hold. For instance, correctness of `abs_env_is_consistent` is stated as an equivalence with a validity predicate$^{27}$ under the assumption that the constraints in `UDecl` that are checked are about levels that appear either in `UDecl` or are already in the environment, stated using the `declared_cstrLevels` predicate. The validity predicate itself states that any valuation valid for the environment can be extended to a valuation that also validates the constraints in `UDecl`. The correctness properties of other decision procedures are stated in the same way.

<footnote>$^{27}$Note that we are using boolean reflection to consider decision procedures as a particular form of predicates.</footnote>
Equations $\mathcal{E} \Gamma (Ht : \forall \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \text{welltyped } \Sigma \Gamma t) : \mathbf{E}.\text{term} := \mathcal{E} \Gamma H \Gamma t \text{ with } (\mathbf{is}\_\text{erasableb} \times \Gamma t Ht) :=$
$\begin{aligned}
& \{ \mid \text{left is\_er} := \square; \\
& \mid \text{right not\_is\_er with } t := \{ \\
& \quad \mid \text{tRel } i := \mathbf{E}.\text{tRel } i \\
& \quad \mid \text{tConst } kn \text{ u } := \mathbf{E}.\text{tConst } kn \\
& \quad \mid \text{tLambda } na \text{ b } b' := \mathbf{E}.\text{tLambda } na.(\text{binder\_name}) (\mathcal{E} (\Gamma, na : b) b') \\
& \quad \mid \text{tApp } f u := \mathbf{E}.\text{tApp} (\mathcal{E} \Gamma f \_) (\mathcal{E} \Gamma u \_) \\
& \quad \quad (* \dots *) \}.
\end{aligned}$

<caption>Fig. 17. Erasure function (excerpt)</caption>

## 6.2 Definition of an Erasure Function

In the remainder of the section, we assume an abstract environment X. Parametrized by this abstract environment, a type and proof erasure function $\mathcal{E}$ can be defined from terms of PCUIC to terms of $\lambda_{\square}$.

Its implementation is based on a decision procedure `is_erasableb` which checks whether a well-typed term is *erasable*. The implementation relies on the retyping function which correctly reconstructs the type of merely well-typed terms, along with *weak-head reduction* to inspect types. We leave out the implementation of `is_erasableb` as we only need that it reflects the property `isErasable`, specifying that a term is erasable when it is typeable with some type $\Gamma$ which is either an arity or typeable itself with sort `tProp`.

Definition `isErasable` $\Sigma \Gamma t := \{ \Gamma \& \Sigma ; \Gamma \vdash t : \Gamma \times (\mathit{isArity} \Gamma + \Sigma ; \Gamma \vdash T : \mathit{tProp}) \}$.

This boolean reflection proof in particular involves proving that if `isErasable` $\Sigma \Gamma T \rightarrow \perp$ then `is_eraseableb` returns false. This requires meta-theoretic properties beyond those proved already for the system, as it focuses on proof terms specifically (those whose sort is `tProp`) and essentially quantifies over all possible types for $\Gamma$. In particular, it is necessary to show that if a term is typeable by a type which can have sort `tProp`, then for all other terms that are syntactically smaller or equal to it up to universes and are typeable, they must also have sort `tProp`. This is a generalization of principality that is particularly tricky to prove in presence of cumulative inductive types, as for example `nil@{i} N` and `nil@{j} N` are in this relation but can have unrelated sorts `Type@{i}` and `Type@{j}`. To solve this issue, we devise an alternative, coarser version of the cumulativity relation (in PCUIC: `CumulProp`), named sort quality equivalence, that identifies all `Type@{\_}` sorts, becoming symmetric. Cumulativity is hence a subrelation of sort quality equivalence. We can then prove a theorem that essentially says that two typeable terms that are in the syntactical inequality up to universes relation have sort quality equivalent types. From this, it follows that if one as sort `tProp`, then the other must have it too, establishing a unique sort quality principle.

An excerpt of the definition of the erasure function is depicted in Figure 17. It starts by looking at the result of `is_erasableb`. When the decision procedure says that the term is erasable, it simply returns `\square`. When the term is not erasable, it proceeds by induction on the syntax of the term, coarsely by simply applying the erasure functions on sub-arguments and removing some type information (such as the universe instance $u$ in the `tConst` case). Note the use of `EQUATIONS` to defer the definition of complex arguments such as the proof that a sub-term is well-typed using underscores.
Class abs_envProperty (abs_env_impl abs_env_ext_impl: Type): Prop := {
(* connection to an global environment (similar definition for abs_env_ext_impl) *)
abs_env_∃X : || {Σ & X ~ Σ} ||;
abs_envWF X Σ : X ~ Σ → || WF Σ ||;
abs_env_irk X Σ Σ' : X ~ Σ → X ~ Σ' → Σ = Σ';

(* correctness properties of operations (excerpt) *)
abs_env_add_udecl_correct X Σ udecl H :
(X ~ Σ.1 ∧ Σ.2 = udecl) ↔ abs_env_add_udecl X udecl H ~ext Σ;

(* correctness property of queries *)
abs_env_lookup_correct X Σ kn decl : X ~ext Σ →
(kn, decl) ∈ declarations Σ ↔ abs_env_lookup X kn = Some decl ;

(* correctness properties of decision procedures *)
abs_env_level_mem_correct X Σ 1 : X ~ext Σ →
1 ∈ levels Σ ↔ abs_env_level_mem X 1 ;
abs_env_leqb_level_n_correct X Σ n 1 l' :
X ~ext Σ → l ∈ levels Σ → l' ∈ levels Σ →
( V v : valuation, satisfies v Σ → val v 1 + n ≤ val v l' ) ↔ abs_env_leqb_level_n X n 1 l' ;
abs_env_is_consistent_correct X Σ udecl :
X ~ Σ → For_all (declared_cstrLevels (udecl.1 ∪ levels Σ)) udecl.2 →
( V v, satisfies v Σ → ∃ v', satisfies v' udecl ∧ For_all (fun l ⇒ val v l = val v' l) (levels Σ))
↔ abs_env_is_consistent X udecl ;
abs_env-guard correct X Σ fix_cofix Γ mfix : X ~ext Σ →
guard fix_cofix Σ Γ mfix ↔ abs_env-guard X fix_cofix Γ mfix }.

<caption>Fig. 15. Properties of the abstract global environment (excerpt)</caption>

6.2.3 Reference Implementation. To show that our primitive decision procedures are indeed dealing
with decidable properties, we provide a reference implementation that directly reuses the notion of
well-formed global environment and just implements naïve decision procedures on top of it.

Record reference_impl := {
  reference_impl_env : global_env;
  reference_implWF : || WF reference_impl_env ||}.

The correct implementation of all operations and queries is direct. As for decision procedures, the
only non-direct part are constraints and consistency checking. Indeed, for those, the specification
as the existence of a correct valuation is not obviously decidable.

Fortunately, in § 4.1 we have developed an equivalent description not using the existence of a
valuation but rather acyclicity of a corresponding graph of constraints. Concretely, the equivalence
between the two notions is proven by mediating with the lsp function, computing the length of a
shortest simple path in a graph. Namely, to know that a graph is acyclic, we simply have to check
that lsp V x x is 0 for every node x in the graph. We can express this in Coq as a boolean decision
procedure:

Definition is_acyclic (G : RootedGraph) : 𝒩 :=
for_all (fun x ⇒ match lsp V x x with | Some 0 ⇒ true | _ ⇒ false end) V.
Inductive Σ; Γ ⊢ _ ↝ Ε _ : term → E.term → Prop :=
| erases_tRel : ∀ i : N, Σ; Γ ⊢ tRel i ↝ Ε E.tRel i
| erases_tLambda : ∀ (na : name) (b t : term) (t' : E.term),
Σ; (Γ, na : b) ⊢ t ↝ Ε t' → Σ; Γ ⊢ tLambda na b t ↝ Ε E.tLambda na t'
| erases_tApp : ∀ (f u : term) (f' u' : E.term),
Σ; Γ ⊢ f ↝ Ε f' → Σ; Γ ⊢ u ↝ Ε u' → Σ; Γ ⊢ tApp f u ↝ Ε E.tApp f' u'
| erases_tConst : ∀ (kn : kername) (u : universe_instance),
Σ; Γ ⊢ tConst kn u ↝ Ε E.tConst kn
| erases_tCase : ∀ (ci : case_info) (p : predicate term)
(c : term) (brs : list (branch term)) (c' : E.term) (brs' : list (list name × E.term)),
Subsingleton Σ ci.(ci_ind) →
Σ; Γ ⊢ c ↝ Ε c' →
All2 (fun (x : branch term) (x' : list name × E.term) ⇒
Σ; Γ ++ inst_caseahan context p x ⊢ bbody x ↝ Ε snd x' × Ε (bcontext x) = fst x') brs brs' →
Σ; Γ ⊢ tCase ci p c brs ↝ Ε E.tCase (ci.(ci_ind), ci.(ci_npar)) c' brs'
(* ... *)
| erases_box : ∀ t : term, isErasable Σ Γ t → Σ; Γ ⊢ t ↝ Ε □.

<caption>Fig. 18. Erasure relation (excerpt)</caption>

6.3 Correctness of Erasure

Ideally, we would like to prove that if Σ ⊢ t ⇝ v, then we have Ε Σ ⊢ Ε [] t ⇝ Ε [] v for a suitable extension of Ε to global environments. However, this already fails on simple counter-examples: the Coq term (fun X : Type ⇒ (1, fun x : X ⇒ x)) Type has type N ∗ (Type → Type) and evaluates to the value (1, fun x : Type ⇒ x). Erasing the term yields (fun X ⇒ (1, fun x ⇒ x)) □, with value (1, fun x ⇒ x). Erasing the value however yields (1, □), because fun x : Type ⇒ x is a type former of type Type → Type, which is an arity and thus erased to □. This means intuitively that the erasure function can erase more parts of the term after it has been reduced.

Following Letouzey [2004], we get around this problem by considering a relation Σ; Γ ⊢ t ↝ Ε t', as depicted in Fig. 18, extending the erasure function, which will be closed under weak call-by-value evaluation. For normal terms of first-order inductive types like N or N ∗ N, the relation and the function agree and we can still get the strongest result described above on such first-order types.

Essentially, the relation extends the erasure function by nondeterministic rules allowing not to erase a certain part of a term which could be erased. The only exception here is the **tCase** rule. If the **tCase** matches on a proof of a proposition which is not a **Subsingleton** (i.e., there is more than one branch in the case analysis), the whole case analysis has to be erased. This is necessary because erased discriminatees do not contain any information about which branch to use during evaluation. For subsingleton propositions, there is at most one branch where all arguments are proofs and thus can be erased, they can thus be still evaluated (by picking the one available branch, if any). We can prove global weakening, weakening and substitutivity of the erasure relation.

The erasure relation contains (the graph of) the erasure function:

Lemma erases.erase Γ t (wt : ∀ Σ, X ~ext Σ → welltyped Σ Γ t) :
∀ Σ, X ~ext Σ → Σ; Γ ⊢ t ↝ Ε Ε Γ t wt.

To state the correctness lemma, we need to extend erasure to global environments Σ. We write
Σ ↝ Ε Σ' for this relation. It can be defined in a straightforward way by pointwise extension of
This `is_acyclic` procedure can be directly used to implement `abs_env_is_consistent`.

To implement the decision procedure checking a constraint between levels, we use a rephrasing using labeling on graph.

**Definition leqVertices n x y :=** $V l$, correct_labeling $l \to l \times n \le l y$.

This characterization is not a priori decidable as there is potentially an infinite number of such correct_labeling. However, using lsp again, we can prove that when the graph is acyclic, this property can just be tested on one correct labeling, namely the one induced by lsp.

**Lemma leqVertices_charact n x y {In y V} : leqVertices G n x y $\leftrightarrow$ Some n $\le$ lsp G x y.

Using this, we can characterize the statement "$x+n$ is smaller than $y$" by either $y$ is in the graph of constraints and `lsp G x y` is bigger than $n$, or $y$ is constraint free, and in that case, $n$ must be 0 and $x$ must be at distance 0 from `Set` (which is the source $s G$ of the graph).

**Definition leqbVertices n x y : B :=**

```pascal
if mem y V then le_dec (Some n) (lsp G x y)
else N.eqb n 0 && (eq_dec x y || le_dec (Some 0) (lsp G x (s G)))
```

Because all the (in)equalities involved in the definition are decidable, this gives rise to a boolean decision procedure for constraint checking.

### 6.2.4 More efficient implementations.
Beyond this naïve implementation, we additionally provide a more efficient representation of the environment to perform lookups by using *AVL trees* (a.k.a. self-balancing binary search tree) in the file `PCUIC: WfEnvImpl`. This representation allows additions, removals and lookups in the environment in $O(\log n)$.

But the main venue for optimization is of course the decision procedure for universe consistency. We could for instance use the algorithm proposed by Bender et al. [2015], as recently formalized by Guéneau et al. [2019] (in the particular case where there is no constraint of the form $\le$) to check the acyclicity of the graph. Similarly, we could experiment with the proposal of Bezem and Coquand [2022] using join-semilattices.

Note that the acyclicity checking algorithm is currently a performance bottleneck in Coq too, and our formalization offers the possibility to experiment with more efficient consistency checking and first prove it is correct before deploying it in an official release of Coq.

## 6.3 Conversion and Cumulativity Without Fuel

Being able to decide conversion and cumulativity is essential for defining a type checker and relies on a lot of the meta-theory. The *definition of the conversion algorithm* is optimized to be more efficient than just comparing the normal forms up to cumulativity. It has been designed so that it mimics the conversion algorithm implemented in Coq which consists of

(1) first weak-head reducing the two terms without $\delta$-reductions (i.e., without unfolding definitions);

(2) then comparing their heads, and if they match comparing the subterms recursively;

(3) if they do not match, checking if some computation (pattern-matching or fixpoint) or even the whole term is blocked by a definition that could unfold to a value, unfolding this definition and comparing again.

From this we can already identify a few requirements. First, weak-head reduction has to be defined as an algorithm, which in turn needs normalization (§5.5) to be proven terminating. Furthermore, as normalization can only be assumed for well-typed terms, the conversion algorithm is only defined on well-typed terms. This means that we need to know that the term obtained after reduction is still well typed, which is guaranteed by subject reduction (§5.4). Finally, when reducing a term
the erasure relation. Concretely, we however use an alternative definition which drops unneeded dependencies in $\Sigma'$ (e.g., type definitions), we discuss this in detail in §6.4.

Contrarily to the erasure function, the erasure relation satisfies a general correctness lemma.

**Lemma simple_erases correct:** $\forall \Sigma t' v \Sigma', \mathrm{wf} \Sigma \to \mathrm{welltyped} \Sigma t \to \Sigma \vdash t \downarrow v \to \Sigma; [\vdash t \rightsquigarrow \varepsilon t' \to \Sigma \rightsquigarrow \varepsilon \Sigma'] \to \exists v', \Sigma'; [\vdash v \rightsquigarrow \varepsilon v' \wedge \| \Sigma' \vdash t' \downarrow v' \|].$

Note that this lemma is not proven in our development as we directly prove the more complex optimized one instead (§6.4).

To instantiate the erasure correctness theorem to the erasure function, we introduce the notion of first-order inductive types. An inductive *i* is first-order in a global context $\Sigma$, written *firstorder_ind* $\Sigma i$, if all its parameters, indices, and constructor arguments have a type which is syntactically of the shape *mkApps* (*tInd* *i* *u*) *args* where *i*' is again first-order.

The crucial property is that values of first-order types are just nested constructor applications where neither proofs nor types can occur. Thus, on those terms, the erasure relation and the erasure function coincide, because they both just erase the type information to get an *E.term*.

**Lemma firstorder_erases_deterministic:** $\forall v v' i u \mathrm{args} (\mathrm{wv} : \forall \Sigma, X \sim_{\mathrm{ext}} \Sigma \to \mathrm{welltyped} \Sigma [] v) \Sigma, X \sim_{\mathrm{ext}} \Sigma \to \mathrm{firstorder\_ind} \Sigma i \to \Sigma; [\vdash v : \mathrm{mkApps} (\mathrm{tInd} i u) \mathrm{args} \to \Sigma \vdash v \downarrow v \to \Sigma; [\vdash v \rightsquigarrow \varepsilon v' \to v' = \varepsilon [] v \mathrm{wv}].$

This brings us to the correctness of the erasure function. Because the proof of correctness is based on progress (§4.6), its statement has to be restricted to axiom free global environments.

**Lemma erase_correct_firstorder:** $\forall t v i u \mathrm{args} \Sigma, X \sim_{\mathrm{ext}} \Sigma \to \mathrm{axiom\_free} \Sigma \to \mathrm{firstorder\_ind} \Sigma i \to \Sigma; [\vdash t : \mathrm{mkApps} (\mathrm{tInd} i u) \mathrm{args} \to \Sigma; [\vdash t \rightsquigarrow v \to \neg \{v' & \Sigma; [\vdash v \rightsquigarrow v'\} \to \exists \mathrm{wv}', \|\Sigma \vdash \varepsilon [] t \mathrm{wt} \downarrow \varepsilon [] v \mathrm{wv}'\|].$

That is, if a closed term *t* of first-order inductive type reduces to a value *v*, using the non-deterministic reduction $\rightsquigarrow^*$ defined in §3.2, then the erasure of *t* evaluates to the erasure of that value.

In particular, this observation entails that our type and proof erasure function supports separate compilation: Let $\Sigma; \Gamma \vdash \mathrm{mkApps} \ f \ L : T$, where *T* is a first-order type. Then the value of $\mathrm{mkApps}(\varepsilon f)(\varepsilon L)$ is the erasure of the value of $\mathrm{mkApps} \ f \ L$.

## 6.4 Optimizations

The erasure function defined in Letouzey's PhD thesis [Letouzey 2004] and the definition described by Sozeau et al. [2019b] immediately inline an optimization on case analysis: if the case analysis is on a propositional inductive type, then the case analysis is immediately replaced by the first branch, where an appropriate amount of `□` is inserted for all arguments of the branch. This is necessary for extraction, because `□`, which would witness this erasable inductive value, cannot be extracted to a constructor application as it must obey rule (1) from Page 54, thus a case analysis on it will fail or get stuck in most target languages.

Thus, the evaluation relation on $\lambda_{\square}$ could have been defined without rule (2) as described on Page 54. However, this direct expansion of cases considerably complicates the correctness proof of erasure, as it relies on typing invariants and inversion principles. We decide not to include it into the erasure function, and instead define it as a second pass. This second pass is done by defining
during conversion, we sometimes need to focus on subterms to reduce them to constructors. This is the case for pattern matching but also for fixpoints that only unfold when their recursive argument is a constructor to preserve termination. As the argument is not itself a subterm of the fixpoint, we use the more general notion of position inside the original term to ensure termination. We now describe all these points in more details, leading up to the definition of a decision algorithm for conversion and cumulativity.

### 6.3.1 Term positions.
A position in a term can be seen as a path from the root the desired subterm. As our terms have structure this path is described by a sequence of choices one makes at each node. For instance `app_l` goes left in an application `tApp u v` and points to `u`.

**Inductive choice :=**
| app_l | app_r | case_par (n : N) | case_preturn | case_c | case_brsbody (n : N) | proj_c
| fix_mfixTy (n : N) | fix_mfixbd (n : N) | cofix_mfixTy (n : N) | cofix_mfixbd (n : N) | lamTy
| lamTM | prod_l | prod_r | letbd | letTy | let_in.

**Definition position := list choice.**

Of course, choosing `app_l` when the term is `tLambda` does not make sense. We thus define a boolean predicate `validpos t p` that checks that the position `p` is valid in term `t`. This lets us define the type of valid positions in a term:

**Definition pos (t : term) := { p : position | validpos t p = true } .**

As advertised, the goal of these positions is to help in the termination proof of our reduction machine and our cumulativity checker. We thus define an order on positions as below:

**Inductive positionR : position → position → Prop :=**
| positionR_app_lrpq : positionR (app_r :: p) (app_l :: q)
| positionR_deeCPq : positionR p q → positionR (c :: p) (c :: q)
| positionR_rootcp : positionR (c :: p) [].

The idea is that going deeper inside a term, always yields a smaller position, but crucially going on the right of an application node is smaller than going left. This last point is what lets us inspect and reduce the argument of a fixpoint after inspecting the fixpoint itself.

This order in itself is not well founded, as one could go arbitrarily deep. It becomes well founded when restricted to positions in the same term:

**Definition posR {t} (p q : pos t) : Prop :=** positionR p.π₁ q.π₁.

**Lemma posR_Acc : ∀ t p, Acc (@posR t) p.**

In the reduction and cumulativity algorithms, instead of always carrying around the whole term together with a position, we adopt the equivalent approach of having the term currently under scrutiny, together with its evaluation context: the whole term with a hole. We represent those using *stacks*, defined as follows in a dual manner to positions.
a function `optimize` that is essentially the identity function but for `E.tCase` where it performs the optimization discussed above:

```hkl
optimize Σ (E.tCase ind c brs) := let brs' := map (on_snd (optimize Σ)) brs in
  if isprop_ind Σ ind then
    match brs' with
      | [(a, b)] ⇒ substl (repeat □ #|a|) b
      | _ ⇒ E.tCase ind (optimize c) brs'
    end
  else E.tCase ind (optimize Σ c) brs'
```

The function `isprop_ind` checks whether an inductive definition lives in `Prop`, in which case, when there is only one (optimized) branch, it directly returns that branch where every argument is substituted by `□` (using the function `substl`).

In order to express that rule (2) is not needed anymore after this pass, we parametrize the evaluation relation over a record of flags:

```hkl
Class WcbvFlags := { withProp_case : B ; (* other flags not described in this paper *) }.
```

If `withProp_case = true`, then the rule is enabled, otherwise it is disabled. The correctness theorem for the propositional case expansion pass states that it does not change the evaluation of a term, where `eval` is the weak call-by-value evaluation predicate of `λ_`, for which we use no notation to be able to make the flags explicit.

```hkl
Definition disableProp_cases fl := { withProp_case := false ; (* ... *) }.
```

Lemma `optimize correct Σ tv:wf Σ → closed t →`
`eval fl Σ tv →`
`eval (disableProp_cases fl) (optimize_env Σ) (optimize Σ t) (optimize Σ v).`

Note that technically, we also need to extend `optimize` on environments because we need to optimize the body of definitions. The proof is direct as it just inlines the reduction rule (2).

In the same spirit, we plan on including other passes in the future, e.g., optimization passes removing parameters from inductives. If efficiency becomes a concern, we can always inline these passes again in a new erasure function and prove that it yields the same result as first running the erasure function as defined in this paper and then the propagation pass.

Another source of optimization is in the management of the global context. Indeed, the erasure process as explained here is too inefficient to be executed on realistic examples. The reason is that applying the erasure function pointwise to the global environment will perform retyping and yield numerous constants that are erased to `□` but not used everywhere. This is because dependency on proofs disappear, as all proof are erased but also because in practice a term usually only depends on a small subset of the global environment it is defined in. The full erasure theorem then reads as follows:

Lemma erases_correct Σ t' v Σ' : wf Σ → welltyped Σ t →
Σ ⊢ t ⇓ v → Σ; [] ⊢ t ↣ ε t' → erases_dependencies Σ' t' →
∃ v', Σ; [] ⊢ v ↣ ε v' ∧ || Σ' ⊢ t'▷v' ||.

In order not to produce a large environment polluted by irrelevant constants, we use an inductive predicate `erases_dependencies Σ Σ' t'` stating that the global environment `Σ'` is obtained from applying erasure recursively and selectively to `Σ` by considering only the dependencies of the `erased` term `t'`, in a bottom-up fashion. Note that this is where we need the `abs_pop_decls` primitive that removes a declaration from the global context. This models the `Recursive Extraction <term>` command of
Variant stack_entry : Type :=
| App_l (v : term)
| App_r (u : term)
| Prod_l (na : aname) (B : term)
| Prod_r (na : aname) (A : term)
| Lambda ty (na : aname) (b : term)
| Lambda bd (na : aname) (A : term)
(* ... other cases are similar, reflecting the constructors of choice *)

Definition stack := list stack_entry.

A stack is composed of a list of nodes with a hole. The hole might for instance appear in one of the branches of a pattern matching as expressed by `branches_hole` or inside the motive as described by a `predicate_hole`.

From a stack $\pi$, one can do two things: (i) plug a term $t$ in its hole, written $zip t \pi$; (ii) recover the position associated to its hole: `stack_position \pi`.

### 6.3.2 Weak-Head Normalization Using a Stack Machine.
We are now equipped enough to define weak-head reduction, that is a reduction algorithm which produces a term in weak-head normal form as described in Fig. 13. As we often need to inspect subterms of an expression, the basic input of the algorithm is not just a term but a term under focus as well as its surrounding context, which we called stack in §6.3.1. A reduction step amounts to either reducing the whole expression (term and stack, zipped together with the function `zip`) or focusing on a subterm, and sometimes looking things up on the stack. To prove termination, we use a (dependent) lexicographical order on first coreduction of the whole expression, and then the position order for the positions corresponding to the stacks:

Definition $R_{aux} \Gamma :=$
$dlexprod(cored \ \Sigma \ \Gamma) (@posR)$.

Definition $R \Gamma (u v : term \cdot stack) :=$
$R_{aux} \Gamma (zip u ; stack_pos (fst u) (snd u)) (zip v ; stack_pos (fst v) (snd v))$.

We can then define our algorithm by well-founded induction on $R$. For this, we start by defining a function `_reduce_stack` in open-recursion style (§ 6.1). It takes as argument a term $t$, a stack $\pi$ such that the whole expression is well typed (`welltyped $\Sigma \Gamma$ (zip $(t,\pi)$) `), as well as a function corresponding to recursive calls that can only be applied on pairs that are smaller than $(t,\pi)$ for $R$. It returns a new pair $(t', \pi')$ together with a proof that $(t',\pi')$ is smaller than or equal to $(t, \pi)$ for $R$ so that one can conclude that the resulting whole expression is indeed a reduct of the original one, possibly in zero steps. Additionally, it also provides some technical invariants to ensure that the produced terms are in weak-head normal form.

We can then close the open recursion and obtain a `reduce_term` function that we prove sound, which is expressed by saying that it indeed computes a term that is in the transitive closure of one-step reduction ($\rightsquigarrow$):

Theorem `reduce_term_sound X`:
$\forall \Gamma t (h : \forall \Sigma, X \sim_{ext} \Sigma \rightarrow \text{welltyped } \Sigma \Gamma t) \Sigma, X \sim_{ext} \Sigma \rightarrow \|\Sigma; \Gamma \vdash t \rightsquigarrow * \text{ reduce_term } \Gamma t h \|$.

Note that the theorem is quantified over any abstract environment $X$, and properties mentioning a concrete environment $\Sigma$, such as typing, are stated by quantifying over any concrete environment in relation with $X$. Similarly, we can prove that the reduction is complete, which is expressed by