Mercurial > cpdt > repo
comparison src/Hoas.v @ 164:391ccedd0568
Cfold_correct, with a handful of cheating in the substitution lemma
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 04 Nov 2008 18:34:31 -0500 |
parents | ba306bf9ec80 |
children | cf60d8dc57c9 |
comparison
equal
deleted
inserted
replaced
163:ba306bf9ec80 | 164:391ccedd0568 |
---|---|
123 where "E1 ==> E2" := (Step E1 E2). | 123 where "E1 ==> E2" := (Step E1 E2). |
124 | 124 |
125 Hint Constructors isCtx Step. | 125 Hint Constructors isCtx Step. |
126 | 126 |
127 Inductive Closed : forall t, Exp t -> Prop := | 127 Inductive Closed : forall t, Exp t -> Prop := |
128 | CConst : forall b, | 128 | CConst : forall n, |
129 Closed (Const b) | 129 Closed (Const n) |
130 | CPlus : forall E1 E2, | 130 | CPlus : forall E1 E2, |
131 Closed E1 | 131 Closed E1 |
132 -> Closed E2 | 132 -> Closed E2 |
133 -> Closed (Plus E1 E2) | 133 -> Closed (Plus E1 E2) |
134 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2, | 134 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2, |
366 Lemma fold_Cfold1 : forall t1 t2 (E : Exp1 t1 t2), | 366 Lemma fold_Cfold1 : forall t1 t2 (E : Exp1 t1 t2), |
367 (fun _ x => cfold (E _ x)) = Cfold1 E. | 367 (fun _ x => cfold (E _ x)) = Cfold1 E. |
368 reflexivity. | 368 reflexivity. |
369 Qed. | 369 Qed. |
370 | 370 |
371 Hint Rewrite fold_Cfold1 : fold. | |
372 | |
371 Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1), | 373 Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1), |
372 (fun _ => flatten (cfold (E _ (V _)))) | 374 (fun _ => flatten (cfold (E _ (V _)))) |
373 = Subst V (Cfold1 E). | 375 = Subst V (Cfold1 E). |
374 reflexivity. | 376 reflexivity. |
375 Qed. | 377 Qed. |
398 (fun _ => flatten (E1 _ (V _))) = Subst V E1. | 400 (fun _ => flatten (E1 _ (V _))) = Subst V E1. |
399 reflexivity. | 401 reflexivity. |
400 Qed. | 402 Qed. |
401 | 403 |
402 Hint Rewrite fold_Subst : fold. | 404 Hint Rewrite fold_Subst : fold. |
403 | |
404 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t. | |
405 | |
406 Definition ConstN G (n : nat) : ExpN G Nat := | |
407 fun _ _ => Const' n. | |
408 Definition VarN G t (m : member t G) : ExpN G t := fun _ s => Var (hget s m). | |
409 Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat := | |
410 fun _ s => Plus' (E1 _ s) (E2 _ s). | |
411 Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran := | |
412 fun _ s => App' (F _ s) (X _ s). | |
413 Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) := | |
414 fun _ s => Abs' (fun x => B _ (x ::: s)). | |
415 | |
416 Inductive ClosedN : forall G t, ExpN G t -> Prop := | |
417 | CConstN : forall G b, | |
418 ClosedN (ConstN G b) | |
419 | CPlusN : forall G (E1 E2 : ExpN G _), | |
420 ClosedN E1 | |
421 -> ClosedN E2 | |
422 -> ClosedN (PlusN E1 E2) | |
423 | CAppN : forall G dom ran (E1 : ExpN G (dom --> ran)) E2, | |
424 ClosedN E1 | |
425 -> ClosedN E2 | |
426 -> ClosedN (AppN E1 E2) | |
427 | CAbsN : forall G dom ran (E1 : ExpN (dom :: G) ran), | |
428 ClosedN E1 | |
429 -> ClosedN (AbsN E1). | |
430 | |
431 Axiom closedN : forall G t (E : ExpN G t), ClosedN E. | |
432 | |
433 Hint Resolve closedN. | |
434 | 405 |
435 Section Closed1. | 406 Section Closed1. |
436 Variable xt : type. | 407 Variable xt : type. |
437 | 408 |
438 Definition Const1 (n : nat) : Exp1 xt Nat := | 409 Definition Const1 (n : nat) : Exp1 xt Nat := |
444 fun _ s => App' (F _ s) (X _ s). | 415 fun _ s => App' (F _ s) (X _ s). |
445 Definition Abs1 dom ran (B : forall var, var dom -> Exp1 xt ran) : Exp1 xt (dom --> ran) := | 416 Definition Abs1 dom ran (B : forall var, var dom -> Exp1 xt ran) : Exp1 xt (dom --> ran) := |
446 fun _ s => Abs' (fun x => B _ x _ s). | 417 fun _ s => Abs' (fun x => B _ x _ s). |
447 | 418 |
448 Inductive Closed1 : forall t, Exp1 xt t -> Prop := | 419 Inductive Closed1 : forall t, Exp1 xt t -> Prop := |
449 | CConst1 : forall b, | 420 | CConst1 : forall n, |
450 Closed1 (Const1 b) | 421 Closed1 (Const1 n) |
451 | CPlus1 : forall E1 E2, | 422 | CPlus1 : forall E1 E2, |
452 Closed1 E1 | 423 Closed1 E1 |
453 -> Closed1 E2 | 424 -> Closed1 E2 |
454 -> Closed1 (Plus1 E1 E2) | 425 -> Closed1 (Plus1 E1 E2) |
455 | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2, | 426 | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2, |
462 Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E. | 433 Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E. |
463 End Closed1. | 434 End Closed1. |
464 | 435 |
465 Hint Resolve closed1. | 436 Hint Resolve closed1. |
466 | 437 |
467 Definition CfoldN G t (E : ExpN G t) : ExpN G t := fun _ s => cfold (E _ s). | 438 Ltac ssimp := unfold Subst, Cfold in *; simpl in *; autorewrite with fold in *; |
468 | |
469 Theorem fold_CfoldN : forall G t (E : ExpN G t), | |
470 (fun _ s => cfold (E _ s)) = CfoldN E. | |
471 reflexivity. | |
472 Qed. | |
473 | |
474 Definition SubstN t1 G t2 (E1 : ExpN G t1) (E2 : ExpN (G ++ t1 :: nil) t2) : ExpN G t2 := | |
475 fun _ s => flatten (E2 _ (hmap (@Var _) s +++ E1 _ s ::: hnil)). | |
476 | |
477 Lemma fold_SubstN : forall t1 G t2 (E1 : ExpN G t1) (E2 : ExpN (G ++ t1 :: nil) t2), | |
478 (fun _ s => flatten (E2 _ (hmap (@Var _) s +++ E1 _ s ::: hnil))) = SubstN E1 E2. | |
479 reflexivity. | |
480 Qed. | |
481 | |
482 Hint Rewrite fold_CfoldN fold_SubstN : fold. | |
483 | |
484 Ltac ssimp := unfold Subst, Cfold, CfoldN, SubstN in *; simpl in *; autorewrite with fold in *; | |
485 repeat match goal with | 439 repeat match goal with |
486 | [ xt : type |- _ ] => | 440 | [ xt : type |- _ ] => |
487 rewrite (@fold_Subst xt) in * | 441 rewrite (@fold_Subst xt) in * |
488 end; | 442 end; |
489 autorewrite with fold in *. | 443 autorewrite with fold in *. |
490 | 444 |
491 Ltac uiper := | 445 Lemma Cfold_Subst' : forall t (E V : Exp t), |
492 repeat match goal with | 446 E ===> V |
493 | [ H : _ = _ |- _ ] => | 447 -> forall t' B (V' : Exp t') V'', E = Cfold (Subst V' B) |
494 generalize H; subst; intro H; rewrite (UIP_refl _ _ H) | 448 -> V = Cfold V'' |
495 end. | 449 -> Closed1 B |
496 | 450 -> Subst (Cfold V') (Cfold1 B) ===> Cfold V''. |
497 Section eq_arg. | 451 induction 1; inversion 3; my_crush; ssimp; my_crush. |
498 Variable A : Type. | 452 |
499 Variable B : A -> Type. | 453 rewrite <- H0; auto. |
500 | 454 |
501 Variable x : A. | 455 apply cheat. |
502 | 456 apply cheat. |
503 Variables f g : forall x, B x. | 457 apply cheat. |
504 Hypothesis Heq : f = g. | 458 |
505 | 459 repeat rewrite (@fold_Subst_Cfold1 t') in *. |
506 Theorem eq_arg : f x = g x. | 460 repeat rewrite fold_Cfold in *. |
507 congruence. | 461 apply SApp with (Cfold1 B) V2. |
508 Qed. | 462 |
509 End eq_arg. | 463 unfold Abs, Subst, Cfold, Cfold1 in *. |
510 | |
511 Implicit Arguments eq_arg [A B f g]. | |
512 | |
513 (*Lemma Cfold_Subst_comm : forall G t (E : ExpN G t), | |
514 ClosedN E | |
515 -> forall t1 G' (pf : G = G' ++ t1 :: nil) V, | |
516 CfoldN (SubstN V (match pf in _ = G return ExpN G _ with refl_equal => E end)) | |
517 = SubstN (CfoldN V) (CfoldN (match pf in _ = G return ExpN G _ with refl_equal => E end)). | |
518 induction 1; my_crush; uiper; ssimp; crush; | |
519 unfold ExpN; do 2 ext_eq. | |
520 | |
521 generalize (eq_arg x0 (eq_arg x (IHClosedN1 _ _ (refl_equal _) V))). | |
522 generalize (eq_arg x0 (eq_arg x (IHClosedN2 _ _ (refl_equal _) V))). | |
523 crush. | |
524 | |
525 match goal with | 464 match goal with |
526 | [ |- _ = flatten (match ?E with | 465 | [ |- _ ===> ?F ] => |
527 | Const' _ => _ | 466 replace F with (fun var => cfold (Abs' (fun x : var _ => B var x))) |
528 | Plus' _ _ => _ | 467 end. |
529 | Var _ _ => _ | 468 apply IHBigStep1; auto. |
530 | App' _ _ _ _ => _ | 469 apply cheat. |
531 | Abs' _ _ _ => _ | 470 reflexivity. |
532 end) ] => dep_destruct E | 471 |
533 end; crush. | 472 replace V2 with (Cfold V2). |
534 | 473 unfold Cfold, Subst. |
535 match goal with | 474 apply IHBigStep2; auto. |
536 | [ |- _ = flatten (match ?E with | 475 apply cheat. |
537 | Const' _ => _ | 476 apply cheat. |
538 | Plus' _ _ => _ | 477 |
539 | Var _ _ => _ | 478 replace V2 with (Cfold V2). |
540 | App' _ _ _ _ => _ | 479 unfold Subst, Cfold. |
541 | Abs' _ _ _ => _ | 480 apply IHBigStep3; auto. |
542 end) ] => dep_destruct E | 481 apply cheat. |
543 end; crush. | 482 apply cheat. |
544 | 483 |
545 match goal with | 484 apply cheat. |
546 | [ |- match ?E with | 485 Qed. |
547 | Const' _ => _ | |
548 | Plus' _ _ => _ | |
549 | Var _ _ => _ | |
550 | App' _ _ _ _ => _ | |
551 | Abs' _ _ _ => _ | |
552 end = _ ] => dep_destruct E | |
553 end; crush. | |
554 rewrite <- H2. | |
555 | |
556 dep_destruct e. | |
557 intro | |
558 | |
559 | |
560 apply cheat. | |
561 | |
562 unfold ExpN; do 2 ext_eq. | |
563 generalize (eq_arg x0 (eq_arg x (IHClosedN1 _ _ (refl_equal _) V))). | |
564 generalize (eq_arg x0 (eq_arg x (IHClosedN2 _ _ (refl_equal _) V))). | |
565 congruence. | |
566 | |
567 unfold ExpN; do 2 ext_eq. | |
568 f_equal. | |
569 ext_eq. | |
570 exact (eq_arg (x1 ::: x0) (eq_arg x (IHClosedN _ (dom :: G') (refl_equal _) (fun _ s => V _ (snd s))))). | |
571 Qed.*) | |
572 | |
573 Lemma Cfold_Subst' : forall t (E V' : Exp t), | |
574 E ===> V' | |
575 -> forall G xt (V : ExpN G xt) B, E = SubstN V B | |
576 -> ClosedN B | |
577 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. | |
578 induction 1; inversion 2; my_crush; ssimp. | |
579 | |
580 auto. | |
581 | |
582 apply cheat. | |
583 | |
584 my_crush. | |
585 econstructor. | |
586 instantiate (1 := Cfold1 B). | |
587 unfold Subst, Cfold1 in *; eauto. | |
588 unfold Subst, Cfold1 in *; eauto. | |
589 unfold Subst, Cfold; eauto. | |
590 | |
591 my_crush; ssimp. | |
592 | |
593 | |
594 | |
595 | |
596 Lemma Cfold_Subst' : forall t (B : Exp1 xt t), | |
597 Closed1 B | |
598 -> forall V', Subst V B ===> V' | |
599 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. | |
600 induction 1; my_crush; ssimp. | |
601 | |
602 inversion H; my_crush. | |
603 | |
604 apply cheat. | |
605 | |
606 inversion H1; my_crush. | |
607 econstructor. | |
608 instantiate (1 := Cfold1 B). | |
609 eauto. | |
610 change (Abs (Cfold1 B)) with (Cfold (Abs B)). | |
611 auto. | |
612 eauto. | |
613 eauto. | |
614 | |
615 apply IHClosed1_1. | |
616 eauto. | |
617 | |
618 match goal with | |
619 | [ (*H : ?F = ?G,*) H2 : ?X (fun _ => unit) = ?Y _ _ _ _ (fun _ => unit) |- _ ] => | |
620 idtac(*match X with | |
621 | Y => fail 1 | |
622 | _ => | |
623 idtac(*assert (X = Y); [ unfold Exp; apply ext_eq; intro var; | |
624 let H' := fresh "H'" in | |
625 assert (H' : F var = G var); [ congruence | |
626 | match type of H' with | |
627 | ?X = ?Y => | |
628 let X := eval hnf in X in | |
629 let Y := eval hnf in Y in | |
630 change (X = Y) in H' | |
631 end; injection H'; clear H'; my_crush' ] | |
632 | my_crush'; clear H2 ]*) | |
633 end*) | |
634 end. | |
635 | |
636 clear H5 H3. | |
637 my_crush. | |
638 | |
639 | |
640 unfold Subst in *; simpl in *; autorewrite with fold in *. | |
641 | |
642 | |
643 Check fold_Subst. | |
644 | |
645 repeat rewrite (@fold_Subst t1) in *. | |
646 | |
647 simp (Subst (t2 := Nat) V). | |
648 | |
649 | |
650 induction 1; my_crush. | |
651 End Exp1. | |
652 | |
653 Axiom closed1 : forall t1 t2 (E : Exp1 t1 t2), Closed1 E. | |
654 | |
655 | |
656 | |
657 Lemma Cfold_Subst' : forall t1 (V : Exp t1) t2 (B : Exp1 t1 t2), | |
658 Closed1 B | |
659 -> forall V', Subst V B ===> V' | |
660 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. | |
661 induction 1; my_crush. | |
662 | |
663 unfold Subst in *; simpl in *; autorewrite with fold in *. | |
664 inversion H; my_crush. | |
665 | |
666 unfold Subst in *; simpl in *; autorewrite with fold in *. | |
667 Check fold_Subst. | |
668 | |
669 repeat rewrite (@fold_Subst t1) in *. | |
670 | |
671 simp (Subst (t2 := Nat) V). | |
672 | |
673 | |
674 induction 1; my_crush. | |
675 | 486 |
676 Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2), | 487 Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2), |
677 Subst V B ===> V' | 488 Subst (Cfold V) (Cfold1 B) ===> Cfold V' |
678 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. | 489 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. |
490 Hint Resolve Cfold_Subst'. | |
491 | |
492 eauto. | |
493 Qed. | |
494 | |
495 Hint Resolve Cfold_Subst. | |
679 | 496 |
680 Theorem Cfold_correct : forall t (E V : Exp t), | 497 Theorem Cfold_correct : forall t (E V : Exp t), |
681 E ===> V | 498 E ===> V |
682 -> Cfold E ===> Cfold V. | 499 -> Cfold E ===> Cfold V. |
683 induction 1; unfold Cfold in *; crush; simp; auto. | 500 induction 1; unfold Cfold in *; crush; ssimp; eauto. |
684 | 501 |
685 simp. | 502 change ((fun H1 : type -> Type => |
686 simp. | 503 match Cfold E1 H1 with |
687 apply cheat. | 504 | Const' n3 => |
688 | 505 match Cfold E2 H1 with |
689 simp. | 506 | Const' n4 => Const' (var:=H1) (n3 + n4) |
690 econstructor; eauto. | 507 | Plus' _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
691 | 508 | Var _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
692 | 509 | App' _ _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
693 | 510 | Abs' _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
694 match goal with | |
695 | [ |- ?E ===> ?V ] => | |
696 try simp1 ltac:(fun E' => change (E' ===> V)); | |
697 try match goal with | |
698 | [ |- ?E' ===> _ ] => | |
699 simp1 ltac:(fun V' => change (E' ===> V')) | |
700 end | |
701 | [ H : ?E ===> ?V |- _ ] => | |
702 try simp1 ltac:(fun E' => change (E' ===> V) in H); | |
703 try match type of H with | |
704 | ?E' ===> _ => | |
705 simp1 ltac:(fun V' => change (E' ===> V') in H) | |
706 end | |
707 end. | |
708 simp. | |
709 | |
710 let H := IHBigStep1 in | |
711 match type of H with | |
712 | ?E ===> ?V => | |
713 try simp1 ltac:(fun E' => change (E' ===> V) in H); | |
714 try match type of H with | |
715 | ?E' ===> _ => | |
716 simp1 ltac:(fun V' => change (E' ===> V') in H) | |
717 end | 511 end |
718 end. | 512 | Plus' _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
719 | 513 | Var _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
720 try simp1 ltac:(fun E' => change (E' ===> V) in H) | 514 | App' _ _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
721 end. | 515 | Abs' _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1)) |
722 | 516 end) ===> Const (n1 + n2)). |
723 simp. | 517 |
724 | 518 Ltac simp := |
725 try simp1 ltac:(fun E' => change (fun H : type -> Type => cfold (E1 H)) with E' in IHBigStep1). | 519 repeat match goal with |
726 try simp1 ltac:(fun V' => change (fun H : type -> Type => | 520 | [ H : _ = Cfold _ |- _ ] => rewrite <- H in * |
727 Abs' (dom:=dom) (fun x : H dom => cfold (B H x))) with V' in IHBigStep1). | 521 | [ H : Const _ ===> Const _ |- _ ] => |
728 | 522 inversion H; clear H; my_crush |
729 simp1 ltac:(fun E => change ((fun H : type -> Type => cfold (E1 H)) ===> E) in IHBigStep1). | 523 end. |
730 | 524 |
731 change ((fun H : type -> Type => cfold (E1 H)) ===> Abs (fun _ x => cfold (B _ x))) in IHBigStep1. | 525 generalize (closed (Cfold E1)); inversion 1; my_crush; simp; |
732 (fun H : type -> Type => | 526 try solve [ ssimp; simp; eauto ]; |
733 Abs' (dom:=dom) (fun x : H dom => cfold (B H x))) | 527 generalize (closed (Cfold E2)); inversion 1; my_crush; simp; ssimp; simp; eauto. |
734 | 528 Qed. |
735 fold Cfold. | |
736 | |
737 | |
738 | |
739 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t. | |
740 | |
741 Definition ConstN G (n : nat) : ExpN G Nat := | |
742 fun _ _ => Const' n. | |
743 Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat := | |
744 fun _ s => Plus' (E1 _ s) (E2 _ s). | |
745 Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran := | |
746 fun _ s => App' (F _ s) (X _ s). | |
747 Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) := | |
748 fun _ s => Abs' (fun x => B _ (x ::: s)). |