Dependent Subtyping, Refinement, and Graduality

Proof. By $\mathrm{\Pi }$-Sub and subsumption, $\mathrm{\Gamma }⊢F:{\mathrm{\Pi }}_{x:A_2}{B}_2$. Rule $\mathrm{\Pi }$-E then gives $\mathrm{\Gamma }⊢FN:B_2[N/x]$. The same substitution $[N/x]$ acts on the codomain used in the subtyping premise and on the application result, so the result contains no untransported occurrence of $x$. ◻

Proof. Prove clauses 1–3 simultaneously by induction on derivations. For narrowing, the variable equal to $x$ is retyped by the premise and subsumption; every other variable is unchanged. Under a term or type binder, alpha-rename the binder outside $\mathrm{FV}(A_0)\cup \mathrm{dom}(\mathrm{\Gamma })$ and apply the induction hypothesis to the suffix. Dependent-product subtyping uses the induction hypothesis contravariantly in its domain and under the narrowed client domain in its codomain. Bound selection uses transitivity with the narrowed bound. These are the variable, binder, product, bound, and structural rule families.

For substitution, the variable equal to the substituted variable uses the substituting typing derivation; a different variable is unchanged. Type and term application use both induction hypotheses. Under each dependent binder, choose a name outside the free variables of the substituting expression and apply the induction hypothesis to the renamed body. Kinding and subtyping rebuild their product and bound rules after the same capture-avoiding substitution. Thus substitution preserves all three judgments. A ${\beta }_1$ or ${\beta }_2$ root is then an instance of substitution; congruence cases use the induction hypothesis under the unique reduction context, and conversion cases use transitivity. This proves clause 3.

For clause 4, first ${\beta }_2$-normalize both well-kinded input types. The algorithm compares equal head variables, decomposes dependent products contravariantly in the domain and covariantly in the codomain, and replaces a bounded variable by its declared upper bound only in the designated bound rule. Its recursive measure is the lexicographic pair consisting of the number of unreduced ${\beta }_2$ roots and the sum of the two normal-form sizes; following a declared bound decreases the derivation height of the input’s kinding proof. Hence every recursive call terminates on well-formed inputs.

Soundness is induction on the algorithmic derivation: reflexivity, product, and bound calls rebuild the corresponding declarative rules, while the two normalization phases use clause 3 and conversion. For completeness, induct on a declarative subtyping derivation after eliminating transitivity: commute a transitivity conclusion upward until either its middle type is a head constructor, where the two neighboring rules compose componentwise, or a bounded variable, where the bound rule absorbs it. The measure is the number of transitivity rules below constructor rules, followed by total derivation height. The resulting syntax-directed derivation is exactly an algorithmic one. Formation and kind inference recurse on syntax; minimal typing recurses on the Church annotations; subtyping uses the terminating procedure just proved. Equality of names and the grade-free syntax are decidable, so the four judgments are decidable on well-formed inputs. ◻

Proof. Let $\rho$ be a valuation satisfying $\mathrm{\Phi }(\mathrm{\Gamma })$. Extend $\rho$ by mapping $x$ to the integer denoted by $v$, or by mapping $\mathsf{len}(x)$ to the length denoted by the array value $v$. Variables are interpreted by $\rho$; literals have their displayed integer or length. The second hypothesis gives ${\varphi }_x[v/x]$ under $\rho$, so the extended valuation satisfies $\mathrm{\Phi }(\mathrm{\Gamma }),{\varphi }_x$. The first hypothesis then gives $\psi$. Evaluating $\psi$ in the extension is the same integer calculation as evaluating $\psi [v/x]$ under $\rho$. Since $\rho$ was arbitrary, the required entailment holds. ◻

Proof. For narrowing, induct on the derivation of $J$. Variable typing uses reflexivity when the selected declaration is not $x$ and uses subsumption from $R^{\prime }$ to $R$ when it is $x$. In R-Base-Sub, the assumptions contributed by $R^{\prime }$ imply those contributed by $R$, so composing implications preserves the entailment premise. The binder cases rename their bound variable to a name outside $\mathrm{dom}(\mathrm{\Gamma },\mathrm{\Delta })\cup \{x\}$ and apply the induction hypothesis under the extended context. Formation, application, and subsumption rebuild their displayed rules. These are all rule families.

For substitution, use simultaneous induction on the three derivations. The variable case for $x$ is the given derivation of $v:R$; every other variable case is unchanged. Rule R-Base-Sub uses lemma 106.6 when $R$ is a base refinement. The value grammar and inversion of its typing derivation make $v$ an integer or array variable or literal in that case. When $R$ is a dependent function type, well-sortedness forbids $x$ as a difference-logic vertex, so the entailment is unchanged. In R-Lam and R-$\mathrm{\Pi }$-F, alpha-rename the binder $y$ so that $y\notin \mathrm{fv}(v)\cup \mathrm{dom}(\mathrm{\Gamma },\mathrm{\Delta })\cup \{x\}$, then apply the induction hypothesis to the body. Rule R-App applies the two induction hypotheses and uses $S[u/y][v/x]=S[v/x][u[v/x]/y]$, whose freshness premise is the chosen $y\notin \mathrm{fv}(v)$. Subsumption applies both induction hypotheses and rebuilds R-Sub. Base formation performs literal normalization of difference constraints after substitution. No other rule binds a variable or changes a predicate. ◻

Proof. Outer-form inversion follows because R-Base-Sub and R-$\mathrm{\Pi }$-Sub are the only subtyping rules. Reflexivity is structural induction on the type. At a base type it is reflexivity of semantic implication. At a dependent function, apply the induction hypotheses to the domain and to the codomain under its binder, then apply R-$\mathrm{\Pi }$-Sub.

For transitivity, induct on the middle type. At a base type, implication composition gives the required $\mathrm{Entails}$ premise. For dependent functions, suppose the two derivations have respective codomain premises and domain premises and . The domain induction hypothesis gives . Narrow the first codomain premise from $x:R_2$ to $x:R_3$ using lemma 106.7; the codomain induction hypothesis then gives under $x:R_3$. Rule R-$\mathrm{\Pi }$-Sub completes the derivation. ◻

Proof. For clause 1, use simultaneous induction on synthesis and checking, with the auxiliary claim that $\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e\Leftarrow R$ implies $\mathrm{\Gamma }{⊢}_{\mathsf{DRef}}e:R$. The variable and lambda cases apply R-Var and R-Lam. The exact singleton constraints of A-Int and A-Arr hold after substituting the displayed literal, so R-Int and R-Arr apply. The application case uses the synthesis and checking induction hypotheses before applying R-App. In the auxiliary A-Check case, the synthesis induction hypothesis followed by R-Sub proves the claim.

For clause 2, induct on the declarative typing derivation. Variables synthesize their declarations. In the integer case, any valuation satisfying $\mathrm{\Phi }(\mathrm{\Gamma })$ and $\nu =m$ satisfies the requested predicate because the premise of R-Int proves that predicate after substituting $m$ for $\nu$. Hence $[m{]}_{\mathsf{Int}}$ is a subtype of the requested refinement. The array case uses the same valuation argument with $\mathsf{len}(\nu )=k$. In the lambda case, the induction hypothesis for the body gives ; reflexivity on the annotated domain and R-$\mathrm{\Pi }$-Sub give .

In the application case, let the induction hypothesis for the function give By lemma 106.8, and under $x:R$. If $P_v$ is the synthesized type of $v$, the value induction hypothesis gives ; transitivity gives , so A-Check checks $v$ against $R_0$. Rule A-App synthesizes $S_0[v/x]$. Declarative typing gives $v:R$ by clause 1 and subsumption, so substitution in lemma 106.7 gives Finally, a declarative R-Sub case composes the subtype supplied by the induction hypothesis with its displayed subtype premise. These are all declarative typing rules.

Each synthesis rule is selected by the outer term constructor, and A-App recurses on the proper function subterm. Thus the synthesized type is unique. Clause 3 follows from clauses 1 and 2 together with A-Check. ◻

Proof. For preservation, induct on the reduction derivation. Consider first the root beta step $(\lambda x:R_0.e_0)v⟶e_0[v/x]$ at a declared result type $T$. By theorem 106.9, its unique synthesis derivation ends in A-App and has the form $$\frac{{\displaystyle \frac{x:R_0{⊢}_{\mathsf{DRef}}{e}_0\Rightarrow S_0}{\cdot {⊢}_{\mathsf{DRef}}\lambda x:R_0.e_0\Rightarrow {\mathrm{\Pi }}_{x:R_0}{S}_0}\cdot {⊢}_{\mathsf{DRef}}v\Leftarrow R_0}}{\cdot {⊢}_{\mathsf{DRef}}(\lambda x:R_0.e_0)v\Rightarrow S_0[v/x]},$$ together with . Soundness of synthesis and checking gives $x:R_0{⊢}_{\mathsf{DRef}}{e}_0:S_0$ and $\cdot {⊢}_{\mathsf{DRef}}v:R_0$. Substitution gives $\cdot {⊢}_{\mathsf{DRef}}{e}_0[v/x]:S_0[v/x]$; one use of R-Sub at restores the declared result type. Thus no inversion through a hidden use of R-Sub is required.

For a compatible step $e_0{v}_1⟶e_0^{\prime }{v}_1$, principality gives a synthesized function type ${\mathrm{\Pi }}_{x:R_1}{S}_1$, a check of $v_1$ against $R_1$, and a final relation . The induction hypothesis preserves $e_0:{\mathrm{\Pi }}_{x:R_1}{S}_1$. Rule R-App, followed by the recorded final subtyping relation, types $e_0^{\prime }{v}_1:T$. These are all reduction rules.

For decidability, execute the rules of definition 106.5. Synthesis recurses on a proper term subexpression; checking makes one structural subtyping call. Function subtyping recurses on strict type subexpressions. A base call asks finitely many difference-constraint consequences. For an antecedent graph $G$, a consequence holds when either $G$ has a negative cycle, making the antecedent inconsistent, or $G$ has no negative cycle and its shortest-path bound implies the requested inequality. Bellman–Ford terminates on the finite vertex set; the certificate checker validates the returned cycle in the first case and the returned path bound in the second. Alpha-equivalence and well-formedness are structural decisions. The equivalence in theorem 106.9 transfers this decision from algorithmic checking to declarative typing with R-Sub. ◻

Proof. Let $$\delta =\lambda x:?.\mathsf{cast}[?\to ?\Leftarrow ?](x)x,\mathrm{\Omega }=\delta \mathsf{cast}[?\Leftarrow ?\to ?](\delta ).$$ Put $U=?\to ?$, $u=\mathsf{cast}[?\Leftarrow U](\delta )$, and $C[z]=zu$. Clauses 1 and 2 type $\delta :U$, $u:?$, and $\mathrm{\Omega }=C[\delta ]:?$.

We prove ${\mathsf{Steps}}_{\ge k}(\mathrm{\Omega })$ by induction on $k:\mathsf{Nat}$. The empty sequence proves the case $k=0$. Suppose ${\mathsf{Steps}}_{\ge k}(\mathrm{\Omega })$. Since $\mathrm{\Omega }=C[\delta ]$, clause 3 with $A=U$ and $B=?$ gives $$\begin{array}{}\text{(}1\text{)}& {\mathsf{Steps}}_{\ge k}\left(C[\mathsf{cast}[U\Leftarrow ?](\mathsf{cast}[?\Leftarrow U](\delta ))]\right).\end{array}$$ One beta step gives $$\begin{array}{}\text{(}2\text{)}& \mathrm{\Omega }⟶C[\mathsf{cast}[U\Leftarrow ?](\mathsf{cast}[?\Leftarrow U](\delta ))].\end{array}$$ Prefix the $k$ steps from (1) by (2). This proves ${\mathsf{Steps}}_{\ge k+1}(\mathrm{\Omega })$.

Thus $\mathrm{\Omega }$ has a reduction prefix of every finite length and cannot be strongly normalizing. ◻

Proof. For clause 1, induct simultaneously on elaboration and target typing. Variables and static constructors elaborate homomorphically. A consistency check between $A$ and $B$ inserts $\mathsf{cast}[B\Leftarrow A]$; the cast typing rule has exactly the two formation premises produced by the induction hypotheses. Dependent application substitutes the elaborated argument into both the source and target codomain. Inductive elimination substitutes the constructor indices into its motive. These are the binder, conversion, application, constructor, and eliminator families, so cast insertion preserves typing.

Preservation is induction on a CastCIC${}_G$ root step. A successful cast between equal head constructors recursively casts their parameters and indices, and the constructor typing rule rebuilds the result. A failed head comparison yields ${\mathsf{err}}_B:B$. Beta, iota, and fixpoint roots use substitution; congruence uses the induction hypothesis. For progress, invert a closed typing derivation. A lambda or constructor is a value; an error is an allowed outcome; application, elimination, and cast forms either contain a reducible subterm or match one of the preceding roots. This proves the target part of clause 1.

For clause 2, induct on a static CIC elaboration. No unknown or error rule can be the last rule. Every inserted cast therefore has equal source and target types and erases to the identity. The binder and inductive cases commute with erasure and substitution, so erasing all inserted casts recovers the original term and type.

For clauses 3–4, interpret every type by a pointed omega-cpo of computations and define an admissible precision relation on that domain. At a universe or inductive type, the relation compares equal head constructors componentwise; on the less precise side it also admits the error point and the least element representing divergence. At a dependent product it relates functions that send related arguments to related results. At an inductive family it also requires the constructor indices to be related. Admissibility closes each clause under limits of increasing computation chains, so a diverging approximation cannot be mistaken for a terminating constructor.

The fundamental lemma is a simultaneous induction on the precision and typing derivations, strengthened to related substitutions. Variables use the substitution relation. Constructors and eliminators use the corresponding domain clauses. Dependent binders apply the induction hypothesis after extending both substitutions by related arguments. The cast case uses the constructor-directed reduction from clause 1; incompatible heads land at the error point, while compatible heads reduce to the component relations. Conversion uses invariance of the interpretation under definitional equality. These cases exhaust the static, binder, inductive, conversion, and cast rule families. Specializing the fundamental lemma to closing Boolean contexts gives exactly the observation refinement of clause 3: a Boolean constructor on the precise side is matched by the same constructor, an error, or divergence on the less precise side.

If $A$ is more precise than $B$, the upcast maps each related $A$-value to its $B$ image. The downcast performs the same constructor test in reverse. The type induction shows that downcast after upcast returns the original constructor and recursively satisfies the relation on every field; functions use extensionality at related arguments. Hence the round trip is equiprecise with the identity on $A$, proving clause 4. This observational result does not compare finite reduction lengths, so theorem 106.13 still rules out adding strong normalization under context-wise reduction retraction. ◻

Proof. Both directions are structural inductions on $n$. For the first, at $n=0$ the only vector is $\mathsf{nil}$, ${\mathsf{forget}}_0$ returns the empty list, and ${\mathsf{check}}_0$ accepts it. At $\mathsf{suc}n$ write $v=\mathsf{cons}a{v}^{\prime }$; $\mathsf{forget}$ emits $a$ and recurses, and ${\mathsf{check}}_{\mathsf{suc}n}$ strips $a$ and recurses, so the induction hypothesis applies to $v^{\prime }$ and the head $a$ is returned unchanged. The second direction inducts on the same measure and reads the two recursive equations in the other order. Neither direction makes the pair an equivalence, because ${\mathsf{check}}_n$ is partial; exercise 106.7 asks for both inductions in full. ◻