Library ALEA.Ccpo

Ccpo.v: Specification and properties of a cpo

Require Export Arith.
From Coq Require Import Lia.

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

Declare Scope signature_scope.
#[local] Open Scope signature_scope.
Declare Scope O_scope.
Delimit Scope O_scope with O.
#[local] Open Scope O_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 }.

Generalizable Variables A E R.

#[export] Instance OrderEqRefl `{Order A E R} : Reflexive E.
Qed.

#[export] Instance OrderEqSym `{Order A E R} : Symmetric E.
Qed.

#[export] Instance OrderEqTrans `{Order A E R} : Transitive E.
Qed.

#[export] Instance OrderEquiv `{Order A E R} : Equivalence E.
Qed.
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 : O_scope.
Infix " ≈ " := Oeq : type_scope.

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

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

#[export] Hint Immediate Ole_refl_eq : core.

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

#[export] Hint Immediate Ole_refl_eq_inv : core.

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.

#[export] Hint Resolve Ole_refl : core.

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.
#[export] Hint Immediate Ole_antisym : core.

Lemma Oeq_refl : forall {O} {o:ord O} (x:O), x ≈ x.
#[export] Hint Resolve Oeq_refl : core.

Lemma Oeq_refl_eq : forall {O} {o:ord O} (x y:O), x = y -> x ≈ y.
#[export] Hint Resolve Oeq_refl_eq : core.

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.

#[export] Hint Resolve Oeq_le : core.
#[export] Hint Immediate Oeq_sym Oeq_le_sym : core.

Lemma Oeq_trans
   : forall {O} {o:ord O} (x y z:O), x ≈ y -> y ≈ z -> x ≈ z.
#[export] Hint Resolve Oeq_trans : core.

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

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 : O_scope.

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.
Qed.

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.

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

#[export] Hint Immediate Olt_neq Olt_neq_rev Olt_le Olt_notle : core.
#[export] Hint Resolve Ole_diff_lt : core.

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.

#[export] Hint Resolve Olt_antirefl : core.

Lemma Ole_not_lt `{o:ord A} : forall x y:A, x ≤ y -> ~ y < x.
#[export] Hint Resolve Ole_not_lt : core.

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.

Arguments Iord O {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).
Arguments fun_ext A [B] R.

ford f g := forall x, f x ≤ g x

#[export] Program Instance ford A O {o:ord O} : ord (A -> O) :=
{Oeq:=fun_ext A (Oeq (A:=O)); Ole:=fun_ext A (Ole (A:=O))}.

Lemma ford_le_elim : forall A O (o:ord O) (f g:A -> O), f ≤ g -> forall n, f n ≤ g n.
#[export] Hint Immediate ford_le_elim : core.

Lemma ford_le_intro : forall A O (o:ord O) (f g:A -> O), ( forall n, f n ≤ g n ) -> f ≤ g.
#[export] Hint Resolve ford_le_intro : core.

Lemma ford_eq_elim : forall A O (o:ord O) (f g:A -> O), f ≈ g -> forall n, f n ≈ g n.
#[export] Hint Immediate ford_eq_elim : core.

Lemma ford_eq_intro : forall A O (o:ord O) (f g:A -> O), ( forall n, f n ≈ g n ) -> f ≈ g.
#[export] Hint Resolve ford_eq_intro : core.

Monotonicity

Definition and properties

Generalizable Variables Oa Ob Oc Od.

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.
#[export] Hint Resolve monotonic_intro : core.

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.
Qed.

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

Lemma stable_intro : forall `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob),
  (forall x y, x ≈ y -> f x ≈ f y ) -> stable f.
#[export] Hint Resolve stable_intro : core.

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.
Qed.

#[export] Typeclasses Opaque monotonic stable.

#[export] Instance monotonic_stable `{o1:ord Oa} `{o2:ord Ob} (f : Oa -> Ob) {m:monotonic f}
         : stable f.
Qed.

Type of monotonic functions

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

#[export]
Existing Instance fmonotonic.

Arguments mon [Oa o1 Ob o2] fmont {fmonotonic}.
Arguments fmon Oa [o1] Ob {o2}.

#[export] Hint Resolve fmonotonic : core.

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.
#[export] Hint Resolve mon_simpl : core.

#[export] Instance fstable `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m > Ob) : stable f.
Qed.

#[export] Hint Resolve fstable : core.

Lemma fmon_le : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m > Ob) x y,
                x ≤ y -> f x ≤ f y.
#[export] Hint Resolve fmon_le : core.

Lemma fmon_eq : forall `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m > Ob) x y,
                x ≈ y -> f x ≈ f y.
#[export] Hint Resolve fmon_eq : core.

#[export] Program 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}.

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.
#[export] Hint Resolve mon_le_compat : core.

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.
#[export] Hint Resolve mon_eq_compat : core.

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.

#[export] 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.

#[export] 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.
Qed.

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).
#[export] 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).

#[export] 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)).
Qed.

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

#[export] Instance monotonic2_stable2 `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
    (f:Oa -> Ob -> Oc) {m:monotonic2 f} : stable2 f.
Qed.

#[export] 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.
#[export] Hint Resolve mon2_simpl : core.

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.

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

#[export] Instance fun2_monotonic `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
         (f:Oa -> Ob -m > Oc) {mf:monotonic f} : monotonic (fun2 f).
Qed.
#[export] Hint Resolve fun2_monotonic : core.

#[export] Instance fmonotonic2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m > Ob -m > Oc)
         : monotonic2 (fun2 f).
Qed.
#[export] Hint Resolve fmonotonic2 : core.

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.

#[export] Instance mfun2_mon `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc}
         (f:Oa -m > Ob -m > Oc) x : monotonic (mfun2 f x).
Qed.

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.
#[export] Hint Resolve mon2_fun2 fun2_mon2 : core.

#[export] Instance fstable2 `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc} (f:Oa -m > Ob -m > Oc)
                : stable2 (fun2 f).
Qed.
#[export] Hint Resolve fstable2 : core.

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.

#[export] 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

#[export] Program Instance natO : ord nat :=
    { Oeq := fun n m : nat => n = m;
       Ole := fun n m : nat => (n ≤ m)%nat}.

Lemma le_Ole : forall n m, ((n ≤ m)%nat)-> n ≤ m.
#[export] Hint Resolve le_Ole : core.

Lemma nat_monotonic : forall {O} {o:ord O}
               (f:nat -> O), (forall n, f n ≤ f (S n)) -> monotonic f.
#[export] Hint Resolve nat_monotonic : core.

Lemma nat_monotonic_inv : forall {O} {o:ord O}
               (f:nat -> O), (forall n, f (S n) ≤ f n ) -> monotonic (o2:=Iord O) f.
#[export] Hint Resolve nat_monotonic_inv : core.

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).
#[export] Hint Resolve fnatO_elim : core.

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

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

#[export] Instance mon_seq_lift_left
  : forall n {O} {o:ord O} (f:nat -> O) {m:monotonic f}, monotonic (seq_lift_left f n).
Qed.

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.
#[export] Hint Resolve mseq_lift_left_le_compat : core.

Add Parametric Morphism {O} {o:ord O} : (@mseq_lift_left _ o)
  with signature Oeq ⇾ eq ⇾ Oeq
  as mseq_lift_left_eq_compat.
Qed.
#[export] Hint Resolve mseq_lift_left_eq_compat : core.

Add Parametric Morphism {O} {o:ord O}: (@seq_lift_left O)
  with signature Oeq ⇾ eq ⇾ Oeq
  as seq_lift_left_eq_compat.
Qed.
#[export] Hint Resolve seq_lift_left_eq_compat : core.

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

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

#[export] Instance mon_seq_lift_right
   : forall n {O} {o:ord O} (f:nat -> O) {m:monotonic f}, monotonic (seq_lift_right f n).
Qed.

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.
#[export] Hint Resolve mseq_lift_right_le_compat : core.

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

Add Parametric Morphism {O} {o:ord O}: (@seq_lift_right O)
  with signature Oeq ⇾ eq ⇾ Oeq
  as seq_lift_right_eq_compat.
Qed.
#[export] Hint Resolve seq_lift_right_eq_compat : core.

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

#[export] 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).
Qed.

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.
#[export] Hint Resolve shift_le_compat : core.

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.
Qed.

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

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.
#[export] Hint Resolve ishift_le_compat : core.

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.
Qed.

#[export] 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).
Qed.

#[export] 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).
Qed.
#[export] Hint Resolve shift_mon_fun shift_fun_mon shift_mon2 : core.

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.

#[export] Instance mon_id : forall {O:Type} {o:ord O}, monotonic (id O).
Qed.

(cte c) n = c

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

#[export] Instance mon_cte : forall `{o1:ord Oa} `{o2:ord Ob} (c:Ob), monotonic (cte Oa c).
Qed.

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.
Qed.

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

#[export] Instance mon_diag `{o1:ord Oa} `{o2:ord Ob}(f:Oa -m > (Oa -m > Ob ))
     : monotonic (fun x => f x x).
Qed.
#[export] Hint Resolve mon_diag : core.

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.
#[export] Hint Resolve diag_le_compat : core.

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

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

#[export] Hint Resolve diag_shift : core.

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.
#[export] Hint Resolve mshift_le_compat : core.

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

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)

#[export] 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)).
Qed.
#[export] Hint Resolve monotonic_comp : core.

#[export] 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)).
Qed.
#[export] Hint Resolve monotonic_comp_mon : core.

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.
Qed.

#[export] Hint Immediate comp_le_compat : core.

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.
Qed.

#[export] Hint Immediate comp_eq_compat : core.

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

#[export] 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)).
Qed.

#[export] 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)).
Qed.

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.
Qed.

#[export] Hint Immediate app2_le_compat : core.

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.
Qed.

#[export] Hint Immediate app2_eq_compat : core.

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.
#[export] Hint Resolve comp_monotonic_right : core.

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.
#[export] Hint Resolve comp_monotonic_left : core.

#[export] Instance comp_monotonic2 : forall `{o1:ord Oa} `{o2:ord Ob} `{o3:ord Oc},
             monotonic2 (@comp Oa _ Ob _ Oc _).
Qed.
#[export] Hint Resolve comp_monotonic2 : core.

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 _).

Arguments fcomp Oa [o1] Ob [o2] Oc {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 ).

Arguments fcomp2 Oa [o1] Ob [o2] Oc [o3] Od {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), x ≤ y -> z ≤ t -> f x z ≤ f y t.
#[export] Hint Resolve fmon_le_compat2 : core.

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}.
Arguments islub [O o I] f x.
Arguments le_islub [O o I f x].
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.
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.
Arguments le_isglb [O o I f x].
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):
      f ≈ g -> x ≈ y -> islub f x -> islub g y.

Lemma islub_eq_compat_left O (o:ord O) I (f g:I -> O) (x:O):
      f ≈ g -> 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):
      f ≈ g -> x ≈ y -> isglb f x -> isglb g y.

Lemma isglb_eq_compat_left O (o:ord O) I (f g:I -> O) (x:O):
      f ≈ g -> 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.
Qed.

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

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

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

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.

#[export] Hint Resolve islub_incr_ext isglb_decr_ext : core.

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

Generalizable Variables D.

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}.

Arguments cpo D {o}.

Notation "0" := D0 : O_scope.

#[export] Hint Resolve Dbot le_lub lub_le : core.

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.
Qed.
#[export] Hint Resolve lub_le_compat : core.

Add Parametric Morphism `{c:cpo D}: (lub (cpo:=c))
      with signature Oeq ⇾ Oeq as lub_eq_compat.
Qed.
#[export] Hint Resolve lub_eq_compat : core.

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.
#[export] Hint Resolve mlub_le_compat : core.

Lemma mlub_eq_compat : forall `{c:cpo D} (f g:nat -> D) {mf:monotonic f} {mg:monotonic g},
                f ≈ g -> mlub f ≈ mlub g.
#[export] Hint Resolve mlub_eq_compat : core.

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.
#[export] Hint Resolve le_mlub mlub_le : core.

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).

#[export] Hint Resolve islub_mlub islub_lub : core.

#[export] Instance lub_mon `{c:cpo D} : monotonic lub.
Qed.

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

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

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

#[export] Hint Resolve lub_cte : core.

Lemma mlub_lift_right : forall `{c:cpo D} (f:nat -m > D) n,
      lub f ≈ mlub (seq_lift_right f n ).
#[export] Hint Resolve mlub_lift_right : core.

Lemma mlub_lift_left : forall `{c:cpo D} (f:nat -m > D) n,
      lub f ≈ mlub (seq_lift_left f n ).
#[export] Hint Resolve mlub_lift_left : core.

Lemma lub_lift_right : forall `{c:cpo D} (f:nat -m > D) n,
      lub f ≈ lub (mseq_lift_right f n).
#[export] Hint Resolve lub_lift_right : core.

Lemma lub_lift_left : forall `{c:cpo D} (f:nat -m > D) n,
      lub f ≈ lub (mseq_lift_left f n).
#[export] Hint Resolve lub_lift_left : core.

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 ).

#[export] 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)).
Qed.
#[export] Hint Resolve lub_shift_mon : core.

Functional cpos

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

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

#[export] Program 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))}.

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).
#[export] Hint Resolve fmon_lub_simpl : core.

#[export] 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).
Qed.

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).
#[export] Hint Resolve double_lub_diag : core.

Lemma double_lub_shift : forall `{c:cpo D} (h : nat -m > nat -m > D),
        lub (lub h) ≈ lub (lub (mshift h)).
#[export] Hint Resolve double_lub_shift : core.

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).
#[export] Hint Resolve lub_comp_le : core.

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).
#[export] Hint Resolve lub_app2_le : core.

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).

#[export] 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.
Qed.

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).
#[export] Hint Resolve lub_comp_eq : core.

mon0 x == 0

#[export] Instance cont0 `{c1:cpo D1} `{c2:cpo D2} : continuous (mon (cte D1 (0:D2))).
Qed.

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).

#[export] 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.
#[export] Hint Immediate continuous2_continuous : core.

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.

#[export] Hint Resolve continuous2_app continuous2_continuous continuous_continuous2 : core.

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).
#[export] Hint Resolve mshift_continuous2 : core.

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.
#[export] Hint Immediate monotonic_sym : core.

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.
#[export] Hint Immediate monotonic2_sym : core.

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.
#[export] Hint Resolve continuous2_sym : core.

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)).
#[export] Hint Resolve continuous_comp : core.

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).
#[export] Hint Resolve continuous2_comp : core.

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).
#[export] Hint Resolve continuous2_comp2 : core.

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).
#[export] Hint Resolve continuous2_app2 : core.

Cpo of continuous functions

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

Record fcont `{c1:cpo D1} `{c2:cpo D2}: Type
     := cont {fcontm :> D1 -m > D2; fcontinuous : continuous fcontm}.
#[export] Existing Instance fcontinuous.

#[export] Hint Resolve fcontinuous : core.
Arguments fcont D1 [o][c1] D2 {o0}{c2}.
Arguments cont [D1][o][c1] [D2][o0][c2] fcontm {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.

#[export] Program 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}.

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.
#[export] Hint Resolve fcont_le : core.

Lemma fcont_eq : forall `{c1:cpo D1} `{c2:cpo D2} (f : D1 -c > D2) (x y : D1),
            x ≈ y -> f x ≈ f y.
#[export] Hint Resolve fcont_eq : core.

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

#[export] Instance fcontm_monotonic : forall `{c1:cpo D1} `{c2:cpo D2},
         monotonic (fcontm (D1:=D1) (D2:=D2)).
Qed.

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

#[export] 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)).
Qed.

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)).

#[export] Program Instance fcont_cpo `{c1:cpo D1} `{c2:cpo D2} : cpo (D1 -c > D2) :=
  {D0:=fcont0 D1 D2; lub:=fcont_lub (D1:=D1) (D2:=D2)}.

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.

#[export] 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).

#[export] 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)).
Qed.

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).

#[export] 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).

#[export] 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)).

#[export] Instance Fcontm_continuous `{c1:cpo D1} `{c2:cpo D2} : continuous (Fcontm D1 D2).
Qed.
#[export] Hint Resolve Fcontm_continuous : core.

#[export] 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).
Qed.

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.
#[export] Hint Resolve fcont_comp_le_compat : core.

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.
Qed.

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.
Qed.

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.

#[export] Instance fcont_Comp_continuous2
   : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}, continuous2 (fcont_Comp D1 D2 D3).
Qed.

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.
#[export] Hint Resolve fcont_le_compat2 : core.

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.
#[export] Hint Resolve fcont_eq_compat2 : core.

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

#[export] Instance fcont_continuous2 : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
         (f:D1 -c > D2 -c > D3), continuous2 (Fcontm D2 D3 @ f).
Qed.
#[export] Hint Resolve fcont_continuous2 : core.

#[export] 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)).
Qed.
#[export] Hint Resolve cshift_continuous2 : core.

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.

#[export] Instance Id_mon : forall `{o1:ord Oa}, monotonic (fun x:Oa => x).
Qed.

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).
#[export] Hint Resolve iter_incr : core.

#[export] Instance iter_mon : forall `{c: cpo D} (f : D -m > D), monotonic (iter_ f).
Qed.

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).
#[export] Hint Resolve fixp_le : core.

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.
Qed.
#[export] Hint Resolve fixp_cte : core.

Lemma fixp_le_compat : forall `{c:cpo D} (f g : D -m > D),
      f ≤ g -> fixp f ≤ fixp g.
#[export] Hint Resolve fixp_le_compat : core.

#[export] Instance fixp_monotonic `{c:cpo D} : monotonic fixp.
Qed.

Add Parametric Morphism `{c:cpo D} : (fixp (c:=c))
    with signature Oeq ⇾ Oeq as fixp_eq_compat.
Qed.
#[export] Hint Resolve fixp_eq_compat : core.

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.

#[export] Instance iter_monotonic `{c:cpo D} : monotonic iter.
Qed.

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).

#[export] Hint Resolve iter_continuous : core.

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).
#[export] Hint Resolve fixp_continuous : core.

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).

#[export] Instance Fixp_cont_continuous : forall D `{c:cpo D}, continuous (Fixp_cont D).
Qed.

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.
#[export] Hint Resolve FIXP_le_compat : core.

Lemma FIXP_eq_compat : forall `{c:cpo D} (f g : D -c > D),
            f ≈ g -> FIXP D f ≈ FIXP D g.
#[export] Hint Resolve FIXP_eq_compat : core.

Lemma FIXP_eq : forall `{c:cpo D} (f:D -c > D), FIXP D f ≈ f (FIXP D f).
#[export] Hint Resolve FIXP_eq : core.

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

Definition admissible `{c:cpo D}(P:D ->Type) :=
          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.

#[export] Instance fif_mon2 `{o:ord A} (b:bool) : monotonic2 (@fif _ b).
Qed.

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).
#[export] Hint Resolve Fif_continuous_right Fif_continuous_left : core.

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

Lemma fif_continuous_left2 :
forall (A : Type) (o : ord A) (c : cpo A) (b : bool) (f : nat -m > A) (g:A),
fif b (lub f) g ≈ lub (Fif b @ f) g.

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

#[export] Hint Resolve fif_continuous_right fif_continuous_left fif_continuous_left2 : core.

#[export] Instance Fif_continuous2 `{c:cpo A} (b:bool) : continuous2 (Fif (A:=A) b).
Qed.

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.
Qed.

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