LambdaCalculusAndTypeSoundness: untyped lambda calculus semantics, two ways

LambdaCalculusAndTypeSoundness.v

@@ -5,6 +5,213 @@
 
 Require Import Frap.
 
+Module Ulc.
+  Inductive exp : Set :=
+  | Var : var -> exp
+  | Abs : var -> exp -> exp
+  | App : exp -> exp -> exp.
+
+  Fixpoint subst (rep : exp) (x : string) (e : exp) : exp :=
+    match e with
+    | Var y => if string_dec y x then rep else Var y
+    | Abs y e1 => Abs y (if string_dec y x then e1 else subst rep x e1)
+    | App e1 e2 => App (subst rep x e1) (subst rep x e2)
+    end.
+
+
+  (** * Big-step semantics *)
+
+  (** This is the most straightforward way to give semantics to lambda terms:
+    * We evaluate any closed term into a value (that is, an [Abs]). *)
+  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.
+
+  (** Note that we omit a [Var] case, since variable terms can't be *closed*. *)
+
+
+  (** Which terms are values, that is, final results of execution? *)
+  Inductive value : exp -> Prop :=
+  | Value : forall x e, value (Abs x e).
+  (** We're cheating a bit here, *assuming* that the term is also closed. *)
+
+  Hint Constructors eval value.
+
+  (** Actually, let's prove that [eval] only produces values. *)
+  Theorem eval_value : forall e v,
+    eval e v
+    -> value v.
+  Proof.
+    induct 1; eauto.
+  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).
+  (* Subtle point: the [value] hypothesis right above enforces a well-formedness
+   * condition on contexts that may actually be plugged.  We don't allow
+   * skipping over a lefthand subterm of an application when that term has
+   * evaluation work left to do.  This condition is the essence of
+   * *call-by-value* instead of other evaluation strategies.  Details are
+   * largely beyond our scope here. *)
+
+  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.
+
+  (** We can move directly to establishing inclusion from basic small steps to contextual small steps. *)
+
+  Theorem value_eval : forall v,
+    value v
+    -> eval v v.
+  Proof.
+    invert 1; eauto.
+  Qed.
+
+  Hint Resolve value_eval.
+
+  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.
   (* Expression syntax *)
   Inductive exp : Set :=
   | Var (x : var)
@@ -519,3 +726,4 @@ Proof.
     apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
+End Stlc.