Mercurial > cpdt > repo

comparison src/Firstorder.v @ 154:358dcb6e08f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Progress and preservation
author Adam Chlipala <adamc@hcoop.net>
date Sun, 02 Nov 2008 13:14:08 -0500
parents 8c19768f1a1a
children b31ca896f211
comparison
equal deleted inserted replaced
153:8c19768f1a1a 154:358dcb6e08f2
294 intros; change (nil ++ nil |-e subst e2 : t); 294 intros; change (nil ++ nil |-e subst e2 : t);
295 eapply subst_hasType; eauto. 295 eapply subst_hasType; eauto.
296 Qed. 296 Qed.
297 End subst. 297 End subst.
298 298
299 Hint Resolve subst_hasType_closed.
300
301 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
302
303 Inductive val : exp -> Prop :=
304 | VConst : forall b, val (Const b)
305 | VAbs : forall x e, val (Abs x e).
306
307 Hint Constructors val.
308
309 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
310
311 Inductive step : exp -> exp -> Prop :=
312 | Beta : forall x e1 e2,
313 App (Abs x e1) e2 ==> [x ~> e2] e1
314 | Cong1 : forall e1 e2 e1',
315 e1 ==> e1'
316 -> App e1 e2 ==> App e1' e2
317 | Cong2 : forall e1 e2 e2',
318 val e1
319 -> e2 ==> e2'
320 -> App e1 e2 ==> App e1 e2'
321
322 where "e1 ==> e2" := (step e1 e2).
323
324 Hint Constructors step.
325
326 Theorem progress : forall G e t, G |-e e : t
327 -> G = nil
328 -> val e \/ exists e', e ==> e'.
329 induction 1; crush; eauto;
330 try match goal with
331 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
332 end;
333 repeat match goal with
334 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
335 end.
336 Qed.
337
338 Theorem preservation : forall G e t, G |-e e : t
339 -> G = nil
340 -> forall e', e ==> e'
341 -> G |-e e' : t.
342 induction 1; inversion 2; crush; eauto;
343 match goal with
344 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
345 end; eauto.
346 Qed.
347
299 End Concrete. 348 End Concrete.