Require Import FlatCompletePreorder ZArith ExtractionConsts. Set Implicit Arguments. Unset Strict Implicit. Definition f_cond (D:cpo)(t:&cpo bool)(x y:D) : D := match t with Def true => x | Def false => y | Undef => bot D end. Lemma f_cond_y_monotonic : forall (D:cpo)(t:&cpo bool)(x:D), monotonic (fun y => f_cond t x y). intros D t x y y' Hyy'. case t. intros [|]. apply ord_refl_law. apply Hyy'. unfold f_cond. apply ord_refl_law. Qed. Definition m_cond_y (D:cpo)(t:&cpo bool)(x:D) : (D -m-> D). intros. exists (fun y => f_cond t x y). apply f_cond_y_monotonic. Defined. Lemma simpl_m_cond_y : forall (D:cpo)(t:&cpo bool)(x y:D), m_cond_y t x y = f_cond t x y. trivial. Qed. Lemma m_cond_y_continuous : forall (D:cpo)(t:&cpo bool)(x:D), continuous (m_cond_y t x). intros D t x c. (* change (m_cond_y t x (lub c)) with (f_cond t x (lub c)). *) rewrite (simpl_m_cond_y t x). unfold f_cond. case t. intros [|]. assert (Hc:chain_const x <= m_cond_y (Def true) x @ c). intro n; simpl; apply ord_refl_law. apply ord_trans_law with (lub (chain_const x)). destruct (lub_chain_const_eq x) as [_ Hcst2]. exact Hcst2. apply lub_monotonic. exact Hc. assert (Hc:c <= m_cond_y (Def false) x @ c). intro n; simpl; apply ord_refl_law. apply lub_monotonic. exact Hc. apply bot_least_law. Qed. Definition c_cond_y (D:cpo)(t:&cpo bool)(x:D) : D -C-> D. intros. exists (m_cond_y t x). apply m_cond_y_continuous. Defined. Definition mc_cond_xy (D:cpo)(t:&cpo bool) : D -m-> D -C-> D. intros. exists (fun x:D => c_cond_y t x). intros x x' Hxx' y. simpl. unfold f_cond. case t. intros [|]. apply Hxx'. apply ord_refl_law. apply ord_refl_law. Defined. (* Implicit Arguments mc_cond_xy [D]. *) Lemma simpl_mc_cond_xy : forall (D:cpo)(t:&ord bool)(x y:D), mc_cond_xy D t x y = f_cond t x y. trivial. Qed. Lemma mc_cond_xy_continuous : forall (D:cpo)(t:&cpo bool), continuous (mc_cond_xy D t). intros D t c y. rewrite simpl_mc_cond_xy. unfold f_cond. case t. intros [|]. simpl. apply lub_monotonic. intro n. simpl. apply ord_refl_law. assert (Hy:forall n, y <= (mc_cond_xy D (Def false) @ c) n y). intro; apply ord_refl_law. apply ord_trans_law with (1:=Hy 0). exact (lub_upper_bound_law (mc_cond_xy D (Def false) @ c) 0 y). apply bot_least_law. Qed. Definition cc_cond_xy (D:cpo)(t:&cpo bool) : D -C-> D -C-> D. intros. exists (mc_cond_xy D t). apply mc_cond_xy_continuous. Defined. Definition mcc_cond (D:cpo) : (&cpo bool) -m-> D -C-> D -C-> D. intro. exists (cc_cond_xy D). intros t t' Htt' x y. simpl. unfold f_cond. case Htt'; intro Heq; rewrite Heq. apply ord_refl_law. apply bot_least_law. Defined. Lemma mcc_cond_continuous : forall (D:cpo), continuous (mcc_cond D). intros D c x y. assert (Hx:forall n, c n = lub c -> f_cond (c n) x y <= (mcc_cond D @ c) n x y). intros n Hcn. change ((mcc_cond D @ c) n x y) with (f_cond (c n) x y). apply ord_refl_law. destruct (lub_flat_cpo_witness c) as [n Hwit]. case_eq (lub c). intros b Hlubc. rewrite <- Hlubc. rewrite <- Hwit. change (mcc_cond D (c n)) with ((mcc_cond D @ c) n). apply (lub_upper_bound_law (mcc_cond D @ c)). intro. change (mcc_cond D Undef x y) with (bot D). apply bot_least_law. Qed. Definition cond (D:cpo) : (&cpo bool) -C-> D -C-> D -C-> D. intro. exists (mcc_cond D). apply mcc_cond_continuous. Defined. Implicit Arguments cond [D]. Lemma simpl_cond : forall (D:cpo)(t:&cpo bool)(x y:D), cond t x y = f_cond t x y. trivial. Qed. Definition f_Apply (A B:Type)(f:&ord (A->&ord B))(x:&ord A) : &ord B := match x with Def y => match f with Def g => g y | Undef => Undef end | Undef => Undef end. Definition m_Apply_x (A B:Type)(f:&ord (A->&ord B)) : monotonic (fun x => f_Apply f x). intros. intros x x' Hxx'. unfold f_Apply. case Hxx'; intro Hxeq; rewrite Hxeq; simpl; red; auto. Defined. Lemma m_Apply_x_continuous : forall (A B:Type)(f:&ord (A->&ord B)), continuous (m_Apply_x f). intros A B f c. apply ord_trans_law with (*(@m_Apply_x A B f (lub c)) with*) (f_Apply f (lub c)). apply ord_refl_law. unfold f_Apply. case_eq (lub c). intros a Hlubc. case_eq f. intros c' Hf. destruct (lub_flat_cpo_witness c) as [n Hwit]. apply ord_trans_law with ((m_Apply_x (Def c') @ c) n). rewrite simpl_monofunord_composition. apply ord_trans_law with (f_Apply (Def c') (c n)). unfold f_Apply. rewrite Hwit. rewrite Hlubc. apply ord_refl_law. apply ord_refl_law. apply (lub_upper_bound_law (m_Apply_x (Def c') @ c)). intro Hf. simpl; red; auto. intro Hlubc. simpl; red; auto. Qed. Definition c_Apply_x (A B:Type)(f:&ord (A->&ord B)) : (&cpo A) -C-> (&cpo B). intros. (* Coq 8.1 release version bug workaround *) (*info exists (m_Apply_x f).*) change (contfun (&cpo A) (&cpo B)). refine (Build_contfun (f_cont:=@m_Apply_x A B f) _). apply m_Apply_x_continuous. Defined. Lemma simpl_c_Apply_x : forall (A B:Type)(f:&ord (A->&ord B))(x:&cpo A), c_Apply_x f x = f_Apply f x. trivial. Qed. Definition m_Apply (A B:Type) : monotonic (fun f : (&cpo (A->&cpo B)) => c_Apply_x f). intros. intros f f' Hff'. intro x. repeat rewrite simpl_c_Apply_x. unfold f_Apply. case Hff'; intro Hfeq; rewrite Hfeq. apply ord_refl_law. case x; try intro; simpl; red; auto. Defined. Lemma m_Apply_continuous : forall (A B:Type), continuous (@m_Apply A B). intros A B c y. apply ord_trans_law with (f_Apply (lub c) y). apply ord_refl_law. unfold f_Apply. case_eq y. intros a Hy. case_eq (lub c). intros c' Hlubc. destruct (lub_flat_cpo_witness c) as [n Hwit]. apply ord_trans_law with (((m_Apply (A:=A) (B:=B) @ c) n) (Def a)). rewrite simpl_monofunord_composition. apply ord_trans_law with (f_Apply (c n) (Def a)). unfold f_Apply. rewrite Hwit. rewrite Hlubc. apply ord_refl_law. apply ord_refl_law. apply (lub_upper_bound_law (m_Apply (A:=A) (B:=B) @ c)). intro Hlubc. simpl; red; auto. intro Hy. simpl; red; auto. Qed. Definition Apply (A B:Type) : (&cpo (A->&cpo B)) -C-> (&cpo A) -C-> (&cpo B). intros. (* Coq 8.1 release version bug workaround *) (*info exists (@m_Apply A B).*) change (contfun (&cpo (A -> &cpo B)) ((&cpo A) -C-> &cpo B)). refine (Build_contfun (f_cont:=@m_Apply A B) _). apply m_Apply_continuous. Defined. Implicit Arguments Apply [A B]. Lemma simpl_Apply : forall (A B:Type)(f:&cpo (A->&cpo B))(x:&cpo A), Apply f x = f_Apply f x. trivial. Qed. Open Scope Z_scope. Open Scope ord_scope. Definition f_fact : (Z -> &ord Z) -> (Z -> &ord Z) := fun f z => cond (Def (Zeq_bool z 0)) (Def 1) (Apply (Def (fun v => Def (z*v))) (f (z-1))). Lemma f_fact_monotonic : @monotonic (Z-O->&cpo Z) (Z-O->&cpo Z) f_fact. intros f g Hfg z. unfold f_fact. repeat rewrite simpl_cond. repeat rewrite simpl_Apply. apply f_cond_y_monotonic. case (Hfg (z-1)); intro Hz; rewrite Hz; simpl; red; auto. Qed. Definition monofact : (Z-O->&cpo Z) -m-> (Z-O->&cpo Z). exists f_fact. apply f_fact_monotonic. Defined. Lemma simpl_monofact : forall (f:Z -o-> &ord Z)(z:Z), monofact f z = f_fact f z. trivial. Qed. Lemma monofact_continuous : continuous monofact. intros c z. rewrite simpl_monofact. unfold f_fact. destruct (lub_flat_cpo_witness (c <_o> (z-1))) as [n Hwit]. apply ord_trans_law with ((monofact @ c) n z). rewrite simpl_monofunord_composition. rewrite simpl_monofact. unfold f_fact. apply monofun_law. apply monofun_law. change (c n (z - 1)) with ((c <_o> (z - 1)) n). rewrite Hwit. apply ord_refl_law. apply (lub_upper_bound_law (monofact @ c)). Qed. Definition contfact : (Z-O->&cpo Z) -C-> (Z-O->&cpo Z). exists monofact. apply monofact_continuous. Defined. Definition f_fact' := Eval lazy beta iota zeta delta [cond Apply f_fact f_mono contfun_monofun f_cont mcc_cond cc_cond_xy mc_cond_xy c_cond_y m_cond_y f_cond c_Apply_x f_Apply] in f_fact. Print f_fact'. Definition monofact' : (Z-O->&cpo Z) -m-> (Z-O->&cpo Z). exists f_fact'. apply f_fact_monotonic. Defined. Definition contfact' : (Z-O->&cpo Z) -C-> (Z-O->&cpo Z). exists monofact'. apply monofact_continuous. Defined. Definition fact := fixp contfact'. Extract Inductive bool => "bool" [ "true" "false" ]. (* Extract Constant fixp => "let rec t d f x = f (fun y -> t d f y) x in t". Extract Constant constructive_definite_description => "Obj.magic". *) Extraction "fact.ml" fact Zdiv_eucl.