Library LambdaDInf
Add LoadPath "../domain-theory".
new in 8.4!
Set Automatic Coercions Import.
Unset Automatic Introduction.
Unset Automatic Introduction.
endof new in 8.4
Require Export PredomAll.
Require Import PredomRec.
Require Import DomainStuff.
Require Import Cppo_cppoECat.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Module Type RecDom.
Variable DInf : cppoType.
Definition VInf := (DInf -=> DInf).
Variable Roll : VInf =-> DInf.
Variable Unroll : DInf =-> VInf.
Variable RU_id : Roll << Unroll =-= Id.
Variable UR_id : Unroll << Roll =-= Id.
Variable delta : (DInf -=> DInf) =-> (DInf -=> DInf).
Variable delta_simpl : forall (e : DInf -=> DInf),
delta e =-= Roll <<
((exp_fun (CCOMP DInf DInf DInf
:cppoCatType _ _)
e : cppoCatType _ _)
<<
((exp_fun
((CCOMP DInf DInf DInf) << SWAP)
e : cppoCatType _ _)))
<< Unroll.
Variable delta_eta : delta Id =-= Id.
Variable id_min : Id =-= @FIXP _ delta.
End RecDom.
Module RD : RecDom.
Lemma summ_mon (F G : BiFunctor cppoBaseCatType) X Y Z W :
monotonic (fun p => [|
in1 << (morph F X Y Z W p : (ob F X Z) =-> (ob F Y W)),
in2 << (morph G X Y Z W p : (ob G X Z) =-> (ob G Y W))
|]
).
Proof.
move => F G X Y Z W. move => p p' l. simpl.
unfold sum_fun. simpl. unfold in1. simpl. unfold in2. simpl.
move => x. simpl. do 2 rewrite -> SUM_fun_simpl. case: x.
- move => s. by rewrite -> l.
- move => s. by rewrite -> l.
Qed.
Definition summ (F G : BiFunctor cppoBaseCatType) X Y Z W :=
Eval hnf in mk_fmono (@summ_mon F G X Y Z W).
Lemma sumc (F G : BiFunctor cppoBaseCatType) X Y Z W :
continuous (@summ F G X Y Z W).
Proof.
move => F G X Y Z W c. simpl.
repeat rewrite -> lub_comp_eq. unfold sum_fun. simpl.
intro s. destruct s; simpl.
- rewrite -> SUM_fun_simpl. simpl.
setoid_rewrite -> lub_comp_eq with (f:=INL (ob F Y W) (ob G Y W)).
apply lub_le_compat.
intro i. simpl. unfold sum_fun; simpl. by rewrite -> SUM_fun_simpl.
- rewrite -> SUM_fun_simpl. simpl.
setoid_rewrite -> lub_comp_eq with (f:=INR (ob F Y W) (ob G Y W)).
apply lub_le_compat.
intro i. simpl. unfold sum_fun; simpl. by rewrite -> SUM_fun_simpl.
Qed.
Definition sum_func (F G : BiFunctor cppoBaseCatType) X Y Z W :=
Eval hnf in mk_fcont (@sumc F G X Y Z W).
Lemma sum_func_simpl F G X Y Z W x :
@sum_func F G X Y Z W x =
[| in1 << (morph F X Y Z W x : (ob F X Z) =-> (ob F Y W)),
in2 << (morph G X Y Z W x : (ob G X Z) =-> (ob G Y W))
|].
by [].
Qed.
Definition prod_morph (A B C D : cpoType)
(fg : (A =-> B) * (C =-> D)) :=
prod_fun ((fst fg) << pi1) ((snd fg) << pi2).
Definition PRODm_morph (A B C D : cpoType):
monotonic (fun (fg : (A =-> B) * (C =-> D)) => (@prod_morph A B C D fg)).
Proof.
intros A B C D. intros (f, g) (f',g') l.
intros (a,c). simpl. destruct l. rewrite -> H, H0. auto.
Qed.
Definition prodm_morph (A B C D : cpoType) :=
Eval hnf in mk_fmono (@PRODm_morph A B C D).
Definition PRODc_morph (A B C D : cpoType) :
continuous (@prodm_morph A B C D ).
Proof.
intros A B C D. intros fgi. intros (a,c). simpl.
rewrite -> pair_lub. auto.
Qed.
Definition pprodc_morph (A B C D : cpoType) :=
Eval hnf in mk_fcont (@PRODc_morph A B C D).
Definition prodc_morph (A B C D : cpoType) := CURRY (pprodc_morph A B C D).
Arguments prodc_morph [A B C D].
Lemma prodm_mon (F G : BiFunctor cppoBaseCatType) X Y Z W :
monotonic (fun p : (cppoMorph Y X * cppoMorph Z W) =>
prodc_morph
((morph F X Y Z W p : (ob F X Z) =-> (ob F Y W)))
((morph G X Y Z W p : (ob G X Z) =-> (ob G Y W)))
).
move => F G X Y Z W. move => p p' l. simpl.
intros (xz,yz). simpl. by rewrite -> l.
Qed.
Definition prodm (F G : BiFunctor cppoBaseCatType) X Y Z W :=
Eval hnf in mk_fmono (@prodm_mon F G X Y Z W).
Lemma lub_prod_fun : forall (D1 D2 D3 D4 D5 : cpoType) (d2 : D2) (d4 : D4)
(f : cpoCatType D1 (D2 -=> D3)) (g : cpoCatType D1 (D4 -=> D5))
(h : ordCatType natO D1),
(f (lub h) >< g (lub h)) (d2,d4) =-= lub
(<| (mk_fmono (fcont_lub_mono (ocomp f h))) d2,
(mk_fmono (fcont_lub_mono (ocomp g h))) d4 |>).
Proof.
intros D1 D2 D3 D4 D5 d2 d4 f g h.
do 2 rewrite -> lub_comp_eq. simpl.
rewrite -> pair_lub. by simpl.
Qed.
Lemma prodc (F G : BiFunctor cppoBaseCatType) X Y Z W :
continuous (@prodm F G X Y Z W).
move => F G X Y Z W c. simpl.
set (mF := (morph F X Y Z W)).
set (mG := (morph G X Y Z W)).
unfold prod_morph. simpl.
intros (a,b). setoid_rewrite -> lub_prod_fun. simpl.
cbn. auto.
Qed.
Definition prod_func (F G : BiFunctor cppoBaseCatType) X Y Z W :=
Eval hnf in mk_fcont (@prodc F G X Y Z W).
Lemma Smash_ValVal : forall (A B : cpoType) (a : A) (b : B),
Smash _ _ (Val a) (Val b) =-= Val (a, b).
Proof.
intros A B a b.
unfold Smash, Operator2. unlock. simpl.
rewrite -> kleisliVal. simpl. rewrite -> kleisliVal.
simpl. rewrite -> kleisliVal. by simpl.
Qed.
Lemma pairl_mon (O0 O1 : ordType) (y:O1) : monotonic (fun (x:O0) => (x,y)).
move => O0 O1 x y y' l. by rewrite -> l.
Qed.
Definition Pairl (O0 O1 : ordType) (y:O1) : O0 =-> (O0 * O1) :=
Eval hnf in mk_fmono (pairl_mon y).
Lemma Pairl_cont (D0 D1 : cpoType) (y:D1) : continuous (@Pairl D0 D1 y).
move => D0 D1 y c. simpl. split.
- simpl. by apply lub_le_compat => i.
- simpl. by apply: (Ole_trans _ (le_lub (pi2 << (Pairl D0 y << c)) O)).
Qed.
Definition PAIRL (D0 D1 : cpoType) (y:D1) : D0 =-> D0 * D1 :=
Eval hnf in mk_fcont (Pairl_cont y).
Lemma PAIR_eq : forall (D0 D1 : cpoType) (x : D0),
SWAP << (@PAIR D0 D1) x =-= @PAIRL D1 D0 x.
Proof.
intros D0 D1 x. split; intros y; auto.
Qed.
Lemma Smash_Eps_l :
forall (A B : cpoType) (d : A _BOT) (d' : B _BOT),
(Smash A B) (Eps d) d' = Eps ((Smash A B) d d').
Proof.
intros A B d d'.
unfold Smash. unfold Operator2. unlock. simpl.
do 2 rewrite kleisli_simpl. do 2 rewrite kleisli_Eps.
by do 2 rewrite <- kleisli_simpl.
Qed.
Lemma Smash_Eps_r_leq :
forall (A B : cpoType) (d : A _BOT) (d' : B _BOT),
(Smash A B) d (Eps d') <= Eps ((Smash A B) d d').
Proof.
intros A B d d'.
unfold Smash, Operator2; unlock; simpl.
assert (
(kleisli ((uncurry KLEISLI << SWAP) << PAIR (B -=> (A * B) _BOT) (Eps d')))
((kleisli (eta << exp_fun eta)) d)
=-=
((kleisli ((uncurry KLEISLI << SWAP) << PAIR (B -=> (A * B) _BOT) (Eps d')))
<<
(kleisli (eta << exp_fun eta))) d
) by auto.
rewrite -> H; clear H.
rewrite <- kleisli_comp2. simpl.
repeat rewrite -> kleisli_simpl.
generalize dependent d.
cofix.
intros d.
destruct d.
repeat rewrite -> kleisli_Eps.
apply DLleEps. apply Smash_Eps_r_leq.
Guarded. repeat rewrite <- kleisli_simpl.
repeat rewrite -> kleisliVal. simpl.
rewrite -> kleisli_simpl.
rewrite -> kleisli_Eps.
apply DLleEps.
rewrite -> kleisliVal.
assert (((eta << exp_fun eta) s) = (Val (eta << PAIR B s))) by auto.
setoid_rewrite -> H. clear H.
rewrite -> kleisliVal.
rewrite <- kleisli_simpl.
simpl. apply DLle_refl.
Qed.
Lemma Smash_Eps_r_leq' :
forall (A B : cpoType) (d : A _BOT) (d' : B _BOT),
Eps ((Smash A B) d d') <= (Smash A B) d (Eps d').
Proof.
intros A B d d'.
unfold Smash, Operator2; unlock; simpl.
assert (
(kleisli ((uncurry KLEISLI << SWAP) << PAIR (B -=> (A * B) _BOT) (Eps d')))
((kleisli (eta << exp_fun eta)) d)
=-=
((kleisli ((uncurry KLEISLI << SWAP) << PAIR (B -=> (A * B) _BOT) (Eps d')))
<<
(kleisli (eta << exp_fun eta))) d
) by auto.
rewrite -> H; clear H.
rewrite <- kleisli_comp2. simpl.
repeat rewrite -> kleisli_simpl.
generalize dependent d.
cofix.
intros d.
destruct d.
repeat rewrite -> kleisli_Eps.
apply DLleEps. apply Smash_Eps_r_leq'.
Guarded. clear Smash_Eps_r_leq'.
apply DLleEps_left.
Guarded.
repeat rewrite <- kleisli_simpl.
repeat rewrite -> kleisliVal. simpl.
rewrite -> kleisliVal. simpl.
do 2 rewrite -> kleisli_simpl.
rewrite -> kleisli_Eps.
apply DLleEps_right.
apply DLle_refl.
Qed.
Lemma Smash_Eps_r :
forall (A B : cpoType) (d : A _BOT) (d' : B _BOT),
(Smash A B) d (Eps d') =-= Eps ((Smash A B) d d').
Proof.
intros A B d d'.
split.
apply Smash_Eps_r_leq.
apply Smash_Eps_r_leq'.
Qed.
Lemma Smash_Val : forall (A B : cpoType) (a : A) (b : B _BOT),
(Smash A B) (Val a) b = (kleisli (eta << PAIR B a)) b.
Proof.
intros A B a b.
unfold Smash. unfold Operator2. unlock. simpl.
do 2 rewrite kleisli_simpl. repeat rewrite kleisli_Val. by simpl.
Qed.
Lemma able : forall (A B C D : cpoType)
(fa : A =-> C _BOT) (fb : B =-> D _BOT) (a : A),
(uncurry (Smash C D) << prod_morph (fa, fb)) << PAIR B a
=-=
(Smash C D) (fa a) << fb.
Proof.
intros A B C D fa fb a.
split; intro b; by simpl.
Qed.
Lemma miguel : forall (A B C : cpoType)
(f : B =-> C _BOT) (a : A _BOT) b,
(((Smash A C) a) << kleisli f) b =-= (kleisli ((Smash A C) a << f)) b.
Proof.
intros A B C f a b.
repeat rewrite kleisli_simpl.
rewrite kleislit_comp.
simpl. by rewrite kleisli_simpl.
intros x xx0 H.
unfold Smash, Operator2 in H; unlock in H; simpl in H.
apply kleisliValVal in H. destruct H as [fc [? ?]].
apply kleisliValVal in H. destruct H as [a' [? ?]].
apply kleisliValVal in H0. destruct H0 as [c' [? ?]].
simpl in *.
exists c'. auto.
Qed.
Lemma Smash_prop_r : forall (B C E F : cpoType)
(fa : B =-> C _BOT) (ga : B _BOT)
(fb : E =-> F _BOT) (gb : E _BOT),
Smash _ _ ((kleislit fa) ga) ((kleislit fb) gb)
<=
kleislit (uncurry (Smash _ _ ) << prod_morph (fa, fb))
(Smash _ _ ga gb).
Proof.
cofix.
intros B C E F fa ga fb gb.
destruct ga. rewrite Smash_Eps_l.
repeat rewrite -> kleisli_Eps.
rewrite Smash_Eps_l. apply DLleEps.
apply Smash_prop_r.
Guarded.
rewrite -> Smash_Val.
rewrite <- kleisli_simpl.
rewrite -> kleisliVal.
rewrite -> kleisli_simpl.
repeat rewrite <- kleisli_simpl.
assert ((kleisli (uncurry (Smash C F) << prod_morph (fa, fb)))
((kleisli (eta << PAIR E s)) gb)
=-=
(kleisli (uncurry (Smash C F) << prod_morph (fa, fb))
<<
(kleisli (eta << PAIR E s))) gb
) by auto.
rewrite -> H; clear H.
rewrite <- kleisli_comp2.
assert (((Smash C F) (fa s)) ((kleisli fb) gb)
=-=
((Smash C F) (fa s) << (kleisli fb)) gb
) by auto. rewrite -> H; clear H.
rewrite -> miguel.
rewrite -> able. auto.
Qed.
Lemma Smash_prop_l : forall (B C E F : cpoType)
(fa : B =-> C _BOT) (ga : B _BOT)
(fb : E =-> F _BOT) (gb : E _BOT),
kleislit (uncurry (Smash _ _ ) << prod_morph (fa, fb))
(Smash _ _ ga gb)
<=
Smash _ _ ((kleislit fa) ga) ((kleislit fb) gb).
Proof.
cofix.
intros B C E F fa ga fb gb.
destruct ga. rewrite Smash_Eps_l.
repeat rewrite -> kleisli_Eps.
rewrite Smash_Eps_l. apply DLleEps.
apply Smash_prop_l.
Guarded.
rewrite -> Smash_Val.
repeat rewrite <- kleisli_simpl.
rewrite -> kleisliVal.
rewrite -> kleisli_simpl.
repeat rewrite <- kleisli_simpl.
assert ((kleisli (uncurry (Smash C F) << prod_morph (fa, fb)))
((kleisli (eta << PAIR E s)) gb)
=-=
(kleisli (uncurry (Smash C F) << prod_morph (fa, fb))
<<
(kleisli (eta << PAIR E s))) gb
) by auto.
rewrite -> H; clear H.
rewrite <- kleisli_comp2.
assert (((Smash C F) (fa s)) ((kleisli fb) gb)
=-=
((Smash C F) (fa s) << (kleisli fb)) gb
) by auto. rewrite -> H; clear H.
rewrite -> miguel.
rewrite -> able. auto.
Qed.
Lemma Smash_prop : forall (B C E F : cpoType)
(fa : B =-> C _BOT) (ga : B _BOT)
(fb : E =-> F _BOT) (gb : E _BOT),
Smash _ _ ((kleisli fa) ga) ((kleisli fb) gb)
=-=
kleisli (uncurry (Smash _ _ ) << prod_morph (fa, fb))
(Smash _ _ ga gb).
Proof.
intros B C E F fa ga fb gb.
repeat rewrite -> kleisli_simpl.
split; simpl.
apply Smash_prop_r.
apply Smash_prop_l.
Qed.
Definition biProd (F G : BiFunctor cppoBaseCatType) : BiFunctor cppoBaseCatType.
move => F G. exists (fun X Y => (ob F X Y) * (ob G X Y))
(fun X Y Z W => @prod_func F G X Y Z W).
intros T0 T1 T2 T3 T4 T5 f g h k.
simpl.
set (uSmash45 := uncurry (Smash (ob F T4 T5) (ob G T4 T5))).
set (uSmash13 := uncurry (Smash (ob F T1 T3) (ob G T1 T3))).
split;simpl.
intros (a,b). simpl.
repeat rewrite <- morph_comp. simpl. auto.
intros (a,b). simpl.
repeat rewrite <- morph_comp. simpl. auto.
split;simpl.
intros (a,b). simpl.
do 2 rewrite -> morph_id. unfold Id; simpl. auto.
intros (a,b). simpl.
do 2 rewrite -> morph_id. unfold Id; simpl. auto.
Defined.
Lemma bifunm X Y Z W :
monotonic (fun (p:@cppoMorph cppoBaseCatType Y X *
@cppoMorph cppoBaseCatType Z W) =>
(exp_fun (CCOMP _ _ _ :cppoCatType _ _)
((snd p)) : cppoCatType _ _)
<< (exp_fun ((CCOMP _ _ _) << SWAP) (fst p))).
intros X Y Z W p p' l h.
simpl. case: l => l l'. rewrite l. by rewrite l'.
Qed.
Add Parametric Morphism (D:cpoType) : (@Val D)
with signature (@Ole D: D -> D -> Prop) ++> (@Ole (D _BOT))
as Val_le_cpo_compat.
intros.
apply: DLle_leVal.
auto.
Qed.
Lemma bifunc X Y Z W : continuous (mk_fmono (@bifunm X Y Z W)).
Proof.
move => X Y Z W. move => c x. simpl.
apply Ole_trans with
(y:= ((((lub (pi2 << (c:natO =-> _))):cppoCatType _ _)
<<
exp_fun (CCOMP _ _ _:cppoCatType _ _)
x (lub (pi1 << (c:natO =-> _)))))) ; first by [].
rewrite lub_comp_eq.
rewrite -> lub_comp_both with (M:=cppoBaseCatType) (X:=Y) (Y:=Z) (Z:=W)
(c':=(pi2 << c)).
by apply lub_le_compat => n.
Qed.
Definition bi_fun (X Y Z W : cppoBaseCatType)
:= Eval hnf in mk_fcont (@bifunc X Y Z W).
Lemma bi_fun_simpl T0 T2 T4 T5 f g x : (bi_fun T0 T4 T2 T5) (f,g) x =
(g << (x << f)).
by [].
Qed.
Definition biFun : BiFunctor cppoBaseCatType.
exists (fun (X Y : cppoType) => exp_cppoType X Y)
(fun X Y Z W => @bi_fun X Y Z W).
move => T0 T1 T2 T3 T4 T5 f g h k. apply: fmon_eq_intro => x.
simpl. repeat rewrite <- comp_assoc.
rewrite {6 8} /Category.comp. simpl.
by rewrite -> comp_assoc.
move => X Y. apply: fmon_eq_intro => x.
simpl. rewrite comp_idR. by rewrite comp_idL.
Defined.
Definition biVar : BiFunctor cppoBaseCatType.
exists (fun X Y => Y) (fun X Y Z W => pi2).
by [].
by [].
Defined.
Definition biConst (X:cppoBaseCatType) : BiFunctor cppoBaseCatType.
move => D. exists (fun (X Y:cppoBaseCatType) => D)
(fun (X Y Z W:cppoBaseCatType) => const _ (Id (A:=D))).
move => T0 T1 T2 T3 T4 T5 f g h k. simpl. unfold Category.comp. simpl.
by rewrite comp_idL.
move => T0 T1. by [].
Defined.
Definition FS := biFun.
Definition DInf : cppoType := @DInf cppoBaseCatType cppoLimit FS leftss.
Definition VInf := (DInf -=> DInf).
Definition Fold : VInf =-> DInf := Fold cppoLimit FS leftss.
Definition Unfold : DInf =-> VInf := Unfold cppoLimit FS leftss.
Lemma FU_iso : Fold << Unfold =-= Id.
by apply (FU_id cppoLimit FS leftss).
Qed.
Lemma UF_iso : Unfold << Fold =-= Id.
by apply (UF_id cppoLimit FS leftss).
Qed.
Lemma ob X Y : ob FS X Y = X -=> Y.
by simpl.
Qed.
Definition delta : (DInf -=> DInf) =-> (DInf -=> DInf)
:= @delta cppoBaseCatType cppoLimit FS leftss.
Lemma eta_mono X Y (f g : X =-> Y) : eta << f =-= eta << g -> f =-= g.
move => X Y f g A. apply: fmon_eq_intro => x.
have A':=fmon_eq_elim A x. by apply (vinj A').
Qed.
Lemma foldT : total (eta << Fold).
move => x. simpl.
have X:=fmon_eq_elim UF_iso x.
exists (lub (fcont_app (chainFPE cppoLimit (DCoCone cppoLimit FS leftss)) x)).
auto.
Qed.
Lemma unfoldT : total (eta << Unfold).
move => x. simpl.
have X:=fmon_eq_elim FU_iso x.
exists ((lub (fcont_app (chainPEc cppoLimit (ECoCone cppoLimit FS leftss)) x))).
auto.
Qed.
Definition Roll : VInf =-> DInf := totalL foldT.
Definition Unroll : DInf =-> VInf := totalL unfoldT.
Lemma RU_id : Roll << Unroll =-= Id. apply eta_mono.
have X:=FU_iso.
have A:eta << Roll =-= eta << Fold by apply totalL_eta.
apply eta_injp in A.
rewrite <- A in X. clear A.
have A:eta << Unroll =-= eta << Unfold by apply totalL_eta.
apply eta_injp in A.
rewrite <- A in X. clear A.
rewrite X. by rewrite comp_idR.
Qed.
Lemma UR_id : Unroll << Roll =-= Id.
apply eta_mono.
have X:=UF_iso.
have A:eta << Roll =-= eta << Fold by apply totalL_eta.
apply eta_injp in A.
rewrite <- A in X. clear A.
have A:eta << Unroll =-= eta << Unfold by apply totalL_eta.
apply eta_injp in A.
rewrite <- A in X. clear A.
rewrite X. by rewrite comp_idR.
Qed.
Lemma delta_simpl (e:DInf -=> DInf) :
delta e =-= Roll <<
((exp_fun (CCOMP DInf DInf DInf
:cppoCatType _ _)
e : cppoCatType _ _)
<<
((exp_fun
((CCOMP DInf DInf DInf) << SWAP)
e : cppoCatType _ _)))
<< Unroll.
Proof.
move => e.
rewrite (@delta_simpl _ cppoLimit FS leftss e).
fold Fold. fold Unfold. fold DInf. simpl.
have A:eta << Unroll =-= eta << Unfold by apply totalL_eta.
apply eta_injp in A.
have B:eta << Roll =-= eta << Fold by apply totalL_eta.
apply eta_injp in B.
rewrite <- A. rewrite <- B.
auto.
Qed.
Lemma id_min : Id =-= FIXP delta.
apply tset_sym. rewrite <- (id_min cppoLimit FS leftss). fold delta.
by simpl.
Qed.
Lemma delta_eta : delta Id =-= Id.
by apply (delta_id_id cppoLimit FS leftss).
Qed.
End RD.