+++ /dev/null
-Require Import Recursion.Monad.
-Require Import Coq.Logic.JMeq.
-
-Section Termination.
-
- (* an inductive predicate proving that a given computation terminates with a particular value *)
- Inductive TerminatesWith (A:Set) : #A -> A -> Prop :=
- | TerminatesReturnWith :
- forall (a:A),
- TerminatesWith 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
- .
-
- (* 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)
- .
-
- 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)
- (c:#B)
- (f:B->#A),
- InvokedBy A B C (@Bind A B f c) c z
- | invokesFunc : forall
- (c:#C)
- (b:C)
- (f:C->#A)
- (pf:#A->#B)
- (eqpf:A=B)
- (_:JMeq (pf (f b)) (f b))
- (_:TerminatesWith C c b),
- InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
-
- 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.
-
- 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.
- apply (H B).
- Defined.
-
- Notation "! c :: A" := {a:A|TerminatesWith A 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).
- 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
- | Return x => fun _ => exist _ x _
- | Bind CN f cn =>
- fun eval_pred =>
- match eval_pred CN cn Z z (invokesPrev C CN Z z cn f) with
- | exist b pf =>
- match eval_pred C (f b) CN cn _ with
- | exist a' pf' => exist _ a' _
- end
- end
- end
- in
- fix eval_all C c Z z (s:Safe C c) {struct s} : !c::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))
- ).
-
- constructor.
-
- refine (invokesFunc C C CN cn b f (fun x:#C=>x) _ _ _).
- auto.
- auto.
- assumption.
-
- apply (TerminatesBindWith C CN b a' f cn).
- assumption.
- assumption.
- Defined.
-
- 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).
- intros.
- inversion H.
- split.
- dependent rewrite H3.
- simpl.
- auto.
- split.
- dependent rewrite H2.
- simpl.
- auto.
- auto.
- Qed.
-
- Theorem termination_is_safe : forall (A:Set) (c:#A) (t:Terminates A c), Safe A c.
- intros.
- induction t.
- apply Safe_intro.
- intros.
- inversion H.
-
- apply Safe_intro.
- intros.
- simple inversion H1.
- subst.
-
- apply jmeq_lemma in H2.
- destruct H2.
- destruct H3.
- subst.
- apply JMeq_eq in H2.
- subst.
- auto.
-
- intros.
- apply jmeq_lemma in H4.
- destruct H4.
- destruct H7.
- rewrite <- H5.
- clear H5.
- generalize H2.
- clear H2.
- subst.
- apply JMeq_eq in H7.
- apply JMeq_eq in H4.
- subst.
- intros.
- apply JMeq_eq in H2.
- rewrite H2.
- apply H0.
- auto.
- 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].
-