Mercurial > cpdt > repo

comparison src/Hoas.v @ 163:ba306bf9ec80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Feeling stuck with Hoas
author Adam Chlipala <adamc@hcoop.net>
date Tue, 04 Nov 2008 16:45:50 -0500
parents df02642f93b8
children 391ccedd0568
comparison
equal deleted inserted replaced
162:df02642f93b8 163:ba306bf9ec80
138 | CAbs : forall dom ran (E1 : Exp1 dom ran), 138 | CAbs : forall dom ran (E1 : Exp1 dom ran),
139 Closed (Abs E1). 139 Closed (Abs E1).
140 140
141 Axiom closed : forall t (E : Exp t), Closed E. 141 Axiom closed : forall t (E : Exp t), Closed E.
142 142
143 Ltac my_subst :=
144 repeat match goal with
145 | [ x : type |- _ ] => subst x
146 end.
147
143 Ltac my_crush' := 148 Ltac my_crush' :=
144 crush; 149 crush; my_subst;
145 repeat (match goal with 150 repeat (match goal with
146 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H 151 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
147 end; crush). 152 end; crush; my_subst).
153
154 Ltac equate_conj F G :=
155 match constr:(F, G) with
156 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
157 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
158 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
159 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
160 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
161 end.
148 162
149 Ltac my_crush := 163 Ltac my_crush :=
150 my_crush'; 164 my_crush';
151 try (match goal with 165 repeat (match goal with
152 | [ H : ?F = ?G |- _ ] => 166 | [ H : ?F = ?G |- _ ] =>
153 match goal with 167 (let H' := fresh "H'" in
154 (*| [ _ : F (fun _ => unit) = G (fun _ => unit) |- _ ] => fail 1*) 168 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
155 | _ => 169 | discriminate || injection H'; clear H' ];
156 let H' := fresh "H'" in 170 my_crush';
157 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence 171 repeat match goal with
158 | discriminate || injection H' ]; 172 | [ H : context[fun _ => unit] |- _ ] => clear H
159 clear H' 173 end;
160 end 174 match type of H with
161 end; my_crush'); 175 | ?F = ?G =>
162 repeat match goal with 176 let ec := equate_conj F G in
163 | [ H : ?F = ?G, H2 : ?X (fun _ => unit) = ?Y (fun _ => unit) |- _ ] => 177 let var := fresh "var" in
164 match X with 178 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
165 | Y => fail 1 179 assert (H' : F var = G var); try congruence;
166 | _ => 180 match type of H' with
167 assert (X = Y); [ unfold Exp; apply ext_eq; intro var; 181 | ?X = ?Y =>
168 let H' := fresh "H'" in 182 let X := eval hnf in X in
169 assert (H' : F var = G var); [ congruence 183 let Y := eval hnf in Y in
170 | match type of H' with 184 change (X = Y) in H'
171 | ?X = ?Y => 185 end; injection H'; my_crush'; tauto
172 let X := eval hnf in X in 186 | intuition; subst ]
173 let Y := eval hnf in Y in 187 end);
174 change (X = Y) in H' 188 clear H
175 end; injection H'; clear H'; my_crush' ] 189 end; my_crush');
176 | my_crush'; clear H2 ] 190 my_crush'.
177 end
178 end.
179 191
180 Hint Extern 1 (_ = _ @ _) => simpl. 192 Hint Extern 1 (_ = _ @ _) => simpl.
181 193
182 Lemma progress' : forall t (E : Exp t), 194 Lemma progress' : forall t (E : Exp t),
183 Closed E 195 Closed E
340 | Abs' _ _ e' => Abs' (fun x => cfold (e' x)) 352 | Abs' _ _ e' => Abs' (fun x => cfold (e' x))
341 end. 353 end.
342 End cfold. 354 End cfold.
343 355
344 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). 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 Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1),
372 (fun _ => flatten (cfold (E _ (V _))))
373 = Subst V (Cfold1 E).
374 reflexivity.
375 Qed.
376
377 Axiom cheat : forall T, T.
378
379
380 Lemma fold_Const : forall n, (fun _ => Const' n) = Const n.
381 reflexivity.
382 Qed.
383 Lemma fold_Plus : forall (E1 E2 : Exp _), (fun _ => Plus' (E1 _) (E2 _)) = Plus E1 E2.
384 reflexivity.
385 Qed.
386 Lemma fold_App : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom),
387 (fun _ => App' (F _) (X _)) = App F X.
388 reflexivity.
389 Qed.
390 Lemma fold_Abs : forall dom ran (B : Exp1 dom ran),
391 (fun _ => Abs' (B _)) = Abs B.
392 reflexivity.
393 Qed.
394
395 Hint Rewrite fold_Const fold_Plus fold_App fold_Abs : fold.
396
397 Lemma fold_Subst : forall t1 t2 (E1 : Exp1 t1 t2) (V : Exp t1),
398 (fun _ => flatten (E1 _ (V _))) = Subst V E1.
399 reflexivity.
400 Qed.
401
402 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
435 Section Closed1.
436 Variable xt : type.
437
438 Definition Const1 (n : nat) : Exp1 xt Nat :=
439 fun _ _ => Const' n.
440 Definition Var1 : Exp1 xt xt := fun _ x => Var x.
441 Definition Plus1 (E1 E2 : Exp1 xt Nat) : Exp1 xt Nat :=
442 fun _ s => Plus' (E1 _ s) (E2 _ s).
443 Definition App1 dom ran (F : Exp1 xt (dom --> ran)) (X : Exp1 xt dom) : Exp1 xt ran :=
444 fun _ s => App' (F _ s) (X _ s).
445 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).
447
448 Inductive Closed1 : forall t, Exp1 xt t -> Prop :=
449 | CConst1 : forall b,
450 Closed1 (Const1 b)
451 | CPlus1 : forall E1 E2,
452 Closed1 E1
453 -> Closed1 E2
454 -> Closed1 (Plus1 E1 E2)
455 | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2,
456 Closed1 E1
457 -> Closed1 E2
458 -> Closed1 (App1 E1 E2)
459 | CAbs1 : forall dom ran (E1 : forall var, var dom -> Exp1 _ ran),
460 Closed1 (Abs1 E1).
461
462 Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E.
463 End Closed1.
464
465 Hint Resolve closed1.
466
467 Definition CfoldN G t (E : ExpN G t) : ExpN G t := fun _ s => cfold (E _ s).
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
486 | [ xt : type |- _ ] =>
487 rewrite (@fold_Subst xt) in *
488 end;
489 autorewrite with fold in *.
490
491 Ltac uiper :=
492 repeat match goal with
493 | [ H : _ = _ |- _ ] =>
494 generalize H; subst; intro H; rewrite (UIP_refl _ _ H)
495 end.
496
497 Section eq_arg.
498 Variable A : Type.
499 Variable B : A -> Type.
500
501 Variable x : A.
502
503 Variables f g : forall x, B x.
504 Hypothesis Heq : f = g.
505
506 Theorem eq_arg : f x = g x.
507 congruence.
508 Qed.
509 End eq_arg.
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
526 | [ |- _ = flatten (match ?E with
527 | Const' _ => _
528 | Plus' _ _ => _
529 | Var _ _ => _
530 | App' _ _ _ _ => _
531 | Abs' _ _ _ => _
532 end) ] => dep_destruct E
533 end; crush.
534
535 match goal with
536 | [ |- _ = flatten (match ?E with
537 | Const' _ => _
538 | Plus' _ _ => _
539 | Var _ _ => _
540 | App' _ _ _ _ => _
541 | Abs' _ _ _ => _
542 end) ] => dep_destruct E
543 end; crush.
544
545 match goal with
546 | [ |- match ?E with
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
676 Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2),
677 Subst V B ===> V'
678 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
679
680 Theorem Cfold_correct : forall t (E V : Exp t),
681 E ===> V
682 -> Cfold E ===> Cfold V.
683 induction 1; unfold Cfold in *; crush; simp; auto.
684
685 simp.
686 simp.
687 apply cheat.
688
689 simp.
690 econstructor; eauto.
691
692
693
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
718 end.
719
720 try simp1 ltac:(fun E' => change (E' ===> V) in H)
721 end.
722
723 simp.
724
725 try simp1 ltac:(fun E' => change (fun H : type -> Type => cfold (E1 H)) with E' in IHBigStep1).
726 try simp1 ltac:(fun V' => change (fun H : type -> Type =>
727 Abs' (dom:=dom) (fun x : H dom => cfold (B H x))) with V' in IHBigStep1).
728
729 simp1 ltac:(fun E => change ((fun H : type -> Type => cfold (E1 H)) ===> E) in IHBigStep1).
730
731 change ((fun H : type -> Type => cfold (E1 H)) ===> Abs (fun _ x => cfold (B _ x))) in IHBigStep1.
732 (fun H : type -> Type =>
733 Abs' (dom:=dom) (fun x : H dom => cfold (B H x)))
734
735 fold Cfold.
736
345 737
346 738
347 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t. 739 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t.
348 740
349 Definition ConstN G (n : nat) : ExpN G Nat := 741 Definition ConstN G (n : nat) : ExpN G Nat :=