--- /dev/null
+Require Export Relation_Definitions.
+Require Setoid.
+Require Export Computation.Monad.
+Require Export Computation.Termination.
+Require Import Coq.Logic.JMeq.
+
+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].
+
+Theorem ce_refl :
+ forall (A:Set)(x:#A),
+ CE x x.
+ intros.
+ constructor.
+ intros.
+ constructor.
+ auto.
+ auto.
+Qed.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
\ No newline at end of file