Library fixes


Require Import String.
Require Import List.
Require Import Setoid.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import cpo.
Require Import profinite.
Require Import profinite_adj.

A fixpoint operator for nonstrict functions in PLT.


Program Definition precompose hf (A B C:PLT.PLT hf) (f:A B) :
  (Preord.hom (PLT.hom_ord hf B C) (PLT.hom_ord hf A C)) :=
  Preord.Hom (PLT.hom_ord hf B C) (PLT.hom_ord hf A C)
     (fun g => g f) _.

Program Definition postcompose hf (A B C:PLT.PLT hf) (g:B C) :
  (Preord.hom (PLT.hom_ord hf A B) (PLT.hom_ord hf A C)) :=
  Preord.Hom (PLT.hom_ord hf A B) (PLT.hom_ord hf A C)
      (fun f => g f) _.

Lemma precompose_continuous hf (A B C:PLT.PLT hf) (f:A B) :
  continuous (directed_hf_cl hf) (precompose C f).

Lemma postcompose_continuous hf (A B C:PLT.PLT hf) (g:B C) :
  continuous (directed_hf_cl hf) (postcompose A g).

Program Definition pair_right hf (A B C:PLT.PLT hf) (f:C A) :
  (Preord.hom (PLT.hom_ord hf C B) (PLT.hom_ord hf C (PLT.prod A B))) :=
  Preord.Hom (PLT.hom_ord hf C B) (PLT.hom_ord hf C (PLT.prod A B))
  (fun g => PLT.pair f g) _.

Program Definition pair_left hf (A B C:PLT.PLT hf) (g:C B) :
  (Preord.hom (PLT.hom_ord hf C A) (PLT.hom_ord hf C (PLT.prod A B))) :=
  Preord.Hom (PLT.hom_ord hf C A) (PLT.hom_ord hf C (PLT.prod A B))
  (fun f => PLT.pair f g) _.

Lemma pair_right_continuous hf (A B C:PLT.PLT hf) (f:C A) :
  continuous (directed_hf_cl hf) (pair_right B f).

Lemma pair_left_continuous hf (A B C:PLT.PLT hf) (g:C B) :
  continuous (directed_hf_cl hf) (pair_left A g).

Section fixes.
  Variable Γ:PLT.
  Variable A:PLT.
  Variable f:Γ U A U A.

  Definition fixes_step
    (x:Γ U A) : Γ U A :=

    apply f, x.

  Program Definition fixes_step' :
    PLT.homset_cpo _ Γ (U A) PLT.homset_cpo _ Γ (U A) :=

    CPO.Hom _ (PLT.homset_cpo _ Γ (U A)) (PLT.homset_cpo _ Γ (U A))
    fixes_step _ _.

  Definition fixes : Γ U A := lfp fixes_step'.

  Lemma fixes_unroll :
    fixes apply f, fixes.

End fixes.

Lemma fixes_mono Γ A (f g:Γ U A U A) :
  f g -> fixes Γ A f fixes Γ A g.

Lemma fixes_eq Γ A (f g:Γ U A U A) :
  f g -> fixes Γ A f fixes Γ A g.

Add Parametric Morphism Γ A :
  (fixes Γ A)
  with signature (Preord.ord_op _ ==> Preord.ord_op _)
  as fixes_le_morphism.

Add Parametric Morphism Γ A :
  (fixes Γ A)
  with signature (eq_op _ ==> eq_op _)
  as fixes_morphism.

Lemma plt_bot_None A B x y :
  (x,y) PLT.hom_rel ( : A U B) <-> y = None.

Lemma plt_bot_chomp A B C (g:A B) :
  ( : B U C) g .

Lemma fixes_compose_commute Γ Γ' A f (g:Γ' Γ) :
  fixes Γ A f g fixes Γ' A (f g).