From ee264e907728f3b07c8230199bca84e2484cb9bb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 5 Oct 2020 19:57:27 +0200
Subject: [PATCH] Define non-unital camera functors in such a way that the
 non-unital camera is used.

---
 theories/algebra/auth.v        | 12 ++++++++++--
 theories/algebra/cmra.v        | 11 +++++++++--
 theories/algebra/gmap.v        | 11 +++++++++--
 theories/algebra/list.v        | 11 +++++++++--
 theories/base_logic/lib/wsat.v |  4 ++--
 5 files changed, 39 insertions(+), 10 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index e6a124cac..13f796c51 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -328,5 +328,13 @@ Proof.
   apply viewO_map_ne; by apply urFunctor_map_contractive.
 Qed.
 
-Definition authRF (F : urFunctor) :=
-  urFunctor_to_rFunctor (authURF F).
+Program Definition authRF (F : urFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
+|}.
+Solve Obligations with apply authURF.
+
+Instance authRF_contractive F :
+  urFunctorContractive F → rFunctorContractive (authRF F).
+Proof. apply authURF_contractive. Qed.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 61fac8868..5b29880c0 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1575,8 +1575,15 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
-Definition optionRF (F : rFunctor) : rFunctor :=
-  urFunctor_to_rFunctor (optionURF F).
+Program Definition optionRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
+|}.
+Solve Obligations with apply optionURF.
+
+Instance optionRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (optionRF F).
+Proof. apply optionURF_contractive. Qed.
 
 (* Dependently-typed functions over a discrete domain *)
 Section discrete_fun_cmra.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index b0832496f..2f5974324 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -718,5 +718,12 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
 Qed.
 
-Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor :=
-  urFunctor_to_rFunctor (gmapURF K F).
+Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := gmapR K (rFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
+|}.
+Solve Obligations with apply gmapURF.
+
+Instance gmapRF_contractive K `{Countable K} F :
+  rFunctorContractive F → rFunctorContractive (gmapRF K F).
+Proof. apply gmapURF_contractive. Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 9aa392107..e8b9af034 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -572,5 +572,12 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
 Qed.
 
-Definition listRF (F : urFunctor) : rFunctor :=
-  urFunctor_to_rFunctor (listURF F).
+Program Definition listRF (F : urFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := listR (urFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
+|}.
+Solve Obligations with apply listURF.
+
+Instance listRF_contractive F :
+  urFunctorContractive F → rFunctorContractive (listRF F).
+Proof. apply listURF_contractive. Qed.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 700ea9589..87d3a7a7a 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -19,8 +19,8 @@ Module invG.
 
   Definition invΣ : gFunctors :=
     #[GFunctor (gmap_viewRF positive (laterOF idOF));
-      GFunctor coPset_disjUR;
-      GFunctor (gset_disjUR positive)].
+      GFunctor coPset_disjR;
+      GFunctor (gset_disjR positive)].
 
   Class invPreG (Σ : gFunctors) : Set := WsatPreG {
     inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-- 
GitLab