StlcPropProperties of STLC

In this chapter, we develop the fundamental theory of the Simply Typed Lambda Calculus — in particular, the type safety theorem.


As before, the progress 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 Types chapter.

Theorem progress : t T,
     empty tT
     value t t', t t'.

Proof with eauto.
  intros t T Ht.
  remember (@empty ty) as Γ.
  has_type_cases (induction Ht) Case; subst Γ...
  Case "T_Var".
    (* contradictory: variables cannot be typed in an 
       empty context *)

    inversion H.

  Case "T_App".
    (* t = t1 t2.  Proceed by cases on whether t1 is a 
       value or steps... *)

    right. destruct IHHt1...
    SCase "t1 is a value".
      destruct IHHt2...
      SSCase "t2 is also a value".
        (* Since t1 is a value and has an arrow type, it
           must be an abs. Sometimes this is proved separately 
           and called a "canonical forms" lemma. *)

        inversion H; subst. ([x0:=t2]t)...
        solve by inversion. solve by inversion.
      SSCase "t2 steps".
        inversion H0 as [t2' Hstp]. (tapp t1 t2')...

    SCase "t1 steps".
      inversion H as [t1' Hstp]. (tapp t1' t2)...

  Case "T_If".
    right. destruct IHHt1...

    SCase "t1 is a value".
      (* Since t1 is a value of boolean type, it must
         be true or false *)

      inversion H; subst. solve by inversion.
      SSCase "t1 = true". eauto.
      SSCase "t1 = false". eauto.

    SCase "t1 also steps".
      inversion H as [t1' Hstp]. (tif t1' t2 t3)...


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:
  • The preservation theorem is proved by induction on a typing derivation, pretty much as we did in the Types chapter. The one case that is significantly different is the one for the ST_AppAbs 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...
  • substitution lemma, stating that substituting a (closed) term s for a variable x in a term t preserves the type of t. The proof goes by induction on the form of t 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 s that has been shown to be well-typed in some context Γ and consider the same term s in a slightly different context Γ'. For this we prove a...
  • context invariance lemma, showing that typing is preserved under "inessential changes" to the context Γ — in particular, changes that do not affect any of the free variables of the term. For this, we need a careful definition of
  • the free variables of a term — i.e., the variables occuring in the term that are not in the scope of a function abstraction that binds them.

Free Occurrences

A variable x appears free in a term t if t contains some occurrence of x that is not under an abstraction labeled x. For example:
  • y appears free, but x does not, in λx:TU. x y
  • both x and y appear free in x:TU. x y) x
  • no variables appear free in λx:TU. λy:T. x y

Inductive appears_free_in : id tm Prop :=
  | afi_var : x,
      appears_free_in x (tvar x)
  | afi_app1 : x t1 t2,
      appears_free_in x t1 appears_free_in x (tapp t1 t2)
  | afi_app2 : x t1 t2,
      appears_free_in x t2 appears_free_in x (tapp t1 t2)
  | afi_abs : x y T11 t12,
      appears_free_in x t12
      appears_free_in x (tabs y T11 t12)
  | afi_if1 : x t1 t2 t3,
      appears_free_in x t1
      appears_free_in x (tif t1 t2 t3)
  | afi_if2 : x t1 t2 t3,
      appears_free_in x t2
      appears_free_in x (tif t1 t2 t3)
  | afi_if3 : x t1 t2 t3,
      appears_free_in x t3
      appears_free_in x (tif t1 t2 t3).

Tactic Notation "afi_cases" tactic(first) ident(c) :=
  [ Case_aux c "afi_var"
  | Case_aux c "afi_app1" | Case_aux c "afi_app2"
  | Case_aux c "afi_abs"
  | Case_aux c "afi_if1" | Case_aux c "afi_if2"
  | Case_aux c "afi_if3" ].

Hint Constructors appears_free_in.

A term in which no variables appear free is said to be closed.

Definition closed (t:tm) :=
  x, ¬ appears_free_in x t.


We first need a technical lemma connecting free variables and typing contexts. If a variable x appears free in a term t, and if we know t is well typed in context Γ, then it must be the case that Γ assigns a type to x.

Lemma free_in_context : x t T Γ,
   appears_free_in x t
   Γ tT
   T', Γ x = Some T'.

  intros x t T Γ H H0. generalize dependent Γ.
  generalize dependent T.
  afi_cases (induction H) Case;
         intros; try solve [inversion H0; eauto].
  Case "afi_abs".
    inversion H1; subst.
    apply IHappears_free_in in H7.
    rewrite extend_neq in H7; assumption.

Next, we'll need the fact that any term t which is well typed in the empty context is closed — that is, it has no free variables.

Corollary typable_empty__closed : t T,
    empty tT
    closed t.
  (* FILL IN HERE *) Admitted.

Sometimes, when we have a proof Γ t : T, we will need to replace Γ by a different context Γ'. When is it safe to do this? Intuitively, it must at least be the case that Γ' assigns the same types as Γ to all the variables that appear free in t. In fact, this is the only condition that is needed.

Lemma context_invariance : Γ Γ' t T,
     Γ tT
     (x, appears_free_in x t Γ x = Γ' x)
     Γ' tT.

Proof with eauto.
  generalize dependent Γ'.
  has_type_cases (induction H) Case; intros; auto.
  Case "T_Var".
    apply T_Var. rewrite H0...
  Case "T_Abs".
    apply T_Abs.
    apply IHhas_type. intros x1 Hafi.
    (* the only tricky step... the Γ' we use to 
       instantiate is extend Γ x T11 *)

    unfold extend. destruct (eq_id_dec x0 x1)...
  Case "T_App".
    apply T_App with T11...

Now we come to the conceptual heart of the proof that reduction preserves types — namely, the observation that substitution preserves types.
Formally, the so-called Substitution Lemma says this: suppose we have a term t with a free variable x, and suppose we've been able to assign a type T to t under the assumption that x has some type U. Also, suppose that we have some other term v and that we've shown that v has type U. Then, since v satisfies the assumption we made about x when typing t, we should be able to substitute v for each of the occurrences of x in t and obtain a new term that still has type T.
Lemma: If Γ,x:U t T and v U, then Γ [x:=v]t T.

Lemma substitution_preserves_typing : Γ x U t v T,
     extend Γ x U tT
     empty vU
     Γ [x:=v]tT.

Proof with eauto.
  intros Γ x U t v T Ht Ht'.
  generalize dependent Γ. generalize dependent T.
  t_cases (induction t) Case; intros T Γ H;
    (* in each case, we'll want to get at the derivation of H *)
    inversion H; subst; simpl...
  Case "tvar".
    rename i into y. destruct (eq_id_dec x y).
    SCase "x=y".
      rewrite extend_eq in H2.
      inversion H2; subst. clear H2.
                  eapply context_invariance... intros x Hcontra.
      destruct (free_in_context _ _ T empty Hcontra) as [T' HT']...
      inversion HT'.
    SCase "x≠y".
      apply T_Var. rewrite extend_neq in H2...
  Case "tabs".
    rename i into y. apply T_Abs.
    destruct (eq_id_dec x y).
    SCase "x=y".
      eapply context_invariance...
      intros x Hafi. unfold extend.
      destruct (eq_id_dec y x)...
    SCase "x≠y".
      apply IHt. eapply context_invariance...
      intros z Hafi. unfold extend.
      destruct (eq_id_dec y z)...
      subst. rewrite neq_id...

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 t and v separately (under suitable contexts) and then combine them using substitution, or we can substitute first and then assign a type to [x:=v] t — the result is the same either way.

Main Theorem

We now have the tools we need to prove preservation: if a closed term t has type T, and takes an evaluation step to t', then t' is also a closed term with type T. In other words, the small-step evaluation relation preserves types.

Theorem preservation : t t' T,
     empty tT
     t t'
     empty t'T.

Proof with eauto.
  remember (@empty ty) as Γ.
  intros t t' T HT. generalize dependent t'.
  has_type_cases (induction HT) Case;
       intros t' HE; subst Γ; subst;
       try solve [inversion HE; subst; auto].
  Case "T_App".
    inversion HE; subst...
    (* Most of the cases are immediate by induction, 
       and eauto takes care of them *)

    SCase "ST_AppAbs".
      apply substitution_preserves_typing with T11...
      inversion HT1...

End STLCProp.