The Calculus of Inductive Constructions

Definition 89.3 — Raw PCUIC terms¶

The raw terms of the frozen artifact are generated by the following constructors: Here $n$ is a de Bruijn index; names on binders are printing annotations; $\overline{u}$ is a universe instance; $n_p$ is the number of uniform parameters; $\overline{b}$ is a list of branches with arities; and $\overline{d}$ is a mutually recursive block with one selected component $k$. The raw syntax contains $\mathsf{Var}$ and $\mathsf{Evar}$ for quotation and goal-level data, but the typing family below has no rule for either constructor. They are therefore not closed kernel terms.

Definition 89.4 — Contexts and global environments¶

A local declaration is either an assumption $x:A$ or a definition $x:=b:A$. A local context is a snoc-ordered list of such declarations; de Bruijn index zero denotes its last declaration. A global environment $\mathrm{\Sigma }$ is an ordered list whose entries are constants or mutual inductive bodies. A constant body contains a type, an optional body, and a universe declaration. A mutual inductive body contains

1. one shared parameter context and its length $n_p$;

2. one or more inductive bodies, each with an arity, constructor list, primitive-projection list, and allowed elimination sort families;

3. a Finite, CoFinite, or BiFinite tag and one universe declaration. These mean inductive, coinductive, and nonrecursive record, respectively.

A reference may use only an earlier global declaration. We write $\mathrm{\Sigma };\mathrm{\Gamma }⊢t:T$ for the artifact’s typing family.

Definition 89.5 — Frozen well-formedness and typing¶

Write $\mathsf{WF}(\mathrm{\Sigma })$ for the artifact’s well-formed global-environment family and ${\mathsf{WF}}_{\mathrm{\Sigma }}(\mathrm{\Gamma })$ for its local-context family. The empty global environment is well formed. An extension $\mathrm{\Sigma },d$ is well formed exactly when $\mathrm{\Sigma }$ is well formed, the name of $d$ is fresh, the universe declaration of $d$ introduces fresh levels and satisfiable constraints, and $d$ satisfies its declaration condition. A constant body has its declared type; an axiom’s type inhabits a sort. A mutual inductive block has a well-formed parameter context with the recorded number of assumptions, checked arities, constructors and projections, valid universe and elimination data, and a true $\mathsf{ind}\mathsf{\_}\mathsf{guard}$ oracle. Writing $\mathsf{UDeclOK}(\mathrm{\Sigma },U)$ for fresh declared levels, constraints over declared levels, monomorphic-level discipline, and satisfiability, and $\mathsf{DeclOK}(\mathrm{\Sigma },U,d)$ for the preceding constant or inductive condition, the global family has the exact outer rules

For a transparent constant, $\mathsf{DeclOK}$ is the typing judgment for its body at its declared type; for an axiom it is the existence of a sort for the declared type. For a mutual block it is exactly the parameter, body, constructor, projection, universe, elimination, and guard tuple listed above.

The term-typing family is the least family generated by the following named rules. Here $\mathsf{Inst}(u,U)$ checks a universe instance, $d[n]$ lifts by $n$, and ${\mathsf{WfType}}_{\mathrm{\Sigma },\mathrm{\Gamma }}(B)$ means that $B$ is a well-formed arity or has some sort.

Global lookup has three distinct rules. In the constructor conclusion, $\mathsf{ctorType}$ performs universe instantiation and substitutes the mutual families for the block-local de Bruijn references.

For the case rule, define ${\mathsf{CaseOK}}_{\mathrm{\Sigma },\mathrm{\Gamma }}$ to be the exact conjunction Here $\mathsf{allowedFamily}(s,D.\mathsf{kelim})$ is the artifact’s existential Boolean test that compares the sort family against the stored elimination families. Nothing is hidden behind a source-language coverage judgment. The rule is

The paired branch arities must agree exactly, and a branch binds only the nonparameter constructor arguments; PCUIC-Case creates no induction hypotheses.

If $p=(I,n_p,n_a)$ is a declared projection with stored type $T_p$, the projection rule is

Let ${\mathrm{\Delta }}_{\overline{d}}:=\mathsf{fixContext}(\overline{d})$ and let $|{\mathrm{\Delta }}_{\overline{d}}|$ also denote the lift cutoff used below. The two recursive rules are exactly

The historical cofix rule has neither a cofix guard nor a lambda-shape premise. Finally,

There are no rules for $\mathsf{Var}$ or $\mathsf{Evar}$. These declaration and term clauses, rather than the raw grammar alone, are the frozen well-formed syntax.

Definition 89.7 — Universe expressions and consistency¶

A universe level is one of $$\mathsf{Prop},\mathsf{Set},\mathsf{Level}(x),\mathsf{Var}(n).$$ A universe expression is a nonempty maximum of terms $\ell$ and $\ell +1$. A universe constraint is , $\ell \le {\ell }^{\prime }$, or $\ell ={\ell }^{\prime }$. A valuation sends $\mathsf{Prop}$ to $-1$, $\mathsf{Set}$ to $0$, monomorphic named levels to positive integers, and polymorphic variables to natural numbers. A constraint set is consistent when some valuation satisfies every constraint.

The order $U{\le }_{\varphi }V$ holds when every valuation satisfying $\varphi$ gives the integer denotation of $U$ at most that of $V$. Equality of universes is mutual order. This semantic definition is the specification; the checker uses a graph algorithm whose correctness is a separate obligation.

Definition 89.8 — Cumulative conversion¶

Write $\mathrm{\Sigma };\mathrm{\Gamma }⊢t{⇝}_{0}u$ for a root contraction. Its rules are the following named inferences; $\mathsf{apps}$ forms a left-associated application spine.

Define Abbreviate Then constructor case reduction is

The three guarded unfolding rules expose their side conditions.

For the cofix rules, abbreviate $c:=\mathsf{apps}(\mathsf{CoFix}(\overline{d},k),\overline{a})$ and $c^{\prime }:=\mathsf{apps}(f,\overline{a})$.

The compatible one-step relation $t⟶u$ closes these root contractions under every argument position of every raw constructor, using the extended local context under binders. The artifact’s declarative cumulativity is generated by exactly three clauses:

The base comparison ${\mathsf{leq}\mathsf{\_}\mathsf{term}}_{\mathrm{\Sigma }}$ is relative to the global universe constraints. At sorts it includes constraint-relative $\mathsf{eq}\mathsf{\_}\mathsf{universe}$ and universe order; at products it compares domains by conversion and codomains covariantly. Historical PCUIC does not use contravariant domain cumulativity. The artifact’s $\mathsf{Conv}$ relation has the same reduction clauses and uses the equality comparison $\mathsf{eq}\mathsf{\_}\mathsf{term}$ in its base clause. Neither relation is defined as an equivalence closure. Transitivity of $\mathsf{Cumul}$, and symmetry of $\mathsf{Conv}$, are derived theorems using confluence. The $\mathsf{Cumul}$ premise in PCUIC-Cumul is therefore PCUIC term cumulativity, not subtyping from an earlier programming calculus.

Definition 89.10 — Parameters, indices, and constructor uniformity¶

In a mutual block, parameters are the initial telescope copied unchanged into every family and constructor conclusion. indices are the remaining arguments of an inductive family and may vary between constructor conclusions. A block is constructor-uniform when each constructor concludes in a family from the block applied first to exactly the declared parameters in their original order.

The historical artifact records strict positivity through the Boolean oracle $\mathsf{ind}\mathsf{\_}\mathsf{guard}$. A well-formed block requires $\mathsf{ind}\mathsf{\_}\mathsf{guard}(M)=\mathsf{true}$. The polynomial arrow fragment uses the strict-positivity condition of remark 28.36: a recursive family may occur only as the final result of a recursive arity, never to the left of an arrow. The kernel guard also delta-unfolds transparent aliases and admits a nested occurrence only when it appears as a uniform parameter of a previously declared inductive whose stored positivity information permits that occurrence. Thus the simple arrow condition is exact for the declarations printed in this chapter, but is not a complete definition of the kernel’s nested-positivity criterion. The artifact does not prove that its Boolean oracle implements this mathematical account, so the oracle belongs to the trusted theory boundary.

Definition 89.11 — Cases and generated induction schemes¶

For each inductive family $I$ with parameters $\overline{p}$, indices $\overline{i}$, and constructors $c_1,\dots ,c_m$, a case term contains

1. a predicate $P$ over the indices and scrutinee;

2. the scrutinee $c:I\overline{p}\overline{i}$;

3. one branch for each constructor, binding exactly that constructor’s nonparameter arguments.

The declaration stores a list $\mathsf{kelim}(I)$ of target sort families among $\mathsf{Prop}$, $\mathsf{Set}$, and $\mathsf{Type}$. The case rule checks that the sort family of $P$ belongs below one of those stored families. When $I$ lives in $\mathsf{Prop}$, singleton elimination means that well-formedness permits an informative target only when there is at most one constructor and every nonparameter constructor field has sort $\mathsf{Prop}$. A proposition with two constructors fails the first test, just as an existential carrying $x:A$ fails the second. For a predicative inductive, the frozen $\mathsf{check}\mathsf{\_}\mathsf{ind}\mathsf{\_}\mathsf{sorts}$ checks constructor universes and checks index universes only when the configuration flag $\mathsf{indices}\mathsf{\_}\mathsf{matter}$ is true. Every $\mathsf{checker}\mathsf{\_}\mathsf{flags}$ instance shipped with the artifact sets that flag to false. The function does not validate $\mathsf{kelim}$. Thus the vector trace below explicitly records $[\mathsf{Prop},\mathsf{Set},\mathsf{Type}]$ as declaration data; this list is not derived as a well-formedness invariant for every Type-valued inductive.

The kernel case rule is nonrecursive. A generated induction scheme is a separate constant whose body is a guarded fixpoint containing such a case. Its recursive branch invokes the fixpoint on each recursive constructor argument and passes those results to the branch method. Thus induction hypotheses belong to the type and fixpoint body of the generated scheme; they are not additional arguments passed by $\iota$-reduction of $\mathsf{Case}$.

Definition 89.13 — Historical recursive guards¶

A mutual fixpoint body records a name, type, body, and the position of its principal recursive argument. The historical PCUIC typing rule requires the Boolean oracle $\mathsf{fix}\mathsf{\_}\mathsf{guard}(\overline{d})=\mathsf{true}$ and selects one well-typed component. Root reduction unfolds that component only when its principal argument is constructor-headed. The artifact assumes that the guard is stable under reduction, universe equality, renaming, lifting, and substitution.

A cofixpoint uses the same mutual-body representation and unfolds only when the surrounding term is a case or primitive projection. In the frozen artifact, however, PCUIC-CoFix requires only that the configuration flag $\mathsf{allow}\mathsf{\_}\mathsf{cofix}$ is enabled, the selected component exists, the mutual context is well formed, and every body has its declared lifted type. It has no cofix guard premise. This asymmetry with PCUIC-Fix is an exact historical boundary, not an omitted source-language check. Tactics that synthesize decreasing evidence or elaborate an equation compiler are not kernel rules.