Library cpo

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import directed.

Delimit Scope cpo_scope with cpo.
Open Scope cpo_scope.

Definition continuous (CL:color) (A B:preord) (f:A B) :=
  forall lub (XS:cl_eset CL A),
    least_upper_bound lub XS ->
    least_upper_bound (f lub) (image f XS).

Lemma continuous_sequence CL (A B C:preord)
  (g:B C) (f:A B) :
  continuous CL g -> continuous CL f -> continuous CL (g f).

Lemma continuous_equiv CL (A B:preord) (f f':A B) :
  f f' -> continuous CL f -> continuous CL f'.

Lemma continuous_pair CL (C A B:preord) (f:C A) (g:C B) :
  continuous CL f -> continuous CL g -> continuous CL f, g.

Lemma continuous_pi1 CL (A B:preord) :
  @continuous CL (A×B) A π.

Lemma continuous_pi2 CL (A B:preord) :
  @continuous CL (A×B) B π.

Complete partial orders

Here we define the category of colored CPOs. We will mostly be interested in the case where the color is one of the two instances of h-directedness; however much of the the theory goes through in the more general setting of arbitrary colors.
A CPO is a preorder where there is a supremum operation for every colored set. CPOs form a category together with the Scott-continuous functions, which are monotone and preserve colored suprema.
Module CPO.
  Record mixin_of (CL:color) (A:preord)
    := Mixin
    { sup : cl_eset CL A -> A
    ; sup_is_ub : forall X, upper_bound (sup X) X
    ; sup_is_least : forall X ub, upper_bound ub X -> sup X ub

  Record type (CL:color) := Pack
    { carrier :> Type
    ; ord_mixin : Preord.mixin_of carrier
    ; ord := Preord.Pack carrier ord_mixin
    ; cpo_mixin : mixin_of CL ord

  Hint Resolve cpo_mixin.
  Canonical Structure ord.

  Definition cpo_eq CL (T:type CL) : Eq.type :=
    Eq.Pack (carrier T) (Eq.mixin (Preord_Eq (ord T))).
  Canonical Structure cpo_eq.

  Definition sup_op CL (t:type CL) : cl_eset CL (ord t) -> ord t :=
    sup CL (ord t) (cpo_mixin t).

  Notation "∐ XS" := (@sup_op _ _ (XS)%set) : cpo_scope.

  Lemma sup_is_lub : forall CL (A:type CL) (XS:cl_eset CL (ord A)),
    least_upper_bound (XS) XS.

  Lemma continuous_sup : forall CL (A B:type CL) (f:ord A ord B),
    continuous CL f <->
    forall (XS:cl_eset CL (ord A)), f (sup_op XS) sup_op (image f XS).

  Lemma continuous_sup' : forall CL (A B:type CL) (f:ord A ord B),
    continuous CL f <->
    forall (XS:cl_eset CL (ord A)), f (sup_op XS) sup_op (image f XS).

  Record hom CL (A B:type CL) :=
    { map :> ord A -> ord B
    ; mono : forall (a b:carrier A),
               Preord.ord_op (ord A) a b ->
               Preord.ord_op (ord B) (map a) (map b)
    ; cont : continuous CL (Preord.Hom _ _ map mono)

  Definition ord_hom {CL:color} {A B:type CL} (f:hom CL A B) : Preord.hom (ord A) (ord B) :=
    Preord.Hom _ _ (map f) (mono f).
  Coercion ord_hom : hom >-> Preord.hom.

  Program Definition build_hom {CL:color} (A B:type CL)
    (f:Preord.hom (ord A) (ord B))
    (H:continuous CL f)
    : hom CL A B
    := Hom CL A B ( _ _ f) _ _.

  Program Definition ident {CL:color} (X:type CL) :
    hom CL X X := build_hom X X (Preord.ident (ord X)) _.

  Program Definition compose {CL:color} {X Y Z:type CL} (g:hom CL Y Z) (f:hom CL X Y)
    := build_hom X Z (g f) _.

  Definition comp_mixin CL := Comp.Mixin (type CL) (hom CL) (@ident CL) (@compose CL).
  Canonical Structure comp CL := Comp.Pack (type CL) (hom CL) (comp_mixin CL).

  Definition app {CL:color} {X Y:type CL} (f:hom CL X Y) (x:X) : Y := map f x.

  Definition hom_order {CL:color} (X Y:type CL) (f g:hom CL X Y) :=
    forall x:X, app f x app g x.

  Program Definition hom_ord_mixin CL X Y :=
    Preord.Mixin (hom CL X Y) (hom_order X Y) _ _.

  Canonical Structure hom_ord CL (A B:type CL) :=
    Preord.Pack (CPO.hom CL A B) (CPO.hom_ord_mixin CL A B).

  Program Definition app_to CL (X Y:type CL) (x:X) : Preord.hom (hom_ord CL X Y) (ord Y) :=
    Preord.Hom (hom_ord CL X Y) (ord Y) (fun f => map f x) _.

  Program Definition hom_sup CL (X Y:type CL) (FS:cl_eset CL (hom_ord CL X Y)) : hom CL X Y :=
    Hom CL X Y (fun x => sup_op (image (app_to CL X Y x) FS)) _ _.

  Program Definition hom_mixin CL X Y :=
    Mixin CL (hom_ord CL X Y) (hom_sup CL X Y) _ _.

  Canonical Structure hom_cpo CL X Y :=
    Pack CL (hom CL X Y) (hom_ord_mixin CL X Y) (hom_mixin CL X Y).

  Definition cpo_eq_mixin CL X Y := Preord.ord_eq (hom_ord CL X Y).

  Lemma cat_axioms CL : Category.axioms (type CL) (hom CL) (cpo_eq_mixin CL) (comp_mixin CL).

  Canonical Structure CPO CL := Category (type CL) (hom CL) _ _ (cat_axioms CL).

  Lemma axiom : forall CL (A B:ob (CPO CL)) (f:A B),
    forall X, f (X) ∐(image f X).

  Section prod.
    Variable CL:color.
    Variables A B:type CL.

    Program Definition prod_sup (X:cl_eset CL (prod_preord (ord A) (ord B))) : A*B :=
      (∐(image π X), ∐(image π X)).

    Program Definition prod_mixin : mixin_of CL (prod_preord (ord A) (ord B)) :=
      Mixin CL _ prod_sup _ _.

    Definition prod_cpo :=
      Pack CL (A*B) (Preord.mixin (prod_preord (ord A) (ord B))) prod_mixin.

    Program Definition pi1 : prod_cpo A :=
      Hom CL prod_cpo A (fun x => fst x) _ _.

    Program Definition pi2 : prod_cpo B :=
      Hom CL prod_cpo B (fun x => snd x) _ _.
  End prod.

  Program Definition pair CL (C A B:type CL) (f:C A) (g:C B) : C prod_cpo CL A B :=
    Hom CL C (prod_cpo CL A B) (fun x => (f x, g x)) _ _.

End CPO.

A "dcpo" is a directed-complete partial order; that is a CPO with one of the the directedness color variants.
Notation dcpo hf := (CPO.type (directed_hf_cl hf)).

A "cpo" is a directed-complete cpo not necessarily containing a least element.
Notation cpo := (CPO.type (directed_hf_cl false)).

A "cppo" is a directed-complete pointed partial order; that is certainly has a least element.
Notation cppo := (CPO.type (directed_hf_cl true)).

Notation CPO := CPO.CPO.

Notation dirset := (cl_eset (directed_hf_cl _)).

Canonical Structure CPO.
Canonical Structure CPO.ord.
Canonical Structure CPO.ord_hom.
Canonical Structure CPO.comp.
Canonical Structure CPO.hom_ord.
Canonical Structure CPO.hom_cpo.
Canonical Structure hom_eq CL X Y:=
  Eq.Pack (CPO.hom CL X Y) (Preord.ord_eq (CPO.hom_ord CL X Y)).
Coercion CPO.ord : CPO.type >-> preord.
Coercion CPO.ord_hom : CPO.hom >-> Preord.hom.

Notation "∐ XS" := (@CPO.sup_op _ _ (XS)%set) : cpo_scope.

Supremum is a monotone operation.
Lemma sup_monotone : forall CL (A:CPO.type CL) (X X':cl_eset CL A),
  X X' -> X X'.

Supremum respects equality of sets.
Lemma sup_equiv : forall CL (A:CPO.type CL) (X X':cl_eset CL A),
  X X' -> X X'.

Class pointed (CL:color) (X:CPO.type CL) :=
  { bottom : X
  ; bottom_least : forall x, bottom x

Notation "⊥" := (@bottom _ _ _) : cpo_scope.

Hint Resolve bottom_least.

Every cppo has a least element, which arises as the supremum of the empty set.
Section bottom.
  Variables X Y:cppo.

  Lemma empty_semidirected : color_prop (directed_hf_cl true) (:eset X).

  Definition empty_dir : dirset X := exist _ empty_semidirected.

  Definition cppo_bot : X := empty_dir.

  Lemma cppo_bot_least : forall x, cppo_bot x.
End bottom.

Instance cppo_pointed (X:cppo) : pointed X :=
  { bottom := cppo_bot X; bottom_least := cppo_bot_least X }.

Every Scott-continuous map between cppos preserves the bottom element, i.e., is strict.
Lemma strict_map (X Y:cppo) (f:X Y) : f .

Chain suprema and least fixed points

A chain is specified by a base case a monotone operation to iterate, where base ≤ step base.
Every chain gives rise to a directed set and thus has a suprema. Suprema of chains have a nice induction principle.
Require Import NArith.

Lemma Niter_succ A f (a:A) : forall n,
  N.iter (N.succ n) f a = f (N.iter n f a).

Definition admissible hf (X:dcpo hf) (P:X -> Prop) (q:X) :=
  P q /\ forall XS:dirset X, q XS -> (forall x, x XS -> P x) -> P (XS).

Section iter_chain.
  Variable hf:bool.
  Variable X:dcpo hf.

  Variable base : X.
  Variable step : X -> X.

  Hypothesis step_mono : forall x y, x y -> step x step y.
  Hypothesis step_base : base step base.

  Definition iter_chain_set : eset X :=
    fun n => Some (N.iter n step base).

  Lemma iter_le : forall n1 n2,
    (n1 <= n2)%N -> N.iter n1 step base N.iter n2 step base.

  Lemma iter_set_directed : color_prop (directed_hf_cl hf) iter_chain_set.

  Definition iter_chain : dirset X :=
    exist _ iter_chain_set iter_set_directed.

  Lemma iter_chain_base :
    base iter_chain.

  Lemma iter_chain_step : forall x,
    x iter_chain -> step x iter_chain.

  Definition chain_sup : X := iter_chain.

  Lemma chain_induction (P:X -> Prop) :
    admissible P base ->
    (forall x y, x y -> P x -> P y) ->
    (forall x, P x -> P (step x)) ->
    P chain_sup.
End iter_chain.

The least-fixed point of a continous function in a cpo arises as a particular instance of a chain suprema, and the Scott induction principle is an instance of chain induction.
Section lfp.
  Variable X:cpo.
  Variable f:X X.
  Variable Hpointed : pointed X.

  Definition lfp := chain_sup false X f (CPO.mono f) (bottom_least (f )).

  Lemma scott_induction (P:X -> Prop) :
    admissible P ->
    (forall x y, x y -> P x -> P y) ->
    (forall x, P x -> P (f x)) ->
    P lfp.

  Lemma lfp_least : forall x, f x x -> lfp x.

  Lemma lfp_fixpoint : f lfp lfp.
End lfp.

The least-fixed point in cpos is uniform. This fact is somtimes called Plotkin's axiom.
Lemma lfp_uniform (D E:cpo)
  (HD:pointed D) (HE:pointed E)
  (f:D E) (d:D D) (e:E E) :

  f ->
  e f f d ->
  lfp e f (lfp d).