better comments/documentation

[coinductive-monad.git] / src / Computation / Equivalence.v

diff --git a/src/Computation/Equivalence.v b/src/Computation/Equivalence.v
new file mode 100644 (file)
index 0000000..1ea567c
--- /dev/null
+++ b/src/Computation/Equivalence.v
@@ -0,0 +1,212 @@
+Require Export Relation_Definitions.
+Require Setoid.
+Require Export Computation.Monad.
+Require Export Computation.Termination.
+Require Import Coq.Logic.JMeq.
+
+(** Computational Equivalence relation *)
+Inductive CE
+  (A:Set)(ca1:#A)(ca2:#A)
+  : Prop :=
+
+  | CE_intro :
+    (forall a,
+        TerminatesWith A ca1 a
+        <->
+        TerminatesWith A ca2 a)
+
+    -> CE A ca1 ca2.
+Implicit Arguments CE [A].
+
+(** CE is reflexive *)
+Theorem ce_refl :
+   forall (A:Set)(x:#A),
+     CE x x.
+  intros.
+  constructor.
+  intros.
+  constructor.
+  auto.
+  auto.
+Qed.
+
+(** CE is symmetric *)
+Theorem ce_symm :
+   forall (A:Set)(x y:#A),
+     (CE x y) ->
+     (CE y x).
+  intros.
+  inversion H.
+  constructor.
+  intros.
+  assert (TerminatesWith A x a <-> TerminatesWith A y a).
+  apply H0.
+  inversion H1.
+  constructor.
+  auto.
+  auto.
+Qed.
+
+(** CE is transitive *)
+Theorem ce_trans :
+   forall (A:Set)(x y z:#A),
+     (CE x y) ->
+     (CE y z) ->
+     (CE x z).
+  intros.
+  inversion H0.
+  inversion H.
+  constructor.
+  intros.
+  assert (TerminatesWith A y a <-> TerminatesWith A z a). apply H1.
+  assert (TerminatesWith A x a <-> TerminatesWith A y a). apply H2.
+  inversion H3.
+  inversion H4.
+  constructor.
+  auto.
+  auto.
+Qed.
+
+(** CE is a relation *)
+Add Relation Computation CE
+  reflexivity proved by ce_refl
+  symmetry proved by ce_symm
+  transitivity proved by ce_trans
+   as CE_rel.
+
+Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
+  ((c1>>=f1)=(c2>>=f2))
+  -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
+  intros.
+  inversion H.
+  split.
+  dependent rewrite H3.
+  simpl.
+  auto.
+  split.
+  dependent rewrite H2.
+  simpl.
+  auto.
+  auto.
+Qed.
+
+Lemma inversion_lemma :
+  forall (A B:Set)(c:#A)(f:A->#B)(b:B),
+    TerminatesWith B (Bind f c) b
+    ->
+    (exists a:A,
+     TerminatesWith A c a
+     /\
+     TerminatesWith B (f a) b).
+  intros.
+  simple inversion H.
+  subst.
+  inversion H0.
+  subst.
+  apply jmeq_lemma in H2.
+  inversion H2.
+  inversion H1.
+  subst.
+  clear H2.
+  clear H1.
+  intros.
+  apply JMeq_eq in H0.
+  subst.
+  exists b0.
+  constructor.
+  auto.
+  clear H.
+  clear H1.
+  apply JMeq_eq in H3.
+  subst.
+  auto.
+Qed.
+
+(** First Monad Law *)
+Theorem monad_law_1 :
+  forall (A B:Set)(a:A)(c:#A)(f:A->#B),
+     CE (Bind f (Return a)) (f a).
+  intros.
+  constructor.
+  intros.
+  constructor.
+  intros.
+  apply inversion_lemma in H.
+  inversion H.
+  inversion H0.
+  assert (x=a).
+  inversion H1.
+  subst.
+  auto.
+  subst.
+  auto.
+  intro.
+  apply (@TerminatesBindWith B A a).
+  constructor.
+  auto.
+Qed.
+
+(** Second Monad Law *)
+Theorem monad_law_2 :
+  forall (A:Set)(c:#A),
+     CE (Bind (fun x => Return x) c) c.
+  intros.
+  constructor.
+  intros.
+  constructor.
+  intros.
+  apply inversion_lemma in H.
+  inversion H.
+  inversion H0.
+  inversion H2.
+  subst.
+  auto.
+  intros.
+  apply (@TerminatesBindWith A A a).
+  auto.
+  constructor.
+Qed.
+
+(** Third Monad Law *)
+Theorem monad_law_3 :
+  forall (A B C:Set)(a:A)(c:#A)(f:A->#B)(g:B->#C),
+     CE (Bind g (Bind f c)) (Bind (fun x => (Bind g (f x))) c).
+  intros.
+  constructor.
+  intros.
+  constructor.
+
+  intros.
+  apply inversion_lemma in H.
+  inversion H.
+  inversion H0.
+  clear H.
+  clear H0.
+  apply inversion_lemma in H1.
+  inversion H1.
+  clear H1.
+  inversion H.
+  clear H.
+  apply (@TerminatesBindWith C A x0).
+  auto.
+  apply (@TerminatesBindWith C B x).
+  auto.
+  auto.
+
+  intros.
+  apply inversion_lemma in H.
+  inversion H.
+  inversion H0.
+  clear H.
+  clear H0.
+  apply inversion_lemma in H2.
+  inversion H2.
+  clear H2.
+  inversion H.
+  clear H.
+  apply (@TerminatesBindWith C B x0).
+  apply (@TerminatesBindWith B A x).
+  auto.
+  auto.
+  auto.
+Qed.
\ No newline at end of file