Mercurial > cpdt > repo

changeset 161:6087a32b1926

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Firstorder clean-ups after class
author Adam Chlipala <adamc@hcoop.net>
date Tue, 04 Nov 2008 11:23:20 -0500
parents 56e205f966cc
children df02642f93b8
files src/Firstorder.v
diffstat 1 files changed, 6 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/Firstorder.v	Mon Nov 03 14:47:46 2008 -0500
+++ b/src/Firstorder.v	Tue Nov 04 11:23:20 2008 -0500
@@ -102,13 +102,7 @@
       eapply weaken_hasType'; eauto.
   Qed.
 
-  Theorem weaken_hasType_closed : forall e t,
-    nil |-e e : t
-    -> forall G, G |-e e : t.
-    intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
-  Qed.
-
-  Hint Resolve weaken_hasType_closed.
+  Hint Resolve weaken_hasType.
 
   Section subst.
     Variable x : var.
@@ -243,7 +237,8 @@
 
   Inductive step : exp -> exp -> Prop :=
   | Beta : forall x e1 e2,
-    App (Abs x e1) e2 ==> [x ~> e2] e1
+    val e2
+    -> App (Abs x e1) e2 ==> [x ~> e2] e1
   | Cong1 : forall e1 e2 e1',
     e1 ==> e1'
     -> App e1 e2 ==> App e1' e2
@@ -367,13 +362,7 @@
       eapply weaken_hasType'; eauto.
   Qed.
 
-  Theorem weaken_hasType_closed : forall e t,
-    nil |-e e : t
-    -> forall G, G |-e e : t.
-    intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
-  Qed.
-
-  Hint Resolve weaken_hasType_closed.
+  Hint Resolve weaken_hasType.
 
   Section subst.
     Variable e1 : exp.
@@ -465,7 +454,8 @@
 
   Inductive step : exp -> exp -> Prop :=
   | Beta : forall e1 e2,
-    App (Abs e1) e2 ==> [O ~> e2] e1
+    val e2
+    -> App (Abs e1) e2 ==> [O ~> e2] e1
   | Cong1 : forall e1 e2 e1',
     e1 ==> e1'
     -> App e1 e2 ==> App e1' e2