1 Require Export Relation_Definitions.
3 Require Export Computation.Monad.
4 Require Export Computation.Termination.
5 Require Import Coq.Logic.JMeq.
7 (** Computational Equivalence relation *)
9 (A:Set)(ca1:#A)(ca2:#A)
14 TerminatesWith A ca1 a
16 TerminatesWith A ca2 a)
19 Implicit Arguments CE [A].
21 (** CE is reflexive *)
33 (** CE is symmetric *)
35 forall (A:Set)(x y:#A),
42 assert (TerminatesWith A x a <-> TerminatesWith A y a).
50 (** CE is transitive *)
52 forall (A:Set)(x y z:#A),
61 assert (TerminatesWith A y a <-> TerminatesWith A z a). apply H1.
62 assert (TerminatesWith A x a <-> TerminatesWith A y a). apply H2.
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
77 Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
79 -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
93 Lemma inversion_lemma :
94 forall (A B:Set)(c:#A)(f:A->#B)(b:B),
95 TerminatesWith B (Bind f c) b
100 TerminatesWith B (f a) b).
106 apply jmeq_lemma in H2.
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).
134 apply inversion_lemma in H.
144 apply (@TerminatesBindWith B A a).
149 (** Second Monad Law *)
150 Theorem monad_law_2 :
151 forall (A:Set)(c:#A),
152 CE (Bind (fun x => Return x) c) c.
158 apply inversion_lemma in H.
165 apply (@TerminatesBindWith A A a).
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).
180 apply inversion_lemma in H.
185 apply inversion_lemma in H1.
190 apply (@TerminatesBindWith C A x0).
192 apply (@TerminatesBindWith C B x).
197 apply inversion_lemma in H.
202 apply inversion_lemma in H2.
207 apply (@TerminatesBindWith C B x0).
208 apply (@TerminatesBindWith B A x).