Require Import Relations Le.

Set Implicit Arguments.
Unset Strict Implicit.

(* The axiom of extensionality would be needed in case the underlying order of
   our particular kind of a cpo had the antisymmetry condition. We don't put or
   use that condition. Therefore we don't introduce the extensionality axiom. *)
(*
Axiom extensionality :
  forall (A:Type)(B:A->Type)(f g:forall x:A, B x), (forall x, f x = g x) -> f = g.
*)

(* preorder *)
Record ord : Type := Build_ord {
  carrier_ord :> Type;
  rel_ord : relation carrier_ord;
  order_refl_law : reflexive carrier_ord rel_ord;
  order_trans_law : transitive carrier_ord rel_ord
  (* order_antisym_law : antisymmetric carrier_ord rel_ord *)
}.

Bind Scope ord_scope with ord.

Infix "<=" := rel_ord : ord_scope.

Open Scope ord_scope.

Lemma eq_rel_ord : forall (O:ord)(x y:O), x=y -> x<=y.
intros O x y H.
rewrite H.
apply order_refl_law.
Qed.

Lemma eq_rel_ord_sym : forall (O:ord)(x y:O), x=y -> y<=x.
intros O x y H.
rewrite <- H.
apply order_refl_law.
Qed.

Section ordered_function_space.

Variables (A:Type)(O:ord).

Definition rel_funord := fun f g:A->O => forall x, f x <= g x.

Lemma rel_funord_refl : reflexive (A->O) rel_funord.
red.
red.
intros f x.
apply order_refl_law.
Qed.

Lemma rel_funord_trans : transitive (A->O) rel_funord.
red.
red.
intros f g h Hfg Hgh x.
apply order_trans_law with (g x); firstorder.
Qed.

(*
(* this is how one proves antisymmetry using a non-constructive axiom *)
Lemma rel_funord_antisym : antisymmetric (A->O) rel_funord.
red.
unfold rel_funord.
intros f g Hfg Hgf.
apply extensionality.
intro x.
apply (@order_antisym_law O); firstorder.
Qed.
*)

Canonical Structure funord :=
  Build_ord rel_funord_refl rel_funord_trans (* rel_funord_antisym *) .

End ordered_function_space.

(* an alternative definition *)
(*
Definition funord (A:Type)(O:ord) : ord.
intros A O.
exists (A->O) (fun f g:A->O => forall x, (f x) <= (g x)).
unfold reflexive.
intros f x.
apply order_refl_law.
unfold transitive.
intros f g h Hfg Hgh x.
apply order_trans_law with (g x); auto.
Defined.
*)

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

Definition eq_ord (O:ord)(a b:O) := a <= b /\ b <= a.
Infix "==" := eq_ord (at level 80, no associativity) : ord_scope.

Lemma eq_eq_ord (O:ord)(a b:O) : a=b -> a==b.
intros O a b H.
split; [apply eq_rel_ord | apply eq_rel_ord_sym]; trivial.
Qed.

Lemma eq_ord_rel_ord : forall (O:ord)(x y:O), x==y -> x<=y.
(* unfold eq_ord. *)
firstorder.
Qed.

Lemma eq_ord_rel_ord_sym : forall (O:ord)(x y:O), x==y -> y<=x.
firstorder.
Qed.

Lemma eq_ord_refl : forall (O:ord)(x:O), x == x.
(* unfold eq_ord. *)
split; apply order_refl_law.
Qed.

Lemma eq_ord_sym : forall (O:ord)(x y:O), x==y -> y==x.
firstorder.
Qed.

Lemma eq_ord_trans : forall (O:ord)(x y z:O), x==y -> y==z -> x==z.
unfold eq_ord.
split; apply order_trans_law with y; firstorder.
Qed.

(* a weaker lemma in place of a non-constructive proof of
   rel_funord being antisymmetric *)
Lemma rel_ord_antisym : forall (O:ord)(x y:O), x<=y -> y<=x -> x==y.
split; assumption.
Qed.

Section ordered_nat.

Lemma nat_le_refl : reflexive nat le.
red.
auto with arith.
Qed.

Lemma nat_le_trans : transitive nat le.
red.
intros x y z Hxy Hyz.
apply le_trans with y; auto.
Qed.

Definition nat_ord := Build_ord nat_le_refl nat_le_trans.

End ordered_nat.

Section monotonic_function_space.

Variables O1 O2:ord.

Definition monotonic (f:O1->O2) := forall (x y:O1), x <= y -> f x <= f y.

Record > monofun : Type := Build_monofun {
  f_mono :> O1 -> O2;
  monofun_law : monotonic f_mono
}.

Definition rel_monofunord := fun f g:monofun => forall x, f x <= g x.

Lemma rel_monofunord_refl : reflexive monofun rel_monofunord.
red.
red.
intros f x.
apply order_refl_law.
Qed.

Lemma rel_monofunord_trans : transitive monofun rel_monofunord.
red.
red.
intros f g h Hfg Hgh x.
apply order_trans_law with (g x); firstorder.
Qed.

Canonical Structure monofunord :=
  Build_ord rel_monofunord_refl rel_monofunord_trans.

End monotonic_function_space.

(*
Definition monofunord (O1 O2:ord) : ord.
intros.
exists (monofun O1 O2) (fun f g:monofun O1 O2 => forall x, f x <= g x); red.
intros f x.
apply order_refl_law.
intros f g h Hfg Hgh x.
apply order_trans_law with (g x); firstorder.
Qed.
*)

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

Definition monofunord_const (O1 O2:ord)(k:O2) : O1-m->O2.
intros.
exists (fun x:O1 => k).
unfold monotonic.
intros.
apply order_refl_law.
Defined.

Definition chain (O:ord) := nat_ord -m-> O.

Definition chain_const (O:ord)(k:O) : nat_ord -m-> O :=
  monofunord_const nat_ord k.

Lemma chains_pointwise : forall (O:ord)(c c':chain O),
  (forall (n:nat_ord), c n <= c' n) -> c <= c'.
trivial.
Qed.

Lemma chain_weak_determinacy : forall (O:ord)(c:chain O)(n m:nat_ord)(x:O),
  m > n -> (c m) = x -> (c n) <= x.
intros O c n m x Hnm Hcm.
assert (n <= m)%nat by (auto with arith).
assert (c n <= c m) by (apply (monofun_law c); assumption).
assert (c m <= x) by (apply eq_rel_ord; assumption).
apply order_trans_law with (c m); assumption.
Qed.

Lemma monotonic2 :
  forall (O1 O2 O3:ord)(f:O1-m->O2-m->O3)(x x':O1)(y y':O2)
    (Hx:x <= x')(Hy:y <= y'), f x y <= f x' y'.
intros.
apply order_trans_law with (f x y').
exact (monofun_law (f x) Hy).
assert (Hf:f x <= f x') by exact (monofun_law f Hx).
trivial.
Qed.

Definition funord_app (A:Type)(O1 O2:ord)(f:O1-m->A-o->O2)(x:A) : O1-m->O2.
intros.
exists (fun y:O1 => f y x).
unfold monotonic.
intros y1 y2 Hy.
assert (Hf:f y1 <= f y2).
apply monofun_law.
exact Hy.
apply Hf.
Defined.

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

Lemma simpl_funord_app :
  forall (O1 O2:ord)(A:Type)(f:O1-m->A-o->O2)(x:A)(y:O1), (f <_o> x) y = f y x.
trivial.
Qed.

Lemma funord_app_rel :
  forall (A:Type)(O1 O2:ord)(f g:O1-m->A-o->O2)(x:A), f <= g
    -> f <_o> x <= g <_o> x.
intros A O1 O2 f g x Hfg.
simpl.
unfold rel_monofunord.
intro y.
simpl.
apply Hfg.
Qed.

Definition monofunord_app (O1 O2 O3:ord)(f:O1-m->O2-m->O3)(x:O2) : O1-m->O3.
intros.
exists (fun y:O1 => f y x).
unfold monotonic.
intros y1 y2 Hy.
assert (Hf:f y1 <= f y2).
apply monofun_law.
exact Hy.
apply Hf.
Defined.

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

Lemma simpl_monofunord_app :
  forall (O1 O2 O3:ord)(f:O1-m->O2-m->O3)(x:O2)(y:O1), (f <_m> x) y = f y x.
simpl.
trivial.
Qed.

Lemma monofunord_app_rel :
  forall (O1 O2 O3:ord)(f g:O1-m->O2-m->O3)(x1 x2:O2), f <= g -> x1 <= x2
    -> f <_m> x1 <= g <_m> x2.
intros O1 O2 O3 f g x1 x2 Hfg Hx.
simpl.
unfold rel_monofunord.
intro y.
simpl.
apply order_trans_law with (f y x2).
apply (monofun_law (f y)); apply Hx.
apply Hfg.
Qed.

Definition monofunord_id (O:ord) : O-m->O.
intro.
exists (fun x:O => x).
red.
firstorder.
Defined.

Lemma simpl_monofunord_id : forall (O:ord)(x:O), monofunord_id O x = x.
trivial.
Qed.

Definition monofunord_composition
  (O1 O2 O3:ord)(f:O1-m->O2)(g:O2-m->O3) : O1-m->O3.
intros O1 O2 O3 f g.
exists (fun n => g (f n)).
red.
intros x y Hxy.
apply (monofun_law g).
apply (monofun_law f).
apply Hxy.
Defined.

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

Lemma simpl_monofunord_composition : forall (O1 O2 O3:ord)(f:O1-m->O2)(g:O2-m->O3)(x:O1),
  (g @ f) x = g (f x).
simpl.
trivial.
Qed.

Lemma monofunord_composition_assoc : forall (O1 O2 O3 O4:ord)(f:O1-m->O2)(g:O2-m->O3)(h:O3-m->O4),
  h@(g@f) = (h@g)@f.
trivial.
Qed.

Lemma monofunord_composition_rel : forall (O1 O2 O3:ord)(f f':O1-m->O2)(g g':O2-m->O3),
  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 auto.
replace ((g'@f') x) with (g' (f' x)) by auto.
apply order_trans_law with (g (f' x)).
apply monofun_law; apply Hf.
apply Hg.
Qed.

Lemma simpl_monofunord_id_left : forall (O1 O2:ord)(f:O1-m->O2)(x:O1),
  (monofunord_id O2 @ f) x = f x.
trivial.
Qed.

Lemma simpl_monofunord_id_right : forall (O1 O2:ord)(f:O1-m->O2)(x:O1),
  (f @ monofunord_id O1) x = f x.
trivial.
Qed.

Lemma monofunord_id_left : forall (O1 O2:ord)(f:O1-m->O2),
  monofunord_id O2 @ f == f.
intros.
split;
  simpl; unfold rel_monofunord; intro x; apply eq_rel_ord;
  [ | apply sym_eq]; apply simpl_monofunord_id_left.
Qed.

Lemma monofunord_id_right : forall (O1 O2:ord)(f:O1-m->O2),
  f @ monofunord_id O1 == f.
intros.
split;
  simpl; unfold rel_monofunord; intro x; apply eq_rel_ord;
  [ | apply sym_eq]; apply simpl_monofunord_id_right.
Qed.

Definition monofunord_swap (O1 O2 O3:ord)(f:O1-m->O2-m->O3) : O2-m->O1-m->O3.
intros.
exists (fun x => f <_m> x).
unfold monotonic.
intros x y Hxy z.
simpl.
exact (monofun_law (f z) Hxy).
Defined.

Definition monofunord_app2 (O1 O2 O3 O4:ord)(f:O1-m->O3-m->O4)(g:O2-m->O3) :
  O2 -m-> (O1 -m-> O4) := (monofunord_swap f) @ g.

Definition monofunord_diag (O1 O2:ord)(f:O1-m->(O1-m->O2)) : O1-m->O2.
intros.
exists (fun x => f x x).
unfold monotonic.
intros x y Hxy.
apply order_trans_law with (f x y).
exact (monofun_law (f x) Hxy).
assert (f x <= f y) by exact (monofun_law f Hxy).
trivial.
Defined.

(*
Definition monofun_const (O1 O2:ord)(k:O2) : O1-m->O2.
intros.
exists (fun x:O1 => k).
unfold monotonic.
intros.
apply order_refl_law.
Qed.
*)