Library UniMath.OrderTheory.DCPOs.FixpointTheorems.LeastFixpoint
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.Posets.Basics.
Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.
Require Import UniMath.OrderTheory.Posets.PointedPosets.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.
Require Import UniMath.OrderTheory.DCPOs.Examples.Fixpoints.
Require Import UniMath.OrderTheory.DCPOs.Examples.Exponentials.
Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.
Local Open Scope dcpo.
Section FixpointTheorem.
Context {X : dcppo}
(f : scott_continuous_map X X).
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.Posets.Basics.
Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.
Require Import UniMath.OrderTheory.Posets.PointedPosets.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.
Require Import UniMath.OrderTheory.DCPOs.Examples.Fixpoints.
Require Import UniMath.OrderTheory.DCPOs.Examples.Exponentials.
Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.
Local Open Scope dcpo.
Section FixpointTheorem.
Context {X : dcppo}
(f : scott_continuous_map X X).
1. The least fixpoint
Definition bot_iteration_map
(n : ℕ)
: X.
Show proof.
Lemma is_monotone_bot_iteration_map_S
(n : ℕ)
: bot_iteration_map n ⊑ f (bot_iteration_map n).
Show proof.
Definition bot_iteration_directed_set
: directed_set X.
Show proof.
Definition least_fixpoint
: X
:= ⨆ bot_iteration_directed_set.
Proposition is_fixpoint_least_fixpoint
: f least_fixpoint = least_fixpoint.
Show proof.
Theorem is_least_fixpoint_least_fixpoint
(x : X)
(p : f x = x)
: least_fixpoint ⊑ x.
Show proof.
Definition bottom_element_fixpoint_dcpo
: bottom_element (fixpoint_dcpo f).
Show proof.
(n : ℕ)
: X.
Show proof.
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).
- apply is_min_bottom_dcppo.
- exact (is_monotone_scott_continuous_map f IHn).
Definition bot_iteration_directed_set
: directed_set X.
Show proof.
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.
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).
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)).
- 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.
: 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.
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.
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.
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.
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.
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.
{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).
- 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.
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.
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).
- 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).
- 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.
- 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.