Mercurial > cpdt > repo

comparison src/Hoas.v @ 164:391ccedd0568

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)).