author adam Sun, 28 Oct 2007 22:16:03 +0000 (22:16 +0000) committer adam Sun, 28 Oct 2007 22:16:03 +0000 (22:16 +0000)
darcs-hash:20071028221603-5007d-09c59f3bc826b721b3708b92c9291b498b6306de.gz

index d20d57a..a64fa6b 100644 (file)
@@ -3,62 +3,27 @@ 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 :
forall (a:A),
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),

| 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)
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))
(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 :=
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.

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).
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 =>
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 =>
| Return x => fun _ => exist _ x _
| Bind CN f cn =>
fun eval_pred =>
@@ -105,7 +70,7 @@ Section Termination.
end
end
in
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))
).

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.

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.
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.
apply Safe_intro.
intros.
inversion H.
@@ -147,11 +143,9 @@ Section Termination.
apply Safe_intro.
intros.
simple inversion H1.
apply Safe_intro.
intros.
simple inversion H1.
-    subst.
-
apply jmeq_lemma in H2.
destruct H2.
apply jmeq_lemma in H2.
destruct H2.
-    destruct H3.
+    destruct H5.
subst.
apply JMeq_eq in H2.
subst.
subst.
apply JMeq_eq in H2.
subst.
@@ -162,25 +156,29 @@ Section Termination.
destruct H4.
destruct H7.
rewrite <- H5.
destruct H4.
destruct H7.
rewrite <- H5.
+    rewrite <- H5 in H1.
clear H5.
generalize H2.
clear H2.
subst.
clear H5.
generalize H2.
clear H2.
subst.
-    apply JMeq_eq in H7.
apply JMeq_eq in H4.
subst.
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.
intros.
apply JMeq_eq in H2.
rewrite H2.
-    apply H0.
-    auto.
+    apply IHTerminatesWith2.
Defined.

End Termination.

Implicit Arguments Terminates [A].
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].
Implicit Arguments TerminatesReturnWith [A].
Implicit Arguments TerminatesBindWith [A].
Implicit Arguments eval' [CC].