better comments/documentation

[coinductive-monad.git] / src / Computation / Termination.v

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 (file)
--- a/Computation/Termination.v
+++ b/src/Computation/Termination.v
@@ -3,7 +3,7 @@ Require Import Coq.Logic.JMeq.
 
 Section Termination.
 
 
 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 :
   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)
       .
   
      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).
 
   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)
   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.
 
     (_: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.
 
   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.
   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.
 
     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).
   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.
 
     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.
   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.
 
     auto.
   Qed.
 

+  (** Any terminating computation is Safe *)

   Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
     intros.
     destruct H.
   Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
     intros.
     destruct H.