From: adam <adam@megacz.com>
Date: Sun, 28 Oct 2007 22:43:11 +0000 (+0000)
Subject: better comments/documentation
X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=commitdiff_plain;h=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hp=bb471fbb694313a6aa61816752bd179b3af6711d

better comments/documentation

darcs-hash:20071028224311-5007d-c6cdcdb8a2938b6874581fabb8b6471f086859ed.gz
---

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).
diff --git a/Computation/Eval.v b/src/Computation/Eval.v
similarity index 73%
rename from Computation/Eval.v
rename to src/Computation/Eval.v
index 28a00a0..7693483 100644
--- a/Computation/Eval.v
+++ b/src/Computation/Eval.v
@@ -1,7 +1,7 @@
 Require Export Computation.Monad.
 Require Export Computation.Termination.
 
-(* evaluate up to [n] computation steps *)
+(** evaluate up to [n] computation steps *)
 Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
   match n with
     | O      => None
@@ -16,17 +16,10 @@ Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
       end
   end.
 
-Inductive Unit : Set := unit : Unit.
-
-(*
- * In theory we'd like to be able to do this (below), but it violates
- * the Prop/Set separation:
- *
- * "Elimination of an inductive object of sort Prop is not allowed on a
- *  predicate in sort Set because proofs can be eliminated only to
- *  build proofs."
+(** In theory we'd like to be able to do this (below), but it violates the Prop/Set separation.
  *)
-(*
+(**
+<<
 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
   match t with
     | (Terminates_intro t') =>
@@ -34,8 +27,13 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
         | (ex_intro x y) => x
       end
   end.
-*)
+ 
+ "Elimination of an inductive object of sort Prop is not allowed on a
+  predicate in sort Set because proofs can be eliminated only to
+  build proofs."
+>>*)
 
+Inductive Unit : Set := unit : Unit.
 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
   match eval' c Unit (Return unit) (termination_is_safe A c t) with
     | exist x pf => x
@@ -43,3 +41,4 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
 
 Implicit Arguments eval [A].
 Implicit Arguments bounded_eval [A].
+
diff --git a/Computation/Monad.v b/src/Computation/Monad.v
similarity index 79%
rename from Computation/Monad.v
rename to src/Computation/Monad.v
index 082a3dd..91df0c6 100644
--- a/Computation/Monad.v
+++ b/src/Computation/Monad.v
@@ -1,13 +1,13 @@
 Reserved Notation "# A" (at level 30).
 Section Constructors.
 
-  (* a co-inductive type representing a possibly-nonterminating computation *)
-     CoInductive Computation (A:Set) : Type :=
+  (** A co-inductive type representing a possibly-nonterminating computation *)
+      CoInductive Computation (A:Set) : Type :=
 
-  (* terminate and return a value *)
+  (** terminate and return a value *)
        | Return  : A                               -> #A
          
-  (* monadic >>= (bind) operator *)
+  (** monadic >>= (bind) operator *)
        | Bind    : forall (B:Set),  (B->#A) ->  #B -> #A
          where "# A" := (Computation A).
      Implicit Arguments Return [A].
diff --git a/Computation/Tactics.v b/src/Computation/Tactics.v
similarity index 85%
rename from Computation/Tactics.v
rename to src/Computation/Tactics.v
index c710817..67ed175 100644
--- a/Computation/Tactics.v
+++ b/src/Computation/Tactics.v
@@ -1,6 +1,6 @@
 Require Import Computation.Monad.
 
-(* decomposition lemma *)
+(** A decomposition lemma *)
 Definition decomp (A:Set)(c:#A) : #A := 
   match c with
     | Return x => Return x
@@ -8,12 +8,12 @@ Definition decomp (A:Set)(c:#A) : #A :=
   end.
 Implicit Arguments decomp.
 
-(* decomposition theorem: we can always decompose *)
+(** A decomposition theorem: we can always decompose *)
 Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c.
   intros A l; case l; simpl; trivial. 
 Qed. 
 
-(* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
+(** 1-, 2-, 3-, 4-, and 5-ary decompositions; you should use this *)
 Ltac uncomp comp :=
   match goal with
     | [ |- context[(comp ?X)] ] =>
diff --git a/Computation/Termination.v b/src/Computation/Termination.v
similarity index 86%
rename from Computation/Termination.v
rename to src/Computation/Termination.v
index a64fa6b..1497fbf 100644
--- a/Computation/Termination.v
+++ b/src/Computation/Termination.v
@@ -3,7 +3,7 @@ Require Import Coq.Logic.JMeq.
 
 Section Termination.
 
-  (* an inductive predicate proving that a given computation terminates with a particular value *)  
+  (** An inductive predicate proving that a given computation terminates with a particular value *)
   Reserved Notation "c ! y" (at level 30).
   Inductive TerminatesWith (A:Set) : #A -> A -> Prop :=
   | TerminatesReturnWith :
@@ -18,12 +18,13 @@ Section Termination.
      where "c ! y" := (TerminatesWith _ c y)
       .
   
-  (* an inductive predicate proving that a given computation terminates with /some/ value *)  
+  (** An inductive predicate proving that a given computation terminates with /some/ value *)  
   Reserved Notation "c !?" (at level 30).
   Inductive Terminates (A:Set)(c:#A) : Prop :=
     | Terminates_intro : (exists a:A, c!a) -> c!?
       where "c !?" := (Terminates _ c).
 
+  (** A predicate indicating which computations might be subcomputations of a given computation *)
   Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
   | invokesPrev : forall
     (z:#C)
@@ -40,12 +41,14 @@ Section Termination.
     (_:c!b),
     InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
 
+  (** A predicate asserting that it is safe to evaluate a computation (this is the single-constructor Prop type) *)
   Inductive Safe : forall (A:Set) (c:#A), Prop :=
     Safe_intro :
     forall (A:Set) (c:#A),
       (forall (B C:Set) (c':#B)(z:#C), InvokedBy A B C c c' z -> Safe B c')
       -> Safe A c.
 
+  (** Inversion principle for Safe *)
   Definition Safe_inv
     : forall (A B C:Set)(c:#A)(_:Safe A c)(c':#B)(z:#C)(_:InvokedBy A B C c c' z), Safe B c'.
     destruct 1.
@@ -86,6 +89,7 @@ Section Termination.
     assumption.
   Defined.
 
+  (** A lemma to help apply JMeq *)
   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).
@@ -102,7 +106,7 @@ Section Termination.
     auto.
   Qed.
 
-
+  (** If we can prove that a given computation terminates with two different values, they must be the same *)
   Lemma computation_is_deterministic :
     forall (A:Set) (c:#A) (x y:A), c!x -> c!y -> x=y.
     intros.
@@ -131,6 +135,7 @@ Section Termination.
     auto.
   Qed.
 
+  (** Any terminating computation is Safe *)
   Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
     intros.
     destruct H.