X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FTermination.v;fp=Computation%2FTermination.v;h=1497fbf2d9ed3ce06c88b0c326466100d1ac2b41;hp=a64fa6b3bf2fc45ac7c48959ffb049d3e9d1074b;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d;ds=sidebyside

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.