Require Export Computation.Termination.
Require Import Coq.Logic.JMeq.
+(** Computational Equivalence relation *)
Inductive CE
(A:Set)(ca1:#A)(ca2:#A)
: Prop :=
-> CE A ca1 ca2.
Implicit Arguments CE [A].
+(** CE is reflexive *)
Theorem ce_refl :
forall (A:Set)(x:#A),
CE x x.
auto.
Qed.
+(** CE is symmetric *)
Theorem ce_symm :
forall (A:Set)(x y:#A),
(CE x y) ->
auto.
Qed.
+(** CE is transitive *)
Theorem ce_trans :
forall (A:Set)(x y z:#A),
(CE x y) ->
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.
+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),
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).
auto.
Qed.
+(** Second Monad Law *)
Theorem monad_law_2 :
forall (A:Set)(c:#A),
CE (Bind (fun x => Return x) c) c.
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).