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 :
where "c ! y" := (TerminatesWith _ c y)
.
- (* an inductive predicate proving that a given computation terminates with /some/ value *)
+ (** 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).
+ (** A predicate indicating which computations might be subcomputations of a given computation *)
Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
| invokesPrev : forall
(z:#C)
(_:c!b),
InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
+ (** A predicate asserting that it is safe to evaluate a computation (this is the single-constructor Prop type) *)
Inductive Safe : forall (A:Set) (c:#A), Prop :=
Safe_intro :
forall (A:Set) (c:#A),
(forall (B C:Set) (c':#B)(z:#C), InvokedBy A B C c c' z -> Safe B c')
-> Safe A c.
+ (** Inversion principle for Safe *)
Definition Safe_inv
: forall (A B C:Set)(c:#A)(_:Safe A c)(c':#B)(z:#C)(_:InvokedBy A B C c c' z), Safe B c'.
destruct 1.
assumption.
Defined.
+ (** A lemma to help apply JMeq *)
Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
((c1>>=f1)=(c2>>=f2))
-> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
auto.
Qed.
-
+ (** If we can prove that a given computation terminates with two different values, they must be the same *)
Lemma computation_is_deterministic :
forall (A:Set) (c:#A) (x y:A), c!x -> c!y -> x=y.
intros.
auto.
Qed.
+ (** Any terminating computation is Safe *)
Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
intros.
destruct H.