Require Export Preorder.
Require Import Relations.

Set Implicit Arguments.
Unset Strict Implicit.

(* complete preorder *)
Record cpo : Type := Build_cpo {
  O_cpo :> ord;
  bot : O_cpo;
  lub : (chain O_cpo) -> O_cpo;
  bot_least_law : forall x:O_cpo, bot <= x;
  lub_upper_bound_law :
    forall (c:chain O_cpo)(n:nat_ord), c n <= lub c;
  lub_least_law :
    forall (c:chain O_cpo)(x:O_cpo),   (forall n, c n <= x) -> lub c <= x
}.

Lemma lub_monotonic : forall (D:cpo)(c c':chain D), c <= c' -> lub c <= lub c'.
intros D c c' Hcc'.
apply lub_least_law.
intro n.
apply order_trans_law with (c' n).
apply Hcc'.
apply lub_upper_bound_law.
Qed.

Definition monolub (D:cpo) : chain D -m-> D.
intro.
exists (@lub D).
unfold monotonic.
intros c c'.
apply lub_monotonic.
Defined.

Lemma precontinuous : forall (D1 D2:cpo)(f:D1 -m-> D2)(c:chain D1),
  lub (f @ c) <= f (lub c).
intros.
apply lub_least_law.
intro n.
simpl.
apply (monofun_law f).
apply (lub_upper_bound_law c).
Qed.

Lemma lub_upper_bound_eq : forall (D:cpo)(c:chain D)(x:D),
  (lub c) = x -> (forall n, c n <= x).
intros D c x Hlubc n.
assert (Hrel:lub c <= x) by (apply eq_rel_ord; exact Hlubc).
apply order_trans_law with (lub c).
apply lub_upper_bound_law.
exact Hrel.
Qed.

Lemma lub_chain_const_eq : forall (D:cpo)(k:D),
  lub (chain_const k) == k.
intros.
split.
apply lub_least_law.
intro n.
simpl.
apply order_refl_law.

assert (Hk:forall n, k <= (chain_const k) n).
intro n.
simpl.
apply order_refl_law.

apply order_trans_law with (1:=Hk 0).
exact (lub_upper_bound_law (chain_const k) 0).
Qed.

Section continuous_function_space.

Variables D1 D2:cpo.

Definition continuous (f:D1 -m-> D2) := forall c:chain D1, f (lub c) <= lub (f @ c).

Record > contfun : Type := Build_contfun {
  f_cont : D1 -m-> D2;
  contfun_law : continuous f_cont
}.

Definition contfun_monofun : contfun -> monofun D1 D2.
intro f.
exists (f_mono (f_cont f)).
auto.
unfold monotonic.
apply (monofun_law (f_cont f)).
Defined.
Coercion contfun_monofun : contfun >-> monofun.

Definition rel_contfunord := fun f g:contfun => forall x, f x <= g x.

Lemma rel_contfunord_refl : reflexive contfun rel_contfunord.
red.
red.
intros f x.
apply order_refl_law.
Qed.

Lemma rel_contfunord_trans : transitive contfun rel_contfunord.
red.
red.
unfold rel_contfunord.
intros f g h Hfg Hgh x.
apply order_trans_law with (g x); firstorder.
Qed.

Canonical Structure contfunord :=
  Build_ord rel_contfunord_refl rel_contfunord_trans.

End continuous_function_space.

Infix "-c->" := contfunord (at level 35, right associativity) : ord_scope.

Lemma mutually_continuous :
  forall (D D':cpo)(f:D-c->D')(g:D-m->D')(c:chain D),
    (forall (n:nat_ord), f (c n) <= (g @ c) n) -> f (lub c) <= lub (g @ c).
intros D A f g c Hn.
apply order_trans_law with (lub (f @ c)).
apply (contfun_law f c).
assert (Hn_comp:forall n, (f @ c) n <= (g @ c) n) by trivial.
assert (Hcomp:f @ c <= g @ c) by exact (chains_pointwise Hn_comp).
exact (lub_monotonic Hcomp).
Qed.

Definition contfunord_mono_monofunord (D1 D2:cpo) : (D1-c->D2)-m->(D1-m->D2).
intros.
exists (@f_cont D1 D2).
unfold monotonic.
intros; trivial.
Defined.

Definition contfunord_app (O:ord)(D1 D2:cpo)(f:O-m->D1-c->D2)(x:D1) : O-m->D2 :=
  ((contfunord_mono_monofunord D1 D2) @ f) <_m> x.

Infix "<_c>" := contfunord_app (at level 30, no associativity) : ord_scope.

Lemma simpl_contfunord_app :
  forall (O:ord)(D1 D2:cpo)(f:O-m->D1-c->D2)(x:D1)(y:O), (f <_c> x) y = f y x.
trivial.
Qed.

Lemma monofunord_id_continuous : forall (D:cpo), continuous (monofunord_id D).
unfold continuous.
intros D c.
simpl.
assert (H:c <= monofunord_id D @ c) by
  (apply eq_ord_rel_ord; apply (monofunord_id_left c)).
apply lub_monotonic; apply H.
Qed.

Definition contfunord_id (D:cpo) : D-c->D.
intro.
exists (monofunord_id D).
unfold continuous.
intro c.
apply monofunord_id_continuous.
Defined.

Lemma composition_continuous : forall (D1 D2 D3:cpo)(f:D1-c->D2)(g:D2-c->D3),
  continuous (g@f).
intros D1 D2 D3 f g c.
rewrite simpl_monofunord_composition.
(*replace ((g@f) (lub c)) with (g (f (lub c))) by auto.*)
assert (H:g (f (lub c)) <= g (lub (f@c))) by
  (apply monofun_law; apply (contfun_law f c)).
apply order_trans_law with (1:=H).
replace ((g@f)@c) with (g@(f@c)) by trivial.
  (* by apply (monofunord_composition_assoc c f g). *)
apply (contfun_law g (f@c)).
Qed.

Definition contfunord_composition
  (D1 D2 D3:cpo)(f:D1-c->D2)(g:D2-c->D3) : D1-c->D3.
intros.
exists (g@f).
apply composition_continuous.
Defined.

Notation "g @@ f" := (contfunord_composition f g) (at level 45, right associativity) : ord_scope.

Lemma simpl_contfunord_composition : forall (D1 D2 D3:cpo)(f:D1-c->D2)(g:D2-c->D3)(x:D1),
  (g @@ f) x = g (f x).
trivial.
Qed.

(* can this be proven without extensionality ?
Lemma contfunord_composition_assoc : forall (D1 D2 D3 D4:cpo)(f:D1-c->D2)(g:D2-c->D3)(h:D3-c->D4),
  h@@(g@@f) = (h@@g)@@f.
*)

Lemma contfunord_composition_assoc : forall (D1 D2 D3 D4:cpo)(f:D1-c->D2)(g:D2-c->D3)(h:D3-c->D4),
  (h@@(g@@f)) == ((h@@g)@@f).
intros.
split; red; intro x.
apply order_trans_law with (h ((g@@f) x));
 elim simpl_contfunord_composition with (f:=g@@f) (g:=h) (x:=x);
 apply order_refl_law.
(* <== *)
apply order_trans_law with ((h@@g) (f x));
 elim simpl_contfunord_composition with (f:=f) (g:=h@@g) (x:=x);
 apply order_refl_law.
Qed.

Lemma contfunord_composition_rel : forall (D1 D2 D3:cpo)(f f':D1-c->D2)(g g':D2-c->D3),
  f <= f' -> g <= g' -> g@@f <= g'@@f'.
intros O1 O2 O3 f f' g g' Hf Hg.
simpl.
unfold rel_monofunord.
intro x.
replace ((g@@f) x) with (g (f x)) by trivial.
replace ((g'@@f') x) with (g' (f' x)) by trivial.
apply order_trans_law with (g (f' x)).
apply monofun_law; trivial.
trivial.
Qed.

Section cpo_functional_constructs.

Variables (A:Type)(D:cpo).

Definition bot_funcpo : A-o->D := fun _:A => bot D.

Lemma bot_funcpo_least : forall x:(A-o->D), bot_funcpo <= x.
unfold bot_funcpo.
simpl.
intros f x.
apply bot_least_law.
Qed.

Definition lub_funcpo (c:chain (A-o->D)) : A-o->D :=
  fun x:A => lub (c <_o> x).

Lemma lub_funcpo_upper_bound : forall (c:chain (A-o->D))(n:nat_ord),
  (c n) <= (lub_funcpo c).
unfold lub_funcpo.
simpl.
intros c n x.
exact (lub_upper_bound_law (c <_o> x) n).
Qed.

Lemma lub_funcpo_least : forall (c:chain (A-o->D))(f:(A-o->D)),
  (forall n, (c n) <= f) -> (lub_funcpo c) <= f.
simpl.
unfold rel_funord.
intros c f Hfx x.
unfold lub_funcpo.
apply lub_least_law.
intro n.
simpl.
exact (Hfx n x).
Qed.

Canonical Structure funcpo :=
  Build_cpo bot_funcpo_least lub_funcpo_upper_bound lub_funcpo_least.

End cpo_functional_constructs.

Infix "-O->" := funcpo (at level 35, right associativity) : ord_scope.

Lemma simpl_lub_funord_app : forall (A:Type)(D:cpo)(c:chain (A-O->D))(x:A),
  lub (c <_o> x) = (lub c) x.
trivial.
Qed.

Section cpo_monotonic_functional_constructs.

Variables (O:ord)(D:cpo).

Lemma bot_funcpo_monotonic : monotonic (@bot_funcpo O D).
unfold monotonic.
intros x y Hxy.
apply order_refl_law.
Qed.

Definition bot_monofuncpo := Build_monofun bot_funcpo_monotonic.

Lemma bot_monofuncpo_least : forall f:(O-m->D), bot_monofuncpo <= f.
simpl.
unfold rel_monofunord.
intros f x.
apply (bot_least_law (f x)).
Qed.

Definition lub_monofuncpo (c:chain (O-m->D)) : O-m->D.
intros.
exists (fun n => lub (c <_m> n)).
unfold monotonic.
intros x y Hxy.
apply lub_monotonic.
simpl.
intro m.
simpl.
apply (monofun_law (c m)).
exact Hxy.
Defined.

Lemma lub_monofuncpo_app_eq : forall (c:chain (O-m->D))(x:O),
  lub_monofuncpo c x == lub (c <_m> x).
split; apply order_refl_law.
Qed.

Lemma lub_monofuncpo_upper_bound : forall (c:chain (O-m->D))(n:nat_ord),
  (c n) <= (lub_monofuncpo c).
intros.
simpl.
intro m.
apply order_trans_law with (lub (c <_m> m)).
apply order_trans_law with ((c <_m> m) n).
simpl; apply order_refl_law.
apply lub_upper_bound_law.
case (lub_monofuncpo_app_eq c m); trivial.
Qed.

Lemma lub_monofuncpo_least : forall (c:chain (O-m->D))(f:O-m->D),
  (forall n, (c n) <= f) -> (lub_monofuncpo c) <= f.
intros c f H x.
simpl.
apply lub_least_law.
intro n.
simpl.
apply H.
Qed.

Canonical Structure monofuncpo :=
  Build_cpo bot_monofuncpo_least lub_monofuncpo_upper_bound lub_monofuncpo_least.

End cpo_monotonic_functional_constructs.

Infix "-M->" := monofuncpo (at level 35, right associativity) : ord_scope.

Lemma simpl_lub_monofuncpo : forall (O:ord)(D:cpo)(c:chain (O-M->D))(x:O),
  (lub c) x = lub (c <_m> x).
trivial.
Qed.

Definition chaincpo (D:cpo) := nat_ord -M-> D.

Lemma lub2_diag : forall (D:cpo)(c:chain (chaincpo D)),
             lub (lub c) == lub (monofunord_diag c).
intros.
split.
apply lub_least_law.
intro n.
simpl.
apply lub_least_law.
intro m.
simpl.
apply order_trans_law with (c (n+m) (n+m)).
apply (monotonic2 c); simpl; auto with arith.
exact (lub_upper_bound_law (monofunord_diag c) (n+m)).
apply lub_monotonic.
intro n.
simpl.
exact (lub_upper_bound_law (c <_m> n) n).
Qed.

Lemma lub_monolub_monofunord_app : forall (D:cpo)(c:chain (chain D)),
  lub ((monolub D) @ c) <= lub (lub_monofuncpo c).
intros.
apply lub_least_law.
intro n.
simpl.
apply lub_monotonic.
intro m.
apply order_trans_law with (lub (c <_m> m)).
replace (c n m) with ((c <_m> m) n) by trivial.
apply lub_upper_bound_law.
simpl.
apply lub_monotonic.
apply order_refl_law.
Qed.

Lemma lub_monolub_monofunord_app_sym : forall (D:cpo)(c:chain (chain D)),
  lub (lub_monofuncpo c) <= lub ((monolub D) @ c).
intros.
apply lub_least_law.
intro n.
simpl.
apply lub_monotonic.
intro m.
simpl.
apply lub_upper_bound_law.
Qed.

Section cpo_continuous_functional_constructs.

Variables (D1 D2:cpo).

Lemma bot_monofuncpo_continuous : continuous (bot_monofuncpo D1 D2).
unfold continuous.
intro c.
simpl.
unfold bot_funcpo.
apply bot_least_law.
Qed.

Definition bot_contfuncpo := Build_contfun bot_monofuncpo_continuous.

Lemma bot_contfuncpo_least : forall f:(D1-c->D2), bot_contfuncpo <= f.
intro f.
simpl.
unfold rel_contfunord.
simpl.
intro x.
unfold bot_funcpo.
exact (bot_least_law (f x)).
Qed.

Lemma lub_monofuncpo_continuous : forall (c:chain (D1-m->D2)),
  (forall n:nat_ord, continuous (c n)) -> continuous (@lub (D1-M->D2) c).
unfold continuous.
intros c H c0.
simpl.
(* unfold f_lub_monofuncpo. *)
apply lub_least_law.
intro n.
simpl.
apply order_trans_law with (1:=(H n c0)).
apply lub_least_law.
intro n0.
(*simpl.*)
assert (HlubM:(c n @ c0) n0 <= (lub_monofuncpo c @ c0) n0) by
  (repeat rewrite simpl_monofunord_composition; apply lub_monofuncpo_upper_bound).
apply order_trans_law with (1:=HlubM).
apply lub_upper_bound_law.
Qed.

Definition lub_contfuncpo (c:chain (D1-c->D2)) : D1-c->D2.
intro.
exists (lub ((contfunord_mono_monofunord D1 D2)@c)).
(* exists (@lub (D1-M->D2) (contfunord_mono_monofunord D1 D2) @ c). *)
apply lub_monofuncpo_continuous.
intro n.
simpl.
apply contfun_law.
Defined.

Lemma simpl_lub_contfuncpo : forall (c:chain (D1-c->D2))(x:D1),
  lub_contfuncpo c x = lub (c <_c> x).
trivial.
Qed.

Lemma lub_contfuncpo_upper_bound : forall (c:chain (D1-c->D2))(n:nat_ord),
  (c n) <= (lub_contfuncpo c).
intros c n m.
rewrite simpl_lub_contfuncpo.
apply order_trans_law with ((c <_c> m) n).
simpl; apply order_refl_law.
apply lub_upper_bound_law.
Qed.

Lemma lub_contfuncpo_least : forall (c:chain (D1-c->D2))(f:D1-c->D2),
  (forall n, (c n) <= f) -> (lub_contfuncpo c) <= f.
intros c f H x.
simpl.
apply lub_least_law.
intro n.
simpl.
apply (H n x).
Qed.

Canonical Structure contfuncpo :=
  Build_cpo bot_contfuncpo_least lub_contfuncpo_upper_bound lub_contfuncpo_least.

End cpo_continuous_functional_constructs.

Infix "-C->" := contfuncpo (at level 35, right associativity) : ord_scope.

Definition contfuncpo_id (D:cpo) : D-C->D.
exact contfunord_id.
Defined.

Definition contfuncpo_composition
  (D1 D2 D3:cpo)(f:D1-C->D2)(g:D2-C->D3) : D1-C->D3.
exact contfunord_composition.
Defined.