StlcPropProperties of STLC
In this chapter, we develop the fundamental theory of the Simply
Typed Lambda Calculus — in particular, the type safety
theorem.
Progress
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 = 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)...
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 = 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)...
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
- 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 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,
y ≠ x →
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) :=
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 T11 *)
unfold extend. destruct (eq_id_dec x0 x1)...
Case "T_App".
apply T_App with T11...
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 T11 *)
unfold extend. destruct (eq_id_dec x0 x1)...
Case "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.
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 ⊢ 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 T11...
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 T11...
inversion HT1...
Qed.
End STLCProp.