X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FEquivalence.v;fp=Computation%2FEquivalence.v;h=1ea567c63beaefdd965941c7cee6717ed0d3d3cd;hp=ad8b9adad834a06145380cf37511b25908dd4bc2;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d

diff --git a/Computation/Equivalence.v b/src/Computation/Equivalence.v
similarity index 86%
rename from Computation/Equivalence.v
rename to src/Computation/Equivalence.v
index ad8b9ad..1ea567c 100644
--- a/Computation/Equivalence.v
+++ b/src/Computation/Equivalence.v
@@ -4,6 +4,7 @@ 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 :=
@@ -17,6 +18,7 @@ Inductive CE
     -> CE A ca1 ca2.
 Implicit Arguments CE [A].
 
+(** CE is reflexive *)
 Theorem ce_refl :
    forall (A:Set)(x:#A),
      CE x x.
@@ -28,6 +30,7 @@ Theorem ce_refl :
   auto.
 Qed.
 
+(** CE is symmetric *)
 Theorem ce_symm :
    forall (A:Set)(x y:#A),
      (CE x y) ->
@@ -44,6 +47,7 @@ Theorem ce_symm :
   auto.
 Qed.
 
+(** CE is transitive *)
 Theorem ce_trans :
    forall (A:Set)(x y z:#A),
      (CE x y) ->
@@ -63,27 +67,28 @@ Theorem ce_trans :
   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.
+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),
@@ -117,6 +122,7 @@ Lemma inversion_lemma :
   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).
@@ -140,6 +146,7 @@ Theorem monad_law_1 :
   auto.
 Qed.
 
+(** Second Monad Law *)
 Theorem monad_law_2 :
   forall (A:Set)(c:#A),
      CE (Bind (fun x => Return x) c) c.
@@ -160,6 +167,7 @@ Theorem monad_law_2 :
   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).