src/Computation/Termination.v

   1 Require Import Computation.Monad.
   2 Require Import Coq.Logic.JMeq.
   3
   4 Section Termination.
   5
   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 :
  10     forall (a:A),
  11       (Return a)!a
  12
  13   | TerminatesBindWith :
  14     forall (B:Set) (b:B) (a:A) (f:B->#A) (c:#B),
  15       c!b
  16       -> (f b)!a
  17       -> (c >>= f)!a
  18      where "c ! y" := (TerminatesWith _ c y)
  19       .
  20
  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).
  26
  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
  30     (z:#C)
  31     (c:#B)
  32     (f:B->#A),
  33     InvokedBy A B C (@Bind A B f c) c z
  34   | invokesFunc : forall
  35     (c:#C)
  36     (b:C)
  37     (f:C->#A)
  38     (pf:#A->#B)
  39     (eqpf:A=B)
  40     (_:JMeq (pf (f b)) (f b))
  41     (_:c!b),
  42     InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
  43
  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 :=
  46     Safe_intro :
  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')
  49       -> Safe A c.
  50
  51   (** Inversion principle for Safe *)
  52   Definition Safe_inv
  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'.
  54     destruct 1.
  55     apply (H B).
  56   Defined.
  57
  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}!.
  61     refine(
  62       !Let eval_one_step :=
  63         fun C c Z z =>
  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 _
  66             | Bind CN f cn =>
  67               fun eval_pred =>
  68                 match eval_pred CN cn Z z (invokesPrev C CN Z z cn f) with
  69                   | exist b pf =>
  70                     match eval_pred C (f b) CN cn _ with
  71                       | exist a' pf' => exist _ a' _
  72                     end
  73                 end
  74           end
  75           in
  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))
  78     ).
  79
  80     constructor.
  81
  82     refine (invokesFunc C C CN cn b f (fun x:#C=>x) _ _ _).
  83     auto.
  84     auto.
  85     assumption.
  86
  87     apply (TerminatesBindWith C CN b a' f cn).
  88     assumption.
  89     assumption.
  90   Defined.
  91
  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),
  94     ((c1>>=f1)=(c2>>=f2))
  95     -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
  96     intros.
  97     inversion H.
  98     split.
  99     dependent rewrite H3.
 100     simpl.
 101     auto.
 102     split.
 103     dependent rewrite H2.
 104     simpl.
 105     auto.
 106     auto.
 107   Qed.
 108
 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.
 112     intros.
 113     generalize H0.
 114     clear H0.
 115     induction H.
 116     intros.
 117     inversion H0.
 118     auto.
 119
 120     intros.
 121     simple inversion H1.
 122     inversion H2.
 123
 124     apply jmeq_lemma in H4.
 125     destruct H4.
 126     destruct H3.
 127     subst.
 128     apply JMeq_eq in H2.
 129     apply JMeq_eq in H3.
 130     subst.
 131     intros.
 132     apply IHTerminatesWith2.
 133     apply IHTerminatesWith1 in H2.
 134     subst.
 135     auto.
 136   Qed.
 137
 138   (** Any terminating computation is Safe *)
 139   Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
 140     intros.
 141     destruct H.
 142     destruct H.
 143     induction H.
 144     apply Safe_intro.
 145     intros.
 146     inversion H.
 147
 148     apply Safe_intro.
 149     intros.
 150     simple inversion H1.
 151     apply jmeq_lemma in H2.
 152     destruct H2.
 153     destruct H5.
 154     subst.
 155     apply JMeq_eq in H2.
 156     subst.
 157     auto.
 158
 159     intros.
 160     apply jmeq_lemma in H4.
 161     destruct H4.
 162     destruct H7.
 163     rewrite <- H5.
 164     rewrite <- H5 in H1.
 165     clear H5.
 166     generalize H2.
 167     clear H2.
 168     subst.
 169     apply JMeq_eq in H4.
 170     subst.
 171
 172     assert (b=b0).
 173     apply (computation_is_deterministic B c b b0 H H3).
 174     subst.
 175     apply JMeq_eq in H7.
 176     subst.
 177
 178     intros.
 179     apply JMeq_eq in H2.
 180     rewrite H2.
 181     apply IHTerminatesWith2.
 182   Defined.
 183
 184 End Termination.
 185
 186 Implicit Arguments Terminates [A].
 187 Implicit Arguments TerminatesReturnWith [A].
 188 Implicit Arguments TerminatesBindWith [A].
 189 Implicit Arguments eval' [CC].
 190