Coercive Subtyping and Coherent Cast Insertion

Proof. Prove clauses 1 and 2 simultaneously by induction on the derivation of $p\in {\mathsf{Coe}}_{\mathrm{\Delta }}(A,B)$. For Coe-Id, target lambda introduction gives the required function, and substitution produces ${\mathsf{id}}_{A[\sigma ]}$. For a declared Coe-Edge instance $r[\tau ]$, where $r=(\mathrm{\Xi };A_0,B_0,c)$, the schema typing judgment substituted along $\tau :\mathrm{\Delta }\Rightarrow \mathrm{\Xi }$ gives $\mathrm{\Delta }⊢c[\tau ]:A_0[\tau ]\to B_0[\tau ]$. Substitution along $\sigma$ produces the declared instance $r[\tau \circ \sigma ]$, and the substitution-composition law identifies its cast with $c[\tau ][\sigma ]$.

For Coe-Comp, the two typing induction hypotheses and target application and lambda introduction type the composite cast. The two substitution induction hypotheses, followed by lambda and application congruence, identify $(q\circ p)[\sigma ]$ with $q[\sigma ]\circ p[\sigma ]$. In the Coe-Conv case, substitution stability of judgmental equality converts the substituted source and target endpoints; the cast term is unchanged. These are all four generators.

Clause 3 is clause 2 at the projection substitution. For clause 4, pointwise context conversion makes the identity variable list well typed; apply clause 2 to that substitution. No free variable is introduced or discarded without one of these substitutions. ◻

Proof. Simultaneous rule induction on the two derivations. Coe-Var is the target variable rule and Coe-Ann is its premise unchanged. For Coe-App the two induction hypotheses give $\mathrm{\Gamma }⊢t_1:\prod _{x:A}B$ and $\mathrm{\Gamma }⊢t_2:A$, and target application derives $\mathrm{\Gamma }⊢t_1{t}_2:B[t_2/x]$. For Coe-Pair the two induction hypotheses and product introduction derive $\mathrm{\Gamma }⊢(t_1,t_2):A\times B$. For Coe-Lam the induction hypothesis in the extended context and $\mathrm{\Pi }$-introduction derive $\mathrm{\Gamma }⊢\lambda x.t:\prod _{x:A}B$. For Coe-Insert the induction hypothesis gives $\mathrm{\Gamma }⊢t:A$, while clause 1 of lemma 119.3 gives $\mathrm{\Gamma }⊢{\mathsf{prog}}_p:A\to B$; target application derives $\mathrm{\Gamma }⊢{\mathsf{prog}}_{p}t:B$. These are all six rules. ◻

Proof. The strengthened context and expected-type clauses are the induction invariant needed under lambdas and when two applications synthesize judgmentally equal, but not syntactically identical, domains. Proceed by simultaneous induction on the two pairs of derivations. In the calculations below, judgments from ${\mathrm{\Gamma }}_2$ are compared in ${\mathrm{\Gamma }}_1$ by the ordinary target context-conversion rule. A coercion path from ${\mathrm{\Gamma }}_2$ is transported along the identity variable substitution supplied by clause 4 of lemma 119.3; therefore its cast program is compared in ${\mathrm{\Gamma }}_1$, not in an unmentioned ambient context. In each synthesis case the source term’s outermost constructor selects the rule, so both derivations end in the same rule of definition 119.6.

Coe-Var: both derivations read corresponding declarations for the same variable. Pointwise context equality gives ${\mathrm{\Gamma }}_1⊢A_1\equiv A_2\mathsf{type}$, and $t_1=t_2=x$.

Coe-Ann: both conclude at the written annotation, so $A_1=A_2$, and the strengthened clause 2 for the premises, with reflexivity of the written type, gives ${\mathrm{\Gamma }}_1⊢t_1\equiv t_2:A_1$.

Coe-Pair: clause 1 for the two component premises gives ${\mathrm{\Gamma }}_1⊢A_1^{\prime }\equiv A_2^{\prime }\mathsf{type}$, ${\mathrm{\Gamma }}_1⊢B_1^{\prime }\equiv B_2^{\prime }\mathsf{type}$ and componentwise equality of the elaborated components. Product congruence gives ${\mathrm{\Gamma }}_1⊢A_1^{\prime }\times B_1^{\prime }\equiv A_2^{\prime }\times B_2^{\prime }\mathsf{type}$ and pair congruence closes the terms.

Coe-App: clause 1 for the function premise gives ${\mathrm{\Gamma }}_1⊢\prod _{x:A^1}{B}^1\equiv \prod _{x:A^2}{B}^2\mathsf{type}$ and ${\mathrm{\Gamma }}_1⊢t_1^{\mathrm{f}}\equiv t_2^{\mathrm{f}}:\prod _{x:A^1}{B}^1$. Injectivity of $\mathrm{\Pi }$ gives ${\mathrm{\Gamma }}_1⊢A^1\equiv A^2\mathsf{type}$ and ${\mathrm{\Gamma }}_1,x:A^1⊢B^1\equiv B^2\mathsf{type}$, so the two argument premises check at judgmentally equal types and the strengthened clause 2 gives ${\mathrm{\Gamma }}_1⊢t_1^{\mathrm{a}}\equiv t_2^{\mathrm{a}}:A^1$. Stability of equality under substitution gives ${\mathrm{\Gamma }}_1⊢B^1[t_1^{\mathrm{a}}/x]\equiv B^2[t_2^{\mathrm{a}}/x]\mathsf{type}$, and application congruence closes the terms.

For clause 2 there is exactly one checking rule per source constructor. If the source is $\lambda x.e$, both derivations use Coe-Lam, so ${\mathrm{\Gamma }}_i⊢B_i\equiv \prod _{x:A_i}{C}_i\mathsf{type}$ for $i\in \{1,2\}$. Dependent-$\mathrm{\Pi }$ injectivity applied to the assumed ${\mathrm{\Gamma }}_1⊢B_1\equiv B_2\mathsf{type}$ gives ${\mathrm{\Gamma }}_1⊢A_1\equiv A_2\mathsf{type}$ and, after context conversion, ${\mathrm{\Gamma }}_1,x:A_1⊢C_1\equiv C_2\mathsf{type}$. The body contexts ${\mathrm{\Gamma }}_1,x:A_1$ and ${\mathrm{\Gamma }}_2,x:A_2$ are pointwise judgmentally equal, so the strengthened induction hypothesis applies directly to the body derivations. Lambda congruence gives equality at $B_1$.

Every other source term uses Coe-Insert. The two derivations synthesize $A_1$ and $A_2$ with paths $p\in {\mathsf{Coe}}_{{\mathrm{\Gamma }}_1}(A_1,B_1)$ and $q\in {\mathsf{Coe}}_{{\mathrm{\Gamma }}_2}(A_2,B_2)$. Transport clause 4 of lemma 119.3 gives a path $q^{\iota }\in {\mathsf{Coe}}_{{\mathrm{\Gamma }}_1}(A_2[\iota ],B_2[\iota ])$, whose cast is the context conversion of ${\mathsf{prog}}_q$. Clause 1 gives ${\mathrm{\Gamma }}_1⊢A_1\equiv A_2\mathsf{type}$ and ${\mathrm{\Gamma }}_1⊢u_1\equiv u_2:A_1$; the expected-type premise gives ${\mathrm{\Gamma }}_1⊢B_1\equiv B_2\mathsf{type}$, where the right-hand endpoints abbreviate their substitutions along $\iota$. Hence $p$ and $q^{\iota }$ are parallel in the exact sense of definition 119.2. Path coherence gives ${\mathrm{\Gamma }}_1⊢{\mathsf{prog}}_p\equiv {\mathsf{prog}}_{q^{\iota }}:A_1\to B_1$ after endpoint conversion. Application congruence and conversion of the second result from $B_2$ to $B_1$ give ${\mathrm{\Gamma }}_1⊢{\mathsf{prog}}_p{u}_1\equiv {\mathsf{prog}}_{q^{\iota }}{u}_2:B_1$. The cast-program equality in clause 4 of lemma 119.3 identifies the last term with the context conversion of ${\mathsf{prog}}_q{u}_2$, which is the required conclusion. ◻

Proof. This is clause 2 of lemma 119.8 with $B_1=B_2=A$ and reflexivity of target conversion. ◻

Proof. Fix $f:\prod _{y:A_1}{B}_1(y)$ and $x:A_2$. Function congruence gives $\mathrm{\Gamma },x:A_2⊢f({\mathsf{prog}}_{p}x)\equiv f({\mathsf{prog}}_{p^{\prime }}x):B_1({\mathsf{prog}}_{p}x)$. After the stipulated fiber conversion, congruence with the equal fiber casts gives equality of the two bodies at $B_2(x)$. Lambda congruence first closes over $x$, then over $f$, yielding equality of the casts. ◻

Proof. We reconstruct the two inductions. For a derivation $d$, write $\mathrm{pre}(d)$ for the derivations of all presuppositions of its conclusion: context validity; kind formation for a displayed kind; typing of both sides of an equality; and, for , the typings of $A$, $B$, and $c:A\to B$. Structural induction on $d$ proves the following extraction invariant:

If $\mathrm{\Theta }(d)$ is defined, then $\mathrm{\Theta }$ is defined on every member of $\mathrm{pre}(d)$, and the image extracted from $d$ is $T$-equal to the image obtained from the separately extracted presupposition.

For a variable or primitive formation rule the extracted derivation is the corresponding premise or an identity derivation. Weakening and context replacement use equality of the prefix contexts. For product formation, abstraction, application, and substitution, apply the induction hypotheses to the domain and codomain presuppositions and rebuild the same logical-framework rule after context replacement. Equality formation uses the two endpoint extractions; equality typing uses those plus the type extraction. A basic subtyping rule uses coherence clause 1 to obtain the three required typings. Coercive application extracts the function typing, argument typing, coercion typing, and the equalities that align their independently reconstructed contexts and kinds; after those replacements, ordinary application derives $f(c(k))$. Coercive definition has the same four obligations under its binder. These are all rule families of $T[R]$, so the extraction invariant holds.

We next prove, by induction on the sum of the heights of $d$ and $d^{\prime }$, that whenever they derive the same validity, kind-formation, or term-typing judgment and both images are defined, their images are $T$-equal. If the last rules agree, apply the induction hypothesis to corresponding premises and congruence to the rebuilt conclusion. The possible unequal last rules are structural rules, equality conversion, and coercive versus ordinary application or two coercive applications. Structural and conversion cases are reduced to smaller derivations by the extraction invariant and transitivity of $T$-equality. An ordinary application compared with a coercive one would give, after the smaller comparisons, both equality and a proper subtyping judgment between the same endpoint kinds; coherence clauses 1 and 2 exclude that case. If both are coercive applications, the smaller comparisons identify their source and target kinds. Coherence clause 3 identifies their coercions, and application congruence identifies the completed conclusions. The coercive-definition comparison uses that argument under lambda congruence. Thus all three classes of presupposed judgment have derivation-independent images.

Totality of $\mathrm{\Theta }$ now follows by structural induction on $d$. Images of the premises exist by induction. To rebuild the last rule, the extraction invariant reduces each missing context or kind equality to a comparison of two presupposed judgments; the preceding derivation-independence lemma supplies that equality. The coercive-application and coercive-definition cases use the same comparison and coherence clause 3 for their coercion. Hence every reconstruction obligation is discharged. A derivation already in $T[R{]}_{0K}$ contains no coercive application or definition to replace, and the deterministic context-alignment convention inserts no change at its conclusion; therefore its final judgment is unchanged.

For conservativity, let $d$ derive a non-subtyping, non-subkinding judgment $J$ in $T[R]$. If $J$ has an unchanged completion, then $\mathrm{\Theta }(d)$ is literally a $T$-derivation of $J$. Conversely, a $T$-derivation contains no coercive rule and is fixed by $\mathrm{\Theta }$. For a subtyping or subkinding conclusion the identical argument lands in $T[R{]}_0$ or $T[R{]}_{0K}$, respectively. Derivation independence shows that the existence of one unchanged derivation is equivalent to every derivation being unchanged. This proves both assertions.

The proof uses the complete source rule classification and its three coherence clauses. It proves no path coherence for a different target calculus, licenses no insertion outside definition 119.6, and supplies no generic map law. ◻