Add some missing functors in algebra/lib

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

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 *)

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.

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.

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.

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.

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.