Require Import List.
Require Import String.
Open Scope string_scope.
Definition var := string.
(** Lambda calculus syntax.
We have variables, application, and abstraction. These are all we
need in order to write programs to compute every computable function.
*)
Inductive Expr : Set :=
| EConst (* The one and only constant *)
| EVar (v : var) (* Variables *)
| EApp (e1 : Expr) (e2 : Expr) (* Application, e1 applied to e2 *)
| EAbs (x : var) (body : Expr). (* Abstraction, \x -> body *)
(**
In this homework you will implement call by value semantics of
lambda calculus. This means that when evaluating a function
application, (e1 e2) you will:
1. evaluate e1 down as far as possible (it had better end up an abstraction)
2. next, evaluate e2 down to a VALUE.
NOTE: in our simple lambda calculus, abstractions and constants are values
3. next, substitute the value we got for e2 into the simplified form of e1
NOTE: we define a relation for what it means to be a well formed substitution below
*)
(* Here we formally define what it means to be a value (not able to be evaluated any more) *)
Definition isValue (e : Expr) : Prop :=
match e with
| EVar _ => False
| EAbs _ _ => True
| EConst => True
| EApp _ _ => False
end.
(**
Here we introduce what is called a decidability lemma.
Essentially we are saying that for any expression you have, it's either a value or not.
We need this because we can write down undecidable things as Props.
*)
Lemma isValueDec :
forall e,
{ isValue e } + {~ isValue e}.
Proof.
intros. destruct e; simpl; auto.
Defined.
(* Here we define what it means for a particular substitution to be valid *)
(* e1[e2/x] = e3 *)
Inductive Subst : Expr -> Expr -> var -> Expr -> Prop :=
| SubstConst : forall e x, (* substituting into a const is just that const *)
Subst EConst e x EConst
| SubstVar_same : forall e x, (* substitute an expression in for a variable *)
Subst (EVar x) e x e
| SubstVar_diff : forall e x1 x2,
x1 <> x2 ->
Subst (EVar x1) e x2 (EVar x1)
| SubstApp : forall eA eB e x eA' eB',
Subst eA e x eA' ->
Subst eB e x eB' ->
Subst (EApp eA eB) e x (EApp eA' eB')
| SubstAbs_same : forall eA e x,
Subst (EAbs x eA) e x (EAbs x eA)
| SubstAbs_diff : forall eA e x1 x2 eA',
x1 <> x2 ->
Subst eA e x2 eA' ->
Subst (EAbs x1 eA) e x2 (EAbs x1 eA').
(* Here we give semantics to our simple language *)
Inductive Step : Expr -> Expr -> Prop :=
| ScrunchLeft :
forall e1 e1' e2,
Step e1 e1' ->
Step (EApp e1 e2) (EApp e1' e2)
| ScrunchRight :
forall e1 e2 e2',
isValue e1 ->
Step e2 e2' ->
Step (EApp e1 e2) (EApp e1 e2')
| Ssubst :
forall x e1 e2 e1',
isValue e2 ->
Subst e1 e2 x e1' ->
Step (EApp (EAbs x e1) e2) e1'.
(* Here we define the transitive closure of a step relation. Note that
we are able to define this once for any step relation, which is just
kinda cool *)
Inductive star (step : Expr -> Expr -> Prop) : Expr -> Expr -> Prop :=
| star_refl :
forall e,
star step e e
| star_right :
forall e1 e2 e3,
star step e1 e2 ->
step e2 e3 ->
star step e1 e3.
(* [Problem 1] *)
(* Implement a function to perform substitution *)
(* e1[e2/x] = e3 *)
(* Given e1, e2, and x, produce e3 *)
(* Your function should be a total function (no option in the return type *)
(* Hint: for equality of vars, use "string_dec" *)
(* [Problem 2] *)
(* Prove that, given a valid term of the Subst relation, your function *)
(* from problem 1 will produce the same substitution. *)
(* [Problem 3] *)
(* Prove that if your function from problem 1 produces a substitution, *)
(* it's modeled by the Subst relation *)
(* This should look like problem 2 with the hypothesis and conclusion flipped *)
(* [Problem 4] *)
(* Define a step function *)
(* The skeleton of one has been provided *)
Fixpoint step (e : Expr) : option Expr := None.
(* In lambda calculus, we like to reason about what values can take
steps, and can't. We would love to know that if we have a value,
i.e. something that we have decided is the end result of a
computation, then it can't take a step *)
(* [Problem 5] *)
(* Prove that any value cannot take a step *)
(* We have step function, and a Step relation *)
(* That means we can prove them equivalent *)
(* Let's make sure the step function is implemented correctly *)
(* In proving the next two lemmas, you may find bugs in your step *)
(* function. Change it all you need. Don't modify the Step relation. *)
(* When you've proven the next two lemmas, you will know that you got *)
(* your step function right *)
(* [Problem 6] *)
(* Prove that if the Step relation says e1 can step to e2, then your *)
(* step function will take e1 and produce "Some e2" *)
(* [Problem 7] *)
(* Prove that if your step function produces "Some", that the Step *)
(* relation models that step *)
(* That's awesome, we defined relations and functions for evaluation *)
(* Now, we were able to prove that if something is a value, it can't take a step *)
(* What if we were to try to prove the other way, that if something
can't take a step, then it's not a value? *)
Lemma no_step_value :
forall v,
step v = None ->
isValue v.
Proof.
Abort.
(* Turns out we can have malformed expressions, which can't step, but aren't values. *)
(* [Problem 8] *)
(* Explain in English how we can have expressions that both can't step and aren't values *)
(* [Problem 9] *)
(* Prove the following lemma in Coq to show you have a counterexample *)
Lemma no_step_and_not_value :
exists e,
step e = None /\ ~ isValue e.
Proof.
admit.
Qed.
(* How do we solve this? With types! *)
(* Here we define the types for the simply typed lambda calculus *)
Inductive SimpleType :=
| TUnit
| TFun (arg : SimpleType) (res : SimpleType).
(* Here we define what a type environment is *)
(* Simply a mapping from variables to types *)
Definition Env := var -> option SimpleType.
(* Here is how we extend a typing environment with another variable binding *)
Definition extend (env : Env) x t :=
fun y => if string_dec x y then Some t else env y.
(* What it means for a lambda expression to be well typed *)
(* These are the type rules for STLC *)
(* You will frequently see them in the literature with horizontal lines *)
Inductive WellTyped : Env -> Expr -> SimpleType -> Prop :=
| WtConst :
forall env,
WellTyped env EConst TUnit
| WtVar :
forall env x t,
env x = Some t ->
WellTyped env (EVar x) t
| WtAbs :
forall env x t exp t',
WellTyped (extend env x t) exp t' ->
WellTyped env (EAbs x exp) (TFun t t')
| WtApp :
forall env f arg t t',
WellTyped env arg t ->
WellTyped env f (TFun t t') ->
WellTyped env (EApp f arg) t'.
(* [Problem 10] *)
(* Explain in English why we will run into trouble if we try to write *)
(* a typechecker as a function. For everything else, we write a relation *)
(* and a function, and prove the two equivalent. Why, in this particular *)
(* case, can we not simply write the "well_typed" function, of type *)
(* Env -> Expr -> SimpleType -> Bool? *)
(* Here's another decidability lemma for types *)
Lemma st_eq_dec :
forall (t1 t2 : SimpleType),
{t1 = t2} + {t1 <> t2}.
Proof.
decide equality.
Qed.
(* The empty environment *)
Definition Empty : Env := fun x => None.
(* [Problem 11] *)
(* Here's what we call a "canonical forms" lemma *)
(* We want to say that if something has a type of a value in an empty *)
(* context, it is in its "canonical form" *)
Lemma canonical_const :
forall e,
isValue e ->
WellTyped Empty e TUnit ->
e = EConst.
Proof.
admit.
Qed.
(* [Problem 12] *)
(* Here's something more interesting. Canonical forms for functions *)
Lemma canonical_abs :
forall e t t',
isValue e ->
WellTyped Empty e (TFun t t') ->
exists x body,
e = EAbs x body.
Proof.
admit.
Qed.
(* [Problem 13] *)
(* In order to prove type soundness, we destructure the proof into two lemmas *)
(* The first one is called progress *)
(* If I have a well typed term, it can either take a step, or is a value *)
(* Prove the progress lemma *)
(* Hint: before inducting, use "remember Empty as env" to preserve the *)
(* knowledge that the environment is Empty *)
(* Hint: you will need one of your canonical forms lemmas from above *)
Lemma type_progress :
forall e t,
WellTyped Empty e t ->
((exists e', Step e e') \/ isValue e).
Proof.
admit.
Qed.
(* The second lemma is called type preservation *)
(* In order to prove that, we're going to need a lot of auxiliary machinery *)
(* Don't worry, I'll walk you through it. *)
(* FROM THIS POINT ON *)
(* I may not tell you to use a lemma that you've previously proved *)
(* but you absolutely should *)
(* I give you the lemmas I think you need to succeed. If you need more *)
(* lemmas that's completely fine. If you try to do some of these proofs *)
(* without using the lemmas you've already proven, you will not have a *)
(* good time. *)
(* Here we define what it means for two environments to be extensionally equivalent *)
(* Extensional Equality for functions means they return the same result for every argument *)
(* for example, \x -> 1 + x and \x -> x + 1 are extensionally equivalent, but not the same function *)
Definition ext_equiv (env1 env2 : Env) : Prop :=
forall x,
env1 x = env2 x.
(* [Problem 14] *)
(* Prove a lemma about extending extensionally equivalent environments *)
Lemma extend_pres_ext_equiv :
forall env env2,
ext_equiv env env2 ->
forall x t,
ext_equiv (extend env x t) (extend env2 x t).
Proof.
admit.
Qed.
(* [Problem 15] *)
(* Prove that if a term is well typed in an environment, it is also *)
(* well typed in any extensionally equivalent environment *)
(* Hint: Be careful with your induction *)
Lemma well_typed_ext_equiv :
forall env1 e t,
WellTyped env1 e t ->
forall env2,
ext_equiv env1 env2 ->
WellTyped env2 e t.
Proof.
admit.
Qed.
(* [Problem 16] *)
(* Prove that extending an environment with the same variable twice is *)
(* the same as extending it once *)
(* Hint: use well_typed_ext_equiv *)
Lemma extend_same:
forall env x t t' e t'',
WellTyped (extend (extend env x t) x t') e t'' <->
WellTyped (extend env x t') e t''.
Proof.
admit.
Qed.
(* [Problem 17] *)
(* Prove that extending an environment with two different variables is *)
(* ok to do in either order *)
Lemma extend_different:
forall e t env x1 x2 t1 t2,
x1 <> x2 ->
(WellTyped (extend (extend env x2 t2) x1 t1) e t <->
WellTyped (extend (extend env x1 t1) x2 t2) e t).
Proof.
admit.
Qed.
(* Here we define what free variables exist in an expression *)
(* Intuitively, these are all the variables which exist, but are not *)
(* bound by an abstraction *)
Fixpoint free_variables (e : Expr) : list var :=
match e with
| EConst => nil
| EVar x => x :: nil
| EAbs x body => remove string_dec x (free_variables body)
| EApp e1 e2 => app (free_variables e1) (free_variables e2)
end.
(* [Problem 18] *)
(* This may seem to be an obvious lemma about remove and lists *)
(* It does not happen to be in the standard library *)
(* Let's go prove it *)
Lemma remove_different :
forall {A} (eq_dec : forall (a b : A), {a = b} + {a <> b}) l x y,
x <> y ->
(In x l <->
In x (remove eq_dec y l)).
Proof.
admit.
Qed.
(* [Problem 19] *)
(* Here we prove what's called weakening *)
(* If a variable isn't in the free variables of an expression, *)
(* we can extend the context with that variable, and produce the same *)
(* typing derivation *)
Lemma weakening :
forall e env t x t',
~ (In x (free_variables e)) ->
(WellTyped (extend env x t') e t <->
WellTyped env e t).
Proof.
admit.
Qed.
(* [Problem 20] *)
(* Here we prove that a correct substitution preserves typing *)
(* This one's a bit tricky, but remember to use inversion where *)
(* necessary, and to use previously proven lemmas *)
Lemma subst_type_pres :
forall e e' e'' x,
Subst e' e x e'' ->
forall env t t',
WellTyped env e t ->
free_variables e = nil ->
WellTyped (extend env x t) e' t' ->
WellTyped env e'' t'.
Proof.
admit.
Qed.
(* [Problem 21] *)
(* Here we prove that if we have free variables in an expression, we *)
(* need them in the type environment if that is well typed *)
Lemma env_vars_required :
forall env e t,
WellTyped env e t ->
(forall x, In x (free_variables e) -> env x <> None).
Proof.
admit.
Qed.
(* [Problem 22] *)
(* Here we prove that something that's well typed in the empty *)
(* environment has no free variables *)
(* Hint: Use a previously proven lemma *)
Lemma no_free_vars_empty :
forall e t,
WellTyped Empty e t ->
free_variables e = nil.
Proof.
admit.
Qed.
(* [Problem 23] *)
(* We finally have enough lemmas to prove type preservation, the other *)
(* lemma necessary for type soundness. It says that if we have a well *)
(* typed term, and take a step, then the result is still well typed with *)
(* the same type. *)
Lemma type_preservation :
forall e t,
WellTyped Empty e t ->
forall e',
Step e e' ->
WellTyped Empty e' t.
Proof.
admit.
Qed.
(* [Problem 24] *)
(* Prove type preservation over any sequence of steps *)
(* The lemma should look almost identical to the previous problem *)
(* [Problem 25] *)
(* Prove that our simple type system for lambda calculus is sound *)
(* Prove that any term reachable from any well typed term can either *)
(* take a step, or is a value *)
Theorem type_soundness :
forall e t,
WellTyped Empty e t ->
forall e',
star Step e e' ->
(exists e'', Step e' e'') \/ isValue e'.
Proof.
admit.
Qed.
(* Crowning Achievement *)
(* [Problem 26] *)
(* Prove the lemma we originally set out to prove, but with the *)
(* additional hypothesis of the term being well typed *)
Lemma no_step_value_typed :
forall e t,
WellTyped Empty e t ->
step e = None ->
isValue e.
Proof.
admit.
Qed.
(* Bonus Problem 1 *)
(* Hint: you will need strong induction on the size of the type *)
(* which means you will need to define what the size of the type means *)
(* Theorem strong_normalization : *)
(* forall t e, *)
(* WellTyped Empty e t -> *)
(* exists v, *)
(* star Step e v /\ isValue v. *)
(* Proof. *)
(* Note: the implication of this is interesting. This says that every *)
(* well typed term will halt. *)
(* Bonus Problem 2 *)
(* Construct your own definitions of the simply typed lambda calculus *)
(* that allow you to write a typechecker as a function (i.e. to get *)
(* around the problem you describe above) *)