StlcPropProperties of STLC
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From PLF Require Import Maps.
From PLF Require Import Types.
From PLF Require Import Stlc.
From PLF Require Import Smallstep.
Set Default Goal Selector "!".
Module STLCProp.
Import STLC.
From PLF Require Import Maps.
From PLF Require Import Types.
From PLF Require Import Stlc.
From PLF Require Import Smallstep.
Set Default Goal Selector "!".
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 \in Bool →
value t →
(t = <{true}>) ∨ (t = <{false}>).
Lemma canonical_forms_fun : ∀ t T_{1} T_{2},
empty |-- t \in (T_{1} → T_{2}) →
value t →
∃ x u, t = <{\x:T_{1}, 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 T_{1} T_{2},
empty |-- t \in (T_{1} → T_{2}) →
value t →
∃ x u, t = <{\x:T_{1}, u}>.
Proof.
intros t T_{1} T_{2} HT HVal.
destruct HVal as [x ? t_{1}| |] ; inversion HT; subst.
∃ x, t_{1}. reflexivity.
Qed.
intros t T_{1} T_{2} HT HVal.
destruct HVal as [x ? t_{1}| |] ; inversion HT; subst.
∃ x, t_{1}. reflexivity.
Qed.
Progress
Proof: By induction on the derivation of |-- t \in T.
- The last rule of the derivation cannot be T_Var, since a
variable is never well typed in an empty context.
- The T_True, T_False, 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} \in T_{2} → T
and |-- t_{2} \in 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_If, then t = if
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 true or false. If it is true, 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_If).
- If t_{1} is a value, then since it has type Bool it must be
either true or false. If it is true, then t steps to
t_{2}; otherwise it steps to t_{3}.
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 = 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 *)
eapply canonical_forms_fun in Ht_{1}; [|assumption].
destruct Ht_{1} as [x [t_{0} H_{1}]]. subst.
∃ (<{ [x:=t_{2}]t_{0} }>)...
× (* t_{2} steps *)
destruct H_{0} as [t_{2}' Hstp]. ∃ (<{t_{1} t_{2}'}>)...
+ (* t_{1} steps *)
destruct H as [t_{1}' Hstp]. ∃ (<{t_{1}' t_{2}}>)...
- (* T_If *)
right. destruct IHHt1...
+ (* t_{1} is a value *)
destruct (canonical_forms_bool t_{1}); subst; eauto.
+ (* t_{1} also steps *)
destruct H as [t_{1}' Hstp]. ∃ <{if t_{1}' then t_{2} else t_{3}}>...
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 = 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 *)
eapply canonical_forms_fun in Ht_{1}; [|assumption].
destruct Ht_{1} as [x [t_{0} H_{1}]]. subst.
∃ (<{ [x:=t_{2}]t_{0} }>)...
× (* t_{2} steps *)
destruct H_{0} as [t_{2}' Hstp]. ∃ (<{t_{1} t_{2}'}>)...
+ (* t_{1} steps *)
destruct H as [t_{1}' Hstp]. ∃ (<{t_{1}' t_{2}}>)...
- (* T_If *)
right. destruct IHHt1...
+ (* t_{1} is a value *)
destruct (canonical_forms_bool t_{1}); subst; eauto.
+ (* t_{1} also steps *)
destruct H as [t_{1}' Hstp]. ∃ <{if t_{1}' then t_{2} else 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 \in T →
value t ∨ ∃ t', t --> t'.
Proof.
intros t.
induction t; intros T Ht; auto.
(* FILL IN HERE *) Admitted.
☐
empty |-- t \in 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,
well-typed) 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, for the variables
case, we discover that we need to deduce from the fact that a
term s has type S in the empty context the fact that s has
type S in every context. For this we prove a...
- weakening lemma, showing that typing is preserved under "extensions" to the context Gamma.
The Weakening Lemma
Lemma weakening : ∀ Gamma Gamma' t T,
includedin Gamma Gamma' →
Gamma |-- t \in T →
Gamma' |-- t \in T.
includedin 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 includedin_update.
Qed.
intros Gamma Gamma' t T H Ht.
generalize dependent Gamma'.
induction Ht; eauto using includedin_update.
Qed.
The following simple corollary is what we actually need below.
The Substitution Lemma
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.
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 \in T and |-- v \in U, then
Gamma |-- [x:=v]t \in T.
- 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 \in
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 the weakening lemma.
- 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 \in
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 the weakening lemma.
- If t is an abstraction \y:S, t_{0}, then T = S→T_{1} and
the IH tells us, for all Gamma' and T_{0}, that if x⊢>U;
Gamma' |-- t_{0} \in T_{0}, then Gamma' |-- [x:=v]t_{0} \in T_{0}.
Moreover, by inspecting the typing rules we see it must be
the case that y⊢>S; x⊢>U; Gamma |-- t_{0} \in T_{1}.
- 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.
intros Gamma x U t v T Ht Hv.
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; clear H; subst; simpl; eauto.
- (* var *)
rename s into y. destruct (eqb_spec x y); subst.
+ (* x=y *)
rewrite update_eq in H_{2}.
injection H_{2} as H_{2}; subst.
apply weakening_empty. assumption.
+ (* x<>y *)
apply T_Var. rewrite update_neq in H_{2}; auto.
- (* abs *)
rename s into y, t into S.
destruct (eqb_spec x y); subst; apply T_Abs.
+ (* x=y *)
rewrite update_shadow in H_{5}. assumption.
+ (* x<>y *)
apply IHt.
rewrite update_permute; auto.
Qed.
intros Gamma x U t v T Ht Hv.
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; clear H; subst; simpl; eauto.
- (* var *)
rename s into y. destruct (eqb_spec x y); subst.
+ (* x=y *)
rewrite update_eq in H_{2}.
injection H_{2} as H_{2}; subst.
apply weakening_empty. assumption.
+ (* x<>y *)
apply T_Var. rewrite update_neq in H_{2}; auto.
- (* abs *)
rename s into y, t into S.
destruct (eqb_spec x y); subst; apply T_Abs.
+ (* x=y *)
rewrite update_shadow in H_{5}. assumption.
+ (* x<>y *)
apply IHt.
rewrite update_permute; auto.
Qed.
One technical subtlety in the statement of the above lemma is that
we assume v has type U in the empty context -- in other
words, we assume v is closed. (Since we are using a simple
definition of substition that is not capture-avoiding, it doesn't
make sense to substitute non-closed terms into other terms.
Fortunately, closed terms are all we need!)
Exercise: 3 stars, advanced (substitution_preserves_typing_from_typing_ind)
Show that substitution_preserves_typing can also be proved by induction on typing derivations instead of induction on terms.
Lemma substitution_preserves_typing_from_typing_ind : ∀ 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.
remember (x ⊢> U; Gamma) as Gamma'.
generalize dependent Gamma.
induction Ht; intros Gamma' G; simpl; eauto.
(* FILL IN HERE *) Admitted.
☐
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.
remember (x ⊢> U; Gamma) as Gamma'.
generalize dependent Gamma.
induction Ht; intros Gamma' G; simpl; eauto.
(* FILL IN HERE *) Admitted.
☐
Main Theorem
Proof: By induction on the derivation of |-- t \in T.
- We can immediately rule out T_Var, T_Abs, T_True, and
T_False 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} \in T_{2}→T and
|-- t_{2} \in T_{2} plus two induction hypotheses: (1) t_{1} --> t_{1}'
implies |-- t_{1}' \in T_{2}→T and (2) t_{2} --> t_{2}' implies |-- t_{2}'
\in T_{2}. 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}' \in T_{2}→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_{0},t_{0} and t_{1} t_{2} steps to [x_{0}:=t_{2}]t_{0}; 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}' \in T_{2}→T), and hence by T_App t_{1}' t_{2} has
type T.
- If the last rule in the derivation is T_If, then t = if
t_{1} then t_{2} else t_{3}, with |-- t_{1} \in Bool, |-- t_{2} \in T_{1}, and
|-- t_{3} \in T_{1}, and with three induction hypotheses: (1) t_{1} -->
t_{1}' implies |-- t_{1}' \in Bool, (2) t_{2} --> t_{2}' implies |-- t_{2}'
\in T_{1}, and (3) t_{3} --> t_{3}' implies |-- t_{3}' \in T_{1}.
- If t steps to t_{2} or t_{3} by ST_IfTrue or
ST_IfFalse, the result is immediate, since t_{2} and t_{3}
have the same type as t.
- Otherwise, t steps by ST_If, and the desired conclusion follows directly from the first induction hypothesis.
- If t steps to t_{2} or t_{3} by ST_IfTrue or
ST_IfFalse, the result is immediate, since t_{2} and t_{3}
have the same type as 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 T_{2}...
inversion HT_{1}...
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 T_{2}...
inversion HT_{1}...
Qed.
Exercise: 2 stars, standard, especially useful (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 empty |-- t' \in T, then empty |-- t \in T. Show this by giving a counter-example that does not involve conditionals.
(* FILL IN HERE *)
Theorem not_subject_expansion:
∃ t t' T, t --> t' ∧ (empty |-- t' \in T) ∧ ¬ (empty |-- t \in T).
Proof.
(* Write "exists <{ ... }>" to use STLC notation. *)
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_subject_expansion_stlc : option (nat×string) := None.
☐
Theorem not_subject_expansion:
∃ t t' T, t --> t' ∧ (empty |-- t' \in T) ∧ ¬ (empty |-- t \in T).
Proof.
(* Write "exists <{ ... }>" to use STLC notation. *)
(* FILL IN HERE *) Admitted.
(* 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 type_soundness : ∀ t t' T,
empty |-- t \in T →
t -->* t' →
~(stuck t').
(normal_form step) t ∧ ¬ value t.
Corollary type_soundness : ∀ 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.
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 \in T →
Gamma |-- e \in T' →
T = T'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Gamma |-- e \in T →
Gamma |-- e \in T' →
T = T'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Context Invariance (Optional)
- 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 (x : string) : tm → Prop :=
| afi_var : appears_free_in x <{x}>
| afi_app1 : ∀ t_{1} t_{2},
appears_free_in x t_{1} →
appears_free_in x <{t_{1} t_{2}}>
| afi_app2 : ∀ t_{1} t_{2},
appears_free_in x t_{2} →
appears_free_in x <{t_{1} t_{2}}>
| afi_abs : ∀ y T_{1} t_{1},
y ≠ x →
appears_free_in x t_{1} →
appears_free_in x <{\y:T_{1}, t_{1}}>
| afi_if_{1} : ∀ t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x <{if t_{1} then t_{2} else t_{3}}>
| afi_if_{2} : ∀ t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x <{if t_{1} then t_{2} else t_{3}}>
| afi_if_{3} : ∀ t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x <{if t_{1} then t_{2} else t_{3}}>.
Hint Constructors appears_free_in : core.
| afi_var : appears_free_in x <{x}>
| afi_app1 : ∀ t_{1} t_{2},
appears_free_in x t_{1} →
appears_free_in x <{t_{1} t_{2}}>
| afi_app2 : ∀ t_{1} t_{2},
appears_free_in x t_{2} →
appears_free_in x <{t_{1} t_{2}}>
| afi_abs : ∀ y T_{1} t_{1},
y ≠ x →
appears_free_in x t_{1} →
appears_free_in x <{\y:T_{1}, t_{1}}>
| afi_if_{1} : ∀ t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x <{if t_{1} then t_{2} else t_{3}}>
| afi_if_{2} : ∀ t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x <{if t_{1} then t_{2} else t_{3}}>
| afi_if_{3} : ∀ t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x <{if t_{1} then t_{2} else t_{3}}>.
Hint Constructors appears_free_in : core.
The free variables of a term are just the variables that appear
free in it. This gives us another way to define closed terms --
arguably a better one, since it applies even to ill-typed
terms. Indeed, this is the standard definition of the term
"closed."
Conversely, 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, optional (afi)
(Officially optional, but strongly recommended!) 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.
☐
Lemma free_in_context : ∀ x t T Gamma,
appears_free_in x t →
Gamma |-- t \in T →
∃ T', Gamma x = Some T'.
appears_free_in x t →
Gamma |-- t \in 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_{1},t_{1} and x appears free in t_{1}, 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_{1} is well typed under y⊢>T_{1}; Gamma, so the IH allows us to conclude that x is assigned some type by the extended context y⊢>T_{1}; Gamma. To conclude that Gamma assigns a type to x, we appeal to lemma update_neq, noting that x and y are different variables.
Exercise: 2 stars, standard (free_in_context)
Complete the following proof.
Proof.
intros x t T Gamma H H_{0}. generalize dependent Gamma.
generalize dependent T.
induction H as [| | |y T_{1} t_{1} H H_{0} IHappears_free_in| | |];
intros; try solve [inversion H_{0}; eauto].
(* FILL IN HERE *) Admitted.
☐
intros x t T Gamma H H_{0}. generalize dependent Gamma.
generalize dependent T.
induction H as [| | |y T_{1} t_{1} H H_{0} IHappears_free_in| | |];
intros; try solve [inversion H_{0}; eauto].
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (typable_empty__closed)
Corollary typable_empty__closed : ∀ t T,
empty |-- t \in T →
closed t.
Proof.
(* FILL IN HERE *) Admitted.
☐
empty |-- t \in T →
closed t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma context_invariance : ∀ Gamma Gamma' t T,
Gamma |-- t \in T →
(∀ x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' |-- t \in T.
Gamma |-- t \in T →
(∀ x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' |-- t \in T.
Proof: By induction on the derivation of Gamma |-- t \in 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 \in T by T_Var.
- If the last rule was T_Abs, then t = \y:T_{2}, t_{1}, with T =
T_{2} → T_{1} and y⊢>T_{2}; Gamma |-- t_{1} \in T_{1}. The induction
hypothesis states that for any context Gamma'', if y⊢>T_{2};
Gamma and Gamma'' assign the same types to all the free
variables in t_{1}, then t_{1} has type T_{1} under Gamma''.
Let Gamma' be a context which agrees with Gamma on the free
variables in t; we must show Gamma' |-- \y:T_{2}, t_{1} \in T_{2} → T_{1}.
- If the last rule was T_App, then t = t_{1} t_{2}, with Gamma |-- t_{1} \in T_{2} → T and Gamma |-- t_{2} \in 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.
Exercise: 3 stars, standard, optional (context_invariance)
Complete the following proof.
Proof.
intros.
generalize dependent Gamma'.
induction H as [| ? x_{0} ????? | | | |]; intros; auto.
(* FILL IN HERE *) Admitted.
☐
intros.
generalize dependent Gamma'.
induction H as [| ? x_{0} ????? | | | |]; intros; auto.
(* FILL IN HERE *) Admitted.
☐
Additional Exercises
Exercise: 1 star, standard, optional (progress_preservation_statement)
(Officially optional, but strongly recommended!) 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 --> true |
- 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_FunnyIfTrue) | |
(if true then t_{1} else t_{2}) --> true |
- 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
☐
Exercise: STLC with Arithmetic
To types, we add a base type of natural numbers (and remove
booleans, for brevity).
To terms, we add natural number constants, along with
successor, predecessor, multiplication, and zero-testing.
Inductive tm : Type :=
| tm_var : string → tm
| tm_app : tm → tm → tm
| tm_abs : string → ty → tm → tm
| tm_const : nat → tm
| tm_succ : tm → tm
| tm_pred : tm → tm
| tm_mult : tm → tm → tm
| tm_if_{0} : tm → tm → tm → tm.
Notation "{ x }" := x (in custom stlc at level 1, x constr).
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 "'Nat'" := Ty_Nat (in custom stlc at level 0).
Notation "'succ' x" := (tm_succ x) (in custom stlc at level 0,
x custom stlc at level 0).
Notation "'pred' x" := (tm_pred x) (in custom stlc at level 0,
x custom stlc at level 0).
Notation "x * y" := (tm_mult x y) (in custom stlc at level 1,
left associativity).
Notation "'if_{0}' x 'then' y 'else' z" :=
(tm_if_{0} 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).
Coercion tm_const : nat >-> tm.
| tm_var : string → tm
| tm_app : tm → tm → tm
| tm_abs : string → ty → tm → tm
| tm_const : nat → tm
| tm_succ : tm → tm
| tm_pred : tm → tm
| tm_mult : tm → tm → tm
| tm_if_{0} : tm → tm → tm → tm.
Notation "{ x }" := x (in custom stlc at level 1, x constr).
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 "'Nat'" := Ty_Nat (in custom stlc at level 0).
Notation "'succ' x" := (tm_succ x) (in custom stlc at level 0,
x custom stlc at level 0).
Notation "'pred' x" := (tm_pred x) (in custom stlc at level 0,
x custom stlc at level 0).
Notation "x * y" := (tm_mult x y) (in custom stlc at level 1,
left associativity).
Notation "'if_{0}' x 'then' y 'else' z" :=
(tm_if_{0} 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).
Coercion tm_const : nat >-> tm.
In this extended exercise, your job is to finish formalizing the
definition and properties of the STLC extended with arithmetic.
Specifically:
Fill in the core definitions for STLCArith, by starting with the rules
and terms which are the same as STLC. Then prove the key lemmas and
theorems we provide. You will need to define and prove helper lemmas,
as before.
It will be necessary to also fill in "Reserved Notation", "Notation",
and "Hint Constructors".
Hint: If you get an error "STLC.tm" found instead of term "tm" then Coq
is picking up the old notation for ie: subst instead of the new
notation for STLCArith, so you need to overwrite the old with the
notation before you can use it.
Make sure Coq accepts the whole file before submitting.
Reserved Notation "'[' x ':=' s ']' t" (in custom stlc at level 20, x constr).
Fixpoint subst (x : string) (s : tm) (t : tm) : tm
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(You'll need to add remove the period at the end of this
definition and add
where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).when you fill it in.)
Inductive value : tm → Prop :=
(* FILL IN HERE *)
.
Hint Constructors value : core.
Inductive step : tm → tm → Prop :=
(* FILL IN HERE *)
where "t '-->' t'" := (step t t').
Notation multistep := (multi step).
Notation "t_{1} '-->*' t_{2}" := (multistep t_{1} t_{2}) (at level 40).
Hint Constructors step : core.
(* An example *)
Example Nat_step_example : ∃ t,
<{(\x: Nat, \y: Nat, x × y ) 3 2 }> -->* t.
Proof. (* FILL IN HERE *) Admitted.
(* Typing *)
Definition context := partial_map ty.
Inductive has_type : context → tm → ty → Prop :=
(* FILL IN HERE *)
where "Gamma '|--' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type : core.
(* An example *)
Example Nat_typing_example :
empty |-- ( \x: Nat, \y: Nat, x × y ) 3 2 \in Nat.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Hint Constructors value : core.
Inductive step : tm → tm → Prop :=
(* FILL IN HERE *)
where "t '-->' t'" := (step t t').
Notation multistep := (multi step).
Notation "t_{1} '-->*' t_{2}" := (multistep t_{1} t_{2}) (at level 40).
Hint Constructors step : core.
(* An example *)
Example Nat_step_example : ∃ t,
<{(\x: Nat, \y: Nat, x × y ) 3 2 }> -->* t.
Proof. (* FILL IN HERE *) Admitted.
(* Typing *)
Definition context := partial_map ty.
Inductive has_type : context → tm → ty → Prop :=
(* FILL IN HERE *)
where "Gamma '|--' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type : core.
(* An example *)
Example Nat_typing_example :
empty |-- ( \x: Nat, \y: Nat, x × y ) 3 2 \in Nat.
Proof.
(* FILL IN HERE *) Admitted.
☐
The Technical Theorems
Exercise: 4 stars, standard (STLCArith.weakening)
Lemma weakening : ∀ Gamma Gamma' t T,
includedin Gamma Gamma' →
Gamma |-- t \in T →
Gamma' |-- t \in T.
Proof. (* FILL IN HERE *) Admitted.
(* FILL IN HERE *)
☐
includedin Gamma Gamma' →
Gamma |-- t \in T →
Gamma' |-- t \in T.
Proof. (* FILL IN HERE *) Admitted.
(* FILL IN HERE *)
☐
(* Preservation *)
(* Hint: You will need to define and prove the same helper lemmas we used before *)
(* Hint: You will need to define and prove the same helper lemmas we used before *)
Theorem preservation : ∀ t t' T,
empty |-- t \in T →
t --> t' →
empty |-- t' \in T.
Proof with eauto. (* FILL IN HERE *) Admitted.
☐
empty |-- t \in T →
t --> t' →
empty |-- t' \in T.
Proof with eauto. (* FILL IN HERE *) Admitted.
☐
(* Progress *)