Mercurial > cpdt > repo

comparison src/Firstorder.v @ 156:be15ed0a8bae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
De Bruijn
author Adam Chlipala <adamc@hcoop.net>
date Sun, 02 Nov 2008 13:51:51 -0500
parents b31ca896f211
children 2022e3f2aa26
comparison
equal deleted inserted replaced
155:b31ca896f211 156:be15ed0a8bae
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List String. 11 Require Import Arith String List.
12 12
13 Require Import Tactics. 13 Require Import Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
339 -> nil |-e e' : t. 339 -> nil |-e e' : t.
340 intros; eapply preservation'; eauto. 340 intros; eapply preservation'; eauto.
341 Qed. 341 Qed.
342 342
343 End Concrete. 343 End Concrete.
344
345
346 (** * De Bruijn Indices *)
347
348 Module DeBruijn.
349
350 Definition var := nat.
351 Definition var_eq := eq_nat_dec.
352
353 Inductive exp : Set :=
354 | Const : bool -> exp
355 | Var : var -> exp
356 | App : exp -> exp -> exp
357 | Abs : exp -> exp.
358
359 Inductive type : Set :=
360 | Bool : type
361 | Arrow : type -> type -> type.
362
363 Infix "-->" := Arrow (right associativity, at level 60).
364
365 Definition ctx := list type.
366
367 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
368
369 Inductive lookup : ctx -> var -> type -> Prop :=
370 | First : forall t G,
371 t :: G |-v O : t
372 | Next : forall x t t' G,
373 G |-v x : t
374 -> t' :: G |-v S x : t
375
376 where "G |-v x : t" := (lookup G x t).
377
378 Hint Constructors lookup.
379
380 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
381
382 Inductive hasType : ctx -> exp -> type -> Prop :=
383 | TConst : forall G b,
384 G |-e Const b : Bool
385 | TVar : forall G v t,
386 G |-v v : t
387 -> G |-e Var v : t
388 | TApp : forall G e1 e2 dom ran,
389 G |-e e1 : dom --> ran
390 -> G |-e e2 : dom
391 -> G |-e App e1 e2 : ran
392 | TAbs : forall G e' dom ran,
393 dom :: G |-e e' : ran
394 -> G |-e Abs e' : dom --> ran
395
396 where "G |-e e : t" := (hasType G e t).
397
398 Hint Constructors hasType.
399
400 Lemma weaken_lookup : forall G' v t G,
401 G |-v v : t
402 -> G ++ G' |-v v : t.
403 induction 1; crush.
404 Qed.
405
406 Hint Resolve weaken_lookup.
407
408 Theorem weaken_hasType' : forall G' G e t,
409 G |-e e : t
410 -> G ++ G' |-e e : t.
411 induction 1; crush; eauto.
412 Qed.
413
414 Theorem weaken_hasType : forall e t,
415 nil |-e e : t
416 -> forall G', G' |-e e : t.
417 intros; change G' with (nil ++ G');
418 eapply weaken_hasType'; eauto.
419 Qed.
420
421 Theorem weaken_hasType_closed : forall e t,
422 nil |-e e : t
423 -> forall G, G |-e e : t.
424 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
425 Qed.
426
427 Theorem weaken_hasType1 : forall e t,
428 nil |-e e : t
429 -> forall t', t' :: nil |-e e : t.
430 intros; change (t' :: nil) with ((t' :: nil) ++ nil);
431 apply weaken_hasType; crush.
432 Qed.
433
434 Hint Resolve weaken_hasType_closed weaken_hasType1.
435
436 Section subst.
437 Variable e1 : exp.
438
439 Fixpoint subst (x : var) (e2 : exp) : exp :=
440 match e2 with
441 | Const b => Const b
442 | Var x' =>
443 if var_eq x' x
444 then e1
445 else Var x'
446 | App e1 e2 => App (subst x e1) (subst x e2)
447 | Abs e' => Abs (subst (S x) e')
448 end.
449
450 Variable xt : type.
451
452 Lemma subst_eq : forall t G1,
453 G1 ++ xt :: nil |-v length G1 : t
454 -> t = xt.
455 induction G1; inversion 1; crush.
456 Qed.
457
458 Implicit Arguments subst_eq [t G1].
459
460 Lemma subst_eq' : forall t G1 x,
461 G1 ++ xt :: nil |-v x : t
462 -> x <> length G1
463 -> G1 |-v x : t.
464 induction G1; inversion 1; crush;
465 match goal with
466 | [ H : nil |-v _ : _ |- _ ] => inversion H
467 end.
468 Qed.
469
470 Hint Resolve subst_eq'.
471
472 Lemma subst_neq : forall v t G1,
473 G1 ++ xt :: nil |-v v : t
474 -> v <> length G1
475 -> G1 |-e Var v : t.
476 induction G1; inversion 1; crush.
477 Qed.
478
479 Hint Resolve subst_neq.
480
481 Hypothesis Ht' : nil |-e e1 : xt.
482
483 Lemma hasType_push : forall dom G1 e' ran,
484 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
485 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
486 trivial.
487 Qed.
488
489 Hint Resolve hasType_push.
490
491 Theorem subst_hasType : forall G e2 t,
492 G |-e e2 : t
493 -> forall G1, G = G1 ++ xt :: nil
494 -> G1 |-e subst (length G1) e2 : t.
495 induction 1; crush;
496 try match goal with
497 | [ |- context[if ?E then _ else _] ] => destruct E
498 end; crush; eauto 6;
499 try match goal with
500 | [ H : _ |-v _ : _ |- _ ] =>
501 rewrite (subst_eq H)
502 end; crush.
503 Qed.
504
505 Theorem subst_hasType_closed : forall e2 t,
506 xt :: nil |-e e2 : t
507 -> nil |-e subst O e2 : t.
508 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
509 Qed.
510 End subst.
511
512 Hint Resolve subst_hasType_closed.
513
514 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
515
516 Inductive val : exp -> Prop :=
517 | VConst : forall b, val (Const b)
518 | VAbs : forall e, val (Abs e).
519
520 Hint Constructors val.
521
522 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
523
524 Inductive step : exp -> exp -> Prop :=
525 | Beta : forall e1 e2,
526 App (Abs e1) e2 ==> [O ~> e2] e1
527 | Cong1 : forall e1 e2 e1',
528 e1 ==> e1'
529 -> App e1 e2 ==> App e1' e2
530 | Cong2 : forall e1 e2 e2',
531 val e1
532 -> e2 ==> e2'
533 -> App e1 e2 ==> App e1 e2'
534
535 where "e1 ==> e2" := (step e1 e2).
536
537 Hint Constructors step.
538
539 Lemma progress' : forall G e t, G |-e e : t
540 -> G = nil
541 -> val e \/ exists e', e ==> e'.
542 induction 1; crush; eauto;
543 try match goal with
544 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
545 end;
546 repeat match goal with
547 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
548 end.
549 Qed.
550
551 Theorem progress : forall e t, nil |-e e : t
552 -> val e \/ exists e', e ==> e'.
553 intros; eapply progress'; eauto.
554 Qed.
555
556 Lemma preservation' : forall G e t, G |-e e : t
557 -> G = nil
558 -> forall e', e ==> e'
559 -> nil |-e e' : t.
560 induction 1; inversion 2; crush; eauto;
561 match goal with
562 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
563 end; eauto.
564 Qed.
565
566 Theorem preservation : forall e t, nil |-e e : t
567 -> forall e', e ==> e'
568 -> nil |-e e' : t.
569 intros; eapply preservation'; eauto.
570 Qed.
571
572 End DeBruijn.