From 4388ecc80e41fe050b6cef3dcad4b79c9d6ab451 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 1 Apr 2018 13:06:47 -0400
Subject: [PATCH] Revising LambdaCalculusAndTypeSoundness

---
 LambdaCalculusAndTypeSoundness.v          | 11 ++++++-----
 LambdaCalculusAndTypeSoundness_template.v | 22 ++--------------------
 2 files changed, 8 insertions(+), 25 deletions(-)

diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v
index 5903a3f..f3ecd14 100644
--- a/LambdaCalculusAndTypeSoundness.v
+++ b/LambdaCalculusAndTypeSoundness.v
@@ -27,7 +27,7 @@ Module Ulc.
    * discussion. *)
   Fixpoint subst (rep : exp) (x : var) (e : exp) : exp :=
     match e with
-    | Var y => if string_dec y x then rep else Var y
+    | Var y => if y ==v 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.
@@ -49,10 +49,10 @@ Module Ulc.
   (* Note that we omit a [Var] case, since variable terms can't be *closed*,
    * and therefore they aren't meaningful as top-level programs. *)
 
-  (** Which terms are values, that is, final results of execution? *)
+  (* 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. *)
+  (* We're cheating a bit here, *assuming* that the term is also closed. *)
 
   Hint Constructors eval value.
 
@@ -66,7 +66,7 @@ Module Ulc.
 
   Hint Resolve value_eval.
 
-  (** Conversely, let's prove that [eval] only produces values. *)
+  (* Conversely, let's prove that [eval] only produces values. *)
   Theorem eval_value : forall e v,
     eval e v
     -> value v.
@@ -467,7 +467,8 @@ End Ulc.
 
 (** * Now we turn to a variant of lambda calculus with static type-checking.
     * This variant is called *simply typed* lambda calculus, and *simple* has a
-    * technical meaning, which we will explore relaxing in a problem set. *)
+    * technical meaning, basically meaning "no polymorphism" in the sense of
+    * example file Polymorphism.v from this book. *)
 Module Stlc.
   (* We add expression forms for numeric constants and addition. *)
   Inductive exp : Set :=
diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v
index 1c5ab96..e3af65e 100644
--- a/LambdaCalculusAndTypeSoundness_template.v
+++ b/LambdaCalculusAndTypeSoundness_template.v
@@ -17,7 +17,7 @@ Module Ulc.
 
   Fixpoint subst (rep : exp) (x : var) (e : exp) : exp :=
     match e with
-    | Var y => if string_dec y x then rep else Var y
+    | Var y => if y ==v 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.
@@ -548,23 +548,6 @@ Module Stlc.
   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
@@ -579,8 +562,7 @@ Module Stlc.
     -> forall G', G' = G
       -> hasty G' e t.
   Proof.
-    t.
-  Qed.
+  Admitted.
 
   Hint Resolve hasty_change.