# StlcPropProperties of STLC

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

# Progress

*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 ⊢ t ∈ T →

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 = t

value or steps... *)

right. destruct IHHt1...

SCase "t

destruct IHHt2...

SSCase "t

(* Since t

must be an abs. Sometimes this is proved separately

and called a "canonical forms" lemma. *)

inversion H; subst. ∃([x0:=t

solve by inversion. solve by inversion.

SSCase "t

inversion H0 as [t

SCase "t

inversion H as [t

Case "T_If".

right. destruct IHHt1...

SCase "t

(* Since t

be true or false *)

inversion H; subst. solve by inversion.

SSCase "t

SSCase "t

SCase "t

inversion H as [t

Qed.

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 = t

_{1}t_{2}. Proceed by cases on whether t_{1}is avalue or steps... *)

right. destruct IHHt1...

SCase "t

_{1}is a value".destruct IHHt2...

SSCase "t

_{2}is also a value".(* Since t

_{1}is a value and has an arrow type, itmust be an abs. Sometimes this is proved separately

and called a "canonical forms" lemma. *)

inversion H; subst. ∃([x0:=t

_{2}]t)...solve by inversion. solve by inversion.

SSCase "t

_{2}steps".inversion H0 as [t

_{2}' Hstp]. ∃(tapp t_{1}t_{2}')...SCase "t

_{1}steps".inversion H as [t

_{1}' Hstp]. ∃(tapp t_{1}' t_{2})...Case "T_If".

right. destruct IHHt1...

SCase "t

_{1}is a value".(* Since t

_{1}is a value of boolean type, it mustbe true or false *)

inversion H; subst. solve by inversion.

SSCase "t

_{1}= true". eauto.SSCase "t

_{1}= false". eauto.SCase "t

_{1}also steps".inversion H as [t

_{1}' Hstp]. ∃(tif t_{1}' t_{2}t_{3})...Qed.

# Preservation

- 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

*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

Inductive appears_free_in : id → tm → Prop :=

| afi_var : ∀x,

appears_free_in x (tvar x)

| afi_app1 : ∀x t

_{1}t

_{2},

appears_free_in x t

_{1}→ appears_free_in x (tapp t

_{1}t

_{2})

| afi_app2 : ∀x t

_{1}t

_{2},

appears_free_in x t

_{2}→ appears_free_in x (tapp t

_{1}t

_{2})

| afi_abs : ∀x y T

_{11}t

_{12},

y ≠ x →

appears_free_in x t

_{12}→

appears_free_in x (tabs y T

_{11}t

_{12})

| afi_if1 : ∀x t

_{1}t

_{2}t

_{3},

appears_free_in x t

_{1}→

appears_free_in x (tif t

_{1}t

_{2}t

_{3})

| afi_if2 : ∀x t

_{1}t

_{2}t

_{3},

appears_free_in x t

_{2}→

appears_free_in x (tif t

_{1}t

_{2}t

_{3})

| afi_if3 : ∀x t

_{1}t

_{2}t

_{3},

appears_free_in x t

_{3}→

appears_free_in x (tif t

_{1}t

_{2}t

_{3}).

Tactic Notation "afi_cases" tactic(first) ident(c) :=

first;

[ 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.

## Substitution

Lemma free_in_context : ∀x t T Γ,

appears_free_in x t →

Γ ⊢ t ∈ T →

∃T', Γ x = Some T'.

Proof.

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.

Qed.

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.

Qed.

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 ⊢ t ∈ T →

closed t.

Proof.

(* 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,

Γ ⊢ t ∈ T →

(∀x, appears_free_in x t → Γ x = Γ' x) →

Γ' ⊢ t ∈ T.

Proof with eauto.

intros.

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 T

unfold extend. destruct (eq_id_dec x0 x1)...

Case "T_App".

apply T_App with T

Qed.

intros.

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 T

_{11}*)unfold extend. destruct (eq_id_dec x0 x1)...

Case "T_App".

apply T_App with T

_{11}...Qed.

Now we come to the conceptual heart of the proof that reduction
preserves types — namely, the observation that
Formally, the so-called

*substitution*preserves types.*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 ⊢ t ∈ T →

empty ⊢ v ∈ U →

Γ ⊢ [x:=v]t ∈ T.

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".

subst.

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...

subst.

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...

Qed.

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".

subst.

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...

subst.

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...

Qed.

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

Theorem preservation : ∀t t' T,

empty ⊢ t ∈ T →

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 T

inversion HT1...

Qed.

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 T

_{11}...inversion HT1...

Qed.

End STLCProp.