From: adam Date: Mon, 25 Jun 2007 05:12:33 +0000 (+0000) Subject: checkpoint X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=commitdiff_plain;h=77cbfc0e93ec5db4f7dc39c01b8327fec7dd53c4 checkpoint darcs-hash:20070625051233-5007d-64b9240079af604f99477226dd95679707239b35.gz --- 77cbfc0e93ec5db4f7dc39c01b8327fec7dd53c4 diff --git a/Recursion/Eval.v b/Recursion/Eval.v new file mode 100644 index 0000000..6c9b016 --- /dev/null +++ b/Recursion/Eval.v @@ -0,0 +1,26 @@ +Require Export Recursion.Monad. +Require Export Recursion.Termination. + +(* evaluate up to [n] computation steps *) +Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A := + match n with + | O => None + | (S n') => + match c with + | Return b => Some b + | Bind _ f c' => + match (bounded_eval _ n' c') with + | None => None + | Some a => bounded_eval A n' (f a) + end + end + end. + +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 + end. + +Implicit Arguments eval [A]. +Implicit Arguments bounded_eval [A]. diff --git a/Recursion/Monad.v b/Recursion/Monad.v new file mode 100644 index 0000000..082a3dd --- /dev/null +++ b/Recursion/Monad.v @@ -0,0 +1,32 @@ +Reserved Notation "# A" (at level 30). +Section Constructors. + + (* a co-inductive type representing a possibly-nonterminating computation *) + CoInductive Computation (A:Set) : Type := + + (* terminate and return a value *) + | Return : A -> #A + + (* monadic >>= (bind) operator *) + | Bind : forall (B:Set), (B->#A) -> #B -> #A + where "# A" := (Computation A). + Implicit Arguments Return [A]. + Implicit Arguments Bind [A B]. + Notation "c >>= f" := (Bind f c) (at level 20). + +End Constructors. + +Notation "# A" := (Computation A). +Implicit Arguments Return [A]. +Implicit Arguments Bind [A B]. +Notation "c >>= f" := (Bind f c) (at level 20). + +Notation "'call' c" := + (c >>= (fun x=>(Return x))) + (at level 60, right associativity) +. + +Notation "var <- c ; rest" := + (* I need this "fun" to tell the parser that "var" is bound *) + (c >>= (fun var => rest)) + (at level 60, right associativity). diff --git a/Recursion/Tactics.v b/Recursion/Tactics.v new file mode 100644 index 0000000..bf441df --- /dev/null +++ b/Recursion/Tactics.v @@ -0,0 +1,39 @@ +Require Import Recursion.Monad. + +(* decomposition lemma *) +Definition decomp (A:Set)(c:#A) : #A := + match c with + | Return x => Return x + | Bind B f c => Bind f c + end. +Implicit Arguments decomp. + +(* 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 *) +Ltac uncomp comp := + match goal with + | [ |- context[(comp ?X)] ] => + pattern (comp X) at 1; + rewrite decomp_thm; + simpl + | [ |- context[(comp ?X ?Y)] ] => + pattern (comp X Y) at 1; + rewrite decomp_thm; + simpl + | [ |- context[(comp ?X ?Y ?Z)] ] => + pattern (comp X Y Z) at 1; + rewrite decomp_thm; + simpl + | [ |- context[(comp ?X ?Y ?Z ?R)] ] => + pattern (comp X Y Z R) at 1; + rewrite decomp_thm; + simpl + | [ |- context[(comp ?X ?Y ?Z ?R ?Q)] ] => + pattern (comp X Y Z R Q) at 1; + rewrite decomp_thm; + simpl + end. diff --git a/Recursion/Termination.v b/Recursion/Termination.v new file mode 100644 index 0000000..4d47a4a --- /dev/null +++ b/Recursion/Termination.v @@ -0,0 +1,187 @@ +Require Import Recursion.Monad. +Require Import Coq.Logic.JMeq. + +Section Termination. + + (* an inductive predicate proving that a given computation terminates with a particular value *) + Inductive TerminatesWith (A:Set) : #A -> A -> Prop := + | TerminatesReturnWith : + forall (a:A), + TerminatesWith A (Return a) a + + | TerminatesBindWith : + forall (B:Set) (b:B) (a:A) (f:B->#A) (c:#B), + (TerminatesWith B c b) + -> TerminatesWith A (f b) a + -> TerminatesWith A (@Bind A B f c) a + . + + (* an inductive predicate proving that a given computation terminates with /some/ value *) + Inductive Terminates (A:Set) : #A -> Prop := + | TerminatesReturn : + forall (a:A), + Terminates A (Return a) + + | TerminatesBind : + forall (B:Set) (f:B->#A) (c:#B), + Terminates B c + -> (forall (b:B), (TerminatesWith B c b) -> Terminates A (f b)) + -> Terminates A (@Bind A B f c) + . + + Lemma terminating_computations_must_produce_a_value + : forall (A:Set) (c:#A), Terminates A c -> ex (fun a:A => TerminatesWith A c a). + induction 1. + + exists a. + constructor. + + elim IHTerminates. + intros. + clear IHTerminates. + + assert (exists a : A, TerminatesWith A (f x) a). + apply H1. + assumption. + + elim H3. + intros. + + exists x0. + apply (TerminatesBindWith A B x x0 f c). + assumption. + assumption. + Defined. + + Theorem coerce : forall (A B:Set)(pf:A=B)(a:#A), #B. + intros. + subst. + exact a. + Defined. + + Inductive InvokedBy (A B C:Set) : #A -> #B -> #C -> Prop := + | invokesPrev : forall + (z:#C) + (c:#B) + (f:B->#A), + InvokedBy A B C (@Bind A B f c) c z + | invokesFunc : forall + (c:#C) + (b:C) + (f:C->#A) + (pf:#A->#B) + (eqpf:A=B) + (_:JMeq (pf (f b)) (f b)) + (_:TerminatesWith C c b), + InvokedBy A B C (@Bind A C f c) (pf (f b)) c. + + 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. + + 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. + apply (H B). + Defined. + + Notation "! c :: A" := {a:A|TerminatesWith A c a} (at level 5). + Notation "'!Let' x := y 'in' z" := ((fun x => z)y)(at level 100). + Definition eval' CC cc (Z:Set) (z:#Z) (s:Safe CC cc) : (!cc::CC). + refine( + !Let eval_one_step := + fun C c Z z => + match c return (forall PRED pred Z z, InvokedBy C PRED Z c pred z -> !pred::PRED) -> !c::C with + | Return x => fun _ => exist _ x _ + | Bind CN f cn => + fun eval_pred => + match eval_pred CN cn Z z (invokesPrev C CN Z z cn f) with + | exist b pf => + match eval_pred C (f b) CN cn _ with + | exist a' pf' => exist _ a' _ + end + end + end + in + fix eval_all C c Z z (s:Safe C c) {struct s} : !c::C := + eval_one_step C c Z z (fun C' c' Z z icc => eval_all C' c' Z z (Safe_inv C C' Z c s c' z icc)) + ). + + constructor. + + refine (invokesFunc C C CN cn b f (fun x:#C=>x) _ _ _). + auto. + auto. + assumption. + + apply (TerminatesBindWith C CN b a' f cn). + assumption. + assumption. + Defined. + + 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 termination_is_safe : forall (A:Set) (c:#A) (t:Terminates A c), Safe A c. + intros. + induction t. + apply Safe_intro. + intros. + inversion H. + + apply Safe_intro. + intros. + simple inversion H1. + subst. + + apply jmeq_lemma in H2. + destruct H2. + destruct H3. + subst. + apply JMeq_eq in H2. + subst. + auto. + + intros. + apply jmeq_lemma in H4. + destruct H4. + destruct H7. + rewrite <- H5. + clear H5. + generalize H2. + clear H2. + subst. + apply JMeq_eq in H7. + apply JMeq_eq in H4. + subst. + intros. + apply JMeq_eq in H2. + rewrite H2. + apply H0. + auto. + Defined. + +End Termination. + +Implicit Arguments Terminates [A]. +Implicit Arguments TerminatesReturn [A]. +Implicit Arguments TerminatesBind [A]. +Implicit Arguments TerminatesReturnWith [A]. +Implicit Arguments TerminatesBindWith [A]. +Implicit Arguments eval' [CC]. +