From f32b158060d2be2811e5ba058756c7dc3fb71672 Mon Sep 17 00:00:00 2001
From: adam <adam@megacz.com>
Date: Tue, 2 Oct 2007 15:38:45 +0000
Subject: [PATCH] add Computation/Equivalence.v

darcs-hash:20071002153845-5007d-0ad5426ab748435060fa542572e06b2147b3d938.gz
---
 Computation/Equivalence.v |  204 +++++++++++++++++++++++++++++++++++++++++++++
 Makefile                  |    3 +-
 2 files changed, 206 insertions(+), 1 deletion(-)
 create mode 100644 Computation/Equivalence.v

diff --git a/Computation/Equivalence.v b/Computation/Equivalence.v
new file mode 100644
index 0000000..ad8b9ad
--- /dev/null
+++ b/Computation/Equivalence.v
@@ -0,0 +1,204 @@
+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
diff --git a/Makefile b/Makefile
index bef71fe..8d5d281 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,8 @@
 
-all: Computation/Eval.vo Computation/Tactics.vo Computation/Termination.vo Computation/Monad.vo
+all: Computation/Eval.vo Computation/Tactics.vo Computation/Termination.vo Computation/Monad.vo Computation/Equivalence.vo
 clean:; rm */*.vo
 
+Computation/Equivalence.vo: Computation/Monad.vo Computation/Termination.vo
 Computation/Termination.vo: Computation/Monad.vo
 Computation/Tactics.vo: Computation/Monad.vo
 Computation/Eval.vo: Computation/Termination.vo
-- 
1.7.10.4