[proofplan] We prove preservation by induction on the derivation of the one-step [reduction](/page/Reduction) $t \longrightarrow u$. The redex cases are handled directly from the inversion principles for the [typing judgment](/page/Typing%20Judgment): function beta-reduction and sum beta-reduction require a [substitution](/page/Substitution) lemma, while product projection reductions only use the typing rule for pairs. The congruence cases, which express closure under [term contexts](/page/Term%20Context), are handled by applying the induction hypothesis to the reduced subterm and rebuilding the original typing derivation with the same outer typing rule. [/proofplan] [step:Prove substitution preserves typing] [claim:Structural admissibility] Weakening and exchange are admissible for typing contexts. More precisely, if $\Delta \vdash m:M$ and $\Delta'$ is obtained from $\Delta$ by adding fresh variable declarations and permuting declarations while preserving the declared types of all free variables of $m$, then $\Delta' \vdash m:M$. [/claim] [proof] We prove this by induction on the typing derivation of $\Delta \vdash m:M$. In the variable case, the required declaration is still present in $\Delta'$ with the same type. Each term-forming rule is then rebuilt from the induction hypotheses applied to its premises: abstraction extends both contexts by the same bound-variable declaration after alpha-renaming the bound variable fresh for $\Delta'$, application rebuilds the application rule, pairing rebuilds the pairing rule, projections rebuild the corresponding projection rule, injections rebuild the corresponding injection rule, and case analysis rebuilds the case rule after alpha-renaming the branch variables fresh for $\Delta'$. Hence weakening and exchange are admissible. [/proof] [claim:Substitution lemma] Let $\Gamma$ be a context, let $x$ be a variable not already declared in $\Gamma$, and let $B,A$ be types. If $\Gamma,x:B \vdash r:A$ and $\Gamma \vdash a:B$, then $\Gamma \vdash r[a/x]:A$. [/claim] [proof] We prove the claim by induction on the typing derivation of $\Gamma,x:B \vdash r:A$. If the final rule is the variable rule, then $r$ is a variable $z$. There are two cases. If $z=x$, then the typing derivation gives $A=B$, and $r[a/x]=a$, so $\Gamma \vdash r[a/x]:A$ follows from the hypothesis $\Gamma \vdash a:B$. If $z \neq x$, then $z:A$ must occur in $\Gamma$, and $r[a/x]=z$, so the variable rule gives $\Gamma \vdash z:A$. If the final rule is abstraction, then $r=\lambda y:C.\,r_0$ and the derivation has premise \begin{align*} \Gamma,x:B,y:C \vdash r_0:D \end{align*} with $A=C \to D$. Renaming bound variables if necessary, assume $y \neq x$ and $y$ is not free in $a$. By exchange, view the premise as $\Gamma,y:C,x:B \vdash r_0:D$. By weakening applied to $\Gamma \vdash a:B$, we have $\Gamma,y:C \vdash a:B$. The induction hypothesis applied in the context $\Gamma,y:C$ gives \begin{align*} \Gamma,y:C \vdash r_0[a/x]:D. \end{align*} The abstraction typing rule gives \begin{align*} \Gamma \vdash \lambda y:C.\,r_0[a/x] : C \to D. \end{align*} Since $(\lambda y:C.\,r_0)[a/x]=\lambda y:C.\,r_0[a/x]$, this is the desired judgment. If the final rule is application, then $r=r_1\,r_2$ and there is a type $C$ such that \begin{align*} \Gamma,x:B \vdash r_1:C \to A, \qquad \Gamma,x:B \vdash r_2:C. \end{align*} The induction hypothesis gives \begin{align*} \Gamma \vdash r_1[a/x]:C \to A, \qquad \Gamma \vdash r_2[a/x]:C. \end{align*} The application rule gives $\Gamma \vdash r_1[a/x]\,r_2[a/x]:A$, which is exactly $\Gamma \vdash (r_1\,r_2)[a/x]:A$. If the final rule is pairing, then $r=\langle r_1,r_2\rangle$ and $A=C \times D$ for types $C,D$, with premises \begin{align*} \Gamma,x:B \vdash r_1:C, \qquad \Gamma,x:B \vdash r_2:D. \end{align*} Applying the induction hypothesis to both premises and then the pairing rule gives \begin{align*} \Gamma \vdash \langle r_1[a/x],r_2[a/x]\rangle:C \times D. \end{align*} If the final rule is a projection rule, the result follows by applying the induction hypothesis to the premise typing the projected term and then reapplying the same projection rule. If the final rule is an injection rule, the result follows by applying the induction hypothesis to the premise typing the injected term and then reapplying the same injection rule. If the final rule is case analysis, then \begin{align*} r=\operatorname{case}(r_0,y.p,z.q), \end{align*} and there are types $C,D$ such that \begin{align*} \Gamma,x:B \vdash r_0:C+D, \qquad \Gamma,x:B,y:C \vdash p:A, \qquad \Gamma,x:B,z:D \vdash q:A. \end{align*} After renaming bound variables, assume $y,z$ are distinct from $x$ and not free in $a$. By weakening, $\Gamma,y:C \vdash a:B$ and $\Gamma,z:D \vdash a:B$. By exchange, view the branch premises as $\Gamma,y:C,x:B \vdash p:A$ and $\Gamma,z:D,x:B \vdash q:A$. The induction hypothesis gives \begin{align*} \Gamma \vdash r_0[a/x]:C+D, \qquad \Gamma,y:C \vdash p[a/x]:A, \qquad \Gamma,z:D \vdash q[a/x]:A. \end{align*} The case typing rule gives \begin{align*} \Gamma \vdash \operatorname{case}(r_0[a/x],y.p[a/x],z.q[a/x]):A. \end{align*} This term is exactly $r[a/x]$. Hence $\Gamma \vdash r[a/x]:A$. All typing rules have been covered, so the substitution lemma follows. [/proof] [/step] [step:Handle the primitive reduction redexes] We verify preservation for each generating reduction rule. [guided] We first treat the primitive redexes before any surrounding term context is added. The method is the same in each case: assume $\Gamma \vdash t:A$, invert the typing rule that could have produced this judgment, and then derive the same type for the reduct $u$. For function beta-reduction, suppose \begin{align*} t=(\lambda x:B.\,r)\,a \qquad\text{and}\qquad u=r[a/x]. \end{align*} Here $r[a/x]$ denotes capture-avoiding [substitution](/page/Substitution) of $a$ for the free occurrences of $x$ in $r$. If $\Gamma \vdash t:A$, then inversion for the application typing rule gives \begin{align*} \Gamma \vdash \lambda x:B.\,r:B \to A, \qquad \Gamma \vdash a:B. \end{align*} Inversion for the abstraction typing rule then gives \begin{align*} \Gamma,x:B \vdash r:A. \end{align*} The substitution lemma applies with the context $\Gamma$, substituted variable $x$, substituted term $a$, source type $B$, and target type $A$. Its hypotheses are exactly the two judgments just obtained, so \begin{align*} \Gamma \vdash r[a/x]:A. \end{align*} Since $u=r[a/x]$, this proves $\Gamma \vdash u:A$. For the first product projection, suppose \begin{align*} t=\pi_1\langle r,s\rangle \qquad\text{and}\qquad u=r. \end{align*} If $\Gamma \vdash t:A$, then inversion for the first projection typing rule gives a type $C$ such that \begin{align*} \Gamma \vdash \langle r,s\rangle:A \times C. \end{align*} Inversion for the pair typing rule gives \begin{align*} \Gamma \vdash r:A, \qquad \Gamma \vdash s:C. \end{align*} The first of these judgments is exactly $\Gamma \vdash u:A$. For the second product projection, suppose \begin{align*} t=\pi_2\langle r,s\rangle \qquad\text{and}\qquad u=s. \end{align*} If $\Gamma \vdash t:A$, then inversion for the second projection typing rule gives a type $C$ such that \begin{align*} \Gamma \vdash \langle r,s\rangle:C \times A. \end{align*} Inversion for the pair typing rule gives \begin{align*} \Gamma \vdash r:C, \qquad \Gamma \vdash s:A. \end{align*} The second of these judgments is exactly $\Gamma \vdash u:A$. For the left sum reduction, suppose \begin{align*} t=\operatorname{case}(\operatorname{inl}_{B+C}(r),x.p,y.q) \qquad\text{and}\qquad u=p[r/x]. \end{align*} If $\Gamma \vdash t:A$, then inversion for the case typing rule gives \begin{align*} \Gamma \vdash \operatorname{inl}_{B+C}(r):B+C, \qquad \Gamma,x:B \vdash p:A, \qquad \Gamma,y:C \vdash q:A. \end{align*} The annotation $\operatorname{inl}_{B+C}$ fixes the scrutinee sum type as $B+C$, so inversion for the left injection typing rule identifies the injected branch type as $B$ and gives \begin{align*} \Gamma \vdash r:B. \end{align*} The substitution lemma applies to the branch premise $\Gamma,x:B \vdash p:A$ and the argument judgment $\Gamma \vdash r:B$, yielding \begin{align*} \Gamma \vdash p[r/x]:A. \end{align*} Since $u=p[r/x]$, this proves $\Gamma \vdash u:A$. For the right sum reduction, suppose \begin{align*} t=\operatorname{case}(\operatorname{inr}_{B+C}(s),x.p,y.q) \qquad\text{and}\qquad u=q[s/y]. \end{align*} If $\Gamma \vdash t:A$, then inversion for the case typing rule gives \begin{align*} \Gamma \vdash \operatorname{inr}_{B+C}(s):B+C, \qquad \Gamma,x:B \vdash p:A, \qquad \Gamma,y:C \vdash q:A. \end{align*} The annotation $\operatorname{inr}_{B+C}$ fixes the scrutinee sum type as $B+C$, so inversion for the right injection typing rule identifies the injected branch type as $C$ and gives \begin{align*} \Gamma \vdash s:C. \end{align*} The substitution lemma applies to the branch premise $\Gamma,y:C \vdash q:A$ and the argument judgment $\Gamma \vdash s:C$, yielding \begin{align*} \Gamma \vdash q[s/y]:A. \end{align*} Since $u=q[s/y]$, this proves $\Gamma \vdash u:A$. [/guided] For function beta-reduction, suppose \begin{align*} t=(\lambda x:B.\,r)\,a \qquad\text{and}\qquad u=r[a/x]. \end{align*} If $\Gamma \vdash t:A$, then inversion for application gives \begin{align*} \Gamma \vdash \lambda x:B.\,r:B \to A, \qquad \Gamma \vdash a:B. \end{align*} Inversion for abstraction gives \begin{align*} \Gamma,x:B \vdash r:A. \end{align*} By the substitution lemma, $\Gamma \vdash r[a/x]:A$, so $\Gamma \vdash u:A$. For the first product projection, suppose \begin{align*} t=\pi_1\langle r,s\rangle \qquad\text{and}\qquad u=r. \end{align*} If $\Gamma \vdash t:A$, then inversion for the first projection gives a type $C$ such that \begin{align*} \Gamma \vdash \langle r,s\rangle:A \times C. \end{align*} Inversion for pairing gives $\Gamma \vdash r:A$, hence $\Gamma \vdash u:A$. For the second product projection, suppose \begin{align*} t=\pi_2\langle r,s\rangle \qquad\text{and}\qquad u=s. \end{align*} If $\Gamma \vdash t:A$, then inversion for the second projection gives a type $C$ such that \begin{align*} \Gamma \vdash \langle r,s\rangle:C \times A. \end{align*} Inversion for pairing gives $\Gamma \vdash s:A$, hence $\Gamma \vdash u:A$. For the left sum reduction, suppose \begin{align*} t=\operatorname{case}(\operatorname{inl}_{B+C}(r),x.p,y.q) \qquad\text{and}\qquad u=p[r/x]. \end{align*} If $\Gamma \vdash t:A$, then inversion for case analysis gives \begin{align*} \Gamma \vdash \operatorname{inl}_{B+C}(r):B+C, \qquad \Gamma,x:B \vdash p:A, \qquad \Gamma,y:C \vdash q:A. \end{align*} The annotation $\operatorname{inl}_{B+C}$ fixes the scrutinee sum type as $B+C$. Therefore inversion for the left injection gives $\Gamma \vdash r:B$. By the substitution lemma, $\Gamma \vdash p[r/x]:A$, so $\Gamma \vdash u:A$. For the right sum reduction, suppose \begin{align*} t=\operatorname{case}(\operatorname{inr}_{B+C}(s),x.p,y.q) \qquad\text{and}\qquad u=q[s/y]. \end{align*} If $\Gamma \vdash t:A$, then inversion for case analysis gives \begin{align*} \Gamma \vdash \operatorname{inr}_{B+C}(s):B+C, \qquad \Gamma,x:B \vdash p:A, \qquad \Gamma,y:C \vdash q:A. \end{align*} The annotation $\operatorname{inr}_{B+C}$ fixes the scrutinee sum type as $B+C$. Therefore inversion for the right injection gives $\Gamma \vdash s:C$. By the substitution lemma, $\Gamma \vdash q[s/y]:A$, so $\Gamma \vdash u:A$. [/step] [step:Propagate preservation through term-forming contexts] It remains to treat reductions obtained by closing the primitive redex rules under term-forming contexts. We argue by induction on the final congruence rule used to derive $t \longrightarrow u$. If the reduction occurs in the function position of an application, then \begin{align*} t=t_1\,a, \qquad u=u_1\,a, \qquad t_1 \longrightarrow u_1. \end{align*} From $\Gamma \vdash t:A$, inversion for application gives a type $B$ such that \begin{align*} \Gamma \vdash t_1:B \to A, \qquad \Gamma \vdash a:B. \end{align*} The induction hypothesis gives $\Gamma \vdash u_1:B \to A$, and the application rule gives $\Gamma \vdash u_1\,a:A$. If the reduction occurs in the argument position of an application, then \begin{align*} t=f\,t_1, \qquad u=f\,u_1, \qquad t_1 \longrightarrow u_1. \end{align*} Inversion gives a type $B$ with \begin{align*} \Gamma \vdash f:B \to A, \qquad \Gamma \vdash t_1:B. \end{align*} The induction hypothesis gives $\Gamma \vdash u_1:B$, and application gives $\Gamma \vdash f\,u_1:A$. If the reduction occurs under an abstraction, then \begin{align*} t=\lambda x:B.\,r, \qquad u=\lambda x:B.\,r', \qquad r \longrightarrow r'. \end{align*} From $\Gamma \vdash t:A$, inversion for abstraction gives a type $C$ such that $A=B \to C$ and \begin{align*} \Gamma,x:B \vdash r:C. \end{align*} The induction hypothesis applies in the extended context $\Gamma,x:B$ and gives \begin{align*} \Gamma,x:B \vdash r':C. \end{align*} The abstraction typing rule then gives \begin{align*} \Gamma \vdash \lambda x:B.\,r':B \to C. \end{align*} Since $A=B \to C$, this is $\Gamma \vdash u:A$. If the reduction occurs in one component of a pair, one premise of the pairing rule changes and the other premise is unchanged. The induction hypothesis supplies the typing of the reduced component, and the pairing rule rebuilds the typing of the resulting pair. If the reduction occurs inside a projection, inversion gives the typing of the projected term as a product type. The induction hypothesis preserves that product type, and the same projection rule gives the required type for the reduct. If the reduction occurs inside an injection, inversion gives the typing of the injected term. The induction hypothesis preserves that type, and the same injection rule rebuilds the typing of the reduct. If the reduction occurs in the scrutinee of a case expression, write \begin{align*} t=\operatorname{case}(t_0,x.p,y.q), \qquad u=\operatorname{case}(u_0,x.p,y.q), \qquad t_0 \longrightarrow u_0. \end{align*} From $\Gamma \vdash t:A$, inversion for case analysis gives types $B,C$ such that \begin{align*} \Gamma \vdash t_0:B+C, \qquad \Gamma,x:B \vdash p:A, \qquad \Gamma,y:C \vdash q:A. \end{align*} The induction hypothesis gives $\Gamma \vdash u_0:B+C$, and the case typing rule gives $\Gamma \vdash u:A$. If the reduction occurs in one branch of a case expression, inversion gives the typing derivation for that branch under its extended context. Applying the induction hypothesis in that extended context preserves the branch type $A$, and the same case typing rule rebuilds the typing of the whole case expression. Thus every congruence rule preserves the type assigned by the surrounding typing rule. [/step] [step:Conclude preservation for every one-step reduction] The reduction relation $\longrightarrow$ is generated only by the primitive redex rules and by the congruence rules for term constructors, including the abstraction congruence rule. The primitive redex cases preserve typing by the redex analysis above, and every congruence case preserves typing by rebuilding the outer typing rule after applying the induction hypothesis to the reduced subterm in the appropriate context. Therefore, for every context $\Gamma$, terms $t,u$, and type $A$, if $\Gamma \vdash t:A$ and $t \longrightarrow u$, then $\Gamma \vdash u:A$. This is exactly subject reduction for the simply typed lambda calculus with products and sums. [/step]