add \Sigma for boxes; use a coercion for constant functors

theories/algebra/cmra.v

@@ -700,6 +700,9 @@ Structure rFunctor := RFunctor {
 Existing Instances rFunctor_ne rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
 
+Delimit Scope rFunctor_scope with RF.
+Bind Scope rFunctor_scope with rFunctor.
+
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
 
@@ -709,6 +712,7 @@ Coercion rFunctor_diag : rFunctor >-> Funclass.
 Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
+Coercion constRF : cmraT >-> rFunctor.
 
 Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
@@ -729,6 +733,9 @@ Structure urFunctor := URFunctor {
 Existing Instances urFunctor_ne urFunctor_mono.
 Instance: Params (@urFunctor_map) 5.
 
+Delimit Scope urFunctor_scope with URF.
+Bind Scope urFunctor_scope with urFunctor.
+
 Class urFunctorContractive (F : urFunctor) :=
   urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
 
@@ -738,6 +745,7 @@ Coercion urFunctor_diag : urFunctor >-> Funclass.
 Program Definition constURF (B : ucmraT) : urFunctor :=
   {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
+Coercion constURF : ucmraT >-> urFunctor.
 
 Instance constURF_contractive B : urFunctorContractive (constURF B).
 Proof. rewrite /urFunctorContractive; apply _. Qed.
@@ -1064,6 +1072,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !rFunctor_compose.
 Qed.
+Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
 
 Instance prodRF_contractive F1 F2 :
   rFunctorContractive F1 → rFunctorContractive F2 →
@@ -1086,6 +1095,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !urFunctor_compose.
 Qed.
+Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
 
 Instance prodURF_contractive F1 F2 :
   urFunctorContractive F1 → urFunctorContractive F2 →
@@ -1243,6 +1253,29 @@ Proof.
     intros [->|(x&y&->&->&[Hxy|?])]; simpl; eauto 10 using @cmra_monotone.
     right; exists (f x), (f y). by rewrite {3}Hxy; eauto.
 Qed.
+
+Program Definition optionRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := optionR (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
+Qed.
+
+Instance optionRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (optionRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+Qed.
+
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_car A B := optionUR (rFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)

theories/algebra/ofe.v

@@ -552,6 +552,7 @@ Coercion cFunctor_diag : cFunctor >-> Funclass.
 Program Definition constCF (B : ofeT) : cFunctor :=
   {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
+Coercion constCF : ofeT >-> cFunctor.
 
 Instance constCF_contractive B : cFunctorContractive (constCF B).
 Proof. rewrite /cFunctorContractive; apply _. Qed.
@@ -559,6 +560,7 @@ Proof. rewrite /cFunctorContractive; apply _. Qed.
 Program Definition idCF : cFunctor :=
   {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
 Solve Obligations with done.
+Notation "∙" := idCF : cFunctor_scope.
 
 Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
@@ -573,6 +575,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !cFunctor_compose.
 Qed.
+Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
 
 Instance prodCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
@@ -604,6 +607,7 @@ Next Obligation.
   intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
   by rewrite !cFunctor_compose.
 Qed.
+Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
 
 Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
   cFunctorContractive F → cFunctorContractive (ofe_funCF T F).
@@ -629,6 +633,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *.
   rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
 Qed.
+Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
 
 Instance ofe_morCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
@@ -716,6 +721,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [?|?]; simpl;
     by rewrite !cFunctor_compose.
 Qed.
+Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
 
 Instance sumCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
@@ -949,6 +955,7 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose.
   apply later_map_ext=>y; apply cFunctor_compose.
 Qed.
+Notation "▶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
 
 Instance laterCF_contractive F : cFunctorContractive (laterCF F).
 Proof.
@@ -1026,12 +1033,3 @@ Section sigma.
 End sigma.
 
 Arguments sigC {_} _.
-
-(** Notation for writing functors *)
-Notation "∙" := idCF : cFunctor_scope.
-Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
-Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
-Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
-Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
-Notation "▶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
-Coercion constCF : ofeT >-> cFunctor.

theories/base_logic/lib/auth.v

@@ -11,7 +11,7 @@ Class authG Σ (A : ucmraT) := AuthG {
   auth_inG :> inG Σ (authR A);
   auth_discrete :> CMRADiscrete A;
 }.
-Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
+Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
 
 Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
 Proof. intros ?%subG_inG ?. by split. Qed.

theories/base_logic/lib/boxes.v

@@ -11,6 +11,13 @@ Class boxG Σ :=
     (authR (optionUR (exclR boolC)))
     (optionR (agreeR (laterC (iPreProp Σ))))).
 
+Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
+                                            optionRF (agreeRF (▶ ∙)) ) ].
+
+Instance subG_stsΣ Σ :
+  subG boxΣ Σ → boxG Σ.
+Proof. apply subG_inG. Qed.
+
 Section box_defs.
   Context `{invG Σ, boxG Σ} (N : namespace).
 

theories/base_logic/lib/gen_heap.v

@@ -20,7 +20,7 @@ Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
   { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
 
 Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
-  #[GFunctor (constRF (authR (gen_heapUR L V)))].
+  #[GFunctor (authR (gen_heapUR L V))].
 
 Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
   subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.

theories/base_logic/lib/sts.v

@@ -9,8 +9,8 @@ Class stsG Σ (sts : stsT) := StsG {
   sts_inG :> inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
-Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (constRF (stsR sts)) ].
 
+Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
 Instance subG_stsΣ Σ sts :
   subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
 Proof. intros ?%subG_inG ?. by split. Qed.

theories/heap_lang/lib/counter.v

@@ -14,7 +14,7 @@ Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
 Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
-Definition mcounterΣ : gFunctors := #[GFunctor (constRF (authR mnatUR))].
+Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
 
 Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.

theories/heap_lang/lib/spawn.v

@@ -20,7 +20,7 @@ Definition join : val :=
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
-Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
 
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.

theories/heap_lang/lib/spin_lock.v

@@ -15,7 +15,7 @@ Definition release : val := λ: "l", "l" <- #false.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. intros ?%subG_inG. split; apply _. Qed.

theories/heap_lang/lib/ticket_lock.v

@@ -31,7 +31,7 @@ Definition release : val :=
 Class tlockG Σ :=
   tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
 Definition tlockΣ : gFunctors :=
-  #[ GFunctor (constRF (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat)))) ].
+  #[ GFunctor (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
 
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. by intros ?%subG_inG. Qed.

theories/program_logic/adequacy.v

@@ -9,8 +9,8 @@ Import uPred.
 (* Global functor setup *)
 Definition invΣ : gFunctors :=
   #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
-    GFunctor (constRF coPset_disjUR);
-    GFunctor (constRF (gset_disjUR positive))].
+    GFunctor coPset_disjUR;
+    GFunctor (gset_disjUR positive)].
 
 Class invPreG (Σ : gFunctors) : Set := WsatPreG {
   inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));

theories/program_logic/ownp.v

@@ -20,7 +20,7 @@ Global Opaque iris_invG.
 
 Definition ownPΣ (Λstate : Type) : gFunctors :=
   #[invΣ;
-    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
+    GFunctor (authUR (optionUR (exclR (leibnizC Λstate))))].
 
 Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
   ownPPre_invG :> invPreG Σ;
@@ -31,7 +31,6 @@ Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
 Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ → ownPPreG' Λstate Σ.
 Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
 
-
 (** Ownership *)
 Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
   own ownP_name (◯ (Excl' σ)).

theories/tests/counter.v

@@ -73,7 +73,7 @@ Section M.
 End M.
 
 Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
-Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
+Definition counterΣ : gFunctors := #[GFunctor M_UR].
 Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 

theories/tests/one_shot.v

@@ -25,7 +25,7 @@ Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
 Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
 
 Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
-Definition one_shotΣ : gFunctors := #[GFunctor (constRF one_shotR)].
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.