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
    in_pointed true => x
  | in_pointed false => y
  | bottom => 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 order_refl_law.
apply Hyy'.
unfold f_cond.
apply order_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 (in_pointed true) x @ c).
intro n; simpl; apply order_refl_law.
apply order_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 (in_pointed false) x @ c).
intro n; simpl; apply order_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 order_refl_law.
apply order_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 order_refl_law.

assert (Hy:forall n, y <= (mc_cond_xy D (in_pointed false) @ c) n y).
intro; apply order_refl_law.
apply order_trans_law with (1:=Hy 0).
exact (lub_upper_bound_law (mc_cond_xy D (in_pointed 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 order_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 order_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 bottom 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
    in_pointed y =>
      match f with
        in_pointed g => g y
      | bottom => bottom
      end
  | bottom => bottom
  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 order_trans_law with (*(@m_Apply_x A B f (lub c)) with*)
  (f_Apply f (lub c)).
apply order_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 order_trans_law with ((m_Apply_x (in_pointed c') @ c) n).
rewrite simpl_monofunord_composition.
apply order_trans_law with (f_Apply (in_pointed c') (c n)).
unfold f_Apply.
rewrite Hwit.
rewrite Hlubc.
apply order_refl_law.
apply order_refl_law.
apply (lub_upper_bound_law (m_Apply_x (in_pointed 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 order_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 order_trans_law with (f_Apply (lub c) y).
apply order_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 order_trans_law with (((m_Apply (A:=A) (B:=B) @ c) n) (in_pointed a)).
rewrite simpl_monofunord_composition.
apply order_trans_law with (f_Apply (c n) (in_pointed a)).
unfold f_Apply.
rewrite Hwit.
rewrite Hlubc.
apply order_refl_law.
apply order_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
      (in_pointed (Zeq_bool z 0))
      (in_pointed 1)
      (Apply (in_pointed (fun v => in_pointed (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 order_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 order_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.