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   Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
  28   | invokesPrev : forall
  29     (z:#C)
  30     (c:#B)
  31     (f:B->#A),
  32     InvokedBy A B C (@Bind A B f c) c z
  33   | invokesFunc : forall
  34     (c:#C)
  35     (b:C)
  36     (f:C->#A)
  37     (pf:#A->#B)
  38     (eqpf:A=B)
  39     (_:JMeq (pf (f b)) (f b))
  40     (_:c!b),
  41     InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
  42
  43   Inductive Safe : forall (A:Set) (c:#A), Prop :=
  44     Safe_intro :
  45     forall (A:Set) (c:#A),
  46       (forall (B C:Set) (c':#B)(z:#C), InvokedBy A B C c c' z -> Safe B c')
  47       -> Safe A c.
  48
  49   Definition Safe_inv
  50     : forall (A B C:Set)(c:#A)(_:Safe A c)(c':#B)(z:#C)(_:InvokedBy A B C c c' z), Safe B c'.
  51     destruct 1.
  52     apply (H B).
  53   Defined.
  54
  55   Notation "{ c }!" := {a:_|TerminatesWith _ c a} (at level 5).
  56   Notation "'!Let' x := y 'in' z" := ((fun x => z)y)(at level 100).
  57   Definition eval' CC cc (Z:Set) (z:#Z) (s:Safe CC cc) : {cc}!.
  58     refine(
  59       !Let eval_one_step :=
  60         fun C c Z z =>
  61           match c return (forall PRED pred Z z, InvokedBy C PRED Z c pred z -> {pred}!) -> {c}! with
  62             | Return x => fun _ => exist _ x _
  63             | Bind CN f cn =>
  64               fun eval_pred =>
  65                 match eval_pred CN cn Z z (invokesPrev C CN Z z cn f) with
  66                   | exist b pf =>
  67                     match eval_pred C (f b) CN cn _ with
  68                       | exist a' pf' => exist _ a' _
  69                     end
  70                 end
  71           end
  72           in
  73           fix eval_all C c Z z (s:Safe C c) {struct s} : {c}! :=
  74           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))
  75     ).
  76
  77     constructor.
  78
  79     refine (invokesFunc C C CN cn b f (fun x:#C=>x) _ _ _).
  80     auto.
  81     auto.
  82     assumption.
  83
  84     apply (TerminatesBindWith C CN b a' f cn).
  85     assumption.
  86     assumption.
  87   Defined.
  88
  89   Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
  90     ((c1>>=f1)=(c2>>=f2))
  91     -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
  92     intros.
  93     inversion H.
  94     split.
  95     dependent rewrite H3.
  96     simpl.
  97     auto.
  98     split.
  99     dependent rewrite H2.
 100     simpl.
 101     auto.
 102     auto.
 103   Qed.
 104
 105
 106   Lemma computation_is_deterministic :
 107     forall (A:Set) (c:#A) (x y:A), c!x -> c!y -> x=y.
 108     intros.
 109     generalize H0.
 110     clear H0.
 111     induction H.
 112     intros.
 113     inversion H0.
 114     auto.
 115
 116     intros.
 117     simple inversion H1.
 118     inversion H2.
 119
 120     apply jmeq_lemma in H4.
 121     destruct H4.
 122     destruct H3.
 123     subst.
 124     apply JMeq_eq in H2.
 125     apply JMeq_eq in H3.
 126     subst.
 127     intros.
 128     apply IHTerminatesWith2.
 129     apply IHTerminatesWith1 in H2.
 130     subst.
 131     auto.
 132   Qed.
 133
 134   Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
 135     intros.
 136     destruct H.
 137     destruct H.
 138     induction H.
 139     apply Safe_intro.
 140     intros.
 141     inversion H.
 142
 143     apply Safe_intro.
 144     intros.
 145     simple inversion H1.
 146     apply jmeq_lemma in H2.
 147     destruct H2.
 148     destruct H5.
 149     subst.
 150     apply JMeq_eq in H2.
 151     subst.
 152     auto.
 153
 154     intros.
 155     apply jmeq_lemma in H4.
 156     destruct H4.
 157     destruct H7.
 158     rewrite <- H5.
 159     rewrite <- H5 in H1.
 160     clear H5.
 161     generalize H2.
 162     clear H2.
 163     subst.
 164     apply JMeq_eq in H4.
 165     subst.
 166
 167     assert (b=b0).
 168     apply (computation_is_deterministic B c b b0 H H3).
 169     subst.
 170     apply JMeq_eq in H7.
 171     subst.
 172
 173     intros.
 174     apply JMeq_eq in H2.
 175     rewrite H2.
 176     apply IHTerminatesWith2.
 177   Defined.
 178
 179 End Termination.
 180
 181 Implicit Arguments Terminates [A].
 182 Implicit Arguments TerminatesReturnWith [A].
 183 Implicit Arguments TerminatesBindWith [A].
 184 Implicit Arguments eval' [CC].
 185