From 8e6b5b8996baa9ed106a984d5db3ec72ff056738 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 14 Mar 2016 13:14:41 -0400 Subject: [PATCH] LambdaCalculusAndTypeSoundness_template --- LambdaCalculusAndTypeSoundness_template.v | 617 ++++++++++++++++++++++ _CoqProject | 1 + frap_book.tex | 2 +- 3 files changed, 619 insertions(+), 1 deletion(-) create mode 100644 LambdaCalculusAndTypeSoundness_template.v diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v new file mode 100644 index 0000000..3585756 --- /dev/null +++ b/LambdaCalculusAndTypeSoundness_template.v @@ -0,0 +1,617 @@ +(** Formal Reasoning About Programs + * Chapter 8: Lambda Calculus and Simple Type Soundness + * Author: Adam Chlipala + * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) + +Require Import Frap. + +(* The last few chapters have focused on small programming languages that are + * representative of the essence of the imperative languages. We now turn to + * lambda-calculus, the usual representative of functional languages. *) + +Module Ulc. + Inductive exp : Set := + | Var (x : var) + | Abs (x : var) (body : exp) + | App (e1 e2 : exp). + + Fixpoint subst (rep : exp) (x : var) (e : exp) : exp := + match e with + | Var y => if string_dec y x then rep else Var y + | Abs y e1 => Abs y (if y ==v x then e1 else subst rep x e1) + | App e1 e2 => App (subst rep x e1) (subst rep x e2) + end. + + + (** * Big-step semantics *) + + Inductive eval : exp -> exp -> Prop := + | BigAbs : forall x e, + eval (Abs x e) (Abs x e) + | BigApp : forall e1 x e1' e2 v2 v, + eval e1 (Abs x e1') + -> eval e2 v2 + -> eval (subst v2 x e1') v + -> eval (App e1 e2) v. + + Inductive value : exp -> Prop := + | Value : forall x e, value (Abs x e). + + Hint Constructors eval value. + + Theorem value_eval : forall v, + value v + -> eval v v. + Proof. + invert 1; eauto. + Qed. + + Hint Resolve value_eval. + + Theorem eval_value : forall e v, + eval e v + -> value v. + Proof. + induct 1; eauto. + Qed. + + Hint Resolve eval_value. + + (* Some notations, to let us write more normal-looking lambda terms *) + Coercion Var : var >-> exp. + Notation "\ x , e" := (Abs x e) (at level 50). + Infix "@" := App (at level 49, left associativity). + + (* Believe it or not, this is a Turing-complete language! Here's an example + * nonterminating program. *) + Example omega := (\"x", "x" @ "x") @ (\"x", "x" @ "x"). + + + (** * Church Numerals, everyone's favorite example of lambda terms in + * action *) + + (* Here are two curious definitions. *) + Definition zero := \"f", \"x", "x". + Definition plus1 := \"n", \"f", \"x", "f" @ ("n" @ "f" @ "x"). + + (* We can build up any natural number [n] as [plus1^n @ zero]. Let's prove + * that, in fact, these definitions constitute a workable embedding of the + * natural numbers in lambda-calculus. *) + + (* A term [plus^n @ zero] evaluates to something very close to what this + * function returns. *) + Fixpoint canonical' (n : nat) : exp := + match n with + | O => "x" + | S n' => "f" @ ((\"f", \"x", canonical' n') @ "f" @ "x") + end. + + (* This missing piece is this wrapper. *) + Definition canonical n := \"f", \"x", canonical' n. + + (* Let's formalize our definition of what it means to represent a number. *) + Definition represents (e : exp) (n : nat) := + eval e (canonical n). + + (* Zero passes the test. *) + Theorem zero_ok : represents zero 0. + Proof. + unfold zero, represents, canonical. + simplify. + econstructor. + Qed. + + (* So does our successor operation. *) + Theorem plus1_ok : forall e n, represents e n + -> represents (plus1 @ e) (S n). + Proof. + unfold plus1, represents, canonical; simplify. + econstructor. + econstructor. + eassumption. + simplify. + econstructor. + Qed. + + (* What's basically going on here? The representation of number [n] is [N] + * such that, for any function [f]: + * N(f) = f^n + * That is, we represent a number as its repeated-composition operator. + * So, given a number, we can use it to repeat any operation. In particular, + * to implement addition, we can just repeat [plus1]! *) + Definition add := \"n", \"m", "n" @ plus1 @ "m". + + (* Our addition works properly on this test case. *) + Example add_1_2 : exists v, + eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v + /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v. + Proof. + eexists; propositional. + repeat (econstructor; simplify). + repeat econstructor. + Qed. + + (* By the way: since [canonical'] doesn't mention variable "m", substituting + * for "m" has no effect. This fact will come in handy shortly. *) + Lemma subst_m_canonical' : forall m n, + subst m "m" (canonical' n) = canonical' n. + Proof. + induct n; simplify; equality. + Qed. + + (* This inductive proof is the workhorse for the next result, so let's skip + * ahead there. *) + Lemma add_ok' : forall m n, + eval + (subst (\ "f", (\ "x", canonical' m)) "x" + (subst (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x")))) "f" + (canonical' n))) (canonical (n + m)). + Proof. + induct n; simplify. + + econstructor. + + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + simplify. + econstructor. + econstructor. + simplify. + eassumption. + + simplify. + econstructor. + Qed. + + (* [add] properly encodes the usual addition. *) + Theorem add_ok : forall n ne m me, + represents ne n + -> represents me m + -> represents (add @ ne @ me) (n + m). + Proof. + unfold represents; simplify. + + econstructor. + econstructor. + econstructor. + eassumption. + simplify. + econstructor. + eassumption. + simplify. + econstructor. + econstructor. + econstructor. + econstructor. + simplify. + econstructor. + econstructor. + rewrite subst_m_canonical'. + apply add_ok'. + Qed. + + (* Let's repeat the same exercise for multiplication. *) + + Definition mult := \"n", \"m", "n" @ (add @ "m") @ zero. + + Example mult_1_2 : exists v, + eval (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v + /\ eval (plus1 @ (plus1 @ zero)) v. + Proof. + eexists; propositional. + repeat (econstructor; simplify). + repeat econstructor. + Qed. + + Lemma mult_ok' : forall m n, + eval + (subst (\ "f", (\ "x", "x")) "x" + (subst + (\ "m", + ((\ "f", (\ "x", canonical' m)) @ + (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x"))))) @ "m") + "f" (canonical' n))) (canonical (n * m)). + Proof. + induct n; simplify. + + econstructor. + + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + simplify. + econstructor. + econstructor. + simplify. + eassumption. + + simplify. + econstructor. + econstructor. + econstructor. + econstructor. + simplify. + econstructor. + econstructor. + rewrite subst_m_canonical'. + apply add_ok'. (* Note the recursive appeal to correctness of [add]. *) + Qed. + + Theorem mult_ok : forall n ne m me, + represents ne n + -> represents me m + -> represents (mult @ ne @ me) (n * m). + Proof. + unfold represents; simplify. + + econstructor. + econstructor. + econstructor. + eassumption. + simplify. + econstructor. + eassumption. + simplify. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + simplify. + econstructor. + simplify. + econstructor. + econstructor. + simplify. + rewrite subst_m_canonical'. + apply mult_ok'. + Qed. + + + (** * Small-step semantics with evaluation contexts *) + + Inductive context : Set := + | Hole : context + | App1 : context -> exp -> context + | App2 : exp -> context -> context. + + Inductive plug : context -> exp -> exp -> Prop := + | PlugHole : forall e, + plug Hole e e + | PlugApp1 : forall c e1 e2 e, + plug c e1 e + -> plug (App1 c e2) e1 (App e e2) + | PlugApp2 : forall c e1 e2 e, + value e1 + -> plug c e2 e + -> plug (App2 e1 c) e2 (App e1 e). + + Inductive step : exp -> exp -> Prop := + | ContextBeta : forall c x e v e1 e2, + value v + -> plug c (App (Abs x e) v) e1 + -> plug c (subst v x e) e2 + -> step e1 e2. + + Hint Constructors plug step. + + (* Here we now go through a proof of equivalence between big- and small-step + * semantics, though we won't spend any further commentary on it. *) + + Lemma step_eval'' : forall v c x e e1 e2 v0, + value v + -> plug c (App (Abs x e) v) e1 + -> plug c (subst v x e) e2 + -> eval e2 v0 + -> eval e1 v0. + Proof. + induct c; invert 2; invert 1; simplify; eauto. + invert H0; eauto. + invert H0; eauto. + Qed. + + Hint Resolve step_eval''. + + Lemma step_eval' : forall e1 e2, + step e1 e2 + -> forall v, eval e2 v + -> eval e1 v. + Proof. + invert 1; simplify; eauto. + Qed. + + Hint Resolve step_eval'. + + Theorem step_eval : forall e v, + step^* e v + -> value v + -> eval e v. + Proof. + induct 1; eauto. + Qed. + + Lemma plug_functional : forall C e e1, + plug C e e1 + -> forall e2, plug C e e2 + -> e1 = e2. + Proof. + induct 1; invert 1; simplify; try f_equal; eauto. + Qed. + + Lemma plug_mirror : forall C e e', plug C e e' + -> forall e1, exists e1', plug C e1 e1'. + Proof. + induct 1; simplify; eauto. + + specialize (IHplug e0); first_order; eauto. + + specialize (IHplug e0); first_order; eauto. + Qed. + + Fixpoint compose (C1 C2 : context) : context := + match C2 with + | Hole => C1 + | App1 C2' e => App1 (compose C1 C2') e + | App2 v C2' => App2 v (compose C1 C2') + end. + + Lemma compose_ok : forall C1 C2 e1 e2 e3, + plug C1 e1 e2 + -> plug C2 e2 e3 + -> plug (compose C1 C2) e1 e3. + Proof. + induct 2; simplify; eauto. + Qed. + + Hint Resolve compose_ok. + + Lemma step_plug : forall e1 e2, + step e1 e2 + -> forall C e1' e2', plug C e1 e1' + -> plug C e2 e2' + -> step e1' e2'. + Proof. + invert 1; simplify; eauto. + Qed. + + Lemma stepStar_plug : forall e1 e2, + step^* e1 e2 + -> forall C e1' e2', plug C e1 e1' + -> plug C e2 e2' + -> step^* e1' e2'. + Proof. + induct 1; simplify. + + assert (e1' = e2') by (eapply plug_functional; eassumption). + subst. + constructor. + + assert (exists y', plug C y y') by eauto using plug_mirror. + invert H3. + eapply step_plug in H. + econstructor. + eassumption. + eapply IHtrc. + eassumption. + assumption. + eassumption. + assumption. + Qed. + + Hint Resolve stepStar_plug eval_value. + + Theorem eval_step : forall e v, + eval e v + -> step^* e v. + Proof. + induct 1; eauto. + + eapply trc_trans. + eapply stepStar_plug with (e1 := e1) (e2 := Abs x e1') (C := App1 Hole e2); eauto. + eapply trc_trans. + eapply stepStar_plug with (e1 := e2) (e2 := v2) (C := App2 (Abs x e1') Hole); eauto. + eauto. + Qed. +End Ulc. + + +Module Stlc. + Inductive exp : Set := + | Var (x : var) + | Const (n : nat) + | Plus (e1 e2 : exp) + | Abs (x : var) (e1 : exp) + | App (e1 e2 : exp). + + Inductive value : exp -> Prop := + | VConst : forall n, value (Const n) + | VAbs : forall x e1, value (Abs x e1). + + Fixpoint subst (e1 : exp) (x : string) (e2 : exp) : exp := + match e2 with + | Var y => if y ==v x then e1 else Var y + | Const n => Const n + | Plus e2' e2'' => Plus (subst e1 x e2') (subst e1 x e2'') + | Abs y e2' => Abs y (if y ==v x then e2' else subst e1 x e2') + | App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'') + end. + + Inductive context : Set := + | Hole : context + | Plus1 : context -> exp -> context + | Plus2 : exp -> context -> context + | App1 : context -> exp -> context + | App2 : exp -> context -> context. + + Inductive plug : context -> exp -> exp -> Prop := + | PlugHole : forall e, plug Hole e e + | PlugPlus1 : forall e e' C e2, + plug C e e' + -> plug (Plus1 C e2) e (Plus e' e2) + | PlugPlus2 : forall e e' v1 C, + value v1 + -> plug C e e' + -> plug (Plus2 v1 C) e (Plus v1 e') + | PlugApp1 : forall e e' C e2, + plug C e e' + -> plug (App1 C e2) e (App e' e2) + | PlugApp2 : forall e e' v1 C, + value v1 + -> plug C e e' + -> plug (App2 v1 C) e (App v1 e'). + + Inductive step0 : exp -> exp -> Prop := + | Beta : forall x e v, + value v + -> step0 (App (Abs x e) v) (subst v x e) + | Add : forall n1 n2, + step0 (Plus (Const n1) (Const n2)) (Const (n1 + n2)). + + Inductive step : exp -> exp -> Prop := + | StepRule : forall C e1 e2 e1' e2', + plug C e1 e1' + -> plug C e2 e2' + -> step0 e1 e2 + -> step e1' e2'. + + Definition trsys_of (e : exp) := {| + Initial := {e}; + Step := step + |}. + + + Inductive type := + | Nat (* Numbers *) + | Fun (dom ran : type) (* Functions *). + + Inductive hasty : fmap var type -> exp -> type -> Prop := + | HtVar : forall G x t, + G $? x = Some t + -> hasty G (Var x) t + | HtConst : forall G n, + hasty G (Const n) Nat + | HtPlus : forall G e1 e2, + hasty G e1 Nat + -> hasty G e2 Nat + -> hasty G (Plus e1 e2) Nat + | HtAbs : forall G x e1 t1 t2, + hasty (G $+ (x, t1)) e1 t2 + -> hasty G (Abs x e1) (Fun t1 t2) + | HtApp : forall G e1 e2 t1 t2, + hasty G e1 (Fun t1 t2) + -> hasty G e2 t1 + -> hasty G (App e1 e2) t2. + + Hint Constructors value plug step0 step hasty. + + (* Some notation to make it more pleasant to write programs *) + Infix "-->" := Fun (at level 60, right associativity). + Coercion Const : nat >-> exp. + Infix "^+^" := Plus (at level 50). + Coercion Var : var >-> exp. + Notation "\ x , e" := (Abs x e) (at level 51). + Infix "@" := App (at level 49, left associativity). + + (* Some examples of typed programs *) + + Example one_plus_one : hasty $0 (1 ^+^ 1) Nat. + Proof. + repeat (econstructor; simplify). + Qed. + + Example add : hasty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat). + Proof. + repeat (econstructor; simplify). + Qed. + + Example eleven : hasty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat. + Proof. + repeat (econstructor; simplify). + Qed. + + Example seven_the_long_way : hasty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat. + Proof. + repeat (econstructor; simplify). + Qed. + + + (** * Let's prove type soundness. *) + + Definition unstuck e := value e + \/ (exists e' : exp, step e e'). + + (* For class, we'll stick with this magic tactic, to save proving time. *) + + Ltac t0 := match goal with + | [ H : ex _ |- _ ] => invert H + | [ H : _ /\ _ |- _ ] => invert H + | [ |- context[?x ==v ?y] ] => cases (x ==v y) + | [ H : Some _ = Some _ |- _ ] => invert H + + | [ H : step _ _ |- _ ] => invert H + | [ H : step0 _ _ |- _ ] => invert1 H + | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H + | [ H : hasty _ _ _ |- _ ] => invert1 H + | [ H : plug _ _ _ |- _ ] => invert1 H + end; subst. + + Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6. + + Lemma progress : forall e t, + hasty $0 e t + -> value e + \/ (exists e' : exp, step e e'). + Proof. + Admitted. + + (* Replacing a typing context with an equal one has no effect (useful to guide + * proof search as a hint). *) + Lemma hasty_change : forall G e t, + hasty G e t + -> forall G', G' = G + -> hasty G' e t. + Proof. + t. + Qed. + + Hint Resolve hasty_change. + + Lemma preservation : forall e1 e2, + step e1 e2 + -> forall t, hasty $0 e1 t + -> hasty $0 e2 t. + Proof. + Admitted. + + Theorem safety_snazzy : forall e t, hasty $0 e t + -> invariantFor (trsys_of e) unstuck. + Proof. + simplify. + + (* Step 1: strengthen the invariant. In particular, the typing relation is + * exactly the right stronger invariant! Our progress theorem proves the + * required invariant inclusion. *) + apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t). + + (* Step 2: apply invariant induction, whose induction step turns out to match + * our preservation theorem exactly! *) + apply invariant_induction; simplify. + equality. + + eapply preservation. + eassumption. + assumption. + + simplify. + eapply progress. + eassumption. + Qed. +End Stlc. diff --git a/_CoqProject b/_CoqProject index 19e563f..7ce48d1 100644 --- a/_CoqProject +++ b/_CoqProject @@ -19,4 +19,5 @@ ModelChecking.v OperationalSemantics_template.v OperationalSemantics.v AbstractInterpretation.v +LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness.v diff --git a/frap_book.tex b/frap_book.tex index 80980d5..6c7dc61 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -2072,7 +2072,7 @@ Notice a peculiar property of this definition when we work with \emph{open} term According to the definition $\subst{\lambda x. \; y}{y}{x} = \lambda x. \; x$. In this example, we say that $\lambda$-bound variable $x$ has been \emph{captured}\index{variable capture} unintentionally, where substitution created a reference to that $\lambda$ where none existed before. Such a problem can only arise when replacing a variable with an open term. -In this case, that term is $y$, where $\fv{y} = \{y\} \neq \emptyset$. +In this case, that term is $x$, where $\fv{x} = \{x\} \neq \emptyset$. More general investigations into $\lambda$-calculus will define a more involved notion of \emph{capture-avoiding} substitution\index{capture-avoiding substitution}. Instead, in this book, we carefully steer clear of the $\lambda$-calculus applications that require substituting open terms for variables, letting us stick with the simpler definiton.