StlcProp.html

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>StlcProp: Properties of STLC</title>
<script type="text/javascript" src="jquery-1.8.3.js"></script>
<script type="text/javascript" src="main.js"></script>
</head>

<body>

<div id="page">

<div id="header">
</div>

<div id="main">

<h1 class="libtitle">StlcProp<span class="subtitle">Properties of STLC</span></h1>

<div class="code code-tight">
</div>

<div class="doc">

</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Stlc</span>.<br/>

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">STLCProp</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">STLC</span>.<br/>

<br/>
</div>

<div class="doc">
In this chapter, we develop the fundamental theory of the Simply
    Typed Lambda Calculus &mdash; in particular, the type safety
    theorem. 
</div>
<div class="code code-tight">

<br/>
</div>

<div class="doc">
<a name="lab680"></a><h1 class="section">Canonical Forms</h1>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">canonical_forms_bool</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">TBool</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;(<span class="id" type="var">t</span> = <span class="id" type="var">ttrue</span>) <span style="font-family: arial;">&or;</span> (<span class="id" type="var">t</span> = <span class="id" type="var">tfalse</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">HT</span> <span class="id" type="var">HVal</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HVal</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">inversion</span> <span class="id" type="var">HT</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">canonical_forms_fun</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; (<span class="id" type="var">TArrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;<span style="font-family: arial;">&exist;</span><span class="id" type="var">x</span> <span class="id" type="var">u</span>, <span class="id" type="var">t</span> = <span class="id" type="var">tabs</span> <span class="id" type="var">x</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">u</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">HT</span> <span class="id" type="var">HVal</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HVal</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">inversion</span> <span class="id" type="var">HT</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span style="font-family: arial;">&exist;</span><span class="id" type="var">x0</span>. <span style="font-family: arial;">&exist;</span><span class="id" type="var">t0</span>. <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>

<br/>
</div>

<div class="doc">
<a name="lab681"></a><h1 class="section">Progress</h1>

<div class="paragraph"> </div>

 As before, the <i>progress</i> theorem tells us that closed, well-typed
    terms are not stuck: either a well-typed term is a value, or it
    can take an evaluation step.  The proof is a relatively
    straightforward extension of the progress proof we saw in the
    <span class="inlinecode"><span class="id" type="keyword">Types</span></span> chapter. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">progress</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> <span style="font-family: arial;">&or;</span> <span style="font-family: arial;">&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span style="font-family: arial;">&rArr;</span> <span class="id" type="var">t'</span>.<br/>

<br/>
</div>

<div class="doc">
<i>Proof</i>: by induction on the derivation of <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> The last rule of the derivation cannot be <span class="inlinecode"><span class="id" type="var">T_Var</span></span>, since a
      variable is never well typed in an empty context.

<div class="paragraph"> </div>


</li>
<li> The <span class="inlinecode"><span class="id" type="var">T_True</span></span>, <span class="inlinecode"><span class="id" type="var">T_False</span></span>, and <span class="inlinecode"><span class="id" type="var">T_Abs</span></span> cases are trivial, since in
      each of these cases we know immediately that <span class="inlinecode"><span class="id" type="var">t</span></span> is a value.

<div class="paragraph"> </div>


</li>
<li> If the last rule of the derivation was <span class="inlinecode"><span class="id" type="var">T_App</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
      <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, and we know that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> are also well typed in the
      empty context; in particular, there exists a type <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> such that
      <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&rarr;</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>.  By the induction
      hypothesis, either <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value or it can take an evaluation
      step.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value, we now consider <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, which by the other
          induction hypothesis must also either be a value or take an
          evaluation step.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> is a value.  Since <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value with an
              arrow type, it must be a lambda abstraction; hence <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
              <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> can take a step by <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> can take a step, and hence so can <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
              <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" type="var">ST_App2</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> can take a step, then so can <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" type="var">ST_App1</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If the last rule of the derivation was <span class="inlinecode"><span class="id" type="var">T_If</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="keyword">if</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
      <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>, where <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> has type <span class="inlinecode"><span class="id" type="var">Bool</span></span>.  By the IH, <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
      either is a value or takes a step.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value, then since it has type <span class="inlinecode"><span class="id" type="var">Bool</span></span> it must be
          either <span class="inlinecode"><span class="id" type="var">true</span></span> or <span class="inlinecode"><span class="id" type="var">false</span></span>.  If it is <span class="inlinecode"><span class="id" type="var">true</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> steps
          to <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>; otherwise it steps to <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> takes a step, and therefore so does <span class="inlinecode"><span class="id" type="var">t</span></span> (by
          <span class="inlinecode"><span class="id" type="var">ST_If</span></span>).

</li>
</ul>

</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">subst</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>...<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_Var".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;contradictory:&nbsp;variables&nbsp;cannot&nbsp;be&nbsp;typed&nbsp;in&nbsp;an&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;empty&nbsp;context&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_App".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="var">t</span></span>&nbsp;=&nbsp;<span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>.&nbsp;&nbsp;Proceed&nbsp;by&nbsp;cases&nbsp;on&nbsp;whether&nbsp;<span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>&nbsp;is&nbsp;a&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;value&nbsp;or&nbsp;steps...&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "t<sub>1</sub> is a value".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt2</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SSCase</span> "t<sub>2</sub> is also a value".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span style="font-family: arial;">&exist;</span><span class="id" type="var">x0</span> <span class="id" type="var">t0</span>, <span class="id" type="var">t<sub>1</sub></span> = <span class="id" type="var">tabs</span> <span class="id" type="var">x0</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t0</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">canonical_forms_fun</span>; <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H1</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">x0</span> [<span class="id" type="var">t0</span> <span class="id" type="var">Heq</span>]]. <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style="font-family: arial;">&exist;</span>([<span class="id" type="var">x0</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t0</span>)...<br/>

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SSCase</span> "t<sub>2</sub> steps".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H0</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>2</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style="font-family: arial;">&exist;</span>(<span class="id" type="var">tapp</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub>'</span>)...<br/>

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "t<sub>1</sub> steps".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style="font-family: arial;">&exist;</span>(<span class="id" type="var">tapp</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>)...<br/>

<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_If".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>...<br/>

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "t<sub>1</sub> is a value".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">canonical_forms_bool</span> <span class="id" type="var">t<sub>1</sub></span>); <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">eauto</span>.<br/>

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "t<sub>1</sub> also steps".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style="font-family: arial;">&exist;</span>(<span class="id" type="var">tif</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
</div>

<div class="doc">
<a name="lab682"></a><h4 class="section">Exercise: 3 stars, optional (progress_from_term_ind)</h4>
 Show that progress can also be proved by induction on terms
    instead of induction on typing derivations. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">progress'</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> <span style="font-family: arial;">&or;</span> <span style="font-family: arial;">&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span style="font-family: arial;">&rArr;</span> <span class="id" type="var">t'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">t_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">t</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">Ht</span>; <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
</div>
<div class="code code-tight">

<br/>
</div>

<div class="doc">
<a name="lab683"></a><h1 class="section">Preservation</h1>

<div class="paragraph"> </div>

 The other half of the type soundness property is the preservation
    of types during reduction.  For this, we need to develop some
    technical machinery for reasoning about variables and
    substitution.  Working from top to bottom (the high-level property
    we are actually interested in to the lowest-level technical lemmas
    that are needed by various cases of the more interesting proofs),
    the story goes like this:

<div class="paragraph"> </div>

<ul class="doclist">
<li> The <i>preservation theorem</i> is proved by induction on a typing
        derivation, pretty much as we did in the <span class="inlinecode"><span class="id" type="keyword">Types</span></span> chapter.  The
        one case that is significantly different is the one for the
        <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span> rule, which is defined using the substitution
        operation.  To see that this step preserves typing, we need to
        know that the substitution itself does.  So we prove a...

<div class="paragraph"> </div>


</li>
<li> <i>substitution lemma</i>, stating that substituting a (closed)
        term <span class="inlinecode"><span class="id" type="var">s</span></span> for a variable <span class="inlinecode"><span class="id" type="var">x</span></span> in a term <span class="inlinecode"><span class="id" type="var">t</span></span> preserves the type
        of <span class="inlinecode"><span class="id" type="var">t</span></span>.  The proof goes by induction on the form of <span class="inlinecode"><span class="id" type="var">t</span></span> and
        requires looking at all the different cases in the definition
        of substitition.  This time, the tricky cases are the ones for
        variables and for function abstractions.  In both cases, we
        discover that we need to take a term <span class="inlinecode"><span class="id" type="var">s</span></span> that has been shown
        to be well-typed in some context <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> and consider the same
        term <span class="inlinecode"><span class="id" type="var">s</span></span> in a slightly different context <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>.  For this
        we prove a...

<div class="paragraph"> </div>


</li>
<li> <i>context invariance</i> lemma, showing that typing is preserved
        under "inessential changes" to the context <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> &mdash; in
        particular, changes that do not affect any of the free
        variables of the term.  For this, we need a careful definition
        of

<div class="paragraph"> </div>


</li>
<li> the <i>free variables</i> of a term &mdash; i.e., the variables occuring
        in the term that are not in the scope of a function
        abstraction that binds them.

</li>
</ul>

</div>
<div class="code code-tight">

<br/>
</div>

<div class="doc">
<a name="lab684"></a><h2 class="section">Free Occurrences</h2>

<div class="paragraph"> </div>

 A variable <span class="inlinecode"><span class="id" type="var">x</span></span> <i>appears free in</i> a term <i>t</i> if <span class="inlinecode"><span class="id" type="var">t</span></span> contains some
    occurrence of <span class="inlinecode"><span class="id" type="var">x</span></span> that is not under an abstraction labeled <span class="inlinecode"><span class="id" type="var">x</span></span>.  For example: 

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">y</span></span> appears free, but <span class="inlinecode"><span class="id" type="var">x</span></span> does not, in <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">T</span><span style="font-family: arial;">&rarr;</span><span class="id" type="var">U</span>.</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> 

</li>
<li> both <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span> appear free in <span class="inlinecode">(\<span class="id" type="var">x</span>:<span class="id" type="var">T</span><span style="font-family: arial;">&rarr;</span><span class="id" type="var">U</span>.</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span>)</span> <span class="inlinecode"><span class="id" type="var">x</span></span> 

</li>
<li> no variables appear free in <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">T</span><span style="font-family: arial;">&rarr;</span><span class="id" type="var">U</span>.</span> <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T</span>.</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span>  
</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">appears_free_in</span> : <span class="id" type="var">id</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_var</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tvar</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_app1</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tapp</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_app2</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>2</sub></span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tapp</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_abs</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">y</span> ≠ <span class="id" type="var">x</span>  <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>12</sub></span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tabs</span> <span class="id" type="var">y</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_if1</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tif</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_if2</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>2</sub></span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tif</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_if3</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>3</sub></span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">tif</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">

<br/>
<span class="id" type="keyword">Tactic Notation</span> "afi_cases" <span class="id" type="var">tactic</span>(<span class="id" type="var">first</span>) <span class="id" type="var">ident</span>(<span class="id" type="var">c</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="var">first</span>;<br/>
&nbsp;&nbsp;[ <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_var"<br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_app1" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_app2" <br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_abs" <br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_if1" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_if2" <br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "afi_if3" ].<br/>

<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">appears_free_in</span>.<br/>
</div>

<br/>
</div>

<div class="doc">
A term in which no variables appear free is said to be <i>closed</i>. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">closed</span> (<span class="id" type="var">t</span>:<span class="id" type="var">tm</span>) :=<br/>
&nbsp;&nbsp;<span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span>, ¬ <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span>.<br/>

<br/>
</div>

<div class="doc">
<a name="lab685"></a><h2 class="section">Substitution</h2>

<div class="paragraph"> </div>

 We first need a technical lemma connecting free variables and
    typing contexts.  If a variable <span class="inlinecode"><span class="id" type="var">x</span></span> appears free in a term <span class="inlinecode"><span class="id" type="var">t</span></span>,
    and if we know <span class="inlinecode"><span class="id" type="var">t</span></span> is well typed in context <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, then it must
    be the case that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> assigns a type to <span class="inlinecode"><span class="id" type="var">x</span></span>. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">free_in_context</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;<span style="font-family: serif; font-size:85%;">&Gamma;</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;<span style="font-family: arial;">&exist;</span><span class="id" type="var">T'</span>, <span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">T'</span>.<br/>

<br/>
</div>

<div class="doc">
<i>Proof</i>: We show, by induction on the proof that <span class="inlinecode"><span class="id" type="var">x</span></span> appears free
      in <span class="inlinecode"><span class="id" type="var">t</span></span>, that, for all contexts <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, if <span class="inlinecode"><span class="id" type="var">t</span></span> is well typed
      under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, then <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> assigns some type to <span class="inlinecode"><span class="id" type="var">x</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule used was <span class="inlinecode"><span class="id" type="var">afi_var</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>, and from
        the assumption that <span class="inlinecode"><span class="id" type="var">t</span></span> is well typed under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> we have
        immediately that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> assigns a type to <span class="inlinecode"><span class="id" type="var">x</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the last rule used was <span class="inlinecode"><span class="id" type="var">afi_app1</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">x</span></span>
        appears free in <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>.  Since <span class="inlinecode"><span class="id" type="var">t</span></span> is well typed under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>,
        we can see from the typing rules that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> must also be, and
        the IH then tells us that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> assigns <span class="inlinecode"><span class="id" type="var">x</span></span> a type.

<div class="paragraph"> </div>


</li>
<li> Almost all the other cases are similar: <span class="inlinecode"><span class="id" type="var">x</span></span> appears free in a
        subterm of <span class="inlinecode"><span class="id" type="var">t</span></span>, and since <span class="inlinecode"><span class="id" type="var">t</span></span> is well typed under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, we
        know the subterm of <span class="inlinecode"><span class="id" type="var">t</span></span> in which <span class="inlinecode"><span class="id" type="var">x</span></span> appears is well typed
        under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> as well, and the IH gives us exactly the
        conclusion we want.

<div class="paragraph"> </div>


</li>
<li> The only remaining case is <span class="inlinecode"><span class="id" type="var">afi_abs</span></span>.  In this case <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub>.t<sub>12</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">x</span></span> appears free in <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>; we also know that
        <span class="inlinecode"><span class="id" type="var">x</span></span> is different from <span class="inlinecode"><span class="id" type="var">y</span></span>.  The difference from the previous
        cases is that whereas <span class="inlinecode"><span class="id" type="var">t</span></span> is well typed under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, its
        body <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> is well typed under <span class="inlinecode">(<span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>)</span>, so the IH
        allows us to conclude that <span class="inlinecode"><span class="id" type="var">x</span></span> is assigned some type by the
        extended context <span class="inlinecode">(<span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>)</span>.  To conclude that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>
        assigns a type to <span class="inlinecode"><span class="id" type="var">x</span></span>, we appeal to lemma <span class="inlinecode"><span class="id" type="var">extend_neq</span></span>, noting
        that <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span> are different variables. 
</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">H</span> <span class="id" type="var">H0</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">afi_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>) <span class="id" type="var">Case</span>; <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="tactic">inversion</span> <span class="id" type="var">H0</span>; <span class="id" type="tactic">eauto</span>].<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "afi_abs".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H1</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHappears_free_in</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H7</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">extend_neq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H7</span>; <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
</div>

<div class="doc">
Next, we'll need the fact that any term <span class="inlinecode"><span class="id" type="var">t</span></span> which is well typed in
    the empty context is closed &mdash; that is, it has no free variables. 
<div class="paragraph"> </div>

<a name="lab686"></a><h4 class="section">Exercise: 2 stars, optional (typable_empty__closed)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Corollary</span> <span class="id" type="var">typable_empty__closed</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span>  <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">closed</span> <span class="id" type="var">t</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

 Sometimes, when we have a proof <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>, we will need to
    replace <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> by a different context <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>.  When is it safe
    to do this?  Intuitively, it must at least be the case that
    <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> assigns the same types as <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> to all the variables
    that appear free in <span class="inlinecode"><span class="id" type="var">t</span></span>. In fact, this is the only condition that
    is needed. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">context_invariance</span> : <span style="font-family: arial;">&forall;</span><span style="font-family: serif; font-size:85%;">&Gamma;</span> <span style="font-family: serif; font-size:85%;">&Gamma;'</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style="font-family: serif; font-size:85%;">&Gamma;</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span>  <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style="font-family: arial;">&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> <span style="font-family: arial;">&rarr;</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">x</span> = <span style="font-family: serif; font-size:85%;">&Gamma;'</span> <span class="id" type="var">x</span>) <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style="font-family: serif; font-size:85%;">&Gamma;'</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span>.<br/>

<br/>
</div>

<div class="doc">
<i>Proof</i>: By induction on the derivation of <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule in the derivation was <span class="inlinecode"><span class="id" type="var">T_Var</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>
        and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  By assumption, <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T</span></span> as well, and
        hence <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> by <span class="inlinecode"><span class="id" type="var">T_Var</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the last rule was <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, with <span class="inlinecode"><span class="id" type="var">T</span></span>
        <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&rarr;</span></span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span>.  The induction
        hypothesis is that for any context <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;''</span></span>, if <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span>
        <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;''</span></span> assign the same types to all the free
        variables in <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, then <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> has type <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;''</span></span>.
        Let <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> be a context which agrees with <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> on the
        free variables in <span class="inlinecode"><span class="id" type="var">t</span></span>; we must show <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span>
        <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&rarr;</span></span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span>.

<div class="paragraph"> </div>

        By <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>, it suffices to show that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span>
        <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span>.  By the IH (setting <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;''</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span>), it
        suffices to show that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> agree
        on all the variables that appear free in <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>.  

<div class="paragraph"> </div>

        Any variable occurring free in <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> must either be <span class="inlinecode"><span class="id" type="var">y</span></span>, or
        some other variable.  <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span>
        clearly agree on <span class="inlinecode"><span class="id" type="var">y</span></span>.  Otherwise, we note that any variable
        other than <span class="inlinecode"><span class="id" type="var">y</span></span> which occurs free in <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> also occurs free in
        <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, and by assumption <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>
        agree on all such variables, and hence so do <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span>
        and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> If the last rule was <span class="inlinecode"><span class="id" type="var">T_App</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, with <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span>
        <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&rarr;</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>.  One induction
        hypothesis states that for all contexts <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>, if <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>
        agrees with <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> on the free variables in <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>, then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
        has type <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&rarr;</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>; there is a similar IH for
        <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>.  We must show that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> also has type <span class="inlinecode"><span class="id" type="var">T</span></span> under
        <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>, given the assumption that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> agrees with
        <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> on all the free variables in <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>.  By <span class="inlinecode"><span class="id" type="var">T_App</span></span>, it
        suffices to show that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> each have the same type
        under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> as under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>.  However, we note that all
        free variables in <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> are also free in <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, and similarly
        for free variables in <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>; hence the desired result follows
        by the two IHs.

</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span style="font-family: serif; font-size:85%;">&Gamma;'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_Var".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Var</span>. <span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">&larr;</span> <span class="id" type="var">H0</span>...<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_Abs".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Abs</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHhas_type</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">x1</span> <span class="id" type="var">Hafi</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;the&nbsp;only&nbsp;tricky&nbsp;step...&nbsp;the&nbsp;<span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span>&nbsp;we&nbsp;use&nbsp;to&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;instantiate&nbsp;is&nbsp;<span class="inlinecode"><span class="id" type="var">extend</span></span> <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">extend</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">eq_id_dec</span> <span class="id" type="var">x0</span> <span class="id" type="var">x1</span>)...<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_App".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_App</span> <span class="id" type="keyword">with</span> <span class="id" type="var">T<sub>11</sub></span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
</div>

<div class="doc">
Now we come to the conceptual heart of the proof that reduction
    preserves types &mdash; namely, the observation that <i>substitution</i>
    preserves types.

<div class="paragraph"> </div>

    Formally, the so-called <i>Substitution Lemma</i> says this: suppose we
    have a term <span class="inlinecode"><span class="id" type="var">t</span></span> with a free variable <span class="inlinecode"><span class="id" type="var">x</span></span>, and suppose we've been
    able to assign a type <span class="inlinecode"><span class="id" type="var">T</span></span> to <span class="inlinecode"><span class="id" type="var">t</span></span> under the assumption that <span class="inlinecode"><span class="id" type="var">x</span></span> has
    some type <span class="inlinecode"><span class="id" type="var">U</span></span>.  Also, suppose that we have some other term <span class="inlinecode"><span class="id" type="var">v</span></span> and
    that we've shown that <span class="inlinecode"><span class="id" type="var">v</span></span> has type <span class="inlinecode"><span class="id" type="var">U</span></span>.  Then, since <span class="inlinecode"><span class="id" type="var">v</span></span> satisfies
    the assumption we made about <span class="inlinecode"><span class="id" type="var">x</span></span> when typing <span class="inlinecode"><span class="id" type="var">t</span></span>, we should be
    able to substitute <span class="inlinecode"><span class="id" type="var">v</span></span> for each of the occurrences of <span class="inlinecode"><span class="id" type="var">x</span></span> in <span class="inlinecode"><span class="id" type="var">t</span></span>
    and obtain a new term that still has type <span class="inlinecode"><span class="id" type="var">T</span></span>. 
<div class="paragraph"> </div>

 <i>Lemma</i>: If <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,<span class="id" type="var">x</span>:<span class="id" type="var">U</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">U</span></span>, then <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span>
    <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">substitution_preserves_typing</span> : <span style="font-family: arial;">&forall;</span><span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span class="id" type="var">t</span> <span class="id" type="var">v</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">extend</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">v</span> &#x2208; <span class="id" type="var">U</span>   <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style="font-family: serif; font-size:85%;">&Gamma;</span> <span style="font-family: arial;">&#8866;</span> [<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span>.<br/>

<br/>
</div>

<div class="doc">
One technical subtlety in the statement of the lemma is that we
    assign <span class="inlinecode"><span class="id" type="var">v</span></span> the type <span class="inlinecode"><span class="id" type="var">U</span></span> in the <i>empty</i> context &mdash; in other words,
    we assume <span class="inlinecode"><span class="id" type="var">v</span></span> is closed.  This assumption considerably simplifies
    the <span class="inlinecode"><span class="id" type="var">T_Abs</span></span> case of the proof (compared to assuming <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode">&#x2208;</span>
    <span class="inlinecode"><span class="id" type="var">U</span></span>, which would be the other reasonable assumption at this point)
    because the context invariance lemma then tells us that <span class="inlinecode"><span class="id" type="var">v</span></span> has
    type <span class="inlinecode"><span class="id" type="var">U</span></span> in any context at all &mdash; we don't have to worry about
    free variables in <span class="inlinecode"><span class="id" type="var">v</span></span> clashing with the variable being introduced
    into the context by <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: We prove, by induction on <span class="inlinecode"><span class="id" type="var">t</span></span>, that, for all <span class="inlinecode"><span class="id" type="var">T</span></span> and
    <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, if <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,<span class="id" type="var">x</span>:<span class="id" type="var">U</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">U</span></span>, then <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span>
    <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> is a variable, there are two cases to consider, depending
        on whether <span class="inlinecode"><span class="id" type="var">t</span></span> is <span class="inlinecode"><span class="id" type="var">x</span></span> or some other variable.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>, then from the fact that <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span> <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">U</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> we
            conclude that <span class="inlinecode"><span class="id" type="var">U</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  We must show that <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">v</span></span> has
            type <span class="inlinecode"><span class="id" type="var">T</span></span> under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>, given the assumption that <span class="inlinecode"><span class="id" type="var">v</span></span> has
            type <span class="inlinecode"><span class="id" type="var">U</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T</span></span> under the empty context.  This follows from
            context invariance: if a closed term has type <span class="inlinecode"><span class="id" type="var">T</span></span> in the
            empty context, it has that type in any context.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> is some variable <span class="inlinecode"><span class="id" type="var">y</span></span> that is not equal to <span class="inlinecode"><span class="id" type="var">x</span></span>, then
            we need only note that <span class="inlinecode"><span class="id" type="var">y</span></span> has the same type under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,</span>
            <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">U</span></span> as under <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> is an abstraction <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, then the IH tells us,
        for all <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> and <span class="inlinecode"><span class="id" type="var">T'</span></span>, that if <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span>,<span class="id" type="var">x</span>:<span class="id" type="var">U</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T'</span></span>
        and <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">U</span></span>, then <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;'</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T'</span></span>.

<div class="paragraph"> </div>

        The substitution in the conclusion behaves differently,
        depending on whether <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span> are the same variable name.

<div class="paragraph"> </div>

        First, suppose <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">y</span></span>.  Then, by the definition of
        substitution, <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t</span></span>, so we just need to show <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span>
        <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  But we know <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,<span class="id" type="var">x</span>:<span class="id" type="var">U</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>, and since the
        variable <span class="inlinecode"><span class="id" type="var">y</span></span> does not appear free in <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, the
        context invariance lemma yields <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

        Second, suppose <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">y</span></span>.  We know <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,<span class="id" type="var">x</span>:<span class="id" type="var">U</span>,<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span>
        <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> by inversion of the typing relation, and <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>,<span class="id" type="var">x</span>:<span class="id" type="var">U</span></span>
        <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> follows from this by the context invariance
        lemma, so the IH applies, giving us <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span>,<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span>
        <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span>.  By <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>, <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span><span style="font-family: arial;">&rarr;</span><span class="id" type="var">T<sub>12</sub></span></span>, and
        by the definition of substitution (noting that <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">y</span></span>),
        <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode">\<span class="id" type="var">y</span>:<span class="id" type="var">T<sub>11</sub></span>.</span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span><span style="font-family: arial;">&rarr;</span><span class="id" type="var">T<sub>12</sub></span></span> as required.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> is an application <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, the result follows
        straightforwardly from the definition of substitution and the
        induction hypotheses.

<div class="paragraph"> </div>


</li>
<li> The remaining cases are similar to the application case.

</li>
</ul>

<div class="paragraph"> </div>

    Another technical note: This proof is a rare case where an
    induction on terms, rather than typing derivations, yields a
    simpler argument.  The reason for this is that the assumption
    <span class="inlinecode"><span class="id" type="var">extend</span></span> <span class="inlinecode"><span style="font-family: serif; font-size:85%;">&Gamma;</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">U</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> is not completely generic, in
    the sense that one of the "slots" in the typing relation &mdash; namely
    the context &mdash; is not just a variable, and this means that Coq's
    native induction tactic does not give us the induction hypothesis
    that we want.  It is possible to work around this, but the needed
    generalization is a little tricky.  The term <span class="inlinecode"><span class="id" type="var">t</span></span>, on the other
    hand, <i>is</i> completely generic. 
</div>
<div class="code code-tight">

<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span class="id" type="var">t</span> <span class="id" type="var">v</span> <span class="id" type="var">T</span> <span class="id" type="var">Ht</span> <span class="id" type="var">Ht'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">t_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">t</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;in&nbsp;each&nbsp;case,&nbsp;we'll&nbsp;want&nbsp;to&nbsp;get&nbsp;at&nbsp;the&nbsp;derivation&nbsp;of&nbsp;H&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">simpl</span>...<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "tvar".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">i</span> <span class="id" type="var">into</span> <span class="id" type="var">y</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">eq_id_dec</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "x=y".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">extend_eq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H2</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">clear</span> <span class="id" type="var">H2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>... <span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">Hcontra</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">free_in_context</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">T</span> <span class="id" type="var">empty</span> <span class="id" type="var">Hcontra</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">T'</span> <span class="id" type="var">HT'</span>]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HT'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "x≠y".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Var</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">extend_neq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>...<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "tabs".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">i</span> <span class="id" type="var">into</span> <span class="id" type="var">y</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Abs</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eq_id_dec</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "x=y".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">Hafi</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">extend</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eq_id_dec</span> <span class="id" type="var">y</span> <span class="id" type="var">x</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "x≠y".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHt</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">z</span> <span class="id" type="var">Hafi</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">extend</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eq_id_dec</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">neq_id</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
</div>

<div class="doc">
The substitution lemma can be viewed as a kind of "commutation"
    property.  Intuitively, it says that substitution and typing can
    be done in either order: we can either assign types to the terms
    <span class="inlinecode"><span class="id" type="var">t</span></span> and <span class="inlinecode"><span class="id" type="var">v</span></span> separately (under suitable contexts) and then combine
    them using substitution, or we can substitute first and then
    assign a type to <span class="inlinecode"></span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"></span> &mdash; the result is the same either
    way. 
</div>
<div class="code code-tight">

<br/>
</div>

<div class="doc">
<a name="lab687"></a><h2 class="section">Main Theorem</h2>

<div class="paragraph"> </div>

 We now have the tools we need to prove preservation: if a closed
    term <span class="inlinecode"><span class="id" type="var">t</span></span> has type <span class="inlinecode"><span class="id" type="var">T</span></span>, and takes an evaluation step to <span class="inlinecode"><span class="id" type="var">t'</span></span>, then <span class="inlinecode"><span class="id" type="var">t'</span></span>
    is also a closed term with type <span class="inlinecode"><span class="id" type="var">T</span></span>.  In other words, the small-step
    evaluation relation preserves types.

</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span>  <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t</span> <span style="font-family: arial;">&rArr;</span> <span class="id" type="var">t'</span>  <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t'</span> &#x2208; <span class="id" type="var">T</span>.<br/>

<br/>
</div>

<div class="doc">
<i>Proof</i>: by induction on the derivation of <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> We can immediately rule out <span class="inlinecode"><span class="id" type="var">T_Var</span></span>, <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>, <span class="inlinecode"><span class="id" type="var">T_True</span></span>, and
      <span class="inlinecode"><span class="id" type="var">T_False</span></span> as the final rules in the derivation, since in each of
      these cases <span class="inlinecode"><span class="id" type="var">t</span></span> cannot take a step.

<div class="paragraph"> </div>


</li>
<li> If the last rule in the derivation was <span class="inlinecode"><span class="id" type="var">T_App</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
      <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>.  There are three cases to consider, one for each rule that
      could have been used to show that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> takes a step to <span class="inlinecode"><span class="id" type="var">t'</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> takes a step by <span class="inlinecode"><span class="id" type="var">ST_App1</span></span>, with <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> stepping to
          <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>, then by the IH <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> has the same type as <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>, and
          hence <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> has the same type as <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> The <span class="inlinecode"><span class="id" type="var">ST_App2</span></span> case is similar.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> takes a step by <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span>, then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span>
          <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">T<sub>11</sub>.t<sub>12</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> steps to <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span></span>; the
          desired result now follows from the fact that substitution
          preserves types.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If the last rule in the derivation was <span class="inlinecode"><span class="id" type="var">T_If</span></span>, then <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="keyword">if</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
      <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>, and there are again three cases depending on
      how <span class="inlinecode"><span class="id" type="var">t</span></span> steps.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> steps to <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> or <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>, the result is immediate, since
          <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> have the same type as <span class="inlinecode"><span class="id" type="var">t</span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" type="var">t</span></span> steps by <span class="inlinecode"><span class="id" type="var">ST_If</span></span>, and the desired conclusion
          follows directly from the induction hypothesis.

</li>
</ul>

</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">HT</span>) <span class="id" type="var">Case</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t'</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span> <span style="font-family: serif; font-size:85%;">&Gamma;</span>; <span class="id" type="tactic">subst</span>; <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">auto</span>].<br/>
&nbsp;&nbsp;<span class="id" type="var">Case</span> "T_App".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Most&nbsp;of&nbsp;the&nbsp;cases&nbsp;are&nbsp;immediate&nbsp;by&nbsp;induction,&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>&nbsp;takes&nbsp;care&nbsp;of&nbsp;them&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SCase</span> "ST_AppAbs".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">substitution_preserves_typing</span> <span class="id" type="keyword">with</span> <span class="id" type="var">T<sub>11</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HT1</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
</div>

<div class="doc">
<a name="lab688"></a><h4 class="section">Exercise: 2 stars (subject_expansion_stlc)</h4>
 An exercise in the <span class="inlinecode"><span class="id" type="keyword">Types</span></span> chapter asked about the subject
    expansion property for the simple language of arithmetic and
    boolean expressions.  Does this property hold for STLC?  That is,
    is it always the case that, if <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span style="font-family: arial;">&rArr;</span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> and <span class="inlinecode"><span class="id" type="var">has_type</span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>,
    then <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode"><span style="font-family: arial;">&#8866;</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>?  If so, prove it.  If not, give a
    counter-example not involving conditionals.

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<font size=-2>&#9744;</font>

</div>
<div class="code code-tight">

<br/>
</div>

<div class="doc">
<a name="lab689"></a><h1 class="section">Type Soundness</h1>

<div class="paragraph"> </div>

<a name="lab690"></a><h4 class="section">Exercise: 2 stars, optional (type_soundness)</h4>

<div class="paragraph"> </div>

 Put progress and preservation together and show that a well-typed
    term can <i>never</i> reach a stuck state.  
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">stuck</span> (<span class="id" type="var">t</span>:<span class="id" type="var">tm</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">normal_form</span> <span class="id" type="var">step</span>) <span class="id" type="var">t</span> <span style="font-family: arial;">&and;</span> ¬ <span class="id" type="var">value</span> <span class="id" type="var">t</span>.<br/>

<br/>
<span class="id" type="keyword">Corollary</span> <span class="id" type="var">soundness</span> : <span style="font-family: arial;">&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">empty</span> <span style="font-family: arial;">&#8866;</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> <span style="font-family: arial;">&rarr;</span> <br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span style="font-family: arial;">&rArr;*</span> <span class="id" type="var">t'</span> <span style="font-family: arial;">&rarr;</span><br/>
&nbsp;&nbsp;~(<span class="id" type="var">stuck</span> <span class="id" type="var">t'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">Hhas_type</span> <span class="id" type="var">Hmulti</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">stuck</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> [<span class="id" type="var">Hnf</span> <span class="id" type="var">Hnot_val</span>]. <span class="id" type="tactic">unfold</span> <span class="id" type="var">normal_form</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hnf</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hmulti</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>

<br/>
</div>

<div class="doc">
<a name="lab691"></a><h1 class="section">Uniqueness of Types</h1>

<div class="paragraph"> </div>

<a name="lab692"></a><h4 class="section">Exercise: 3 stars (types_unique)</h4>
 Another pleasant property of the STLC is that types are
    unique: a given term (in a given context) has at most one
    type.  Formalize this statement and prove it. 
</div>
<div class="code code-tight">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
</div>
<div class="code code-tight">

<br/>
</div>

<div class="doc">
<a name="lab693"></a><h1 class="section">Additional Exercises</h1>

<div class="paragraph"> </div>

<a name="lab694"></a><h4 class="section">Exercise: 1 star (progress_preservation_statement)</h4>
 Without peeking, write down the progress and preservation
    theorems for the simply typed lambda-calculus.  <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a name="lab695"></a><h4 class="section">Exercise: 2 stars (stlc_variation1)</h4>
 Suppose we add a new term <span class="inlinecode"><span class="id" type="var">zap</span></span> with the following reduction rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Zap) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">t&nbsp;<span style="font-family: arial;">&rArr;</span>&nbsp;zap</td>
  <td></td>
</td>
</table></center>and the following typing rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Zap) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;zap&nbsp;:&nbsp;T</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>

<font size=-2>&#9744;</font>

<div class="paragraph"> </div>

<a name="lab696"></a><h4 class="section">Exercise: 2 stars (stlc_variation2)</h4>
 Suppose instead that we add a new term <span class="inlinecode"><span class="id" type="var">foo</span></span> with the following reduction rules:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Foo1) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(\x:A.&nbsp;x)&nbsp;<span style="font-family: arial;">&rArr;</span>&nbsp;foo</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Foo2) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">foo&nbsp;<span style="font-family: arial;">&rArr;</span>&nbsp;true</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>

<font size=-2>&#9744;</font>

<div class="paragraph"> </div>

<a name="lab697"></a><h4 class="section">Exercise: 2 stars (stlc_variation3)</h4>
 Suppose instead that we remove the rule <span class="inlinecode"><span class="id" type="var">ST_App1</span></span> from the <span class="inlinecode"><span class="id" type="var">step</span></span>
    relation. Which of the following properties of the STLC remain
    true in the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>

<font size=-2>&#9744;</font>

<div class="paragraph"> </div>

<a name="lab698"></a><h4 class="section">Exercise: 2 stars, optional (stlc_variation4)</h4>
 Suppose instead that we add the following new rule to the reduction relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_FunnyIfTrue) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(if&nbsp;true&nbsp;then&nbsp;t<sub>1</sub>&nbsp;else&nbsp;t<sub>2</sub>)&nbsp;<span style="font-family: arial;">&rArr;</span>&nbsp;true</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<a name="lab699"></a><h4 class="section">Exercise: 2 stars, optional (stlc_variation5)</h4>
 Suppose instead that we add the following new rule to the typing relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Bool->Bool->Bool</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;t<sub>2</sub>&nbsp;&#x2208;&nbsp;Bool</td>
  <td class="infrulenamecol" rowspan="3">
    (T_FunnyApp) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;t<sub>1</sub>&nbsp;t<sub>2</sub>&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<a name="lab700"></a><h4 class="section">Exercise: 2 stars, optional (stlc_variation6)</h4>
 Suppose instead that we add the following new rule to the typing relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;t<sub>2</sub>&nbsp;&#x2208;&nbsp;Bool</td>
  <td class="infrulenamecol" rowspan="3">
    (T_FunnyApp') &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: serif; font-size:85%;">&Gamma;</span>&nbsp;<span style="font-family: arial;">&#8866;</span>&nbsp;t<sub>1</sub>&nbsp;t<sub>2</sub>&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<a name="lab701"></a><h4 class="section">Exercise: 2 stars, optional (stlc_variation7)</h4>
 Suppose we add the following new rule to the typing
    relation of the STLC:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_FunnyAbs) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule"><span style="font-family: arial;">&#8866;</span>&nbsp;\x:Bool.t&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" type="var">step</span></span>

<div class="paragraph"> </div>


</li>
<li> Progress

<div class="paragraph"> </div>


</li>
<li> Preservation

</li>
</ul>

<div class="paragraph"> </div>

<font size=-2>&#9744;</font>

</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">STLCProp</span>.<br/>

<br/>
</div>

<div class="doc">
<a name="lab702"></a><h2 class="section">Exercise: STLC with Arithmetic</h2>

<div class="paragraph"> </div>

 To see how the STLC might function as the core of a real
    programming language, let's extend it with a concrete base
    type of numbers and some constants and primitive
    operators. 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">STLCArith</span>.<br/>

<br/>
</div>

<div class="doc">
To types, we add a base type of natural numbers (and remove
    booleans, for brevity) 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ty</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">TArrow</span> : <span class="id" type="var">ty</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">ty</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">TNat</span>   : <span class="id" type="var">ty</span>.<br/>

<br/>
</div>

<div class="doc">
To terms, we add natural number constants, along with
    successor, predecessor, multiplication, and zero-testing... 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tm</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">tvar</span> : <span class="id" type="var">id</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tapp</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tabs</span> : <span class="id" type="var">id</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">ty</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tnat</span>  : <span class="id" type="var">nat</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tsucc</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tpred</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tmult</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tif0</span>  : <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">&rarr;</span> <span class="id" type="var">tm</span>.<br/>

<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Tactic Notation</span> "t_cases" <span class="id" type="var">tactic</span>(<span class="id" type="var">first</span>) <span class="id" type="var">ident</span>(<span class="id" type="var">c</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="var">first</span>;<br/>
&nbsp;&nbsp;[ <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tvar" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tapp" <br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tabs" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tnat" <br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tsucc" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tpred"<br/>
&nbsp;&nbsp;| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tmult" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tif0" ].<br/>
</div>

<br/>
</div>

<div class="doc">
<a name="lab703"></a><h4 class="section">Exercise: 4 stars (stlc_arith)</h4>
 Finish formalizing the definition and properties of the STLC extended
    with arithmetic.  Specifically:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Copy the whole development of STLC that we went through above (from
      the definition of values through the Progress theorem), and
      paste it into the file at this point.

<div class="paragraph"> </div>


</li>
<li> Extend the definitions of the <span class="inlinecode"><span class="id" type="tactic">subst</span></span> operation and the <span class="inlinecode"><span class="id" type="var">step</span></span>
      relation to include appropriate clauses for the arithmetic operators.

<div class="paragraph"> </div>


</li>
<li> Extend the proofs of all the properties (up to <span class="inlinecode"><span class="id" type="var">soundness</span></span>) of
      the original STLC to deal with the new syntactic forms.  Make
      sure Coq accepts the whole file. 
</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
</div>
<div class="code code-tight">

<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">STLCArith</span>.<br/>

<br/>
<span class="comment">(*&nbsp;$Date:&nbsp;2014-04-23&nbsp;09:37:37&nbsp;-0400&nbsp;(Wed,&nbsp;23&nbsp;Apr&nbsp;2014)&nbsp;$&nbsp;*)</span><br/>

<br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://www.lix.polytechnique.fr/coq/">coqdoc</a>
</div>

</div>

</body>
</html>