Merge branch 'robbert/local_instance_pragma' into 'master'

Use `#[local] field ::` to make `inG` instances local.

Closes #561

See merge request iris/iris!1065

docs/proof_guide.md

@@ -99,10 +99,9 @@ for further details on `libG` classes).  For example, the STS library is
 parameterized by an STS and assumes that the STS state space is inhabited:
 ```coq
 Class stsG Σ (sts : stsT) := {
-  sts_inG : inG Σ (stsR sts);
+  #[local] sts_inG :: inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
-Local Existing Instance sts_inG.
 ```
 In this case, the `Instance` for this `libG` class has more than just a `subG`
 assumption:

docs/resource_algebras.md

@@ -126,14 +126,13 @@ class for the generalized heap module, bundles the usual `inG` assumptions
 together with the `gname`:
 ```coq
 Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heapGpreS_heap : ghost_mapG Σ L V;
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
 }.
-Local Existing Instances gen_heapGpreS_heap.
+
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  gen_heap_inG : gen_heapGpreS L V Σ;
+  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
   gen_heap_name : gname;
 }.
-Local Existing Instances gen_heap_inG.
 ```
 The trailing `S` here is for "singleton", because the idea is that only one
 instance of `gen_heapGS` ever exists. This is important, since two instances
@@ -283,8 +282,8 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
 your example would look as follows:
 
 ```coq
-Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
-Local Existing Instance lib_inG.
+Class libG Σ :=
+  { #[local] lib_inG :: inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
 
 Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.

iris/base_logic/lib/boxes.v

@@ -6,10 +6,9 @@ Import uPred.
 
 (** The CMRAs we need. *)
 Class boxG Σ :=
-  boxG_inG : inG Σ (prodR
+  #[local] boxG_inG :: inG Σ (prodR
     (excl_authR boolO)
     (optionR (agreeR (laterO (iPropO Σ))))).
-Local Existing Instance boxG_inG.
 
 Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
                                             optionRF (agreeRF (▶ ∙)) ) ].

iris/base_logic/lib/cancelable_invariants.v

@@ -5,8 +5,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class cinvG Σ := { cinv_inG : inG Σ fracR }.
-Local Existing Instance cinv_inG.
+Class cinvG Σ := { #[local] cinv_inG :: inG Σ fracR }.
 
 Definition cinvΣ : gFunctors := #[GFunctor fracR].
 

iris/base_logic/lib/fancy_updates.v

@@ -23,21 +23,19 @@ Import le_upd_if.
 Inductive has_lc := HasLc | HasNoLc.
 
 Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
-  invGpreS_wsat : wsatGpreS Σ;
-  invGpreS_lc : lcGpreS Σ;
+  #[local] invGpreS_wsat :: wsatGpreS Σ;
+  #[local] invGpreS_lc :: lcGpreS Σ;
 }.
 
+(* [invGS_lc] needs to be global in order to enable the use of lemmas like
+[lc_split] that require [lcGS], and not [invGS]. [invGS_wsat] also needs to be
+global as the lemmas in [invariants.v] require it. *)
 Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set := InvG {
-  invGS_wsat : wsatGS Σ;
-  invGS_lc : lcGS Σ;
+  #[global] invGS_wsat :: wsatGS Σ;
+  #[global] invGS_lc :: lcGS Σ;
 }.
 Global Hint Mode invGS_gen - - : typeclass_instances.
 Global Hint Mode invGpreS - : typeclass_instances.
-Local Existing Instances invGpreS_wsat invGpreS_lc.
-(* [invGS_lc] needs to be global in order to enable the use of lemmas like [lc_split]
-   that require [lcGS], and not [invGS].
-   [invGS_wsat] also needs to be global as the lemmas in [invariants.v] require it. *)
-Global Existing Instances invGS_lc invGS_wsat.
 
 Notation invGS := (invGS_gen HasLc).
 

iris/base_logic/lib/gen_heap.v

@@ -66,18 +66,16 @@ these can be matched up with the invariant namespaces. *)
 (** The CMRAs we need, and the global ghost names we are using. *)
 
 Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heapGpreS_heap : ghost_mapG Σ L V;
-  gen_heapGpreS_meta : ghost_mapG Σ L gname;
-  gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
+  #[local] gen_heapGpreS_meta :: ghost_mapG Σ L gname;
+  #[local] gen_heapGpreS_meta_data :: inG Σ (reservation_mapR (agreeR positiveO));
 }.
-Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta.
 
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  gen_heap_inG : gen_heapGpreS L V Σ;
+  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
   gen_heap_name : gname;
   gen_meta_name : gname
 }.
-Local Existing Instance gen_heap_inG.
 Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
 Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
 Global Arguments gen_meta_name {L V Σ _ _} _ : assert.

iris/base_logic/lib/gen_inv_heap.v

@@ -31,15 +31,13 @@ Definition to_inv_heap {L V : Type} `{Countable L}
   prod_map (λ x, Excl' x) to_agree <$> h.
 
 Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  inv_heapGpreS_inG : inG Σ (authR (inv_heap_mapUR L V))
+  #[local] inv_heapGpreS_inG :: inG Σ (authR (inv_heap_mapUR L V))
 }.
-Local Existing Instance inv_heapGpreS_inG.
 
 Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
-  inv_heap_inG : inv_heapGpreS L V Σ;
+  #[local] inv_heap_inG :: inv_heapGpreS L V Σ;
   inv_heap_name : gname
 }.
-Local Existing Instance inv_heap_inG.
 Global Arguments Inv_HeapG _ _ {_ _ _ _}.
 Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
 

iris/base_logic/lib/ghost_map.v

@@ -12,9 +12,8 @@ From iris.prelude Require Import options.
 FIXME: This is intentionally discrete-only, but
 should we support setoids via [Equiv]? *)
 Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
-  ghost_map_inG : inG Σ (gmap_viewR K (agreeR (leibnizO V)));
+  #[local] ghost_map_inG :: inG Σ (gmap_viewR K (agreeR (leibnizO V)));
 }.
-Local Existing Instance ghost_map_inG.
 
 Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
   #[ GFunctor (gmap_viewR K (agreeR (leibnizO V))) ].

iris/base_logic/lib/ghost_var.v

@@ -8,9 +8,8 @@ From iris.prelude Require Import options.
 
 (** The CMRA we need. *)
 Class ghost_varG Σ (A : Type) := GhostVarG {
-  ghost_var_inG : inG Σ (dfrac_agreeR $ leibnizO A);
+  #[local] ghost_var_inG :: inG Σ (dfrac_agreeR $ leibnizO A);
 }.
-Local Existing Instance ghost_var_inG.
 Global Hint Mode ghost_varG - ! : typeclass_instances.
 
 Definition ghost_varΣ (A : Type) : gFunctors :=

iris/base_logic/lib/gset_bij.v

@@ -28,8 +28,7 @@ From iris.prelude Require Import options.
 
 (* The uCMRA we need. *)
 Class gset_bijG Σ A B `{Countable A, Countable B} :=
-  GsetBijG { gset_bijG_inG : inG Σ (gset_bijR A B); }.
-Local Existing Instance gset_bijG_inG.
+  GsetBijG { #[local] gset_bijG_inG :: inG Σ (gset_bijR A B); }.
 Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=

iris/base_logic/lib/later_credits.v

@@ -10,15 +10,14 @@ Import uPred.
 
 (** The ghost state for later credits *)
 Class lcGpreS (Σ : gFunctors) := LcGpreS {
-  lcGpreS_inG : inG Σ (authR natUR)
+  #[local] lcGpreS_inG :: inG Σ (authR natUR)
 }.
 
 Class lcGS (Σ : gFunctors) := LcGS {
-  lcGS_inG : inG Σ (authR natUR);
+  #[local] lcGS_inG :: inG Σ (authR natUR);
   lcGS_name : gname;
 }.
 Global Hint Mode lcGS - : typeclass_instances.
-Local Existing Instances lcGS_inG lcGpreS_inG.
 
 Definition lcΣ := #[GFunctor (authR (natUR))].
 Global Instance subG_lcΣ {Σ} : subG lcΣ Σ → lcGpreS Σ.

iris/base_logic/lib/mono_Z.v

@@ -25,8 +25,7 @@ From iris.prelude Require Import options.
 Local Open Scope Z_scope.
 
 Class mono_ZG Σ :=
-  MonoZG { mono_ZG_natG : mono_natG Σ; }.
-Local Existing Instance mono_ZG_natG.
+  MonoZG { #[local] mono_ZG_natG :: mono_natG Σ; }.
 Definition mono_ZΣ := mono_natΣ.
 
 Local Definition mono_Z_auth_own_def `{!mono_ZG Σ}

iris/base_logic/lib/mono_nat.v

@@ -14,8 +14,7 @@ From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
 Class mono_natG Σ :=
-  MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
-Local Existing Instance mono_natG_inG.
+  MonoNatG { #[local] mono_natG_inG :: inG Σ mono_natR; }.
 
 Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
 Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.

iris/base_logic/lib/na_invariants.v

@@ -9,8 +9,7 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  na_inv_inG : inG Σ (prodR coPset_disjR (gset_disjR positive)).
-Local Existing Instance na_inv_inG.
+  #[local] na_inv_inG :: inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Definition na_invΣ : gFunctors :=
   #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].

iris/base_logic/lib/proph_map.v

@@ -9,16 +9,14 @@ Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
 Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
-  proph_map_GpreS_inG : ghost_mapG Σ P (list V)
+  #[local] proph_map_GpreS_inG :: ghost_mapG Σ P (list V)
 }.
-Local Existing Instances proph_map_GpreS_inG.
 
 Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
-  proph_map_inG : proph_mapGpreS P V Σ;
+  #[local] proph_map_inG :: proph_mapGpreS P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
-Local Existing Instances proph_map_inG.
 
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
   #[ghost_mapΣ P (list V)].

iris/base_logic/lib/saved_prop.v

@@ -10,10 +10,9 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG : inG Σ (dfrac_agreeR (oFunctor_apply F (iPropO Σ)));
+  #[local] saved_anything_inG :: inG Σ (dfrac_agreeR (oFunctor_apply F (iPropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
-Local Existing Instance saved_anything_inG.
 
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
   #[ GFunctor (dfrac_agreeRF F) ].

iris/base_logic/lib/token.v

@@ -8,9 +8,8 @@ From iris.prelude Require Import options.
 
 (** The CMRA we need. *)
 Class tokenG Σ := TokenG {
-  token_inG : inG Σ (exclR unitO);
+  #[local] token_inG :: inG Σ (exclR unitO);
 }.
-Local Existing Instance token_inG.
 Global Hint Mode tokenG - : typeclass_instances.
 
 Definition tokenΣ : gFunctors :=

iris/base_logic/lib/wsat.v

@@ -31,6 +31,9 @@ Module wsatGS.
   Proof. solve_inG. Qed.
 End wsatGS.
 Import wsatGS.
+
+(* Make the instances local to this file. We cannot use #[local] in the code
+above, as that would make the instances local to the module. *)
 Local Existing Instances wsat_inG wsatGpreS_inv wsatGpreS_enabled wsatGpreS_disabled.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=

iris/program_logic/ownp.v

@@ -16,10 +16,9 @@ union.
 
 Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
   ownP_invG : invGS Σ;
-  ownP_inG : inG Σ (excl_authR (stateO Λ));
+  #[local] ownP_inG :: inG Σ (excl_authR (stateO Λ));
   ownP_name : gname;
 }.
-Local Existing Instance ownP_inG.
 
 Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
   iris_invGS := ownP_invG;
@@ -36,9 +35,8 @@ Definition ownPΣ (Λ : language) : gFunctors :=
 
 Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set := {
   #[global] ownPPre_invG :: invGpreS Σ;
-  ownPPre_state_inG : inG Σ (excl_authR (stateO Λ))
+  #[local] ownPPre_state_inG :: inG Σ (excl_authR (stateO Λ))
 }.
-Local Existing Instance ownPPre_state_inG.
 
 Global Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPGpreS Λ Σ.
 Proof. solve_inG. Qed.

iris_deprecated/base_logic/auth.v

@@ -11,10 +11,9 @@ Import uPred.
 
 (* The CMRA we need. *)
 Class authG Σ (A : ucmra) := AuthG {
-  auth_inG : inG Σ (authR A);
+  #[local] auth_inG :: inG Σ (authR A);
   #[global] auth_cmra_discrete :: CmraDiscrete A;
 }.
-Local Existing Instance auth_inG.
 
 Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].