From 68eb561f71dd052a346319cd1b92dd077cb1c8bb Mon Sep 17 00:00:00 2001 From: adam Date: Sun, 28 Oct 2007 22:16:03 +0000 Subject: [PATCH] change Terminates to (exists x, TerminatesWith x) and improve notation darcs-hash:20071028221603-5007d-09c59f3bc826b721b3708b92c9291b498b6306de.gz --- Computation/Termination.v | 122 ++++++++++++++++++++++----------------------- 1 file changed, 60 insertions(+), 62 deletions(-) diff --git a/Computation/Termination.v b/Computation/Termination.v index d20d57a..a64fa6b 100644 --- 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]. -- 1.7.10.4