(*
 * The strength of partial recursive functions is achieved in the library of
 * flat complete preorders by specifying the minimisation functional mu.
 *)

Require Export FlatCompletePreorder FixedPoint.
Set Implicit Arguments.

(* primitive recursion *)
Fixpoint primrec (f:nat->nat) (g:nat->nat->nat->nat) (x y:nat) {struct y} : nat :=
  match y with
    0 => f x
  | S p => g x p (primrec f g x p)
  end.

Section minimisation.

Variable A : Type.
Variable f : A -> nat -> pointed nat.

Definition f_mu (mu : A -> nat -> pointed nat) : A -> nat -> pointed nat :=
  fun x y =>
    match f x y with
      bottom => bottom
    | in_pointed 0 => in_pointed y
    | _ => mu x (S y)
    end.

Lemma f_mu_monotonic :
  @monotonic (A -o-> nat_ord -o-> &ord nat) (A -o-> nat_ord -o-> &ord nat) f_mu.
intros g h Hgh x y.
unfold f_mu.
case (f x y).
induction n.
apply order_refl_law.
apply Hgh.
apply order_refl_law.
Qed.

Definition mono_mu :
  (A -o-> nat_ord -o-> &ord nat) -m-> (A -o-> nat_ord -o-> &ord nat).
exists f_mu.
exact f_mu_monotonic.
Defined.

Lemma simpl_mono_mu : forall (g:A -o-> nat_ord -o-> &ord nat) (x:A) (y:nat_ord),
  mono_mu g x y = f_mu g x y.
trivial.
Qed.

Lemma mono_mu_continuous : continuous mono_mu.
intros c x y.
rewrite simpl_mono_mu.
unfold f_mu.
destruct (lub_flat_cpo_witness ((c <_o> x) <_o> (S y))) as [n Hwit].
apply order_trans_law with ((mono_mu @ c) n x y).
rewrite simpl_monofunord_composition.
rewrite simpl_mono_mu.
unfold f_mu.
case (f x y).
induction n0.
apply order_refl_law.
change (c n x (S y)) with (((c <_o> x) <_o> (S y)) n).
rewrite Hwit.
apply order_refl_law.
apply order_refl_law.
apply (lub_upper_bound_law (mono_mu @ c)).
Qed.

Definition cont_mu :
  (A -O-> nat_ord -O-> &cpo nat) -C-> (A -O-> nat_ord -O-> &cpo nat).
exists mono_mu.
exact mono_mu_continuous.
Defined.

Definition mu := fixp cont_mu.

End minimisation.