Require Export Relation_Definitions. Require Setoid. Require Export Computation.Monad. Require Export Computation.Termination. Require Import Coq.Logic.JMeq. (** Computational Equivalence relation *) Inductive CE (A:Set)(ca1:#A)(ca2:#A) : Prop := | CE_intro : (forall a, TerminatesWith A ca1 a <-> TerminatesWith A ca2 a) -> CE A ca1 ca2. Implicit Arguments CE [A]. (** CE is reflexive *) Theorem ce_refl : forall (A:Set)(x:#A), CE x x. intros. constructor. intros. constructor. auto. auto. Qed. (** CE is symmetric *) Theorem ce_symm : forall (A:Set)(x y:#A), (CE x y) -> (CE y x). intros. inversion H. constructor. intros. assert (TerminatesWith A x a <-> TerminatesWith A y a). apply H0. inversion H1. constructor. auto. auto. Qed. (** CE is transitive *) Theorem ce_trans : forall (A:Set)(x y z:#A), (CE x y) -> (CE y z) -> (CE x z). intros. inversion H0. inversion H. constructor. intros. assert (TerminatesWith A y a <-> TerminatesWith A z a). apply H1. assert (TerminatesWith A x a <-> TerminatesWith A y a). apply H2. inversion H3. inversion H4. constructor. auto. auto. Qed. (** CE is a relation *) Add Relation Computation CE reflexivity proved by ce_refl symmetry proved by ce_symm transitivity proved by ce_trans as CE_rel. Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B), ((c1>>=f1)=(c2>>=f2)) -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2). intros. inversion H. split. dependent rewrite H3. simpl. auto. split. dependent rewrite H2. simpl. auto. auto. Qed. Lemma inversion_lemma : forall (A B:Set)(c:#A)(f:A->#B)(b:B), TerminatesWith B (Bind f c) b -> (exists a:A, TerminatesWith A c a /\ TerminatesWith B (f a) b). intros. simple inversion H. subst. inversion H0. subst. apply jmeq_lemma in H2. inversion H2. inversion H1. subst. clear H2. clear H1. intros. apply JMeq_eq in H0. subst. exists b0. constructor. auto. clear H. clear H1. apply JMeq_eq in H3. subst. auto. Qed. (** First Monad Law *) Theorem monad_law_1 : forall (A B:Set)(a:A)(c:#A)(f:A->#B), CE (Bind f (Return a)) (f a). intros. constructor. intros. constructor. intros. apply inversion_lemma in H. inversion H. inversion H0. assert (x=a). inversion H1. subst. auto. subst. auto. intro. apply (@TerminatesBindWith B A a). constructor. auto. Qed. (** Second Monad Law *) Theorem monad_law_2 : forall (A:Set)(c:#A), CE (Bind (fun x => Return x) c) c. intros. constructor. intros. constructor. intros. apply inversion_lemma in H. inversion H. inversion H0. inversion H2. subst. auto. intros. apply (@TerminatesBindWith A A a). auto. constructor. Qed. (** Third Monad Law *) Theorem monad_law_3 : forall (A B C:Set)(a:A)(c:#A)(f:A->#B)(g:B->#C), CE (Bind g (Bind f c)) (Bind (fun x => (Bind g (f x))) c). intros. constructor. intros. constructor. intros. apply inversion_lemma in H. inversion H. inversion H0. clear H. clear H0. apply inversion_lemma in H1. inversion H1. clear H1. inversion H. clear H. apply (@TerminatesBindWith C A x0). auto. apply (@TerminatesBindWith C B x). auto. auto. intros. apply inversion_lemma in H. inversion H. inversion H0. clear H. clear H0. apply inversion_lemma in H2. inversion H2. clear H2. inversion H. clear H. apply (@TerminatesBindWith C B x0). apply (@TerminatesBindWith B A x). auto. auto. auto. Qed.