diff --git a/algebra/cofe.v b/algebra/cofe.v index 5724b5a6320b7d9bbb79f920ed2cd7da828134a5..ecffb4e660e108da5ba254344db4e7c1bc70e41d 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -239,6 +239,7 @@ Section cofe_mor. Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _. Lemma cofe_mor_ext (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x. Proof. done. Qed. + End cofe_mor. Arguments cofe_mor : clear implicits. @@ -257,6 +258,22 @@ Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n : f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. +(* Function space maps *) +Definition cofe_mor_map {A A' B B' : cofeT} (f : A' -n> A) (g : B -n> B') + (h : A -n> B) : A' -n> B' := g ◎ h ◎ f. +Instance cofe_mor_map_ne {A A' B B' : cofeT} n : + Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B'). +Proof. intros ??? ??? ???. apply ccompose_ne; first apply ccompose_ne;done. Qed. + +Definition cofe_morC_map {A A' B B' : cofeT} (f : A' -n> A) (g : B -n> B') : + (A -n> B) -n> (A' -n> B') := CofeMor (cofe_mor_map f g). +Instance cofe_morC_map_ne {A A' B B' : cofeT} n : + Proper (dist n ==> dist n ==> dist n) (@cofe_morC_map A A' B B'). +Proof. + intros f f' Hf g g' Hg ?. rewrite /= /cofe_mor_map. + apply ccompose_ne; first apply ccompose_ne; done. +Qed. + (** unit *) Section unit. Instance unit_dist : Dist unit := λ _ _ _, True. @@ -351,6 +368,26 @@ Next Obligation. by rewrite !cFunctor_compose. Qed. +Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {| + cFunctor_car A B := cofe_mor (cFunctor_car F1 B A) (cFunctor_car F2 A B); + cFunctor_map A1 A2 B1 B2 fg := + cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg) +|}. +Next Obligation. + by intros F1 F2 A1 A2 B1 B2 n [??] [??] [??]; apply cofe_morC_map_ne; + apply cFunctor_ne; apply pair_ne. +Qed. +Next Obligation. + intros F1 F2 A B [??] ?; rewrite /= !cFunctor_id. apply ne_proper; first done. + apply cFunctor_id. +Qed. +Next Obligation. + intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??] ?; simpl. + rewrite !cFunctor_compose. apply ne_proper; first by solve_proper. + apply ne_proper; first by solve_proper. apply ne_proper; first done. + apply cFunctor_compose. +Qed. + (** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. diff --git a/prelude/base.v b/prelude/base.v index 41fb9c5b9b7593c7b6bd6f822c46c98abff10d57..575a0671ffc421b3c0cf5646b1842f46cb2665d7 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -91,6 +91,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope. Notation "p .1" := (fst p) (at level 10, format "p .1"). Notation "p .2" := (snd p) (at level 10, format "p .2"). +Definition fun_map {A A' B B'} (f : A' -> A) (g : B -> B') + (h : A -> B) : A' -> B' := g ∘ h ∘ f. Definition prod_map {A A' B B'} (f : A → A') (g : B → B') (p : A * B) : A' * B' := (f (p.1), g (p.2)). Arguments prod_map {_ _ _ _} _ _ !_ /.