(* GENERAL RECURSION VIA COINDUCTIVE TYPES *) (* by Venanzio Capretta. See corresponding article *) Require Import Relations. Require Import vectors. Require Import Arith. Require Import List. Require Import Max. (* SECTION 3. Coinductive Types of Partial Elements. *) Set Implicit Arguments. Section Partial_Definitions. Variable A:Set. CoInductive Partial: Set := rtrn : A -> Partial | step : Partial -> Partial. Inductive Value : Partial -> A -> Prop := value_return : forall a:A, Value (rtrn a) a | value_step : forall (x:Partial)(a:A), Value x a -> Value (step x) a. CoInductive Diverge : Partial -> Prop := diverge : forall x:Partial, Diverge x -> Diverge (step x). CoInductive Eqp : Partial -> Partial -> Prop := eqp_value : forall (x y:Partial)(a:A), Value x a -> Value y a -> (Eqp x y) | eqp_step : forall (x y:Partial), Eqp x y -> Eqp (step x) (step y). End Partial_Definitions. Unset Implicit Arguments. Notation "^ a " := (rtrn a) (at level 0). Notation "|> x" := (step x) (at level 0, right associativity). Notation "x ~> a" := (Value x a) (at level 71). Notation "x ~^" := (Diverge x) (at level 71). Notation "x [=] y" := (Eqp x y) (at level 70). Section Partial_Elements. Variable A:Set. Definition unfold_partial : (Partial A) -> (Partial A) := fun x => match x with rtrn a => rtrn a | step x' => step x' end. Fixpoint partial_compute (x:Partial A)(n:nat){struct n}: Partial A := match n with 0 => x | (S n') => match x with rtrn a => rtrn a | step x' => step (partial_compute x' n') end end. Lemma unfold_partial_eq : forall x:(Partial A), x = unfold_partial x. Proof. intro x; case x; auto. Qed. CoFixpoint infinite_step : (Partial A) := |> infinite_step. Fixpoint steps_return (n:nat): A -> Partial A := match n with O => fun a => ^a | S n => fun a => |> (steps_return n a) end. Lemma steps_return_value: forall (n:nat)(a:A), steps_return n a ~> a. Proof. induction n as [|n IH]. intro a; simpl; apply value_return. intro a; simpl; apply value_step; apply IH. Qed. Lemma steps_return_eq: forall (n:nat)(a:A), steps_return n a [=] ^a. Proof. intros n a; apply eqp_value with a; [apply steps_return_value | apply value_return]. Qed. (* The following is very useful: it allows us to do induction on n instead of induction on the proof of x~>a. I realize this late, so most of the proofs do not exploit this. In the next version: try to simplify proofs using it. *) Lemma value_steps_return: forall (x:Partial A)(a:A), x~>a -> exists n, x = steps_return n a. Proof. intros x a H; elim H. intro a'; exists O; trivial. intros x' a' H' [n IH]. exists (S n). simpl. rewrite IH; trivial. Qed. (* Lemma 7 in article *) Lemma infinite_diverge: (Diverge infinite_step). Proof. cofix H. rewrite (unfold_partial_eq infinite_step). simpl. apply diverge. exact H. Qed. (* Theorem 8 in article *) Theorem not_value_diverge : forall x:(Partial A), ~ (exists a:A, x~>a) -> x~^. Proof. cofix H. intros x; case x. intros a Ha; elim Ha. exists a; apply value_return. intros y Hy; apply diverge; apply H. intro Habs; case Habs. intros a0 Ha0; apply Hy; exists a0. apply value_step; assumption. Qed. (* The following 16 lemmas corresponds to the points of *) (* Lemma 10 in article *) Lemma partial_basic_1 : forall (x y:(Partial A))(a:A), x~>a -> y~>a -> x [=] y. Proof eqp_value (A:=A). Lemma partial_basic_2 : forall (x y:(Partial A)), x~^ -> y~^ -> x [=] y. Proof. cofix H. intros x y Hx Hy. inversion_clear Hx; inversion_clear Hy. apply eqp_step. apply H; assumption. Qed. Lemma partial_basic_5 : forall (x:(Partial A))(a:A), x~>a -> x[=] ^a. Proof. intros; apply eqp_value with (a:=a); try assumption. apply value_return. Qed. Lemma partial_basic_13 : forall a1 a2:A, ^a1~>a2 -> a1=a2. Proof. intros a1 a2 H; inversion_clear H; trivial. Qed. Lemma partial_basic_6 : forall (x:(Partial A))(a:A), x[=]^a -> x~>a. Proof. intros x a H; inversion_clear H. rewrite (partial_basic_13 a a0); assumption. Qed. Lemma partial_basic_14 : forall x:(Partial A), x [=] x. Proof. cofix H. intro x; case x. intro a; apply eqp_value with (a:=a); apply value_return. intro y; apply eqp_step; apply H. Qed. Lemma partial_basic_15 : forall x y:(Partial A), x [=] y -> y [=] x. Proof. cofix H. intros x y Heq; inversion_clear Heq. apply eqp_value with (a:=a); assumption. apply eqp_step; apply H; assumption. Qed. Lemma partial_basic_7 : forall (x:(Partial A))(a:A), |>x~>a -> x~>a. Proof. intros x a H; inversion_clear H; assumption. Qed. Lemma partial_basic_11 : forall x y:(Partial A), x [=] y -> x [=] |>y. Proof. cofix H. intros x y Heq; inversion_clear Heq. apply eqp_value with (a:=a); [idtac|apply value_step]; assumption. apply eqp_step; apply H; assumption. Qed. Lemma partial_basic_12 : forall x y:(Partial A), |>x [=] y -> x[=]y. Proof. intros x y Heq;inversion_clear Heq. apply eqp_value with (a:=a); [apply partial_basic_7|idtac]; assumption. apply partial_basic_11; assumption. Qed. Lemma partial_basic_3 : forall (x y:(Partial A))(a:A), x~>a -> x [=] y -> y~>a. Proof. intros x y a Hx; elim Hx. intros a0 H0; apply partial_basic_6. apply partial_basic_15; assumption. intros x0 a0 H0 IH Heq. apply IH; apply partial_basic_12; assumption. Qed. Lemma partial_basic_8 : forall x:(Partial A), |>x~^ -> x~^. Proof. intros x Hx; inversion_clear Hx. assumption. Qed. Lemma partial_basic_9 : forall (x:(Partial A))(a:A), x~>a -> ~ x~^. Proof. intros x a H; elim H. intros a0 H0; inversion H0. intros x0 a0 H0 IH H1. apply IH; apply partial_basic_8; assumption. Qed. Lemma partial_basic_4 : forall x y:(Partial A), x~^ -> x [=] y -> y~^. Proof. cofix H. intros x y Hx Heq. generalize Hx; inversion_clear Heq. elim partial_basic_9 with (x:=x)(a:=a); assumption. intro H1; apply diverge. apply H with (x:=x0); [apply partial_basic_8|idtac]; assumption. Qed. Lemma partial_basic_10 : forall (x y:(Partial A))(a:A), x~>a -> y~^ -> ~ x[=]y. Proof. intros x y a H; elim H. intros a0 H0 H1. apply partial_basic_9 with (x:=y)(a:=a0). apply partial_basic_6; apply partial_basic_15; assumption. assumption. intros x0 a0 H0 IH H1 H2; apply IH. assumption. apply partial_basic_12; assumption. Qed. Lemma partial_basic_16 : forall x y z:(Partial A), x [=] y -> y [=] z -> x [=] z. Proof. cofix H. intros x y z Hxy; inversion_clear Hxy. intro Hyz. apply partial_basic_1 with (a:=a); [assumption|idtac]. apply partial_basic_3 with (x:=y); assumption. intro Hyz; inversion_clear Hyz. apply partial_basic_1 with (a:=a); [idtac|assumption]. apply partial_basic_3 with (x:=|>y0); [assumption|apply eqp_step]. apply partial_basic_15; assumption. apply eqp_step; apply H with (y:=y0); assumption. Qed. Theorem eqp_refl : reflexive (Partial A) (Eqp (A:=A)). Proof partial_basic_14. Theorem eqp_sym : symmetric (Partial A) (Eqp (A:=A)). Proof partial_basic_15. Theorem eqp_trans : transitive (Partial A) (Eqp (A:=A)). Proof partial_basic_16. (* The following is useful to use induction on natural numbers in place of induction on the proof of x~>b. *) Fixpoint parfold (n:nat): Partial A -> Partial A := match n with O => fun x => x | (S n) => fun x => match x with ^a => ^a | |>x => parfold n x end end. Lemma parfold_eq: forall (n:nat)(x:Partial A), parfold n x [=] x. Proof. intros n; elim n. intro x; apply eqp_refl. intros n' IH x; case x. intro a; apply eqp_refl. intro x'; simpl. apply eqp_trans with x'. apply IH. apply partial_basic_11; apply eqp_refl. Qed. Lemma value_parfold: forall (x:Partial A)(a:A), x~>a -> exists n:nat, parfold n x = ^a. Proof. intros x a H; elim H. intro a'; exists 0; trivial. intros x' a' H' [n IH]. exists (S n); simpl. exact IH. Qed. Lemma parfold_value: forall (n:nat)(x:Partial A)(a:A), parfold n x = ^a -> x~>a. Proof. induction n as [|n IH]. intros x a Hxa; simpl in Hxa; rewrite Hxa; apply value_return. intro x; case x. intros a1 a2 Ha; simpl in Ha; rewrite Ha; apply value_return. intros x' a Hx'a; simpl in Hx'a; apply value_step; apply IH; assumption. Qed. (* Theorem 11 in article *) Theorem eqp_equiv : equivalence (Partial A) (Eqp (A:=A)). Proof (Build_equivalence (Partial A) (Eqp (A:=A)) eqp_refl eqp_trans eqp_sym). Inductive is_finite : (Partial A) -> Prop := finite_return : forall a:A, is_finite (^a) | finite_step : forall x:(Partial A), is_finite x -> is_finite (|>x). (* The following two lemmas correspond to *) (* Lemma 13 in article *) Lemma finite_value : forall x:(Partial A), is_finite x -> (exists a:A, x~>a). Proof. induction 1. exists a; apply value_return. case IHis_finite; intros a H0; exists a; apply value_step; assumption. Qed. Lemma value_finite : forall x:(Partial A), (exists a:A, x~>a) -> is_finite x. Proof. intros x Hex; case Hex; intros a H; elim H. exact finite_return. intros; apply finite_step; assumption. Qed. End Partial_Elements. Implicit Arguments parfold [A]. Ltac psimpl t := rewrite unfold_partial_eq with (x:=t); simpl. Section Lifting. Variables A B:Set. (* Definition 3.10 in article *) CoFixpoint par_lift : (A->B) -> (Partial A -> Partial B) := fun f x => match x with ^ a => ^ (f a) | |> x' => |> (par_lift f x') end. (* Lemma 15 from article *) Lemma par_lift_coeq : forall (f:A->B)(a:A), (par_lift f ^a) [=] ^(f a). Proof. intros f a. rewrite unfold_partial_eq with (x:=(par_lift f ^a)); simpl. apply eqp_refl. Qed. CoFixpoint mixed_pair : A -> (Partial B) -> Partial (A*B) := fun a y => match y with ^ b => ^ (a,b) | |> y' => |> (mixed_pair a y') end. CoFixpoint strict_pair : (Partial A) -> (Partial B) -> Partial (A*B) := fun x y => match x with ^ a => mixed_pair a y | |> x' => |> (strict_pair x' y) end. End Lifting. Implicit Arguments par_lift [A B]. Implicit Arguments strict_pair [A B]. Fixpoint strict_tuple (A:Set)(n:nat){struct n}: Tuple (Partial A) n -> Partial (Tuple A n) := match n return Tuple (Partial A) n -> Partial (Tuple A n) with O => fun x:unit => ^x | (S n') => fun x: (Partial A)*(Tuple (Partial A) n') => strict_pair (fst x) (strict_tuple A n' (snd x)) end. Implicit Arguments strict_tuple [A n]. Definition strict_proj: forall (A:Set)(n k:nat), k Tuple (Partial A) n -> (Partial A) := fun A n k h t => par_lift (tuple_proj k h) (strict_tuple t). Implicit Arguments strict_proj [A n]. (* SECTION 4: Recursive Functions *) (* Implementation of codes for recursive functions Inductive Recursive_Function: nat -> Set := rec_zero: Recursive_Function 1 | rec_succ: Recursive_Function 1 | rec_proj: forall n i:nat, i Recursive_Function n | rec_comp: forall k n:nat, (Recursive_Function k) -> Tuple (Recursive_Function n) k -> (Recursive_Function n) | rec_prec: forall n:nat, (Recursive_Function (1+n)) -> (Recursive_Function (2+n)) -> (Recursive_Function (1+n)) | rec_min: forall n:nat, (Recursive_Function (1+n)) -> (Recursive_Function n). TO BE COMPLETED + OPERATIONAL SEMANTICS + PROOF OF CORRECTNESS *) Definition pnat := Partial nat. Definition par_fun (n:nat):= Tuple pnat n -> pnat. Definition zero_par: pnat -> pnat := par_lift (fun x => 0). Definition succ_par: pnat -> pnat := par_lift S. Definition proj_par: forall n i:nat, i Tuple pnat n -> pnat := strict_proj (A:=nat). Definition comp_par: forall k n:nat, (par_fun k) -> Tuple (par_fun n) k -> (par_fun n) := fun k n f g x => f (mult_app g x). Fixpoint prim_rec_aux (n:nat)(f:par_fun n)(g:par_fun (2+n))(y:nat){struct y}: (par_fun n) := match y with O => f | (S y') => fun x => g (prim_rec_aux n f g y' x, (^y', x)) end. CoFixpoint prim_rec_par: forall n:nat,(par_fun n) -> (par_fun (2+n)) -> (par_fun (1+n)) := fun n f g x => let (y,x'):=x in match y with ^ m => (prim_rec_aux n f g m x') | |> y' => |> (prim_rec_par n f g (y',x')) end. CoFixpoint min_aux (n:nat)(f:par_fun (1+n))(x:Tuple pnat n): nat -> pnat -> pnat:= fun i z => match z with ^ m => match m with 0 => ^ i | (S m') => |> (min_aux n f x (S i) (f (^(S i), x))) end | |> z' => |> (min_aux n f x i z') end. Definition min_par (n:nat)(f:par_fun (1+n)): par_fun n:= fun x => min_aux n f x 0 (f (^0,x)). (* SECTION 5: Nested recursion *) CoFixpoint cnest: nat -> nat -> pnat := fun n m => match n, m with n, 0 => ^n | 0, (S m') => |> (cnest 0 m') | (S n'), (S m') => |> (cnest n' (2+m')) end. Definition nest: nat -> pnat := fun n => cnest n 1. Section Devils_Nest. Variables (A:Set) (P:A->Prop) (i:A->A) (g:forall x:A,P x->A). Hypothesis P_dec: forall x:A, {P x}+{~P x}. CoFixpoint dev_aux: A -> nat -> Partial A := fun a m => match P_dec a with left h => match m with 0 => ^(g a h) | (S m') => |> (dev_aux (g a h) m') end | right _ => |> (dev_aux (i a) (S m)) end. Definition dev: A -> Partial A := fun a => dev_aux a 0. Variable h:A->A. CoFixpoint d_cont_aux: (A -> Partial A) -> A -> Partial A := fun k a => match P_dec a with left p => k (g a p) | right _ => |> (d_cont_aux (fun y => k (h y)) (i a)) end. Definition d_cont: A -> Partial A := fun a => d_cont_aux (fun x=>^x) a. CoFixpoint devil_aux: (A -> Partial A) -> nat -> A -> Partial A := fun k m a => match P_dec a with left p => match m with 0 => k (g a p) | (S m') => |> (devil_aux k m' (g a p)) end | right _ => |> (devil_aux (fun y => k (h y)) (S m) (i a)) end. Definition devil: A -> Partial A := fun a => devil_aux (fun x => ^x) 0 a. End Devils_Nest. (* SECTION 7: Fixed points of function operators *) Definition ext_eq (A B:Set)(f1 f2: A->Partial B): Prop := forall a:A, f1 a [=] f2 a. Implicit Arguments ext_eq [A B]. Notation "x {=} y" := (ext_eq x y) (at level 70). Lemma ext_eq_sym: forall (A B:Set)(f1 f2:A->Partial B), f1{=}f2 -> f2{=}f1. Proof. intros A B f1 f2 Hf a; apply eqp_sym; apply Hf. Qed. Definition Extensional (A B:Set)(F: (A->Partial B)->(A->Partial B)): Prop := forall f1 f2:A->Partial B, f1 {=} f2 -> F f1 {=} F f2. Implicit Arguments Extensional [A B]. CoInductive cole (A:Set): Partial A -> Partial A -> Prop := cole_value : forall (x y:Partial A)(a:A), x ~> a -> y ~> a -> (cole A x y) | cole_steps : forall (x y:Partial A), cole A x y -> cole A (step x) (step y) | cole_lstep : forall (x y:Partial A), cole A x y -> cole A (step x) y. Implicit Arguments cole [A]. Implicit Arguments cole_value [A]. Implicit Arguments cole_steps [A]. Implicit Arguments cole_lstep [A]. Notation "x [<=] y" := (cole x y) (at level 70). Lemma cole_refl: forall (A:Set)(x1 x2:Partial A), x1 [=] x2 -> x1 [<=] x2. Proof. cofix H. intros A x1 x2 Heq; case Heq. intros y1 y2 a H1 H2; apply cole_value with a; assumption. intros y1 y2 H12; apply cole_steps; apply H; assumption. Qed. Lemma value_eq: forall (A:Set)(x:Partial A)(a1 a2:A),x~>a1 -> x~>a2 -> a1=a2. Proof. intros A x a1 a2 H1; elim H1. intros; apply partial_basic_13; assumption. intros x' a1' H1' IH1 H2. inversion_clear H2. apply IH1; assumption. Qed. Lemma cole_step_right: forall (A:Set)(x y:Partial A), x[<=]y -> x[<=]|>y. Proof. cofix H. intros A x y Hxy; case Hxy. intros x' y' a Hx Hy; apply cole_value with a; [idtac|apply value_step]; assumption. intros x' y' Hxy'; apply cole_steps; apply H; assumption. intros x' y' Hxy'; apply cole_lstep; apply H; assumption. Qed. Lemma cole_left_step: forall (A:Set)(x y:Partial A), |>x[<=]y -> x[<=]y. Proof. intros A x y Hle; inversion_clear Hle. apply cole_value with a; [apply partial_basic_7;assumption|assumption]. apply cole_step_right; assumption. assumption. Qed. Lemma cole_value_left: forall (A:Set)(x y:Partial A)(a:A), x~>a -> x[<=]y -> y~>a. Proof. intros A x y a Hx; elim Hx. intros a' Ha'; inversion Ha'. rewrite partial_basic_13 with (1:=H); assumption. intros x' a' Hx' IH Hle. apply IH; apply cole_left_step; assumption. Qed. Lemma cole_trans: forall (A:Set)(x y z:Partial A), x [<=] y -> y [<=] z -> x [<=] z. Proof. cofix H. intros A x y z Hxy; case Hxy. intros x' y' a Hx Hy Hyz; apply cole_value with a; [idtac|apply cole_value_left with y']; assumption. intros x' y' Hxy' Hyz; apply cole_lstep; apply H with y'; [idtac|apply cole_left_step]; assumption. intros x' y' Hxy' Hyz; apply cole_lstep; apply H with y'; assumption. Qed. (* Lemma 6.5 from article *) Lemma value_imp_cole: forall (A:Set)(x y:Partial A), (forall a:A, x~>a -> y~>a) -> x [<=] y. Proof. cofix H. intros A x; case x. intros a y Ha; apply cole_value with a; [idtac| apply Ha]; apply value_return. intros x' y Hx'; apply cole_lstep; apply H. intros a Hxa; apply Hx'; apply value_step; assumption. Qed. Lemma cole_imp_value: forall (A:Set)(x y:Partial A), x [<=] y -> (forall a:A, x~>a -> y~>a). Proof. intros A x y Hxy a Hxa; generalize Hxy; clear Hxy; elim Hxa. intros a' Ha'y; inversion_clear Ha'y. inversion_clear H. assumption. intros x' a' H' IH H. apply IH. apply cole_left_step; assumption. Qed. Definition ext_le (A B:Set)(f1 f2:A->Partial B): Prop := forall a:A, f1 a [<=] f2 a. Implicit Arguments ext_le [A B]. Notation "f1 {<=} f2" := (ext_le f1 f2) (at level 70). Lemma ext_le_refl: forall (A B:Set)(f:A->Partial B), f {<=} f. Proof. intros A B f a; apply cole_refl. apply eqp_refl. Qed. Lemma ext_le_trans: forall (A B:Set)(f1 f2 f3:A->Partial B), f1 {<=} f2 -> f2 {<=} f3 -> f1 {<=} f3. Proof. intros A B f1 f2 f3 H12 H23 a; apply cole_trans with (f2 a); [apply H12 | apply H23]. Qed. Section Fixed_Points. Variables (A B:Set) (F: (A->Partial B)->(A->Partial B)). Variable call_num_args: forall (f:A->Partial B)(a:A)(b:B), (F f a)~>b -> nat. Variable call_args: forall (f:A->Partial B)(a:A)(b:B)(h:(F f a)~>b), Vector A (call_num_args f a b h). Variable call_values: forall (f:A->Partial B)(a:A)(b:B)(h: (F f a)~>b), Vector B (call_num_args f a b h). Hypothesis call_converge: forall (f:A->Partial B)(a:A)(b:B)(h: (F f a)~>b), forall (i:Finite (call_num_args f a b h)), (f (call_args f a b h i)) ~> (call_values f a b h i). Definition finitary := forall (f:A->Partial B)(a:A)(b:B)(h: (F f a)~>b), forall (g:A->Partial B), (forall i: Finite (call_num_args f a b h), g (call_args f a b h i)[=]f (call_args f a b h i)) -> (F g a)~>b. Hypothesis F_finitary: finitary. (* Lemma 22 from article *) Lemma F_order: forall f1 f2:A->Partial B, f1 {<=} f2 -> F f1 {<=} F f2. Proof. intros f1 f2 Hf a. unfold finitary in F_finitary. apply value_imp_cole; intros b Hab. apply F_finitary with (f:=f1)(h:=Hab). intro i; apply eqp_value with (call_values f1 a b Hab i). apply cole_value_left with (x:=f1 (call_args f1 a b Hab i)). apply call_converge. apply Hf. apply call_converge. Qed. CoFixpoint fstconv: Partial B -> Partial B -> Partial B := fun x y => match x, y with ^b, _ => ^b | _, ^b => ^b | |> x, |> y => |> (fstconv x y) end. (* Lemma 23 from article *) Lemma fstconv_converge: forall (x y:Partial B)(b:B), (fstconv x y)~>b -> (x~>b)\/(y~>b). Proof. set (P:= fun (z:Partial B)(b:B) => forall (x y:Partial B), z=(fstconv x y) -> (x~>b)\/(y~>b)). intros x0 y0 b0 H0; cut (P (fstconv x0 y0) b0). intro HP; red in HP; apply HP; trivial. elim H0. intros b x; case x. intros bx y Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq; rewrite Heq; left; constructor. intros x' y; case y. intros by Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq; rewrite Heq; right; constructor. intros y' Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; discriminate Heq. intros z b Hzb IH x y; red in IH. case x. intros bx Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; discriminate Heq. intro x'; case y. intros by Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; discriminate Heq. intros y' Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq. case IH with (x:=x')(y:=y'). assumption. intro; left; constructor; assumption. intro; right; constructor; assumption. Qed. Lemma cole_second_step: forall x y:Partial B, x [<=] |>y -> x [<=] y. Proof. cofix H. intros x y Hxy. set (P := fun x y :Partial B => forall y', y=|>y' -> x[<=]y'). cut (P x |>y). intro HP; red in HP; apply HP; trivial. case Hxy. intros x0 y0 b Hx0 Hy0; red; intros y' Heq. apply cole_value with b. assumption. apply partial_basic_7; rewrite <- Heq; assumption. intros x0 y0 Hle0; red; intros y' Heq. apply cole_lstep. injection Heq; clear Heq; intro Heq; rewrite <- Heq; assumption. intros x0 y0 Hle0; red; intros y' Heq. apply cole_lstep. apply H. rewrite <- Heq; assumption. Qed. Lemma cole_step_second: forall x y: Partial B, x [<=] y -> x [<=] |>y. Proof. cofix cIH. intros x y Hle; case Hle. intros x0 y0 b Hx0 Hy0. apply cole_value with b; [assumption | apply value_step; assumption]. intros x' y' Hle'; apply cole_steps. apply cIH; assumption. intros x' y' Hle'; apply cole_steps; assumption. Qed. Lemma cole_first_step: forall x y:Partial B, |>x [<=] y -> x [<=] y. Proof. intros x y Hle. set (P := fun x y => forall x':Partial B, x=|>x' -> x'[<=]y). cut (P |>x y). intro HP; red in HP; apply HP; trivial. case Hle. intros x0 y0 b Hx0 Hy0; red; intros x' Heq; apply cole_value with b. apply partial_basic_3 with x0. assumption. rewrite Heq. apply eqp_sym; apply partial_basic_11; apply eqp_refl. assumption. intros x0 y0 Hle0 x' Heq. injection Heq; clear Heq; intro Heq; rewrite <- Heq. apply cole_step_second; assumption. intros x0 y0 Hle0; red; intros x' Heq. injection Heq; clear Heq; intro Heq; rewrite <- Heq; assumption. Qed. Lemma cole_step: forall x y:Partial B, |>x [<=] |>y -> x [<=] y. Proof. intros; apply cole_first_step; apply cole_second_step; assumption. Qed. Lemma cole_antisym: forall (x y:Partial B), x [<=] y -> y [<=] x -> x [=] y. Proof. cofix coIH. intro x; case x. intros a y Hay Hya. apply eqp_value with a. apply value_return. apply cole_value_left with (x:=^a). apply value_return. assumption. intros x' y; case y. intros a Hxa Hax. apply eqp_value with a. apply cole_value_left with (x:=^a); [apply value_return | assumption]. apply value_return. intros y' Hxy Hyx. apply eqp_step. apply coIH; apply cole_step; assumption. Qed. (* Lemma 6.6 from article *) Lemma value_equiv_eqp: forall (x y:Partial B), (forall b:B, x~>b <-> y~>b) -> x[=]y. Proof. intros x y H; apply cole_antisym; apply value_imp_cole; intro a; elim (H a); auto. Qed. Lemma eqp_value_equiv: forall (x y:Partial B), x[=]y -> (forall b:B, x~>b <-> y~>b). Proof. intros x y Hxy b; split. apply cole_imp_value. apply cole_refl; assumption. apply cole_imp_value. apply cole_refl; apply eqp_sym; assumption. Qed. Lemma ext_le_antisym: forall f1 f2:A->Partial B, f1{<=}f2 -> f2{<=}f1 -> f1{=}f2. Proof. intros f1 f2 H12 H21 a; apply cole_antisym. apply H12. apply H21. Qed. Lemma ext_eq_le: forall f1 f2:A->Partial B, f1{=}f2 -> f1{<=}f2. Proof. intros f1 f2 Hf a; apply cole_refl. apply Hf. Qed. (* Lemma 20 from article *) Lemma extF: Extensional F. Proof. red. intros f1 f2 Hf. apply ext_le_antisym. apply F_order. apply ext_eq_le; assumption. apply F_order. apply ext_eq_le; apply ext_eq_sym; assumption. Qed. Lemma fstconv_cole_right: forall x y:Partial B, x [<=] y -> fstconv x y [=] y. Proof. cofix H. intros x y; case x. intros b Hle; rewrite unfold_partial_eq with (x:=fstconv ^b y); simpl. apply partial_basic_1 with (a:=b); [apply value_return | apply cole_value_left with ^b]. apply value_return. assumption. intro x'; case y. intros b Hle; rewrite unfold_partial_eq with (x:=fstconv |>x' ^b); simpl. apply eqp_value with b; apply value_return. intros y' Hle; rewrite unfold_partial_eq with (x:=fstconv |>x' |>y'); simpl. apply eqp_step; apply H. apply cole_step; assumption. Qed. Lemma fstconv_cole_left: forall x y:Partial B, y [<=] x -> fstconv x y [=] x. Proof. cofix H. intros x y; case x. intros b Hle; rewrite unfold_partial_eq with (x:=fstconv ^b y); simpl. apply eqp_refl. intros x'; case y. intros b' Hle. inversion_clear Hle. apply eqp_value with a. rewrite unfold_partial_eq with (x:=fstconv |>x' ^b'); assumption. assumption. intros y' Hle. rewrite unfold_partial_eq with (x:=fstconv |>x' |>y'); simpl. apply eqp_step. apply H. apply cole_first_step; apply cole_second_step; assumption. Qed. Lemma fstconv_value: forall (x y:Partial B)(b:B), x~>b -> y~>b -> (fstconv x y)~>b. Proof. intros x y b Hx Hy. apply partial_basic_3 with y. assumption. apply eqp_sym. apply fstconv_cole_right. apply cole_value with b; assumption. Qed. (* Lemma 24 from article *) Lemma fst_converge_fstconverge: forall (x y: Partial B)(b:B), x~>b -> x [<=] y -> (fstconv x y)~>b. Proof. intros x y b Hxb Hle. apply partial_basic_3 with y. apply cole_value_left with x; assumption. apply eqp_sym; apply fstconv_cole_right; assumption. Qed. (* Lemma 21 from article *) Lemma fstconv_infty_id: forall y:Partial B, fstconv (infinite_step B) y [=] y. Proof. cofix H. intro y. rewrite (unfold_partial_eq B (infinite_step B)); simpl. case y. intro b; rewrite (unfold_partial_eq B (fstconv |>(cofix infinite_step : Partial B := |>infinite_step) ^(b))); simpl; apply eqp_refl. intro p; rewrite (unfold_partial_eq B (fstconv |>(cofix infinite_step : Partial B := |>infinite_step) |>p)); simpl. apply eqp_step. apply H. Qed. Let k := (fix k (n : nat) : A -> Partial B := match n with | O => fun _ : A => infinite_step B | S n0 => F (k n0) end) : nat -> A -> Partial B. Lemma infinite_step_least: forall b: Partial B, infinite_step B [<=] b. Proof. intro b; cofix H; rewrite unfold_partial_eq with (x:=infinite_step B); simpl; apply cole_lstep; assumption. Qed. Lemma infinite_step_fun_least: forall f:A->Partial B, (fun a => infinite_step B) {<=} f. Proof. intro f; red; intro a; apply infinite_step_least. Qed. Lemma k_less_step: forall n:nat, (k n) {<=} (k (S n)). Proof. simple induction n. apply infinite_step_fun_least. intros n' IH; simpl. apply F_order. apply IH. Qed. (* Lemma 22 from article *) Lemma k_inclusion: forall n m:nat, n<=m -> k n {<=} k m. Proof. induction m as [|m' IH]. intro Hn0; rewrite <- (le_n_O_eq n Hn0). apply ext_le_refl. intro HnSm'; case (le_lt_or_eq n (S m') HnSm'). intro Hnm'; simpl in HnSm'. apply ext_le_trans with (k m'); [apply IH | apply k_less_step; apply IH]. apply le_S_n; assumption. intro Heq; rewrite Heq; apply ext_le_refl. Qed. CoFixpoint parallel_search_aux: (nat->(Partial B)) -> nat -> Partial B -> Partial B:= fun f n x => match x with ^b => ^b | |>x' => |> (parallel_search_aux f (S n) (fstconv x' (f n))) end. Definition parallel_search: (nat->(Partial B)) -> Partial B := fun f => parallel_search_aux f O (infinite_step B). (* Lemma 26 from article *) Lemma parallel_search_converge: forall (f:nat->Partial B)(b:B), (parallel_search f)~>b -> exists n:nat, (f n)~>b. Proof. intros f b Hfb. set (P := fun (b:B)(y:Partial B) => forall (n:nat)(x:Partial B), y=(parallel_search_aux f n x) -> x~>b \/ exists m:nat, (f m)~>b). cut (P b (parallel_search f)). intro Hf; red in Hf. case Hf with (n:=0)(x:=infinite_step B); try auto. intro Hinf_b. elim partial_basic_9 with (x:=infinite_step B)(a:=b); [assumption | apply infinite_diverge]. elim Hfb. intro b0; red. intros n x; case x; intros b1 Hb; rewrite unfold_partial_eq in Hb; simpl in Hb. injection Hb; clear Hb; intro Hb; rewrite Hb; left; constructor. discriminate Hb. intros y' b0 Hy' IH; red in IH; red; intros n x; case x. intros b1 Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; discriminate Heq. intros x' Heq; rewrite unfold_partial_eq in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq. case IH with (n:=(S n))(x:=(fstconv x' (f n))). exact Heq. intro Hconv. elim fstconv_converge with (x:=x')(y:=(f n))(b:=b0). intro; left; constructor; assumption. intro; right; exists n; assumption. assumption. intro; right; assumption. Qed. Definition cole_monotone: (nat -> Partial B) -> Prop := fun f => (forall n m: nat, n<=m -> (f n) [<=] (f m)). Lemma monotone_convergence: forall f:nat -> Partial B, cole_monotone f -> forall (b:B)(n:nat), (f n)~>b -> forall m:nat, n <= m -> (f m)~>b. Proof. intros f Hf b n Hnb m Hnm. apply cole_value_left with (f n); [assumption | apply Hf; assumption]. Qed. Lemma fstconv_split: forall (x y:Partial B)(b:B), (fstconv x y)~>b -> (x~>b)\/(y~>b). Proof. intros x y b Hxyb. set (Q:= fun z b => forall x y, z=(fstconv x y) -> x~>b \/ y~>b). cut (Q (fstconv x y) b). intro HQ; case (HQ x y); [trivial | left; assumption | right; assumption]. elim Hxyb. intros b' x'; case x'. intros b0 y' Heq. rewrite unfold_partial_eq with (x:=fstconv ^b0 y') in Heq; simpl; injection Heq; clear Heq; intro Heq; rewrite Heq. left; apply value_return. intros x0 y'; case y'. intros b0 Heq. rewrite unfold_partial_eq with (x:=fstconv |>x0 ^(b0)) in Heq; simpl; injection Heq; clear Heq; intro Heq; rewrite Heq. right; apply value_return. intros y0 Heq. rewrite unfold_partial_eq with (x:=fstconv |>x0 |>y0) in Heq; simpl; discriminate Heq. intros z' b' H' IH x'; case x'. intros bx y' Heq. rewrite unfold_partial_eq with (x:=fstconv ^(bx) y') in Heq; discriminate Heq. intros x0 y'; case y'. intros by Heq. rewrite unfold_partial_eq with (x:=fstconv |>x0 ^(by)) in Heq; discriminate Heq. intros y0 Heq. rewrite unfold_partial_eq with (x:=fstconv |>x0 |>y0) in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq. elim (IH x0 y0). intro Hx0b'; left; apply value_step; assumption. intro Hy0b'; right; apply value_step; assumption. assumption. Qed. Lemma parallel_search_aux_converge: forall (f:nat->Partial B)(x:Partial B)(b:B)(n:nat), (parallel_search_aux f n x)~>b -> x~>b \/ exists m:nat, (f m)~>b. Proof. intros f x b n H. set (Q:= fun z b => forall x n, z=(parallel_search_aux f n x) -> x~>b \/ exists m : nat, f m ~> b). cut (Q (parallel_search_aux f n x) b). intro HQ; case (HQ x n); try auto. elim H. intros b' x'; case x'. intros b0 n' Heq. rewrite unfold_partial_eq with (x:=parallel_search_aux f n' ^(b0)) in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq; rewrite Heq; left; apply value_return. intros x'0 n' Heq. rewrite unfold_partial_eq with (x:=parallel_search_aux f n' |>x'0) in Heq; simpl in Heq; discriminate Heq. intros z b' H' IH x'; case x'. intros b0 n' Heq. rewrite unfold_partial_eq with (x:=parallel_search_aux f n' ^(b0)) in Heq; simpl in Heq; discriminate Heq. intros x0 n' Heq. rewrite unfold_partial_eq with (x:=parallel_search_aux f n' |>x0) in Heq; simpl in Heq; injection Heq; clear Heq; intro Heq. elim (IH (fstconv x0 (f n')) (S n')). intro Hconv; case fstconv_split with (1:=Hconv). intro Hx0b'; left; apply value_step; assumption. intro Hfn'b'; right; exists n'; assumption. auto. assumption. Qed. Lemma fstconv_bound: forall x y z:Partial B, x[<=]z -> y[<=]z -> (fstconv x y)[<=]z. Proof. cofix H. intro x; case x. intros bx y; case y. intros by z Hxz Hyz. psimpl (fstconv ^(bx) ^(by)); assumption. intros y' z Hxz Hyz. psimpl (fstconv ^(bx) |>y'); assumption. intros x' y; case y. intros by z Hxz Hyz. psimpl (fstconv |>x' ^(by)); assumption. intros by z Hxz Hyz. psimpl (fstconv |>x' |>by). apply cole_lstep. apply H; apply cole_first_step; assumption. Qed. Lemma both_converge_cole_eq: forall (x y:Partial B)(bx by:B), x~>bx -> y~>by -> x[<=]y -> bx=by. Proof. cut (forall (x:Partial B)(bx:B), x~>bx -> forall (y:Partial B)(by:B), y~>by -> x[<=]y -> bx=by). intros HH x y bx by Hx Hy Hxy; apply (HH x bx Hx y by Hy Hxy). intros x0 bx0 H0; elim H0. intros bx y by Hy Hle. apply partial_basic_13; apply partial_basic_3 with (x:=y). assumption. apply partial_basic_5. apply cole_value_left with (x:=^bx). apply value_return. assumption. intros x' bx Hx IH y by Hy Hle. apply IH with (y:=y)(by:=by). assumption. apply cole_left_step; assumption. Qed. Lemma snd_converge_fstconverge: forall (x y : Partial B) (b : B), y ~> b -> x[<=]y -> fstconv x y ~> b. Proof. cut (forall y b, y ~> b -> forall x, x[<=]y -> fstconv x y ~> b). auto. intros y0 b0 Hyb; elim Hyb. intros b x; case x. intros bx H. psimpl (fstconv ^(bx) ^(b)). rewrite both_converge_cole_eq with (bx:=bx)(by:=b)(3:=H); apply value_return. intros x' H; psimpl (fstconv |>x' ^(b)); apply value_return. intros y b H IH x; case x. intros bx Hx; psimpl (fstconv ^bx |>y). rewrite both_converge_cole_eq with (bx:=bx)(by:=b)(3:=Hx); try apply value_return. apply value_step; assumption. intros x' Hx; psimpl (fstconv |>x' |>y). apply value_step; apply IH; apply cole_step; assumption. Qed. Lemma fstconv_preserves_left_cole: forall x y z:Partial B, x[<=]y -> y[<=]z -> (fstconv x z)[<=](fstconv y z). Proof. cofix H. intros x; case x. intros b y z Hby Hyz. apply cole_value with b. psimpl (fstconv ^b z); apply value_return. apply snd_converge_fstconverge. apply cole_value_left with ^b. apply value_return. apply cole_trans with y; assumption. assumption. intros x' y; case y. intros b z Hx'b Hbz. apply cole_value with b. apply snd_converge_fstconverge. apply cole_value_left with ^b; [apply value_return | assumption]. apply cole_trans with ^b; assumption. apply fst_converge_fstconverge; [apply value_return | assumption]. intros y' z; case z. intros b Hx'y' Hy'b. psimpl (fstconv |>x' ^b); psimpl (fstconv |>y' ^b); apply cole_value with b; apply value_return. intros z' Hx'y' Hy'z'. psimpl (fstconv |>x' |>z'); psimpl (fstconv |>y' |>z'); apply cole_steps; apply H; apply cole_step; assumption. Qed. Lemma parfold_fstconv_first: forall (n:nat)(x y:Partial B)(b:B), (parfold n x)=^b -> x[<=]y -> (parfold n (fstconv x y)) = ^b. Proof. induction n as [|n IH]. intros x y b Heq Hle; simpl in Heq; rewrite Heq; simpl. psimpl (fstconv ^b y); simpl; trivial. intro x; case x. intros bx y b Heq; simpl in Heq; rewrite Heq. intro Hle; simpl; trivial. intros x' y; case y. intros by b Heq; simpl in Heq; intro Hle; simpl. cut (by=b). intro Hbyb; rewrite Hbyb; trivial. apply partial_basic_13. apply cole_value_left with (x:=|>x'). apply partial_basic_3 with (parfold n x'). rewrite Heq; apply value_return. apply eqp_trans with x'. apply parfold_eq. apply partial_basic_11; apply eqp_refl. exact Hle. intros y' b Heq; simpl in Heq; intro Hle; simpl. apply IH. exact Heq. apply cole_step; exact Hle. Qed. Lemma cole_step_parfold: forall f:nat -> Partial B, cole_monotone f -> forall (h:nat)(x:Partial B), forall n:nat, (forall m:nat, n<=m -> x[<=](f m)) -> forall b:B, parfold h x = ^b -> parfold h (parallel_search_aux f n x) = ^b. Proof. intros f Hf h; induction h as [|h IH]. intros x n Hx b H0; simpl in H0; rewrite H0. simpl. psimpl (parallel_search_aux f n ^b); simpl; trivial. intros x; case x. intros b' n Hb' b Hb'b; simpl in Hb'b; rewrite Hb'b. simpl; trivial. intros x' n Hx' b Hx'b; simpl in Hx'b. simpl. apply IH. intros m Hm; apply fstconv_bound. apply cole_first_step; apply Hx'. apply le_Sn_le; assumption. apply Hf. apply le_Sn_le; assumption. apply parfold_fstconv_first. assumption. apply cole_first_step; apply Hx'. apply le_n. Qed. Lemma parallel_base: forall f:nat -> Partial B, cole_monotone f -> forall x:Partial B, forall n:nat, (forall m:nat, n<=m -> x[<=](f m)) -> forall b:B, x~>b -> (parallel_search_aux f n x)~>b. Proof. intros f Hf x n Hx b Hxb. case value_parfold with (1:=Hxb). intros h Hn. apply parfold_value with (n:=h). apply cole_step_parfold; try assumption. Qed. Lemma parallel_cole_preserves: forall f:nat->Partial B, cole_monotone f -> forall x y:Partial B, x [<=] y -> forall n:nat, (forall m:nat, n<=m -> y[<=](f m)) -> (parallel_search_aux f n x) [=] (parallel_search_aux f n y). Proof. cofix H. intros f Hf x; case x. intros b y Hby n Hy; apply eqp_value with b. rewrite unfold_partial_eq with (x:=parallel_search_aux f n ^b); simpl; apply value_return. apply parallel_base. assumption. intros m Hm; apply Hy; try trivial. apply cole_value_left with ^b; [apply value_return | assumption]. intros x' y; case y. intros b Hx'b n Hb. rewrite unfold_partial_eq with (x:=parallel_search_aux f n |>x'). rewrite unfold_partial_eq with (x:=parallel_search_aux f n ^b). simpl. apply eqp_value with b. apply value_step; apply parallel_base. exact Hf. intros m Hm; apply fstconv_bound. apply cole_trans with ^b. apply cole_left_step; assumption. apply Hb. apply le_Sn_le; assumption. apply Hf. apply le_Sn_le; assumption. apply snd_converge_fstconverge. apply cole_value_left with ^b. apply value_return. apply Hb. apply le_n. apply cole_trans with ^b. apply cole_left_step; assumption. apply Hb. apply le_n. apply value_return. intros y' H' n Hy'f. rewrite unfold_partial_eq with (x:=parallel_search_aux f n |>x'). rewrite unfold_partial_eq with (x:=parallel_search_aux f n |>y'). simpl. apply eqp_step. apply H. assumption. apply fstconv_preserves_left_cole. apply cole_step; assumption. apply cole_first_step; apply Hy'f; apply le_n. intros m Hm; apply fstconv_bound. apply cole_left_step; apply Hy'f. apply le_Sn_le; assumption. apply Hf. apply le_Sn_le; assumption. Qed. (* Lemma 27 from article *) Lemma parallel_search_aux_converge_n: forall f:nat -> Partial B, cole_monotone f -> forall x:Partial B, forall n:nat, (forall m:nat, n<=m -> x[<=](f m)) -> forall m:nat, n<=m -> forall b:B, (f m)~>b -> (parallel_search_aux f n x)~>b. Proof. intros f Hf. cut (forall (b:B)(h:nat)(x:Partial B)(n:nat), (forall m:nat, n<=m -> x[<=](f m)) -> (f (n+h))~>b -> (parallel_search_aux f n x)~>b). intros HH x n Hx m Hm b Hmb. apply HH with (h:=m-n). exact Hx. rewrite <- le_plus_minus; assumption. intros b h; elim h. intros x; case x. intros b' n Hb' Hfb. psimpl (parallel_search_aux f n ^(b')). apply partial_basic_3 with (f n). rewrite (plus_0_r n) in Hfb; exact Hfb. apply eqp_value with b'. apply cole_value_left with ^b'. apply value_return. apply Hb'. apply le_n. apply value_return. intros x' n Hx' H0b. psimpl (parallel_search_aux f n |>x'). apply value_step. apply parallel_base. assumption. intros m Hm. apply fstconv_bound. apply cole_left_step; apply Hx'. apply le_Sn_le; exact Hm. apply Hf. apply le_Sn_le; exact Hm. apply snd_converge_fstconverge. rewrite (plus_0_r n) in H0b; exact H0b. apply cole_left_step; apply Hx'. apply le_n. intros h' IH x; case x. intros b' n Hb' Hfb. psimpl (parallel_search_aux f n ^(b')). apply partial_basic_3 with (f (n+(S h'))). assumption. apply eqp_value with b'. apply cole_value_left with ^b'. apply value_return. apply Hb'. apply le_plus_l. apply value_return. intros x' n Hx' Hh'b. psimpl (parallel_search_aux f n |>x'). apply value_step. apply IH. intros m Hm; apply fstconv_bound; [apply cole_left_step; apply Hx' | apply Hf]; apply le_Sn_le; exact Hm. rewrite plus_Snm_nSm with (n:=n)(m:=h'); assumption. Qed. Lemma parallel_search_converge_n: forall f:nat->Partial B, cole_monotone f -> forall (n:nat)(b:B), (f n)~>b -> (parallel_search f)~>b. Proof. intros f Hf n b Hnb; unfold parallel_search. apply parallel_search_aux_converge_n with (m:=n); try assumption. intros m Hm; apply infinite_step_least. apply le_O_n. Qed. Definition Y: A -> Partial B := fun a => parallel_search (fun n => k n a). (* Lemma 32 from article, left-to-right *) Lemma Y_to_k_1: forall (a:A)(b:B), (Y a)~>b -> exists n:nat, (k n a)~>b. Proof. intros a b HY; apply (parallel_search_converge (fun n => (k n a))). exact HY. Qed. (* Lemma 32 from article, right-to-left *) Lemma Y_to_k_2: forall (a:A)(b:B), (exists n:nat, (k n a)~>b) -> (Y a)~>b. Proof. intros a b [n H]. unfold Y. apply parallel_search_converge_n with n. intros n' m' Hle; apply k_inclusion; assumption. assumption. Qed. Lemma vector_max_le: forall (m:nat)(P:Finite m -> nat -> Prop), (forall (i:Finite m)(n1 n2:nat), n1<=n2 -> P i n1 -> P i n2) -> (forall i, exists n, P i n) -> exists N, forall i, P i N. Proof. induction m as [|m IH]. intros P HP H. exists 0. intro i; inversion i. intros P HP H. case (H (fin_zero m)). intros n0 Hn0. set (P':= fun (i:Finite m)(n:nat) => P (fin_succ i) n). cut (forall (i : Finite m) (n1 n2 : nat), n1 <= n2 -> P' i n1 -> P' i n2). intro HP'. cut (forall i : Finite m, exists n : nat, P' i n). intro H'. case (IH P' HP' H'); intros N HN. exists (max n0 N). intros i; case (finite_case m i). intro Heq; rewrite Heq; apply HP with (n1:=n0). apply le_max_l. assumption. intros [j Hj]; rewrite Hj. change (P' j (max n0 N)). apply HP' with (n1:= N). apply le_max_r. apply HN. intros i; case (H (fin_succ i)); intros n Hn; exists n; exact Hn. intros i; exact (HP (fin_succ i)). Qed. Section Arguments_Vectors. Variables (m:nat) (a:Vector A m) (b:Vector B m). Hypothesis args_converge: forall i:Finite m, (Y (a i))~>(b i). Lemma stage_sup: exists N, forall i:Finite m, (k N (a i))~>(b i). Proof. apply vector_max_le with (m:=m) (P:= fun i n => (k n (a i))~>(b i)). intros i n1 n2 Hn12 Habi. apply cole_value_left with (x:=k n1 (a i)). assumption. apply k_inclusion; assumption. intros i. exact (Y_to_k_1 (a i) (b i) (args_converge i)). Qed. End Arguments_Vectors. Lemma k_cole_Y: forall n:nat, k n {<=} Y. Proof. intros n a; apply value_imp_cole; intros b H. apply Y_to_k_2. exists n; exact H. Qed. Theorem Y_prefix_point: (F Y) {<=} Y. red. intro a. apply value_imp_cole. intros b Hab. apply Y_to_k_2. elim stage_sup with (a:=call_args Y a b Hab) (b:=call_values Y a b Hab). intros N HN; exists (S N). simpl. unfold finitary in F_finitary. apply (F_finitary Y a b Hab). intro i. apply eqp_value with (call_values Y a b Hab i). apply HN. apply cole_value_left with (x:=k N (call_args Y a b Hab i)). apply HN. apply k_cole_Y. apply call_converge. Qed. Lemma parallel_search_aux_bound: forall (f: nat -> Partial B)(n:nat)(x y:Partial B), x[<=]y -> (forall m:nat, n<=m -> (f m)[<=]y) -> parallel_search_aux f n x [<=] y. Proof. cofix coIH. intros f n x; case x. intros b y Hby Hf; psimpl (parallel_search_aux f n ^b); assumption. intros x' y Hx'y Hf; psimpl (parallel_search_aux f n |>x'). apply cole_lstep. apply coIH. apply fstconv_bound. apply cole_first_step; assumption. apply Hf. apply le_n. intros m Hm; apply Hf. apply le_Sn_le; assumption. Qed. Lemma parallel_search_bound: forall (f: nat -> Partial B)(y: Partial B), (forall n:nat, f n [<=] y) -> parallel_search f [<=] y. Proof. intros f y H; unfold parallel_search; apply parallel_search_aux_bound. apply infinite_step_least. intros; apply H. Qed. (* Theorem 35 from article *) Theorem Y_fixed_point: F Y {=} Y. Proof. intro a. apply cole_antisym. apply Y_prefix_point. unfold Y at 1. apply parallel_search_bound. intro n; case n. apply infinite_step_least. intro n'; simpl. apply F_order. apply k_cole_Y. Qed. (* Theorem 36 from article *) Theorem Y_least: forall f: A -> Partial B, F f {<=} f -> Y {<=} f. Proof. intros f H. assert (Hle: forall n, k n {<=} f). induction n as [|n IH]. intro; apply infinite_step_least. apply ext_le_trans with (F f). simpl; apply F_order; assumption. assumption. unfold Y; intro a; apply parallel_search_bound. intro n; apply (Hle n a). Qed. End Fixed_Points.