Mercurial > cpdt > repo
comparison src/Intensional.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 10:52:43 -0500 |
parents | 0198181d1b64 |
children | 2a34c4dc6a10 |
comparison
equal
deleted
inserted
replaced
203:71ade09024ac | 204:cbf2f74a5130 |
---|---|
5 * Unported License. | 5 * Unported License. |
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 *) | |
11 Require Import Arith Bool String List Eqdep JMeq. | |
12 | |
13 Require Import Axioms Tactics DepList. | |
14 | |
15 Set Implicit Arguments. | |
16 | |
17 Infix "==" := JMeq (at level 70, no associativity). | |
18 (* end hide *) | |
19 | |
20 | |
21 | |
22 | 10 |
23 (** %\chapter{Intensional Transformations}% *) | 11 (** %\chapter{Intensional Transformations}% *) |
24 | 12 |
25 (** TODO: Prose for this chapter *) | 13 (** TODO: This chapter! (Old version was too complicated) *) |
26 | |
27 | |
28 (** * Closure Conversion *) | |
29 | |
30 Module Source. | |
31 Inductive type : Type := | |
32 | TNat : type | |
33 | Arrow : type -> type -> type. | |
34 | |
35 Notation "'Nat'" := TNat : source_scope. | |
36 Infix "-->" := Arrow (right associativity, at level 60) : source_scope. | |
37 | |
38 Open Scope source_scope. | |
39 Bind Scope source_scope with type. | |
40 Delimit Scope source_scope with source. | |
41 | |
42 Section vars. | |
43 Variable var : type -> Type. | |
44 | |
45 Inductive exp : type -> Type := | |
46 | Var : forall t, | |
47 var t | |
48 -> exp t | |
49 | |
50 | Const : nat -> exp Nat | |
51 | Plus : exp Nat -> exp Nat -> exp Nat | |
52 | |
53 | App : forall t1 t2, | |
54 exp (t1 --> t2) | |
55 -> exp t1 | |
56 -> exp t2 | |
57 | Abs : forall t1 t2, | |
58 (var t1 -> exp t2) | |
59 -> exp (t1 --> t2). | |
60 End vars. | |
61 | |
62 Definition Exp t := forall var, exp var t. | |
63 | |
64 Implicit Arguments Var [var t]. | |
65 Implicit Arguments Const [var]. | |
66 Implicit Arguments Plus [var]. | |
67 Implicit Arguments App [var t1 t2]. | |
68 Implicit Arguments Abs [var t1 t2]. | |
69 | |
70 Notation "# v" := (Var v) (at level 70) : source_scope. | |
71 | |
72 Notation "^ n" := (Const n) (at level 70) : source_scope. | |
73 Infix "+^" := Plus (left associativity, at level 79) : source_scope. | |
74 | |
75 Infix "@" := App (left associativity, at level 77) : source_scope. | |
76 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. | |
77 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. | |
78 | |
79 Bind Scope source_scope with exp. | |
80 | |
81 Definition zero : Exp Nat := fun _ => ^0. | |
82 Definition one : Exp Nat := fun _ => ^1. | |
83 Definition zpo : Exp Nat := fun _ => zero _ +^ one _. | |
84 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. | |
85 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. | |
86 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | |
87 \f, \x, #f @ #x. | |
88 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. | |
89 | |
90 Fixpoint typeDenote (t : type) : Set := | |
91 match t with | |
92 | Nat => nat | |
93 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | |
94 end. | |
95 | |
96 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | |
97 match e in (exp _ t) return (typeDenote t) with | |
98 | Var _ v => v | |
99 | |
100 | Const n => n | |
101 | Plus e1 e2 => expDenote e1 + expDenote e2 | |
102 | |
103 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | |
104 | Abs _ _ e' => fun x => expDenote (e' x) | |
105 end. | |
106 | |
107 Definition ExpDenote t (e : Exp t) := expDenote (e _). | |
108 | |
109 Section exp_equiv. | |
110 Variables var1 var2 : type -> Type. | |
111 | |
112 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop := | |
113 | EqVar : forall G t (v1 : var1 t) v2, | |
114 In (existT _ t (v1, v2)) G | |
115 -> exp_equiv G (#v1) (#v2) | |
116 | |
117 | EqConst : forall G n, | |
118 exp_equiv G (^n) (^n) | |
119 | EqPlus : forall G x1 y1 x2 y2, | |
120 exp_equiv G x1 x2 | |
121 -> exp_equiv G y1 y2 | |
122 -> exp_equiv G (x1 +^ y1) (x2 +^ y2) | |
123 | |
124 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2, | |
125 exp_equiv G f1 f2 | |
126 -> exp_equiv G x1 x2 | |
127 -> exp_equiv G (f1 @ x1) (f2 @ x2) | |
128 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, | |
129 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) | |
130 -> exp_equiv G (Abs f1) (Abs f2). | |
131 End exp_equiv. | |
132 | |
133 Axiom Exp_equiv : forall t (E : Exp t) var1 var2, | |
134 exp_equiv nil (E var1) (E var2). | |
135 End Source. | |
136 | |
137 Module Closed. | |
138 Inductive type : Type := | |
139 | TNat : type | |
140 | Arrow : type -> type -> type | |
141 | Code : type -> type -> type -> type | |
142 | Prod : type -> type -> type | |
143 | TUnit : type. | |
144 | |
145 Notation "'Nat'" := TNat : cc_scope. | |
146 Notation "'Unit'" := TUnit : cc_scope. | |
147 Infix "-->" := Arrow (right associativity, at level 60) : cc_scope. | |
148 Infix "**" := Prod (right associativity, at level 59) : cc_scope. | |
149 Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope. | |
150 | |
151 Bind Scope cc_scope with type. | |
152 Delimit Scope cc_scope with cc. | |
153 | |
154 Open Local Scope cc_scope. | |
155 | |
156 Section vars. | |
157 Variable var : type -> Set. | |
158 | |
159 Inductive exp : type -> Type := | |
160 | Var : forall t, | |
161 var t | |
162 -> exp t | |
163 | |
164 | Const : nat -> exp Nat | |
165 | Plus : exp Nat -> exp Nat -> exp Nat | |
166 | |
167 | App : forall dom ran, | |
168 exp (dom --> ran) | |
169 -> exp dom | |
170 -> exp ran | |
171 | |
172 | Pack : forall env dom ran, | |
173 exp (env @@ dom ---> ran) | |
174 -> exp env | |
175 -> exp (dom --> ran) | |
176 | |
177 | EUnit : exp Unit | |
178 | |
179 | Pair : forall t1 t2, | |
180 exp t1 | |
181 -> exp t2 | |
182 -> exp (t1 ** t2) | |
183 | Fst : forall t1 t2, | |
184 exp (t1 ** t2) | |
185 -> exp t1 | |
186 | Snd : forall t1 t2, | |
187 exp (t1 ** t2) | |
188 -> exp t2 | |
189 | |
190 | Let : forall t1 t2, | |
191 exp t1 | |
192 -> (var t1 -> exp t2) | |
193 -> exp t2. | |
194 | |
195 Section funcs. | |
196 Variable T : Type. | |
197 | |
198 Inductive funcs : Type := | |
199 | Main : T -> funcs | |
200 | Abs : forall env dom ran, | |
201 (var env -> var dom -> exp ran) | |
202 -> (var (env @@ dom ---> ran) -> funcs) | |
203 -> funcs. | |
204 End funcs. | |
205 | |
206 Definition prog t := funcs (exp t). | |
207 End vars. | |
208 | |
209 Implicit Arguments Var [var t]. | |
210 Implicit Arguments Const [var]. | |
211 Implicit Arguments EUnit [var]. | |
212 Implicit Arguments Fst [var t1 t2]. | |
213 Implicit Arguments Snd [var t1 t2]. | |
214 | |
215 Implicit Arguments Main [var T]. | |
216 Implicit Arguments Abs [var T env dom ran]. | |
217 | |
218 Notation "# v" := (Var v) (at level 70) : cc_scope. | |
219 | |
220 Notation "^ n" := (Const n) (at level 70) : cc_scope. | |
221 Infix "+^" := Plus (left associativity, at level 79) : cc_scope. | |
222 | |
223 Infix "@" := App (left associativity, at level 77) : cc_scope. | |
224 Infix "##" := Pack (no associativity, at level 71) : cc_scope. | |
225 | |
226 Notation "()" := EUnit : cc_scope. | |
227 | |
228 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope. | |
229 Notation "#1 x" := (Fst x) (at level 72) : cc_scope. | |
230 Notation "#2 x" := (Snd x) (at level 72) : cc_scope. | |
231 | |
232 Notation "f <== \\ x , y , e ; fs" := | |
233 (Abs (fun x y => e) (fun f => fs)) | |
234 (right associativity, at level 80, e at next level) : cc_scope. | |
235 Notation "f <== \\ ! , y , e ; fs" := | |
236 (Abs (fun _ y => e) (fun f => fs)) | |
237 (right associativity, at level 80, e at next level) : cc_scope. | |
238 Notation "f <== \\ x , ! , e ; fs" := | |
239 (Abs (fun x _ => e) (fun f => fs)) | |
240 (right associativity, at level 80, e at next level) : cc_scope. | |
241 Notation "f <== \\ ! , ! , e ; fs" := | |
242 (Abs (fun _ _ => e) (fun f => fs)) | |
243 (right associativity, at level 80, e at next level) : cc_scope. | |
244 | |
245 Notation "x <- e1 ; e2" := (Let e1 (fun x => e2)) | |
246 (right associativity, at level 80, e1 at next level) : cc_scope. | |
247 | |
248 Bind Scope cc_scope with exp funcs prog. | |
249 | |
250 Fixpoint typeDenote (t : type) : Set := | |
251 match t with | |
252 | Nat => nat | |
253 | Unit => unit | |
254 | dom --> ran => typeDenote dom -> typeDenote ran | |
255 | t1 ** t2 => typeDenote t1 * typeDenote t2 | |
256 | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran | |
257 end%type. | |
258 | |
259 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | |
260 match e in (exp _ t) return (typeDenote t) with | |
261 | Var _ v => v | |
262 | |
263 | Const n => n | |
264 | Plus e1 e2 => expDenote e1 + expDenote e2 | |
265 | |
266 | App _ _ f x => (expDenote f) (expDenote x) | |
267 | Pack _ _ _ f env => (expDenote f) (expDenote env) | |
268 | |
269 | EUnit => tt | |
270 | |
271 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) | |
272 | Fst _ _ e' => fst (expDenote e') | |
273 | Snd _ _ e' => snd (expDenote e') | |
274 | |
275 | Let _ _ e1 e2 => expDenote (e2 (expDenote e1)) | |
276 end. | |
277 | |
278 Fixpoint funcsDenote T (fs : funcs typeDenote T) : T := | |
279 match fs with | |
280 | Main v => v | |
281 | Abs _ _ _ e fs => | |
282 funcsDenote (fs (fun env arg => expDenote (e env arg))) | |
283 end. | |
284 | |
285 Definition progDenote t (p : prog typeDenote t) : typeDenote t := | |
286 expDenote (funcsDenote p). | |
287 | |
288 Definition Exp t := forall var, exp var t. | |
289 Definition Prog t := forall var, prog var t. | |
290 | |
291 Definition ExpDenote t (E : Exp t) := expDenote (E _). | |
292 Definition ProgDenote t (P : Prog t) := progDenote (P _). | |
293 End Closed. | |
294 | |
295 Import Source Closed. | |
296 | |
297 Section splice. | |
298 Open Local Scope cc_scope. | |
299 | |
300 Fixpoint spliceFuncs var T1 (fs : funcs var T1) | |
301 T2 (f : T1 -> funcs var T2) {struct fs} : funcs var T2 := | |
302 match fs with | |
303 | Main v => f v | |
304 | Abs _ _ _ e fs' => Abs e (fun x => spliceFuncs (fs' x) f) | |
305 end. | |
306 End splice. | |
307 | |
308 Notation "x <-- e1 ; e2" := (spliceFuncs e1 (fun x => e2)) | |
309 (right associativity, at level 80, e1 at next level) : cc_scope. | |
310 | |
311 Definition natvar (_ : Source.type) := nat. | |
312 Definition isfree := hlist (fun (_ : Source.type) => bool). | |
313 | |
314 Ltac maybe_destruct E := | |
315 match goal with | |
316 | [ x : _ |- _ ] => | |
317 match E with | |
318 | x => idtac | |
319 end | |
320 | _ => | |
321 match E with | |
322 | eq_nat_dec _ _ => idtac | |
323 end | |
324 end; destruct E. | |
325 | |
326 Ltac my_crush := | |
327 crush; repeat (match goal with | |
328 | [ x : (_ * _)%type |- _ ] => destruct x | |
329 | [ |- context[if ?B then _ else _] ] => maybe_destruct B | |
330 | [ _ : context[if ?B then _ else _] |- _ ] => maybe_destruct B | |
331 end; crush). | |
332 | |
333 Section isfree. | |
334 Import Source. | |
335 Open Local Scope source_scope. | |
336 | |
337 Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT} | |
338 : isfree envT -> option Source.type := | |
339 match envT return (isfree envT -> _) with | |
340 | nil => fun _ => None | |
341 | first :: rest => fun fvs => | |
342 if eq_nat_dec n (length rest) | |
343 then match fvs with | |
344 | (true, _) => Some first | |
345 | (false, _) => None | |
346 end | |
347 else lookup_type rest n (snd fvs) | |
348 end. | |
349 | |
350 Implicit Arguments lookup_type [envT]. | |
351 | |
352 Notation ok := (fun (envT : list Source.type) (fvs : isfree envT) | |
353 (n : nat) (t : Source.type) | |
354 => lookup_type n fvs = Some t). | |
355 | |
356 Fixpoint wfExp (envT : list Source.type) (fvs : isfree envT) | |
357 t (e : Source.exp natvar t) {struct e} : Prop := | |
358 match e with | |
359 | Var t v => ok envT fvs v t | |
360 | |
361 | Const _ => True | |
362 | Plus e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2 | |
363 | |
364 | App _ _ e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2 | |
365 | Abs dom _ e' => wfExp (dom :: envT) (true ::: fvs) (e' (length envT)) | |
366 end. | |
367 | |
368 Implicit Arguments wfExp [envT t]. | |
369 | |
370 Theorem wfExp_weaken : forall t (e : exp natvar t) envT (fvs fvs' : isfree envT), | |
371 wfExp fvs e | |
372 -> (forall n t, ok _ fvs n t -> ok _ fvs' n t) | |
373 -> wfExp fvs' e. | |
374 Hint Extern 1 (lookup_type (envT := _ :: _) _ _ = Some _) => | |
375 simpl in *; my_crush. | |
376 | |
377 induction e; my_crush; eauto. | |
378 Defined. | |
379 | |
380 Fixpoint isfree_none (envT : list Source.type) : isfree envT := | |
381 match envT return (isfree envT) with | |
382 | nil => tt | |
383 | _ :: _ => (false, isfree_none _) | |
384 end. | |
385 | |
386 Implicit Arguments isfree_none [envT]. | |
387 | |
388 Fixpoint isfree_one (envT : list Source.type) (n : nat) {struct envT} : isfree envT := | |
389 match envT return (isfree envT) with | |
390 | nil => tt | |
391 | _ :: rest => | |
392 if eq_nat_dec n (length rest) | |
393 then (true, isfree_none) | |
394 else (false, isfree_one _ n) | |
395 end. | |
396 | |
397 Implicit Arguments isfree_one [envT]. | |
398 | |
399 Fixpoint isfree_merge (envT : list Source.type) : isfree envT -> isfree envT -> isfree envT := | |
400 match envT return (isfree envT -> isfree envT -> isfree envT) with | |
401 | nil => fun _ _ => tt | |
402 | _ :: _ => fun fv1 fv2 => (fst fv1 || fst fv2, isfree_merge _ (snd fv1) (snd fv2)) | |
403 end. | |
404 | |
405 Implicit Arguments isfree_merge [envT]. | |
406 | |
407 Fixpoint fvsExp t (e : exp natvar t) | |
408 (envT : list Source.type) {struct e} : isfree envT := | |
409 match e with | |
410 | Var _ n => isfree_one n | |
411 | |
412 | Const _ => isfree_none | |
413 | Plus e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT) | |
414 | |
415 | App _ _ e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT) | |
416 | Abs dom _ e' => snd (fvsExp (e' (length envT)) (dom :: envT)) | |
417 end. | |
418 | |
419 Lemma isfree_one_correct : forall t (v : natvar t) envT fvs, | |
420 ok envT fvs v t | |
421 -> ok envT (isfree_one (envT:=envT) v) v t. | |
422 induction envT; my_crush; eauto. | |
423 Defined. | |
424 | |
425 Lemma isfree_merge_correct1 : forall t (v : natvar t) envT fvs1 fvs2, | |
426 ok envT fvs1 v t | |
427 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t. | |
428 induction envT; my_crush; eauto. | |
429 Defined. | |
430 | |
431 Hint Rewrite orb_true_r : cpdt. | |
432 | |
433 Lemma isfree_merge_correct2 : forall t (v : natvar t) envT fvs1 fvs2, | |
434 ok envT fvs2 v t | |
435 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t. | |
436 induction envT; my_crush; eauto. | |
437 Defined. | |
438 | |
439 Hint Resolve isfree_one_correct isfree_merge_correct1 isfree_merge_correct2. | |
440 | |
441 Lemma fvsExp_correct : forall t (e : exp natvar t) | |
442 envT (fvs : isfree envT), wfExp fvs e | |
443 -> forall (fvs' : isfree envT), | |
444 (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs' v t) | |
445 -> wfExp fvs' e. | |
446 Hint Extern 1 (_ = _) => | |
447 match goal with | |
448 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] => | |
449 destruct (fvsExp X Y); my_crush | |
450 end. | |
451 | |
452 induction e; my_crush; eauto. | |
453 Defined. | |
454 | |
455 Lemma lookup_type_unique : forall v t1 t2 envT (fvs1 fvs2 : isfree envT), | |
456 lookup_type v fvs1 = Some t1 | |
457 -> lookup_type v fvs2 = Some t2 | |
458 -> t1 = t2. | |
459 induction envT; my_crush; eauto. | |
460 Defined. | |
461 | |
462 Implicit Arguments lookup_type_unique [v t1 t2 envT fvs1 fvs2]. | |
463 | |
464 Hint Extern 2 (lookup_type _ _ = Some _) => | |
465 match goal with | |
466 | [ H1 : lookup_type ?v _ = Some _, | |
467 H2 : lookup_type ?v _ = Some _ |- _ ] => | |
468 (generalize (lookup_type_unique H1 H2); intro; subst) | |
469 || rewrite <- (lookup_type_unique H1 H2) | |
470 end. | |
471 | |
472 Lemma lookup_none : forall v t envT, | |
473 lookup_type (envT:=envT) v (isfree_none (envT:=envT)) = Some t | |
474 -> False. | |
475 induction envT; my_crush. | |
476 Defined. | |
477 | |
478 Hint Extern 2 (_ = _) => elimtype False; eapply lookup_none; eassumption. | |
479 | |
480 Lemma lookup_one : forall v' v t envT, | |
481 lookup_type (envT:=envT) v' (isfree_one (envT:=envT) v) = Some t | |
482 -> v' = v. | |
483 induction envT; my_crush. | |
484 Defined. | |
485 | |
486 Implicit Arguments lookup_one [v' v t envT]. | |
487 | |
488 Hint Extern 2 (lookup_type _ _ = Some _) => | |
489 match goal with | |
490 | [ H : lookup_type _ _ = Some _ |- _ ] => | |
491 generalize (lookup_one H); intro; subst | |
492 end. | |
493 | |
494 Lemma lookup_merge : forall v t envT (fvs1 fvs2 : isfree envT), | |
495 lookup_type v (isfree_merge fvs1 fvs2) = Some t | |
496 -> lookup_type v fvs1 = Some t | |
497 \/ lookup_type v fvs2 = Some t. | |
498 induction envT; my_crush. | |
499 Defined. | |
500 | |
501 Implicit Arguments lookup_merge [v t envT fvs1 fvs2]. | |
502 | |
503 Lemma lookup_bound : forall v t envT (fvs : isfree envT), | |
504 lookup_type v fvs = Some t | |
505 -> v < length envT. | |
506 Hint Resolve lt_S. | |
507 induction envT; my_crush; eauto. | |
508 Defined. | |
509 | |
510 Hint Resolve lookup_bound. | |
511 | |
512 Lemma lookup_bound_contra : forall t envT (fvs : isfree envT), | |
513 lookup_type (length envT) fvs = Some t | |
514 -> False. | |
515 intros; assert (length envT < length envT); eauto; crush. | |
516 Defined. | |
517 | |
518 Hint Resolve lookup_bound_contra. | |
519 | |
520 Lemma lookup_push_drop : forall v t t' envT fvs, | |
521 v < length envT | |
522 -> lookup_type (envT := t :: envT) v (true, fvs) = Some t' | |
523 -> lookup_type (envT := envT) v fvs = Some t'. | |
524 my_crush. | |
525 Defined. | |
526 | |
527 Lemma lookup_push_add : forall v t t' envT fvs, | |
528 lookup_type (envT := envT) v (snd fvs) = Some t' | |
529 -> lookup_type (envT := t :: envT) v fvs = Some t'. | |
530 my_crush; elimtype False; eauto. | |
531 Defined. | |
532 | |
533 Hint Resolve lookup_bound lookup_push_drop lookup_push_add. | |
534 | |
535 Theorem fvsExp_minimal : forall t (e : exp natvar t) | |
536 envT (fvs : isfree envT), wfExp fvs e | |
537 -> (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs v t). | |
538 Hint Extern 1 (_ = _) => | |
539 match goal with | |
540 | [ H : lookup_type _ (isfree_merge _ _) = Some _ |- _ ] => | |
541 destruct (lookup_merge H); clear H; eauto | |
542 end. | |
543 | |
544 induction e; my_crush; eauto. | |
545 Defined. | |
546 | |
547 Fixpoint ccType (t : Source.type) : Closed.type := | |
548 match t with | |
549 | Nat%source => Nat | |
550 | (dom --> ran)%source => ccType dom --> ccType ran | |
551 end%cc. | |
552 | |
553 Open Local Scope cc_scope. | |
554 | |
555 Fixpoint envType (envT : list Source.type) : isfree envT -> Closed.type := | |
556 match envT return (isfree envT -> _) with | |
557 | nil => fun _ => Unit | |
558 | t :: _ => fun tup => | |
559 if fst tup | |
560 then ccType t ** envType _ (snd tup) | |
561 else envType _ (snd tup) | |
562 end. | |
563 | |
564 Implicit Arguments envType [envT]. | |
565 | |
566 Fixpoint envOf (var : Closed.type -> Set) (envT : list Source.type) {struct envT} | |
567 : isfree envT -> Set := | |
568 match envT return (isfree envT -> _) with | |
569 | nil => fun _ => unit | |
570 | first :: rest => fun fvs => | |
571 match fvs with | |
572 | (true, fvs') => (var (ccType first) * envOf var rest fvs')%type | |
573 | (false, fvs') => envOf var rest fvs' | |
574 end | |
575 end. | |
576 | |
577 Implicit Arguments envOf [envT]. | |
578 | |
579 Notation "var <| to" := (match to with | |
580 | None => unit | |
581 | Some t => var (ccType t) | |
582 end) (no associativity, at level 70). | |
583 | |
584 Fixpoint lookup (var : Closed.type -> Set) (envT : list Source.type) : | |
585 forall (n : nat) (fvs : isfree envT), envOf var fvs -> var <| lookup_type n fvs := | |
586 match envT return (forall (n : nat) (fvs : isfree envT), envOf var fvs | |
587 -> var <| lookup_type n fvs) with | |
588 | nil => fun _ _ _ => tt | |
589 | first :: rest => fun n fvs => | |
590 match (eq_nat_dec n (length rest)) as Heq return | |
591 (envOf var (envT := first :: rest) fvs | |
592 -> var <| (if Heq | |
593 then match fvs with | |
594 | (true, _) => Some first | |
595 | (false, _) => None | |
596 end | |
597 else lookup_type n (snd fvs))) with | |
598 | left _ => | |
599 match fvs return (envOf var (envT := first :: rest) fvs | |
600 -> var <| (match fvs with | |
601 | (true, _) => Some first | |
602 | (false, _) => None | |
603 end)) with | |
604 | (true, _) => fun env => fst env | |
605 | (false, _) => fun _ => tt | |
606 end | |
607 | right _ => | |
608 match fvs return (envOf var (envT := first :: rest) fvs | |
609 -> var <| (lookup_type n (snd fvs))) with | |
610 | (true, fvs') => fun env => lookup var rest n fvs' (snd env) | |
611 | (false, fvs') => fun env => lookup var rest n fvs' env | |
612 end | |
613 end | |
614 end. | |
615 | |
616 Theorem lok : forall var n t envT (fvs : isfree envT), | |
617 lookup_type n fvs = Some t | |
618 -> var <| lookup_type n fvs = var (ccType t). | |
619 crush. | |
620 Defined. | |
621 End isfree. | |
622 | |
623 Implicit Arguments lookup_type [envT]. | |
624 Implicit Arguments lookup [envT fvs]. | |
625 Implicit Arguments wfExp [t envT]. | |
626 Implicit Arguments envType [envT]. | |
627 Implicit Arguments envOf [envT]. | |
628 Implicit Arguments lok [var n t envT fvs]. | |
629 | |
630 Section lookup_hints. | |
631 Hint Resolve lookup_bound_contra. | |
632 | |
633 Hint Resolve lookup_bound_contra. | |
634 | |
635 Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2, | |
636 (forall (n : nat) (t : Source.type), | |
637 lookup_type (envT := t' :: envT) n (b1, fvs1) = Some t -> | |
638 lookup_type (envT := t' :: envT) n (b2, fvs2) = Some t) | |
639 -> (forall (n : nat) (t : Source.type), | |
640 lookup_type n fvs1 = Some t -> | |
641 lookup_type n fvs2 = Some t). | |
642 intros until b2; intro H; intros n t; | |
643 generalize (H n t); my_crush; elimtype False; eauto. | |
644 Defined. | |
645 | |
646 Lemma lookup_type_push_contra : forall t' envT (fvs1 fvs2 : isfree envT), | |
647 (forall (n : nat) (t : Source.type), | |
648 lookup_type (envT := t' :: envT) n (true, fvs1) = Some t -> | |
649 lookup_type (envT := t' :: envT) n (false, fvs2) = Some t) | |
650 -> False. | |
651 intros until fvs2; intro H; generalize (H (length envT) t'); my_crush. | |
652 Defined. | |
653 End lookup_hints. | |
654 | |
655 Section packing. | |
656 Open Local Scope cc_scope. | |
657 | |
658 Hint Resolve lookup_type_push lookup_type_push_contra. | |
659 | |
660 Definition packExp (var : Closed.type -> Set) (envT : list Source.type) | |
661 (fvs1 fvs2 : isfree envT) | |
662 : (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t) | |
663 -> envOf var fvs2 -> exp var (envType fvs1). | |
664 refine (fix packExp (var : Closed.type -> Set) (envT : list Source.type) {struct envT} | |
665 : forall fvs1 fvs2 : isfree envT, | |
666 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t) | |
667 -> envOf var fvs2 -> exp var (envType fvs1) := | |
668 match envT return (forall fvs1 fvs2 : isfree envT, | |
669 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t) | |
670 -> envOf var fvs2 | |
671 -> exp var (envType fvs1)) with | |
672 | nil => fun _ _ _ _ => () | |
673 | first :: rest => fun fvs1 => | |
674 match fvs1 return (forall fvs2 : isfree (first :: rest), | |
675 (forall n t, lookup_type (envT := first :: rest) n fvs1 = Some t | |
676 -> lookup_type n fvs2 = Some t) | |
677 -> envOf var fvs2 | |
678 -> exp var (envType (envT := first :: rest) fvs1)) with | |
679 | (false, fvs1') => fun fvs2 => | |
680 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (false, fvs1') = Some t | |
681 -> lookup_type (envT := first :: rest) n fvs2 = Some t) | |
682 -> envOf (envT := first :: rest) var fvs2 | |
683 -> exp var (envType (envT := first :: rest) (false, fvs1'))) with | |
684 | (false, fvs2') => fun Hmin env => | |
685 packExp var _ fvs1' fvs2' _ env | |
686 | (true, fvs2') => fun Hmin env => | |
687 packExp var _ fvs1' fvs2' _ (snd env) | |
688 end | |
689 | (true, fvs1') => fun fvs2 => | |
690 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (true, fvs1') = Some t | |
691 -> lookup_type (envT := first :: rest) n fvs2 = Some t) | |
692 -> envOf (envT := first :: rest) var fvs2 | |
693 -> exp var (envType (envT := first :: rest) (true, fvs1'))) with | |
694 | (false, fvs2') => fun Hmin env => | |
695 False_rect _ _ | |
696 | (true, fvs2') => fun Hmin env => | |
697 [#(fst env), packExp var _ fvs1' fvs2' _ (snd env)] | |
698 end | |
699 end | |
700 end); eauto. | |
701 Defined. | |
702 | |
703 Hint Resolve fvsExp_correct fvsExp_minimal. | |
704 Hint Resolve lookup_push_drop lookup_bound lookup_push_add. | |
705 | |
706 Implicit Arguments packExp [var envT]. | |
707 | |
708 Fixpoint unpackExp (var : Closed.type -> Set) t (envT : list Source.type) {struct envT} | |
709 : forall fvs : isfree envT, | |
710 exp var (envType fvs) | |
711 -> (envOf var fvs -> exp var t) -> exp var t := | |
712 match envT return (forall fvs : isfree envT, | |
713 exp var (envType fvs) | |
714 -> (envOf var fvs -> exp var t) -> exp var t) with | |
715 | nil => fun _ _ f => f tt | |
716 | first :: rest => fun fvs => | |
717 match fvs return (exp var (envType (envT := first :: rest) fvs) | |
718 -> (envOf var (envT := first :: rest) fvs -> exp var t) | |
719 -> exp var t) with | |
720 | (false, fvs') => fun p f => | |
721 unpackExp rest fvs' p f | |
722 | (true, fvs') => fun p f => | |
723 x <- #1 p; | |
724 unpackExp rest fvs' (#2 p) | |
725 (fun env => f (x, env)) | |
726 end | |
727 end. | |
728 | |
729 Implicit Arguments unpackExp [var t envT fvs]. | |
730 | |
731 Theorem wfExp_lax : forall t t' envT (fvs : isfree envT) (e : Source.exp natvar t), | |
732 wfExp (envT := t' :: envT) (true, fvs) e | |
733 -> wfExp (envT := t' :: envT) (true, snd (fvsExp e (t' :: envT))) e. | |
734 Hint Extern 1 (_ = _) => | |
735 match goal with | |
736 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] => | |
737 destruct (fvsExp X Y); my_crush | |
738 end. | |
739 eauto. | |
740 Defined. | |
741 | |
742 Implicit Arguments wfExp_lax [t t' envT fvs e]. | |
743 | |
744 Lemma inclusion : forall t t' envT fvs (e : Source.exp natvar t), | |
745 wfExp (envT := t' :: envT) (true, fvs) e | |
746 -> (forall n t, lookup_type n (snd (fvsExp e (t' :: envT))) = Some t | |
747 -> lookup_type n fvs = Some t). | |
748 eauto. | |
749 Defined. | |
750 | |
751 Implicit Arguments inclusion [t t' envT fvs e]. | |
752 | |
753 Definition env_prog var t envT (fvs : isfree envT) := | |
754 funcs var (envOf var fvs -> Closed.exp var t). | |
755 | |
756 Implicit Arguments env_prog [envT]. | |
757 | |
758 Import Source. | |
759 Open Local Scope cc_scope. | |
760 | |
761 Definition proj1 A B (pf : A /\ B) : A := | |
762 let (x, _) := pf in x. | |
763 Definition proj2 A B (pf : A /\ B) : B := | |
764 let (_, y) := pf in y. | |
765 | |
766 Fixpoint ccExp var t (e : Source.exp natvar t) | |
767 (envT : list Source.type) (fvs : isfree envT) | |
768 {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs := | |
769 match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with | |
770 | Const n => fun _ => Main (fun _ => ^n) | |
771 | Plus e1 e2 => fun wf => | |
772 n1 <-- ccExp var e1 _ fvs (proj1 wf); | |
773 n2 <-- ccExp var e2 _ fvs (proj2 wf); | |
774 Main (fun env => n1 env +^ n2 env) | |
775 | |
776 | Var _ n => fun wf => | |
777 Main (fun env => #(match lok wf in _ = T return T with | |
778 | refl_equal => lookup var n env | |
779 end)) | |
780 | |
781 | App _ _ f x => fun wf => | |
782 f' <-- ccExp var f _ fvs (proj1 wf); | |
783 x' <-- ccExp var x _ fvs (proj2 wf); | |
784 Main (fun env => f' env @ x' env) | |
785 | |
786 | Abs dom _ b => fun wf => | |
787 b' <-- ccExp var (b (length envT)) (dom :: envT) _ (wfExp_lax wf); | |
788 f <== \\env, arg, unpackExp (#env) (fun env => b' (arg, env)); | |
789 Main (fun env => #f ## | |
790 packExp | |
791 (snd (fvsExp (b (length envT)) (dom :: envT))) | |
792 fvs (inclusion wf) env) | |
793 end. | |
794 End packing. | |
795 | |
796 Implicit Arguments packExp [var envT]. | |
797 Implicit Arguments unpackExp [var t envT fvs]. | |
798 | |
799 Implicit Arguments ccExp [var t envT]. | |
800 | |
801 Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs} | |
802 : funcs var T2 := | |
803 match fs with | |
804 | Main v => Main (f v) | |
805 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x)) | |
806 end. | |
807 | |
808 Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) := | |
809 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf). | |
810 | |
811 | |
812 (** ** Examples *) | |
813 | |
814 Open Local Scope source_scope. | |
815 | |
816 Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x. | |
817 Theorem ident_ok : wfExp (envT := nil) tt (ident _). | |
818 crush. | |
819 Defined. | |
820 Eval compute in CcExp' ident ident_ok. | |
821 Eval compute in ProgDenote (CcExp' ident ident_ok). | |
822 | |
823 Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0. | |
824 Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _). | |
825 crush. | |
826 Defined. | |
827 Eval compute in CcExp' app_ident app_ident_ok. | |
828 Eval compute in ProgDenote (CcExp' app_ident app_ident_ok). | |
829 | |
830 Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ => | |
831 \x, \y, #x. | |
832 Theorem first_ok : wfExp (envT := nil) tt (first _). | |
833 crush. | |
834 Defined. | |
835 Eval compute in CcExp' first first_ok. | |
836 Eval compute in ProgDenote (CcExp' first first_ok). | |
837 | |
838 Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0. | |
839 Theorem app_first_ok : wfExp (envT := nil) tt (app_first _). | |
840 crush. | |
841 Defined. | |
842 Eval compute in CcExp' app_first app_first_ok. | |
843 Eval compute in ProgDenote (CcExp' app_first app_first_ok). | |
844 | |
845 | |
846 (** ** Correctness *) | |
847 | |
848 Section spliceFuncs_correct. | |
849 Variables T1 T2 : Type. | |
850 Variable f : T1 -> funcs typeDenote T2. | |
851 | |
852 Theorem spliceFuncs_correct : forall fs, | |
853 funcsDenote (spliceFuncs fs f) | |
854 = funcsDenote (f (funcsDenote fs)). | |
855 induction fs; crush. | |
856 Qed. | |
857 End spliceFuncs_correct. | |
858 | |
859 | |
860 Notation "var <| to" := (match to return Set with | |
861 | None => unit | |
862 | Some t => var (ccType t) | |
863 end) (no associativity, at level 70). | |
864 | |
865 Section packing_correct. | |
866 Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT), | |
867 Closed.typeDenote (envType fvs) | |
868 -> envOf Closed.typeDenote fvs := | |
869 match envT return (forall (fvs : isfree envT), | |
870 Closed.typeDenote (envType fvs) | |
871 -> envOf Closed.typeDenote fvs) with | |
872 | nil => fun _ _ => tt | |
873 | first :: rest => fun fvs => | |
874 match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs) | |
875 -> envOf (envT := first :: rest) Closed.typeDenote fvs) with | |
876 | (false, fvs') => fun env => makeEnv rest fvs' env | |
877 | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env)) | |
878 end | |
879 end. | |
880 | |
881 Implicit Arguments makeEnv [envT fvs]. | |
882 | |
883 Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT) | |
884 (e1 : Closed.exp Closed.typeDenote (envType fvs)) | |
885 (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t), | |
886 Closed.expDenote (unpackExp e1 e2) | |
887 = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))). | |
888 induction envT; my_crush. | |
889 Qed. | |
890 | |
891 Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v, | |
892 (v2 = length envT -> False) | |
893 -> lookup_type v2 (envT := t :: envT) (b, fvs) = v | |
894 -> lookup_type v2 fvs = v. | |
895 my_crush. | |
896 Qed. | |
897 | |
898 Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v, | |
899 (v2 = length envT -> False) | |
900 -> lookup_type v2 (snd fvs) = v | |
901 -> lookup_type v2 (envT := t :: envT) fvs = v. | |
902 my_crush. | |
903 Qed. | |
904 | |
905 Hint Resolve lookup_bound_contra. | |
906 | |
907 Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v, | |
908 lookup_type v fvs = Some t | |
909 -> v = length envT | |
910 -> False. | |
911 my_crush; elimtype False; eauto. | |
912 Qed. | |
913 | |
914 Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e, | |
915 wfExp (envT := t' :: envT) (true, fvs) e | |
916 -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t'' | |
917 -> lookup_type v fvs = Some t''. | |
918 Hint Resolve lookup_bound_contra_eq fvsExp_minimal | |
919 lookup_type_more lookup_type_less. | |
920 Hint Extern 2 (Some _ = Some _) => elimtype False. | |
921 | |
922 eauto 6. | |
923 Qed. | |
924 | |
925 Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2), | |
926 match H1 in _ = T return T with | |
927 | refl_equal => x | |
928 end | |
929 = match H2 in _ = T return T with | |
930 | refl_equal => x | |
931 end. | |
932 intros; generalize H1; crush; | |
933 repeat match goal with | |
934 | [ |- context[match ?pf with refl_equal => _ end] ] => | |
935 rewrite (UIP_refl _ _ pf) | |
936 end; | |
937 reflexivity. | |
938 Qed. | |
939 | |
940 Hint Immediate cast_irrel. | |
941 | |
942 Hint Extern 3 (_ == _) => | |
943 match goal with | |
944 | [ |- context[False_rect _ ?H] ] => | |
945 apply False_rect; exact H | |
946 end. | |
947 | |
948 Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT) | |
949 Hincl env, | |
950 lookup_type v fvs1 = Some t | |
951 -> lookup Closed.typeDenote v env | |
952 == lookup Closed.typeDenote v | |
953 (makeEnv (Closed.expDenote | |
954 (packExp fvs1 fvs2 Hincl env))). | |
955 induction envT; my_crush. | |
956 Qed. | |
957 End packing_correct. | |
958 | |
959 Implicit Arguments packExp_correct [v envT fvs1]. | |
960 Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e]. | |
961 Implicit Arguments inclusion [t t' envT fvs e]. | |
962 | |
963 Lemma typeDenote_same : forall t, | |
964 Source.typeDenote t = Closed.typeDenote (ccType t). | |
965 induction t; crush. | |
966 Qed. | |
967 | |
968 Hint Resolve typeDenote_same. | |
969 | |
970 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop := | |
971 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with | |
972 | Nat => @eq nat | |
973 | dom --> ran => fun f1 f2 => | |
974 forall x1 x2, lr dom x1 x2 | |
975 -> lr ran (f1 x1) (f2 x2) | |
976 end. | |
977 | |
978 Theorem ccExp_correct : forall t G | |
979 (e1 : Source.exp Source.typeDenote t) | |
980 (e2 : Source.exp natvar t), | |
981 exp_equiv G e1 e2 | |
982 -> forall (envT : list Source.type) (fvs : isfree envT) | |
983 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2), | |
984 (forall t (v1 : Source.typeDenote t) (v2 : natvar t), | |
985 In (existT _ _ (v1, v2)) G | |
986 -> v2 < length envT) | |
987 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t), | |
988 In (existT _ _ (v1, v2)) G | |
989 -> forall pf, | |
990 lr t v1 (match lok pf in _ = T return T with | |
991 | refl_equal => lookup Closed.typeDenote v2 env | |
992 end)) | |
993 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)). | |
994 | |
995 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt. | |
996 Hint Resolve packExp_correct lookup_type_inner. | |
997 | |
998 induction 1; crush; | |
999 match goal with | |
1000 | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] => | |
1001 apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV)))) | |
1002 end; crush; | |
1003 match goal with | |
1004 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] => | |
1005 solve [ generalize (Hlt _ _ _ Hin); crush ] | |
1006 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf | |
1007 end; simpl; | |
1008 match goal with | |
1009 | [ |- context[if ?E then _ else _] ] => destruct E | |
1010 end; intuition; subst; | |
1011 match goal with | |
1012 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption | |
1013 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] => | |
1014 generalize (Hlt _ _ _ Hin); crush | |
1015 | [ HG : _, Hin : In _ _, wf : wfExp _ _, pf : _ = Some _, | |
1016 fvs : isfree _, env : envOf _ _ |- _ ] => | |
1017 generalize (HG _ _ _ Hin (lookup_type_inner wf pf)); clear_all; | |
1018 repeat match goal with | |
1019 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf | |
1020 end; simpl; | |
1021 generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl; | |
1022 match goal with | |
1023 | [ |- ?X == ?Y -> _ ] => | |
1024 generalize X Y | |
1025 end; | |
1026 rewrite pf; rewrite (lookup_type_inner wf pf); | |
1027 intros lhs rhs Heq; intros; | |
1028 repeat match goal with | |
1029 | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in * | |
1030 end; | |
1031 rewrite <- Heq; assumption | |
1032 end. | |
1033 Qed. | |
1034 | |
1035 | |
1036 (** * Parametric version *) | |
1037 | |
1038 Section wf. | |
1039 Lemma Exp_wf' : forall G t (e1 e2 : Source.exp natvar t), | |
1040 exp_equiv G e1 e2 | |
1041 -> forall envT (fvs : isfree envT), | |
1042 (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G | |
1043 -> lookup_type v1 fvs = Some t) | |
1044 -> wfExp fvs e1. | |
1045 Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto. | |
1046 | |
1047 induction 1; crush; eauto; | |
1048 match goal with | |
1049 | [ H : _, envT : list Source.type |- _ ] => | |
1050 apply H with (length envT); my_crush; eauto | |
1051 end. | |
1052 Qed. | |
1053 | |
1054 Theorem Exp_wf : forall t (E : Source.Exp t), | |
1055 wfExp (envT := nil) tt (E _). | |
1056 Hint Resolve Exp_equiv. | |
1057 | |
1058 intros; eapply Exp_wf'; crush. | |
1059 Qed. | |
1060 End wf. | |
1061 | |
1062 Definition CcExp t (E : Source.Exp t) : Prog (ccType t) := | |
1063 CcExp' E (Exp_wf E). | |
1064 | |
1065 Lemma map_funcs_correct : forall T1 T2 (f : T1 -> T2) (fs : funcs Closed.typeDenote T1), | |
1066 funcsDenote (map_funcs f fs) = f (funcsDenote fs). | |
1067 induction fs; crush. | |
1068 Qed. | |
1069 | |
1070 Theorem CcExp_correct : forall (E : Source.Exp Nat), | |
1071 Source.ExpDenote E | |
1072 = ProgDenote (CcExp E). | |
1073 Hint Rewrite map_funcs_correct : cpdt. | |
1074 | |
1075 unfold Source.ExpDenote, ProgDenote, CcExp, CcExp', progDenote; crush; | |
1076 apply (ccExp_correct | |
1077 (G := nil) | |
1078 (e1 := E _) | |
1079 (e2 := E _) | |
1080 (Exp_equiv _ _ _) | |
1081 nil | |
1082 tt | |
1083 tt); crush. | |
1084 Qed. |