11 - Simply-Typed Lambda Calculus | Formal Models and Semantics

lec_11_stlc

From Coq Require Import Strings.String.
Require Import Maps.
Require Import Multi.

References

https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html
https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html

Recap

Last time, we introduced Lambda Calculus, a theory of "substitution".
In particular, we saw that *capture-avoid substitution* was the appropriate notion of substitution.
We then gave two semantics for Lambda Calculus: call-by-value and call-by-name and saw that they could give different semantics.
At the end, we introduced an extension of Lambda Calculus with booleans and translated them away using Church encodings.
This extension can create terms that get "stuck" in evaluation.
Today we'll look at a solution of "stuck" terms and solution to that problem via type-system.
More concretely, we'll introduce the *simply-typed lambda calculus*, which forms the foundation of every modern functional programming language including Coq.

Goal for today

Introduce the simply-typed Lambda Calculus (STLC) and it's type-system.
Prove type-soundness via progress and preservation.
Show that STLC cannot express recursion.

Problem

Module UNTYPED_LAMBDA_CALCULUS.

Require Import lec_10_lambda.

Recall the lambda calculus with booleans.

Print tm'.

Terms

Inductive tm' : Set :=
| tm_var' : string -> tm'
| tm_app' : tm' -> tm' -> tm'
| tm_abs' : string -> tm' -> tm'
| tm_true' : tm'
| tm_false' : tm'
| tm_if' : tm' -> tm' -> tm' -> tm'

Print cbv_step'.

Call-by-value Semantics

Inductive cbv_step' : tm' -> tm' -> Prop :=
| _cbv_app1 :
forall t1 t2 t1' : tm',
t1 ~--> t1' ->
tm_app' t1 t2 ~--> tm_app' t1' t2
| _cbv_app2 :
forall v t2 t2' : tm',
value' v -> t2 ~--> t2' -> tm_app' v t2 ~--> tm_app' v t2'
| _cbv_beta :
forall (x : string) (t v : tm'),
value' v -> tm_app' (tm_abs' x t) v ~--> subst' x v t
| _if_cond :
forall tcond ttrue tfalse tcond' : tm',
tcond ~--> tcond' ->
tm_if' tcond ttrue tfalse ~--> tm_if' tcond' ttrue tfalse
| _if_true :
forall ttrue tfalse : tm',
tm_if' tm_true' ttrue tfalse ~--> ttrue
| _if_false :
forall ttrue tfalse : tm',
tm_if' tm_true' ttrue tfalse ~--> tfalse.

Stuck Terms

Example 1:

false true

Can't apply false to true.

Example 2:

true (\x, x)

Can't apply true to lambda.

Example 3:

if (\x, x) (\y, y) (\z, z)

Can't apply if to lambda.

Example 4:

if true (false (\x, x)) (\z, z)

The if true reduces to a (false (\x, x)) which is stuck.

Types: idea

We will introduce a notion called types that will classify terms according to the shape of values they compute.
We can then prove a type-soundness theorem: well-typed terms do not get stuck.
A sufficiently powerful type-system cannot be both *sound* and complete.
Soundness means: if a term is well-typed, then it does not get stuck.
Completeness means: if a term does not get stuck, then it is well-typed.
Type-systems are generally designed to be sound.
We will introduce type-systems via the simply-typed lambda calculus (STLC).
Coq is a sophisticated verion of typed lambda calculus.

End UNTYPED_LAMBDA_CALCULUS.

Simply-Typed Lambda Calculus Syntax

Types or the shape of a value

We first need the "shape" of values.
Let us remind ourselves what the values were.

Inductive value' : tm' -> Prop :=
| v_abs' : forall (x : string) (t1 : tm'), value' (tm_abs' x t1)
| v_true' : value' tm_true'
| v_false' : value' tm_false

Type Syntax

(*

T ::= Bool
| T -> T

*)
Inductive ty : Type :=
| Ty_Bool : ty (* for the boolean values *)
| Ty_Arrow : ty -> ty -> ty (* t1 -> t2, for the abstraction values *)
.

Examples

(*
   Example 1:

     true: Bool
     false: Bool
*)

(*
   Example 2:

     negation: Bool -> Bool
*)

(*
   Example 3:

     and: Bool -> (Bool -> Bool) = Bool -> Bool -> Bool
*)

(*

   Example 4:

     \f, true: (Bool -> Bool) -> Bool

*)

Syntax

Notation

Declare Custom Entry stlc.
Notation "<{ e }>" := e (e custom stlc at level 99).
Notation "( x )" := x (in custom stlc, x at level 99).
Notation "x" := x (in custom stlc at level 0, x constr at level 0).
Notation "S -> T" := (Ty_Arrow S T) (in custom stlc at level 50, right associativity).
Notation "x y" := (tm_app x y) (in custom stlc at level 1, left associativity).
Notation "\ x : t , y" :=
  (tm_abs x t y) (in custom stlc at level 90, x at level 99,
                     t custom stlc at level 99,
                     y custom stlc at level 99,
                     left associativity).
Coercion tm_var : string >-> tm.
Notation "'Bool'" := Ty_Bool (in custom stlc at level 0).
Notation "'if' x 'then' y 'else' z" :=
  (tm_if x y z) (in custom stlc at level 89,
                    x custom stlc at level 99,
                    y custom stlc at level 99,
                    z custom stlc at level 99,
                    left associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := tm_true (in custom stlc at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := tm_false (in custom stlc at level 0).

Definition x : string := "x".
Definition y : string := "y".
Definition z : string := "z".
Definition f : string := "f".
Definition g : string := "g".
Definition h : string := "h".
(*
Hint Unfold x : core.
Hint Unfold y : core.
Hint Unfold z : core.
Hint Unfold f : core.
Hint Unfold g : core.
Hint Unfold h : core.
*)

Examples

Example ex1 :=
  <{ \x : Bool , x }>.

Example ex2 :=
  <{ \x : Bool , (f (g x )) }>.

Example ex3 :=
  <{ (\x : Bool , \y : Bool -> Bool , x ) }>.

Example ex4 :=
  <{ (\x : Bool -> Bool , x ) (\x : Bool , x ) }>.

Example ex5 :=
  <{ (\x : Bool -> Bool -> Bool , x ) h }>.

Example ex6 :=
  <{ (\x : Bool , \y : (Bool -> Bool ) -> Bool , \x : Bool -> Bool , y x ) }>.

Example not :=
  <{ (\x : Bool , if x then false else true ) }>.

Example and :=
  <{ (\x : Bool , \y : Bool , if x then y else false ) }>.

Example or :=
  <{ (\x : Bool , \y : Bool , if x then true else y ) }>.

Semantics

Values

Our values are essentially the same, although we will use the new version of lambda's that have been decorated with types.

Inductive value : tm -> Prop :=
  | v_abs : forall x T2 t1,
      value <{\x :T2 , t1 }> (* this case changed *)
  | v_true :
      value <{true }>
  | v_false :
    value <{false }>.
Hint Constructors value : core.

Capture-avoid Substitution

Nothing changes about substitution.
Thus we should expect beta-reduction to stay the same.

Reserved Notation "'[' x ':=' s ']' t" (in custom stlc at level 20, x constr).
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
  match t with
  | tm_var y =>
      if eqb_string x y then s else t
  | <{\y:T, t1}> =>
      if eqb_string x y then t else <{\y:T, [x :=s ] t1}>
  | <{t1 t2}> =>
      <{([x :=s ] t1) ([x :=s ] t2)}>
  | <{true }> =>
      <{true }>
  | <{false }> =>
      <{false }>
  | <{if t1 then t2 else t3}> =>
      <{if ([x :=s ] t1) then ([x :=s ] t2) else ([x :=s ] t3)}>
  end

where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).

Call-by-value Semantics

Nothing changes with the semantics.
Intuitively, this makes sense: we shouldn't expect types to change the semantics of our programs.
In other words, types are a *static* construct as opposed to a *dynamic* construct.

(*
  Note that the type is ignored by the semantics!

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

       t1 --> t1'
  -------------------- ST_App1
    t1' t2 --> t1 t2

    value t1   t2 --> t2'
  ------------------------ ST_App2
      v1 t2 --> v1 t2

  ------------------------ ST_IfTrue
    if true t1 t2 --> t1

  ------------------------ ST_IfFalse
   if false t1 t2 --> t2

              t1 --> t1'
  ------------------------------ ST_If
   if t1 t2 t3 --> if t1' t2 t3

*)

Reserved Notation "t '-->' t'" (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T2 t1 v2,
    value v2 ->
    <{(\x :T2 , t1 ) v2 }> --> <{ [x :=v2 ]t1 }>
| ST_App1 : forall t1 t1' t2,
    t1 --> t1' ->
    <{t1 t2 }> --> <{t1' t2 }>
| ST_App2 : forall v1 t2 t2',
    value v1 ->
    t2 --> t2' ->
    <{v1 t2 }> --> <{v1 t2'}>
| ST_IfTrue : forall t1 t2,
    <{if true then t1 else t2 }> --> t1
| ST_IfFalse : forall t1 t2,
    <{if false then t1 else t2 }> --> t2
| ST_If : forall t1 t1' t2 t3,
    t1 --> t1' ->
    <{if t1 then t2 else t3 }> --> <{if t1' then t2 else t3 }>

where "t '-->' t'" := (step t t').
Hint Constructors step : core.

Multi-step reduction

Notation multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).

Examples

Lemma step1 :
  <{ (\x : Bool , x ) true }> -->* <{ true }>.
Proof.
  eapply multi_step.
  + apply ST_AppAbs.
    apply v_true.
  + simpl.
    apply multi_refl.
Qed.

<{ true }> is a value.
So this term intutively has a good reduction sequence.

Lemma step2 :
  <{ (\x : Bool , (f (g x ))) true }> -->* <{ f (g true ) }>.
Proof.
  eapply multi_step.
  + apply ST_AppAbs.
    apply v_true.
  + simpl.
    apply multi_refl.
Qed.

<{ f (g true) }> is not a value and cannot be reduced anymore.
So this term intutively has a bad reduction sequence.

Lemma step3 :
  <{ (\x : Bool , \y : Bool -> Bool , x ) (\x : Bool -> Bool , x ) false }> -->*
  <{(\x : Bool -> Bool , x ) }>.
Proof.
  eapply multi_step.
  + apply ST_App1.
    apply ST_AppAbs.
    apply v_abs.
  + simpl.
    eapply multi_step.
    * apply ST_AppAbs.
      apply v_false.
    * simpl.
      apply multi_refl.
Qed.

This term could be reduced to a value.
But intuitively the types are off because we are passing in (\x: Bool -> Bool) for a Bool and false for a Bool -> Bool.
We will see that a *type-system* will reject these terms even though the reduction is ok.

Lemma step4 :
  <{ and (not true ) (not false ) }> -->* <{ false }>.
Proof.
  unfold and, not.
  eapply multi_step. {
    apply ST_App1.
    apply ST_App2.
    apply v_abs.
    apply ST_AppAbs.
    apply v_true.
  } {
    simpl.
    eapply multi_step. {
      apply ST_App1.
      apply ST_App2.
      apply v_abs.
      apply ST_IfTrue.
    } {
      eapply multi_step. {
        apply ST_App1.
        apply ST_AppAbs.
        apply v_false.
      } {
        simpl.
        eapply multi_step. {
          apply ST_App2.
          apply v_abs.
          apply ST_AppAbs.
          apply v_false.
        } {
          simpl.
          eapply multi_step. {
            apply ST_App2.
            apply v_abs.
            apply ST_IfFalse.
          } {
            eapply multi_step. {
              apply ST_AppAbs.
              apply v_true.
            } {
              simpl.
              eapply multi_step.
              + apply ST_IfFalse.
              + apply multi_refl.
            }
          }
        }
      }
    }
  }
Qed.

Exercise

Try drawing the proof tree corresponding to the reduction sequence above.
Imagine what the reduction sequence would look like with Church encodings!

Typing Relation

We will now formalize a typing relation which will accept "good terms", i.e., those with "good" reduction sequences and reject "bad" terms, i.e., those with "bad" reduction sequences.
As the examples hint at, we will reject some terms that have "good" reduction sequences.
Similar to how we needed to define substitution for the operational semantics, we first need to define a *context* that will help us interpret the types of lambda bindings.

Context

A context is a partial map from variables to types. This means that we are not required to assign every variable to a type.
You may sometimes see a context can be presented as an associative list.
It is typically given the name Γ (Gamma).

Print partial_map.
Print total_map.
Definition context := partial_map ty.

Typing Judgement

The typing judgement is notated Γ ⊢ t : T where

Γ is a context
the turnstyle ⊢ is common notation for "proves"
t is a term
T is a Type

The typing judgement Γ ⊢ t : T can be read: The term t can be shown to have type T under context Γ.

Reserved Notation "Gamma '⊢' t '\in' T"
(at level 101,
t custom stlc, T custom stlc at level 0).

Typing Rules

(*
     The type of a variable is what the context says it is.

         Γ(x) = Some T
     --------------------- T_Var
           Γ ⊢ x : T

     If under the context with x mapped to T2, t1 can be shown to have type T1,
     then the abstraction \x: T2, t1 has type T2 -> T1. Note that t1 is a term
     that may have x free.

              Γ, x: T2 ⊢ t1 : T1
     --------------------------------- T_Abs
          Γ ⊢ \x: T2, t1 : T2 -> T1

     We require the abstraction's parameter type and the argument's type to match.

           Γ ⊢ t1 : T2 -> T1    Γ ⊢ t2: T2
     ----------------------------------------- T_App
                  Γ ⊢ t1 t2 : T1

     ----------------------- T_True
          Γ ⊢ true : Bool

     ------------------------ T_False
          Γ ⊢ false : Bool


     We require each branch to have the same type.

        Γ ⊢ t1 : Bool       Γ ⊢ t2 : T1        Γ ⊢ t3 : T1
     -------------------------------------------------------- T_If
                     Γ ⊢ if t1 t2 t3 : T1

*)

Inductive has_type : context -> tm -> ty -> Prop :=
  | T_Var : forall Gamma x T1,
      Gamma x = Some T1 ->
      Gamma ⊢ x \in T1
  | T_Abs : forall Gamma x T1 T2 t1,
      x |-> T2 ; Gamma ⊢ t1 \in T1 ->
      Gamma ⊢ \x :T2 , t1 \in (T2 -> T1 )
  | T_App : forall T1 T2 Gamma t1 t2,
      Gamma ⊢ t1 \in (T2 -> T1 ) ->
      Gamma ⊢ t2 \in T2 ->
      Gamma ⊢ t1 t2 \in T1
  | T_True : forall Gamma,
       Gamma ⊢ true \in Bool
  | T_False : forall Gamma,
       Gamma ⊢ false \in Bool
  | T_If : forall t1 t2 t3 T1 Gamma,
       Gamma ⊢ t1 \in Bool ->
       Gamma ⊢ t2 \in T1 ->
       Gamma ⊢ t3 \in T1 ->
       Gamma ⊢ if t1 then t2 else t3 \in T1

where "Gamma '⊢' t '\in' T" := (has_type Gamma t T).

Hint Constructors has_type : core.

Example 1

(*

            --------------------- T_Var
              x: Bool ⊢ x : Bool
      ------------------------------------ T_Abs
       empty ⊢ \x:Bool, x : (Bool -> Bool)

*)

Example typing_example_1 :
  empty ⊢ \x :Bool , x \in (Bool -> Bool ).
Proof.
  apply T_Abs.
  apply T_Var.
  reflexivity.
Qed.

Example 2

(*

                                          --------------------- T_Var  ------------- T_Var
                                           Γ ⊢ y : Bool -> Bool         Γ ⊢ x : Bool
        --------------------- T_Var  ------------------------------------------------ T_App
            Γ ⊢ y : Bool -> Bool          Γ ⊢ y x : Bool
------------------------------------------------------------------------------------- T_App
                     Γ = x: Bool, y: Bool -> Bool ⊢ y (y x) : Bool
        ------------------------------------------------------------------ T_Abs
           x: Bool ⊢ \y:Bool -> Bool, (y (y x) : (Bool -> Bool) -> Bool
--------------------------------------------------------------------------------- T_Abs
  empty ⊢ \x:Bool, \y:Bool -> Bool, (y (y x)) : (Bool -> (Bool -> Bool) -> Bool)

*)

Example typing_example_2 :
  empty ⊢
    \x :Bool ,
       \y :Bool -> Bool ,
          (y (y x )) \in
    (Bool -> (Bool -> Bool ) -> Bool ).
Proof.
  apply T_Abs.
  apply T_Abs.
  eapply T_App.
  + apply T_Var.
    apply update_eq.
  + eapply T_App.
    * apply T_Var.
      apply update_eq.
    * apply T_Var.
      apply update_neq.
      intros Contra.
      discriminate.
Qed.

Not Complete 1

(*

-------------------------------------------- ??
empty ⊢ if true (\x: Bool, x) true : ?

*)

Not Complete 2

(*

---------------------------------------------------------- ??
empty ⊢ if true (\x: Bool, x) (true (\x: Bool, x)) : ?

*)

Type Soundness

We will now prove a type-soundness result.
In words, a well-typed term does not get stuck.
well-typed means that a term can be assigned a type according to the typing relation.
not stuck means that every term reduces to a value with the appropriate type.
The proof proceeds in two major steps: progress and preservation.
The basic idea of *progress* is that either we have reached a value (no more computation) or we can take a step.
The basic idea of preservation is that taking a step does not change the type of a term.
By interweaving progress and preservation, we will get that we eventually hit a value of the appropriate type.
This leads us to a few canonical forms lemmas.

Lemma canonical_forms_bool : forall 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 : forall t T1 T2,
  empty ⊢ t \in (T2 -> T1 ) ->
  value t ->
  exists x u , t = <{\x :T2 , u }>.
Proof.
  intros t T1 T2 HT HVal.
  destruct HVal; inversion HT; subst.
  exists x0, t1.
  reflexivity.
Qed.

Progress

Proving Progress

We prove progress now.
We have two inductive relations that we can induct on.
Either the derivation of the typing judgement or the term.
It turns out in this case it is possible to induct on either terms or the typing judgement.

Theorem progress : forall t T,
  empty ⊢ t \in T ->
  value t \/ exists t', t --> t'.
Proof.
  (*
     We proceed by induction on the typing derivation Γ ⊢ t : T.
   *)
  intros t T Ht.
  remember empty as Gamma.
  induction Ht.

  {
    (*
       Case

        empty(x) = Some T
     --------------------- T_Var
         empty ⊢ x : T

       We show that this case is impossible.
       In particular, observe that we have that empty(x) = Some T which is impossible.
     *)
    subst Gamma.
    inversion H.
  }
  {
    (*
       Case

           empty, x: T2 ⊢ t1 : T1
     --------------------------------- T_Abs
       empty ⊢ \x: T2, t1 : T2 -> T1

       We have to show that either value (\x: T2, t1) or exists t', \x: T2, t1 --> t'.
       We choose to show that value (\x: T2, t1).
       This follows because we can derive value (\x: T2, t1) with v_abs.
     *)
    subst Gamma.
    left.
    apply v_abs.
  }
  { (*
       Case

       empty ⊢ t1 : T2 -> T1   empty ⊢ t2: T2
     ----------------------------------------- T_App
                empty ⊢ t1 t2 : T1

       We have to show that either value (t1 t2) or exists t', t1 t2 --> t'.
       We choose to show that exists t', t1 t2 --> t' (it's definitely not a value).
       We have two inductive hypotheses.

       IHHt1: empty = empty -> (value t1 \/ (exists t' : tm, t1 --> t'))
       IHHt2: empty = empty -> (value t2 \/ (exists t' : tm, t2 --> t'))

       Clearly, empty = empty, so our inductive hypotheses simplify to

       IHHt1: value t1 \/ (exists t' : tm, t1 --> t')
       IHHt2: value t2 \/ (exists t' : tm, t2 --> t')

        *)
    right.

    assert (Gamma = Gamma) as HTriv by reflexivity.
    subst Gamma.
    specialize (IHHt1 HTriv).
    specialize (IHHt2 HTriv).
    clear HTriv.

    (*
       We proceed by case analysis on IHHt1.
     *)
    destruct IHHt1.
    {
      (*
         Case value t1:

           We proceed by case analysis on IHHt2.

           Case value t2:
             Recall that we have to show that exists t', t1 t2 --> t'.

             We have that empty ⊢ t1 \in (T2 -> T1) from the induction on the
             typing derivation.
             We also have that t1 = \x: T2, t0 by canoncial forms of arrow
             types for some variable x and term t0.

             Thus we have to show that exists t', (\x: T2, t0) t2 --> t'.
             We claim that t' = x:=t2 t0.
             Thus we have to show that (\x: T2, t0) t2 --> x:=t2 t0.
             This is the rule for ST_AppAbs where we use that value t2.

           Case exists t' : tm, t2 --> t':
             Recall that we have to show that exists t', t1 t2 --> t'.

             We have that t2 --> t2' for some t2' by assumption.
             We claim that t' = t1 t2'.
             Thus we have to show that t1 t2 --> t1 t2'.
             This is the rule for ST_App2.
       *)
      destruct IHHt2.
      + eapply canonical_forms_fun in Ht1; auto.
        destruct Ht1 as [x [t0 H1]]; subst.
        exists (<{ [x:=t2] t0 }>).
        apply ST_AppAbs.
        assumption.
      + destruct H0 as [t2' Hstp].
        exists (<{t1 t2'}>).
        apply ST_App2.
        assumption.
        assumption.
    }
    {
      (*
         Case exists t' : tm, t1 --> t':

           Recall that we have to show that exists t', t1 t2 --> t'.
           We have that t1 --> t1' for some t1' by assumption.
           We claim that t' = t1' t2.
           Thus we have to show that t1' t2 --> t1 t2.
           This is exactly the rule for ST_App1.
       *)
      destruct H as [t1' Hstp].
      exists (<{t1' t2}>).
      apply ST_App1.
      assumption.
    }
  }
  {
    (*
       Case

     ----------------------- T_True
        empty ⊢ true : Bool

      We have to show that either value true or exists t', true --> t'.
      We choose to show that value true.
      This can be constructed with an application of v_true.
     *)
    left.
    apply v_true.
  }
  {
    (*
       Case

     ----------------------- T_False
       empty ⊢ false : Bool

      We have to show that either value false or exists t', false --> t'.
      We choose to show that value false.
      This can be constructed with an application of v_false.
     *)

    left.
    apply v_false.
  }
  {
    (*
       Case

        empty ⊢ t1 : Bool   empty ⊢ t2 : T1  empty ⊢ t3 : T1
     -------------------------------------------------------- T_If
                     empty ⊢ if t1 t2 t3 : T1

       We have to show that either value (if t1 t2 t3) or exists t', if t1 t2 t3 --> t'.
       We choose to show that exists t', if t1 t2 t3 --> t' (it's definitely not a value).
       We have three inductive hypotheses.

       IHHt1: empty = empty -> (value t1 \/ (exists t' : tm, t1 --> t'))
       IHHt2: empty = empty -> (value t2 \/ (exists t' : tm, t2 --> t'))
       IHHt3: empty = empty -> (value t3 \/ (exists t' : tm, t3 --> t'))

       Clearly, empty = empty, so our inductive hypotheses simplify to

       IHHt1: value t1 \/ (exists t' : tm, t1 --> t')
       IHHt2: value t2 \/ (exists t' : tm, t2 --> t')
       IHHt3: value t3 \/ (exists t' : tm, t3 --> t')

     *)

    right.

    assert (Gamma = Gamma) as HTriv by reflexivity.
    subst Gamma.
    specialize (IHHt1 HTriv).
    specialize (IHHt2 HTriv).
    specialize (IHHt3 HTriv).
    clear HTriv.

    (*
       We proceed by case analysis on IHHt1.
     *)
    destruct IHHt1.
    {
      (*
         Case value t1:

           We have that empty ⊢ t1 : Bool from our induction on the typing derivation.
           Thus t1 = true or t1 = false by canonical forms on booleans.
           We proceed by case analysis.
       *)

      assert (t1 = <{true }> \/ t1 = <{false }>) as HTorF. {
        apply canonical_forms_bool.
        assumption.
        assumption.
      }
      destruct HTorF; subst.
      + (*
           Case t1 = true:
             Recall that we have to show that exists t', if t1 t2 t3 --> t'.
             We claim that t1' = t2.
             We have that if true t2 t3 --> t2 by ST_IfTrue.
         *)
        exists t2.
        apply ST_IfTrue.
      + (*
           Case t1 = false:
             Recall that we have to show that exists t', if t1 t2 t3 --> t'.
             We claim that t1' = t2.
             We have that if true t2 t3 --> t2 by ST_IfTrue.
         *)
        exists t3.
        apply ST_IfFalse.
    }
    {
      (*
         Case exists t' : tm, t1 --> t':

         We have that t1 --> t1' for some t1' by assumption.
         Recall that we have to show that exists t', if t1 t2 t3 --> t'.
         We claim that t' = if t1' t2 t3.
         We have that if t1 t2 t3 --> if t1' t2 t3 by ST_If.
       *)
      destruct H as [t1' Hstp].
      exists <{if t1' then t2 else t3}>.
      apply ST_If.
      assumption.
    }
  }
Qed.

Preservation

Non-empty contexts

You may have noticed that the proof of progress assumed an empty context.
The proof of preservation will require us to work with non-empty contexts.
We need a few extra lemmas on contexts.
First, let's start with a theorem that illustrates more the idea of inducting on typing derivations but with non-empty contexts.

Theorem unique_types : forall Gamma e T T',
  Gamma ⊢ e \in T ->
  Gamma ⊢ e \in T' ->
  T = T'.
Proof.
  intros Gamma e T T' H.
  generalize dependent T'.

  (*
     By induction on the typing derivation Γ ⊢ t : T.
   *)

  induction H; intros T' H'.
  {
    (*
       Case

          Γ(x) = Some T
     --------------------- T_Var
            Γ ⊢ x : T

       We have to show that T = T'.
       By inversion on Γ ⊢ x : T', we have that Γ(x) = T'.
       Since Γ(x) = T as well, we have that T = T'.
     *)
    inversion H'; subst.
    rewrite H2 in H.
    inversion H.
    reflexivity.
  }
  {
    (*
       Case

             Γ, x: T2 ⊢ t1 : T1
     --------------------------------- T_Abs
         Γ ⊢ \x: T2, t1 : T2 -> T1

       We have to show that T2' -> T1' = T2 -> T1 whenever Γ ⊢ \x: T2', t1 : T2' -> T1'
       By inversion on Γ ⊢ \x: T2', t1 : T2' -> T1', we have that
       Γ, x: T2' ⊢ t1 : T2' -> T1'.
       Moreover, by our inductive hypothesis, we obtain that T2' -> T1' = T2 -> T1,
       which is what we wanted to show.
     *)
    inversion H'; subst.
    apply IHhas_type in H5.
    subst.
    reflexivity.
  }
  {
    (*
       Case

           Γ ⊢ t1 : T2 -> T1   Γ ⊢ t2: T2
     ----------------------------------------- T_App
                  Γ ⊢ t1 t2 : T1

       We have to show that T1 = T1' if Γ ⊢ t1 t2: T1'.
       By inversion on Γ ⊢ t1 t2: T1', we have that
       Γ ⊢ t2: T2' and Γ ⊢ t1: T2' -> T1'.
       By our inductive hypothesis, we have that T2' -> T1' = T2 -> T1.
       Thus the result follows.

     *)
    inversion H'; subst.
    apply IHhas_type1 in H4.
    inversion H4; subst.
    reflexivity.
  }
  {
    (*
       Case

     ----------------------- T_True
          Γ ⊢ true : Bool

       By inversion on Γ ⊢ true : Bool, we have that Bool = Bool.

     *)
    inversion H'; subst.
    reflexivity.
  }
  {
     (*
       Case

     ----------------------- T_False
          Γ ⊢ false : Bool

       By inversion on Γ ⊢ false : Bool, we have that Bool = Bool.

     *)

    inversion H'; subst.
    reflexivity.
  }
  {
    inversion H'; subst.
    apply IHhas_type2 in H8.
    assumption.
  }
Qed.

Print inclusion.

Lemma weakening : forall 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'.

  (*
     By induction on the typing derivation Γ ⊢ t : T.
   *)
  induction Ht; intros.
  {
    (*
       Case

          Γ(x) = Some T
     --------------------- T_Var
            Γ ⊢ x : T

       We have to show that Γ' ⊢ x : T.
       It suffices to show that Γ'(x) = T by T_Var.
       By assumption, we have that Γ ⊢ x : T and Γ' extends Γ.
       By inversion on Γ ⊢ x : T, we have that Γ(x) = T.
       Since Γ' extends Γ, we clearly have Γ'(x) = T as well.
     *)
    apply T_Var.
    unfold inclusion in H0.
    auto.
  }
  {
    (*
       Case

             Γ, x: T2 ⊢ t1 : T1
     --------------------------------- T_Abs
         Γ ⊢ \x: T2, t1 : T2 -> T1

       We have to show that Γ' ⊢ \x: T2, t1: T2 -> T1.
       It suffices to show that Γ', x: T2 ⊢ t1 : T1 by T_Abs.

       Our inductive hypothesis states:

       inclusion Γ Γ' and Γ, x: T2 ⊢ t1 : T1 implies that Γ', x: T2 ⊢ t1 : T1.

       Thus it suffices to show that inclusion (Γ, x: T2) (Γ', x: T2) and
       Γ, x: T2 ⊢ t1 : T1 by our inductive hypothesis.
       The first requirement follows by inclusion_update.
       The second requirement follows by assumption.
     *)
    apply T_Abs.
    apply IHHt.
    apply inclusion_update.
    assumption.
  }
  {
    (*
       Case

           Γ ⊢ t1 : T2 -> T1   Γ ⊢ t2: T2
     ----------------------------------------- T_App
                  Γ ⊢ t1 t2 : T1

       We have to show that Γ' ⊢ t1 t2: T1.
       It suffices to show that Γ' ⊢ t1 : T2 -> T1 and Γ' ⊢ t2: T1 by T_App.

       We have two inductive hypotheses:
       IHHt1: inclusion Γ Γ' and Γ ⊢ t1 : T2 -> T1 implies that Γ' ⊢ t1 : T2 -> T1.
       IHHt2: inclusion Γ Γ' and Γ ⊢ t2 : T2 implies that Γ' ⊢ t2 : T2.

       We have Γ' ⊢ t1 : T2 -> T1 by IHHt1 and assumption that Γ' extends Γ.
       We have Γ' ⊢ t2 : T2 by IHHt2 and assumption that Γ' extends Γ.

     *)
    eapply T_App.
    + eapply IHHt1.
      assumption.
    + eapply IHHt2.
      assumption.
  }
  {
    (*
       Case

     ----------------------- T_True
          Γ ⊢ true : Bool

       The rule T_True can be applied in any context.

     *)
    apply T_True.
  }
  {
    (*
       Case

     ----------------------- T_False
          Γ ⊢ false : Bool

       The rule T_False can be applied in any context.

     *)
    apply T_False.
  }
  {
    (*
       Case

          Γ ⊢ t1 : Bool     Γ ⊢ t2 : T1      Γ ⊢ t3 : T1
     -------------------------------------------------------- T_If
                     Γ ⊢ if t1 t2 t3 : T1

       We have to show that Γ' ⊢ if t1 t2 t3: T1.
       It suffices to show that Γ' ⊢ t1 : Bool, Γ' ⊢ t2: T1, and Γ' ⊢ t3: T1 by T_If.

       We have three inductive hypotheses:
       IHHt1: inclusion Γ Γ' and Γ ⊢ t1 : Bool implies that Γ' ⊢ t1 : Bool.
       IHHt2: inclusion Γ Γ' and Γ ⊢ t2 : T1 implies that Γ' ⊢ t2 : T1.
       IHHt3: inclusion Γ Γ' and Γ ⊢ t3 : T1 implies that Γ' ⊢ t2 : T1.

       We have Γ' ⊢ t1 : Bool by IHHt1 and assumption that Γ' extends Γ.
       We have Γ' ⊢ t2 : T1 by IHHt2 and assumption that Γ' extends Γ.
       We have Γ' ⊢ t3 : T1 by IHHt3 and assumption that Γ' extends Γ.

     *)
    eapply T_If.
    + eapply IHHt1.
      assumption.
    + eapply IHHt2.
      assumption.
    + eapply IHHt3.
      assumption.
  }
Qed.

Here's a simple consequence of weakening.

Corollary weakening_empty : forall Gamma t T,
  empty ⊢ t \in T ->
  Gamma ⊢ t \in T.
Proof.
  intros Gamma t T.
  eapply weakening.
  discriminate.
Qed.

Substitution and Typing

The main lemma we need is that substituting terms preserves types.
Note that the term t has type T in any context
However, the value that we are substituting must be a closed term, i.e., typeable under the empty context.

Lemma substitution_preserves_typing : forall Gamma x U t v T,
  x |-> U ; Gamma ⊢ t \in T ->
  empty ⊢ v \in U ->
  Gamma ⊢ [x :=v ]t \in T.
Proof.
  intros Gamma x U t v T Ht Hv.
  generalize dependent Gamma.
  generalize dependent T.

  (*
     We proceed by induction on terms t.
   *)
  induction t.
  {
    (*
       Case t = y:

       We have that Γ, x: U(y) = Some T by inversion on Γ, x: U ⊢ y: T.

       We have to show that Γ ⊢ (x := v y): T.
       We proceed by case analysis on whether x == y or not.

     *)
    intros T Gamma H; inversion H; clear H; subst; simpl.
    rename s into y.
    destruct (eqb_stringP x y); subst.
    + (*
          Case x=y

            We have that Γ, y: U(y) = Some T so that U = T.
            From induction on terms we have that empty ⊢ v : U.
            Thus the result follows by weakining.
       *)
      rewrite update_eq in H2.
      injection H2 as H2; subst.
      apply weakening_empty.
      assumption.
    + (*
         Case x<>y

            We have to show that Γ, y: U(y) = Some T when x <> y.
            This follows by T_Var and properties of updating a context.
       *)
      apply T_Var.
      rewrite update_neq in H2; auto.
  }
  {
    (*
       Case t = t1 t2:

       We have to show that Γ ⊢ (x := v t1) (x := v t2) \in T.

       It suffices to show that
       1) Γ ⊢ (x := v t1) \in T2 -> T
       2) Γ ⊢ (x := v t2) \in T2
       by T_App.

       We have that
       H1:  x |-> U; Gamma ⊢ t1 \in (T2 -> T)
       H2:  x |-> U; Gamma ⊢ t2 \in T2
       by inversion on x |-> U ; Gamma ⊢ t1 t2 \in T1.

       We have two induction hypotheses
       IHt1: (x |-> U;  Γ ⊢ t1 \in T)  ->  Γ ⊢ x := v t1 \in T for any T
       IHt2: (x |-> U;  Γ ⊢ t2 \in T)  ->  Γ ⊢ x := v t2 \in T for any T

       We have that Γ ⊢ x := v t1 \in T2 -> T by IHt1 and H1.
       We have that Γ ⊢ x := v t1 \in T2 by IHt2 and H2.

     *)
    intros T Gamma H; inversion H; clear H; subst; simpl.
    eapply T_App.
    + eapply IHt1.
      eapply H3.
    + eapply IHt2.
      assumption.
  }
  {
    (*
       Case t = \y: T2, t0 : T2 -> T1:

       We have to show that Γ ⊢ (x := v \y: T2, t0) : T2 -> T1.

       We have that
       H1:  Gamma, x: U, y: T2 ⊢ t0 : T1
       by inversion on Gamma, x: U ⊢ \y: T2, t0 : T2 -> T1.

       It suffices to show that
       Γ, y: T2  ⊢ if x == y then (\y: T2, to) else (x := v t0) : T2 -> T1
       by T_Abs.
     *)
    intros T Gamma H; inversion H; clear H; subst; simpl.
    rename s into y, t into S.

    (*
       We proceed by case analysis on x == y.
     *)
    destruct (eqb_stringP x y); subst; apply T_Abs.
    + (*
         Case x=y

           y shadows x and therefore has the appropriate type.
       *)
      rewrite update_shadow in H5.
      assumption.
    +

Case x<>y:

We have one inductive hypothesis IHt1: (Γ, x: U ⊢ t1: T) -> Γ ⊢ x := v t0: T for any T

The result follows by the induction hypothesis and permutation of the context.

      apply IHt.
      rewrite update_permute; auto.
  }
  {
    (*
       Case t = true:

       T_True can be applied in any context.

     *)
    intros T Gamma H; inversion H; clear H; subst; simpl.
    apply T_True.
  }
  {
    (*
       Case t = false:

       Similar to case t = true.

     *)
    intros T Gamma H; inversion H; clear H; subst; simpl.
    apply T_False.
  }
  {
    (*
       Case t = if t1 t2 t3

       Similar to case t = t1 t2.
     *)
    intros T Gamma H; inversion H; clear H; subst; simpl.
    apply T_If.
    + apply IHt1.
      assumption.
    + apply IHt2.
      assumption.
    + apply IHt3.
      assumption.
  }
Qed.

Finally the proof of preservation.

Theorem preservation : forall 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.

By induction on the typing derivation.

  induction HT;
       intros t' HE; subst;
       try solve [inversion HE; subst; auto].
  - (* T_App *)
    inversion HE; subst; eauto.
    (* Most of the cases are immediate by induction,
       and eauto takes care of them *)
    + (* ST_AppAbs *)
      apply substitution_preserves_typing with T2.
      inversion HT1; subst.
      assumption.
      assumption.
Qed.

Type-Soundness: Putting It Together

We can now formalize the statement that well-typed terms do not get stuck.
First recall the definition of normal forms.

Definition normal_form {X : Type} (R : relation X) (t : X) : Prop :=
~ exists t', R t t'.

A term is stuck if there is no reduction it can take and it is not a value (which syntactically indicates that there is no more computation left to be done).
Thus this notionof stuck does not assume that normal forms and values coincide.

Definition stuck (t:tm) : Prop :=
  (normal_form step) t /\ ~ value t.

Corollary type_soundness : forall t t' T,
  empty ⊢ t \in T ->
  t -->* t' ->
  ~(stuck t').
Proof.
  intros t t' T Hhas_type Hmulti.
  unfold stuck.
  intros [Hnf Hnot_val].
  unfold normal_form in Hnf.

  (*
     By induction on multi-step relation.
   *)
  induction Hmulti.
  {
    (*
       Case

        ---------------- multi_refl
            t -->* t

       We have to show that t is not stuck.
       By progress, we have that either t is a value or or it has a step.
       Thus this case is proven.
     *)
    apply progress in Hhas_type.
    destruct Hhas_type; auto.
  }
  {
    (*
       Case

          t --> t1      t1 -->* t'
        --------------------------- multi_step
                t -->* t'

        We have to show that t' is not stuck.
        Our inductive hypothesis is:
        empty ⊢ t' : T and t1 -->* t' implies that t' is not stuck.

        Thus it suffices to show that empty ⊢ t' : T.
        This holds by preservation provided we can show that t --> t1 which
        we have in this case of the induction.
     *)
    apply IHHmulti; auto.
    eapply preservation in Hhas_type.
    eapply Hhas_type.
    apply H.
  }
Qed.

Recursion

STLC has many nice properties.
At this point, we may wonder if we lost expressive power?
As it turns out, we will no longer be able to write recursive terms.

Can you type the Y-Combinator?

(*

(\f, (\x, f (x x)) (\x, f (x x))

(\f: ?T, (\x: ?S, f (x x)) (\x: ?U, f (x x))
*)

Let's look at (\x: ?S, f (x x)
We have that x has type ?S
Moreover x is applied to itself.
By application, we know that ?S = ?S2 -> ?S1 and ?S = ?S2.
In other words, we have that ?S2 -> ?S1 = ?S2.
This only has trivial solutions.
Thus we cannot type the Y-combinator

Syntax

(*
    t ::= ...
        | fix t
*)

Values

Nothing changes

Operational Semantics

(*

   same operational rules and ...


  ---------------------------------------------- ST_fix
    fix (\x: T, t) --> x := fix (\x: T, t) t

*)

Typing Rules

(*

   same typing rules and ...

    Γ ⊢ t : T -> T
  ------------------ T_fix
    Γ ⊢ fix t : T

*)

Example 1: Factorial

(*

Γ ⊢ (\f: nat -> nat, \n: nat, if n == 0 then 0 else f (n-1)) : (nat -> nat) -> (nat -> nat)
-------------------------------------------------------------------------------------- T_fix
Γ ⊢ fix (\f: nat -> nat, \n: nat, if n == 0 then 0 else f (n-1)) : nat -> nat

*)

Example 2: Non-termination

(*

     Γ ⊢ (\f: nat -> nat, \n: nat, f n) : (nat -> nat) -> (nat -> nat)
  ----------------------------------------------------------------------- T_fix
          Γ ⊢ fix (\f: nat -> nat, \n: nat, f n) : nat -> nat

*)

Goal for today

We saw the simply-typed Lambda Calculus (STLC) and it's type-system.
We proved type-soundness via progress and preservation.
We saw that STLC could not express recursion, and hence, is not Turing complete.