Mercurial > cpdt > repo

comparison src/Firstorder.v @ 246:cca30734ab40

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proved progress for LocallyNameless
author Adam Chlipala <adamc@hcoop.net>
date Fri, 11 Dec 2009 10:18:45 -0500
parents 4b001a611e79
children ecfa8eec3852
comparison
equal deleted inserted replaced
245:4b001a611e79 246:cca30734ab40
134 134
135 (** We are substituting expression [e1] for every free occurrence of [x]. Note that this definition is specialized to the case where [e1] is closed; substitution is substantially more complicated otherwise, potentially involving explicit alpha-variation. Luckily, our example of type safety for a call-by-value semantics only requires this restricted variety of substitution. *) 135 (** We are substituting expression [e1] for every free occurrence of [x]. Note that this definition is specialized to the case where [e1] is closed; substitution is substantially more complicated otherwise, potentially involving explicit alpha-variation. Luckily, our example of type safety for a call-by-value semantics only requires this restricted variety of substitution. *)
136 136
137 Fixpoint subst (e2 : exp) : exp := 137 Fixpoint subst (e2 : exp) : exp :=
138 match e2 with 138 match e2 with
139 | Const b => Const b 139 | Const _ => e2
140 | Var x' => 140 | Var x' => if var_eq x' x then e1 else e2
141 if var_eq x' x
142 then e1
143 else Var x'
144 | App e1 e2 => App (subst e1) (subst e2) 141 | App e1 e2 => App (subst e1) (subst e2)
145 | Abs x' e' => 142 | Abs x' e' => Abs x' (if var_eq x' x then e' else subst e')
146 Abs x' (if var_eq x' x
147 then e'
148 else subst e')
149 end. 143 end.
150 144
151 (** We can prove a few theorems about substitution in well-typed terms, where we assume that [e1] is closed and has type [xt]. *) 145 (** We can prove a few theorems about substitution in well-typed terms, where we assume that [e1] is closed and has type [xt]. *)
152 146
153 Variable xt : type. 147 Variable xt : type.
432 426
433 (** Substitution is easier to define than with concrete syntax. While our old definition needed to use two comparisons for equality of variables, the de Bruijn substitution only needs one comparison. *) 427 (** Substitution is easier to define than with concrete syntax. While our old definition needed to use two comparisons for equality of variables, the de Bruijn substitution only needs one comparison. *)
434 428
435 Fixpoint subst (x : var) (e2 : exp) : exp := 429 Fixpoint subst (x : var) (e2 : exp) : exp :=
436 match e2 with 430 match e2 with
437 | Const b => Const b 431 | Const _ => e2
438 | Var x' => 432 | Var x' => if var_eq x' x then e1 else e2
439 if var_eq x' x
440 then e1
441 else Var x'
442 | App e1 e2 => App (subst x e1) (subst x e2) 433 | App e1 e2 => App (subst x e1) (subst x e2)
443 | Abs e' => Abs (subst (S x) e') 434 | Abs e' => Abs (subst (S x) e')
444 end. 435 end.
445 436
446 Variable xt : type. 437 Variable xt : type.
575 -> nil |-e e' : t. 566 -> nil |-e e' : t.
576 intros; eapply preservation'; eauto. 567 intros; eapply preservation'; eauto.
577 Qed. 568 Qed.
578 569
579 End DeBruijn. 570 End DeBruijn.
571
572
573 (** * Locally Nameless Syntax *)
574
575 Module LocallyNameless.
576
577 Definition free_var := string.
578 Definition bound_var := nat.
579
580 Inductive exp : Set :=
581 | Const : bool -> exp
582 | FreeVar : free_var -> exp
583 | BoundVar : bound_var -> exp
584 | App : exp -> exp -> exp
585 | Abs : exp -> exp.
586
587 Inductive type : Set :=
588 | Bool : type
589 | Arrow : type -> type -> type.
590
591 Infix "-->" := Arrow (right associativity, at level 60).
592
593 Definition ctx := list (free_var * type).
594
595 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
596
597 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
598
599 Inductive lookup : ctx -> free_var -> type -> Prop :=
600 | First : forall x t G,
601 (x, t) :: G |-v x : t
602 | Next : forall x t x' t' G,
603 x <> x'
604 -> G |-v x : t
605 -> (x', t') :: G |-v x : t
606
607 where "G |-v x : t" := (lookup G x t).
608
609 Hint Constructors lookup.
610
611 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
612
613 Section open.
614 Variable x : free_var.
615
616 Fixpoint open (n : bound_var) (e : exp) : exp :=
617 match e with
618 | Const _ => e
619 | FreeVar _ => e
620 | BoundVar n' =>
621 if eq_nat_dec n' n
622 then FreeVar x
623 else if le_lt_dec n' n
624 then e
625 else BoundVar (pred n')
626 | App e1 e2 => App (open n e1) (open n e2)
627 | Abs e1 => Abs (open (S n) e1)
628 end.
629 End open.
630
631 Inductive notFreeIn (x : free_var) : exp -> Prop :=
632 | NfConst : forall c, notFreeIn x (Const c)
633 | NfFreeVar : forall y, y <> x -> notFreeIn x (FreeVar y)
634 | NfBoundVar : forall y, notFreeIn x (BoundVar y)
635 | NfApp : forall e1 e2, notFreeIn x e1 -> notFreeIn x e2 -> notFreeIn x (App e1 e2)
636 | NfAbs : forall e1, (forall y, y <> x -> notFreeIn x (open y O e1)) -> notFreeIn x (Abs e1).
637
638 Hint Constructors notFreeIn.
639
640 Inductive hasType : ctx -> exp -> type -> Prop :=
641 | TConst : forall G b,
642 G |-e Const b : Bool
643 | TFreeVar : forall G v t,
644 G |-v v : t
645 -> G |-e FreeVar v : t
646 | TApp : forall G e1 e2 dom ran,
647 G |-e e1 : dom --> ran
648 -> G |-e e2 : dom
649 -> G |-e App e1 e2 : ran
650 | TAbs : forall G e' dom ran,
651 (forall x, notFreeIn x e' -> (x, dom) :: G |-e open x O e' : ran)
652 -> G |-e Abs e' : dom --> ran
653
654 where "G |-e e : t" := (hasType G e t).
655
656 Hint Constructors hasType.
657
658 (** We prove roughly the same weakening theorems as before. *)
659
660 Lemma weaken_lookup : forall G' v t G,
661 G |-v v : t
662 -> G ++ G' |-v v : t.
663 induction 1; crush.
664 Qed.
665
666 Hint Resolve weaken_lookup.
667
668 Theorem weaken_hasType' : forall G' G e t,
669 G |-e e : t
670 -> G ++ G' |-e e : t.
671 induction 1; crush; eauto.
672 Qed.
673
674 Theorem weaken_hasType : forall e t,
675 nil |-e e : t
676 -> forall G', G' |-e e : t.
677 intros; change G' with (nil ++ G');
678 eapply weaken_hasType'; eauto.
679 Qed.
680
681 Hint Resolve weaken_hasType.
682
683 Section subst.
684 Variable x : free_var.
685 Variable e1 : exp.
686
687 Fixpoint subst (e2 : exp) : exp :=
688 match e2 with
689 | Const _ => e2
690 | FreeVar x' => if string_dec x' x then e1 else e2
691 | BoundVar _ => e2
692 | App e1 e2 => App (subst e1) (subst e2)
693 | Abs e' => Abs (subst e')
694 end.
695 End subst.
696
697
698 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
699
700 Inductive val : exp -> Prop :=
701 | VConst : forall b, val (Const b)
702 | VAbs : forall e, val (Abs e).
703
704 Hint Constructors val.
705
706 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
707
708 Inductive step : exp -> exp -> Prop :=
709 | Beta : forall x e1 e2,
710 val e2
711 -> notFreeIn x e1
712 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
713 | Cong1 : forall e1 e2 e1',
714 e1 ==> e1'
715 -> App e1 e2 ==> App e1' e2
716 | Cong2 : forall e1 e2 e2',
717 val e1
718 -> e2 ==> e2'
719 -> App e1 e2 ==> App e1 e2'
720
721 where "e1 ==> e2" := (step e1 e2).
722
723 Hint Constructors step.
724
725 Open Scope string_scope.
726
727 Fixpoint vlen (e : exp) : nat :=
728 match e with
729 | Const _ => 0
730 | FreeVar x => String.length x
731 | BoundVar _ => 0
732 | App e1 e2 => vlen e1 + vlen e2
733 | Abs e1 => vlen e1
734 end.
735
736 Opaque le_lt_dec.
737
738 Hint Extern 1 (@eq exp _ _) => f_equal.
739
740 Lemma open_comm : forall x1 x2 e n1 n2,
741 open x1 n1 (open x2 (S n2 + n1) e)
742 = open x2 (n2 + n1) (open x1 n1 e).
743 induction e; crush;
744 repeat (match goal with
745 | [ |- context[if ?E then _ else _] ] => destruct E
746 end; crush).
747
748 replace (S (n2 + n1)) with (n2 + S n1); auto.
749 Qed.
750
751 Hint Rewrite plus_0_r : cpdt.
752
753 Lemma open_comm0 : forall x1 x2 e n,
754 open x1 0 (open x2 (S n) e)
755 = open x2 n (open x1 0 e).
756 intros; generalize (open_comm x1 x2 e 0 n); crush.
757 Qed.
758
759 Hint Extern 1 (notFreeIn _ (open _ 0 (open _ (S _) _))) => rewrite open_comm0.
760
761 Lemma notFreeIn_open : forall x y,
762 x <> y
763 -> forall e,
764 notFreeIn x e
765 -> forall n, notFreeIn x (open y n e).
766 induction 2; crush;
767 repeat (match goal with
768 | [ |- context[if ?E then _ else _] ] => destruct E
769 end; crush).
770 Qed.
771
772 Hint Resolve notFreeIn_open.
773
774 Lemma infVar : forall x y, String.length x > String.length y
775 -> y <> x.
776 intros; destruct (string_dec x y); intros; subst; crush.
777 Qed.
778
779 Hint Resolve infVar.
780
781 Lemma inf' : forall x e, String.length x > vlen e -> notFreeIn x e.
782 induction e; crush; eauto.
783 Qed.
784
785 Fixpoint primes (n : nat) : string :=
786 match n with
787 | O => "x"
788 | S n' => primes n' ++ "'"
789 end.
790
791 Lemma length_app : forall s2 s1, String.length (s1 ++ s2) = String.length s1 + String.length s2.
792 induction s1; crush.
793 Qed.
794
795 Hint Rewrite length_app : cpdt.
796
797 Lemma length_primes : forall n, String.length (primes n) = S n.
798 induction n; crush.
799 Qed.
800
801 Hint Rewrite length_primes : cpdt.
802
803 Lemma inf : forall e, exists x, notFreeIn x e.
804 intro; exists (primes (vlen e)); apply inf'; crush.
805 Qed.
806
807 Lemma progress_Abs : forall e1 e2,
808 val e2
809 -> exists e', App (Abs e1) e2 ==> e'.
810 intros; destruct (inf e1); eauto.
811 Qed.
812
813 Hint Resolve progress_Abs.
814
815 Lemma progress' : forall G e t, G |-e e : t
816 -> G = nil
817 -> val e \/ exists e', e ==> e'.
818 induction 1; crush; eauto;
819 try match goal with
820 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
821 end;
822 repeat match goal with
823 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
824 end.
825 Qed.
826
827 Theorem progress : forall e t, nil |-e e : t
828 -> val e \/ exists e', e ==> e'.
829 intros; eapply progress'; eauto.
830 Qed.
831
832 (*Lemma preservation' : forall G e t, G |-e e : t
833 -> G = nil
834 -> forall e', e ==> e'
835 -> nil |-e e' : t.
836 induction 1; inversion 2; crush; eauto;
837 match goal with
838 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
839 end; eauto.
840 Qed.
841
842 Theorem preservation : forall e t, nil |-e e : t
843 -> forall e', e ==> e'
844 -> nil |-e e' : t.
845 intros; eapply preservation'; eauto.
846 Qed.*)
847
848 End LocallyNameless.