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
*)
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
Lemma canonical_forms_bool : ∀ t,
empty ⊢ t \in Bool →
value t →
(t = <{true}>) ∨ (t = <{false}>).
Lemma canonical_forms_fun : ∀ t T1 T2,
empty ⊢ t \in (T1 → T2) →
value t →
∃ x u, t = <{\x:T1, u}>.
empty ⊢ t \in Bool →
value t →
(t = <{true}>) ∨ (t = <{false}>).
Proof.
intros t HT HVal.
destruct HVal; auto.
inversion HT.
Qed.
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.
intros t T1 T2 HT HVal.
destruct HVal; inversion HT; subst.
∃ x0, t1. reflexivity.
Qed.
Theorem progress : ∀ t T,
empty ⊢ t \in T →
value t ∨ ∃ t', 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.
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
- The preservation theorem is proved by induction on a typing
derivation, pretty much as we did in the Types chapter.
- substitution lemma, stating that substituting a (closed,
well-typed) term s for a variable x in a term t
preserves the type of t.
- weakening lemma, showing that typing is preserved under "extensions" to the context Gamma.
The Weakening Lemma
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.
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.
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.
- 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.
x ⊢> U ; Gamma ⊢ t \in T →
empty ⊢ v \in U →
Gamma ⊢ [x:=v]t \in T.
Main Theorem
Theorem preservation : ∀ t t' T,
empty ⊢ t \in T →
t --> t' →
empty ⊢ t' \in 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.
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.