From 8d1cecf7f77582fcb0a30c05a76b4fcd4b281a06 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 27 Mar 2021 20:26:37 -0400
Subject: [PATCH] EvaluationContexts: determinism

---
 EvaluationContexts.v | 76 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)

diff --git a/EvaluationContexts.v b/EvaluationContexts.v
index 1a0f11c..0beaf26 100644
--- a/EvaluationContexts.v
+++ b/EvaluationContexts.v
@@ -6,6 +6,11 @@
 Require Import Frap.
 
 
+(** * Evaluation Contexts for Lambda Calculus *)
+
+(* Let's revisit the typed language from the end of the previous chapter, this
+ * time casting its small-step semantics using evaluation contexts. *)
+
 Module Stlc.
   Inductive exp : Set :=
   | Var (x : var)
@@ -27,6 +32,10 @@ Module Stlc.
       | App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'')
     end.
 
+  (* Here's the first difference from last chapter.  This is our grammar of
+   * contexts.  Note a difference from the book: we don't enforce here that
+   * the first argument of a [Plus1] or [App1] is a value, but rather that
+   * constraint comes in the next relation definition. *)
   Inductive context : Set :=
   | Hole : context
   | Plus1 : context -> exp -> context
@@ -34,6 +43,7 @@ Module Stlc.
   | App1 : context -> exp -> context
   | App2 : exp -> context -> context.
 
+  (* Again, note how two of the rules include [value] premises. *)
   Inductive plug : context -> exp -> exp -> Prop :=
   | PlugHole : forall e, plug Hole e e
   | PlugPlus1 : forall e e' C e2,
@@ -217,4 +227,70 @@ Module Stlc.
     apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
+
+  (* It may not be obvious that this way of defining the semantics gives us a
+   * unique evaluation sequence for every well-typed program.  Let's prove
+   * it. *)
+
+  Lemma plug_not_value : forall C e v,
+      value v
+      -> plug C e v
+      -> C = Hole /\ e = v.
+  Proof.
+    invert 1; invert 1; auto.
+  Qed.
+
+  Lemma step0_value : forall v e,
+      value v
+      -> step0 v e
+      -> False.
+  Proof.
+    invert 1; invert 1.
+  Qed.
+  
+  Lemma plug_det : forall C e1 e2 e1' f1 f1',
+      step0 e1 e1'
+      -> step0 f1 f1'
+      -> plug C e1 e2
+      -> forall C', plug C' f1 e2
+      -> C = C' /\ e1 = f1.
+  Proof.
+    induct 3; invert 1;
+      repeat match goal with
+             | [ H : step0 _ _ |- _ ] => invert1 H
+             | [ H : plug _ _ _ |- _ ] => eapply plug_not_value in H; [ | solve [ eauto ] ];
+                                            propositional; subst
+             | [ IH : step0 _ _ -> _, H : plug _ _ _ |- _ ] => eapply IH in H; [ | solve [ auto ] ];
+                                                                 equality
+             | [ _ : value ?v, _ : step0 ?v _ |- _ ] => exfalso; eapply step0_value; eauto
+             end; equality.
+  Qed.
+
+  Lemma step0_det : forall e e', step0 e e'
+                                 -> forall e'', step0 e e''
+                                                -> e' = e''.
+  Proof.
+    invert 1; invert 1; auto.
+  Qed.
+  
+  Lemma plug_func : forall C e e1,
+      plug C e e1
+      -> forall e2, plug C e e2
+                    -> e1 = e2.
+  Proof.
+    induct 1; invert 1; auto; f_equal; auto.
+  Qed.
+
+  Theorem deterministic : forall e e', step e e'
+                                       -> forall e'', step e e''
+                                                      -> e' = e''.
+  Proof.
+    invert 1; invert 1.
+
+    assert (C = C0 /\ e1 = e0) by (eapply plug_det; eassumption).
+    propositional; subst.
+    assert (e2 = e3) by (eapply step0_det; eassumption).
+    subst.
+    eapply plug_func; eassumption.
+  Qed.    
 End Stlc.