(* * 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 -> partial nat. Definition f_mu (mu : A -> nat -> partial nat) : A -> nat -> partial nat := fun x y => match f x y with Undef => Undef | Def 0 => Def y | _ => mu x (S y) end. Lemma f_mu_monotonic : @monotonic (A -o-> nat -o-> &ord nat) (A -o-> nat -o-> &ord nat) f_mu. intros g h Hgh x y. unfold f_mu. case (f x y). induction n. apply ord_refl_law. apply Hgh. apply ord_refl_law. Qed. Definition mono_mu : (A -o-> nat -o-> &ord nat) -m-> (A -o-> nat -o-> &ord nat). exists f_mu. exact f_mu_monotonic. Defined. Lemma simpl_mono_mu : forall (g:A -o-> nat -o-> &ord nat) (x:A) (y:nat), 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 ord_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 ord_refl_law. change (c n x (S y)) with (((c <_o> x) <_o> (S y)) n). rewrite Hwit. apply ord_refl_law. apply ord_refl_law. apply (lub_upper_bound_law (mono_mu @ c)). Qed. Definition cont_mu : (A -O-> nat -O-> &cpo nat) -C-> (A -O-> nat -O-> &cpo nat). exists mono_mu. exact mono_mu_continuous. Defined. Definition mu := fixp cont_mu. (* the same as above, with postponed proofs *) Definition mono_mu' := Build_monofun (O1:=A -o-> nat -o-> &ord nat) (O2:=A -o-> nat -o-> &ord nat) (f_mono:=f_mu). Definition cont_mu' (Hm : monotonic (O1:=A -o-> nat -o-> &ord nat) (O2:=A -o-> nat -o-> &ord nat) f_mu) := Build_contfun (f_cont:=mono_mu' Hm). Definition mu' (Hm : monotonic (O1:=A -o-> nat -o-> &ord nat) (O2:=A -o-> nat -o-> &ord nat) f_mu) (Hc : continuous (mono_mu' Hm)) := (fixp (cont_mu' Hc)). (* the same again, in a single definition *) Definition mu'' (Hm : monotonic (O1:=A -o-> nat -o-> &ord nat) (O2:=A -o-> nat -o-> &ord nat) f_mu) (Hc : continuous (Build_monofun (O1:=A -o-> nat -o-> &ord nat) (O2:=A -o-> nat -o-> &ord nat) (f_mono:=f_mu) Hm)) := (fixp (Build_contfun (f_cont:=Build_monofun (O1:=A -o-> nat -o-> &ord nat) (O2:=A -o-> nat -o-> &ord nat) (f_mono:=f_mu) Hm) Hc)). End minimisation.