1 Require Export Relation_Definitions.
3 Require Export Computation.Monad.
4 Require Export Computation.Termination.
5 Require Import Coq.Logic.JMeq.
8 (A:Set)(ca1:#A)(ca2:#A)
13 TerminatesWith A ca1 a
15 TerminatesWith A ca2 a)
18 Implicit Arguments CE [A].
32 forall (A:Set)(x y:#A),
39 assert (TerminatesWith A x a <-> TerminatesWith A y a).
48 forall (A:Set)(x y z:#A),
57 assert (TerminatesWith A y a <-> TerminatesWith A z a). apply H1.
58 assert (TerminatesWith A x a <-> TerminatesWith A y a). apply H2.
66 Add Relation Computation CE
67 reflexivity proved by ce_refl
68 symmetry proved by ce_symm
69 transitivity proved by ce_trans
72 Theorem jmeq_lemma : forall (A1 A2 B:Set)(c1:#A1)(c2:#A2)(f1:A1->#B)(f2:A2->#B),
74 -> (JMeq c1 c2) /\ (JMeq f1 f2) /\ (A1=A2).
88 Lemma inversion_lemma :
89 forall (A B:Set)(c:#A)(f:A->#B)(b:B),
90 TerminatesWith B (Bind f c) b
95 TerminatesWith B (f a) b).
101 apply jmeq_lemma in H2.
120 Theorem monad_law_1 :
121 forall (A B:Set)(a:A)(c:#A)(f:A->#B),
122 CE (Bind f (Return a)) (f a).
128 apply inversion_lemma in H.
138 apply (@TerminatesBindWith B A a).
143 Theorem monad_law_2 :
144 forall (A:Set)(c:#A),
145 CE (Bind (fun x => Return x) c) c.
151 apply inversion_lemma in H.
158 apply (@TerminatesBindWith A A a).
163 Theorem monad_law_3 :
164 forall (A B C:Set)(a:A)(c:#A)(f:A->#B)(g:B->#C),
165 CE (Bind g (Bind f c)) (Bind (fun x => (Bind g (f x))) c).
172 apply inversion_lemma in H.
177 apply inversion_lemma in H1.
182 apply (@TerminatesBindWith C A x0).
184 apply (@TerminatesBindWith C B x).
189 apply inversion_lemma in H.
194 apply inversion_lemma in H2.
199 apply (@TerminatesBindWith C B x0).
200 apply (@TerminatesBindWith B A x).