Library UniMath.OrderTheory.DCPOs.FixpointTheorems.LeastFixpoint

1. The least fixpoint
  Definition bot_iteration_map
             (n : )
    : X.
  Show proof.
    induction n as [ | n IHn ].
    - exact (_{X}).
    - exact (f IHn).

  Lemma is_monotone_bot_iteration_map_S
        (n : )
    : bot_iteration_map n f (bot_iteration_map n).
  Show proof.
    induction n as [ | n IHn ].
    - apply is_min_bottom_dcppo.
    - exact (is_monotone_scott_continuous_map f IHn).

  Definition bot_iteration_directed_set
    : directed_set X.
  Show proof.
    use nat_directed_set.
    - exact bot_iteration_map.
    - apply is_monotone_bot_iteration_map_S.

  Definition least_fixpoint
    : X
    := bot_iteration_directed_set.

  Proposition is_fixpoint_least_fixpoint
    : f least_fixpoint = least_fixpoint.
  Show proof.
    unfold least_fixpoint.
    rewrite scott_continuous_map_on_lub.
    use antisymm_dcpo.
    - use dcpo_lub_is_least.
      cbn ; intro i.
      use less_than_dcpo_lub.
      + exact (S i).
      + apply refl_dcpo.
    - use dcpo_lub_is_least.
      cbn ; intro i.
      use less_than_dcpo_lub.
      + exact i.
      + apply is_monotone_bot_iteration_map_S.

  Theorem is_least_fixpoint_least_fixpoint
          (x : X)
          (p : f x = x)
    : least_fixpoint x.
  Show proof.
    use dcpo_lub_is_least ; cbn.
    intro n.
    induction n as [ | n IHn ].
    - apply is_min_bottom_dcppo.
    - rewrite <- p.
      exact (is_monotone_scott_continuous_map f IHn).

  Definition bottom_element_fixpoint_dcpo
    : bottom_element (fixpoint_dcpo f).
  Show proof.
    simple refine ((least_fixpoint ,, _) ,, _).
    - apply is_fixpoint_least_fixpoint.
    - exact (λ x, is_least_fixpoint_least_fixpoint _ (pr2 x)).

2. Pointed DCPPO of fixpoints
  Definition fixpoint_dcppo
    : dcppo
    := _ ,, pr2 (fixpoint_dcpo f) ,, bottom_element_fixpoint_dcpo.
End FixpointTheorem.

3. Continuous map that assigns to a function its least fixpoint
Definition iterate_on_pt_scott_continuous_map
           {X : dcpo}
           (n : )
  : scott_continuous_map (X × dcpo_funspace X X) X.
Show proof.
  induction n as [ | n IHn ].
  - exact π.
  - exact (comp_scott_continuous_map
              eval_scott_continuous_map X X , π
             IHn).

Proposition iterate_on_pt_scott_continuous_map_fun_pt
            {X : dcpo}
            (n : )
            (f : scott_continuous_map X X)
            (x : X)
  : iterate_on_pt_scott_continuous_map n (f x ,, f)
    =
    f (iterate_on_pt_scott_continuous_map n (x ,, f)).
Show proof.
  revert x.
  induction n as [ | n IHn ].
  - intro ; cbn.
    apply idpath.
  - intro x.
    simpl ; unfold prodtofuntoprod ; simpl.
    apply IHn.

Definition iterate_scott_continuous_map
           {X : dcppo}
           (n : )
  : scott_continuous_map (dcpo_funspace X X) (dcpo_funspace X X)
  := lam_scott_continuous_map (iterate_on_pt_scott_continuous_map n).

Definition iterate_scott_continuous_map_S
           {X : dcppo}
           (n : )
           (f : scott_continuous_map X X)
           (x : X)
  : pr1 (iterate_scott_continuous_map (S n) f) x
    =
    f (pr1 (iterate_scott_continuous_map n f) x).
Show proof.
  simpl ; unfold prodtofuntoprod ; simpl.
  exact (iterate_on_pt_scott_continuous_map_fun_pt n f x).

Definition least_fixpoint_scott_continuous_map_on_N
           {X : dcppo}
           (n : )
  : dcpo_funspace (dcpo_funspace X X) X
  := comp_scott_continuous_map
        constant_scott_continuous_map _ _{X} , iterate_scott_continuous_map n
       (eval_scott_continuous_map _ _).

Definition least_fixpoint_scott_continuous_map_directed_set
           (X : dcppo)
  : directed_set (dcpo_funspace (dcpo_funspace X X) X).
Show proof.
  use nat_directed_set.
  - exact least_fixpoint_scott_continuous_map_on_N.
  - abstract
      (intros i f ;
       simpl ; unfold prodtofuntoprod ; simpl ;
       use is_monotone_scott_continuous_map ;
       split ; [ apply is_min_bottom_dcppo | ] ;
       intro ;
       apply refl_dcpo).

Definition least_fixpoint_scott_continuous_map
           (X : dcppo)
  : dcpo_funspace (dcpo_funspace X X) X
  := least_fixpoint_scott_continuous_map_directed_set X.

Proposition least_fixpoint_scott_continuous_map_is_least_fixpoint_on_N
            {X : dcppo}
            (f : scott_continuous_map X X)
            (n : )
  : pr1 (least_fixpoint_scott_continuous_map_on_N n) f
    =
    bot_iteration_directed_set f n.
Show proof.
  induction n as [ | n IHn ].
  - apply idpath.
  - refine (_ @ maponpaths _ IHn).
    simpl ; unfold prodtofuntoprod ; simpl.
    apply (iterate_on_pt_scott_continuous_map_fun_pt n f).

Proposition least_fixpoint_scott_continuous_map_is_least_fixpoint
            {X : dcppo}
            (f : scott_continuous_map X X)
  : pr1 (least_fixpoint_scott_continuous_map X) f
    =
    least_fixpoint f.
Show proof.
  use antisymm_dcpo.
  - use dcpo_lub_is_least.
    intro i ; cbn in i.
    use less_than_dcpo_lub.
    + exact i.
    + rewrite <- least_fixpoint_scott_continuous_map_is_least_fixpoint_on_N.
      apply refl_dcpo.
  - use dcpo_lub_is_least.
    intro i ; cbn in i.
    use less_than_dcpo_lub.
    + exact i.
    + rewrite <- least_fixpoint_scott_continuous_map_is_least_fixpoint_on_N.
      apply refl_dcpo.