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).
Require Export Computation.Monad.
Require Export Computation.Termination.
-(* evaluate up to [n] computation steps *)
+(** evaluate up to [n] computation steps *)
Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
match n with
| O => None
end
end.
-Inductive Unit : Set := unit : Unit.
-
-(*
- * In theory we'd like to be able to do this (below), but it violates
- * the Prop/Set separation:
- *
- * "Elimination of an inductive object of sort Prop is not allowed on a
- * predicate in sort Set because proofs can be eliminated only to
- * build proofs."
+(** In theory we'd like to be able to do this (below), but it violates the Prop/Set separation.
*)
-(*
+(**
+<<
Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
match t with
| (Terminates_intro t') =>
| (ex_intro x y) => x
end
end.
-*)
+
+ "Elimination of an inductive object of sort Prop is not allowed on a
+ predicate in sort Set because proofs can be eliminated only to
+ build proofs."
+>>*)
+Inductive Unit : Set := unit : Unit.
Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
match eval' c Unit (Return unit) (termination_is_safe A c t) with
| exist x pf => x
Implicit Arguments eval [A].
Implicit Arguments bounded_eval [A].
+
Reserved Notation "# A" (at level 30).
Section Constructors.
- (* a co-inductive type representing a possibly-nonterminating computation *)
- CoInductive Computation (A:Set) : Type :=
+ (** A co-inductive type representing a possibly-nonterminating computation *)
+ CoInductive Computation (A:Set) : Type :=
- (* terminate and return a value *)
+ (** terminate and return a value *)
| Return : A -> #A
- (* monadic >>= (bind) operator *)
+ (** monadic >>= (bind) operator *)
| Bind : forall (B:Set), (B->#A) -> #B -> #A
where "# A" := (Computation A).
Implicit Arguments Return [A].
Require Import Computation.Monad.
-(* decomposition lemma *)
+(** A decomposition lemma *)
Definition decomp (A:Set)(c:#A) : #A :=
match c with
| Return x => Return x
end.
Implicit Arguments decomp.
-(* decomposition theorem: we can always decompose *)
+(** A decomposition theorem: we can always decompose *)
Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c.
intros A l; case l; simpl; trivial.
Qed.
-(* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
+(** 1-, 2-, 3-, 4-, and 5-ary decompositions; you should use this *)
Ltac uncomp comp :=
match goal with
| [ |- context[(comp ?X)] ] =>
Section Termination.
- (* an inductive predicate proving that a given computation terminates with a particular value *)
+ (** An inductive predicate proving that a given computation terminates with a particular value *)
Reserved Notation "c ! y" (at level 30).
Inductive TerminatesWith (A:Set) : #A -> A -> Prop :=
| TerminatesReturnWith :
where "c ! y" := (TerminatesWith _ c y)
.
- (* an inductive predicate proving that a given computation terminates with /some/ value *)
+ (** An inductive predicate proving that a given computation terminates with /some/ value *)
Reserved Notation "c !?" (at level 30).
Inductive Terminates (A:Set)(c:#A) : Prop :=
| Terminates_intro : (exists a:A, c!a) -> c!?
where "c !?" := (Terminates _ c).
+ (** A predicate indicating which computations might be subcomputations of a given computation *)
Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop :=
| invokesPrev : forall
(z:#C)
(_:c!b),
InvokedBy A B C (@Bind A C f c) (pf (f b)) c.
+ (** A predicate asserting that it is safe to evaluate a computation (this is the single-constructor Prop type) *)
Inductive Safe : forall (A:Set) (c:#A), Prop :=
Safe_intro :
forall (A:Set) (c:#A),
(forall (B C:Set) (c':#B)(z:#C), InvokedBy A B C c c' z -> Safe B c')
-> Safe A c.
+ (** Inversion principle for Safe *)
Definition Safe_inv
: forall (A B C:Set)(c:#A)(_:Safe A c)(c':#B)(z:#C)(_:InvokedBy A B C c c' z), Safe B c'.
destruct 1.
assumption.
Defined.
+ (** A lemma to help apply JMeq *)
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).
auto.
Qed.
-
+ (** If we can prove that a given computation terminates with two different values, they must be the same *)
Lemma computation_is_deterministic :
forall (A:Set) (c:#A) (x y:A), c!x -> c!y -> x=y.
intros.
auto.
Qed.
+ (** Any terminating computation is Safe *)
Theorem termination_is_safe : forall (A:Set) (c:#A), c!? -> Safe A c.
intros.
destruct H.
projects / coinductive-monad.git / commitdiff