Library UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo

Tom de Jong
Created: November 2018
Refactored: January 2019
**************************************************************************** Note: a newer and different implementation of DCPOs and fixed point theorems can be found in OrderTheory.DCPOs. ****************************************************************************

Directed complete posets and least fixed points

Contents


Require Import UniMath.Foundations.All.

Local Open Scope poset.

Least upper bounds

Section leastupperbound.
Context {X : Poset}.
Context {I : UU}.
Variable (f : I -> X).
Definition isupperbound (u : X) : UU := (i : I), f i u.
Lemma isaprop_isupperbound (u : X) : isaprop (isupperbound u).
Show proof.
  apply impred_isaprop; intro i; apply propproperty.

Definition islub (u : X) : UU := isupperbound u ×
                                  (y : X), ( (i : I), f i y) -> u y.
Lemma isaprop_islub (u : X) : isaprop (islub u).
Show proof.
  apply isapropdirprod.
  - apply isaprop_isupperbound.
  - apply impred_isaprop; intro x.
    apply isapropimpl; apply propproperty.

Definition islub_isupperbound {u : X} : islub u -> isupperbound u := pr1.
Definition islub_isleast {u : X} :
  islub u -> (y : X), ( (i : I), f i y) -> u y := pr2.

Lemma lubsareunique {u v : X} : islub u -> islub v -> u = v.
Show proof.
  intros islubu islubv.
  apply isantisymm_posetRelation.
  - apply (islub_isleast islubu). exact (islub_isupperbound islubv).
  - apply (islub_isleast islubv). exact (islub_isupperbound islubu).

End leastupperbound.

Directed families

Section directedfamily.
Context {X : Poset}.
Context {I : UU}.

Definition isdirected (f : I -> X) : UU :=
   I × (i j : I), (k : I), f i f k × f j f k.
Lemma isaprop_isdirected (f : I -> X) : isaprop (isdirected f).
Show proof.
  apply isapropdirprod.
  - apply isapropishinh.
  - apply impred_isaprop; intro i; apply impred_isaprop; intro j.
    apply isapropishinh.

Definition directeduntruncated (f : I -> X) (i j : I) : UU :=
   (k : I), f i f k × f j f k.

Definition isdirected_inhabited {f : I -> X} :
  isdirected f -> I := pr1.
Definition isdirected_compatible {f : I -> X} :
  isdirected f -> (i j : I), (k : I), f i f k × f j f k := pr2.

End directedfamily.

Directed complete posets (dcpos)

Section dcpo.
Definition isdirectedcomplete (X : Poset) : UU :=
   (I : UU) (f : I -> X), isdirected f -> (u : X), islub f u.
Lemma isaprop_isdirectedcomplete (X : Poset) : isaprop (isdirectedcomplete X).
Show proof.
  apply impred_isaprop; intro I.
  apply impred_isaprop; intro f.
  apply isapropimpl.
  apply invproofirrelevance.
  intros [u p] [v q].
  apply total2_paths_equiv.
  exists (lubsareunique _ p q).
  apply proofirrelevance. apply isaprop_islub.

Definition dcpo := (X : Poset), isdirectedcomplete X.
Definition dcpoposet : dcpo -> Poset := pr1.
Coercion dcpoposet : dcpo >-> Poset.
Definition dcpoisdirectedcomplete (D : dcpo) : isdirectedcomplete D := pr2 D.
Definition make_dcpo (X : Poset) (i : isdirectedcomplete X) : dcpo := (X,,i).

Definition make_dcpo_lub {D : dcpo} {I : UU} {f : I -> D} : isdirected f -> D.
Show proof.
  intro isdirec.
  exact (pr1 (dcpoisdirectedcomplete D I f isdirec)).

Definition make_dcpo_lub_islub {D : dcpo} {I : UU} {f : I -> D}
           (isdirec : isdirected f) : islub f (make_dcpo_lub isdirec).
Show proof.
  exact (pr2 (dcpoisdirectedcomplete D I f isdirec)).

End dcpo.

Morphisms of dcpos


Section morphismofdcpos.
Definition preserveslub {P Q : Poset} (f : P -> Q) {I : UU} (u : I -> P) : UU :=
   (v : P), islub u v -> islub (f u) (f v).
Lemma isaprop_preserveslub {P Q : Poset} (f : P -> Q) {I : UU} (u : I -> P) :
  isaprop (preserveslub f u).
Show proof.
  apply impred_isaprop; intro v.
  apply isapropimpl. apply isaprop_islub.

Definition isdcpomorphism {D D' : dcpo} (f : D -> D') :=
  isaposetmorphism f ×
   (I : UU) (u : I -> D), isdirected u -> preserveslub f u.
Lemma isaprop_isdcpomorphism {D D' : dcpo} (f : D -> D') :
  isaprop (isdcpomorphism f).
Show proof.
  apply isapropdirprod.
  - apply isaprop_isaposetmorphism.
  - apply impred_isaprop; intro I.
    apply impred_isaprop; intro u.
    apply isapropimpl; apply isaprop_preserveslub.

Definition dcpomorphism (D D' : dcpo) := (f : D -> D'), isdcpomorphism f.

Definition dcpomorphism_posetmorphism (D D' : dcpo) :
  dcpomorphism D D' -> posetmorphism D D'.
Show proof.
  intros [f isdcpomor].
  exists f. exact (pr1 isdcpomor).
Coercion dcpomorphism_posetmorphism : dcpomorphism >-> posetmorphism.

Lemma dcpomorphism_preservesorder {D D' : dcpo} (f : dcpomorphism D D') :
  isaposetmorphism f.
Show proof.
  exact (pr1 (pr2 f)).

Lemma dcpomorphism_preservesdirected {D D' : dcpo} (f : dcpomorphism D D')
      {I : UU} {u : I -> D} : isdirected u -> isdirected (pr1 f u).
Show proof.
  intro isdirec.
  split.
  - exact (isdirected_inhabited isdirec).
  - intros i j. apply (@factor_through_squash (directeduntruncated u i j)).
    + apply isapropishinh.
    + intro direc. apply hinhpr. induction direc as [k ineqs].
      split with k. split.
      * apply dcpomorphism_preservesorder. exact (pr1 ineqs).
      * apply dcpomorphism_preservesorder. exact (pr2 ineqs).
    + exact (isdirected_compatible isdirec i j).

Lemma dcpomorphism_preserveslub {D D' : dcpo} (f : dcpomorphism D D')
           {I : UU} {u : I -> D} : isdirected u -> preserveslub f u.
Show proof.
  intro isdirec.
  apply (pr2 (pr2 f)).
  exact isdirec.

Definition isdcpomorphism' {D D' : dcpo} (f : D -> D') :=
   (I : UU) (u : I -> D), isdirected u -> preserveslub f u.

Lemma preservesdirectedlub_isdcpomorphism {D D' : dcpo} (f : D -> D') :
  isdcpomorphism' f -> isdcpomorphism f.
Show proof.
  intro preservesdireclub.
  split.
  - intros x y ineq.
    set (two := coprod unit unit).
    set (fam := (λ t : two, match t with | inl _ => x | inr _ => y end)).
    assert (isdirec : isdirected fam).
    { split.
      - apply hinhpr. exact (inl tt).
      - intros i j. apply hinhpr. exists (inr tt).
        induction i, j.
        + simpl. exact (ineq,,ineq).
        + simpl. split.
          ++ exact ineq.
          ++ apply isrefl_posetRelation.
        + simpl. split.
          ++ apply isrefl_posetRelation.
          ++ exact ineq.
        + simpl. split.
          ++ apply isrefl_posetRelation.
          ++ apply isrefl_posetRelation. }
    assert (islubfam : islub fam y).
    { split.
      - intro t. induction t.
        + simpl. exact ineq.
        + simpl. apply isrefl_posetRelation.
      - intros d ineqs. exact (ineqs (inr tt)). }
    set (islubfam' := preservesdireclub two fam isdirec y islubfam).
    apply (islub_isupperbound (f fam) islubfam' (inl tt)).
  - exact preservesdireclub.

Definition make_dcpomorphism {D D' : dcpo}
           (f : D -> D') (i : isdcpomorphism' f) : dcpomorphism D D'.
Show proof.
  exists f.
  apply preservesdirectedlub_isdcpomorphism. exact i.

Constant functions between dcpos are continuous
Definition const_dcpomor (D E : dcpo) (e : E) : dcpomorphism D E.
Show proof.
  use make_dcpomorphism.
  - exact (λ _, e).
  - intros I u isdirec v islubv. split.
    + intro i. simpl. apply isrefl_posetRelation.
    + intros d' ineqs. apply (@factor_through_squash I).
      * apply propproperty.
      * intro i. exact (ineqs i).
      * exact (isdirected_inhabited isdirec).

End morphismofdcpos.

The morphisms between two dcpos form a dcpo with the pointwise order.

Section morphismsofdcpos_formdcpo.
Definition pointwiseorder (D D' : dcpo) : hrel (dcpomorphism D D').
Show proof.
  intros f g. use make_hProp.
  - exact ( (d : D), f d g d).
  - apply impred_isaprop; intro d. apply propproperty.

Lemma ispartialorder_pointwiseorder (D D' : dcpo) :
  isPartialOrder (pointwiseorder D D').
Show proof.
  split.
  - split.
    + intros f g h ineq1 ineq2 d.
      eapply istrans_posetRelation.
      ++ use ineq1.
      ++ use ineq2.
    + intros f p. apply isrefl_posetRelation.
  - intros f g ineq1 ineq2. apply total2_paths_equiv.
    assert (funeq : pr1 f = pr1 g).
    { use funextfun; intro d. apply isantisymm_posetRelation.
      - use ineq1.
      - use ineq2. }
    exists funeq.
    apply proofirrelevance, isaprop_isdcpomorphism.

Definition posetofdcpomorphisms (D D' : dcpo) : Poset.
Show proof.
  use make_Poset.
  - use make_hSet.
    + exact (dcpomorphism D D').
    + apply (isofhleveltotal2 2).
      ++ apply impred_isaset; intro d.
         apply setproperty.
      ++ intro f; apply isasetaprop, isaprop_isdcpomorphism.
  - use make_PartialOrder.
    + apply pointwiseorder.
    + apply ispartialorder_pointwiseorder.

Lemma lubpreservesorder {X : Poset} {I : UU} (u v : I -> X) :
  ( (i : I), u i v i) ->
   (lu lv : X), islub u lu -> islub v lv -> lu lv.
Show proof.
  intros ineqs lu lv islubu islubv.
  eapply islub_isleast.
  - exact islubu.
  - intro i. eapply istrans_posetRelation.
    + exact (ineqs i).
    + apply (islub_isupperbound v islubv).

Given a family of dcpo morphisms from D to D' and a point d : D we have a pointwise family in D' by evaluating each morphism at d.
Definition pointwisefamily {D D' : dcpo} {I : UU}
           (F : I -> dcpomorphism D D') : D -> I -> D' :=
  λ (d : D), λ (i : I), (F i) d.

Lemma pointwisefamily_isdirected {D D' : dcpo} {I : UU}
      (F : I -> posetofdcpomorphisms D D') :
  isdirected F -> (d : D), isdirected (pointwisefamily F d).
Show proof.
  intros isdirec d. split.
  - exact (isdirected_inhabited isdirec).
  - intros i j. use factor_through_squash.
    + exact (directeduntruncated F i j).
    + apply isapropishinh.
    + intro direc. apply hinhpr.
      induction direc as [k ineqs].
      exists k. unfold pointwisefamily.
      induction ineqs as [ineq1 ineq2]. split.
      * use ineq1.
      * use ineq2.
    + apply (isdirected_compatible isdirec).

Definition pointwiselub {D D' : dcpo} {I : UU}
           (F : I -> posetofdcpomorphisms D D') (isdir : isdirected F) : D -> D'.
Show proof.
  intro d.
  set (ptfamdir := pointwisefamily_isdirected F isdir d).
  exact (make_dcpo_lub ptfamdir).

Lemma pointwiselub_islubpointwise {D D' : dcpo} {I : UU}
      (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) :
   (d : D), islub (pointwisefamily F d) (pointwiselub F isdirec d).
Show proof.
  intro d.
  set (ptfamdir := pointwisefamily_isdirected F isdirec d).
  exact (make_dcpo_lub_islub ptfamdir).

Lemma pointwiselub_preservesorder {D D' : dcpo} {I : UU}
      (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) :
  isaposetmorphism (pointwiselub F isdirec).
Show proof.
  intros x y ineq. use lubpreservesorder.
  - exact I.
  - intro i. apply (F i). exact x.
  - intro i. apply (F i). exact y.
  - intro i. simpl.
    apply dcpomorphism_preservesorder.
    exact ineq.
  - simpl. apply pointwiselub_islubpointwise.
  - simpl. apply pointwiselub_islubpointwise.

Lemma pointwiselub_isdcpomorphism' {D D' : dcpo} {I : UU}
      (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) :
  isdcpomorphism' (pointwiselub F isdirec).
Show proof.
  unfold isdcpomorphism'. intros J v isdirecv.
  intros w wislub.
  split.
  - intro j. apply pointwiselub_preservesorder.
    apply islub_isupperbound. exact wislub.
  - intros d' ineqs.
    eapply islub_isleast.
    + apply pointwiselub_islubpointwise.
    + intro i. unfold pointwisefamily.
      eapply dcpomorphism_preserveslub.
      * exact isdirecv.
      * exact wislub.
      * intro j. eapply istrans_posetRelation.
        2: { exact (ineqs j). }
        apply pointwiselub_islubpointwise.

Lemma pointwiselub_islub {D D' : dcpo} {I : UU}
      (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) :
  islub F (make_dcpomorphism (pointwiselub F isdirec)
                            (pointwiselub_isdcpomorphism' F isdirec)).
Show proof.
  split.
  - intro i; simpl. intro d; simpl.
    apply pointwiselub_islubpointwise.
  - intros h ineqs; simpl. intro d; simpl.
    apply pointwiselub_islubpointwise.
    intro i. use (ineqs i).

Lemma islub_islubpointwise {D D' : dcpo} {I : UU} {g : posetofdcpomorphisms D D'}
      {F : I -> posetofdcpomorphisms D D'} (isdirec : isdirected F) :
  islub F g -> (d : D), islub (pointwisefamily F d) (pr1 g d).
Show proof.
  intros islubFg d.
  set (ptlub := make_dcpomorphism (pointwiselub F isdirec)
                               (pointwiselub_isdcpomorphism' F isdirec)).
  assert (lubeq : g = ptlub).
  { apply (lubsareunique F islubFg).
    apply pointwiselub_islub. }
  rewrite lubeq.
  apply pointwiselub_islubpointwise.

Lemma posetofdcpomorphisms_isdirectedcomplete (D D' : dcpo) :
  isdirectedcomplete (posetofdcpomorphisms D D').
Show proof.
  intros I F isdirec.
  exists (make_dcpomorphism (pointwiselub F isdirec)
                         (pointwiselub_isdcpomorphism' F isdirec)).
  apply pointwiselub_islub.

Definition dcpoofdcpomorphisms (D D' : dcpo) : dcpo.
Show proof.
  eapply make_dcpo.
  - exact (posetofdcpomorphisms_isdirectedcomplete D D').
End morphismsofdcpos_formdcpo.

Dcpos with bottom

Section dcpowithbottom.
Definition dcpowithbottom := (D : dcpo), (l : D), isMinimal l.
Definition dcpowithbottom_dcpo : dcpowithbottom -> dcpo := pr1.
Coercion dcpowithbottom_dcpo : dcpowithbottom >-> dcpo.
Definition dcpowithbottom_isMinimal (D : dcpowithbottom) := (pr2 (pr2 D)).
Definition dcpowithbottom_bottom (D : dcpowithbottom) := pr1 (pr2 D).

Definition dcpowithbottom_ofdcpomorphisms (D D' : dcpowithbottom) :
  dcpowithbottom.
Show proof.
  exists (dcpoofdcpomorphisms D D').
  set (leastD' := dcpowithbottom_bottom D').
  set (l := const_dcpomor D D' leastD').
  exists l.
  intro f. simpl. intro d.
  apply dcpowithbottom_isMinimal.

End dcpowithbottom.

Declare Scope DCPO.
Delimit Scope DCPO with DCPO.
Local Open Scope DCPO.
Notation "A --> B" := (dcpowithbottom_ofdcpomorphisms A B) : DCPO.

The least fixed point

Section leastfixedpoint.

Definition iter {D : dcpowithbottom} (n : nat) (f : D --> D) : D.
Show proof.
  induction n as [ | m IH].
  - exact (dcpowithbottom_bottom D).
  - apply f. exact IH.

Lemma iter_preservesorder {D : dcpowithbottom} (f g : D --> D) :
  (f g) -> (n : nat), (iter n f iter n g).
Show proof.
  intros ineq n; induction n as [ | m IH].
  - apply isrefl_posetRelation.
  - simpl. eapply istrans_posetRelation.
    + apply dcpomorphism_preservesorder. exact IH.
    + use ineq.

Next, we show that each iter n is continuous, but first a small lemma. It could be generalised using monotone nets, c.f. Proposition 2.1.12 in Abramsky's and Jung's chapter "Domain Theory" in "Handbook of Logic in Computer Science". We're saying that: ⊔ f^(n+1)(⊥) = ⊔ g(⊔ f^n(⊥)), where f,g are in the family F. One inequality is easy; the other crucially relies on the fact that F is directed.
Lemma doublelubdirected {D : dcpowithbottom} {I : UU} (F : I -> D -->D)
      (isdirec : isdirected F) (n : nat) (u u' : D) :
  islub (λ i : I, iter n (F i)) u' -> islub (λ j : I, (pr1) (F j) u') u ->
  islub (λ i : I, iter (S n) (F i)) u.
Show proof.
  intros islubu' islubu.
  split.
  - intro i.
    simpl. eapply istrans_posetRelation.
    + apply dcpomorphism_preservesorder.
      apply (islub_isupperbound _ islubu').
    + apply (islub_isupperbound _ islubu).
  - intros d ineqs.
    apply (islub_isleast _ islubu).
    intro i.
    set (fam := λ i : I, iter n (F i)).
    assert (isdirec' : isdirected (λ i : I, iter n (F i))).
    { split.
      - exact (isdirected_inhabited isdirec).
      - intros i1 i2.
        use factor_through_squash.
        + exact (directeduntruncated F i1 i2).
        + apply isapropishinh.
        + intro direc. apply hinhpr.
          induction direc as [k ineqs'].
          exists k.
          split.
          * apply iter_preservesorder. exact (pr1 ineqs').
          * apply iter_preservesorder. exact (pr2 ineqs').
        + apply (isdirected_compatible isdirec).
    }
    eapply dcpomorphism_preserveslub.
    + exact isdirec'.
    + exact islubu'.
    + intro j. simpl.
      use factor_through_squash.
      * exact (directeduntruncated F i j).
      * apply propproperty.
      * intro direc. induction direc as [k ineqs'].
        eapply istrans_posetRelation.
        -- apply dcpomorphism_preservesorder.
           apply iter_preservesorder.
           apply (pr2 ineqs').
        -- eapply istrans_posetRelation.
           ++ use (pr1 ineqs').
           ++ exact (ineqs k).
      * apply (isdirected_compatible isdirec).

Lemma iter_isdcpomorphism' (D : dcpowithbottom) :
   (n : nat), isdcpomorphism' (@iter D n).
Show proof.
  intros n I F isdirec g islubg.
  induction n as [| m IH].
  - split.
    + intro i. simpl. apply dcpowithbottom_isMinimal.
    + intros y ineqs. apply dcpowithbottom_isMinimal.
  - simpl. eapply doublelubdirected.
    + exact isdirec.
    + exact IH.
    + set (islub' := pointwiselub_islub F isdirec).
      set (eq := lubsareunique _ islubg islub').
      rewrite eq; cbn.
      apply pointwiselub_islubpointwise.

Iter as dcpo morphism
Definition iter' {D : dcpowithbottom} (n : nat) : (D --> D) --> D.
Show proof.
  eapply make_dcpomorphism.
  exact (iter_isdcpomorphism' D n).

Lemma iter'_isomegachain (D : dcpowithbottom) :
   (n : nat), (@iter' D n @iter' D (S n)).
Show proof.
  induction n as [ | m IH].
  - simpl. intro f. apply dcpowithbottom_isMinimal.
  - simpl. intro f. apply dcpomorphism_preservesorder. use IH.

Lemma iter'_increases (D : dcpowithbottom) :
   (n m : nat), (n m)%nat -> (@iter' D n @iter' D m).
Show proof.
  intros n m ineq.
  induction m as [ | m' IH].
  - set (nis0 := natleh0tois0 ineq).
    rewrite nis0. apply isrefl_posetRelation.
  - set (cases := natlehchoice _ _ ineq).
    induction cases as [less | equal].
    + eapply istrans_posetRelation.
      * apply IH. apply less.
      * apply iter'_isomegachain.
    + rewrite equal. apply isrefl_posetRelation.

Lemma iter'_isdirected (D : dcpowithbottom) :
  isdirected (@iter' D).
Show proof.
  split.
  - apply hinhpr. exact O.
  - intros n m. apply hinhpr. exists (n + m).
    split.
    + apply iter'_increases. apply natlehnplusnm.
    + apply iter'_increases, natlehmplusnm.

Definition leastfixedpoint {D : dcpowithbottom} : (D --> D) --> D.
Show proof.
  use make_dcpomorphism.
  - eapply pointwiselub.
    apply iter'_isdirected.
  - apply pointwiselub_isdcpomorphism'.

Notation "'μ'" := leastfixedpoint : DCPO.

Lemma leastfixedpoint_isfixedpoint {D : dcpowithbottom} :
   (f : D --> D), (pr1 f) (pr1 μ f) = pr1 μ f.
Show proof.
  intro f. unfold leastfixedpoint; cbn.
  apply isantisymm_posetRelation.
  - set (isdirec := pointwisefamily_isdirected iter' (iter'_isdirected D) f).
    eapply dcpomorphism_preserveslub.
    + exact isdirec.
    + apply pointwiselub_islubpointwise.
    + intro n. simpl.
      eapply (istrans_posetRelation _ _ (pointwisefamily iter' f (S n)) _).
      * apply isrefl_posetRelation.
      * apply pointwiselub_islubpointwise.
  - eapply (islub_isleast).
    + apply pointwiselub_islubpointwise.
    + intro n. induction n as [ | m IH].
      * apply dcpowithbottom_isMinimal.
      * unfold pointwisefamily; simpl. apply dcpomorphism_preservesorder.
        eapply istrans_posetRelation.
        -- use iter'_increases.
           ++ exact (S m).
           ++ apply natlehnsn.
        -- exact (islub_isupperbound _
                  (pointwiselub_islubpointwise iter' (iter'_isdirected D) f)
                  (S m)).

Lemma leastfixedpoint_isleast {D : dcpowithbottom} (f : D --> D) :
   (d : D), ((pr1 f) d d) -> (pr1 μ f d).
Show proof.
  intros d ineq.
  eapply islub_isleast.
  - apply pointwiselub_islubpointwise.
  - intro n; induction n as [ | m IH].
    + apply dcpowithbottom_isMinimal.
    + unfold pointwisefamily. simpl.
      eapply istrans_posetRelation.
      * apply dcpomorphism_preservesorder. exact IH.
      * exact ineq.

Close Scope DCPO.

End leastfixedpoint.