Library Cppo_cppoECat
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.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Lemma cppoCatAxiom : @Category.axiom
cppoType
(fun (X Y : cppoType) => exp_cppoType X Y)
(fun X Y Z f g => f << g) (@Id _).
split ; last split ; last split.
- move => D0 D1 f. simpl. by rewrite comp_idL.
- move => D0 D1 f. simpl. by rewrite comp_idR.
- move => D0 D1 D2 D3 f g h. simpl. by rewrite comp_assoc.
- move => D0 D1 D2 f f' g g'. simpl. move => e e'. rewrite e. by rewrite e'.
Qed.
Canonical Structure cppoCatMixin := CatMixin cppoCatAxiom.
Canonical Structure cppoCatType := Eval hnf in CatType cppoCatMixin.
Lemma cppoTerminalAxiom : CatTerminal.axiom (one_cppoType : cppoCatType).
simpl. move => D x y. split.
move => i. simpl. by cbn.
move => i. simpl. by cbn.
Qed.
Canonical Structure cppoTermincalCatMixin :=
@terminalCatMixin
cppoCatType
(one_cppoType : cppoCatType)
(fun X => const _ tt) cppoTerminalAxiom.
Canonical Structure cppoTerminalCat :=
Eval hnf in @terminalCatType cppoCatType cppoTermincalCatMixin.
Lemma cppo_comp_eq : forall (X Y Z : cppoType)
(m : exp_cppoType Y Z)
(m' : exp_cppoType X Y),
(CCOMP X Y Z) (m, m') =-= Category.tcomp cppoCatMixin m m'.
auto.
Qed.
Definition cppoBaseCatMixin := CppoECatMixin cppoTermincalCatMixin cppo_comp_eq.
Canonical Structure cppoBaseCatType := Eval hnf in CppoECatType cppoBaseCatMixin.
Lemma leftss : (forall (X Y Z : cppoBaseCatType) (f : cppoBaseCatType X Y),
(PBot:cppoCatType _ _) << f =-= (PBot: X =-> Z)).
move => X Y Z f. apply: fmon_eq_intro.
move => x. auto.
Qed.
Definition ProjSet (T:Tower cppoBaseCatType) :=
fun (d:prodi_cppoType (fun n => tobjects T n)) => forall n,
PROJ (fun n => tobjects T n) n d =-=
(tmorphisms T n) (PROJ (fun n => tobjects T n) (S n) d).
Lemma ProjSet_inclusive T : admissible (@ProjSet T).
move => T. unfold ProjSet. unfold admissible.
intros c C n.
do 3 rewrite -> lub_comp_eq.
refine (lub_eq_compat _).
refine (fmon_eq_intro _).
intros m. simpl. specialize (C m n). by apply C.
Qed.
Lemma EPstrict : forall (D E : cppoType) (f : D =-> E) (g : E =-> D),
(@eppair cppoBaseCatType D E f g) -> f PBot =-= PBot /\ g PBot =-= PBot.
Proof.
intros D E f g ep.
destruct ep as [e p].
assert (PBot <= f PBot) as fL by apply leastP.
assert (monotonic g) as gM by auto.
unfold monotonic in gM. specialize (gM _ _ fL).
assert (xx:=fcont_eq_compat e (tset_refl PBot)). simpl in xx.
rewrite -> xx in gM. unfold id in *.
clear xx.
assert (PBot <= g PBot) as gL by apply leastP.
have gML := Ole_antisym gM gL.
assert (monotonic f) as F by auto.
unfold monotonic in F. specialize (F _ _ gL).
assert (xx:=fcont_le_compat p (Ole_refl PBot)). simpl in xx.
rewrite -> xx in F. unfold id in *.
clear xx.
have fML := Ole_antisym F fL. auto.
Qed.
Lemma Proj_Strict (T:Tower cppoBaseCatType) : forall n , strict (tmorphisms T n).
intros T n.
unfold strict.
destruct T. simpl in *.
specialize (teppair n).
apply EPstrict in teppair as [? ?].
auto.
Qed.
Lemma Proj_PBot (T:Tower cppoBaseCatType) : @ProjSet T (fun n : nat => PBot).
Proof.
intros T.
unfold ProjSet; unfold PROJ; simpl.
intros n.
symmetry.
apply Proj_Strict.
Qed.
Definition cppoCone (T:Tower cppoBaseCatType) : Cone T.
move => T.
eexists (sub_cppoType (@ProjSet_inclusive T) (@Proj_PBot T))
(fun i:nat => PROJ_cppo _ i << Forget (@ProjSet_inclusive T)).
move => i. apply: fmon_eq_intro. case => d Pd.
rewrite -> (Pd i). auto.
Defined.
Arguments InheritFun [D E P].
Lemma retract_total D E (f:D =-> E _BOT) (g:E =-> D _BOT) :
kleisli f << g =-= eta -> total g.
move => D E f g. unfold total. move => X d. have X':=fmon_eq_elim X d.
case: (kleisliValVal X'). move => e [Y _]. exists e. by apply Y.
Qed.
Lemma xx (T:Tower cppoBaseCatType) i :
(forall d : tobjects T i, ProjSet (PRODI_fun_cppo (t_nm T i) d)).
Proof.
move => T i d n. simpl.
rewrite -> (fmon_eq_elim (t_nmProjection T i n) d). auto.
Qed.
Definition cppoCocone (T:Tower cppoBaseCatType) : CoCone T.
move => T. exists (sub_cppoType (@ProjSet_inclusive T) (@Proj_PBot T))
(fun i => @InheritFun _ _ _ (@ProjSet_inclusive T)
(PRODI_fun_cppo (t_nm T i)) (@xx T i)
).
move => i.
apply fmon_eq_intro => d.
split => a; simpl in *.
rewrite -> t_nmEmbedding with (n:=i). auto.
rewrite -> t_nmEmbedding with (n:=i). auto.
Defined.
Lemma prodi_cppo_fun_pi (T:Tower cppoBaseCatType) (n:nat) (m:nat):
(PROJ_cppo (fun n0 : nat => tobjects T n0) n << PRODI_fun_cppo (t_nm T m))
=-= t_nm T m n.
intros T n. split; simpl. intro o. by simpl.
intro o. by simpl.
Qed.
Definition cppoLimit (T:Tower cppoBaseCatType) : Limit T.
move => T. exists (cppoCone T) (fun C : Cone T => lub (chainPE (@cppoCocone T) C)).
move => C n. simpl. split.
- apply: (Ole_trans _ (comp_le_compat (Ole_refl _)
(le_lub (chainPE (cppoCocone T) C) n))).
simpl. rewrite {1} /Category.comp. simpl.
rewrite <- comp_assoc.
assert ((Forget (ProjSet_inclusive (T:=T)) <<
(InheritFun (ProjSet_inclusive (T:=T))
(PRODI_fun_cppo (t_nm T n))
(xx (i:=n)) << mcone C n))
=-=
((Forget (ProjSet_inclusive (T:=T)) <<
InheritFun (ProjSet_inclusive (T:=T))
(PRODI_fun_cppo (t_nm T n))
(xx (i:=n))) << mcone C n)
) by (by rewrite -> comp_assoc). rewrite -> H; clear H.
rewrite -> ForgetInherit. rewrite -> comp_assoc.
rewrite -> prodi_cppo_fun_pi.
rewrite -> t_nn_ID. by rewrite -> comp_idL with (f:=mcone C n).
- simpl. rewrite {1} / Category.comp. simpl.
refine (Ole_trans (Oeq_le (PredomCore.comp_lub_eq _
(chainPE (cppoCocone T) C))) _).
rewrite (lub_lift_left _ n). apply: lub_le => i. simpl.
rewrite <- comp_assoc.
assert ((Forget (ProjSet_inclusive (T:=T)) <<
(InheritFun (ProjSet_inclusive (T:=T))
(PRODI_fun_cppo (t_nm T (n + i)))
(xx (i:=n + i)) << mcone C (n + i)))
=-=
((Forget (ProjSet_inclusive (T:=T)) <<
InheritFun (ProjSet_inclusive (T:=T))
(PRODI_fun_cppo (t_nm T (n + i)))
(xx (i:=n + i))) << mcone C (n + i))
) by (by rewrite -> comp_assoc). rewrite -> H; clear H.
rewrite ForgetInherit. rewrite -> comp_assoc.
rewrite -> prodi_cppo_fun_pi. by apply (proj2 ((coneCom_l C (leq_addr i n)))).
- intros A h C.
apply: fmon_eq_intro => d. simpl in h. split.
-- simpl. destruct (h d) eqn:H.
intro n.
have a := (fmon_eq_elim (C n) d). simpl in a. rewrite -> H in a.
rewrite <- a.
have aa:exists e, (fcont_app (chainPE (cppoCocone T) A) d) n =-= e.
exists (@InheritFun _ _ _ (@ProjSet_inclusive T) (PRODI_fun (t_nm T n))
(@xx T n) (mcone A n d)).
auto.
case: aa => e aa.
setoid_rewrite -> lub_lift_left with (n:=n).
apply Ole_trans with (y:=lub (fmon_cte natO ((mcone A n) d))).
rewrite -> lub_const. apply Ole_refl.
apply lub_le_compat. cbn. intros x0.
assert ((t_nm T (n + x0)%Nrec n) ((mcone A (n + x0)%Nrec) d)
=-=
((t_nm T (n + x0)%Nrec n << (mcone A (n + x0)%Nrec)) d)
) by auto. rewrite -> H0; clear H0.
repeat rewrite <- coneCom_l.
apply Ole_refl.
apply leq_addr.
-- simpl. destruct (h d) eqn:H.
apply lub_le => n. specialize (C n). simpl.
have Y := fmon_eq_elim C d. simpl mcone in Y. intro i.
rewrite -> Y. simpl. rewrite -> H.
case: (ltngtP n i).
--- move => l.
have a := comp_eq_compat (tset_refl (t_nm T n i))
(coneCom_l (cppoCone T) (ltnW l)).
rewrite -> comp_assoc in a.
have yy:t_nm T n i << mcone (cppoCone T) n <= mcone (cppoCone T) i.
rewrite -> a. rewrite -> (comp_le_compat (proj2 (t_nm_EP T (ltnW l)))
(Ole_refl _)).
by rewrite comp_idL.
specialize (yy (exist _ x p)). simpl in yy. auto.
--- move => l.
have a := (proj2 (fmon_eq_elim (coneCom_l (cppoCone T) (ltnW l))
(exist _ x p))).
simpl in a. auto.
--- move => e. rewrite <- e. clear i e.
rewrite -> t_nn_ID. auto.
Defined.