StlcPropProperties of STLC

(*
                  THE SIMPLY TYPED LAMBDA CALCULUS

    Syntax:

       t ::= x                         variable
           | \x:T,t                    abstraction
           | t t                       application
           | true                      constant true
           | false                     constant false
           | if t then t else t        conditional


    Values:

       v ::= \x:T,t
           | true
           | false


    Substitution:

       x:=sx               = s
       x:=sy               = y                      if x <> y
       x:=s(\x:T, t)       = \x:T, t
       x:=s(\y:T, t)       = \y:T, x:=st          if x <> y
       x:=s(t1 t2)         = (x:=st1) (x:=st2)
       x:=strue            = true
       x:=sfalse           = false
       x:=s(if t1 then t2 else t3) =
                       if x:=st1 then x:=st2 else x:=st3


    Small-step operational semantics:

                               value v2
                     ---------------------------                    (ST_AppAbs)
                     (\x:T2,t1) v2 --> x:=v2t1

                              t1 --> t1'
                           ----------------                           (ST_App1)
                           t1 t2 --> t1' t2

                              value v1
                              t2 --> t2'
                           ----------------                           (ST_App2)
                           v1 t2 --> v1 t2'

                    --------------------------------                (ST_IfTrue)
                    (if true then t1 else t2) --> t1

                    ---------------------------------              (ST_IfFalse)
                    (if false then t1 else t2) --> t2

                              t1 --> t1'
         ----------------------------------------------------           (ST_If)
         (if t1 then t2 else t3) --> (if t1' then t2 else t3)


    Typing:

                              Gamma x = T1
                            -----------------                           (T_Var)
                            Gamma ⊢ x ∈ T1

                        x ⊢> T2 ; Gamma ⊢ t1 ∈ T1
                        -----------------------------                   (T_Abs)
                         Gamma ⊢ \x:T2,t1 ∈ T2->T1

                        Gamma ⊢ t1 ∈ T2->T1
                          Gamma ⊢ t2 ∈ T2
                         ----------------------                         (T_App)
                         Gamma ⊢ t1 t2 ∈ T1

                         ---------------------                         (T_True)
                         Gamma ⊢ true ∈ Bool

                         ---------------------                        (T_False)
                         Gamma ⊢ false ∈ Bool

       Gamma ⊢ t1 ∈ Bool    Gamma ⊢ t2 ∈ T1   Gamma ⊢ t3 ∈ T1
       ---------------------------------------------------------------  (T_If)
                  Gamma ⊢ if t1 then t2 else t3 ∈ T1
*)
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 very simple language 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 values) belonging to each type. For Bool, these are again the boolean values true and false; for arrow types, they are lambda-abstractions.
Formally, we will need these lemmas only for terms that are not only well typed but closed -- well typed in the empty context.
Lemma canonical_forms_bool : ∀ t,
  empty ⊢ t \in Bool →
  value t →
  (t = <{true}>) ∨ (t = <{false}>).
Proof.
  intros t HT HVal.
  destruct HVal; auto.
  inversion HT.
Qed.

Lemma canonical_forms_fun : ∀ t T1 T2,
  empty ⊢ t \in (T1 → T2) →
  value t →
  ∃ x u, t = <{\x:T1, u}>.
Proof.
  intros t T1 T2 HT HVal.
  destruct HVal; inversion HT; subst.
  ∃ x0, t1. reflexivity.
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 as Gamma.
  induction Ht; subst Gamma; auto.
  (* auto solves all three cases in which t is a value *)
  - (* T_Var *)
    (* contradictory: variables cannot be typed in an
       empty context *)
    discriminate 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 *)
        eapply canonical_forms_fun in Ht1; [|assumption].
        destruct Ht1 as [x [t0 H1]]. subst.
        ∃ (<{ [x:=t2]t0 }>)...
      × (* t2 steps *)
        destruct H0 as [t2' Hstp]. ∃ (<{t1 t2'}>)...
    + (* t1 steps *)
      destruct H as [t1' Hstp]. ∃ (<{t1' t2}>)...
  - (* T_If *)
    right. destruct IHHt1...
    + (* t1 is a value *)
      destruct (canonical_forms_bool t1); subst; eauto.
    + (* t1 also steps *)
      destruct H as [t1' Hstp]. ∃ <{if t1' then t2 else 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, well-typed) 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 case: variables.
    In this case, we need to deduce from the fact that a term s has type S in the empty context the fact that s has type S in every context. For this we prove a...
    For this we prove a...
  • weakening lemma, showing that typing is preserved under "extensions" to the context Gamma.
To make Coq happy, we need to formalize the story in the opposite order...

The Weakening Lemma

Typing is preserved under "extensions" to the context Gamma. (Recall the definition of "inclusion" from Maps.v.)
Lemma weakening : ∀ Gamma Gamma' t T,
     inclusion Gamma Gamma' →
     Gamma ⊢ t \in T →
     Gamma' ⊢ t \in T.
Proof.
  intros Gamma Gamma' t T H Ht.
  generalize dependent Gamma'.
  induction Ht; eauto using inclusion_update.
Qed.
The following simple corollary is what we actually need below.
Lemma weakening_empty : ∀ Gamma t T,
     empty ⊢ t \in T →
     Gamma ⊢ t \in T.
Proof.
  intros Gamma t T.
  eapply weakening.
  discriminate.
Qed.

A Substitution Lemma

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 ingredients we need to prove preservation: if a closed, well-typed 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.
  intros t t' T HT. generalize dependent t'.
  remember empty as Gamma.
  induction HT;
       intros t' HE; 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 T2...
      inversion HT1...
Qed.
The context invariance lemma can actually be used in place of the weakening lemma to prove the crucial substitution lemma stated earlier.