# Ccpo.v: Specification and properties of a cpo

Require Export Arith.
Require Export Omega.

Require Export Coq.Classes.SetoidTactics.
Require Export Coq.Classes.SetoidClass.
Require Export Coq.Classes.Morphisms.

Open Local Scope signature_scope.

## Ordered type

Definition eq_rel {A} (E1 E2:relation A) := forall x y, E1 x y <-> E2 x y.

Class Order {A} (E:relation A) (R:relation A) :=
{reflexive :> Reflexive R;
order_eq : forall x y, R x y /\ R y x <-> E x y;
transitive :> Transitive R }.

Instance OrderEqRefl `{Order A E R} : Reflexive E.
Save.

Instance OrderEqSym `{Order A E R} : Symmetric E.
Save.

Instance OrderEqTrans `{Order A E R} : Transitive E.
Save.

Instance OrderEquiv `{Order A E R} : Equivalence E.
Save.
Opaque OrderEquiv.

Class ord A :=
{ Oeq : relation A;
Ole : relation A;
order_rel :> Order Oeq Ole }.

Lemma OrdSetoid `(o:ord A) : Setoid A.

Add Parametric Relation {A} {o:ord A} : A (@Oeq _ o)
reflexivity proved by OrderEqRefl
symmetry proved by OrderEqSym
transitivity proved by OrderEqTrans
as Oeq_setoid.

Infix " ≤ " := Ole.
Infix " ≈ " := Oeq : type_scope.

Definition Oge {O} {o:ord O} := fun (x y:O) => y x.
Infix ">=" := Oge.

Lemma Ole_refl_eq : forall {O} {o:ord O} (x y:O), x y -> x y.

Hint Immediate @Ole_refl_eq.

Lemma Ole_refl_eq_inv : forall {O} {o:ord O} (x y:O), x y -> y x.

Hint Immediate @Ole_refl_eq_inv.

Lemma Ole_trans : forall {O} {o:ord O} (x y z:O), x y -> y z -> x z.

Lemma Ole_refl : forall {O} {o:ord O} (x:O), x x.

Hint Resolve @Ole_refl.

Add Parametric Relation {A} {o:ord A} : A (@Ole _ o)
reflexivity proved by Ole_refl
transitivity proved by Ole_trans
as Ole_setoid.

Lemma Ole_antisym : forall {O} {o:ord O} (x y:O), x y -> y x -> x y.
Hint Immediate @Ole_antisym.

Lemma Oeq_refl : forall {O} {o:ord O} (x:O), x x.
Hint Resolve @Oeq_refl.

Lemma Oeq_refl_eq : forall {O} {o:ord O} (x y:O), x = y -> x y.
Hint Resolve @Oeq_refl_eq.

Lemma Oeq_sym : forall {O} {o:ord O} (x y:O), x y -> y x.

Lemma Oeq_le : forall {O} {o:ord O} (x y:O), x y -> x y.

Lemma Oeq_le_sym : forall {O} {o:ord O} (x y:O), x y -> y x.

Hint Resolve @Oeq_le.
Hint Immediate @Oeq_sym @Oeq_le_sym.

Lemma Oeq_trans
: forall {O} {o:ord O} (x y z:O), x y -> y z -> x z.
Hint Resolve @Oeq_trans.

Add Parametric Morphism `(o:ord A): (Ole (ord:=o))
with signature (Oeq (A:=A) ==> Oeq (A:=A) ==> iff) as Ole_eq_compat_iff.
Save.

Equivalence of orders

Definition eq_ord {O} (o1 o2:ord O) := eq_rel (Ole (ord:=o1)) (Ole (ord:=o2)).

Lemma eq_ord_equiv : forall {O} (o1 o2:ord O), eq_ord o1 o2 ->
eq_rel (Oeq (ord:=o1)) (Oeq (ord:=o2)).

Lemma Ole_eq_compat :
forall {O} {o:ord O} (x1 x2 : O),
x1 x2 -> forall x3 x4 : O, x3 x4 -> x1 x3 -> x2 x4.

Lemma Ole_eq_right : forall {O} {o:ord O} (x y z: O),
x y -> y z -> x z.

Lemma Ole_eq_left : forall {O} {o:ord O} (x y z: O),
x y -> y z -> x z.

Add Parametric Morphism `{o:ord A} : (Oeq (A:=A))
with signature Oeq Oeq iff as Oeq_iff_morphism.
Qed.

Add Parametric Morphism `{o:ord A} : (Ole (A:=A))
with signature Oeq Oeq iff as Ole_iff_morphism.
Qed.

Add Parametric Morphism `{o:ord A} : (Ole (A:=A))
with signature Ole --> Ole Basics.impl as Ole_impl_morphism.
Qed.

## Definition and properties of x<y

Definition Olt `{o:ord A} (r1 r2:A) : Prop := (r1 r2) /\ ~ (r1 r2).

Infix "<" := Olt.

Lemma Olt_eq_compat `{o:ord A} :
forall x1 x2 : A, x1 x2 -> forall x3 x4 : A, x3 x4 -> x1 < x3 -> x2 < x4.

Add Parametric Morphism `{o:ord A} : (Olt (A:=A))
with signature Oeq Oeq iff as Olt_iff_morphism.
Save.

Lemma Olt_neq `{o:ord A} : forall x y:A, x < y -> ~ x y.

Lemma Olt_neq_rev `{o:ord A} : forall x y:A, x < y -> ~ y x.

Lemma Olt_le `{o:ord A} : forall x y, x < y -> x y.

Lemma Olt_notle `{o:ord A} : forall x y, x < y -> ~ y x.

Lemma Olt_trans `{o:ord A} : forall x y z:A, x < y -> y < z -> x < z.

Lemma Ole_diff_lt `{o:ord A} : forall x y : A, x y -> ~ x y -> x < y.

Hint Immediate @Olt_neq @Olt_neq_rev @Olt_le @Olt_notle.
Hint Resolve @Ole_diff_lt.

Lemma Olt_antirefl `{o:ord A} : forall x:A, ~ x < x.

Lemma Ole_lt_trans `{o:ord A} : forall x y z:A, x y -> y < z -> x < z.

Lemma Olt_le_trans `{o:ord A} : forall x y z:A, x < y -> y z -> x < z.

Hint Resolve @Olt_antirefl.

Lemma Ole_not_lt `{o:ord A} : forall x y:A, x y -> ~ y < x.
Hint Resolve @Ole_not_lt.

Add Parametric Morphism `{o:ord A} : (Olt (A:=A))
with signature Ole --> Ole Basics.impl as Olt_le_compat.
Qed.

### Dual order

• Iord x y = y x
Definition Iord : forall O {o:ord O}, ord O.
Defined.

Implicit Arguments Iord [[o]].

### Order on functions

Definition fun_ext A B (R:relation B) : relation (A -> B) :=
fun f g => forall x, R (f x) (g x).
Implicit Arguments fun_ext [B].

• ford f g := forall x, f x g x
Instance ford A O {o:ord O} : ord (A -> O) :=
{Oeq:=fun_ext A (Oeq (A:=O));Ole:=fun_ext A (Ole (A:=O))}.
Defined.

Lemma ford_le_elim : forall A O (o:ord O) (f g:A -> O), f g -> forall n, f n g n.
Hint Immediate ford_le_elim.

Lemma ford_le_intro : forall A O (o:ord O) (f g:A -> O), ( forall n, f n g n ) -> f g.
Hint Resolve ford_le_intro.

Lemma ford_eq_elim : forall A O (o:ord O) (f g:A -> O), f g -> forall n, f n g n.
Hint Immediate ford_eq_elim.

Lemma ford_eq_intro : forall A O (o:ord O) (f g:A -> O), ( forall n, f n g n ) -> f g.
Hint Resolve ford_eq_intro.

## Monotonicity

### Definition and properties

Class monotonic `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob) :=
monotonic_def : forall x y, x y -> f x f y.

Lemma monotonic_intro : forall `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob),
(forall x y, x y -> f x f y) -> monotonic f.
Hint Resolve @monotonic_intro.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob) {m:monotonic f} : f
with signature (Ole (A:=Oa) Ole (A:=Ob))
as monotonic_morphism.
Save.

Class stable `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob) :=
stable_def : forall x y, x y -> f x f y.
Hint Unfold stable.

Lemma stable_intro : forall `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob),
(forall x y, x y -> f x f y) -> stable f.
Hint Resolve @stable_intro.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob) {s:stable f} : f
with signature (Oeq (A:=Oa) Oeq (A:=Ob))
as stable_morphism.
Save.

Typeclasses Opaque monotonic stable.

Instance monotonic_stable `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob) {m:monotonic f}
: stable f.
Save.

### Type of monotonic functions

Record fmon `{o1:ord Oa} `{o2:ord Ob}:= mon
{fmont :> Oa -> Ob;
fmonotonic: monotonic fmont}.

Implicit Arguments mon [[Oa] [o1] [Ob] [o2] [fmonotonic]].
Implicit Arguments fmon [[o1] [o2]].

Hint Resolve @fmonotonic.

Notation "Oa -m> Ob" := (fmon Oa Ob)
(right associativity, at level 30) : O_scope.
Notation "Oa --m> Ob" := (fmon Oa (o1:=Iord Oa) Ob )
(right associativity, at level 30) : O_scope.
Notation "Oa --m-> Ob" := (fmon Oa (o1:=Iord Oa) Ob (o2:=Iord Ob))
(right associativity, at level 30) : O_scope.
Notation "Oa -m-> Ob" := (fmon Oa Ob (o2:=Iord Ob))
(right associativity, at level 30) : O_scope.

Open Scope O_scope.

Lemma mon_simpl : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob){mf: monotonic f} x,
mon f x = f x.
Hint Resolve @mon_simpl.

Instance fstable `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> Ob) : stable f.
Save.

Hint Resolve @fstable.

Lemma fmon_le : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> Ob) x y,
x y -> f x f y.
Hint Resolve @fmon_le.

Lemma fmon_eq : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> Ob) x y,
x y -> f x f y.
Hint Resolve @fmon_eq.

Instance fmono Oa Ob {o1:ord Oa} {o2:ord Ob} : ord (Oa -m> Ob)
:= {Oeq := fun (f g : Oa-m> Ob)=> forall x, f x g x;
Ole := fun (f g : Oa-m> Ob)=> forall x, f x g x}.
Defined.

Lemma mon_le_compat : forall `{o1:ord Oa} `{o2:ord Ob} (f g:Oa -> Ob)
{mf:monotonic f} {mg:monotonic g}, f g -> mon f mon g.
Hint Resolve @ mon_le_compat.

Lemma mon_eq_compat : forall `{o1:ord Oa} `{o2:ord Ob} (f g:Oa-> Ob)
{mf:monotonic f} {mg:monotonic g}, f g -> mon f mon g.
Hint Resolve @ mon_eq_compat.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob}
: (fmont (Oa:=Oa) (Ob:=Ob))
with signature Oeq Oeq Oeq as fmont_eq_morphism.
Qed.

### Monotonicity and dual order

Lemma Imonotonic `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob) {m:monotonic f}
: monotonic (o1:=Iord Oa) (o2:=Iord Ob) f.

Hint Extern 2 (@monotonic _ (Iord _) _ (Iord _) _) => apply @Imonotonic
: typeclass_instances.

Definition imon `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob) {m:monotonic f}
: Oa --m-> Ob := mon (o1:=Iord Oa) (o2:=Iord Ob) f.

Lemma imon_simpl : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob) {m:monotonic f} (x:Oa),
imon f x = f x.

• Iord (A -> U) corresponds to A -> Iord U

Lemma Iord_app {A} `{o1:ord Oa} (x: A) : ((A -> Oa) --m-> Oa).

• Imon f uses f as monotonic function over the dual order.

Definition Imon : forall `{o1:ord Oa} `{o2:ord Ob}, (Oa -m> Ob) -> (Oa --m-> Ob).
Defined.

Lemma Imon_simpl : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> Ob)(x:Oa),
Imon f x = f x.

### Monotonicity and equality

Lemma mon_fun_eq_monotonic
: forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob) (g:Oa -m> Ob),
f g -> monotonic f.

Definition mon_fun_subst `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob) (g:Oa -m> Ob) (H:f g)
: Oa -m> Ob := mon f (fmonotonic:= mon_fun_eq_monotonic _ _ H).

Lemma mon_fun_eq
: forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -> Ob) (g:Oa -m> Ob)
(H:f g), g mon_fun_subst f g H.

### Monotonic functions with 2 arguments

Class monotonic2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc) :=
monotonic2_intro : forall (x y:Oa) (z t:Ob), x y -> z t -> f x z f y t.

Instance mon2_intro `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc)
{m1:monotonic f} {m2: forall x, monotonic (f x)} : monotonic2 f | 10.
Save.

Lemma mon2_elim1 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc)
{m:monotonic2 f} : monotonic f.

Lemma mon2_elim2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc)
{m:monotonic2 f} : forall x, monotonic (f x).
Hint Immediate @mon2_elim1 @mon2_elim2: typeclass_instances.

Definition mon_comp {A} `{o1: ord Oa} `{o2: ord Ob}
(f:A -> Oa -> Ob) {mf:forall x, monotonic (f x)} : A -> Oa -m> Ob
:= fun x => mon (f x).

Instance mon_fun_mon `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc)
{m:monotonic2 f} : monotonic (fun x => mon (f x)).
Save.

Class stable2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc) :=
stable2_intro : forall (x y:Oa) (z t:Ob), xy -> z t -> f x z f y t.

Instance monotonic2_stable2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -> Ob -> Oc) {m:monotonic2 f} : stable2 f.
Save.

Typeclasses Opaque monotonic2 stable2.

Definition mon2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc)
{mf:monotonic2 f} : Oa -m> Ob -m> Oc := mon (fun x => mon (f x)).

Lemma mon2_simpl : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -> Oc)
{mf:monotonic2 f} x y, mon2 f x y = f x y.
Hint Resolve @mon2_simpl.

Lemma mon2_le_compat : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f g:Oa -> Ob -> Oc) {mf: monotonic2 f} {mg:monotonic2 g},
f g -> mon2 f mon2 g.

Definition fun2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -m> Oc)
: Oa -> Ob -> Oc := fun x => f x.

Instance fmon2_mon `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc} (f:Oa -> Ob -m> Oc) :
forall x:Oa, monotonic (fun2 f x).
Save.

Instance fun2_monotonic `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -> Ob -m> Oc) {mf:monotonic f} : monotonic (fun2 f).
Save.
Hint Resolve @fun2_monotonic.

Instance fmonotonic2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> Ob -m> Oc)
: monotonic2 (fun2 f).
Save.
Hint Resolve @fmonotonic2.

Definition mfun2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> Ob -m> Oc)
: Oa-m> (Ob -> Oc) := mon (fun2 f).

Lemma mfun2_simpl : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> Ob -m> Oc) x y,
mfun2 f x y = f x y.

Instance mfun2_mon `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f:Oa -m> Ob -m> Oc) x : monotonic (mfun2 f x).
Save.

Lemma mon2_fun2 : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -m> Ob -m> Oc), mon2 (fun2 f) f.

Lemma fun2_mon2 : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -> Ob -> Oc) {mf:monotonic2 f} , fun2 (mon2 f) f.
Hint Resolve @mon2_fun2 @fun2_mon2.

Instance fstable2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> Ob -m> Oc)
: stable2 (fun2 f).
Save.
Hint Resolve @fstable2.

Definition Imon2 : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc},
(Oa -m> Ob -m> Oc) -> (Oa --m> Ob --m-> Oc).
Defined.

Lemma Imon2_simpl : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -m> Ob -m> Oc) (x:Oa) (y: Ob),
Imon2 f x y = f x y.

Lemma Imonotonic2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -> Ob -> Oc){mf : monotonic2 f}
: monotonic2 (o1:=Iord Oa) (o2:=Iord Ob) (o3:=Iord Oc) f.

Hint Extern 2 (@monotonic2 _ (Iord _) _ (Iord _) _ (Iord _) _) => apply @Imonotonic2
: typeclass_instances.

Definition imon2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -> Ob -> Oc){mf : monotonic2 f} : Oa --m> Ob --m-> Oc :=
mon2 (o1:=Iord Oa) (o2:=Iord Ob) (o3:=Iord Oc) f.

Lemma imon2_simpl : forall `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
(f:Oa -> Ob -> Oc){mf : monotonic2 f} (x:Oa) (y:Ob),
imon2 f x y = f x y.

### Strict monotonicity

Lemma inj_strict_mon : forall `{o1: ord Oa} `{o2: ord Ob} (f:Oa -> Ob) {mf:monotonic f},
(forall x y, f x f y -> x y) -> forall x y, x < y -> f x < f y.

## Sequences

### Usual order on natural numbers

Instance natO : ord nat :=
{ Oeq := fun n m : nat => n = m;
Ole := fun n m : nat => (n m)%nat}.
Defined.

Lemma le_Ole : forall n m, ((n m)%nat)-> n m.
Hint Resolve le_Ole.

Lemma nat_monotonic : forall {O} {o:ord O}
(f:nat -> O), (forall n, f n f (S n)) -> monotonic f.
Hint Resolve @nat_monotonic.

Lemma nat_monotonic_inv : forall {O} {o:ord O}
(f:nat -> O), (forall n, f (S n) f n) -> monotonic (o2:=Iord O) f.
Hint Resolve @nat_monotonic_inv.

Definition fnatO_intro : forall {O} {o:ord O} (f:nat -> O), (forall n, f n f (S n)) -> nat -m> O.
Defined.

Lemma fnatO_elim : forall {O} {o:ord O} (f:nat -m> O) (n:nat), f n f (S n).
Hint Resolve @fnatO_elim.

• (mseq_lift_left f n) k = f (n+k)

Definition seq_lift_left {O} (f:nat -> O) n := fun k => f (n+k)%nat.

Instance mon_seq_lift_left
: forall n {O} {o:ord O} (f:nat -> O) {m:monotonic f}, monotonic (seq_lift_left f n).
Save.

Definition mseq_lift_left : forall {O} {o:ord O} (f:nat -m> O) (n:nat), nat -m> O.
Defined.

Lemma mseq_lift_left_simpl : forall {O} {o:ord O} (f:nat -m> O) (n k:nat),
mseq_lift_left f n k = f (n+k)%nat.

Lemma mseq_lift_left_le_compat : forall {O} {o:ord O} (f g:nat -m> O) (n:nat),
f g -> mseq_lift_left f n mseq_lift_left g n.
Hint Resolve @mseq_lift_left_le_compat.

Add Parametric Morphism {O} {o:ord O} : (@mseq_lift_left _ o)
with signature Oeq eq Oeq
as mseq_lift_left_eq_compat.
Save.
Hint Resolve @mseq_lift_left_eq_compat.

Add Parametric Morphism {O} {o:ord O}: (@seq_lift_left O)
with signature Oeq eq Oeq
as seq_lift_left_eq_compat.
Save.
Hint Resolve @seq_lift_left_eq_compat.

• (mseq_lift_right f n) k = f (k+n)

Definition seq_lift_right {O} (f:nat -> O) n := fun k => f (k+n)%nat.

Instance mon_seq_lift_right
: forall n {O} {o:ord O} (f:nat -> O) {m:monotonic f}, monotonic (seq_lift_right f n).
Save.

Definition mseq_lift_right : forall {O} {o:ord O} (f:nat -m> O) (n:nat), nat -m> O.
Defined.

Lemma mseq_lift_right_simpl : forall {O} {o:ord O} (f:nat -m> O) (n k:nat),
mseq_lift_right f n k = f (k+n)%nat.

Lemma mseq_lift_right_le_compat : forall {O} {o:ord O} (f g:nat -m> O) (n:nat),
f g -> mseq_lift_right f n mseq_lift_right g n.
Hint Resolve @mseq_lift_right_le_compat.

Add Parametric Morphism {O} {o:ord O} : (mseq_lift_right (o:=o))
with signature Oeq eq Oeq
as mseq_lift_right_eq_compat.
Save.

Add Parametric Morphism {O} {o:ord O}: (@seq_lift_right O)
with signature Oeq eq Oeq
as seq_lift_right_eq_compat.
Save.
Hint Resolve @seq_lift_right_eq_compat.

Lemma mseq_lift_right_left : forall {O} {o:ord O} (f:nat -m> O) n,
mseq_lift_left f n mseq_lift_right f n.

### Monotonicity and functions

• (shift f x) n = f n x

Instance shift_mon_fun {A} `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> (A -> Ob)) :
forall x:A, monotonic (fun (y:Oa) => f y x).
Save.

Definition shift {A} `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> (A -> Ob)) : A -> Oa -m> Ob
:= fun x => (mon (fun y => f y x)).

Infix " ◊" := shift (at level 30, no associativity) : O_scope.

Lemma shift_simpl : forall {A} `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> (A -> Ob)) x y,
(f <o> x) y = f y x.

Lemma shift_le_compat : forall {A} `{o1:ord Oa} `{o2:ord Ob} (f g:Oa -m> (A -> Ob)),
f g -> shift f shift g.
Hint Resolve @shift_le_compat.

Add Parametric Morphism {A} `{o1:ord Oa} `{o2:ord Ob}
: (shift (A:=A) (Oa:=Oa) (Ob:=Ob)) with signature Oeq eq Oeq
as shift_eq_compat.
Save.

Instance ishift_mon {A} `{o1:ord Oa} `{o2:ord Ob} (f:A -> (Oa -m> Ob)) :
monotonic (fun (y:Oa) (x:A) => f x y).
Save.

Definition ishift {A} `{o1:ord Oa} `{o2:ord Ob} (f:A -> (Oa -m> Ob)) : Oa -m> (A -> Ob)
:= mon (fun (y:Oa) (x:A) => f x y) (fmonotonic:=ishift_mon f).

Lemma ishift_simpl : forall {A} `{o1:ord Oa} `{o2:ord Ob} (f:A -> (Oa -m> Ob)) x y,
ishift f x y = f y x.

Lemma ishift_le_compat : forall {A} `{o1:ord Oa} `{o2:ord Ob} (f g:A -> (Oa -m> Ob)),
f g -> ishift f ishift g.
Hint Resolve @ishift_le_compat.

Add Parametric Morphism {A} `{o1:ord Oa} `{o2:ord Ob}
: (ishift (A:=A) (Oa:=Oa) (Ob:=Ob)) with signature Oeq eq Oeq
as ishift_eq_compat.
Save.

Instance shift_fun_mon `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> (Ob -> Oc))
{m:forall x, monotonic (f x)} : monotonic (shift f).
Save.

Instance shift_mon2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> Ob -m> Oc)
: monotonic2 (fun x y => f y x).
Save.
Hint Resolve @shift_mon_fun @shift_fun_mon @shift_mon2.

Definition mshift `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m> Ob -m> Oc)
: Ob -m> Oa -m> Oc := mon2 (fun x y => f y x).

• id c = c

Definition id O {o:ord O} : O -> O := fun x => x.

Instance mon_id : forall {O:Type} {o:ord O}, monotonic (id O).
Save.

• (cte c) n = c

Definition cte A `{o1:ord Oa} (c:Oa) : A -> Oa := fun x => c.

Instance mon_cte : forall `{o1:ord Oa} `{o2:ord Ob} (c:Ob), monotonic (cte Oa c).
Save.

Definition mseq_cte {O} {o:ord O} (c:O) : nat -m> O := mon (cte nat c).

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} : (@cte Oa Ob _)
with signature Ole Ole as cte_le_compat.
Save.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} : (@cte Oa Ob _)
with signature Oeq Oeq as cte_eq_compat.
Save.

Instance mon_diag `{o1:ord Oa} `{o2:ord Ob}(f:Oa -m> (Oa -m> Ob))
: monotonic (fun x => f x x).
Save.
Hint Resolve @mon_diag.

Definition diag `{o1:ord Oa} `{o2:ord Ob}(f:Oa -m> (Oa -m> Ob)) : Oa-m> Ob
:= mon (fun x => f x x).

Lemma fmon_diag_simpl : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m> (Oa -m> Ob)) (x:Oa),
diag f x = f x x.

Lemma diag_le_compat : forall `{o1:ord Oa} `{o2:ord Ob} (f g:Oa -m> (Oa -m> Ob)),
f g -> diag f diag g.
Hint Resolve @diag_le_compat.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} : (diag (Oa:=Oa) (Ob:=Ob))
with signature Oeq Oeq as diag_eq_compat.
Save.

Lemma diag_shift : forall `{o1:ord Oa} `{o2:ord Ob} (f: Oa -m> Oa -m> Ob),
diag f diag (mshift f).

Hint Resolve @diag_shift.

Lemma mshift_simpl : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(h:Oa -m> Ob -m> Oc) (x : Ob) (y:Oa), mshift h x y = h y x.

Lemma mshift_le_compat : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f g:Oa -m> Ob -m> Oc), f g -> mshift f mshift g.
Hint Resolve @mshift_le_compat.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} : (@mshift Oa _ Ob _ Oc _)
with signature Oeq Oeq as mshift_eq_compat.
Save.

Lemma mshift2_eq : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (h : Oa -m> Ob -m> Oc),
mshift (mshift h) h.

• (f@g) x = f (g x)

Instance monotonic_comp `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f:Ob -> Oc){mf : monotonic f} (g:Oa -> Ob){mg:monotonic g} : monotonic (fun x => f (g x)).
Save.
Hint Resolve @monotonic_comp.

Instance monotonic_comp_mon `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f:Ob -m> Oc)(g:Oa -m> Ob) : monotonic (fun x => f (g x)).
Save.
Hint Resolve @monotonic_comp_mon.

Definition comp `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Ob -m> Oc) (g:Oa -m> Ob)
: Oa -m> Oc := mon (fun x => f (g x)).

Infix "@" := comp (at level 35) : O_scope.

Lemma comp_simpl : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f:Ob -m> Oc) (g:Oa -m> Ob) (x:Oa), (f@g) x = f (g x).

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}: (@comp Oa _ Ob _ Oc _)
with signature Ole ++> Ole ++> Ole
as comp_le_compat.
Save.

Hint Immediate @comp_le_compat.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} : (@comp Oa _ Ob _ Oc _)
with signature Oeq Oeq Oeq
as comp_eq_compat.
Save.

Hint Immediate @comp_eq_compat.

• (f@2 g) h x = f (g x) (h x)

Instance mon_app2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}
(f:Ob -> Oc -> Od) (g:Oa -> Ob) (h:Oa -> Oc)
{mf:monotonic2 f}{mg:monotonic g} {mh:monotonic h}
: monotonic (fun x => f (g x) (h x)).
Save.

Instance mon_app2_mon `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}
(f:Ob -m> Oc -m> Od) (g:Oa -m> Ob) (h:Oa -m> Oc)
: monotonic (fun x => f (g x) (h x)).
Save.

Definition app2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}
(f:Ob -m> Oc -m> Od) (g:Oa -m> Ob) (h:Oa -m> Oc) : Oa -m> Od
:= mon (fun x => f (g x) (h x)).

Infix "@²" := app2 (at level 70) : O_scope.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}:
(@app2 Oa _ Ob _ Oc _ Od _)
with signature Ole ++> Ole ++> Ole ++> Ole
as app2_le_compat.
Save.

Hint Immediate @app2_le_compat.

Add Parametric Morphism `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}:
(@app2 Oa _ Ob _ Oc _ Od _)
with signature Oeq Oeq Oeq Oeq
as app2_eq_compat.
Save.

Hint Immediate @app2_eq_compat.

Lemma app2_simpl :
forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}
(f:Ob -m> Oc -m> Od) (g:Oa -m> Ob) (h:Oa -m> Oc) (x:Oa),
(f@2 g) h x = f (g x) (h x).

Lemma comp_monotonic_right :
forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f: Ob -m> Oc) (g1 g2:Oa -m> Ob),
g1 g2 -> f @ g1 f @ g2.
Hint Resolve @comp_monotonic_right.

Lemma comp_monotonic_left :
forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f1 f2: Ob -m> Oc) (g:Oa -m> Ob),
f1 f2 -> f1 @ g f2 @ g.
Hint Resolve @comp_monotonic_left.

Instance comp_monotonic2 : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc},
monotonic2 (@comp Oa _ Ob _ Oc _).
Save.
Hint Resolve @comp_monotonic2.

Definition fcomp `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} :
(Ob -m> Oc) -m> (Oa -m> Ob) -m> (Oa -m> Oc) := mon2 (@comp Oa _ Ob _ Oc _).

Implicit Arguments fcomp [[o1] [o2] [o3]].

Lemma fcomp_simpl : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f:Ob -m> Oc) (g:Oa -m> Ob), fcomp _ _ _ f g = f@g.

Definition fcomp2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od} :
(Oc -m> Od) -m> (Oa -m> Ob -m> Oc) -m> (Oa -m> Ob -m> Od):=
(fcomp Oa (Ob -m> Oc) (Ob -m> Od))@(fcomp Ob Oc Od).

Implicit Arguments fcomp2 [[o1] [o2] [o3] [o4]].

Lemma fcomp2_simpl : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4:ord Od}
(f:Oc -m> Od) (g:Oa -m> Ob -m> Oc) (x:Oa)(y:Ob), fcomp2 _ _ _ _ f g x y = f (g x y).

Lemma fmon_le_compat2 : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(f: Oa -m> Ob -m> Oc) (x y:Oa) (z t:Ob), xy -> z t -> f x z f y t.
Hint Resolve fmon_le_compat2.

Lemma fmon_cte_comp : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
(c:Oc)(f:Oa -m> Ob), (mon (cte Ob c)) @ f mon (cte Oa c).

## Abstract relational notion of lubs

Record islub O (o:ord O) I (f:I -> O) (x:O) : Prop := mk_islub
{ le_islub : forall i, f i x;
islub_le : forall y, (forall i, f i y) -> x y}.
Implicit Arguments islub [O o I].
Implicit Arguments le_islub [O o I f x].
Implicit Arguments islub_le [O o I f x].

Definition isglb O (o:ord O) I (f:I -> O) (x:O) : Prop
:= islub (o:=Iord O) f x.
Implicit Arguments isglb [O o I].

Lemma le_isglb O (o:ord O) I (f:I -> O) (x:O) :
isglb f x -> forall i, x f i.

Lemma isglb_le O (o:ord O) I (f:I -> O) (x:O) :
isglb f x -> forall y, (forall i, y f i) -> y x.
Implicit Arguments le_isglb [O o I f x].
Implicit Arguments isglb_le [O o I f x].

Lemma mk_isglb O (o:ord O) I (f:I -> O) (x:O) :
(forall i, x f i) -> (forall y, (forall i, y f i) -> y x)
-> isglb f x.

Lemma islub_eq_compat O (o:ord O) I (f g:I -> O) (x y:O):
fg -> x y -> islub f x -> islub g y.

Lemma islub_eq_compat_left O (o:ord O) I (f g:I -> O) (x:O):
fg -> islub f x -> islub g x.

Lemma islub_eq_compat_right O (o:ord O) I (f:I -> O) (x y:O):
x y -> islub f x -> islub f y.

Lemma isglb_eq_compat O (o:ord O) I (f g:I -> O) (x y:O):
fg -> x y -> isglb f x -> isglb g y.

Lemma isglb_eq_compat_left O (o:ord O) I (f g:I -> O) (x:O):
fg -> isglb f x -> isglb g x.

Lemma isglb_eq_compat_right O (o:ord O) I (f:I -> O) (x y:O):
x y -> isglb f x -> isglb f y.

Add Parametric Morphism {O} {o:ord O} I : (@islub _ o I)
with signature Oeq Oeq iff
as islub_morphism.
Save.

Add Parametric Morphism {O} {o:ord O} I : (@isglb _ o I)
with signature Oeq Oeq iff
as isglb_morphism.
Save.

Add Parametric Morphism {O} {o:ord O} I : (@islub _ o I)
with signature (@pointwise_relation I O (@Oeq _ _)) Oeq iff
as islub_morphism_ext.
Save.

Add Parametric Morphism {O} {o:ord O} I : (@isglb _ o I)
with signature (@pointwise_relation I O (@Oeq _ _)) Oeq iff
as isglb_morphism_ext.
Save.

Lemma islub_incr_ext {O} {o:ord O} (f :nat -> O) (x:O) (n:nat):
(forall k, f k f (S k)) -> islub f x -> islub (fun k => f (n + k)) x.

Lemma islub_incr_lift {O} {o:ord O} (f :nat -> O) (x:O) (n:nat):
(forall k, f k f (S k)) -> islub (fun k => f (n + k)) x -> islub f x.

Lemma isglb_decr_ext {O} {o:ord O} (f :nat -> O) (x:O) (n:nat):
(forall k, f (S k) f k) -> isglb f x -> isglb (fun k => f (n + k)) x.

Lemma isglb_decr_lift {O} {o:ord O} (f :nat -> O) (x:O) (n:nat):
(forall k, f (S k) f k) -> isglb (fun k => f (n + k)) x -> isglb f x.

Hint Resolve islub_incr_ext isglb_decr_ext.

Lemma islub_exch {O} {o:ord O} (F :nat -> nat -> O) (f g : nat -> O)(x:O) :
(forall m, islub (fun n => F n m) (f m))
-> (forall n, islub (F n) (g n)) -> islub f x -> islub g x.

Lemma islub_decr {O} {o:ord O} {I} (f g : I -> O) (x y : O) :
(f g) -> islub f x -> islub g y -> x y.

Lemma islub_unique_eq {O} {o:ord O} {I} (f g : I -> O) (x y : O) :
(f g) -> islub f x -> islub g y -> x y.

Lemma islub_unique {O} {o:ord O} {I} (f : I -> O) (x y : O) :
islub f x -> islub f y -> x y.

Lemma islub_fun_intro O (o:ord O) {I A} (F : I -> A -> O) (f : A -> O) :
(forall x, islub (fun i => F i x) (f x)) -> islub F f.

## Basic operators of omega-cpos

• Constant : 0
• lub : limit of monotonic sequences

### Definition of cpos

Class cpo `{o:ord D} : Type := mk_cpo
{D0 : D; lub: forall (f:nat -m> D), D;
Dbot : forall x:D, D0 x;
le_lub : forall (f : nat -m> D) (n:nat), f n lub f;
lub_le : forall (f : nat -m> D) (x:D), (forall n, f n x) -> lub f x}.

Implicit Arguments cpo [[o]].

Notation "0" := D0 : O_scope.

Hint Resolve @Dbot @le_lub @lub_le.

Definition mon_ord_equiv : forall `{o:ord D1} `{o1:ord D2} {o2:ord D2},
eq_ord o1 o2 -> fmon D1 D2 (o2:=o2) -> fmon D1 D2 (o2:=o1).
Defined.

Lemma mon_ord_equiv_simpl : forall `{o:ord D1} `{o1:ord D2} {o2:ord D2}
(H:eq_ord o1 o2) (f:fmon D1 D2 (o2:=o2)) (x:D1),
mon_ord_equiv H f x = f x.

Definition cpo_ord_equiv `{o1:ord D} (o2:ord D)
: eq_ord o1 o2 -> cpo (o:=o1) D -> cpo (o:=o2) D.
Defined.

### Least upper bounds

Add Parametric Morphism `{c:cpo D} : (lub (cpo:=c))
with signature Ole ++> Ole as lub_le_compat.
Save.
Hint Resolve @lub_le_compat.

Add Parametric Morphism `{c:cpo D}: (lub (cpo:=c))
with signature Oeq Oeq as lub_eq_compat.
Save.
Hint Resolve @lub_eq_compat.

Notation "'mlub' f" := (lub (mon f)) (at level 60) : O_scope .

Lemma mlub_le_compat : forall `{c:cpo D} (f g:nat -> D) {mf:monotonic f} {mg:monotonic g},
f g -> mlub f mlub g.
Hint Resolve @mlub_le_compat.

Lemma mlub_eq_compat : forall `{c:cpo D} (f g:nat -> D) {mf:monotonic f} {mg:monotonic g},
f g -> mlub f mlub g.
Hint Resolve @mlub_eq_compat.

Lemma le_mlub : forall `{c:cpo D} (f:nat -> D) {m:monotonic f} (n:nat), f n mlub f.

Lemma mlub_le : forall `{c:cpo D}(f:nat -> D) {m:monotonic f}(x:D), (forall n, f n x) -> mlub f x.
Hint Resolve @le_mlub @mlub_le.

Lemma islub_mlub : forall `{c:cpo D}(f:nat -> D) {m:monotonic f},
islub f (mlub f).

Lemma islub_lub : forall `{c:cpo D}(f:nat -m> D),
islub f (lub f).

Hint Resolve @islub_mlub @islub_lub.

Instance lub_mon `{c:cpo D} : monotonic lub.
Save.

Definition Lub `{c:cpo D} : (nat -m> D) -m> D := mon lub.

Instance monotonic_lub_comp {O} {o:ord O} `{c:cpo D} (f:O -> nat -> D){mf:monotonic2 f}:
monotonic (fun x => mlub (f x)).
Save.

Lemma lub_cte : forall `{c:cpo D} (d:D), mlub (cte nat d) d.

Hint Resolve @lub_cte.

Lemma mlub_lift_right : forall `{c:cpo D} (f:nat -m> D) n,
lub f mlub (seq_lift_right f n).
Hint Resolve @mlub_lift_right.

Lemma mlub_lift_left : forall `{c:cpo D} (f:nat -m> D) n,
lub f mlub (seq_lift_left f n).
Hint Resolve @mlub_lift_left.

Lemma lub_lift_right : forall `{c:cpo D} (f:nat -m> D) n,
lub f lub (mseq_lift_right f n).
Hint Resolve @lub_lift_right.

Lemma lub_lift_left : forall `{c:cpo D} (f:nat -m> D) n,
lub f lub (mseq_lift_left f n).
Hint Resolve @lub_lift_left.

Lemma lub_le_lift : forall `{c:cpo D} (f g:nat -m> D)
(n:nat), (forall k, n k -> f k g k) -> lub f lub g.

Lemma lub_eq_lift : forall `{c:cpo D} (f g:nat -m> D) {m:monotonic f} {m':monotonic g}
(n:nat), (forall k, n k -> f k g k) -> lub f lub g.

Lemma lub_seq_eq : forall `{c:cpo D} (f:nat -> D) (g: nat-m> D) (H:f g),
lub g lub (mon_fun_subst f g H).

Lemma lub_Olt : forall `{c:cpo D} (f:nat -m> D) (k:D),
k < lub f -> ~ (forall n, f n k).

• (lub_fun h) x = lub_n (h n x)
Definition lub_fun {A} `{c:cpo D} (h : nat -m> (A -> D)) : A -> D
:= fun x => mlub (h <o> x).

Instance lub_shift_mon {O} {o:ord O} `{c:cpo D} (h : nat -m> (O -m> D))
: monotonic (fun (x:O) => lub (mshift h x)).
Save.
Hint Resolve @lub_shift_mon.

### Functional cpos

Instance fcpo {A: Type} `(c:cpo D) : cpo (A -> D) :=
{D0 := fun x:A => (0:D);
lub := fun f => lub_fun f}.
Defined.

Lemma fcpo_lub_simpl : forall {A} `{c:cpo D} (h:nat -m> (A -> D))(x:A),
(lub h) x = lub (h <o> x).

Lemma lub_ishift : forall {A} `{c:cpo D} (h:A -> (nat -m> D)),
lub (ishift h) fun x => lub (h x).

## Cpo of monotonic functions

Instance fmon_cpo {O} {o:ord O} `{c:cpo D} : cpo (O -m> D) :=
{ D0 := mon (cte O (0:D));
lub := fun h:nat -m> (O -m> D) => mon (fun (x:O) => lub (cpo:=c) (mshift h x))}.
Defined.

Lemma fmon_lub_simpl : forall {O} {o:ord O} `{c:cpo D}
(h:nat -m> (O -m> D))(x:O), (lub h) x = lub (mshift h x).
Hint Resolve @fmon_lub_simpl.

Instance mon_fun_lub : forall {O} {o:ord O} `{c:cpo D}
(h:nat -m> (O -> D)) {mh:forall n, monotonic (h n)}, monotonic (lub h).
Save.

Link between lubs on ordinary functions and monotonic functions

Lemma lub_mon_fcpo : forall {O} {o:ord O} `{c:cpo D} (h:nat -m> (O -m> D)),
lub h mon (lub (mfun2 h)).

Lemma lub_fcpo_mon : forall {O} {o:ord O} `{c:cpo D} (h:nat -m> (O -> D))
{mh:forall x, monotonic (h x)}, lub h lub (mon2 h).

Lemma double_lub_diag : forall `{c:cpo D} (h : nat -m> nat -m> D),
lub (lub h) lub (diag h).
Hint Resolve @double_lub_diag.

Lemma double_lub_shift : forall `{c:cpo D} (h : nat -m> nat -m> D),
lub (lub h) lub (lub (mshift h)).
Hint Resolve @double_lub_shift.

## Continuity

Lemma lub_comp_le :
forall `{c1:cpo D1} `{c2:cpo D2} (f:D1 -m> D2) (h : nat -m> D1),
lub (f @ h) f (lub h).
Hint Resolve @lub_comp_le.

Lemma lub_app2_le : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F:D1 -m> D2 -m> D3) (f : nat -m> D1) (g: nat -m> D2),
lub ((F f) g) F (lub f) (lub g).
Hint Resolve @lub_app2_le.

Class continuous `{c1:cpo D1} `{c2:cpo D2} (f:D1 -m> D2) :=
cont_intro : forall (h : nat -m> D1), f (lub h) lub (f @ h).

Typeclasses Opaque continuous.

Lemma continuous_eq_compat : forall `{c1:cpo D1} `{c2:cpo D2}(f g:D1 -m> D2),
f g -> continuous f -> continuous g.

Add Parametric Morphism `{c1:cpo D1} `{c2:cpo D2} : (@continuous D1 _ _ D2 _ _)
with signature Oeq iff
as continuous_eq_compat_iff.
Save.

Lemma lub_comp_eq :
forall `{c1:cpo D1} `{c2:cpo D2} (f:D1 -m> D2) (h : nat -m> D1),
continuous f -> f (lub h) lub (f @ h).
Hint Resolve @lub_comp_eq.

• mon0 x == 0
Instance cont0 `{c1:cpo D1} `{c2:cpo D2} : continuous (mon (cte D1 (0:D2))).
Save.
Implicit Arguments cont0 [].

• double_app f g n m = f m (g n)
Definition double_app `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} `{o4: ord Od}
(f:Oa -m> Oc -m> Od) (g:Ob -m> Oc)
: Ob -m> (Oa -m> Od) := mon ((mshift f) @ g).

### Continuity

Class continuous2 `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (F:D1 -m> D2 -m> D3) :=
continuous2_intro : forall (f : nat -m> D1) (g :nat -m> D2),
F (lub f) (lub g) lub ((F f) g).

Lemma continuous2_app : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3) {cF:continuous2 F} (k:D1), continuous (F k).

Typeclasses Opaque continuous2.

Lemma continuous2_eq_compat :
forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f g : D1 -m> D2 -m> D3),
f g -> continuous2 f -> continuous2 g.

Lemma continuous2_continuous : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3), continuous2 F -> continuous F.
Hint Immediate @continuous2_continuous.

Lemma continuous2_left : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3) (h:nat -m> D1) (x:D2),
continuous F -> F (lub h) x lub (mshift (F @ h) x).

Lemma continuous2_right : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3) (x:D1)(h:nat -m> D2),
continuous2 F -> F x (lub h) lub (F x @ h).

Lemma continuous_continuous2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3) (cFr: forall k:D1, continuous (F k)) (cF: continuous F),
continuous2 F.

Hint Resolve @continuous2_app @continuous2_continuous @continuous_continuous2.

Lemma lub_app2_eq : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3) {cFr:forall k:D1, continuous (F k)} {cF : continuous F},
forall (f:nat -m> D1) (g:nat -m> D2),
F (lub f) (lub g) lub ((F@2 f) g).

Lemma lub_cont2_app2_eq : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3){cF : continuous2 F},
forall (f:nat -m> D1) (g:nat -m> D2),
F (lub f) (lub g) lub ((F@2 f) g).

Lemma mshift_continuous2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(F : D1 -m> D2 -m> D3), continuous2 F -> continuous2 (mshift F).
Hint Resolve @mshift_continuous2.

Lemma monotonic_sym : forall `{o1:ord D1} `{o2:ord D2} (F : D1 -> D1 -> D2),
(forall x y, F x y F y x) -> (forall k:D1, monotonic (F k)) -> monotonic F.
Hint Immediate @monotonic_sym.

Lemma monotonic2_sym : forall `{o1:ord D1} `{o2:ord D2} (F : D1 -> D1 -> D2),
(forall x y, F x y F y x) -> (forall k:D1, monotonic (F k)) -> monotonic2 F.
Hint Immediate @monotonic2_sym.

Lemma continuous_sym : forall `{c1:cpo D1} `{c2:cpo D2} (F : D1 -m> D1 -m> D2),
(forall x y, F x y F y x) -> (forall k:D1, continuous (F k)) -> continuous F.

Lemma continuous2_sym : forall `{c1:cpo D1} `{c2:cpo D2} (F : D1 -m>D1 -m>D2),
(forall x y, F x y F y x) -> (forall k, continuous (F k)) -> continuous2 F.
Hint Resolve @continuous2_sym.

• continuity is preserved by composition

Lemma continuous_comp : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D2 -m> D3)(g:D1 -m> D2), continuous f -> continuous g -> continuous (mon (f@g)).
Hint Resolve @continuous_comp.

Lemma continuous2_comp : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} `{c4:cpo D4}
(f:D1 -m> D2)(g:D2 -m> D3 -m> D4),
continuous f -> continuous2 g -> continuous2 (g @ f).
Hint Resolve @continuous2_comp.

Lemma continuous2_comp2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} `{c4:cpo D4}
(f:D3 -m> D4)(g:D1 -m> D2 -m> D3),
continuous f -> continuous2 g -> continuous2 (fcomp2 D1 D2 D3 D4 f g).
Hint Resolve @continuous2_comp2.

Lemma continuous2_app2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} `{c4:cpo D4}
(F : D1 -m> D2 -m> D3) (f:D4 -m> D1)(g:D4 -m> D2), continuous2 F ->
continuous f -> continuous g -> continuous ((F f) g).
Hint Resolve @continuous2_app2.

## Cpo of continuous functions

Instance lub_continuous `{c1:cpo D1} `{c2:cpo D2}
(f:nat -m> (D1 -m> D2)) {cf:forall n, continuous (f n)}
: continuous (lub f).
Save.

Record fcont `{c1:cpo D1} `{c2:cpo D2}: Type
:= cont {fcontm :> D1 -m> D2; fcontinuous : continuous fcontm}.

Hint Resolve @fcontinuous.
Implicit Arguments fcont [[o][c1] [o0][c2]].
Implicit Arguments cont [[D1][o][c1] [D2][o0][c2] [fcontinuous]].

Infix "->" := fcont (at level 30, right associativity) : O_scope.

Definition fcont_fun `{c1:cpo D1} `{c2:cpo D2} (f:D1 -c> D2) : D1 -> D2 := fun x => f x.

Instance fcont_ord `{c1:cpo D1} `{c2:cpo D2} : ord (D1 -c> D2)
:= {Oeq := fun f g => forall x, f x g x; Ole := fun f g => forall x, f x g x}.
Defined.

Lemma fcont_le_intro : forall `{c1:cpo D1} `{c2:cpo D2} (f g : D1 -c> D2),
(forall x, f x g x) -> f g.

Lemma fcont_le_elim : forall `{c1:cpo D1} `{c2:cpo D2} (f g : D1 -c> D2),
f g -> forall x, f x g x.

Lemma fcont_eq_intro : forall `{c1:cpo D1} `{c2:cpo D2} (f g : D1 -c> D2),
(forall x, f x g x) -> f g.

Lemma fcont_eq_elim : forall `{c1:cpo D1} `{c2:cpo D2} (f g : D1 -c> D2),
f g -> forall x, f x g x.

Lemma fcont_le : forall `{c1:cpo D1} `{c2:cpo D2} (f : D1 -c> D2) (x y : D1),
x y -> f x f y.
Hint Resolve @fcont_le.

Lemma fcont_eq : forall `{c1:cpo D1} `{c2:cpo D2} (f : D1 -c> D2) (x y : D1),
x y -> f x f y.
Hint Resolve @fcont_eq.

Definition fcont0 D1 `{c1:cpo D1} D2 `{c2:cpo D2} : D1 -c> D2 := cont (mon (cte D1 (0:D2))).

Instance fcontm_monotonic : forall `{c1:cpo D1} `{c2:cpo D2},
monotonic (fcontm (D1:=D1) (D2:=D2)).
Save.

Definition Fcontm D1 `{c1:cpo D1} D2 `{c2:cpo D2} : (D1 -c> D2) -m> (D1 -m> D2) :=
mon (fcontm (D1:=D1) (D2:=D2)).

Instance fcont_lub_continuous :
forall `{c1:cpo D1} `{c2:cpo D2} (f:nat -m> (D1 -c> D2)),
continuous (lub (D:=D1 -m> D2) (Fcontm D1 D2 @ f)).
Save.

Definition fcont_lub `{c1:cpo D1} `{c2:cpo D2} : (nat -m> (D1 -c> D2)) -> D1 -c> D2 :=
fun f => cont (lub (D:=D1 -m> D2) (Fcontm D1 D2 @ f)).

Instance fcont_cpo `{c1:cpo D1} `{c2:cpo D2} : cpo (D1-c> D2) :=
{D0:=fcont0 D1 D2; lub:=fcont_lub (D1:=D1) (D2:=D2)}.
Defined.

Definition fcont_app {O} {o:ord O} `{c1:cpo D1} `{c2:cpo D2} (f: O -m> D1 -c> D2) (x:D1) : O -m> D2
:= mshift (Fcontm D1 D2 @ f) x.

Infix "<_>" := fcont_app (at level 70) : O_scope.

Lemma fcont_app_simpl : forall {O} {o:ord O} `{c1:cpo D1} `{c2:cpo D2} (f: O -m> D1 -c> D2)(x:D1)(y:O),
(f <_> x) y = f y x.

Instance ishift_continuous :
forall {A:Type} `{c1:cpo D1} `{c2:cpo D2} (f: A -> (D1 -c> D2)),
continuous (ishift f).
Qed.

Definition fcont_ishift {A:Type} `{c1:cpo D1} `{c2:cpo D2} (f: A -> (D1 -c> D2))
: D1 -c> (A -> D2) := cont _ (fcontinuous:=ishift_continuous f).

Instance mshift_continuous : forall {O} {o:ord O} `{c1:cpo D1} `{c2:cpo D2} (f: O -m> (D1 -c> D2)),
continuous (mshift (Fcontm D1 D2 @ f)).
Save.

Definition fcont_mshift {O} {o:ord O} `{c1:cpo D1} `{c2:cpo D2} (f: O -m> (D1 -c> D2))
: D1 -c> O -m> D2 := cont (mshift (Fcontm D1 D2 @ f)).

Lemma fcont_app_continuous :
forall {O} {o:ord O} `{c1:cpo D1} `{c2:cpo D2} (f: O -m> D1 -c> D2) (h:nat -m> D1),
f <_> (lub h) lub (D:=O -m> D2) ((fcont_mshift f) @ h).

Lemma fcont_lub_simpl : forall `{c1:cpo D1} `{c2:cpo D2} (h:nat -m> D1 -c> D2)(x:D1),
lub h x = lub (h <_> x).

Instance cont_app_monotonic : forall `{o1:ord D1} `{c2:cpo D2} `{c3:cpo D3} (f:D1 -m> D2 -m> D3)
(p:forall k, continuous (f k)),
monotonic (Ob:=D2 -c> D3) (fun (k:D1) => cont _ (fcontinuous:=p k)).
Qed.

Definition cont_app `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f:D1 -m> D2 -m> D3)
(p:forall k, continuous (f k)) : D1 -m> (D2 -c> D3)
:= mon (fun k => cont (f k) (fcontinuous:=p k)).

Lemma cont_app_simpl :
forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}(f:D1 -m> D2 -m> D3)(p:forall k, continuous (f k))
(k:D1), cont_app f p k = cont (f k).

Instance cont2_continuous `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f:D1 -m> D2 -m> D3)
(p:continuous2 f) : continuous (cont_app f (continuous2_app f)).
Qed.

Definition cont2 `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f:D1 -m> D2 -m> D3)
{p:continuous2 f} : D1 -c> (D2 -c> D3)
:= cont (cont_app f (continuous2_app f)).

Instance Fcontm_continuous `{c1:cpo D1} `{c2:cpo D2} : continuous (Fcontm D1 D2).
Save.
Hint Resolve @Fcontm_continuous.

Instance fcont_comp_continuous : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D2 -c> D3) (g:D1 -c> D2), continuous (f @ g).
Save.

Definition fcont_comp `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f:D2 -c> D3) (g:D1 -c> D2)
: D1 -c> D3 := cont (f @ g).

Infix "@_" := fcont_comp (at level 35) : O_scope.

Lemma fcont_comp_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D2 -c> D3)(g:D1 -c> D2) (x:D1), (f @_ g) x = f (g x).

Lemma fcontm_fcont_comp_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D2 -c> D3)(g:D1 -c> D2), fcontm (f @_ g) = f @ g.

Lemma fcont_comp_le_compat : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f g : D2 -c> D3) (k l :D1 -c> D2),
f g -> k l -> f @_ k g @_ l.
Hint Resolve @fcont_comp_le_compat.

Add Parametric Morphism `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
: (@fcont_comp _ _ c1 _ _ c2 _ _ c3)
with signature Ole ++> Ole ++> Ole as fcont_comp_le_morph.
Save.

Add Parametric Morphism `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
: (@fcont_comp _ _ c1 _ _ c2 _ _ c3)
with signature Oeq Oeq Oeq as fcont_comp_eq_compat.
Save.

Definition fcont_Comp D1 `{c1:cpo D1} D2 `{c2:cpo D2} D3 `{c3:cpo D3}
: (D2 -c> D3) -m> (D1 -c> D2) -m> D1 -c> D3
:= mon2 _ (mf:=fcont_comp_le_compat (D1:=D1) (D2:=D2) (D3:=D3)).

Lemma fcont_Comp_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D2 -c> D3) (g:D1 -c> D2), fcont_Comp D1 D2 D3 f g = f @_ g.

Instance fcont_Comp_continuous2
: forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}, continuous2 (fcont_Comp D1 D2 D3).
Save.

Definition fcont_COMP D1 `{c1:cpo D1} D2 `{c2:cpo D2} D3 `{c3:cpo D3}
: (D2 -c> D3) -c> (D1 -c> D2) -c> D1 -c> D3
:= cont2 (fcont_Comp D1 D2 D3).

Lemma fcont_COMP_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f: D2 -c> D3) (g:D1 -c> D2),
fcont_COMP D1 D2 D3 f g = f @_ g.

Definition fcont2_COMP D1 `{c1:cpo D1} D2 `{c2:cpo D2} D3 `{c3:cpo D3} D4 `{c4:cpo D4}
: (D3 -c> D4) -c> (D1 -c> D2 -c> D3) -c> D1 -c> D2 -c> D4 :=
(fcont_COMP D1 (D2 -c> D3) (D2 -c> D4)) @_ (fcont_COMP D2 D3 D4).

Definition fcont2_comp `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} `{c4:cpo D4}
(f:D3 -c> D4)(F:D1 -c> D2 -c> D3) := fcont2_COMP D1 D2 D3 D4 f F.

Infix "@@_" := fcont2_comp (at level 35) : O_scope.

Lemma fcont2_comp_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} `{c4:cpo D4}
(f:D3 -c> D4)(F:D1 -c> D2 -c> D3)(x:D1)(y:D2), (f @@_ F) x y = f (F x y).

Lemma fcont_le_compat2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f : D1 -c> D2 -c> D3)
(x y : D1) (z t : D2), x y -> z t -> f x z f y t.
Hint Resolve @fcont_le_compat2.

Lemma fcont_eq_compat2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f : D1 -c> D2 -c> D3)
(x y : D1) (z t : D2), x y -> z t -> f x z f y t.
Hint Resolve @fcont_eq_compat2.

Lemma fcont_continuous : forall `{c1:cpo D1} `{c2:cpo D2} (f:D1 -c> D2)(h:nat -m> D1),
f (lub h) lub (f @ h).
Hint Resolve @fcont_continuous.

Instance fcont_continuous2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D1 -c> D2 -c> D3), continuous2 (Fcontm D2 D3 @ f).
Save.
Hint Resolve @fcont_continuous2.

Instance cshift_continuous2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D1 -c> D2 -c> D3), continuous2 (mshift (Fcontm D2 D3 @ f)).
Save.
Hint Resolve @cshift_continuous2.

Definition cshift `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3} (f:D1 -c> D2 -c> D3)
: D2 -c> D1 -c> D3 := cont2 (mshift (Fcontm D2 D3 @ f)).

Lemma cshift_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f:D1 -c> D2 -c> D3) (x:D2) (y:D1), cshift f x y = f y x.

Definition fcont_SEQ D1 `{c1:cpo D1} D2 `{c2:cpo D2} D3 `{c3:cpo D3}
: (D1 -c> D2) -c> (D2 -c> D3) -c> D1 -c> D3 := cshift (fcont_COMP D1 D2 D3).

Lemma fcont_SEQ_simpl : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
(f: D1 -c> D2) (g:D2 -c> D3), fcont_SEQ D1 D2 D3 f g = g @_ f.

Instance Id_mon : forall `{o1:ord Oa}, monotonic (fun x:Oa => x).
Save.

Definition Id Oa {o1:ord Oa} : Oa -m> Oa := mon (fun x => x).

Lemma Id_simpl : forall `{o1:ord Oa} (x:Oa), Id Oa x = x.

## Fixpoints

Fixpoint iter_ {D} {o} `{c: @cpo D o} (f : D -m> D) n {struct n} : D
:= match n with O => 0 | S m => f (iter_ f m) end.

Lemma iter_incr : forall `{c: cpo D} (f : D -m> D) n, iter_ f n f (iter_ f n).
Hint Resolve @iter_incr.

Instance iter_mon : forall `{c: cpo D} (f : D -m> D), monotonic (iter_ f).
Save.

Definition iter `{c: cpo D} (f : D -m> D) : nat -m> D := mon (iter_ f).

Definition fixp `{c: cpo D} (f : D -m> D) : D := mlub (iter_ f).

Lemma fixp_le : forall `{c: cpo D} (f : D -m> D), fixp f f (fixp f).
Hint Resolve @fixp_le.

Lemma fixp_eq : forall `{c: cpo D} (f : D -m> D) {mf:continuous f},
fixp f f (fixp f).

Lemma fixp_inv : forall `{c: cpo D} (f : D -m> D) g, f g g -> fixp f g.

Definition fixp_cte : forall `{c:cpo D} (d:D), fixp (mon (cte D d)) d.
Save.
Hint Resolve @fixp_cte.

Lemma fixp_le_compat : forall `{c:cpo D} (f g : D -m> D),
f g -> fixp f fixp g.
Hint Resolve @fixp_le_compat.

Instance fixp_monotonic `{c:cpo D} : monotonic fixp.
Save.

Add Parametric Morphism `{c:cpo D} : (fixp (c:=c))
with signature Oeq Oeq as fixp_eq_compat.
Save.
Hint Resolve @fixp_eq_compat.

Definition Fixp D `{c:cpo D} : (D -m> D) -m> D := mon fixp.

Lemma Fixp_simpl : forall `{c:cpo D} (f:D-m>D), Fixp D f = fixp f.

Instance iter_monotonic `{c:cpo D} : monotonic iter.
Save.

Definition Iter D `{c:cpo D} : (D -m> D) -m> (nat -m> D) := mon iter.

Lemma IterS_simpl : forall `{c:cpo D} f n, Iter D f (S n) = f (Iter D f n).

Lemma iterO_simpl : forall `{c:cpo D} (f: D-m> D), iter f O = (0:D).

Lemma iterS_simpl : forall `{c:cpo D} f n, iter f (S n) = f (iter f n).

Lemma iter_continuous : forall `{c:cpo D} (h : nat -m> (D -m> D)),
(forall n, continuous (h n)) -> iter (lub h) lub (mon iter @ h).

Hint Resolve @iter_continuous.

Lemma iter_continuous_eq : forall `{c:cpo D} (h : nat -m> (D -m> D)),
(forall n, continuous (h n)) -> iter (lub h) lub (mon iter @ h).

Lemma fixp_continuous : forall `{c:cpo D} (h : nat -m> (D -m> D)),
(forall n, continuous (h n)) -> fixp (lub h) lub (mon fixp @ h).
Hint Resolve @fixp_continuous.

Lemma fixp_continuous_eq : forall `{c:cpo D} (h : nat -m> (D -m> D)),
(forall n, continuous (h n)) -> fixp (lub h) lub (mon fixp @ h).

Definition Fixp_cont D `{c:cpo D} : (D -c> D) -m> D := Fixp D @ (Fcontm D D).

Lemma Fixp_cont_simpl : forall `{c:cpo D} (f:D -c> D), Fixp_cont D f = fixp (fcontm f).

Instance Fixp_cont_continuous : forall D `{c:cpo D}, continuous (Fixp_cont D).
Save.

Definition FIXP D `{c:cpo D} : (D -c> D) -c> D := cont (Fixp_cont D).

Lemma FIXP_simpl : forall `{c:cpo D} (f:D -c> D), FIXP D f = Fixp D (fcontm f).

Lemma FIXP_le_compat : forall `{c:cpo D} (f g : D -c> D),
f g -> FIXP D f FIXP D g.
Hint Resolve @FIXP_le_compat.

Lemma FIXP_eq_compat : forall `{c:cpo D} (f g : D -c> D),
f g -> FIXP D f FIXP D g.
Hint Resolve @FIXP_eq_compat.

Lemma FIXP_eq : forall `{c:cpo D} (f:D -c> D), FIXP D f f (FIXP D f).
Hint Resolve @FIXP_eq.

Lemma FIXP_inv : forall `{c:cpo D} (f:D -c> D) (g : D), f g g -> FIXP D f g.

### Iteration of functional

Lemma FIXP_comp_com : forall `{c:cpo D} (f g:D-c>D),
g @_ f f @_ g-> FIXP D g f (FIXP D g).

Lemma FIXP_comp : forall `{c:cpo D} (f g:D-c>D),
g @_ f f @_ g -> f (FIXP D g) FIXP D g -> FIXP D (f @_ g) FIXP D g.

Fixpoint fcont_compn {D} {o} `{c:@cpo D o}(f:D -c> D) (n:nat) {struct n} : D -c> D :=
match n with O => f | S p => fcont_compn f p @_ f end.

Lemma fcont_compn_Sn_simpl :
forall `{c:cpo D}(f:D -c> D) (n:nat), fcont_compn f (S n) = fcont_compn f n @_ f.

Lemma fcont_compn_com : forall `{c:cpo D}(f:D-c>D) (n:nat),
f @_ (fcont_compn f n) fcont_compn f n @_ f.

Lemma FIXP_compn :
forall `{c:cpo D} (f:D-c>D) (n:nat), FIXP D (fcont_compn f n) FIXP D f.

Lemma fixp_double : forall `{c:cpo D} (f:D-c>D), FIXP D (f @_ f) FIXP D f.

### Induction principle

forall f : nat -m> D, (forall n, P (f n)) -> P (lub f).

Lemma fixp_ind : forall `{c:cpo D}(F:D -m> D)(P:D->Type),
admissible P -> P 0 -> (forall x, P x -> P (F x)) -> P (fixp F).

Definition admissible2 `{c1:cpo D1}`{c2:cpo D2}(R:D1 -> D2 -> Type) :=
forall (f : nat -m> D1) (g:nat -m> D2), (forall n, R (f n) (g n)) -> R (lub f) (lub g).

Lemma fixp_ind_rel : forall `{c1:cpo D1}`{c2:cpo D2}(F:D1 -m> D1) (G:D2-m> D2)
(R:D1 -> D2 -> Type),
admissible2 R -> R 0 0 -> (forall x y, R x y -> R (F x) (G y)) -> R (fixp F) (fixp G).

Lemma lub_le_fixp : forall `{c1:cpo D1}`{c2:cpo D2} (f:D1-m>D2) (F:D1 -m> D1)
(s:nat-m> D2),
s O f 0 -> (forall x n, s n f x -> s (S n) f (F x))
-> lub s f (fixp F).

Lemma fixp_le_lub : forall `{c1:cpo D1}`{c2:cpo D2} (f:D1-m>D2) (F:D1 -m> D1)
(s:nat-m> D2) {fc:continuous f},
f 0 s O -> (forall x n, f x s n -> f (F x) s (S n)) -> f (fixp F) lub s.

Ltac continuity cont Cont Hcont:=
match goal with
| |- (Ole ?x1 (lub (mon (fun (n:nat) => cont (@?g n))))) =>
let f := fresh "f" in (
pose (f:=g); assert (monotonic f) ;
[auto | (transitivity (lub (Cont@(mon f))); [rewrite <- Hcont | auto])]
)
end.

Ltac gen_monotonic :=
match goal with |- context [(@mon _ _ _ _ ?f ?mf)] => generalize (mf:monotonic f)
end.

Ltac gen_monotonic1 f :=
match goal with |- context [(@mon _ _ _ _ f ?mf)] => generalize (mf:monotonic f)
end.

### Function for conditionnal choice defined as a morphism

Definition fif {A} (b:bool) : A -> A -> A := fun e1 e2 => if b then e1 else e2.

Instance fif_mon2 `{o:ord A} (b:bool) : monotonic2 (@fif _ b).
Save.

Definition Fif `{o:ord A} (b:bool) : A -m> A -m> A := mon2 (@fif _ b).

Lemma Fif_simpl : forall `{o:ord A} (b:bool) (x y:A), Fif b x y = fif b x y.

Lemma Fif_continuous_right `{c:cpo A} (b:bool) (e:A) : continuous (Fif b e).

Lemma Fif_continuous_left `{c:cpo A} (b:bool) : continuous (Fif (A:=A) b).
Hint Resolve @Fif_continuous_right @Fif_continuous_left.

Lemma fif_continuous_left `{c:cpo A} (b:bool) (f:nat-m> A):
fif b (lub f) lub (Fif b@f).

Lemma fif_continuous_right `{c:cpo A} (b:bool) e (f:nat-m> A):
fif b e (lub f) lub (Fif b e@f).

Hint Resolve @fif_continuous_right @fif_continuous_left.

Instance Fif_continuous2 `{c:cpo A} (b:bool) : continuous2 (Fif (A:=A) b).
Save.

Lemma fif_continuous2 `{c:cpo A} (b:bool) (f g : nat-m> A):
fif b (lub f) (lub g) lub ((Fif b@2 f) g).

Add Parametric Morphism `{o:ord A} (b:bool) : (@fif A b)
with signature Ole Ole Ole
as fif_le_compat.
Save.

Add Parametric Morphism `{o:ord A} (b:bool) : (@fif A b)
with signature Oeq Oeq Oeq
as fif_eq_compat.
Save.