Computation/Equivalence.v

   1 Require Export Relation_Definitions.
   2 Require Setoid.
   3 Require Export Computation.Monad.
   4 Require Export Computation.Termination.
   5 Require Import Coq.Logic.JMeq.
   6
   7 Inductive CE
   8   (A:Set)(ca1:#A)(ca2:#A)
   9   : Prop :=
  10
  11   | CE_intro :
  12     (forall a,
  13         TerminatesWith A ca1 a
  14         <->
  15         TerminatesWith A ca2 a)
  16
  17     -> CE A ca1 ca2.
  18 Implicit Arguments CE [A].
  19
  20 Theorem ce_refl :
  21    forall (A:Set)(x:#A),
  22      CE x x.
  23   intros.
  24   constructor.
  25   intros.
  26   constructor.
  27   auto.
  28   auto.
  29 Qed.
  30
  31 Theorem ce_symm :
  32    forall (A:Set)(x y:#A),
  33      (CE x y) ->
  34      (CE y x).
  35   intros.
  36   inversion H.
  37   constructor.
  38   intros.
  39   assert (TerminatesWith A x a <-> TerminatesWith A y a).
  40   apply H0.
  41   inversion H1.
  42   constructor.
  43   auto.
  44   auto.
  45 Qed.
  46
  47 Theorem ce_trans :
  48    forall (A:Set)(x y z:#A),
  49      (CE x y) ->
  50      (CE y z) ->
  51      (CE x z).
  52   intros.
  53   inversion H0.
  54   inversion H.
  55   constructor.
  56   intros.
  57   assert (TerminatesWith A y a <-> TerminatesWith A z a). apply H1.
  58   assert (TerminatesWith A x a <-> TerminatesWith A y a). apply H2.
  59   inversion H3.
  60   inversion H4.
  61   constructor.
  62   auto.
  63   auto.
  64 Qed.
  65
  66 Add Relation Computation CE
  67   reflexivity proved by ce_refl
  68   symmetry proved by ce_symm
  69   transitivity proved by ce_trans
  70    as CE_rel.
  71
  72   Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
  73     ((c1>>=f1)=(c2>>=f2))
  74     -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
  75     intros.
  76     inversion H.
  77     split.
  78     dependent rewrite H3.
  79     simpl.
  80     auto.
  81     split.
  82     dependent rewrite H2.
  83     simpl.
  84     auto.
  85     auto.
  86   Qed.
  87
  88 Lemma inversion_lemma :
  89   forall (A B:Set)(c:#A)(f:A->#B)(b:B),
  90     TerminatesWith B (Bind f c) b
  91     ->
  92     (exists a:A,
  93      TerminatesWith A c a
  94      /\
  95      TerminatesWith B (f a) b).
  96   intros.
  97   simple inversion H.
  98   subst.
  99   inversion H0.
 100   subst.
 101   apply jmeq_lemma in H2.
 102   inversion H2.
 103   inversion H1.
 104   subst.
 105   clear H2.
 106   clear H1.
 107   intros.
 108   apply JMeq_eq in H0.
 109   subst.
 110   exists b0.
 111   constructor.
 112   auto.
 113   clear H.
 114   clear H1.
 115   apply JMeq_eq in H3.
 116   subst.
 117   auto.
 118 Qed.
 119
 120 Theorem monad_law_1 :
 121   forall (A B:Set)(a:A)(c:#A)(f:A->#B),
 122      CE (Bind f (Return a)) (f a).
 123   intros.
 124   constructor.
 125   intros.
 126   constructor.
 127   intros.
 128   apply inversion_lemma in H.
 129   inversion H.
 130   inversion H0.
 131   assert (x=a).
 132   inversion H1.
 133   subst.
 134   auto.
 135   subst.
 136   auto.
 137   intro.
 138   apply (@TerminatesBindWith B A a).
 139   constructor.
 140   auto.
 141 Qed.
 142
 143 Theorem monad_law_2 :
 144   forall (A:Set)(c:#A),
 145      CE (Bind (fun x => Return x) c) c.
 146   intros.
 147   constructor.
 148   intros.
 149   constructor.
 150   intros.
 151   apply inversion_lemma in H.
 152   inversion H.
 153   inversion H0.
 154   inversion H2.
 155   subst.
 156   auto.
 157   intros.
 158   apply (@TerminatesBindWith A A a).
 159   auto.
 160   constructor.
 161 Qed.
 162
 163 Theorem monad_law_3 :
 164   forall (A B C:Set)(a:A)(c:#A)(f:A->#B)(g:B->#C),
 165      CE (Bind g (Bind f c)) (Bind (fun x => (Bind g (f x))) c).
 166   intros.
 167   constructor.
 168   intros.
 169   constructor.
 170
 171   intros.
 172   apply inversion_lemma in H.
 173   inversion H.
 174   inversion H0.
 175   clear H.
 176   clear H0.
 177   apply inversion_lemma in H1.
 178   inversion H1.
 179   clear H1.
 180   inversion H.
 181   clear H.
 182   apply (@TerminatesBindWith C A x0).
 183   auto.
 184   apply (@TerminatesBindWith C B x).
 185   auto.
 186   auto.
 187
 188   intros.
 189   apply inversion_lemma in H.
 190   inversion H.
 191   inversion H0.
 192   clear H.
 193   clear H0.
 194   apply inversion_lemma in H2.
 195   inversion H2.
 196   clear H2.
 197   inversion H.
 198   clear H.
 199   apply (@TerminatesBindWith C B x0).
 200   apply (@TerminatesBindWith B A x).
 201   auto.
 202   auto.
 203   auto.
 204 Qed.