Mercurial > cpdt > repo

comparison src/Firstorder.v @ 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 2022e3f2aa26
children 02569049397b
comparison
equal deleted inserted replaced
160:56e205f966cc 161:6087a32b1926
100 -> forall G', G' |-e e : t. 100 -> forall G', G' |-e e : t.
101 intros; change G' with (nil ++ G'); 101 intros; change G' with (nil ++ G');
102 eapply weaken_hasType'; eauto. 102 eapply weaken_hasType'; eauto.
103 Qed. 103 Qed.
104 104
105 Theorem weaken_hasType_closed : forall e t, 105 Hint Resolve weaken_hasType.
106 nil |-e e : t
107 -> forall G, G |-e e : t.
108 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
109 Qed.
110
111 Hint Resolve weaken_hasType_closed.
112 106
113 Section subst. 107 Section subst.
114 Variable x : var. 108 Variable x : var.
115 Variable e1 : exp. 109 Variable e1 : exp.
116 110
241 235
242 Reserved Notation "e1 ==> e2" (no associativity, at level 90). 236 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
243 237
244 Inductive step : exp -> exp -> Prop := 238 Inductive step : exp -> exp -> Prop :=
245 | Beta : forall x e1 e2, 239 | Beta : forall x e1 e2,
246 App (Abs x e1) e2 ==> [x ~> e2] e1 240 val e2
241 -> App (Abs x e1) e2 ==> [x ~> e2] e1
247 | Cong1 : forall e1 e2 e1', 242 | Cong1 : forall e1 e2 e1',
248 e1 ==> e1' 243 e1 ==> e1'
249 -> App e1 e2 ==> App e1' e2 244 -> App e1 e2 ==> App e1' e2
250 | Cong2 : forall e1 e2 e2', 245 | Cong2 : forall e1 e2 e2',
251 val e1 246 val e1
365 -> forall G', G' |-e e : t. 360 -> forall G', G' |-e e : t.
366 intros; change G' with (nil ++ G'); 361 intros; change G' with (nil ++ G');
367 eapply weaken_hasType'; eauto. 362 eapply weaken_hasType'; eauto.
368 Qed. 363 Qed.
369 364
370 Theorem weaken_hasType_closed : forall e t, 365 Hint Resolve weaken_hasType.
371 nil |-e e : t
372 -> forall G, G |-e e : t.
373 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
374 Qed.
375
376 Hint Resolve weaken_hasType_closed.
377 366
378 Section subst. 367 Section subst.
379 Variable e1 : exp. 368 Variable e1 : exp.
380 369
381 Fixpoint subst (x : var) (e2 : exp) : exp := 370 Fixpoint subst (x : var) (e2 : exp) : exp :=
463 452
464 Reserved Notation "e1 ==> e2" (no associativity, at level 90). 453 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
465 454
466 Inductive step : exp -> exp -> Prop := 455 Inductive step : exp -> exp -> Prop :=
467 | Beta : forall e1 e2, 456 | Beta : forall e1 e2,
468 App (Abs e1) e2 ==> [O ~> e2] e1 457 val e2
458 -> App (Abs e1) e2 ==> [O ~> e2] e1
469 | Cong1 : forall e1 e2 e1', 459 | Cong1 : forall e1 e2 e1',
470 e1 ==> e1' 460 e1 ==> e1'
471 -> App e1 e2 ==> App e1' e2 461 -> App e1 e2 ==> App e1' e2
472 | Cong2 : forall e1 e2 e2', 462 | Cong2 : forall e1 e2 e2',
473 val e1 463 val e1