StlcThe Simply Typed Lambda-Calculus
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From PLF Require Import Smallstep.
Overview
- variables
- function abstractions
- application
t ::= x (variable)
| \x:T,t (abstraction)
| t t (application)
| true (constant true)
| false (constant false)
| if t then t else t (conditional)
- \x:Bool, x
- (\x:Bool, x) true
- \x:Bool, if x then false else true
- \x:Bool, true
- \x:Bool, \y:Bool, x
- (\x:Bool, \y:Bool, x) false true
- \f:Bool→Bool, f (f true)
- (\f:Bool→Bool, f (f true)) (\x:Bool, false)
T ::= Bool
| T → T
- \x:Bool, false has type Bool→Bool
- \x:Bool, x has type Bool→Bool
- (\x:Bool, x) true has type Bool
- \x:Bool, \y:Bool, x has type Bool→Bool→Bool
(i.e., Bool → (Bool→Bool))
- (\x:Bool, \y:Bool, x) false has type Bool→Bool
- (\x:Bool, \y:Bool, x) false true has type Bool
Inductive tm : Type :=
| tm_var : string → tm
| tm_app : tm → tm → tm
| tm_abs : string → ty → tm → tm
| tm_true : tm
| tm_false : tm
| tm_if : tm → tm → tm → tm.
Declare Custom Entry stlc.
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 "'Bool'" := Ty_Bool (in custom stlc at level 0).
Notation "'if' x 'then' y 'else' z" :=
(tm_if 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).
Notation "'true'" := true (at level 1).
Notation "'true'" := tm_true (in custom stlc at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := tm_false (in custom stlc at level 0).
Some more notation magic to set up the concrete syntax, as we did
in the Imp chapter...
Definition x : string := "x".
Definition y : string := "y".
Definition z : string := "z".
Hint Unfold x : core.
Hint Unfold y : core.
Hint Unfold z : core.
Note that an abstraction \x:T,t (formally, tm_abs x T t) is
always annotated with the type T of its parameter, in contrast
to Coq (and other functional languages like ML, Haskell, etc.),
which use type inference to fill in missing annotations. We're
not considering type inference here.
Some examples...
Notation idB :=
<{\x:Bool, x}>.
Notation idBB :=
<{\x:Bool→Bool, x}>.
Notation idBBBB :=
<{\x:((Bool→Bool)→(Bool→Bool)), x}>.
Notation k := <{\x:Bool, \y:Bool, x}>.
Notation notB := <{\x:Bool, if x then false else true}>.
(We write these as Notations rather than Definitions to make
things easier for auto.)
Operational Semantics
Values
- We can say that \x:T, t is a value only when t is a
value -- i.e., only if the function's body has been
reduced (as much as it can be without knowing what argument it
is going to be applied to).
- Or we can say that \x:T, t is always a value, no matter whether t is one or not -- in other words, we can say that reduction stops at abstractions.
Compute (fun x:bool ⇒ 3 + 4)
fun x:bool ⇒ 7
Inductive value : tm → Prop :=
| v_abs : ∀ x T2 t1,
value <{\x:T2, t1}>
| v_true :
value <{true}>
| v_false :
value <{false}>.
Hint Constructors value : core.
Finally, we must consider what constitutes a complete program.
Intuitively, a "complete program" must not refer to any undefined
variables. We'll see shortly how to define the free variables
in a STLC term. A complete program is closed -- that is, it
contains no free variables.
(Conversely, a term with free variables is often called an open
term.)
Having made the choice not to reduce under abstractions, we don't
need to worry about whether variables are values, since we'll
always be reducing programs "from the outside in," and that means
the step relation will always be working with closed terms.
Substitution
(\x:Bool, if x then true else x) false
if false then true else false
- [x:=true] (if x then x else false)
yields if true then true else false
- [x:=true] x yields true
- [x:=true] (if x then x else y) yields if true then true else y
- [x:=true] y yields y
- [x:=true] false yields false (vacuous substitution)
- [x:=true] (\y:Bool, if y then x else false)
yields \y:Bool, if y then true else false
- [x:=true] (\y:Bool, x) yields \y:Bool, true
- [x:=true] (\y:Bool, y) yields \y:Bool, y
- [x:=true] (\x:Bool, x) yields \x:Bool, x
[x:=s]x = s
[x:=s]y = y if x ≠ y
[x:=s](\x:T, t) = \x:T, t
[x:=s](\y:T, t) = \y:T, [x:=s]t if x ≠ y
[x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2)
[x:=s]true = true
[x:=s]false = false
[x:=s](if t1 then t2 else t3) =
if [x:=s]t1 then [x:=s]t2 else [x:=s]t3
Reserved Notation "'[' x ':=' s ']' t" (in custom stlc at level 20, x constr).
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
| tm_var y ⇒
if eqb_string x y then s else t
| <{\y:T, t1}> ⇒
if eqb_string x y then t else <{\y:T, [x:=s] t1}>
| <{t1 t2}> ⇒
<{([x:=s] t1) ([x:=s] t2)}>
| <{true}> ⇒
<{true}>
| <{false}> ⇒
<{false}>
| <{if t1 then t2 else t3}> ⇒
<{if ([x:=s] t1) then ([x:=s] t2) else ([x:=s] t3)}>
end
where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).
Note on notations: You might be wondering why we need curly braces
around the substitution notation in the above definition, and why
do we need to redefine the substition notation in the stlc
custom grammar. The reason is that reserved notations in
definitions have to be defined in the general Coq grammar (and not
a custom one like stlc). This restriction only applies to the
subst definition, that is before the where ... part. From now
on, using the substitution notation in the stlc custom grammar
doesn't need any curly braces.
For example...
Technical note: Substitution becomes trickier to define if we
consider the case where s, the term being substituted for a
variable in some other term, may itself contain free variables.
Since we are only interested here in defining the step relation
on closed terms (i.e., terms like \x:Bool, x that include
binders for all of the variables they mention), we can sidestep this
extra complexity, but it must be dealt with when formalizing
richer languages.
For example, using the definition of substitution above to
substitute the open term s = \x:Bool, r, where r is a free
reference to some global resource, for the variable z in the
term t = \r:Bool, z, where r is a bound variable, we would get
\r:Bool, \x:Bool, r, where the free reference to r in s has
been "captured" by the binder at the beginning of t.
Why would this be bad? Because it violates the principle that the
names of bound variables do not matter. For example, if we rename
the bound variable in t, e.g., let t' = \w:Bool, z, then
[x:=s]t' is \w:Bool, \x:Bool, r, which does not behave the
same as [x:=s]t = \r:Bool, \x:Bool, r. That is, renaming a
bound variable changes how t behaves under substitution.
See, for example, [Aydemir 2008] for further discussion
of this issue.
Exercise: 3 stars, standard (substi_correct)
The definition that we gave above uses Coq's Fixpoint facility to define substitution as a function. Suppose, instead, we wanted to define substitution as an inductive relation substi. We've begun the definition by providing the Inductive header and one of the constructors; your job is to fill in the rest of the constructors and prove that the relation you've defined coincides with the function given above.Inductive substi (s : tm) (x : string) : tm → tm → Prop :=
| s_var1 :
substi s x (tm_var x) s
(* FILL IN HERE *)
.
Hint Constructors substi : core.
Theorem substi_correct : ∀ s x t t',
<{ [x:=s]t }> = t' ↔ substi s x t t'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Reduction
(\x:T,t12) v2 --> [x:=v2]t12
value v2 | (ST_AppAbs) |
(\x:T2,t1) v2 --> [x:=v2]t1 |
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) |
Reserved Notation "t '-->' t'" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀ x T2 t1 v2,
value v2 →
<{(\x:T2, t1) v2}> --> <{ [x:=v2]t1 }>
| ST_App1 : ∀ t1 t1' t2,
t1 --> t1' →
<{t1 t2}> --> <{t1' t2}>
| ST_App2 : ∀ v1 t2 t2',
value v1 →
t2 --> t2' →
<{v1 t2}> --> <{v1 t2'}>
| ST_IfTrue : ∀ t1 t2,
<{if true then t1 else t2}> --> t1
| ST_IfFalse : ∀ t1 t2,
<{if false then t1 else t2}> --> t2
| ST_If : ∀ t1 t1' t2 t3,
t1 --> t1' →
<{if t1 then t2 else t3}> --> <{if t1' then t2 else t3}>
where "t '-->' t'" := (step t t').
Hint Constructors step : core.
Notation multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
Lemma step_example1 :
<{idBB idB}> -->* idB.
Proof.
eapply multi_step.
apply ST_AppAbs.
apply v_abs.
simpl.
apply multi_refl. Qed.
Example:
(\x:Bool→Bool, x) ((\x:Bool→Bool, x) (\x:Bool, x))
-->* \x:Bool, x
i.e.,
(idBB (idBB idB)) -->* idB.
(\x:Bool→Bool, x) ((\x:Bool→Bool, x) (\x:Bool, x))
-->* \x:Bool, x
(idBB (idBB idB)) -->* idB.
Lemma step_example2 :
<{idBB (idBB idB)}> -->* idB.
Proof.
eapply multi_step.
apply ST_App2. auto.
apply ST_AppAbs. auto.
eapply multi_step.
apply ST_AppAbs. simpl. auto.
simpl. apply multi_refl. Qed.
Example:
(\x:Bool→Bool, x)
(\x:Bool, if x then false else true)
true
-->* false
i.e.,
(idBB notB) true -->* false.
(\x:Bool→Bool, x)
(\x:Bool, if x then false else true)
true
-->* false
(idBB notB) true -->* false.
Lemma step_example3 :
<{idBB notB true}> -->* <{false}>.
Proof.
eapply multi_step.
apply ST_App1. apply ST_AppAbs. auto. simpl.
eapply multi_step.
apply ST_AppAbs. auto. simpl.
eapply multi_step.
apply ST_IfTrue. apply multi_refl. Qed.
Example:
(\x:Bool → Bool, x)
((\x:Bool, if x then false else true) true)
-->* false
i.e.,
idBB (notB true) -->* false.
(Note that this term doesn't actually typecheck; even so, we can
ask how it reduces.)
(\x:Bool → Bool, x)
((\x:Bool, if x then false else true) true)
-->* false
idBB (notB true) -->* false.
Lemma step_example4 :
<{idBB (notB true)}> -->* <{false}>.
Proof.
eapply multi_step.
apply ST_App2. auto.
apply ST_AppAbs. auto. simpl.
eapply multi_step.
apply ST_App2. auto.
apply ST_IfTrue.
eapply multi_step.
apply ST_AppAbs. auto. simpl.
apply multi_refl. Qed.
We can use the normalize tactic defined in the Smallstep chapter
to simplify these proofs.
Lemma step_example1' :
<{idBB idB}> -->* idB.
Proof. normalize. Qed.
Lemma step_example2' :
<{idBB (idBB idB)}> -->* idB.
Proof. normalize. Qed.
Lemma step_example3' :
<{idBB notB true}> -->* <{false}>.
Proof. normalize. Qed.
Lemma step_example4' :
<{idBB (notB true)}> -->* <{false}>.
Proof. normalize. Qed.
Lemma step_example5 :
<{idBBBB idBB idB}>
-->* idB.
Proof.
(* FILL IN HERE *) Admitted.
Lemma step_example5_with_normalize :
<{idBBBB idBB idB}>
-->* idB.
Proof.
(* FILL IN HERE *) Admitted.
☐
Contexts
Typing Relation
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 |
Reserved Notation "Gamma '⊢' t '∈' T"
(at level 101,
t custom stlc, T custom stlc at level 0).
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀ Gamma x T1,
Gamma x = Some T1 →
Gamma ⊢ x \in T1
| T_Abs : ∀ Gamma x T1 T2 t1,
x ⊢> T2 ; Gamma ⊢ t1 \in T1 →
Gamma ⊢ \x:T2, t1 \in (T2 → T1)
| T_App : ∀ T1 T2 Gamma t1 t2,
Gamma ⊢ t1 \in (T2 → T1) →
Gamma ⊢ t2 \in T2 →
Gamma ⊢ t1 t2 \in T1
| T_True : ∀ Gamma,
Gamma ⊢ true \in Bool
| T_False : ∀ Gamma,
Gamma ⊢ false \in Bool
| T_If : ∀ t1 t2 t3 T1 Gamma,
Gamma ⊢ t1 \in Bool →
Gamma ⊢ t2 \in T1 →
Gamma ⊢ t3 \in T1 →
Gamma ⊢ if t1 then t2 else t3 \in T1
where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type : core.
Example typing_example_1 :
empty ⊢ \x:Bool, x \in (Bool → Bool).
Proof.
apply T_Abs. apply T_Var. reflexivity. Qed.
Note that, since we added the has_type constructors to the hints
database, auto can actually solve this one immediately.
More examples:
empty ⊢ \x:A, \y:A→A, y (y x)
\in A → (A→A) → A.
empty ⊢ \x:A, \y:A→A, y (y x)
\in A → (A→A) → A.
Exercise: 2 stars, standard, optional (typing_example_2_full)
Prove the same result without using auto, eauto, or eapply (or ...).Example typing_example_2_full :
empty ⊢
\x:Bool,
\y:Bool→Bool,
(y (y x)) \in
(Bool → (Bool → Bool) → Bool).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (typing_example_3)
Formally prove the following typing derivation holds:empty ⊢ \x:Bool→B, \y:Bool→Bool, \z:Bool,
y (x z)
\in T.
Example typing_example_3 :
∃ T,
empty ⊢
\x:Bool→Bool,
\y:Bool→Bool,
\z:Bool,
(y (x z)) \in
T.
Proof.
(* FILL IN HERE *) Admitted.
☐
¬∃ T,
empty ⊢ \x:Bool, \y:Bool, x y \in T.
Example typing_nonexample_1 :
¬ ∃ T,
empty ⊢
\x:Bool,
\y:Bool,
(x y) \in
T.
Proof.
intros Hc. destruct Hc as [T Hc].
(* The clear tactic is useful here for tidying away bits of
the context that we're not going to need again. *)
inversion Hc; subst; clear Hc.
inversion H4; subst; clear H4.
inversion H5; subst; clear H5 H4.
inversion H2; subst; clear H2.
discriminate H1.
Qed.
Exercise: 3 stars, standard, optional (typing_nonexample_3)
Another nonexample:¬(∃ S T,
empty ⊢ \x:S, x x \in T).