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