Verified Metatheory and Realistic Trusted Kernels

Proof. Apply theorem 140.5 to the two displayed derivations. Both conclusions have the same context ${\rho }_{\mathrm{\Sigma }}(\mathrm{\Gamma })$ and the same term ${\rho }_{\mathrm{\Sigma },\mathrm{\Gamma }}(t)$. ◻

Proof. First prove the strip property $$aRb\wedge a{R}^{\ast }c⟹\mathrm{\exists }d.b{R}^{\ast }d\wedge c{R}^{\ast }d$$ by induction on the derivation of $a{R}^{\ast }c$. In the reflexive case, choose $d=b$. In the step case, write $aR{c}_1{R}^{\ast }c$. The diamond for $aRb$ and $aR{c}_1$ supplies $e$ with $bRe$ and $c_{1}Re$. The induction hypothesis, applied to $c_{1}Re$ and $c_1{R}^{\ast }c$, supplies the required $d$.

Now induct on a derivation of $a{R}^{\ast }b$. The reflexive case chooses the endpoint of $a{R}^{\ast }c$. In the step case, write $aR{b}_1{R}^{\ast }b$. The strip property joins $b_1$ to the endpoint of $a{R}^{\ast }c$ at some $d$. Apply the induction hypothesis to $b_1{R}^{\ast }b$ and $b_1{R}^{\ast }d$, then compose the path from $c$ through $d$ with the resulting path. The two composites have the required common endpoint. ◻

Proof. The one-step relation has the diamond property by corollary 140.6. Apply lemma 140.7. ◻

Proof. The conclusion is the type of the second component of the returned pair, so the statement holds because the function type-checks. This is the same move as proposition 134.2 of chapter 134: the obligation has been relocated into the construction of the function, where it is discharged by the proof obligations that the definition leaves open. ◻

Proof. Take $t=(\lambda Z:\mathsf{Type}.(1,\lambda x:Z.x))\mathsf{Type}$, of type $\mathbb{N}\times (\mathsf{Type}\to \mathsf{Type})$. Its value is $v=(1,\lambda x:\mathsf{Type}.x)$. Erasing $t$ gives $(\lambda Z.(1,\lambda x.x))◻$, whose value is $(1,\lambda x.x)$. Erasing $v$ gives $(1,◻)$, because $\lambda x:\mathsf{Type}.x$ is a type former and is therefore erasable. The two values differ. ◻

Proof. For the first clause, induct on the erasure derivation. Variables use the corresponding operation on indices. The lambda case lifts both substitutions under one binder. The let case lifts them under a definition and uses the induction hypotheses for the definiens and body. Application uses the two induction hypotheses. Constants use global weakening. Constructors erase their universe instances and are unchanged by term substitution. Informative case analysis and projection preserve their informative-inductive premise under global extension; apply the induction hypotheses to the scrutinee and, for a case, pointwise to the branches. For a fixed or cofixed block, lift the substitution through the complete mutual fixed-point context and apply the induction hypothesis to every body. The box clause follows because being a type or proof is preserved by weakening and typed substitution. These are all constructors of the erasure relation.

For the second clause, the application statement follows by inversion of typing: an erasable function has a sort or proposition as its result, and adding arguments does not introduce computational data. Lambda inversion is inversion of the same typing classification under its domain binder. For evaluation closure, induct on the evaluation derivation. Beta reduction uses lambda inversion and the substitution clause just proved. Let reduction uses substitution. Constant unfolding uses global weakening and the declaration’s typing derivation. Case and projection use the fact that eliminating a proof or type cannot produce informative data. Fixed- and cofixed-point unfolding use the pointwise hypotheses for the mutual block. Value rules preserve the given classification.

For the third clause, induct on $L$. At $[]$, inversion gives either the relation for $f$ or the box rule, which are the two alternatives with $L_1=[]$. For $L=L_{0}u$, invert the final erasure rule. An application rule exposes related prefixes and arguments; apply the induction hypothesis to the prefix and append the related argument to the appropriate suffix. A box rule makes the whole application erasable and gives the second alternative with $L_1=L$ and empty $L_2$. No constructor, lambda, let, constant, case, projection, fixed-point, or cofixed-point erasure rule can conclude an application judgment. Hence the two alternatives are exhaustive. ◻

Proof. Induct on the derivation $\mathrm{\Sigma };\mathrm{\Gamma }⊢t\Downarrow v$. Strengthen the induction hypothesis over the target environment ${\mathrm{\Sigma }}^{\prime }$, the target term $t^{\prime }$, and the erasure derivation for $t$.

If $t$ is erasable, lemma 140.21(2) makes $v$ erasable. Choose $v^{\prime }=◻$. The target box evaluates to itself, and the box clause relates $v$ to $◻$. This discharges every source rule whose erasure derivation ends in the box clause, including a case over a non-informative proposition.

For a lambda, constructor, fixed-point value, or cofixed-point value whose erasure is not a box, inversion gives the corresponding target constructor and related bodies. Choose that target value; its value rule is the required evaluation and the inverted erasure derivation relates the source value to it.

For a let, write the two source premises as $t_1\Downarrow v_1$ and $t_2[v_1/x]\Downarrow v$. Inversion of the non-box erasure gives $t_1⇝t_1^{\prime }$ and $t_2⇝t_2^{\prime }$. The first induction hypothesis produces $t_1^{\prime }\Downarrow v_1^{\prime }$ and $v_1⇝v_1^{\prime }$. Typed substitution from lemma 140.21(1) gives $t_2[v_1/x]⇝t_2^{\prime }[v_1^{\prime }/x]$. Apply the second induction hypothesis and finish with the target let rule.

For an application spine, use lemma 140.21(3). In its second alternative the target head is $◻$; the amended target application rule evaluates the entire spine to $◻$, and evaluation closure makes the source result erasable. In the first alternative the head and arguments erase pointwise. Invert the source evaluation rule.

Beta.

The head and argument evaluate to $\lambda x.b$ and $u$, respectively, while $b[u/x]\Downarrow v$. The induction hypotheses give a target lambda and a related argument $u^{\prime }$. Lambda inversion gives a related body $b^{\prime }$, and substitution gives $b[u/x]⇝b^{\prime }[u^{\prime }/x]$. Apply the body induction hypothesis, then the target beta rule.

Constant.

The environment-erasure premise supplies a target declaration with a related body. Global weakening transports that relation to the evaluation environment. Apply the induction hypothesis to the unfolded body and rebuild the target constant rule.

Fixed-point unfolding.

Inversion gives pointwise-related mutual bodies. Simultaneous substitution of the fixed-point block into its selected body is covered by lemma 140.21(1). Apply the induction hypothesis to the unfolded body and rebuild the target fixed-point rule. The cofixed-point head case uses the identical schema with the cofixed block and is triggered only by case or projection observation.

For an informative case, the scrutinee induction hypothesis produces the same constructor index in the target. Invert the pointwise branch relation, select the branch with that index, and use simultaneous substitution for its constructor arguments. The branch induction hypothesis gives its target value; the target case rule assembles the result. For a non-informative case, the box case above applies, and the special one-branch target rule supplies the required number of $◻$ arguments. Projection is the one-field version: the scrutinee induction hypothesis produces a target constructor, inversion selects the projected argument, and the target projection rule returns its target value. A cofixed scrutinee is first unfolded by the cofixed-point schema from the application case.

The remaining evaluation rules are congruence instances for the same term constructors. Their erasure derivations expose exactly the premises already covered by the corresponding induction hypotheses, so rebuilding the matching target rule yields $t^{\prime }\Downarrow v^{\prime }$ and the constructor erasure rule yields $v⇝v^{\prime }$. The induction covers every value, beta, let, constant, application-spine, case, projection, fixed-point, and cofixed-point rule of the source evaluation relation, completing the proof. ◻