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 Inductive TerminatesWith (A:Set) : #A -> A -> Prop :=
8 | TerminatesReturnWith :
10 TerminatesWith A (Return a) a
12 | TerminatesBindWith :
13 forall (B:Set) (b:B) (a:A) (f:B->#A) (c:#B),
14 (TerminatesWith B c b)
15 -> TerminatesWith A (f b) a
16 -> TerminatesWith A (@Bind A B f c) a
19 (* an inductive predicate proving that a given computation terminates with /some/ value *)
20 Inductive Terminates (A:Set) : #A -> Prop :=
23 Terminates A (Return a)
26 forall (B:Set) (f:B->#A) (c:#B),
28 -> (forall (b:B), (TerminatesWith B c b) -> Terminates A (f b))
29 -> Terminates A (@Bind A B f c)
32 Lemma terminating_computations_must_produce_a_value
33 : forall (A:Set) (c:#A), Terminates A c -> ex (fun a:A => TerminatesWith A c a).
43 assert (exists a : A, TerminatesWith A (f x) a).
51 apply (TerminatesBindWith A B x x0 f c).
56 Theorem coerce : forall (A B:Set)(pf:A=B)(a:#A), #B.
62 Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
63 | invokesPrev : forall
67 InvokedBy A B C (@Bind A B f c) c z
68 | invokesFunc : forall
74 (_:JMeq (pf (f b)) (f b))
75 (_:TerminatesWith C c b),
76 InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
78 Inductive Safe : forall (A:Set) (c:#A), Prop :=
80 forall (A:Set) (c:#A),
81 (forall (B C:Set) (c':#B)(z:#C), InvokedBy A B C c c' z -> Safe B c')
85 : forall (A B C:Set)(c:#A)(_:Safe A c)(c':#B)(z:#C)(_:InvokedBy A B C c c' z), Safe B c'.
90 Notation "! c :: A" := {a:A|TerminatesWith A c a} (at level 5).
91 Notation "'!Let' x := y 'in' z" := ((fun x => z)y)(at level 100).
92 Definition eval' CC cc (Z:Set) (z:#Z) (s:Safe CC cc) : (!cc::CC).
96 match c return (forall PRED pred Z z, InvokedBy C PRED Z c pred z -> !pred::PRED) -> !c::C with
97 | Return x => fun _ => exist _ x _
100 match eval_pred CN cn Z z (invokesPrev C CN Z z cn f) with
102 match eval_pred C (f b) CN cn _ with
103 | exist a' pf' => exist _ a' _
108 fix eval_all C c Z z (s:Safe C c) {struct s} : !c::C :=
109 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))
114 refine (invokesFunc C C CN cn b f (fun x:#C=>x) _ _ _).
119 apply (TerminatesBindWith C CN b a' f cn).
124 Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
125 ((c1>>=f1)=(c2>>=f2))
126 -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
130 dependent rewrite H3.
134 dependent rewrite H2.
140 Theorem termination_is_safe : forall (A:Set) (c:#A) (t:Terminates A c), Safe A c.
152 apply jmeq_lemma in H2.
161 apply jmeq_lemma in H4.
181 Implicit Arguments Terminates [A].
182 Implicit Arguments TerminatesReturn [A].
183 Implicit Arguments TerminatesBind [A].
184 Implicit Arguments TerminatesReturnWith [A].
185 Implicit Arguments TerminatesBindWith [A].
186 Implicit Arguments eval' [CC].