better comments/documentation

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

diff --git a/Computation/Equivalence.v b/Computation/Equivalence.v
deleted file mode 100644 (file)
index ad8b9ad..0000000
--- a/Computation/Equivalence.v
+++ /dev/null
@@ -1,204 +0,0 @@
-Require Export Relation_Definitions.
-Require Setoid.
-Require Export Computation.Monad.
-Require Export Computation.Termination.
-Require Import Coq.Logic.JMeq.
-
-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].
-
-Theorem ce_refl :
-   forall (A:Set)(x:#A),
-     CE x x.
-  intros.
-  constructor.
-  intros.
-  constructor.
-  auto.
-  auto.
-Qed.
-
-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.
-
-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.
-
-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.
-
-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.
-
-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.
-
-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