checkpoint

darcs-hash:20070625051233-5007d-64b9240079af604f99477226dd95679707239b35.gz

diff --git a/Recursion/Eval.v b/Recursion/Eval.v
new file mode 100644 (file)
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 (file)
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 (file)
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 (file)
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].
+