From 844cec51538521e8d05ddc8b9eecf081d27a8d69 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 00:22:04 +0200
Subject: [PATCH] Add `{o,r,ur}Functor_oFunctor_compose` to compose two
 functors.

---
 theories/algebra/cmra.v | 70 +++++++++++++++++++++++++++++++++++++++++
 theories/algebra/ofe.v  | 43 ++++++++++++++++++++++---
 2 files changed, 109 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 505f56807..54a984004 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -803,6 +803,41 @@ Class rFunctorContractive (F : rFunctor) :=
 Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
   rFunctor_car F A A.
 
+Program Definition rFunctor_oFunctor_compose (F1 : rFunctor) (F2 : oFunctor)
+  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
+  rFunctor_car A _ B _ := rFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
+    rFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
+|}.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  apply rFunctor_map_ne; split; apply oFunctor_map_ne; by split.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(rFunctor_map_id F1 x).
+  apply equiv_dist=> n. apply rFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  rewrite -rFunctor_map_compose. apply equiv_dist=> n. apply rFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_compose.
+Qed.
+Instance rFunctor_oFunctor_compose_contractive_1 (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  rFunctorContractive F1 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
+Qed.
+Instance rFunctor_oFunctor_compose_contractive_2 (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F2 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
+Qed.
+
 Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
@@ -840,6 +875,41 @@ Class urFunctorContractive (F : urFunctor) :=
 Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
   urFunctor_car F A A.
 
+Program Definition urFunctor_oFunctor_compose (F1 : urFunctor) (F2 : oFunctor)
+  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
+  urFunctor_car A _ B _ := urFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
+    urFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
+|}.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  apply urFunctor_map_ne; split; apply oFunctor_map_ne; by split.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(urFunctor_map_id F1 x).
+  apply equiv_dist=> n. apply urFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  rewrite -urFunctor_map_compose. apply equiv_dist=> n. apply urFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_compose.
+Qed.
+Instance urFunctor_oFunctor_compose_contractive_1 (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  urFunctorContractive F1 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
+Qed.
+Instance urFunctor_oFunctor_compose_contractive_2 (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F2 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
+Qed.
+
 Program Definition constURF (B : ucmraT) : urFunctor :=
   {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f13afb314..82d3e7dc8 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -713,6 +713,41 @@ ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *
 Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
   oFunctor_car F A A.
 
+Program Definition oFunctor_oFunctor_compose (F1 F2 : oFunctor)
+  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : oFunctor := {|
+  oFunctor_car A _ B _ := oFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
+  oFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
+    oFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
+|}.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  apply oFunctor_map_ne; split; apply oFunctor_map_ne; by split.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(oFunctor_map_id F1 x).
+  apply equiv_dist=> n. apply oFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  rewrite -oFunctor_map_compose. apply equiv_dist=> n. apply oFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_compose.
+Qed.
+Instance oFunctor_oFunctor_compose_contractive_1 (F1 F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F1 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
+Qed.
+Instance oFunctor_oFunctor_compose_contractive_2 (F1 F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F2 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
+Qed.
+
 Program Definition constOF (B : ofeT) : oFunctor :=
   {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
@@ -1588,14 +1623,14 @@ Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
   OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
     (oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
 Next Obligation.
-  intros F A ? B ? I x. rewrite -oFunctor_compose -{2}(oFunctor_id F x).
+  intros F A ? B ? I x. rewrite -oFunctor_map_compose -{2}(oFunctor_map_id F x).
   apply equiv_dist=> n.
-  apply oFunctor_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
+  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
 Qed.
 Next Obligation.
-  intros F A ? B ? I y. rewrite -oFunctor_compose -{2}(oFunctor_id F y).
+  intros F A ? B ? I y. rewrite -oFunctor_map_compose -{2}(oFunctor_map_id F y).
   apply equiv_dist=> n.
-  apply oFunctor_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
+  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
 Qed.
 Instance iso_ofe_cong_ne (F : oFunctor) `{!Cofe A, !Cofe B} :
   NonExpansive (iso_ofe_cong F (A:=A) (B:=B)).
-- 
GitLab