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