StlcPropProperties of STLC
Set Warnings "-notation-overridden,-parsing".
From PLF Require Import Maps.
From PLF Require Import Types.
From PLF Require Import Stlc.
From PLF Require Import Smallstep.
Module STLCProp.
Import STLC.
From PLF Require Import Maps.
From PLF Require Import Types.
From PLF Require Import Stlc.
From PLF Require Import Smallstep.
Module STLCProp.
Import STLC.
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 ∈ Bool →
value t →
(t = tru) ∨ (t = fls).
Lemma canonical_forms_fun : ∀t T_{1} T_{2},
empty ⊢ t ∈ (Arrow T_{1} T_{2}) →
value t →
∃x u, t = abs x T_{1} u.
empty ⊢ t ∈ Bool →
value t →
(t = tru) ∨ (t = fls).
Proof.
intros t HT HVal.
inversion HVal; intros; subst; try inversion HT; auto.
Qed.
intros t HT HVal.
inversion HVal; intros; subst; try inversion HT; auto.
Qed.
Lemma canonical_forms_fun : ∀t T_{1} T_{2},
empty ⊢ t ∈ (Arrow T_{1} T_{2}) →
value t →
∃x u, t = abs x T_{1} u.
Proof.
intros t T_{1} T_{2} HT HVal.
inversion HVal; intros; subst; try inversion HT; subst; auto.
∃x_{0}, t_{0}. auto.
Qed.
intros t T_{1} T_{2} HT HVal.
inversion HVal; intros; subst; try inversion HT; subst; auto.
∃x_{0}, t_{0}. auto.
Qed.
Progress
Theorem progress : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.
Proof: By induction on the derivation of ⊢ t ∈ T.
- The last rule of the derivation cannot be T_Var, since a
variable is never well typed in an empty context.
- The T_Tru, T_Fls, and T_Abs cases are trivial, since in
each of these cases we can see by inspecting the rule that t
is a value.
- If the last rule of the derivation is T_App, then t has the
form t_{1} t_{2} for some t_{1} and t_{2}, where ⊢ t_{1} ∈ T_{2} → T
and ⊢ t_{2} ∈ T_{2} for some type T_{2}. The induction hypothesis
for the first subderivation says that either t_{1} is a value or
else it can take a reduction step.
- If t_{1} is a value, then consider t_{2}, which by the
induction hypothesis for the second subderivation must also
either be a value or take a step.
- Suppose t_{2} is a value. Since t_{1} is a value with an
arrow type, it must be a lambda abstraction; hence t_{1}
t_{2} can take a step by ST_AppAbs.
- Otherwise, t_{2} can take a step, and hence so can t_{1}
t_{2} by ST_App2.
- Suppose t_{2} is a value. Since t_{1} is a value with an
arrow type, it must be a lambda abstraction; hence t_{1}
t_{2} can take a step by ST_AppAbs.
- If t_{1} can take a step, then so can t_{1} t_{2} by ST_App1.
- If t_{1} is a value, then consider t_{2}, which by the
induction hypothesis for the second subderivation must also
either be a value or take a step.
- If the last rule of the derivation is T_Test, then t = test
t_{1} then t_{2} else t_{3}, where t_{1} has type Bool. The first IH
says that t_{1} either is a value or takes a step.
- If t_{1} is a value, then since it has type Bool it must be
either tru or fls. If it is tru, then t steps to
t_{2}; otherwise it steps to t_{3}.
- Otherwise, t_{1} takes a step, and therefore so does t (by ST_Test).
- If t_{1} is a value, then since it has type Bool it must be
either tru or fls. If it is tru, then t steps to
t_{2}; otherwise it steps to t_{3}.
Proof with eauto.
intros t T Ht.
remember (@empty ty) as Gamma.
induction Ht; subst Gamma...
- (* T_Var *)
(* contradictory: variables cannot be typed in an
empty context *)
inversion H.
- (* T_App *)
(* t = t_{1} t_{2}. Proceed by cases on whether t_{1} is a
value or steps... *)
right. destruct IHHt1...
+ (* t_{1} is a value *)
destruct IHHt2...
* (* t_{2} is also a value *)
assert (∃x_{0} t_{0}, t_{1} = abs x_{0} T_{11} t_{0}).
eapply canonical_forms_fun; eauto.
destruct H_{1} as [x_{0} [t_{0} Heq]]. subst.
∃([x_{0}:=t_{2}]t_{0})...
* (* t_{2} steps *)
inversion H_{0} as [t_{2}' Hstp]. ∃(app t_{1} t_{2}')...
+ (* t_{1} steps *)
inversion H as [t_{1}' Hstp]. ∃(app t_{1}' t_{2})...
- (* T_Test *)
right. destruct IHHt1...
+ (* t_{1} is a value *)
destruct (canonical_forms_bool t_{1}); subst; eauto.
+ (* t_{1} also steps *)
inversion H as [t_{1}' Hstp]. ∃(test t_{1}' t_{2} t_{3})...
Qed.
intros t T Ht.
remember (@empty ty) as Gamma.
induction Ht; subst Gamma...
- (* T_Var *)
(* contradictory: variables cannot be typed in an
empty context *)
inversion H.
- (* T_App *)
(* t = t_{1} t_{2}. Proceed by cases on whether t_{1} is a
value or steps... *)
right. destruct IHHt1...
+ (* t_{1} is a value *)
destruct IHHt2...
* (* t_{2} is also a value *)
assert (∃x_{0} t_{0}, t_{1} = abs x_{0} T_{11} t_{0}).
eapply canonical_forms_fun; eauto.
destruct H_{1} as [x_{0} [t_{0} Heq]]. subst.
∃([x_{0}:=t_{2}]t_{0})...
* (* t_{2} steps *)
inversion H_{0} as [t_{2}' Hstp]. ∃(app t_{1} t_{2}')...
+ (* t_{1} steps *)
inversion H as [t_{1}' Hstp]. ∃(app t_{1}' t_{2})...
- (* T_Test *)
right. destruct IHHt1...
+ (* t_{1} is a value *)
destruct (canonical_forms_bool t_{1}); subst; eauto.
+ (* t_{1} also steps *)
inversion H as [t_{1}' Hstp]. ∃(test t_{1}' t_{2} t_{3})...
Qed.
Exercise: 3 stars, advanced (progress_from_term_ind)
Show that progress can also be proved by induction on terms instead of induction on typing derivations.
Theorem progress' : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.
Proof.
intros t.
induction t; intros T Ht; auto.
(* FILL IN HERE *) Admitted.
☐
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.
Proof.
intros t.
induction t; intros T Ht; auto.
(* FILL IN HERE *) Admitted.
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, whose definition 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)
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, we discover
that we need to take a term s that has been shown to be
well-typed in some context Gamma and consider the same term
s in a slightly different context Gamma'. For this we
prove a...
- context invariance lemma, showing that typing is preserved
under "inessential changes" to the context Gamma — in
particular, changes that do not affect any of the free
variables of the term. And finally, for this, we need a
careful definition of...
- the free variables in a term — i.e., variables that are used in the term in positions that are not in the scope of an enclosing function abstraction binding a variable of the same name.
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 : string → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (var x)
| afi_app1 : ∀x t_{1} t_{2},
appears_free_in x t_{1} →
appears_free_in x (app t_{1} t_{2})
| afi_app2 : ∀x t_{1} t_{2},
appears_free_in x t_{2} →
appears_free_in x (app t_{1} t_{2})
| afi_abs : ∀x y T_{11} t_{12},
y ≠ x →
appears_free_in x t_{12} →
appears_free_in x (abs y T_{11} t_{12})
| afi_test1 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x (test t_{1} t_{2} t_{3})
| afi_test2 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x (test t_{1} t_{2} t_{3})
| afi_test3 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x (test t_{1} t_{2} t_{3}).
Hint Constructors appears_free_in.
| afi_var : ∀x,
appears_free_in x (var x)
| afi_app1 : ∀x t_{1} t_{2},
appears_free_in x t_{1} →
appears_free_in x (app t_{1} t_{2})
| afi_app2 : ∀x t_{1} t_{2},
appears_free_in x t_{2} →
appears_free_in x (app t_{1} t_{2})
| afi_abs : ∀x y T_{11} t_{12},
y ≠ x →
appears_free_in x t_{12} →
appears_free_in x (abs y T_{11} t_{12})
| afi_test1 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x (test t_{1} t_{2} t_{3})
| afi_test2 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x (test t_{1} t_{2} t_{3})
| afi_test3 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x (test t_{1} t_{2} t_{3}).
Hint Constructors appears_free_in.
The free variables of a term are just the variables that appear
free in it. A term with no free variables is said to be
closed.
Definition closed (t:tm) :=
∀x, ¬appears_free_in x t.
∀x, ¬appears_free_in x t.
An open term is one that may contain free variables. (I.e., every
term is an open term; the closed terms are a subset of the open ones.
"Open" precisely means "possibly containing free variables.")
Exercise: 1 star, standard (afi)
In the space below, write out the rules of the appears_free_in relation in informal inference-rule notation. (Use whatever notational conventions you like — the point of the exercise is just for you to think a bit about the meaning of each rule.) Although this is a rather low-level, technical definition, understanding it is crucial to understanding substitution and its properties, which are really the crux of the lambda-calculus.
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_afi : option (nat*string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_afi : option (nat*string) := None.
Substitution
Lemma free_in_context : ∀x t T Gamma,
appears_free_in x t →
Gamma ⊢ t ∈ T →
∃T', Gamma x = Some T'.
appears_free_in x t →
Gamma ⊢ t ∈ T →
∃T', Gamma x = Some T'.
Proof: We show, by induction on the proof that x appears free
in t, that, for all contexts Gamma, if t is well typed
under Gamma, then Gamma assigns some type to x.
- If the last rule used is afi_var, then t = x, and from the
assumption that t is well typed under Gamma we have
immediately that Gamma assigns a type to x.
- If the last rule used is afi_app1, then t = t_{1} t_{2} and x
appears free in t_{1}. Since t is well typed under Gamma,
we can see from the typing rules that t_{1} must also be, and
the IH then tells us that Gamma assigns x a type.
- Almost all the other cases are similar: x appears free in a
subterm of t, and since t is well typed under Gamma, we
know the subterm of t in which x appears is well typed
under Gamma as well, and the IH gives us exactly the
conclusion we want.
- The only remaining case is afi_abs. In this case t = \y:T_{11}.t12 and x appears free in t_{12}, and we also know that x is different from y. The difference from the previous cases is that, whereas t is well typed under Gamma, its body t_{12} is well typed under (y⊢>T_{11}; Gamma, so the IH allows us to conclude that x is assigned some type by the extended context (y⊢>T_{11}; Gamma. To conclude that Gamma assigns a type to x, we appeal to lemma update_neq, noting that x and y are different variables.
Proof.
intros x t T Gamma H H_{0}. generalize dependent Gamma.
generalize dependent T.
induction H;
intros; try solve [inversion H_{0}; eauto].
- (* afi_abs *)
inversion H_{1}; subst.
apply IHappears_free_in in H_{7}.
rewrite update_neq in H_{7}; assumption.
Qed.
From the free_in_context lemma, it immediately follows that any
term t that is well typed in the empty context is closed (it has
no free variables).
Exercise: 2 stars, standard, optional (typable_empty__closed)
Corollary typable_empty__closed : ∀t T,
empty ⊢ t ∈ T →
closed t.
empty ⊢ t ∈ T →
closed t.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *) Admitted.
Sometimes, when we have a proof of some typing relation
Gamma ⊢ t ∈ T, we will need to replace Gamma by a different
context Gamma'. When is it safe to do this? Intuitively, it
must at least be the case that Gamma' assigns the same types as
Gamma to all the variables that appear free in t. In fact,
this is the only condition that is needed.
Lemma context_invariance : ∀Gamma Gamma' t T,
Gamma ⊢ t ∈ T →
(∀x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' ⊢ t ∈ T.
Gamma ⊢ t ∈ T →
(∀x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' ⊢ t ∈ T.
Proof: By induction on the derivation of Gamma ⊢ t ∈ T.
- If the last rule in the derivation was T_Var, then t = x
and Gamma x = T. By assumption, Gamma' x = T as well, and
hence Gamma' ⊢ t ∈ T by T_Var.
- If the last rule was T_Abs, then t = \y:T_{11}. t_{12}, with T
= T_{11} → T_{12} and y⊢>T_{11}; Gamma ⊢ t_{12} ∈ T_{12}. The
induction hypothesis is that, for any context Gamma'', if
y⊢>T_{11}; Gamma and Gamma'' assign the same types to
all the free variables in t_{12}, then t_{12} has type T_{12}
under Gamma''. Let Gamma' be a context which agrees with
Gamma on the free variables in t; we must show Gamma' ⊢
\y:T_{11}. t_{12} ∈ T_{11} → T_{12}.
- If the last rule was T_App, then t = t_{1} t_{2}, with Gamma ⊢ t_{1} ∈ T_{2} → T and Gamma ⊢ t_{2} ∈ T_{2}. One induction hypothesis states that for all contexts Gamma', if Gamma' agrees with Gamma on the free variables in t_{1}, then t_{1} has type T_{2} → T under Gamma'; there is a similar IH for t_{2}. We must show that t_{1} t_{2} also has type T under Gamma', given the assumption that Gamma' agrees with Gamma on all the free variables in t_{1} t_{2}. By T_App, it suffices to show that t_{1} and t_{2} each have the same type under Gamma' as under Gamma. But all free variables in t_{1} are also free in t_{1} t_{2}, and similarly for t_{2}; hence the desired result follows from the induction hypotheses.
Proof with eauto.
intros.
generalize dependent Gamma'.
induction H; intros; auto.
- (* T_Var *)
apply T_Var. rewrite <- H_{0}...
- (* T_Abs *)
apply T_Abs.
apply IHhas_type. intros x_{1} Hafi.
(* the only tricky step... the Gamma' we use to
instantiate is x⊢>T_{11};Gamma *)
unfold update. unfold t_update. destruct (eqb_string x_{0} x_{1}) eqn: Hx0x_{1}...
rewrite eqb_string_false_iff in Hx0x_{1}. auto.
- (* T_App *)
apply T_App with T_{11}...
Qed.
intros.
generalize dependent Gamma'.
induction H; intros; auto.
- (* T_Var *)
apply T_Var. rewrite <- H_{0}...
- (* T_Abs *)
apply T_Abs.
apply IHhas_type. intros x_{1} Hafi.
(* the only tricky step... the Gamma' we use to
instantiate is x⊢>T_{11};Gamma *)
unfold update. unfold t_update. destruct (eqb_string x_{0} x_{1}) eqn: Hx0x_{1}...
rewrite eqb_string_false_iff in Hx0x_{1}. auto.
- (* 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 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 assigned 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 can
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; Gamma ⊢ t ∈ T and ⊢ v ∈ U,
then Gamma ⊢ [x:=v]t ∈ T.
Lemma substitution_preserves_typing : ∀Gamma x U t v T,
(x ⊢> U ; Gamma) ⊢ t ∈ T →
empty ⊢ v ∈ U →
Gamma ⊢ [x:=v]t ∈ T.
(x ⊢> U ; Gamma) ⊢ t ∈ T →
empty ⊢ v ∈ U →
Gamma ⊢ [x:=v]t ∈ T.
One technical subtlety in the statement of the lemma is that
we assume v has type U in the empty context — in other
words, we assume v is closed. This assumption considerably
simplifies the T_Abs case of the proof (compared to assuming
Gamma ⊢ v ∈ U, which would be the other reasonable assumption
at this point) because the context invariance lemma then tells us
that v has type U in any context at all — we don't have to
worry about free variables in v clashing with the variable being
introduced into the context by T_Abs.
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.
Proof: We show, by induction on t, that for all T and
Gamma, if x⊢>U; Gamma ⊢ t ∈ T and ⊢ v ∈ U, then
Gamma ⊢ [x:=v]t ∈ T.
Technical note: This proof is a rare case where an induction on
terms, rather than typing derivations, yields a simpler argument.
The reason for this is that the assumption x⊢>U; Gamma ⊢ t
∈ T is not completely generic, in the sense that one of the
"slots" in the typing relation — namely the context — is not
just a variable, and this means that Coq's native induction tactic
does not give us the induction hypothesis that we want. It is
possible to work around this, but the needed generalization is a
little tricky. The term t, on the other hand, is completely
generic.
- If t is a variable there are two cases to consider,
depending on whether t is x or some other variable.
- If t = x, then from the fact that x⊢>U; Gamma ⊢
x ∈ T we conclude that U = T. We must show that
[x:=v]x = v has type T under Gamma, given the
assumption that v has type U = T under the empty
context. This follows from context invariance: if a
closed term has type T in the empty context, it has that
type in any context.
- If t is some variable y that is not equal to x, then
we need only note that y has the same type under
x⊢>U; Gamma as under Gamma.
- If t = x, then from the fact that x⊢>U; Gamma ⊢
x ∈ T we conclude that U = T. We must show that
[x:=v]x = v has type T under Gamma, given the
assumption that v has type U = T under the empty
context. This follows from context invariance: if a
closed term has type T in the empty context, it has that
type in any context.
- If t is an abstraction \y:T_{11}. t_{12}, then the IH tells us,
for all Gamma' and T', that if x⊢>U; Gamma' ⊢ t_{12}
∈ T' and ⊢ v ∈ U, then Gamma' ⊢ [x:=v]t_{12} ∈ T'.
- If t is an application t_{1} t_{2}, the result follows
straightforwardly from the definition of substitution and the
induction hypotheses.
- The remaining cases are similar to the application case.
Proof with eauto.
intros Gamma x U t v T Ht Ht'.
generalize dependent Gamma. generalize dependent T.
induction t; intros T Gamma H;
(* in each case, we'll want to get at the derivation of H *)
inversion H; subst; simpl...
- (* var *)
rename s into y. destruct (eqb_stringP x y) as [Hxy|Hxy].
+ (* x=y *)
subst.
rewrite update_eq in H_{2}.
inversion H_{2}; subst.
eapply context_invariance. eassumption.
apply typable_empty__closed in Ht'. unfold closed in Ht'.
intros. apply (Ht' x_{0}) in H_{0}. inversion H_{0}.
+ (* x<>y *)
apply T_Var. rewrite update_neq in H_{2}...
- (* abs *)
rename s into y. rename t into T. apply T_Abs.
destruct (eqb_stringP x y) as [Hxy | Hxy].
+ (* x=y *)
subst. rewrite update_shadow in H_{5}. apply H_{5}.
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y z) as [Hyz | Hyz]; subst; trivial.
rewrite <- eqb_string_false_iff in Hxy.
rewrite Hxy...
Qed.
intros Gamma x U t v T Ht Ht'.
generalize dependent Gamma. generalize dependent T.
induction t; intros T Gamma H;
(* in each case, we'll want to get at the derivation of H *)
inversion H; subst; simpl...
- (* var *)
rename s into y. destruct (eqb_stringP x y) as [Hxy|Hxy].
+ (* x=y *)
subst.
rewrite update_eq in H_{2}.
inversion H_{2}; subst.
eapply context_invariance. eassumption.
apply typable_empty__closed in Ht'. unfold closed in Ht'.
intros. apply (Ht' x_{0}) in H_{0}. inversion H_{0}.
+ (* x<>y *)
apply T_Var. rewrite update_neq in H_{2}...
- (* abs *)
rename s into y. rename t into T. apply T_Abs.
destruct (eqb_stringP x y) as [Hxy | Hxy].
+ (* x=y *)
subst. rewrite update_shadow in H_{5}. apply H_{5}.
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y z) as [Hyz | Hyz]; subst; trivial.
rewrite <- eqb_string_false_iff in Hxy.
rewrite Hxy...
Qed.
Main Theorem
Theorem preservation : ∀t t' T,
empty ⊢ t ∈ T →
t --> t' →
empty ⊢ t' ∈ T.
empty ⊢ t ∈ T →
t --> t' →
empty ⊢ t' ∈ T.
Proof: By induction on the derivation of ⊢ t ∈ T.
- We can immediately rule out T_Var, T_Abs, T_Tru, and
T_Fls as final rules in the derivation, since in each of these
cases t cannot take a step.
- If the last rule in the derivation is T_App, then t = t_{1} t_{2},
and there are subderivations showing that ⊢ t_{1} ∈ T_{11}→T and
⊢ t_{2} ∈ T_{11} plus two induction hypotheses: (1) t_{1} --> t_{1}'
implies ⊢ t_{1}' ∈ T_{11}→T and (2) t_{2} --> t_{2}' implies ⊢ t_{2}'
∈ T_{11}. There are now three subcases to consider, one for
each rule that could be used to show that t_{1} t_{2} takes a step
to t'.
- If t_{1} t_{2} takes a step by ST_App1, with t_{1} stepping to
t_{1}', then, by the first IH, t_{1}' has the same type as
t_{1} (⊢ t_{1} ∈ T_{11}→T), and hence by T_App t_{1}' t_{2} has
type T.
- The ST_App2 case is similar, using the second IH.
- If t_{1} t_{2} takes a step by ST_AppAbs, then t_{1} =
\x:T_{11}.t12 and t_{1} t_{2} steps to [x:=t_{2}]t_{12}; the desired
result now follows from the substitution lemma.
- If t_{1} t_{2} takes a step by ST_App1, with t_{1} stepping to
t_{1}', then, by the first IH, t_{1}' has the same type as
t_{1} (⊢ t_{1} ∈ T_{11}→T), and hence by T_App t_{1}' t_{2} has
type T.
- If the last rule in the derivation is T_Test, then t = test
t_{1} then t_{2} else t_{3}, with ⊢ t_{1} ∈ Bool, ⊢ t_{2} ∈ T, and
⊢ t_{3} ∈ T, and with three induction hypotheses: (1) t_{1} -->
t_{1}' implies ⊢ t_{1}' ∈ Bool, (2) t_{2} --> t_{2}' implies ⊢ t_{2}'
∈ T, and (3) t_{3} --> t_{3}' implies ⊢ t_{3}' ∈ T.
- If t steps to t_{2} or t_{3} by ST_TestTru or
ST_TestFalse, the result is immediate, since t_{2} and t_{3}
have the same type as t.
- Otherwise, t steps by ST_Test, and the desired conclusion follows directly from the first induction hypothesis.
- If t steps to t_{2} or t_{3} by ST_TestTru or
ST_TestFalse, the result is immediate, since t_{2} and t_{3}
have the same type as t.
Proof with eauto.
remember (@empty ty) as Gamma.
intros t t' T HT. generalize dependent t'.
induction HT;
intros t' HE; subst Gamma; 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 T_{11}...
inversion HT_{1}...
Qed.
remember (@empty ty) as Gamma.
intros t t' T HT. generalize dependent t'.
induction HT;
intros t' HE; subst Gamma; 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 T_{11}...
inversion HT_{1}...
Qed.
Exercise: 2 stars, standard, recommended (subject_expansion_stlc)
An exercise in the Types chapter asked about the subject expansion property for the simple language of arithmetic and boolean expressions. This property did not hold for that language, and it also fails for STLC. That is, it is not always the case that, if t --> t' and has_type t' T, then empty ⊢ t ∈ T. Show this by giving a counter-example that does not involve conditionals.
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_subject_expansion_stlc : option (nat*string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_subject_expansion_stlc : option (nat*string) := None.
Type Soundness
Exercise: 2 stars, standard, optional (type_soundness)
Put progress and preservation together and show that a well-typed term can never reach a stuck state.
Definition stuck (t:tm) : Prop :=
(normal_form step) t ∧ ¬value t.
Corollary soundness : ∀t t' T,
empty ⊢ t ∈ T →
t -->* t' →
~(stuck t').
☐
(normal_form step) t ∧ ¬value t.
Corollary soundness : ∀t t' T,
empty ⊢ t ∈ T →
t -->* t' →
~(stuck t').
Proof.
intros t t' T Hhas_type Hmulti. unfold stuck.
intros [Hnf Hnot_val]. unfold normal_form in Hnf.
induction Hmulti.
(* FILL IN HERE *) Admitted.
intros t t' T Hhas_type Hmulti. unfold stuck.
intros [Hnf Hnot_val]. unfold normal_form in Hnf.
induction Hmulti.
(* FILL IN HERE *) Admitted.
Uniqueness of Types
Exercise: 3 stars, standard (unique_types)
Another nice property of the STLC is that types are unique: a given term (in a given context) has at most one type.
Theorem unique_types : ∀Gamma e T T',
Gamma ⊢ e ∈ T →
Gamma ⊢ e ∈ T' →
T = T'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Gamma ⊢ e ∈ T →
Gamma ⊢ e ∈ T' →
T = T'.
Proof.
(* FILL IN HERE *) Admitted.
Additional Exercises
Exercise: 1 star, standard (progress_preservation_statement)
Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus (as Coq theorems). You can write Admitted for the proofs.
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_progress_preservation_statement : option (nat*string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_progress_preservation_statement : option (nat*string) := None.
Exercise: 2 stars, standard (stlc_variation1)
Suppose we add a new term zap with the following reduction rule(ST_Zap) | |
t --> zap |
(T_Zap) | |
Gamma ⊢ zap ∈ T |
- Determinism of step
- Progress
- Preservation
(* Do not modify the following line: *)
Definition manual_grade_for_stlc_variation1 : option (nat*string) := None.
☐
Definition manual_grade_for_stlc_variation1 : option (nat*string) := None.
Exercise: 2 stars, standard (stlc_variation2)
Suppose instead that we add a new term foo with the following reduction rules:(ST_Foo1) | |
(\x:A. x) --> foo |
(ST_Foo2) | |
foo --> tru |
- Determinism of step
- Progress
- Preservation
(* Do not modify the following line: *)
Definition manual_grade_for_stlc_variation2 : option (nat*string) := None.
☐
Definition manual_grade_for_stlc_variation2 : option (nat*string) := None.
Exercise: 2 stars, standard (stlc_variation3)
Suppose instead that we remove the rule ST_App1 from the step relation. Which of the following properties of the STLC remain true in the presence of this rule? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample.- Determinism of step
- Progress
- Preservation
(* Do not modify the following line: *)
Definition manual_grade_for_stlc_variation3 : option (nat*string) := None.
☐
Definition manual_grade_for_stlc_variation3 : option (nat*string) := None.
Exercise: 2 stars, standard, optional (stlc_variation4)
Suppose instead that we add the following new rule to the reduction relation:(ST_FunnyTestTru) | |
(test tru then t_{1} else t_{2}) --> tru |
- Determinism of step
- Progress
- Preservation
☐
Exercise: 2 stars, standard, optional (stlc_variation5)
Suppose instead that we add the following new rule to the typing relation:Gamma ⊢ t_{1} ∈ Bool->Bool->Bool | |
Gamma ⊢ t_{2} ∈ Bool | (T_FunnyApp) |
Gamma ⊢ t_{1} t_{2} ∈ Bool |
- Determinism of step
- Progress
- Preservation
☐
Exercise: 2 stars, standard, optional (stlc_variation6)
Suppose instead that we add the following new rule to the typing relation:Gamma ⊢ t_{1} ∈ Bool | |
Gamma ⊢ t_{2} ∈ Bool | (T_FunnyApp') |
Gamma ⊢ t_{1} t_{2} ∈ Bool |
- Determinism of step
- Progress
- Preservation
☐
Exercise: 2 stars, standard, optional (stlc_variation7)
Suppose we add the following new rule to the typing relation of the STLC:(T_FunnyAbs) | |
⊢ \x:Bool.t ∈ Bool |
- Determinism of step
- Progress
- Preservation
☐
End STLCProp.
Exercise: STLC with Arithmetic
Module STLCArith.
Import STLC.
Import STLC.
To types, we add a base type of natural numbers (and remove
booleans, for brevity).
Inductive ty : Type :=
| Arrow : ty → ty → ty
| Nat : ty.
| Arrow : ty → ty → ty
| Nat : ty.
To terms, we add natural number constants, along with
successor, predecessor, multiplication, and zero-testing.
Inductive tm : Type :=
| var : string → tm
| app : tm → tm → tm
| abs : string → ty → tm → tm
| const : nat → tm
| scc : tm → tm
| prd : tm → tm
| mlt : tm → tm → tm
| test0 : tm → tm → tm → tm.
| var : string → tm
| app : tm → tm → tm
| abs : string → ty → tm → tm
| const : nat → tm
| scc : tm → tm
| prd : tm → tm
| mlt : tm → tm → tm
| test0 : tm → tm → tm → tm.
Exercise: 5 stars, standard (stlc_arith)
Finish formalizing the definition and properties of the STLC extended with arithmetic. This is a longer exercise. Specifically:- Fixpoint susbt
- Inductive value
- Inductive step
- Inductive has_type
- Inductive appears_free_in
- Lemma context_invariance
- Lemma free_in_context
- Lemma substitution_preserves_typing
- Theorem preservation
- Theorem progress
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_stlc_arith : option (nat*string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_stlc_arith : option (nat*string) := None.
End STLCArith.
(* Wed Jan 9 12:05:11 EST 2019 *)
(* Wed Jan 9 12:05:11 EST 2019 *)