Mercurial > cpdt > repo

comparison src/Hoas.v @ 166:73279a8aac71

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More easy syntactic examples
author Adam Chlipala <adamc@hcoop.net>
date Wed, 05 Nov 2008 09:21:11 -0500
parents cf60d8dc57c9
children ef485f86a7b6
comparison
equal deleted inserted replaced
165:cf60d8dc57c9 166:73279a8aac71
54 fun _ => Plus' (E1 _) (E2 _). 54 fun _ => Plus' (E1 _) (E2 _).
55 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 :=
56 fun _ => App' (F _) (X _). 56 fun _ => App' (F _) (X _).
57 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := 57 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
58 fun _ => Abs' (B _). 58 fun _ => Abs' (B _).
59
60 Definition zero := Const 0.
61 Definition one := Const 1.
62 Definition one_again := Plus zero one.
63 Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X).
64 Definition app_ident := App ident one_again.
65 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
66 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))).
67 Definition app_ident' := App (App app ident) one_again.
68
69 Fixpoint countVars t (e : exp (fun _ => unit) t) {struct e} : nat :=
70 match e with
71 | Const' _ => 0
72 | Plus' e1 e2 => countVars e1 + countVars e2
73 | Var _ _ => 1
74 | App' _ _ e1 e2 => countVars e1 + countVars e2
75 | Abs' _ _ e' => countVars (e' tt)
76 end.
77
78 Definition CountVars t (E : Exp t) : nat := countVars (E _).
79
80 Eval compute in CountVars zero.
81 Eval compute in CountVars one.
82 Eval compute in CountVars one_again.
83 Eval compute in CountVars ident.
84 Eval compute in CountVars app_ident.
85 Eval compute in CountVars app.
86 Eval compute in CountVars app_ident'.
87
88 Fixpoint countOne t (e : exp (fun _ => bool) t) {struct e} : nat :=
89 match e with
90 | Const' _ => 0
91 | Plus' e1 e2 => countOne e1 + countOne e2
92 | Var _ true => 1
93 | Var _ false => 0
94 | App' _ _ e1 e2 => countOne e1 + countOne e2
95 | Abs' _ _ e' => countOne (e' false)
96 end.
97
98 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat :=
99 countOne (E _ true).
100
101 Definition ident1 : Exp1 Nat Nat := fun _ X => Var X.
102 Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
103 Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
104 Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X).
105
106 Eval compute in CountOne ident1.
107 Eval compute in CountOne add_self.
108 Eval compute in CountOne app_zero.
109 Eval compute in CountOne app_ident1.
110
111 Section ToString.
112 Open Scope string_scope.
113
114 Fixpoint natToString (n : nat) : string :=
115 match n with
116 | O => "O"
117 | S n' => "S(" ++ natToString n' ++ ")"
118 end.
119
120 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) {struct e} : string * string :=
121 match e with
122 | Const' n => (cur, natToString n)
123 | Plus' e1 e2 =>
124 let (cur', s1) := toString e1 cur in
125 let (cur'', s2) := toString e2 cur' in
126 (cur'', "(" ++ s1 ++ ") + (" ++ s2 ++ ")")
127 | Var _ s => (cur, s)
128 | App' _ _ e1 e2 =>
129 let (cur', s1) := toString e1 cur in
130 let (cur'', s2) := toString e2 cur' in
131 (cur'', "(" ++ s1 ++ ") (" ++ s2 ++ ")")
132 | Abs' _ _ e' =>
133 let (cur', s) := toString (e' cur) (cur ++ "'") in
134 (cur', "(\" ++ cur ++ ", " ++ s ++ ")")
135 end.
136
137 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x").
138 End ToString.
139
140 Eval compute in ToString zero.
141 Eval compute in ToString one.
142 Eval compute in ToString one_again.
143 Eval compute in ToString ident.
144 Eval compute in ToString app_ident.
145 Eval compute in ToString app.
146 Eval compute in ToString app_ident'.
59 147
60 Section flatten. 148 Section flatten.
61 Variable var : type -> Type. 149 Variable var : type -> Type.
62 150
63 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t := 151 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
70 end. 158 end.
71 End flatten. 159 End flatten.
72 160
73 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ => 161 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
74 flatten (E2 _ (E1 _)). 162 flatten (E2 _ (E1 _)).
163
164 Eval compute in Subst one ident1.
165 Eval compute in Subst one add_self.
166 Eval compute in Subst ident app_zero.
167 Eval compute in Subst one app_ident1.
75 168
76 169
77 (** * A Type Soundness Proof *) 170 (** * A Type Soundness Proof *)
78 171
79 Reserved Notation "E1 ==> E2" (no associativity, at level 90). 172 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
327 E ==>* V 420 E ==>* V
328 -> Val V 421 -> Val V
329 -> E ===> V. 422 -> E ===> V.
330 induction 1; crush; eauto. 423 induction 1; crush; eauto.
331 Qed. 424 Qed.
332
333
334 (** * Constant folding *)
335
336 Section cfold.
337 Variable var : type -> Type.
338
339 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
340 match e in exp _ t return exp _ t with
341 | Const' n => Const' n
342 | Plus' e1 e2 =>
343 let e1' := cfold e1 in
344 let e2' := cfold e2 in
345 match e1', e2' with
346 | Const' n1, Const' n2 => Const' (n1 + n2)
347 | _, _ => Plus' e1' e2'
348 end
349
350 | Var _ x => Var x
351 | App' _ _ e1 e2 => App' (cfold e1) (cfold e2)
352 | Abs' _ _ e' => Abs' (fun x => cfold (e' x))
353 end.
354 End cfold.
355
356 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
357 Definition Cfold1 t1 t2 (E : Exp1 t1 t2) : Exp1 t1 t2 := fun _ x => cfold (E _ x).
358
359 Lemma fold_Cfold : forall t (E : Exp t),
360 (fun _ => cfold (E _)) = Cfold E.
361 reflexivity.
362 Qed.
363
364 Hint Rewrite fold_Cfold : fold.
365
366 Lemma fold_Cfold1 : forall t1 t2 (E : Exp1 t1 t2),
367 (fun _ x => cfold (E _ x)) = Cfold1 E.
368 reflexivity.
369 Qed.
370
371 Hint Rewrite fold_Cfold1 : fold.
372
373 Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1),
374 (fun _ => flatten (cfold (E _ (V _))))
375 = Subst V (Cfold1 E).
376 reflexivity.
377 Qed.
378
379 Axiom cheat : forall T, T.
380
381
382 Lemma fold_Const : forall n, (fun _ => Const' n) = Const n.
383 reflexivity.
384 Qed.
385 Lemma fold_Plus : forall (E1 E2 : Exp _), (fun _ => Plus' (E1 _) (E2 _)) = Plus E1 E2.
386 reflexivity.
387 Qed.
388 Lemma fold_App : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom),
389 (fun _ => App' (F _) (X _)) = App F X.
390 reflexivity.
391 Qed.
392 Lemma fold_Abs : forall dom ran (B : Exp1 dom ran),
393 (fun _ => Abs' (B _)) = Abs B.
394 reflexivity.
395 Qed.
396
397 Hint Rewrite fold_Const fold_Plus fold_App fold_Abs : fold.
398
399 Lemma fold_Subst : forall t1 t2 (E1 : Exp1 t1 t2) (V : Exp t1),
400 (fun _ => flatten (E1 _ (V _))) = Subst V E1.
401 reflexivity.
402 Qed.
403
404 Hint Rewrite fold_Subst : fold.
405
406 Section Closed1.
407 Variable xt : type.
408
409 Definition Const1 (n : nat) : Exp1 xt Nat :=
410 fun _ _ => Const' n.
411 Definition Var1 : Exp1 xt xt := fun _ x => Var x.
412 Definition Plus1 (E1 E2 : Exp1 xt Nat) : Exp1 xt Nat :=
413 fun _ s => Plus' (E1 _ s) (E2 _ s).
414 Definition App1 dom ran (F : Exp1 xt (dom --> ran)) (X : Exp1 xt dom) : Exp1 xt ran :=
415 fun _ s => App' (F _ s) (X _ s).
416 Definition Abs1 dom ran (B : forall var, var dom -> Exp1 xt ran) : Exp1 xt (dom --> ran) :=
417 fun _ s => Abs' (fun x => B _ x _ s).
418
419 Inductive Closed1 : forall t, Exp1 xt t -> Prop :=
420 | CConst1 : forall n,
421 Closed1 (Const1 n)
422 | CPlus1 : forall E1 E2,
423 Closed1 E1
424 -> Closed1 E2
425 -> Closed1 (Plus1 E1 E2)
426 | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2,
427 Closed1 E1
428 -> Closed1 E2
429 -> Closed1 (App1 E1 E2)
430 | CAbs1 : forall dom ran (E1 : forall var, var dom -> Exp1 _ ran),
431 Closed1 (Abs1 E1).
432
433 Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E.
434 End Closed1.
435
436 Hint Resolve closed1.
437
438 Ltac ssimp := unfold Subst, Cfold in *; simpl in *; autorewrite with fold in *;
439 repeat match goal with
440 | [ xt : type |- _ ] =>
441 rewrite (@fold_Subst xt) in *
442 end;
443 autorewrite with fold in *.
444
445 Lemma cfold_thorough : forall var t (e : exp var t),
446 cfold (cfold e) = cfold e.
447 induction e; crush; try (f_equal; ext_eq; eauto);
448 match goal with
449 | [ e1 : exp _ Nat, e2 : exp _ Nat |- _ ] =>
450 dep_destruct (cfold e1); crush;
451 dep_destruct (cfold e2); crush
452 end.
453 Qed.
454
455 Lemma Cfold_thorough : forall t (E : Exp t),
456 Cfold (Cfold E) = Cfold E.
457 intros; unfold Cfold, Exp; ext_eq;
458 apply cfold_thorough.
459 Qed.
460
461 Hint Resolve Cfold_thorough.
462
463 Section eq_arg.
464 Variable A : Type.
465 Variable B : A -> Type.
466
467 Variable x : A.
468
469 Variables f g : forall x, B x.
470 Hypothesis Heq : f = g.
471
472 Theorem eq_arg : f x = g x.
473 congruence.
474 Qed.
475 End eq_arg.
476
477 Implicit Arguments eq_arg [A B f g].
478
479 Lemma Cfold_Subst_thorough : forall t1 (V : Exp t1) t2 (B : Exp1 t1 t2),
480 Subst (Cfold V) (Cfold1 B) = Cfold (Subst (Cfold V) (Cfold1 B)).
481
482 Lemma Cfold_Step_thorough' : forall t (E V : Exp t),
483 E ===> V
484 -> forall E', E = Cfold E'
485 -> Cfold V = V.
486 induction 1; crush.
487 apply IHBigStep3 with (Subst V2 B).
488
489 generalize (closed E'); inversion 1; my_crush.
490
491 generalize (eq_arg (fun _ => Set) H2); ssimp.
492 dep_destruct (cfold (E0 (fun _ => Set))); try discriminate;
493 dep_destruct (cfold (E3 (fun _ => Set))); discriminate.
494
495 ssimp; my_crush.
496
497 rewrite <- (IHBigStep2 _ (refl_equal _)).
498 generalize (IHBigStep1 _ (refl_equal _)).
499 my_crush.
500 ssimp.
501 assert (B = Cfold1 B).
502 generalize H2; clear_all; my_crush.
503 unfold Exp1; ext_eq.
504 generalize (eq_arg x H2); injection 1; my_crush.
505
506 rewrite H8.
507
508
509 my_crush.
510
511 Lemma Cfold_thorough : forall t (E V : Exp t),
512 Cfold E ===> V
513 -> V = Cfold V.
514
515 Lemma Cfold_Subst' : forall t (E V : Exp t),
516 E ===> V
517 -> forall t' B (V' : Exp t') V'', E = Cfold (Subst V' B)
518 -> V = Cfold V''
519 -> Closed1 B
520 -> Subst (Cfold V') (Cfold1 B) ===> Cfold V''.
521 induction 1; inversion 3; my_crush; ssimp; my_crush.
522
523 rewrite <- H0; auto.
524
525 apply cheat.
526 apply cheat.
527 apply cheat.
528
529 repeat rewrite (@fold_Subst_Cfold1 t') in *.
530 repeat rewrite fold_Cfold in *.
531 apply SApp with (Cfold1 B) V2.
532
533 unfold Abs, Subst, Cfold, Cfold1 in *.
534 match goal with
535 | [ |- _ ===> ?F ] =>
536 replace F with (fun var => cfold (Abs' (fun x : var _ => B var x)))
537 end.
538 apply IHBigStep1; auto.
539 ssimp.
540 apply cheat.
541 reflexivity.
542
543 replace V2 with (Cfold V2).
544 unfold Cfold, Subst.
545 apply IHBigStep2; auto.
546 apply cheat.
547 apply cheat.
548
549 replace V2 with (Cfold V2).
550 unfold Subst, Cfold.
551 apply IHBigStep3; auto.
552 apply cheat.
553 apply cheat.
554
555 apply cheat.
556 Qed.
557
558 Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2),
559 Subst (Cfold V) (Cfold1 B) ===> Cfold V'
560 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
561 Hint Resolve Cfold_Subst'.
562
563 eauto.
564 Qed.
565
566 Hint Resolve Cfold_Subst.
567
568 Theorem Cfold_correct : forall t (E V : Exp t),
569 E ===> V
570 -> Cfold E ===> Cfold V.
571 induction 1; crush; ssimp; eauto.
572
573 change ((fun H1 : type -> Type =>
574 match Cfold E1 H1 with
575 | Const' n3 =>
576 match Cfold E2 H1 with
577 | Const' n4 => Const' (var:=H1) (n3 + n4)
578 | Plus' _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
579 | Var _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
580 | App' _ _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
581 | Abs' _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
582 end
583 | Plus' _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
584 | Var _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
585 | App' _ _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
586 | Abs' _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
587 end) ===> Const (n1 + n2)).
588
589 Ltac simp :=
590 repeat match goal with
591 | [ H : _ = Cfold _ |- _ ] => rewrite <- H in *
592 | [ H : Const _ ===> Const _ |- _ ] =>
593 inversion H; clear H; my_crush
594 end.
595
596 generalize (closed (Cfold E1)); inversion 1; my_crush; simp;
597 try solve [ ssimp; simp; eauto ];
598 generalize (closed (Cfold E2)); inversion 1; my_crush; simp; ssimp; simp; eauto.
599 Qed.