1 Require Import Computation.Monad.
2 Require Import Coq.Logic.JMeq.
6 (** An inductive predicate proving that a given computation terminates with a particular value *)
7 Reserved Notation "c ! y" (at level 30).
8 Inductive TerminatesWith (A:Set) : #A -> A -> Prop :=
9 | TerminatesReturnWith :
13 | TerminatesBindWith :
14 forall (B:Set) (b:B) (a:A) (f:B->#A) (c:#B),
18 where "c ! y" := (TerminatesWith _ c y)
21 (** An inductive predicate proving that a given computation terminates with /some/ value *)
22 Reserved Notation "c !?" (at level 30).
23 Inductive Terminates (A:Set)(c:#A) : Prop :=
24 | Terminates_intro : (exists a:A, c!a) -> c!?
25 where "c !?" := (Terminates _ c).
27 (** A predicate indicating which computations might be subcomputations of a given computation *)
28 Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
29 | invokesPrev : forall
33 InvokedBy A B C (@Bind A B f c) c z
34 | invokesFunc : forall
40 (_:JMeq (pf (f b)) (f b))
42 InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
44 (** A predicate asserting that it is safe to evaluate a computation (this is the single-constructor Prop type) *)
45 Inductive Safe : forall (A:Set) (c:#A), Prop :=
47 forall (A:Set) (c:#A),
48 (forall (B C:Set) (c':#B)(z:#C), InvokedBy A B C c c' z -> Safe B c')
51 (** Inversion principle for Safe *)
53 : forall (A B C:Set)(c:#A)(_:Safe A c)(c':#B)(z:#C)(_:InvokedBy A B C c c' z), Safe B c'.
58 Notation "{ c }!" := {a:_|TerminatesWith _ c a} (at level 5).
59 Notation "'!Let' x := y 'in' z" := ((fun x => z)y)(at level 100).
60 Definition eval' CC cc (Z:Set) (z:#Z) (s:Safe CC cc) : {cc}!.
64 match c return (forall PRED pred Z z, InvokedBy C PRED Z c pred z -> {pred}!) -> {c}! with
65 | Return x => fun _ => exist _ x _
68 match eval_pred CN cn Z z (invokesPrev C CN Z z cn f) with
70 match eval_pred C (f b) CN cn _ with
71 | exist a' pf' => exist _ a' _
76 fix eval_all C c Z z (s:Safe C c) {struct s} : {c}! :=
77 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))
82 refine (invokesFunc C C CN cn b f (fun x:#C=>x) _ _ _).
87 apply (TerminatesBindWith C CN b a' f cn).
92 (** A lemma to help apply JMeq *)
93 Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
95 -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
103 dependent rewrite H2.
109 (** If we can prove that a given computation terminates with two different values, they must be the same *)
110 Lemma computation_is_deterministic :
111 forall (A:Set) (c:#A) (x y:A), c!x -> c!y -> x=y.
124 apply jmeq_lemma in H4.
132 apply IHTerminatesWith2.
133 apply IHTerminatesWith1 in H2.
138 (** Any terminating computation is Safe *)
139 Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
151 apply jmeq_lemma in H2.
160 apply jmeq_lemma in H4.
173 apply (computation_is_deterministic B c b b0 H H3).
181 apply IHTerminatesWith2.
186 Implicit Arguments Terminates [A].
187 Implicit Arguments TerminatesReturnWith [A].
188 Implicit Arguments TerminatesBindWith [A].
189 Implicit Arguments eval' [CC].