Mercurial > cpdt > repo
diff src/Firstorder.v @ 161:6087a32b1926
Firstorder clean-ups after class
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 04 Nov 2008 11:23:20 -0500 |
| parents | 2022e3f2aa26 |
| children | 02569049397b |
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