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