StlcPropProperties of STLC

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

Canonical Forms

As we saw for the simple calculus in the Types chapter, the first step in establishing basic properties of reduction and types is to identify the possible canonical forms (i.e., well-typed closed values) belonging to each type. For Bool, these are the boolean values tru and fls; for arrow types, they are lambda-abstractions.

Lemma canonical_forms_bool : ∀ t,
  empty ⊢ t \in Bool →
  value t →
  (t = tru) ∨ (t = fls).
Proof.
  intros t HT HVal.
  inversion HVal; intros; subst; try inversion HT; auto.
Qed.

Lemma canonical_forms_fun : ∀ t T1 T2,
  empty ⊢ t \in (Arrow T1 T2) →
  value t →
  ∃ x u, t = abs x T1 u.
Proof.
  intros t T1 T2 HT HVal.
  inversion HVal; intros; subst; try inversion HT; subst; auto.
  ∃ x0, t0. auto.
Qed.

Progress

The progress theorem tells us that closed, well-typed terms are not stuck.

Theorem progress : ∀ t T,
  empty ⊢ t \in T →
  value t ∨ ∃ t', t --> t'.
Proof with eauto.
  intros t T Ht.
  remember (@empty ty) as Gamma.
  induction Ht; subst Gamma...
  - (* T_Var *)
    (* contradictory: variables cannot be typed in an
       empty context *)
    inversion H.
  - (* T_App *)
    (* t = t1 t2.  Proceed by cases on whether t1 is a
       value or steps... *)
    right. destruct IHHt1...
    + (* t1 is a value *)
      destruct IHHt2...
      × (* t2 is also a value *)
        assert (∃ x0 t0, t1 = abs x0 T11 t0).
        eapply canonical_forms_fun; eauto.
        destruct H1 as [x0 [t0 Heq]]. subst.
        ∃ ([x0:=t2]t0)...
      × (* t2 steps *)
        inversion H0 as [t2' Hstp]. ∃ (app t1 t2')...
    + (* t1 steps *)
      inversion H as [t1' Hstp]. ∃ (app t1' t2)...
  - (* T_Test *)
    right. destruct IHHt1...
    + (* t1 is a value *)
      destruct (canonical_forms_bool t1); subst; eauto.
    + (* t1 also steps *)
      inversion H as [t1' Hstp]. ∃ (test t1' t2 t3)...
Qed.

Preservation

For preservation, we need some technical machinery for reasoning about variables and substitution.
  • The preservation theorem is proved by induction on a typing derivation, pretty much as we did in the Types chapter.
    Main novelty: ST_AppAbs uses 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.
    Tricky cases: variables and function abstractions.
    In both cases, we need to take a term s that has been shown to be well-typed in some context Gamma and consider the same term s in a slightly different context Gamma'.
    For this we prove a...
  • context invariance lemma, showing that typing is preserved under "inessential changes" to the context Gamma -- in particular, changes that do not affect any of the free variables of the term.
    And finally, for this, we need a careful definition of...
  • the free variables of a term -- i.e., those variables mentioned in a term and not in the scope of an enclosing function abstraction binding a variable of the same name.
To make Coq happy, we need to formalize the story in the opposite order...

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:T→U. x y
  • both x and y appear free in (\x:T→U. x y) x
  • no variables appear free in \x:T→U. \y:T. x y
Formally:

Inductive appears_free_in : string → tm → Prop :=
  | afi_var : ∀ x,
      appears_free_in x (var x)
  | afi_app1 : ∀ x t1 t2,
      appears_free_in x t1 →
      appears_free_in x (app t1 t2)
  | afi_app2 : ∀ x t1 t2,
      appears_free_in x t2 →
      appears_free_in x (app t1 t2)
  | afi_abs : ∀ x y T11 t12,
      y ≠ x →
      appears_free_in x t12 →
      appears_free_in x (abs y T11 t12)
  | afi_test1 : ∀ x t1 t2 t3,
      appears_free_in x t1 →
      appears_free_in x (test t1 t2 t3)
  | afi_test2 : ∀ x t1 t2 t3,
      appears_free_in x t2 →
      appears_free_in x (test t1 t2 t3)
  | afi_test3 : ∀ x t1 t2 t3,
      appears_free_in x t3 →
      appears_free_in x (test t1 t2 t3).
Hint Constructors appears_free_in.

The free variables of a term are just the variables that appear free in it. A term with no free variables is said to be closed.

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

Substitution

To prove that substitution preserves typing, 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 Gamma, then it must be the case that Gamma assigns a type to x.

Lemma free_in_context : ∀ x t T Gamma,
   appears_free_in x t →
   Gamma ⊢ t \in T →
   ∃ T', Gamma x = Some T'.

From the free_in_context lemma, it immediately follows that any term t that is well typed in the empty context is closed (it has no free variables).

Corollary typable_empty__closed : ∀ t T,
    empty ⊢ t \in T →
    closed t.

Sometimes, when we have a proof of some typing relation Gamma ⊢ t \in T, we will need to replace Gamma by a different context Gamma'.
It is safe to do this when Gamma' assigns the same types as Gamma to all the free variables of t.

Lemma context_invariance : ∀ Gamma Gamma' t T,
     Gamma ⊢ t \in T →
     (∀ x, appears_free_in x t → Gamma x = Gamma' x) →
     Gamma' ⊢ t \in T.
Proof with eauto.
  intros.
  generalize dependent Gamma'.
  induction H; intros; auto.
  - (* T_Var *)
    apply T_Var. rewrite <- H0...
  - (* T_Abs *)
    apply T_Abs.
    apply IHhas_type. intros x1 Hafi.
    (* the only tricky step... the Gamma' we use to
       instantiate is x⊢>T11;Gamma *)
    unfold update. unfold t_update. destruct (eqb_string x0 x1) eqn: Hx0x1...
    rewrite eqb_string_false_iff in Hx0x1. auto.
  - (* T_App *)
    apply T_App with T11...
Qed.

Now we come to the conceptual heart of the proof that reduction preserves types -- namely, the observation that substitution preserves types.
The substitution lemma says:
  • 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, we can substitute v for each of the occurrences of x in t and obtain a new term that still has type T.

Lemma substitution_preserves_typing : ∀ Gamma x U t v T,
  (x ⊢> U ; Gamma) ⊢ t \in T →
  empty ⊢ v \in U →
  Gamma ⊢ [x:=v]t \in T.

Main Theorem

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

Theorem preservation : ∀ t t' T,
  empty ⊢ t \in T →
  t --> t' →
  empty ⊢ t' \in T.
Proof with eauto.
  remember (@empty ty) as Gamma.
  intros t t' T HT. generalize dependent t'.
  induction HT;
       intros t' HE; subst Gamma; subst;
       try solve [inversion HE; subst; auto].
  - (* T_App *)
    inversion HE; subst...
    (* Most of the cases are immediate by induction,
       and eauto takes care of them *)
    + (* ST_AppAbs *)
      apply substitution_preserves_typing with T11...
      inversion HT1...
Qed.