Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 354:dc99dffdf20a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Co-inductive non-termination monads
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 18:37:47 -0400
parents 3322367e955d
children 62fdf0993e05
comparison
equal deleted inserted replaced
353:3322367e955d 354:dc99dffdf20a
275 ]] 275 ]]
276 276
277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *) 277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *)
278 278
279 279
280 (** * A Non-Termination Monad *) 280 (** * A Non-Termination Monad Inspired by Domain Theory *)
281 281
282 Section computation. 282 Section computation.
283 Variable A : Type. 283 Variable A : Type.
284 284
285 Definition computation := 285 Definition computation :=
575 Defined. 575 Defined.
576 576
577 Lemma test_looper : run (looper true) tt. 577 Lemma test_looper : run (looper true) tt.
578 exists 1; reflexivity. 578 exists 1; reflexivity.
579 Qed. 579 Qed.
580
581
582 (** * Co-Inductive Non-Termination Monads *)
583
584 CoInductive thunk (A : Type) : Type :=
585 | Answer : A -> thunk A
586 | Think : thunk A -> thunk A.
587
588 CoFixpoint TBind (A B : Type) (m1 : thunk A) (m2 : A -> thunk B) : thunk B :=
589 match m1 with
590 | Answer x => m2 x
591 | Think m1' => Think (TBind m1' m2)
592 end.
593
594 CoInductive thunk_eq A : thunk A -> thunk A -> Prop :=
595 | EqAnswer : forall x, thunk_eq (Answer x) (Answer x)
596 | EqThinkL : forall m1 m2, thunk_eq m1 m2 -> thunk_eq (Think m1) m2
597 | EqThinkR : forall m1 m2, thunk_eq m1 m2 -> thunk_eq m1 (Think m2).
598
599 Section thunk_eq_coind.
600 Variable A : Type.
601 Variable P : thunk A -> thunk A -> Prop.
602
603 Hypothesis H : forall m1 m2, P m1 m2
604 -> match m1, m2 with
605 | Answer x1, Answer x2 => x1 = x2
606 | Think m1', Think m2' => P m1' m2'
607 | Think m1', _ => P m1' m2
608 | _, Think m2' => P m1 m2'
609 end.
610
611 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
612 cofix; intros;
613 match goal with
614 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
615 end; destruct m1; destruct m2; subst; repeat constructor; auto.
616 Qed.
617 End thunk_eq_coind.
618
619 Definition frob A (m : thunk A) : thunk A :=
620 match m with
621 | Answer x => Answer x
622 | Think m' => Think m'
623 end.
624
625 Theorem frob_eq : forall A (m : thunk A), frob m = m.
626 destruct m; reflexivity.
627 Qed.
628
629 Theorem thunk_eq_frob : forall A (m1 m2 : thunk A),
630 thunk_eq (frob m1) (frob m2)
631 -> thunk_eq m1 m2.
632 intros; repeat rewrite frob_eq in *; auto.
633 Qed.
634
635 Ltac findDestr := match goal with
636 | [ |- context[match ?E with Answer _ => _ | Think _ => _ end] ] =>
637 match E with
638 | context[match _ with Answer _ => _ | Think _ => _ end] => fail 1
639 | _ => destruct E
640 end
641 end.
642
643 Theorem thunk_eq_refl : forall A (m : thunk A), thunk_eq m m.
644 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = m2)); crush; findDestr; reflexivity.
645 Qed.
646
647 Hint Resolve thunk_eq_refl.
648
649 Theorem tleft_identity : forall A B (a : A) (f : A -> thunk B),
650 thunk_eq (TBind (Answer a) f) (f a).
651 intros; apply thunk_eq_frob; crush.
652 Qed.
653
654 Theorem tright_identity : forall A (m : thunk A),
655 thunk_eq (TBind m (@Answer _)) m.
656 intros; apply (thunk_eq_coind (fun m1 m2 => m1 = TBind m2 (@Answer _))); crush;
657 findDestr; reflexivity.
658 Qed.
659
660 Lemma TBind_Answer : forall (A B : Type) (v : A) (m2 : A -> thunk B),
661 TBind (Answer v) m2 = m2 v.
662 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
663 simpl; findDestr; reflexivity.
664 Qed.
665
666 Hint Rewrite TBind_Answer : cpdt.
667
668 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
669 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
670 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m,
671 m1 = TBind (TBind m f) g
672 /\ m2 = TBind m (fun x => TBind (f x) g))
673 \/ m1 = m2)); crush; eauto; repeat (findDestr; crush; eauto).
674 Qed.
675
676 CoFixpoint fact (n acc : nat) : thunk nat :=
677 match n with
678 | O => Answer acc
679 | S n' => Think (fact n' (S n' * acc))
680 end.
681
682 Inductive eval A : thunk A -> A -> Prop :=
683 | EvalAnswer : forall x, eval (Answer x) x
684 | EvalThink : forall m x, eval m x -> eval (Think m) x.
685
686 Hint Rewrite frob_eq : cpdt.
687
688 Lemma eval_frob : forall A (c : thunk A) x,
689 eval (frob c) x
690 -> eval c x.
691 crush.
692 Qed.
693
694 Theorem eval_fact : eval (fact 5 1) 120.
695 repeat (apply eval_frob; simpl; constructor).
696 Qed.
697
698 (** [[
699 CoFixpoint fib (n : nat) : thunk nat :=
700 match n with
701 | 0 => Answer 1
702 | 1 => Answer 1
703 | _ => TBind (fib (pred n)) (fun n1 =>
704 TBind (fib (pred (pred n))) (fun n2 =>
705 Answer (n1 + n2)))
706 end.
707 ]]
708 *)
709
710
711 CoInductive comp (A : Type) : Type :=
712 | Ret : A -> comp A
713 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
714
715 Inductive exec A : comp A -> A -> Prop :=
716 | ExecRet : forall x, exec (Ret x) x
717 | ExecBnd : forall B (c : comp B) (f : B -> comp A) x1 x2, exec (A := B) c x1
718 -> exec (f x1) x2
719 -> exec (Bnd c f) x2.
720
721 Hint Constructors exec.
722
723 Definition comp_eq A (c1 c2 : comp A) := forall r, exec c1 r <-> exec c2 r.
724
725 Ltac inverter := repeat match goal with
726 | [ H : exec _ _ |- _ ] => inversion H; []; crush
727 end.
728
729 Theorem cleft_identity : forall A B (a : A) (f : A -> comp B),
730 comp_eq (Bnd (Ret a) f) (f a).
731 red; crush; inverter; eauto.
732 Qed.
733
734 Theorem cright_identity : forall A (m : comp A),
735 comp_eq (Bnd m (@Ret _)) m.
736 red; crush; inverter; eauto.
737 Qed.
738
739 Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
740 exec c r
741 -> forall m, c = Bnd (Bnd m f) g
742 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
743 induction 1; crush.
744 match goal with
745 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
746 end.
747 move H3 after A.
748 generalize dependent B0.
749 do 2 intro.
750 subst.
751 crush.
752 inversion H; clear H; crush.
753 eauto.
754 Qed.
755
756 Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
757 exec c r
758 -> forall m, c = Bnd m (fun x => Bnd (f x) g)
759 -> exec (Bnd (Bnd m f) g) r.
760 induction 1; crush.
761 match goal with
762 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
763 end.
764 move H3 after B.
765 generalize dependent B0.
766 do 2 intro.
767 subst.
768 crush.
769 inversion H0; clear H0; crush.
770 eauto.
771 Qed.
772
773 Hint Resolve cassociativity1 cassociativity2.
774
775 Theorem cassociativity : forall A B C (m : comp A) (f : A -> comp B) (g : B -> comp C),
776 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)).
777 red; crush; eauto.
778 Qed.
779
780 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
781 if le_lt_dec 2 (length ls)
782 then let lss := partition ls in
783 Bnd (mergeSort'' le (fst lss)) (fun ls1 =>
784 Bnd (mergeSort'' le (snd lss)) (fun ls2 =>
785 Ret (merge le ls1 ls2)))
786 else Ret ls.
787
788 Definition frob' A (c : comp A) :=
789 match c with
790 | Ret x => Ret x
791 | Bnd _ c' f => Bnd c' f
792 end.
793
794 Lemma frob'_eq : forall A (c : comp A), frob' c = c.
795 destruct c; reflexivity.
796 Qed.
797
798 Hint Rewrite frob'_eq : cpdt.
799
800 Lemma exec_frob : forall A (c : comp A) x,
801 exec (frob' c) x
802 -> exec c x.
803 crush.
804 Qed.
805
806 Lemma test_mergeSort'' : exec (mergeSort'' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
807 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
808 repeat (apply exec_frob; simpl; econstructor).
809 Qed.
810
811 Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).
812
813 (** [[
814 Definition testCurriedAdd :=
815 Bnd (curriedAdd 2) (fun f => f 3).
816 ]]
817
818 <<
819 Error: Universe inconsistency.
820 >>
821 *)
822
823
824 (** * Comparing the Options *)
825
826 Definition curriedAdd' (n : nat) := Return (fun m : nat => Return (n + m)).
827
828 Definition testCurriedAdd :=
829 Bind (curriedAdd' 2) (fun f => f 3).
830
831 Fixpoint map A B (f : A -> computation B) (ls : list A) : computation (list B) :=
832 match ls with
833 | nil => Return nil
834 | x :: ls' => Bind (f x) (fun x' =>
835 Bind (map f ls') (fun ls'' =>
836 Return (x' :: ls'')))
837 end.
838
839 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil)) (2 :: 3 :: 4 :: nil).
840 exists 1; reflexivity.
841 Qed.