change Terminates to (exists x, TerminatesWith x) and improve notation

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

diff --git a/Computation/Termination.v b/Computation/Termination.v
index d20d57a..a64fa6b 100644 (file)
--- a/Computation/Termination.v
+++ b/Computation/Termination.v
@@ -3,62 +3,27 @@ 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 :
     forall (a:A),
-      TerminatesWith A (Return a) a
+      (Return a)!a
       
   | TerminatesBindWith :
     forall (B:Set) (b:B) (a:A) (f:B->#A) (c:#B),
-      (TerminatesWith B c b)
-      -> TerminatesWith A (f b) a
-      -> TerminatesWith A (@Bind A B f c) a
+      c!b
+      -> (f b)!a
+      -> (c >>= f)!a
+     where "c ! y" := (TerminatesWith _ c y)
       .
   
-     (* an inductive predicate proving that a given computation terminates with /some/ value *)  
-  Inductive Terminates (A:Set) : #A -> Prop :=
-  | TerminatesReturn :
-    forall (a:A),
-      Terminates A (Return a)
-      
-  | TerminatesBind :
-    forall (B:Set) (f:B->#A) (c:#B),
-      Terminates B c
-      -> (forall (b:B), (TerminatesWith B c b) -> Terminates A (f b))
-      -> Terminates A (@Bind A B f c)
-      .
+  (* 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).
 
-  Lemma terminating_computations_must_produce_a_value
-    : forall (A:Set) (c:#A), Terminates A c -> ex (fun a:A => TerminatesWith A c a).
-    induction 1.
-    
-    exists a.
-    constructor.
-    
-    elim IHTerminates.
-    intros.
-    clear IHTerminates.
-    
-    assert (exists a : A, TerminatesWith A (f x) a).
-    apply H1.
-    assumption.
-    
-    elim H3.
-    intros.
-    
-    exists x0.
-    apply (TerminatesBindWith A B x x0 f c).
-    assumption.
-    assumption.
-  Defined.
-
-  Theorem coerce : forall (A B:Set)(pf:A=B)(a:#A), #B.
-    intros.
-    subst.
-    exact a.
-  Defined.
-  
   Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
   | invokesPrev : forall
     (z:#C)
@@ -72,7 +37,7 @@ Section Termination.
     (pf:#A->#B)
     (eqpf:A=B)
     (_:JMeq (pf (f b)) (f b))
-    (_:TerminatesWith C c b),
+    (_:c!b),
     InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
 
   Inductive Safe : forall (A:Set) (c:#A), Prop :=
@@ -87,13 +52,13 @@ Section Termination.
     apply (H B).
   Defined.
 
-  Notation "! c :: A" := {a:A|TerminatesWith A c a} (at level 5).
+  Notation "{ c }!" := {a:_|TerminatesWith _ c a} (at level 5).
   Notation "'!Let' x := y 'in' z" := ((fun x => z)y)(at level 100).
-  Definition eval' CC cc (Z:Set) (z:#Z) (s:Safe CC cc) : (!cc::CC).
+  Definition eval' CC cc (Z:Set) (z:#Z) (s:Safe CC cc) : {cc}!.
     refine(
       !Let eval_one_step :=
         fun C c Z z =>
-          match c return (forall PRED pred Z z, InvokedBy C PRED Z c pred z -> !pred::PRED) -> !c::C with
+          match c return (forall PRED pred Z z, InvokedBy C PRED Z c pred z -> {pred}!) -> {c}! with
             | Return x => fun _ => exist _ x _
             | Bind CN f cn =>
               fun eval_pred =>
@@ -105,7 +70,7 @@ Section Termination.
                 end
           end
           in
-          fix eval_all C c Z z (s:Safe C c) {struct s} : !c::C :=
+          fix eval_all C c Z z (s:Safe C c) {struct s} : {c}! :=
           eval_one_step C c Z z (fun C' c' Z z icc => eval_all C' c' Z z (Safe_inv C C' Z c s c' z icc))
     ).
     
@@ -137,9 +102,40 @@ Section Termination.
     auto.
   Qed.
 
-  Theorem termination_is_safe : forall (A:Set) (c:#A) (t:Terminates A c), Safe A c.
+
+  Lemma computation_is_deterministic :
+    forall (A:Set) (c:#A) (x y:A), c!x -> c!y -> x=y.
+    intros.
+    generalize H0.
+    clear H0.
+    induction H.
+    intros.
+    inversion H0.
+    auto.
+
     intros.
-    induction t.
+    simple inversion H1.
+    inversion H2.
+    
+    apply jmeq_lemma in H4.
+    destruct H4.
+    destruct H3.
+    subst.
+    apply JMeq_eq in H2.
+    apply JMeq_eq in H3.
+    subst.
+    intros.
+    apply IHTerminatesWith2.
+    apply IHTerminatesWith1 in H2.
+    subst.
+    auto.
+  Qed.
+
+  Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
+    intros.
+    destruct H.
+    destruct H.
+    induction H.
     apply Safe_intro.
     intros.
     inversion H.
@@ -147,11 +143,9 @@ Section Termination.
     apply Safe_intro.
     intros.
     simple inversion H1.
-    subst.
-
     apply jmeq_lemma in H2.
     destruct H2.
-    destruct H3.
+    destruct H5.
     subst.
     apply JMeq_eq in H2.
     subst.
@@ -162,25 +156,29 @@ Section Termination.
     destruct H4.
     destruct H7.
     rewrite <- H5.
+    rewrite <- H5 in H1.
     clear H5.
     generalize H2.
     clear H2.
     subst.
-    apply JMeq_eq in H7.
     apply JMeq_eq in H4.
     subst.
+
+    assert (b=b0).
+    apply (computation_is_deterministic B c b b0 H H3).
+    subst.
+    apply JMeq_eq in H7.
+    subst.
+
     intros.
     apply JMeq_eq in H2.
     rewrite H2.
-    apply H0.
-    auto.
+    apply IHTerminatesWith2.
   Defined.
 
 End Termination.
 
 Implicit Arguments Terminates [A].
-Implicit Arguments TerminatesReturn [A].
-Implicit Arguments TerminatesBind [A].
 Implicit Arguments TerminatesReturnWith [A].
 Implicit Arguments TerminatesBindWith [A].
 Implicit Arguments eval' [CC].