Mercurial > cpdt > repo

comparison src/Hoas.v @ 160:56e205f966cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Interderivability of big and small step
author Adam Chlipala <adamc@hcoop.net>
date Mon, 03 Nov 2008 14:47:46 -0500
parents 8b2b652ab0ee
children df02642f93b8
comparison
equal deleted inserted replaced
159:8b2b652ab0ee 160:56e205f966cc
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith Eqdep String List. 11 Require Import Arith Eqdep String List.
12 12
13 Require Import Tactics. 13 Require Import Axioms DepList Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
84 84
85 Hint Constructors Val. 85 Hint Constructors Val.
86 86
87 Inductive Step : forall t, Exp t -> Exp t -> Prop := 87 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
88 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), 88 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
89 App (Abs B) X ==> Subst X B 89 Val X
90 -> App (Abs B) X ==> Subst X B
90 | AppCong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F', 91 | AppCong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
91 F ==> F' 92 F ==> F'
92 -> App F X ==> App F' X 93 -> App F X ==> App F' X
93 | AppCong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X', 94 | AppCong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
94 Val F 95 Val F
99 Plus (Const n1) (Const n2) ==> Const (n1 + n2) 100 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
100 | PlusCong1 : forall E1 E2 E1', 101 | PlusCong1 : forall E1 E2 E1',
101 E1 ==> E1' 102 E1 ==> E1'
102 -> Plus E1 E2 ==> Plus E1' E2 103 -> Plus E1 E2 ==> Plus E1' E2
103 | PlusCong2 : forall E1 E2 E2', 104 | PlusCong2 : forall E1 E2 E2',
104 E2 ==> E2' 105 Val E1
106 -> E2 ==> E2'
105 -> Plus E1 E2 ==> Plus E1 E2' 107 -> Plus E1 E2 ==> Plus E1 E2'
106 108
107 where "E1 ==> E2" := (Step E1 E2). 109 where "E1 ==> E2" := (Step E1 E2).
108 110
109 Hint Constructors Step. 111 Hint Constructors Step.
122 | CAbs : forall dom ran (E1 : Exp1 dom ran), 124 | CAbs : forall dom ran (E1 : Exp1 dom ran),
123 Closed (Abs E1). 125 Closed (Abs E1).
124 126
125 Axiom closed : forall t (E : Exp t), Closed E. 127 Axiom closed : forall t (E : Exp t), Closed E.
126 128
127 Ltac my_crush := 129 Ltac my_crush' :=
128 crush; 130 crush;
129 repeat (match goal with 131 repeat (match goal with
130 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H 132 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
131 end; crush). 133 end; crush).
134
135 Ltac my_crush :=
136 my_crush';
137 try (match goal with
138 | [ H : ?F = ?G |- _ ] =>
139 match goal with
140 | [ _ : F (fun _ => unit) = G (fun _ => unit) |- _ ] => fail 1
141 | _ =>
142 let H' := fresh "H'" in
143 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
144 | discriminate || injection H' ];
145 clear H'
146 end
147 end; my_crush');
148 repeat match goal with
149 | [ H : ?F = ?G, H2 : ?X (fun _ => unit) = ?Y (fun _ => unit) |- _ ] =>
150 match X with
151 | Y => fail 1
152 | _ =>
153 assert (X = Y); [ unfold Exp; apply ext_eq; intro var;
154 let H' := fresh "H'" in
155 assert (H' : F var = G var); [ congruence
156 | match type of H' with
157 | ?X = ?Y =>
158 let X := eval hnf in X in
159 let Y := eval hnf in Y in
160 change (X = Y) in H'
161 end; injection H'; clear H'; my_crush' ]
162 | my_crush'; clear H2 ]
163 end
164 end.
132 165
133 Lemma progress' : forall t (E : Exp t), 166 Lemma progress' : forall t (E : Exp t),
134 Closed E 167 Closed E
135 -> Val E \/ exists E', E ==> E'. 168 -> Val E \/ exists E', E ==> E'.
136 induction 1; crush; 169 induction 1; crush;
142 Theorem progress : forall t (E : Exp t), 175 Theorem progress : forall t (E : Exp t),
143 Val E \/ exists E', E ==> E'. 176 Val E \/ exists E', E ==> E'.
144 intros; apply progress'; apply closed. 177 intros; apply progress'; apply closed.
145 Qed. 178 Qed.
146 179
180
181 (** * Big-Step Semantics *)
182
183 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
184
185 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
186 | SConst : forall n,
187 Const n ===> Const n
188 | SPlus : forall E1 E2 n1 n2,
189 E1 ===> Const n1
190 -> E2 ===> Const n2
191 -> Plus E1 E2 ===> Const (n1 + n2)
192
193 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
194 E1 ===> Abs B
195 -> E2 ===> V2
196 -> Subst V2 B ===> V
197 -> App E1 E2 ===> V
198 | SAbs : forall dom ran (B : Exp1 dom ran),
199 Abs B ===> Abs B
200
201 where "E1 ===> E2" := (BigStep E1 E2).
202
203 Hint Constructors BigStep.
204
205 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
206
207 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
208 | Done : forall t (E : Exp t), E ==>* E
209 | OneStep : forall t (E E' E'' : Exp t),
210 E ==> E'
211 -> E' ==>* E''
212 -> E ==>* E''
213
214 where "E1 ==>* E2" := (MultiStep E1 E2).
215
216 Hint Constructors MultiStep.
217
218 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
219 E1 ==>* E2
220 -> E2 ==>* E3
221 -> E1 ==>* E3.
222 induction 1; eauto.
223 Qed.
224
225 Hint Resolve MultiStep_trans.
226
227 Theorem Big_Val : forall t (E V : Exp t),
228 E ===> V
229 -> Val V.
230 induction 1; crush.
231 Qed.
232
233 Theorem Val_Big : forall t (V : Exp t),
234 Val V
235 -> V ===> V.
236 destruct 1; crush.
237 Qed.
238
239 Hint Resolve Big_Val Val_Big.
240
241 Ltac uiper :=
242 repeat match goal with
243 | [ pf : _ = _ |- _ ] =>
244 generalize pf; subst; intro;
245 rewrite (UIP_refl _ _ pf); simpl;
246 repeat match goal with
247 | [ H : forall pf : ?X = ?X, _ |- _ ] =>
248 generalize (H (refl_equal _)); clear H; intro H
249 end
250 end.
251
252 Lemma Multi_PlusCong1' : forall E2 t (pf : t = Nat) (E1 E1' : Exp t),
253 E1 ==>* E1'
254 -> Plus (match pf with refl_equal => E1 end) E2
255 ==>* Plus (match pf with refl_equal => E1' end) E2.
256 induction 1; crush; uiper; eauto.
257 Qed.
258
259 Lemma Multi_PlusCong1 : forall E1 E2 E1',
260 E1 ==>* E1'
261 -> Plus E1 E2 ==>* Plus E1' E2.
262 intros; generalize (Multi_PlusCong1' E2 (refl_equal _)); auto.
263 Qed.
264
265 Lemma Multi_PlusCong2' : forall E1 (_ : Val E1) t (pf : t = Nat) (E2 E2' : Exp t),
266 E2 ==>* E2'
267 -> Plus E1 (match pf with refl_equal => E2 end)
268 ==>* Plus E1 (match pf with refl_equal => E2' end).
269 induction 2; crush; uiper; eauto.
270 Qed.
271
272 Lemma Multi_PlusCong2 : forall E1 E2 E2',
273 Val E1
274 -> E2 ==>* E2'
275 -> Plus E1 E2 ==>* Plus E1 E2'.
276 intros E1 E2 E2' H; generalize (Multi_PlusCong2' H (refl_equal _)); auto.
277 Qed.
278
279 Lemma Multi_AppCong1' : forall dom ran E2 t (pf : t = dom --> ran) (E1 E1' : Exp t),
280 E1 ==>* E1'
281 -> App (match pf in _ = t' return Exp t' with refl_equal => E1 end) E2
282 ==>* App (match pf in _ = t' return Exp t' with refl_equal => E1' end) E2.
283 induction 1; crush; uiper; eauto.
284 Qed.
285
286 Lemma Multi_AppCong1 : forall dom ran (E1 : Exp (dom --> ran)) E2 E1',
287 E1 ==>* E1'
288 -> App E1 E2 ==>* App E1' E2.
289 intros; generalize (Multi_AppCong1' (ran := ran) E2 (refl_equal _)); auto.
290 Qed.
291
292 Lemma Multi_AppCong2 : forall dom ran (E1 : Exp (dom --> ran)) E2 E2',
293 Val E1
294 -> E2 ==>* E2'
295 -> App E1 E2 ==>* App E1 E2'.
296 induction 2; crush; eauto.
297 Qed.
298
299 Hint Resolve Multi_PlusCong1 Multi_PlusCong2 Multi_AppCong1 Multi_AppCong2.
300
301 Theorem Big_Multi : forall t (E V : Exp t),
302 E ===> V
303 -> E ==>* V.
304 induction 1; crush; eauto 8.
305 Qed.
306
307 Lemma Big_Val' : forall t (V1 V2 : Exp t),
308 Val V2
309 -> V1 = V2
310 -> V1 ===> V2.
311 crush.
312 Qed.
313
314 Hint Resolve Big_Val'.
315
316 Lemma Multi_Big' : forall t (E E' : Exp t),
317 E ==> E'
318 -> forall E'', E' ===> E''
319 -> E ===> E''.
320 induction 1; crush; eauto;
321 match goal with
322 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
323 end.
324 Qed.
325
326 Hint Resolve Multi_Big'.
327
328 Theorem Multi_Big : forall t (E V : Exp t),
329 E ==>* V
330 -> Val V
331 -> E ===> V.
332 induction 1; crush; eauto.
333 Qed.
334
335
336 (** * Constant folding *)
337
338 Section cfold.
339 Variable var : type -> Type.
340
341 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
342 match e in exp _ t return exp _ t with
343 | Const' n => Const' n
344 | Plus' e1 e2 =>
345 let e1' := cfold e1 in
346 let e2' := cfold e2 in
347 match e1', e2' with
348 | Const' n1, Const' n2 => Const' (n1 + n2)
349 | _, _ => Plus' e1' e2'
350 end
351
352 | Var _ x => Var x
353 | App' _ _ e1 e2 => App' (cfold e1) (cfold e2)
354 | Abs' _ _ e' => Abs' (fun x => cfold (e' x))
355 end.
356 End cfold.
357
358 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
359
360
361 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t.
362
363 Definition ConstN G (n : nat) : ExpN G Nat :=
364 fun _ _ => Const' n.
365 Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat :=
366 fun _ s => Plus' (E1 _ s) (E2 _ s).
367 Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran :=
368 fun _ s => App' (F _ s) (X _ s).
369 Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) :=
370 fun _ s => Abs' (fun x => B _ (x ::: s)).