Skip to content

replace ssrfun.{idfun,comp} by universe polymorphic equivalents #188

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
t6s wants to merge 1 commit into
base: master
Choose a base branch
from
Open

replace ssrfun.{idfun,comp} by universe polymorphic equivalents #188

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 20 additions & 20 deletions theories/applications/category_ext.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ Definition slice_category_inhom' (b c : slice) :
Definition slice_category_inhom := Eval hnf in slice_category_inhom'.
Local Notation el := slice_category_obj.
Local Notation inhom := slice_category_inhom.
Lemma slice_category_id : forall a : slice, inhom (@idfun (el a)).
Lemma slice_category_id : forall a : slice, inhom (@up_idfun (el a)).
Proof. by case. Qed.
Lemma slice_category_comp :
forall (aa ba ca : slice) (f : el aa -> el ba) (g : el ba -> el ca),
Expand Down Expand Up @@ -94,7 +94,7 @@ by case: (cid (Hf2 x)) => y ->.
Qed.
Definition inhom (A B : obj) (f : ele A -> ele B) : Prop :=
exists H : separated f, inhom _ _ (sepfst H) /\ inhom _ _ (sepsnd H).
Lemma idfun_separated (X : obj) : @separated X X idfun.
Lemma idfun_separated (X : obj) : @separated X X up_idfun.
Proof. by split; move=> x; exists x. Qed.
Lemma comp_separated (X Y Z : obj) (f : ele X -> ele Y) (g : ele Y -> ele Z) :
separated f -> separated g -> separated (g \o f).
Expand All @@ -104,13 +104,13 @@ move: X Y Z => [X1 X2] [Y1 Y2] [Z1 Z2] f g [/= Hf1 Hf2] [/= Hg1 Hg2]; split=> x.
- by case/cid: (Hf1 x)=> y /= ->; case/cid: (Hg1 y)=> z /= ->; exists z.
- by case/cid: (Hf2 x)=> y /= ->; case/cid: (Hg2 y)=> z /= ->; exists z.
Qed.
Lemma sepfst_idfun X : sepfst (idfun_separated X) = idfun.
Lemma sepfst_idfun X : sepfst (idfun_separated X) = up_idfun.
Proof.
apply funext=> x /=.
suff: inl (B:=el X.2) (sepfst (idfun_separated X) x) = inl x by move=> [=].
by rewrite sepfstK.
Qed.
Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = idfun.
Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = up_idfun.
Proof.
apply funext=> x /=.
suff: inr (A:=el X.1) (sepsnd (idfun_separated X) x) = inr x by move=> [=].
Expand All @@ -134,7 +134,7 @@ suff: inr (A := el Z.1) (sepsnd (comp_separated Hf Hg) x) =
inr (sepsnd Hg (sepsnd Hf x)) by case.
by rewrite 3!sepsndK.
Qed.
Lemma idfun_inhom (X : obj) : @inhom X X idfun.
Lemma idfun_inhom (X : obj) : @inhom X X up_idfun.
Proof.
exists (idfun_separated X); rewrite sepfst_idfun sepsnd_idfun;
split; exact: idfun_inhom.
Expand Down Expand Up @@ -170,14 +170,14 @@ exact: Hom.Pack.
Defined.
Definition homsnd := Eval hnf in _homsnd.
End homfstsnd.
Lemma homfst_idfun x : homfst (x:=x) [hom idfun] = [hom idfun].
Lemma homfst_idfun x : homfst (x:=x) [hom up_idfun] = [hom up_idfun].
Proof.
apply/hom_ext; rewrite boolp.funeqE => x1 /=.
case: cid => i [i1 i2] /=.
rewrite (_ : i = ProductCategory.idfun_separated _)//.
by rewrite ProductCategory.sepfst_idfun.
Qed.
Lemma homsnd_idfun x : homsnd (x:=x) [hom idfun] = [hom idfun].
Lemma homsnd_idfun x : homsnd (x:=x) [hom up_idfun] = [hom up_idfun].
Proof.
apply/hom_ext; rewrite boolp.funeqE => x1 /=.
case: cid => i [i1 i2] /=.
Expand Down Expand Up @@ -259,7 +259,7 @@ End prodCat_pairhom.

Section pairhom_idfun.
Variables (A B : category) (a : A) (b : B).
Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom idfun] [hom idfun] = [hom idfun].
Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom up_idfun] [hom up_idfun] = [hom up_idfun].
Proof. by apply/hom_ext/funext=> -[] x /=. Qed.
End pairhom_idfun.

Expand Down Expand Up @@ -311,18 +311,18 @@ Section def.
Variables (A B C : category) (F : {functor A * B -> C}) (a : A).
Definition acto : B -> C := fun b => F (a, b).
Definition actm (b1 b2 : B) (f : {hom b1 -> b2}) : {hom acto b1 -> acto b2} :=
F # pairhom [hom idfun] f.
F # pairhom [hom up_idfun] f.
Let actm_id : FunctorLaws.id actm.
Proof.
move=> D; rewrite /actm; set h := pairhom _ _.
rewrite (_ : h = [hom idfun]) ?functor_id_hom //.
rewrite (_ : h = [hom up_idfun]) ?functor_id_hom //.
by apply/hom_ext => /=; rewrite boolp.funeqE; case.
Qed.
Let actm_comp : FunctorLaws.comp actm.
Proof.
move=> b b0 b1 g h; rewrite /actm; set i := pairhom _ _.
rewrite (_ : i = [hom (pairhom [hom idfun] g) \o
(pairhom [hom idfun] h)]) ?functor_o_hom //.
rewrite (_ : i = [hom (pairhom [hom up_idfun] g) \o
(pairhom [hom up_idfun] h)]) ?functor_o_hom //.
by apply/hom_ext => /=; rewrite boolp.funeqE; case.
Qed.
HB.instance Definition _ := isFunctor.Build _ _ _ actm_id actm_comp.
Expand All @@ -334,18 +334,18 @@ Section def.
Variables (A B C : category) (F : {functor A * B -> C}) (b : B).
Definition acto : A -> C := fun a => F (a, b).
Definition actm (a1 a2 : A) (f : {hom a1 -> a2}) : {hom acto a1 -> acto a2} :=
F # pairhom f [hom idfun].
F # pairhom f [hom up_idfun].
Let actm_id : FunctorLaws.id actm.
Proof.
move=> D; rewrite /actm; set h := pairhom _ _.
rewrite (_ : h = [hom idfun]) ?functor_id_hom //.
rewrite (_ : h = [hom up_idfun]) ?functor_id_hom //.
by apply/hom_ext => /=; rewrite boolp.funeqE; case.
Qed.
Let actm_comp : FunctorLaws.comp actm.
Proof.
move=> a a0 a1 g h; rewrite /actm; set i := pairhom _ _.
rewrite (_ : i = [hom (pairhom g [hom idfun]) \o
(pairhom h [hom idfun])]) ?functor_o_hom //.
rewrite (_ : i = [hom (pairhom g [hom up_idfun]) \o
(pairhom h [hom up_idfun])]) ?functor_o_hom //.
by apply/hom_ext => /=; rewrite boolp.funeqE; case.
Qed.
HB.instance Definition _ := isFunctor.Build _ _ _ actm_id actm_comp.
Expand Down Expand Up @@ -387,18 +387,18 @@ Variable F : {functor [the category of ((A * B) * C)%type] -> D}.
Variables (a : A) (b : B).
Definition acto : C -> D := papply_left.acto F (a, b).
Definition actm (c1 c2 : C) (f : {hom c1 -> c2}) : {hom acto c1 -> acto c2} :=
F # pairhom [hom idfun] f.
F # pairhom [hom up_idfun] f.
Let actm_id : FunctorLaws.id actm.
Proof.
move=> c0; rewrite /actm; set h := pairhom _ _.
rewrite (_ : h = [hom idfun]) ?functor_id_hom //.
rewrite (_ : h = [hom up_idfun]) ?functor_id_hom //.
by apply/hom_ext => /=; rewrite boolp.funeqE; case.
Qed.
Let actm_comp : FunctorLaws.comp actm.
Proof.
move=> c c0 c1 g h; rewrite /actm; set i := pairhom _ _.
rewrite (_ : i = [hom (pairhom [hom idfun] g) \o
(pairhom [hom idfun] h)]) ?functor_o_hom //.
rewrite (_ : i = [hom (pairhom [hom up_idfun] g) \o
(pairhom [hom up_idfun] h)]) ?functor_o_hom //.
by apply/hom_ext => /=; rewrite boolp.funeqE; case.
Qed.
HB.instance Definition _ := isFunctor.Build _ _ _ actm_id actm_comp.
Expand Down
4 changes: 1 addition & 3 deletions theories/applications/example_relabeling.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,9 +122,7 @@ Proof.
rewrite boolp.funeqE => -[x1 x2].
rewrite 3!compE.
rewrite joinE.
rewrite fmapE.
rewrite 2![in RHS]compE.
rewrite [in RHS]/mpair.
rewrite fmapE/=.
rewrite [in LHS]/mpair.
move H : (fmap dlabels) => h.
rewrite /=.
Expand Down
10 changes: 5 additions & 5 deletions theories/applications/example_typed_store.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -334,9 +334,9 @@ Section eval.
Require Import typed_store_transformer.
Import ModelTypedStoreRun.

Definition M := acto ml_type idfun.
Definition M := acto ml_type up_idfun.

Definition Env := Env ml_type idfun.
Definition Env := Env ml_type up_idfun.

Definition empty_env : Env := [::].

Expand Down Expand Up @@ -367,9 +367,9 @@ Eval vm_compute in it1.
Definition it2 := Restart it1 (do l <- FromW l; incr l).
Eval vm_compute in it2.

Local Notation cycle := (cycle idfun M).
Local Notation rhd := (rhd idfun M).
Local Notation rtl := (rtl idfun M).
Local Notation cycle := (cycle up_idfun M).
Local Notation rhd := (rhd up_idfun M).
Local Notation rtl := (rtl up_idfun M).

Definition it3 := Restart it2 (cycle ml_bool true false).
Eval vm_compute in crun (FromW it3).
Expand Down
16 changes: 8 additions & 8 deletions theories/applications/monad_composition.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ Local Open Scope monae_scope.

Section comp.
Variables (M N : monad).
Definition ret_comp : idfun ~~> M \o N := (@ret M) \h (@ret N).
Lemma naturality_ret : naturality idfun [the functor of M \o N] ret_comp.
Definition ret_comp : up_idfun ~~> M \o N := (@ret M) \h (@ret N).
Lemma naturality_ret : naturality up_idfun [the functor of M \o N] ret_comp.
Proof. by move=> A B h; rewrite -(natural ((@ret M) \h (@ret N))). Qed.
HB.instance Definition _ := isNatural.Build
idfun [the functor of (M \o N)] ret_comp naturality_ret.
up_idfun [the functor of (M \o N)] ret_comp naturality_ret.
End comp.
Definition CRet (M N : monad) := [the idfun ~> [the functor of M \o N] of ret_comp M N].
Definition CRet (M N : monad) := [the up_idfun ~> [the functor of M \o N] of ret_comp M N].

Module Prod.
Section prod.
Expand Down Expand Up @@ -127,7 +127,7 @@ move=> A B g; apply/esym; rewrite {1}/JOIN -compA Hdorp1.
rewrite [LHS]compA.
rewrite (FCompE M N (N # g)).
rewrite -(@functor_o M).
rewrite -natural.
rewrite -(natural join).
by rewrite functor_o.
Qed.

Expand Down Expand Up @@ -218,7 +218,7 @@ Lemma prod1 : Prod.prod1 (@prod).
Proof.
move=> A B f; rewrite {1}/prod.
rewrite -[LHS]compA Hswap1 (compA (M # Join)) -functor_o.
by rewrite -natural functor_o -compA.
by rewrite -(natural join)/= functor_o -compA.
Qed.

Lemma prod2 : Prod.prod2 (@prod).
Expand Down Expand Up @@ -312,13 +312,13 @@ End Swap.

Section nattrans_cast_lemmas.
Variables (F G : functor).
Lemma IV : [the functor of idfun \o G] ~> F -> G ~> F.
Lemma IV : [the functor of up_idfun \o G] ~> F -> G ~> F.
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack [the functor of G] F _ (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
Lemma VI : [the functor of G \o idfun] ~> F -> G ~> F.
Lemma VI : [the functor of G \o up_idfun] ~> F -> G ~> F.
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack [the functor of G] F _ (Nattrans.Class (isNatural.Axioms_ _ _ _))).
Expand Down
Loading
Loading