Mercurial > cpdt > repo

comparison src/Hoas.v @ 159:8b2b652ab0ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add Plus
author Adam Chlipala <adamc@hcoop.net>
date Mon, 03 Nov 2008 09:50:22 -0500
parents fabfaa93c9ea
children 56e205f966cc
comparison
equal deleted inserted replaced
158:fabfaa93c9ea 159:8b2b652ab0ee
22 22
23 23
24 (** * Parametric Higher-Order Abstract Syntax *) 24 (** * Parametric Higher-Order Abstract Syntax *)
25 25
26 Inductive type : Type := 26 Inductive type : Type :=
27 | Bool : type 27 | Nat : type
28 | Arrow : type -> type -> type. 28 | Arrow : type -> type -> type.
29 29
30 Infix "-->" := Arrow (right associativity, at level 60). 30 Infix "-->" := Arrow (right associativity, at level 60).
31 31
32 Section exp. 32 Section exp.
33 Variable var : type -> Type. 33 Variable var : type -> Type.
34 34
35 Inductive exp : type -> Type := 35 Inductive exp : type -> Type :=
36 | Const' : bool -> exp Bool 36 | Const' : nat -> exp Nat
37 | Plus' : exp Nat -> exp Nat -> exp Nat
38
37 | Var : forall t, var t -> exp t 39 | Var : forall t, var t -> exp t
38 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran 40 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
39 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran). 41 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
40 End exp. 42 End exp.
41 43
44 Implicit Arguments Abs' [var dom ran]. 46 Implicit Arguments Abs' [var dom ran].
45 47
46 Definition Exp t := forall var, exp var t. 48 Definition Exp t := forall var, exp var t.
47 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2. 49 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
48 50
49 Definition Const (b : bool) : Exp Bool := 51 Definition Const (n : nat) : Exp Nat :=
50 fun _ => Const' b. 52 fun _ => Const' n.
53 Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
54 fun _ => Plus' (E1 _) (E2 _).
51 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := 55 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
52 fun _ => App' (F _) (X _). 56 fun _ => App' (F _) (X _).
53 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := 57 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
54 fun _ => Abs' (B _). 58 fun _ => Abs' (B _).
55 59
56 Section flatten. 60 Section flatten.
57 Variable var : type -> Type. 61 Variable var : type -> Type.
58 62
59 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t := 63 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
60 match e in exp _ t return exp _ t with 64 match e in exp _ t return exp _ t with
61 | Const' b => Const' b 65 | Const' n => Const' n
66 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
62 | Var _ e' => e' 67 | Var _ e' => e'
63 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2) 68 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
64 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x))) 69 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
65 end. 70 end.
66 End flatten. 71 End flatten.
72 (** * A Type Soundness Proof *) 77 (** * A Type Soundness Proof *)
73 78
74 Reserved Notation "E1 ==> E2" (no associativity, at level 90). 79 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
75 80
76 Inductive Val : forall t, Exp t -> Prop := 81 Inductive Val : forall t, Exp t -> Prop :=
77 | VConst : forall b, Val (Const b) 82 | VConst : forall n, Val (Const n)
78 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B). 83 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
79 84
80 Hint Constructors Val. 85 Hint Constructors Val.
81 86
82 Inductive Step : forall t, Exp t -> Exp t -> Prop := 87 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
83 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), 88 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
84 App (Abs B) X ==> Subst X B 89 App (Abs B) X ==> Subst X B
85 | Cong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F', 90 | AppCong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
86 F ==> F' 91 F ==> F'
87 -> App F X ==> App F' X 92 -> App F X ==> App F' X
88 | Cong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X', 93 | AppCong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
89 Val F 94 Val F
90 -> X ==> X' 95 -> X ==> X'
91 -> App F X ==> App F X' 96 -> App F X ==> App F X'
97
98 | Sum : forall n1 n2,
99 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
100 | PlusCong1 : forall E1 E2 E1',
101 E1 ==> E1'
102 -> Plus E1 E2 ==> Plus E1' E2
103 | PlusCong2 : forall E1 E2 E2',
104 E2 ==> E2'
105 -> Plus E1 E2 ==> Plus E1 E2'
92 106
93 where "E1 ==> E2" := (Step E1 E2). 107 where "E1 ==> E2" := (Step E1 E2).
94 108
95 Hint Constructors Step. 109 Hint Constructors Step.
96 110
97 Inductive Closed : forall t, Exp t -> Prop := 111 Inductive Closed : forall t, Exp t -> Prop :=
98 | CConst : forall b, 112 | CConst : forall b,
99 Closed (Const b) 113 Closed (Const b)
114 | CPlus : forall E1 E2,
115 Closed E1
116 -> Closed E2
117 -> Closed (Plus E1 E2)
100 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2, 118 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
101 Closed E1 119 Closed E1
102 -> Closed E2 120 -> Closed E2
103 -> Closed (App E1 E2) 121 -> Closed (App E1 E2)
104 | CAbs : forall dom ran (E1 : Exp1 dom ran), 122 | CAbs : forall dom ran (E1 : Exp1 dom ran),
114 132
115 Lemma progress' : forall t (E : Exp t), 133 Lemma progress' : forall t (E : Exp t),
116 Closed E 134 Closed E
117 -> Val E \/ exists E', E ==> E'. 135 -> Val E \/ exists E', E ==> E'.
118 induction 1; crush; 136 induction 1; crush;
119 try match goal with 137 repeat match goal with
120 | [ H : @Val (_ --> _) _ |- _ ] => inversion H; my_crush 138 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
121 end; eauto. 139 end; eauto.
122 Qed. 140 Qed.
123 141
124 Theorem progress : forall t (E : Exp t), 142 Theorem progress : forall t (E : Exp t),
125 Val E \/ exists E', E ==> E'. 143 Val E \/ exists E', E ==> E'.
126 intros; apply progress'; apply closed. 144 intros; apply progress'; apply closed.