Library Ccpo

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) := ∀ x y, E1 x y ↔ E2 x y.

Class Order {A} (E:relation A) (R:relation A) :=
  {reflexive :> Reflexive R;
   order_eq : ∀ 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.

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.

Lemma Ole_refl_eq : ∀ {O} {o:ord O} (x y:O), x ≈ y → x ≤ y.

Hint Immediate @Ole_refl_eq.

Lemma Ole_refl_eq_inv : ∀ {O} {o:ord O} (x y:O), x ≈ y → y ≤ x.

Hint Immediate @Ole_refl_eq_inv.

Lemma Ole_trans : ∀ {O} {o:ord O} (x y z:O), x ≤ y → y ≤ z → x ≤ z.

Lemma Ole_refl : ∀ {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 : ∀ {O} {o:ord O} (x y:O), x ≤ y → y ≤ x → x ≈ y.
Hint Immediate @Ole_antisym.

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

Lemma Oeq_refl_eq : ∀ {O} {o:ord O} (x y:O), x = y → x ≈ y.
Hint Resolve @Oeq_refl_eq.

Lemma Oeq_sym : ∀ {O} {o:ord O} (x y:O), x ≈ y → y ≈ x.

Lemma Oeq_le : ∀ {O} {o:ord O} (x y:O), x ≈ y → x ≤ y.

Lemma Oeq_le_sym : ∀ {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
   : ∀ {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 : ∀ {O} (o1 o2:ord O), eq_ord o1 o2 →
      eq_rel (Oeq (ord:=o1)) (Oeq (ord:=o2)).

Lemma Ole_eq_compat :
     ∀ {O} {o:ord O} (x1 x2 : O),
       x1 ≈ x2 → ∀ x3 x4 : O, x3 ≈ x4 → x1 ≤ x3 → x2 ≤ x4.

Lemma Ole_eq_right : ∀ {O} {o:ord O} (x y z: O),
             x ≤ y → y ≈ z → x ≤ z.

Lemma Ole_eq_left : ∀ {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.

Dual order

Iord x y = y ≤ x

Definition Iord : ∀ 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 ⇒ ∀ x, R (f x) (g x).
Implicit Arguments fun_ext [B].

ford f g := ∀ 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 : ∀ A O (o:ord O) (f g:A → O), f ≤ g → ∀ n, f n ≤ g n.
Hint Immediate ford_le_elim.

Lemma ford_le_intro : ∀ A O (o:ord O) (f g:A → O), ( ∀ n, f n ≤ g n ) → f ≤ g.
Hint Resolve ford_le_intro.

Lemma ford_eq_elim : ∀ A O (o:ord O) (f g:A → O), f ≈ g → ∀ n, f n ≈ g n.
Hint Immediate ford_eq_elim.

Lemma ford_eq_intro : ∀ A O (o:ord O) (f g:A → O), ( ∀ 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 : ∀ x y, x ≤ y → f x ≤ f y.

Lemma monotonic_intro : ∀ `{o1:ord Oa} `{o2:ord Ob} (f : Oa → Ob),
  (∀ 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 : ∀ x y, x ≈ y → f x ≈ f y.
Hint Unfold stable.

Lemma stable_intro : ∀ `{o1:ord Oa} `{o2:ord Ob} (f : Oa → Ob),
  (∀ 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 : ∀ `{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 : ∀ `{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 : ∀ `{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)=> ∀ x, f x ≈ g x;
       Ole := fun (f g : Oa-m > Ob)=> ∀ x, f x ≤ g x}.
Defined.

Lemma mon_le_compat : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{o1:ord Oa} `{o2:ord Ob}, (Oa -m > Ob) → (Oa --m → Ob).
Defined.

Lemma Imon_simpl : ∀ `{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
  : ∀ `{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
  : ∀ `{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 : ∀ (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: ∀ 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} : ∀ 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:∀ 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 : ∀ (x y:Oa) (z t:Ob), x ≈ y → 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 : ∀ `{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 : ∀ `{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) :
       ∀ 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 : ∀ `{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 : ∀ `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc}
     (f:Oa -m > Ob -m > Oc), mon2 (fun2 f) ≈ f.

Lemma fun2_mon2 : ∀ `{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 : ∀ `{o1: ord Oa} `{o2: ord Ob} `{o3:ord Oc},
     (Oa -m > Ob -m > Oc) → (Oa --m > Ob --m → Oc).
Defined.

Lemma Imon2_simpl : ∀ `{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 : ∀ `{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.

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 : ∀ n m, ((n ≤ m)%nat)-> n ≤ m.
Hint Resolve le_Ole.

Lemma nat_monotonic : ∀ {O} {o:ord O}
               (f:nat → O), (∀ n, f n ≤ f (S n)) → monotonic f.
Hint Resolve @nat_monotonic.

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

Lemma fnatO_elim : ∀ {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
  : ∀ n {O} {o:ord O} (f:nat → O) {m:monotonic f}, monotonic (seq_lift_left f n).
Save.

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

Lemma mseq_lift_left_simpl : ∀ {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 : ∀ {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
   : ∀ n {O} {o:ord O} (f:nat → O) {m:monotonic f}, monotonic (seq_lift_right f n).
Save.

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

Lemma mseq_lift_right_simpl : ∀ {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 : ∀ {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 : ∀ {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)) :
       ∀ 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 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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:∀ 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 : ∀ {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 : ∀ `{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 : ∀ `{o1:ord Oa} `{o2:ord Ob} (f:Oa -m > (Oa -m > Ob)) (x:Oa),
             diag f x = f x x.

Lemma diag_le_compat : ∀ `{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 : ∀ `{o1:ord Oa} `{o2:ord Ob} (f: Oa -m > Oa -m > Ob),
                   diag f ≈ diag (mshift f).

Hint Resolve @diag_shift.

Lemma mshift_simpl : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 :
    ∀ `{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 :
      ∀ `{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 :
      ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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.
Hint Resolve fmon_le_compat2.

Lemma fmon_cte_comp : ∀ `{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 : ∀ i, f i ≤ x;
       islub_le : ∀ y, (∀ 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 → ∀ i, x ≤ f i.

Lemma isglb_le O (o:ord O) I (f:I → O) (x:O) :
         isglb f x → ∀ y, (∀ 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) :
      (∀ i, x ≤ f i) → (∀ y, (∀ 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 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.

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.

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: ∀ (f:nat -m > D), D;
   Dbot : ∀ x:D, D0 ≤ x;
   le_lub : ∀ (f : nat -m > D) (n:nat), f n ≤ lub f;
   lub_le : ∀ (f : nat -m > D) (x:D), (∀ 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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{c:cpo D} (f:nat → D) {m:monotonic f} (n:nat), f n ≤ mlub f.

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

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 : ∀ `{c:cpo D} (d:D), mlub (cte nat d) ≈ d.

Hint Resolve @lub_cte.

Lemma mlub_lift_right : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{c:cpo D} (f g:nat -m > D)
      (n:nat), (∀ k, n ≤ k → f k ≤ g k) → lub f ≤ lub g.

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

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

(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 : ∀ {A} `{c:cpo D} (h:nat -m > (A → D))(x:A),
      (lub h) x = lub (h <o > x).

Lemma lub_ishift : ∀ {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 : ∀ {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 : ∀ {O} {o:ord O} `{c:cpo D}
         (h:nat -m > (O → D)) {mh:∀ n, monotonic (h n)}, monotonic (lub h).
Save.

Link between lubs on ordinary functions and monotonic functions

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

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

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

Lemma double_lub_shift : ∀ `{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 :
    ∀ `{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 : ∀ `{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 : ∀ (h : nat -m > D1), f (lub h) ≤ lub (f @ h).

Typeclasses Opaque continuous.

Lemma continuous_eq_compat : ∀ `{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 :
    ∀ `{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 : ∀ (f : nat -m > D1) (g :nat -m > D2),
                 F (lub f) (lub g) ≤ lub ((F @² f) g).

Lemma continuous2_app : ∀ `{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 :
   ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}
      (F : D1 -m > D2 -m > D3) (cFr: ∀ k:D1, continuous (F k)) (cF: continuous F),
      continuous2 F.

Hint Resolve @continuous2_app @continuous2_continuous @continuous_continuous2.

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

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

Lemma mshift_continuous2 : ∀ `{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 : ∀ `{o1:ord D1} `{o2:ord D2} (F : D1 → D1 → D2),
      (∀ x y, F x y ≈ F y x) → (∀ k:D1, monotonic (F k)) → monotonic F.
Hint Immediate @monotonic_sym.

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

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

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

continuity is preserved by composition

Lemma continuous_comp : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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} `{c3:cpo D3}
     (f:nat -m > (D1 -m > D2)) {cf:∀ 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 ⇒ ∀ x, f x ≈ g x; Ole := fun f g ⇒ ∀ x, f x ≤ g x}.
Defined.

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

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

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

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

Lemma fcont_le : ∀ `{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 : ∀ `{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 : ∀ `{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 :
    ∀ `{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 : ∀ {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 :
   ∀ {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 : ∀ {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 :
       ∀ {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 : ∀ `{c1:cpo D1} `{c2:cpo D2} (h:nat -m > D1 -c > D2)(x:D1),
            lub h x = lub (h <_> x).

Instance cont_app_monotonic : ∀ `{o1:ord D1} `{c2:cpo D2} `{c3:cpo D3} (f:D1 -m > D2 -m > D3)
            (p:∀ 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:∀ k, continuous (f k)) : D1 -m > (D2 -c > D3)
    := mon (fun k ⇒ cont (f k) (fcontinuous:=p k)).

Lemma cont_app_simpl :
∀ `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}(f:D1 -m > D2 -m > D3)(p:∀ 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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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
   : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{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 : ∀ `{c: cpo D} (f : D -m > D) n, iter_ f n ≤ f (iter_ f n).
Hint Resolve @iter_incr.

Instance iter_mon : ∀ `{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 : ∀ `{c: cpo D} (f : D -m > D), fixp f ≤ f (fixp f).
Hint Resolve @fixp_le.

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

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

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

Lemma fixp_le_compat : ∀ `{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 : ∀ `{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 : ∀ `{c:cpo D} f n, Iter D f (S n) = f (Iter D f n).

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

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

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

Hint Resolve @iter_continuous.

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

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

Lemma fixp_continuous_eq : ∀ `{c:cpo D} (h : nat -m > (D -m > D)),
       (∀ 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 : ∀ `{c:cpo D} (f:D -c > D), Fixp_cont D f = fixp (fcontm f).

Instance Fixp_cont_continuous : ∀ 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 : ∀ `{c:cpo D} (f:D -c > D), FIXP D f = Fixp D (fcontm f).

Lemma FIXP_le_compat : ∀ `{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 : ∀ `{c:cpo D} (f g : D -c > D),
            f ≈ g → FIXP D f ≈ FIXP D g.
Hint Resolve @FIXP_eq_compat.

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

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

Iteration of functional

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

Lemma FIXP_comp : ∀ `{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 :
     ∀ `{c:cpo D}(f:D -c > D) (n:nat), fcont_compn f (S n) = fcont_compn f n @_ f.

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

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

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

Induction principle

Definition admissible `{c:cpo D}(P:D→Type) :=
          ∀ f : nat -m > D, (∀ n, P (f n)) → P (lub f).

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

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

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

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 : ∀ `{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.