From 4563868c7aa68354a397aa73125891a99fbdb0a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Tue, 7 Jun 2022 12:02:42 +0000
Subject: [PATCH] Add some missing functors in algebra/lib

---
 CHANGELOG.md                   |  6 ++++++
 iris/algebra/lib/dfrac_agree.v |  7 +++++++
 iris/algebra/lib/excl_auth.v   | 14 ++++++++++++++
 iris/algebra/lib/frac_auth.v   | 14 ++++++++++++++
 iris/algebra/lib/mono_list.v   | 14 ++++++++++++++
 iris/algebra/lib/ufrac_auth.v  | 14 ++++++++++++++
 iris/algebra/max_prefix_list.v | 14 ++++++++++++++
 7 files changed, 83 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 70a994380..fcb01da5b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,12 @@ lemma.
   custom proof mode tactics. All other unsealing lemmas should be internal, so
   in principle you should not rely on them.
 
+**Changes in `algebra`:**
+
+* Add some missing algebra functors: `dfrac_agreeRF`, `excl_authURF`, `excl_authRF`,
+  `frac_authURF`, `frac_authRF`, `ufrac_authURF`, `ufrac_authRF`, `max_prefix_listURF`,
+  `max_prefix_listRF`, `mono_listURF`, and `mono_listRF`.
+
 **Changes in `bi`:**
 
 * Generalize `big_op` lemmas that were previously assuming `Absorbing`ness of
diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index 8bd125b3c..ed13d9e04 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -125,5 +125,12 @@ Section lemmas.
 
 End lemmas.
 
+Definition dfrac_agreeRF (F : oFunctor) : rFunctor :=
+  prodRF (constRF dfracR) (agreeRF F).
+
+Global Instance dfrac_agreeRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (dfrac_agreeRF F).
+Proof. apply _. Qed.
+
 Typeclasses Opaque to_dfrac_agree.
 (* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)
diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index b1cda8d1d..da52b48cc 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -69,3 +69,17 @@ Section excl_auth.
     intros. by apply auth_update, option_local_update, exclusive_local_update.
   Qed.
 End excl_auth.
+
+Definition excl_authURF (F : oFunctor) : urFunctor :=
+  authURF (optionURF (exclRF F)).
+
+Global Instance excl_authURF_contractive F :
+  oFunctorContractive F → urFunctorContractive (excl_authURF F).
+Proof. apply _. Qed.
+
+Definition excl_authRF (F : oFunctor) : rFunctor :=
+  authRF (optionURF (exclRF F)).
+
+Global Instance excl_authRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (excl_authRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 4f456bbc9..412ada8e4 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -119,3 +119,17 @@ Section frac_auth.
     intros. by apply auth_update, option_local_update, exclusive_local_update.
   Qed.
 End frac_auth.
+
+Definition frac_authURF (F : rFunctor) : urFunctor :=
+  authURF (optionURF (prodRF (constRF fracR) F)).
+
+Global Instance frac_authURF_contractive F :
+  rFunctorContractive F → urFunctorContractive (frac_authURF F).
+Proof. apply _. Qed.
+
+Definition frac_authRF (F : rFunctor) : rFunctor :=
+  authRF (optionURF (prodRF (constRF fracR) F)).
+
+Global Instance frac_authRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (frac_authRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index 60679ecfe..b91656f25 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -182,3 +182,17 @@ Section mono_list_props.
     by apply auth_update_auth_persist.
   Qed.
 End mono_list_props.
+
+Definition mono_listURF (F : oFunctor) : urFunctor :=
+  authURF (max_prefix_listURF F).
+
+Global Instance mono_listURF_contractive F :
+  oFunctorContractive F → urFunctorContractive (mono_listURF F).
+Proof. apply _. Qed.
+
+Definition mono_listRF (F : oFunctor) : rFunctor :=
+  authRF (max_prefix_listURF F).
+
+Global Instance mono_listRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (mono_listRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index 12311d84c..d577614c7 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -147,3 +147,17 @@ Section ufrac_auth.
       destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
   Qed.
 End ufrac_auth.
+
+Definition ufrac_authURF (F : rFunctor) : urFunctor :=
+  authURF (optionURF (prodRF (constRF ufracR) F)).
+
+Global Instance ufrac_authURF_contractive F :
+  rFunctorContractive F → urFunctorContractive (ufrac_authURF F).
+Proof. apply _. Qed.
+
+Definition ufrac_authRF (F : rFunctor) : rFunctor :=
+  authRF (optionURF (prodRF (constRF ufracR) F)).
+
+Global Instance ufrac_authRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (ufrac_authRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/max_prefix_list.v b/iris/algebra/max_prefix_list.v
index 3643c1d83..373463caa 100644
--- a/iris/algebra/max_prefix_list.v
+++ b/iris/algebra/max_prefix_list.v
@@ -171,3 +171,17 @@ Section max_prefix_list.
     apply to_max_prefix_list_validN.
   Qed.
 End max_prefix_list.
+
+Definition max_prefix_listURF (F : oFunctor) : urFunctor :=
+  gmapURF nat (agreeRF F).
+
+Global Instance max_prefix_listURF_contractive F :
+  oFunctorContractive F → urFunctorContractive (max_prefix_listURF F).
+Proof. apply _. Qed.
+
+Definition max_prefix_listRF (F : oFunctor) : rFunctor :=
+  gmapRF nat (agreeRF F).
+
+Global Instance max_prefix_listRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (max_prefix_listRF F).
+Proof. apply _. Qed.
-- 
GitLab