(* 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<n ->
    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<n -> 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<n -> 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.