From 143d0af35ddc573ecc56e7c3239e1514928fb0d4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jan 2021 12:52:15 +0100
Subject: [PATCH] Qualify all instances with Local or Global
Done with a script by Tej; see
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/609 for details.
---
iris/algebra/agree.v | 34 +++---
iris/algebra/auth.v | 10 +-
iris/algebra/big_op.v | 8 +-
iris/algebra/cmra.v | 112 +++++++++---------
iris/algebra/coPset.v | 16 +--
iris/algebra/cofe_solver.v | 14 +--
iris/algebra/csum.v | 28 ++---
iris/algebra/dfrac.v | 6 +-
iris/algebra/dra.v | 10 +-
iris/algebra/excl.v | 22 ++--
iris/algebra/frac.v | 6 +-
iris/algebra/functions.v | 4 +-
iris/algebra/gmap.v | 30 ++---
iris/algebra/gmultiset.v | 10 +-
iris/algebra/gset.v | 16 +--
iris/algebra/lib/excl_auth.v | 4 +-
iris/algebra/lib/frac_auth.v | 4 +-
iris/algebra/lib/gmap_view.v | 4 +-
iris/algebra/lib/ufrac_auth.v | 4 +-
iris/algebra/list.v | 34 +++---
iris/algebra/local_updates.v | 2 +-
iris/algebra/namespace_map.v | 22 ++--
iris/algebra/numbers.v | 36 +++---
iris/algebra/ofe.v | 124 ++++++++++----------
iris/algebra/proofmode_classes.v | 4 +-
iris/algebra/sts.v | 18 +--
iris/algebra/ufrac.v | 6 +-
iris/algebra/updates.v | 4 +-
iris/algebra/vector.v | 10 +-
iris/algebra/view.v | 32 ++---
iris/base_logic/bi.v | 4 +-
iris/base_logic/lib/auth.v | 8 +-
iris/base_logic/lib/boxes.v | 10 +-
iris/base_logic/lib/cancelable_invariants.v | 4 +-
iris/base_logic/lib/fancy_updates.v | 6 +-
iris/base_logic/lib/gen_heap.v | 2 +-
iris/base_logic/lib/gen_inv_heap.v | 6 +-
iris/base_logic/lib/ghost_var.v | 2 +-
iris/base_logic/lib/invariants.v | 2 +-
iris/base_logic/lib/iprop.v | 6 +-
iris/base_logic/lib/mono_nat.v | 2 +-
iris/base_logic/lib/na_invariants.v | 4 +-
iris/base_logic/lib/own.v | 2 +-
iris/base_logic/lib/proph_map.v | 2 +-
iris/base_logic/lib/saved_prop.v | 8 +-
iris/base_logic/lib/sts.v | 10 +-
iris/base_logic/lib/viewshifts.v | 2 +-
iris/base_logic/lib/wsat.v | 12 +-
iris/base_logic/upred.v | 14 +--
iris/bi/big_op.v | 4 +-
iris/bi/derived_connectives.v | 26 ++--
iris/bi/embedding.v | 2 +-
iris/bi/interface.v | 28 ++---
iris/bi/internal_eq.v | 2 +-
iris/bi/lib/core.v | 2 +-
iris/bi/lib/counterexamples.v | 12 +-
iris/bi/lib/fractional.v | 4 +-
iris/bi/lib/relations.v | 8 +-
iris/bi/monpred.v | 6 +-
iris/bi/plainly.v | 6 +-
iris/bi/updates.v | 4 +-
iris/bi/weakestpre.v | 8 +-
iris/program_logic/hoare.v | 2 +-
iris/program_logic/language.v | 2 +-
iris/program_logic/ownp.v | 6 +-
iris/program_logic/total_adequacy.v | 2 +-
iris/proofmode/base.v | 6 +-
iris/proofmode/classes.v | 48 ++++----
iris/proofmode/coq_tactics.v | 2 +-
iris/proofmode/environments.v | 12 +-
iris/proofmode/monpred.v | 2 +-
iris/si_logic/bi.v | 4 +-
iris/si_logic/siprop.v | 4 +-
iris_heap_lang/adequacy.v | 2 +-
iris_heap_lang/class_instances.v | 4 +-
iris_heap_lang/lang.v | 34 +++---
iris_heap_lang/lib/counter.v | 4 +-
iris_heap_lang/lib/lock.v | 2 +-
iris_heap_lang/lib/spawn.v | 2 +-
iris_heap_lang/lib/spin_lock.v | 2 +-
iris_heap_lang/lib/ticket_lock.v | 2 +-
iris_heap_lang/locations.v | 8 +-
iris_heap_lang/primitive_laws.v | 6 +-
tests/algebra.v | 2 +-
tests/heapprop.v | 6 +-
tests/ipm_paper.v | 10 +-
tests/one_shot.v | 2 +-
tests/one_shot_once.v | 2 +-
88 files changed, 515 insertions(+), 515 deletions(-)
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index f5733133f..bfc1a913b 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -55,10 +55,10 @@ Implicit Types a b : A.
Implicit Types x y : agree A.
(* OFE *)
-Instance agree_dist : Dist (agree A) := λ n x y,
+Local Instance agree_dist : Dist (agree A) := λ n x y,
(∀ a, a ∈ agree_car x → ∃ b, b ∈ agree_car y ∧ a ≡{n}≡ b) ∧
(∀ b, b ∈ agree_car y → ∃ a, a ∈ agree_car x ∧ a ≡{n}≡ b).
-Instance agree_equiv : Equiv (agree A) := λ x y, ∀ n, x ≡{n}≡ y.
+Local Instance agree_equiv : Equiv (agree A) := λ x y, ∀ n, x ≡{n}≡ y.
Definition agree_ofe_mixin : OfeMixin (agree A).
Proof.
@@ -79,17 +79,17 @@ Canonical Structure agreeO := OfeT (agree A) agree_ofe_mixin.
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
is convertible to True. This makes working with agreement much more pleasant. *)
-Instance agree_validN : ValidN (agree A) := λ n x,
+Local Instance agree_validN : ValidN (agree A) := λ n x,
match agree_car x with
| [a] => True
| _ => ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b
end.
-Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
+Local Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
-Instance agree_pcore : PCore (agree A) := Some.
+Local Instance agree_pcore : PCore (agree A) := Some.
Lemma agree_validN_def n x :
✓{n} x ↔ ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b.
@@ -98,30 +98,30 @@ Proof.
setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
-Instance agree_comm : Comm (≡) (@op (agree A) _).
+Local Instance agree_comm : Comm (≡) (@op (agree A) _).
Proof. intros x y n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
-Instance agree_assoc : Assoc (≡) (@op (agree A) _).
+Local Instance agree_assoc : Assoc (≡) (@op (agree A) _).
Proof.
intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
Qed.
Lemma agree_idemp x : x ⋅ x ≡ x.
Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
-Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n).
+Local Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n).
Proof.
intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb.
destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto.
Qed.
-Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n).
+Local Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n).
Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed.
-Instance agree_op_ne' x : NonExpansive (op x).
+Local Instance agree_op_ne' x : NonExpansive (op x).
Proof.
intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver.
Qed.
-Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
+Local Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
-Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
+Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
Lemma agree_included x y : x ≼ y ↔ y ≡ x ⋅ y.
Proof.
@@ -258,7 +258,7 @@ Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
End agree.
-Instance: Params (@to_agree) 1 := {}.
+Global Instance: Params (@to_agree) 1 := {}.
Arguments agreeO : clear implicits.
Arguments agreeR : clear implicits.
@@ -277,13 +277,13 @@ Proof. by apply agree_eq. Qed.
Section agree_map.
Context {A B : ofeT} (f : A → B) {Hf: NonExpansive f}.
- Instance agree_map_ne : NonExpansive (agree_map f).
+ Local Instance agree_map_ne : NonExpansive (agree_map f).
Proof using Type*.
intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap.
- intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
- intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.
Qed.
- Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
+ Local Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
Lemma agree_map_ext (g : A → B) x :
(∀ a, f a ≡ g a) → agree_map f x ≡ agree_map g x.
@@ -307,7 +307,7 @@ End agree_map.
Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
OfeMor (agree_map f : agreeO A → agreeO B).
-Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
+Global Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
Proof.
intros n f g Hfg x; split=> b /=;
setoid_rewrite elem_of_list_fmap; naive_solver.
@@ -329,7 +329,7 @@ Next Obligation.
apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
Qed.
-Instance agreeRF_contractive F :
+Global Instance agreeRF_contractive F :
oFunctorContractive F → rFunctorContractive (agreeRF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 29c5c0ae5..52306f467 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -44,7 +44,7 @@ Proof.
intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
Qed.
-Instance auth_view_rel_discrete {A : ucmraT} :
+Global Instance auth_view_rel_discrete {A : ucmraT} :
CmraDiscrete A → ViewRelDiscrete (auth_view_rel (A:=A)).
Proof.
intros ? n a b [??]; split.
@@ -66,8 +66,8 @@ Definition auth_frag {A: ucmraT} : A → auth A := view_frag.
Typeclasses Opaque auth_auth auth_frag.
-Instance: Params (@auth_auth) 2 := {}.
-Instance: Params (@auth_frag) 1 := {}.
+Global Instance: Params (@auth_auth) 2 := {}.
+Global Instance: Params (@auth_frag) 1 := {}.
Notation "â—¯ a" := (auth_frag a) (at level 20).
Notation "â—{ q } a" := (auth_auth q a) (at level 20, format "â—{ q } a").
@@ -358,7 +358,7 @@ Next Obligation.
- by apply (cmra_morphism_validN _).
Qed.
-Instance authURF_contractive F :
+Global Instance authURF_contractive F :
urFunctorContractive F → urFunctorContractive (authURF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
@@ -372,6 +372,6 @@ Program Definition authRF (F : urFunctor) : rFunctor := {|
|}.
Solve Obligations with apply authURF.
-Instance authRF_contractive F :
+Global Instance authRF_contractive F :
urFunctorContractive F → rFunctorContractive (authRF F).
Proof. apply authURF_contractive. Qed.
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 92a790f25..6302c29f1 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -25,7 +25,7 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
-Instance: Params (@big_opL) 4 := {}.
+Global Instance: Params (@big_opL) 4 := {}.
Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
@@ -41,7 +41,7 @@ Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
-Instance: Params (@big_opM) 7 := {}.
+Global Instance: Params (@big_opM) 7 := {}.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope.
@@ -55,7 +55,7 @@ Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
-Instance: Params (@big_opS) 6 := {}.
+Global Instance: Params (@big_opS) 6 := {}.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope.
@@ -66,7 +66,7 @@ Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
-Instance: Params (@big_opMS) 6 := {}.
+Global Instance: Params (@big_opMS) 6 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o mset] x ∈ X , P") : stdpp_scope.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 6164660dc..4cc21f60f 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -4,11 +4,11 @@ From iris.prelude Require Import options.
Class PCore (A : Type) := pcore : A → option A.
Global Hint Mode PCore ! : typeclass_instances.
-Instance: Params (@pcore) 2 := {}.
+Global Instance: Params (@pcore) 2 := {}.
Class Op (A : Type) := op : A → A → A.
Global Hint Mode Op ! : typeclass_instances.
-Instance: Params (@op) 2 := {}.
+Global Instance: Params (@op) 2 := {}.
Infix "â‹…" := op (at level 50, left associativity) : stdpp_scope.
Notation "(â‹…)" := op (only parsing) : stdpp_scope.
@@ -21,23 +21,23 @@ Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Global Hint Extern 0 (_ ≼ _) => reflexivity : core.
-Instance: Params (@included) 3 := {}.
+Global Instance: Params (@included) 3 := {}.
Class ValidN (A : Type) := validN : nat → A → Prop.
Global Hint Mode ValidN ! : typeclass_instances.
-Instance: Params (@validN) 3 := {}.
+Global Instance: Params (@validN) 3 := {}.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A → Prop.
Global Hint Mode Valid ! : typeclass_instances.
-Instance: Params (@valid) 2 := {}.
+Global Instance: Params (@valid) 2 := {}.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
-Instance: Params (@includedN) 4 := {}.
+Global Instance: Params (@includedN) 4 := {}.
Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
Section mixin.
@@ -146,27 +146,27 @@ Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
Arguments core_id {_} _ {_}.
Global Hint Mode CoreId + ! : typeclass_instances.
-Instance: Params (@CoreId) 1 := {}.
+Global Instance: Params (@CoreId) 1 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
Arguments exclusive0_l {_} _ {_} _ _.
Global Hint Mode Exclusive + ! : typeclass_instances.
-Instance: Params (@Exclusive) 1 := {}.
+Global Instance: Params (@Exclusive) 1 := {}.
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
Arguments cancelableN {_} _ {_} _ _ _ _.
Global Hint Mode Cancelable + ! : typeclass_instances.
-Instance: Params (@Cancelable) 1 := {}.
+Global Instance: Params (@Cancelable) 1 := {}.
(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
Arguments id_free0_r {_} _ {_} _ _.
Global Hint Mode IdFree + ! : typeclass_instances.
-Instance: Params (@IdFree) 1 := {}.
+Global Instance: Params (@IdFree) 1 := {}.
(** * CMRAs whose core is total *)
Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
@@ -176,7 +176,7 @@ Global Hint Mode CmraTotal ! : typeclass_instances.
core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
to not require that proof to be able to call this function. *)
Definition core `{PCore A} (x : A) : A := default x (pcore x).
-Instance: Params (@core) 2 := {}.
+Global Instance: Params (@core) 2 := {}.
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
@@ -746,7 +746,7 @@ Section cmra_total.
End cmra_total.
(** * Properties about morphisms *)
-Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
+Global Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
Proof.
split => /=.
- apply _.
@@ -754,9 +754,9 @@ Proof.
- intros. by rewrite option_fmap_id.
- done.
Qed.
-Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CmraMorphism f} :
+Global Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CmraMorphism f} :
Proper ((≡) ==> (≡)) f := ne_proper _.
-Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
+Global Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
CmraMorphism f → CmraMorphism g → CmraMorphism (g ∘ f).
Proof.
split.
@@ -796,7 +796,7 @@ Record rFunctor := RFunctor {
CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_map_ne rFunctor_mor.
-Instance: Params (@rFunctor_map) 9 := {}.
+Global Instance: Params (@rFunctor_map) 9 := {}.
Declare Scope rFunctor_scope.
Delimit Scope rFunctor_scope with RF.
@@ -847,14 +847,14 @@ Next Obligation.
rewrite -rFunctor_map_compose. apply equiv_dist=> n. apply rFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
-Instance rFunctor_oFunctor_compose_contractive_1 (F1 : rFunctor) (F2 : oFunctor)
+Global Instance rFunctor_oFunctor_compose_contractive_1 (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
rFunctorContractive F1 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
-Instance rFunctor_oFunctor_compose_contractive_2 (F1 : rFunctor) (F2 : oFunctor)
+Global Instance rFunctor_oFunctor_compose_contractive_2 (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
oFunctorContractive F2 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
Proof.
@@ -867,7 +867,7 @@ Program Definition constRF (B : cmraT) : rFunctor :=
Solve Obligations with done.
Coercion constRF : cmraT >-> rFunctor.
-Instance constRF_contractive B : rFunctorContractive (constRF B).
+Global Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
(** COFE → UCMRA Functors *)
@@ -887,7 +887,7 @@ Record urFunctor := URFunctor {
CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_map_ne urFunctor_mor.
-Instance: Params (@urFunctor_map) 9 := {}.
+Global Instance: Params (@urFunctor_map) 9 := {}.
Declare Scope urFunctor_scope.
Delimit Scope urFunctor_scope with URF.
@@ -938,14 +938,14 @@ Next Obligation.
rewrite -urFunctor_map_compose. apply equiv_dist=> n. apply urFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
-Instance urFunctor_oFunctor_compose_contractive_1 (F1 : urFunctor) (F2 : oFunctor)
+Global Instance urFunctor_oFunctor_compose_contractive_1 (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
urFunctorContractive F1 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
-Instance urFunctor_oFunctor_compose_contractive_2 (F1 : urFunctor) (F2 : oFunctor)
+Global Instance urFunctor_oFunctor_compose_contractive_2 (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
oFunctorContractive F2 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
Proof.
@@ -958,7 +958,7 @@ Program Definition constURF (B : ucmraT) : urFunctor :=
Solve Obligations with done.
Coercion constURF : ucmraT >-> urFunctor.
-Instance constURF_contractive B : urFunctorContractive (constURF B).
+Global Instance constURF_contractive B : urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.
(** * Transporting a CMRA equality *)
@@ -1014,7 +1014,7 @@ Section discrete.
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist.
- Instance discrete_validN : ValidN A := λ n x, ✓ x.
+ Local Instance discrete_validN : ValidN A := λ n x, ✓ x.
Definition discrete_cmra_mixin : CmraMixin A.
Proof.
destruct ra_mix; split; try done.
@@ -1022,7 +1022,7 @@ Section discrete.
- intros n x y1 y2 ??; by exists y1, y2.
Qed.
- Instance discrete_cmra_discrete :
+ Local Instance discrete_cmra_discrete :
CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
Proof. split; first apply _. done. Qed.
End discrete.
@@ -1062,15 +1062,15 @@ End ra_total.
(** ** CMRA for the unit type *)
Section unit.
- Instance unit_valid : Valid () := λ x, True.
- Instance unit_validN : ValidN () := λ n x, True.
- Instance unit_pcore : PCore () := λ x, Some x.
- Instance unit_op : Op () := λ x y, ().
+ Local Instance unit_valid : Valid () := λ x, True.
+ Local Instance unit_validN : ValidN () := λ n x, True.
+ Local Instance unit_pcore : PCore () := λ x, Some x.
+ Local Instance unit_op : Op () := λ x y, ().
Lemma unit_cmra_mixin : CmraMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
Canonical Structure unitR : cmraT := CmraT unit unit_cmra_mixin.
- Instance unit_unit : Unit () := ().
+ Local Instance unit_unit : Unit () := ().
Lemma unit_ucmra_mixin : UcmraMixin ().
Proof. done. Qed.
Canonical Structure unitUR : ucmraT := UcmraT unit unit_ucmra_mixin.
@@ -1085,10 +1085,10 @@ End unit.
(** ** CMRA for the empty type *)
Section empty.
- Instance Empty_set_valid : Valid Empty_set := λ x, False.
- Instance Empty_set_validN : ValidN Empty_set := λ n x, False.
- Instance Empty_set_pcore : PCore Empty_set := λ x, Some x.
- Instance Empty_set_op : Op Empty_set := λ x y, x.
+ Local Instance Empty_set_valid : Valid Empty_set := λ x, False.
+ Local Instance Empty_set_validN : ValidN Empty_set := λ n x, False.
+ Local Instance Empty_set_pcore : PCore Empty_set := λ x, Some x.
+ Local Instance Empty_set_op : Op Empty_set := λ x y, x.
Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
Canonical Structure Empty_setR : cmraT := CmraT Empty_set Empty_set_cmra_mixin.
@@ -1107,12 +1107,12 @@ Section prod.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_/.
- Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
- Instance prod_pcore : PCore (A * B) := λ x,
+ Local Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
+ Local Instance prod_pcore : PCore (A * B) := λ x,
c1 ↠pcore (x.1); c2 ↠pcore (x.2); Some (c1, c2).
Arguments prod_pcore !_ /.
- Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
- Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
+ Local Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
+ Local Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
Lemma prod_pcore_Some (x cx : A * B) :
pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.2).
@@ -1230,7 +1230,7 @@ Arguments prodR : clear implicits.
Section prod_unit.
Context {A B : ucmraT}.
- Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
+ Local Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
Lemma prod_ucmra_mixin : UcmraMixin (A * B).
Proof.
split.
@@ -1264,7 +1264,7 @@ End prod_unit.
Arguments prodUR : clear implicits.
-Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
+Global Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
Proof.
split; first apply _.
@@ -1294,7 +1294,7 @@ Next Obligation.
Qed.
Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
-Instance prodRF_contractive F1 F2 :
+Global Instance prodRF_contractive F1 F2 :
rFunctorContractive F1 → rFunctorContractive F2 →
rFunctorContractive (prodRF F1 F2).
Proof.
@@ -1317,7 +1317,7 @@ Next Obligation.
Qed.
Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
-Instance prodURF_contractive F1 F2 :
+Global Instance prodURF_contractive F1 F2 :
urFunctorContractive F1 → urFunctorContractive F2 →
urFunctorContractive (prodURF F1 F2).
Proof.
@@ -1333,13 +1333,13 @@ Section option.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
- Instance option_valid : Valid (option A) := λ ma,
+ Local Instance option_valid : Valid (option A) := λ ma,
match ma with Some a => ✓ a | None => True end.
- Instance option_validN : ValidN (option A) := λ n ma,
+ Local Instance option_validN : ValidN (option A) := λ n ma,
match ma with Some a => ✓{n} a | None => True end.
- Instance option_pcore : PCore (option A) := λ ma, Some (ma ≫= pcore).
+ Local Instance option_pcore : PCore (option A) := λ ma, Some (ma ≫= pcore).
Arguments option_pcore !_ /.
- Instance option_op : Op (option A) := union_with (λ a b, Some (a ⋅ b)).
+ Local Instance option_op : Op (option A) := union_with (λ a b, Some (a ⋅ b)).
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.
@@ -1430,7 +1430,7 @@ Section option.
Global Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
- Instance option_unit : Unit (option A) := None.
+ Local Instance option_unit : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
Proof. split; [done| |done]. by intros []. Qed.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
@@ -1551,7 +1551,7 @@ Proof.
intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.
-Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
+Global Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A → option B).
Proof.
split; first apply _.
@@ -1576,7 +1576,7 @@ Next Obligation.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
Qed.
-Instance optionURF_contractive F :
+Global Instance optionURF_contractive F :
rFunctorContractive F → urFunctorContractive (optionURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
@@ -1588,7 +1588,7 @@ Program Definition optionRF (F : rFunctor) : rFunctor := {|
|}.
Solve Obligations with apply optionURF.
-Instance optionRF_contractive F :
+Global Instance optionRF_contractive F :
rFunctorContractive F → rFunctorContractive (optionRF F).
Proof. apply optionURF_contractive. Qed.
@@ -1597,10 +1597,10 @@ Section discrete_fun_cmra.
Context `{B : A → ucmraT}.
Implicit Types f g : discrete_fun B.
- Instance discrete_fun_op : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
- Instance discrete_fun_pcore : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
- Instance discrete_fun_valid : Valid (discrete_fun B) := λ f, ∀ x, ✓ f x.
- Instance discrete_fun_validN : ValidN (discrete_fun B) := λ n f, ∀ x, ✓{n} f x.
+ Local Instance discrete_fun_op : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
+ Local Instance discrete_fun_pcore : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
+ Local Instance discrete_fun_valid : Valid (discrete_fun B) := λ f, ∀ x, ✓ f x.
+ Local Instance discrete_fun_validN : ValidN (discrete_fun B) := λ n f, ∀ x, ✓{n} f x.
Definition discrete_fun_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
@@ -1642,7 +1642,7 @@ Section discrete_fun_cmra.
Qed.
Canonical Structure discrete_funR := CmraT (discrete_fun B) discrete_fun_cmra_mixin.
- Instance discrete_fun_unit : Unit (discrete_fun B) := λ x, ε.
+ Local Instance discrete_fun_unit : Unit (discrete_fun B) := λ x, ε.
Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
@@ -1662,7 +1662,7 @@ End discrete_fun_cmra.
Arguments discrete_funR {_} _.
Arguments discrete_funUR {_} _.
-Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
+Global Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
(∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
Proof.
split; first apply _.
@@ -1686,7 +1686,7 @@ Next Obligation.
intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
Qed.
-Instance discrete_funURF_contractive {C} (F : C → urFunctor) :
+Global Instance discrete_funURF_contractive {C} (F : C → urFunctor) :
(∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
diff --git a/iris/algebra/coPset.v b/iris/algebra/coPset.v
index 872cbfb87..69f257c4b 100644
--- a/iris/algebra/coPset.v
+++ b/iris/algebra/coPset.v
@@ -11,10 +11,10 @@ Section coPset.
Canonical Structure coPsetO := discreteO coPset.
- Instance coPset_valid : Valid coPset := λ _, True.
- Instance coPset_unit : Unit coPset := (∅ : coPset).
- Instance coPset_op : Op coPset := union.
- Instance coPset_pcore : PCore coPset := Some.
+ Local Instance coPset_valid : Valid coPset := λ _, True.
+ Local Instance coPset_unit : Unit coPset := (∅ : coPset).
+ Local Instance coPset_op : Op coPset := union.
+ Local Instance coPset_pcore : PCore coPset := Some.
Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y.
Proof. done. Qed.
@@ -69,15 +69,15 @@ Section coPset_disj.
Arguments op _ _ !_ !_ /.
Canonical Structure coPset_disjO := leibnizO coPset_disj.
- Instance coPset_disj_valid : Valid coPset_disj := λ X,
+ Local Instance coPset_disj_valid : Valid coPset_disj := λ X,
match X with CoPset _ => True | CoPsetBot => False end.
- Instance coPset_disj_unit : Unit coPset_disj := CoPset ∅.
- Instance coPset_disj_op : Op coPset_disj := λ X Y,
+ Local Instance coPset_disj_unit : Unit coPset_disj := CoPset ∅.
+ Local Instance coPset_disj_op : Op coPset_disj := λ X Y,
match X, Y with
| CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetBot
| _, _ => CoPsetBot
end.
- Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ε.
+ Local Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ε.
Ltac coPset_disj_solve :=
repeat (simpl || case_decide);
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index 948c57c22..424fcedc1 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -50,8 +50,8 @@ Record tower := {
tower_car k :> A k;
g_tower k : g k (tower_car (S k)) ≡ tower_car k
}.
-Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
-Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
+Global Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
+Global Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
Definition tower_ofe_mixin : OfeMixin tower.
Proof.
split.
@@ -98,7 +98,7 @@ Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
-Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
+Global Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
Proof. by intros X Y HX. Qed.
Definition project (k : nat) : T -n> A k := OfeMor (λ X : T, tower_car X k).
@@ -151,8 +151,8 @@ Qed.
Program Definition embed (k : nat) (x : A k) : T :=
{| tower_car n := embed_coerce n x |}.
Next Obligation. intros k x i. apply g_embed_coerce. Qed.
-Instance: Params (@embed) 1 := {}.
-Instance embed_ne k : NonExpansive (embed k).
+Global Instance: Params (@embed) 1 := {}.
+Global Instance embed_ne k : NonExpansive (embed k).
Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
Definition embed' (k : nat) : A k -n> T := OfeMor (embed k).
Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
@@ -188,7 +188,7 @@ Next Obligation.
by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed.
Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
-Instance unfold_ne : NonExpansive unfold.
+Global Instance unfold_ne : NonExpansive unfold.
Proof.
intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
(conv_compl n (unfold_chain Y)) /= (HXY (S n)).
@@ -201,7 +201,7 @@ Next Obligation.
rewrite g_S -oFunctor_map_compose.
apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
Qed.
-Instance fold_ne : NonExpansive fold.
+Global Instance fold_ne : NonExpansive fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index e0e5ce8fe..23a2bc2be 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -17,13 +17,13 @@ Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}.
-Instance: Params (@Cinl) 2 := {}.
-Instance: Params (@Cinr) 2 := {}.
-Instance: Params (@CsumBot) 2 := {}.
+Global Instance: Params (@Cinl) 2 := {}.
+Global Instance: Params (@Cinr) 2 := {}.
+Global Instance: Params (@CsumBot) 2 := {}.
-Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
+Global Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
match x with Cinl a => Some a | _ => None end.
-Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
+Global Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
match x with Cinr b => Some b | _ => None end.
Section ofe.
@@ -120,7 +120,7 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
| Cinr b => Cinr (fB b)
| CsumBot => CsumBot
end.
-Instance: Params (@csum_map) 4 := {}.
+Global Instance: Params (@csum_map) 4 := {}.
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed.
@@ -131,14 +131,14 @@ Proof. by destruct x. Qed.
Lemma csum_map_ext {A A' B B' : ofeT} (f f' : A → A') (g g' : B → B') x :
(∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
Proof. by destruct x; constructor. Qed.
-Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
+Global Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
(@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
Definition csumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
csumO A B -n> csumO A' B' :=
OfeMor (csum_map f g).
-Instance csumO_map_ne A A' B B' :
+Global Instance csumO_map_ne A A' B B' :
NonExpansive2 (@csumO_map A A' B B').
Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
@@ -148,25 +148,25 @@ Implicit Types a : A.
Implicit Types b : B.
(* CMRA *)
-Instance csum_valid : Valid (csum A B) := λ x,
+Local Instance csum_valid : Valid (csum A B) := λ x,
match x with
| Cinl a => ✓ a
| Cinr b => ✓ b
| CsumBot => False
end.
-Instance csum_validN : ValidN (csum A B) := λ n x,
+Local Instance csum_validN : ValidN (csum A B) := λ n x,
match x with
| Cinl a => ✓{n} a
| Cinr b => ✓{n} b
| CsumBot => False
end.
-Instance csum_pcore : PCore (csum A B) := λ x,
+Local Instance csum_pcore : PCore (csum A B) := λ x,
match x with
| Cinl a => Cinl <$> pcore a
| Cinr b => Cinr <$> pcore b
| CsumBot => Some CsumBot
end.
-Instance csum_op : Op (csum A B) := λ x y,
+Local Instance csum_op : Op (csum A B) := λ x y,
match x, y with
| Cinl a, Cinl a' => Cinl (a â‹… a')
| Cinr b, Cinr b' => Cinr (b â‹… b')
@@ -364,7 +364,7 @@ End cmra.
Arguments csumR : clear implicits.
(* Functor *)
-Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
+Global Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
CmraMorphism f → CmraMorphism g → CmraMorphism (csum_map f g).
Proof.
split; try apply _.
@@ -389,7 +389,7 @@ Next Obligation.
apply csum_map_ext=>y; apply rFunctor_map_compose.
Qed.
-Instance csumRF_contractive Fa Fb :
+Global Instance csumRF_contractive Fa Fb :
rFunctorContractive Fa → rFunctorContractive Fb →
rFunctorContractive (csumRF Fa Fb).
Proof.
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index d3b668f05..ace017d6d 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -62,7 +62,7 @@ Section dfrac.
Proof. by injection 1. Qed.
(** An element is valid as long as the sum of its content is less than one. *)
- Instance dfrac_valid : Valid dfrac := λ dq,
+ Local Instance dfrac_valid : Valid dfrac := λ dq,
match dq with
| DfracOwn q => q ≤ 1
| DfracDiscarded => True
@@ -72,7 +72,7 @@ Section dfrac.
(** As in the fractional camera the core is undefined for elements denoting
ownership of a fraction. For elements denoting the knowledge that a fraction has
been discarded the core is the identity function. *)
- Instance dfrac_pcore : PCore dfrac := λ dq,
+ Local Instance dfrac_pcore : PCore dfrac := λ dq,
match dq with
| DfracOwn q => None
| DfracDiscarded => Some DfracDiscarded
@@ -81,7 +81,7 @@ Section dfrac.
(** When elements are combined, ownership is added together and knowledge of
discarded fractions is combined with the max operation. *)
- Instance dfrac_op : Op dfrac := λ dq dp,
+ Local Instance dfrac_op : Op dfrac := λ dq dp,
match dq, dp with
| DfracOwn q, DfracOwn q' => DfracOwn (q + q')
| DfracOwn q, DfracDiscarded => DfracBoth q
diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index fa43cb751..ee2b110ca 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -107,10 +107,10 @@ Implicit Types a b : A.
Implicit Types x y z : validity A.
Arguments valid _ _ !_ /.
-Instance validity_valid : Valid (validity A) := validity_is_valid.
-Instance validity_equiv : Equiv (validity A) := λ x y,
+Local Instance validity_valid : Valid (validity A) := validity_is_valid.
+Local Instance validity_equiv : Equiv (validity A) := λ x y,
(valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Instance validity_equivalence : Equivalence (@equiv (validity A) _).
+Local Instance validity_equivalence : Equivalence (@equiv (validity A) _).
Proof.
split; unfold equiv, validity_equiv.
- by intros [x px ?]; simpl.
@@ -120,11 +120,11 @@ Proof.
Qed.
Canonical Structure validityO : ofeT := discreteO (validity A).
-Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
+Local Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
Proof. by split; apply: dra_valid_proper. Qed.
Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
+Local Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
Proof.
intros x1 x2 Hx y1 y2 Hy; split.
- by rewrite Hy (symmetry_iff (##) x1) (symmetry_iff (##) x2) Hx.
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index c5d9ef110..a54699658 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -10,14 +10,14 @@ Inductive excl (A : Type) :=
Arguments Excl {_} _.
Arguments ExclBot {_}.
-Instance: Params (@Excl) 1 := {}.
-Instance: Params (@ExclBot) 1 := {}.
+Global Instance: Params (@Excl) 1 := {}.
+Global Instance: Params (@ExclBot) 1 := {}.
Notation excl' A := (option (excl A)).
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).
-Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
+Global Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end.
Section excl.
@@ -70,12 +70,12 @@ Global Instance ExclBot_discrete : Discrete (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *)
-Instance excl_valid : Valid (excl A) := λ x,
+Local Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ => True | ExclBot => False end.
-Instance excl_validN : ValidN (excl A) := λ n x,
+Local Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ => True | ExclBot => False end.
-Instance excl_pcore : PCore (excl A) := λ _, None.
-Instance excl_op : Op (excl A) := λ x y, ExclBot.
+Local Instance excl_pcore : PCore (excl A) := λ _, None.
+Local Instance excl_op : Op (excl A) := λ x y, ExclBot.
Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof.
@@ -128,15 +128,15 @@ Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : ofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
-Instance excl_map_ne {A B : ofeT} n :
+Global Instance excl_map_ne {A B : ofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Instance excl_map_cmra_morphism {A B : ofeT} (f : A → B) :
+Global Instance excl_map_cmra_morphism {A B : ofeT} (f : A → B) :
NonExpansive f → CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
Definition exclO_map {A B} (f : A -n> B) : exclO A -n> exclO B :=
OfeMor (excl_map f).
-Instance exclO_map_ne A B : NonExpansive (@exclO_map A B).
+Global Instance exclO_map_ne A B : NonExpansive (@exclO_map A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
Program Definition exclRF (F : oFunctor) : rFunctor := {|
@@ -155,7 +155,7 @@ Next Obligation.
apply excl_map_ext=>y; apply oFunctor_map_compose.
Qed.
-Instance exclRF_contractive F :
+Global Instance exclRF_contractive F :
oFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 6135787f1..9dd0a1156 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -15,9 +15,9 @@ Notation frac := Qp (only parsing).
Section frac.
Canonical Structure fracO := leibnizO frac.
- Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qp.
- Instance frac_pcore : PCore frac := λ _, None.
- Instance frac_op : Op frac := λ x y, (x + y)%Qp.
+ Local Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qp.
+ Local Instance frac_pcore : PCore frac := λ _, None.
+ Local Instance frac_op : Op frac := λ x y, (x + y)%Qp.
Lemma frac_valid' p : ✓ p ↔ (p ≤ 1)%Qp.
Proof. done. Qed.
diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 98f36dfbd..9ff96afff 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -6,11 +6,11 @@ From iris.prelude Require Import options.
Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}
(x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Instance: Params (@discrete_fun_insert) 5 := {}.
+Global Instance: Params (@discrete_fun_insert) 5 := {}.
Definition discrete_fun_singleton `{EqDecision A} {B : A → ucmraT}
(x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
-Instance: Params (@discrete_fun_singleton) 5 := {}.
+Global Instance: Params (@discrete_fun_singleton) 5 := {}.
Section ofe.
Context `{Heqdec : EqDecision A} {B : A → ofeT}.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 35a53a731..89fc7ad19 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -8,7 +8,7 @@ Context `{Countable K} {A : ofeT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
-Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
+Local Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
∀ i, m1 !! i ≡{n}≡ m2 !! i.
Definition gmap_ofe_mixin : OfeMixin (gmap K A).
Proof.
@@ -105,17 +105,17 @@ Lemma merge_ne `{Countable K} {A B C : ofeT} (f g : option A → option B → op
((dist n) ==> (dist n) ==> (dist n))%signature f g →
((dist n) ==> (dist n) ==> (dist n))%signature (merge (M:=gmap K) f) (merge g).
Proof. by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge //; apply Hf. Qed.
-Instance union_with_proper `{Countable K} {A : ofeT} n :
+Global Instance union_with_proper `{Countable K} {A : ofeT} n :
Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
(dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
-Instance map_fmap_proper `{Countable K} {A B : ofeT} (f : A → B) n :
+Global Instance map_fmap_proper `{Countable K} {A B : ofeT} (f : A → B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
-Instance map_zip_with_proper `{Countable K} {A B C : ofeT} (f : A → B → C) n :
+Global Instance map_zip_with_proper `{Countable K} {A B C : ofeT} (f : A → B → C) n :
Proper (dist n ==> dist n ==> dist n) f →
Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
Proof.
@@ -141,11 +141,11 @@ Section cmra.
Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
-Instance gmap_unit : Unit (gmap K A) := (∅ : gmap K A).
-Instance gmap_op : Op (gmap K A) := merge op.
-Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
-Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
-Instance gmap_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
+Local Instance gmap_unit : Unit (gmap K A) := (∅ : gmap K A).
+Local Instance gmap_op : Op (gmap K A) := merge op.
+Local Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
+Local Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
+Local Instance gmap_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
Proof. by apply lookup_merge. Qed.
@@ -643,10 +643,10 @@ Qed.
End unital_properties.
(** Functor *)
-Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A → B) n :
+Global Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A → B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A → B)
+Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A → B)
`{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A → gmap K B).
Proof.
split; try apply _.
@@ -657,7 +657,7 @@ Proof.
Qed.
Definition gmapO_map `{Countable K} {A B} (f: A -n> B) :
gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A → gmapO K B).
-Instance gmapO_map_ne `{Countable K} {A B} :
+Global Instance gmapO_map_ne `{Countable K} {A B} :
NonExpansive (@gmapO_map K _ _ A B).
Proof.
intros n f g Hf m k; rewrite /= !lookup_fmap.
@@ -679,7 +679,7 @@ Next Obligation.
intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
Qed.
-Instance gmapOF_contractive K `{Countable K} F :
+Global Instance gmapOF_contractive K `{Countable K} F :
oFunctorContractive F → oFunctorContractive (gmapOF K F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_contractive.
@@ -700,7 +700,7 @@ Next Obligation.
intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
Qed.
-Instance gmapURF_contractive K `{Countable K} F :
+Global Instance gmapURF_contractive K `{Countable K} F :
rFunctorContractive F → urFunctorContractive (gmapURF K F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
@@ -712,6 +712,6 @@ Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
|}.
Solve Obligations with apply gmapURF.
-Instance gmapRF_contractive K `{Countable K} F :
+Global Instance gmapRF_contractive K `{Countable K} F :
rFunctorContractive F → rFunctorContractive (gmapRF K F).
Proof. apply gmapURF_contractive. Qed.
diff --git a/iris/algebra/gmultiset.v b/iris/algebra/gmultiset.v
index 5e2f02f28..2cacca3c8 100644
--- a/iris/algebra/gmultiset.v
+++ b/iris/algebra/gmultiset.v
@@ -10,11 +10,11 @@ Section gmultiset.
Canonical Structure gmultisetO := discreteO (gmultiset K).
- Instance gmultiset_valid : Valid (gmultiset K) := λ _, True.
- Instance gmultiset_validN : ValidN (gmultiset K) := λ _ _, True.
- Instance gmultiset_unit : Unit (gmultiset K) := (∅ : gmultiset K).
- Instance gmultiset_op : Op (gmultiset K) := disj_union.
- Instance gmultiset_pcore : PCore (gmultiset K) := λ X, Some ∅.
+ Local Instance gmultiset_valid : Valid (gmultiset K) := λ _, True.
+ Local Instance gmultiset_validN : ValidN (gmultiset K) := λ _ _, True.
+ Local Instance gmultiset_unit : Unit (gmultiset K) := (∅ : gmultiset K).
+ Local Instance gmultiset_op : Op (gmultiset K) := disj_union.
+ Local Instance gmultiset_pcore : PCore (gmultiset K) := λ X, Some ∅.
Lemma gmultiset_op_disj_union X Y : X ⋅ Y = X ⊎ Y.
Proof. done. Qed.
diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index c95e6c370..18d129bb5 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -10,10 +10,10 @@ Section gset.
Canonical Structure gsetO := discreteO (gset K).
- Instance gset_valid : Valid (gset K) := λ _, True.
- Instance gset_unit : Unit (gset K) := (∅ : gset K).
- Instance gset_op : Op (gset K) := union.
- Instance gset_pcore : PCore (gset K) := λ X, Some X.
+ Local Instance gset_valid : Valid (gset K) := λ _, True.
+ Local Instance gset_unit : Unit (gset K) := (∅ : gset K).
+ Local Instance gset_op : Op (gset K) := union.
+ Local Instance gset_pcore : PCore (gset K) := λ X, Some X.
Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y.
Proof. done. Qed.
@@ -85,15 +85,15 @@ Section gset_disj.
Canonical Structure gset_disjO := leibnizO (gset_disj K).
- Instance gset_disj_valid : Valid (gset_disj K) := λ X,
+ Local Instance gset_disj_valid : Valid (gset_disj K) := λ X,
match X with GSet _ => True | GSetBot => False end.
- Instance gset_disj_unit : Unit (gset_disj K) := GSet ∅.
- Instance gset_disj_op : Op (gset_disj K) := λ X Y,
+ Local Instance gset_disj_unit : Unit (gset_disj K) := GSet ∅.
+ Local Instance gset_disj_op : Op (gset_disj K) := λ X Y,
match X, Y with
| GSet X, GSet Y => if decide (X ## Y) then GSet (X ∪ Y) else GSetBot
| _, _ => GSetBot
end.
- Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ε.
+ Local Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ε.
Ltac gset_disj_solve :=
repeat (simpl || case_decide);
diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index c410935a6..97fc0395d 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -18,8 +18,8 @@ Definition excl_auth_frag {A : ofeT} (a : A) : excl_authR A :=
Typeclasses Opaque excl_auth_auth excl_auth_frag.
-Instance: Params (@excl_auth_auth) 1 := {}.
-Instance: Params (@excl_auth_frag) 2 := {}.
+Global Instance: Params (@excl_auth_auth) 1 := {}.
+Global Instance: Params (@excl_auth_frag) 2 := {}.
Notation "â—E a" := (excl_auth_auth a) (at level 10).
Notation "â—¯E a" := (excl_auth_frag a) (at level 10).
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index b3bed379c..6a6da0da1 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -21,8 +21,8 @@ Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A :=
Typeclasses Opaque frac_auth_auth frac_auth_frag.
-Instance: Params (@frac_auth_auth) 1 := {}.
-Instance: Params (@frac_auth_frag) 2 := {}.
+Global Instance: Params (@frac_auth_auth) 1 := {}.
+Global Instance: Params (@frac_auth_frag) 2 := {}.
Notation "â—F a" := (frac_auth_auth a) (at level 10).
Notation "â—¯F{ q } a" := (frac_auth_frag q a) (at level 10, format "â—¯F{ q } a").
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 137e1cd55..12e9b7252 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -473,7 +473,7 @@ Next Obligation.
rewrite Hagree. rewrite agree_map_to_agree. done.
Qed.
-Instance gmap_viewURF_contractive (K : Type) `{Countable K} F :
+Global Instance gmap_viewURF_contractive (K : Type) `{Countable K} F :
oFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
@@ -493,7 +493,7 @@ Program Definition gmap_viewRF (K : Type) `{Countable K} (F : oFunctor) : rFunct
|}.
Solve Obligations with apply gmap_viewURF.
-Instance gmap_viewRF_contractive (K : Type) `{Countable K} F :
+Global Instance gmap_viewRF_contractive (K : Type) `{Countable K} F :
oFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
Proof. apply gmap_viewURF_contractive. Qed.
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index e7f1f0a39..bbfd9d132 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -39,8 +39,8 @@ Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
-Instance: Params (@ufrac_auth_auth) 2 := {}.
-Instance: Params (@ufrac_auth_frag) 2 := {}.
+Global Instance: Params (@ufrac_auth_auth) 2 := {}.
+Global Instance: Params (@ufrac_auth_frag) 2 := {}.
Notation "â—U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "â—U{ q } a").
Notation "â—¯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "â—¯U{ q } a").
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 363a06e51..9666d5a09 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -7,7 +7,7 @@ Section ofe.
Context {A : ofeT}.
Implicit Types l : list A.
-Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
+Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
@@ -98,27 +98,27 @@ End ofe.
Arguments listO : clear implicits.
(** Non-expansiveness of higher-order list functions and big-ops *)
-Instance list_fmap_ne {A B : ofeT} (f : A → B) n :
+Global Instance list_fmap_ne {A B : ofeT} (f : A → B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
-Instance list_omap_ne {A B : ofeT} (f : A → option B) n :
+Global Instance list_omap_ne {A B : ofeT} (f : A → option B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (omap (M:=list) f).
Proof.
intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
destruct (Hf _ _ Hx); [f_equiv|]; auto.
Qed.
-Instance imap_ne {A B : ofeT} (f : nat → A → B) n :
+Global Instance imap_ne {A B : ofeT} (f : nat → A → B) n :
(∀ i, Proper (dist n ==> dist n) (f i)) → Proper (dist n ==> dist n) (imap f).
Proof.
intros Hf l1 l2 Hl. revert f Hf.
induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
Qed.
-Instance list_bind_ne {A B : ofeT} (f : A → list A) n :
+Global Instance list_bind_ne {A B : ofeT} (f : A → list A) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (mbind f).
Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
-Instance list_join_ne {A : ofeT} : NonExpansive (mjoin (M:=list) (A:=A)).
+Global Instance list_join_ne {A : ofeT} : NonExpansive (mjoin (M:=list) (A:=A)).
Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
-Instance zip_with_ne {A B C : ofeT} (f : A → B → C) n :
+Global Instance zip_with_ne {A B C : ofeT} (f : A → B → C) n :
Proper (dist n ==> dist n ==> dist n) f →
Proper (dist n ==> dist n ==> dist n) (zip_with f).
Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
@@ -141,7 +141,7 @@ Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n :
Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
OfeMor (fmap f : listO A → listO B).
-Instance listO_map_ne A B : NonExpansive (@listO_map A B).
+Global Instance listO_map_ne A B : NonExpansive (@listO_map A B).
Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
Program Definition listOF (F : oFunctor) : oFunctor := {|
@@ -160,7 +160,7 @@ Next Obligation.
apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
Qed.
-Instance listOF_contractive F :
+Global Instance listOF_contractive F :
oFunctorContractive F → oFunctorContractive (listOF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
@@ -172,17 +172,17 @@ Section cmra.
Implicit Types l : list A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
- Instance list_op : Op (list A) :=
+ Local Instance list_op : Op (list A) :=
fix go l1 l2 := let _ : Op _ := @go in
match l1, l2 with
| [], _ => l2
| _, [] => l1
| x :: l1, y :: l2 => x â‹… y :: l1 â‹… l2
end.
- Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
+ Local Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
- Instance list_valid : Valid (list A) := Forall (λ x, ✓ x).
- Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
+ Local Instance list_valid : Valid (list A) := Forall (λ x, ✓ x).
+ Local Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
Lemma cons_valid l x : ✓ (x :: l) ↔ ✓ x ∧ ✓ l.
Proof. apply Forall_cons. Qed.
@@ -299,7 +299,7 @@ End cmra.
Arguments listR : clear implicits.
Arguments listUR : clear implicits.
-Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
+Global Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
replicate n ε ++ [x].
Section properties.
@@ -515,7 +515,7 @@ Section properties.
End properties.
(** Functor *)
-Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A → B)
+Global Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A → B)
`{!CmraMorphism f} : CmraMorphism (fmap f : list A → list B).
Proof.
split; try apply _.
@@ -543,7 +543,7 @@ Next Obligation.
apply list_fmap_equiv_ext=>y; apply urFunctor_map_compose.
Qed.
-Instance listURF_contractive F :
+Global Instance listURF_contractive F :
urFunctorContractive F → urFunctorContractive (listURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
@@ -555,6 +555,6 @@ Program Definition listRF (F : urFunctor) : rFunctor := {|
|}.
Solve Obligations with apply listURF.
-Instance listRF_contractive F :
+Global Instance listRF_contractive F :
urFunctorContractive F → rFunctorContractive (listRF F).
Proof. apply listURF_contractive. Qed.
diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index c662b4229..d8819bf5a 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
(** * Local updates *)
Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
-Instance: Params (@local_update) 1 := {}.
+Global Instance: Params (@local_update) 1 := {}.
Infix "~l~>" := local_update (at level 70).
Section updates.
diff --git a/iris/algebra/namespace_map.v b/iris/algebra/namespace_map.v
index aae353ecb..100e6dde4 100644
--- a/iris/algebra/namespace_map.v
+++ b/iris/algebra/namespace_map.v
@@ -23,26 +23,26 @@ Add Printing Constructor namespace_map.
Arguments NamespaceMap {_} _ _.
Arguments namespace_map_data_proj {_} _.
Arguments namespace_map_token_proj {_} _.
-Instance: Params (@NamespaceMap) 1 := {}.
-Instance: Params (@namespace_map_data_proj) 1 := {}.
-Instance: Params (@namespace_map_token_proj) 1 := {}.
+Global Instance: Params (@NamespaceMap) 1 := {}.
+Global Instance: Params (@namespace_map_data_proj) 1 := {}.
+Global Instance: Params (@namespace_map_token_proj) 1 := {}.
(** TODO: [positives_flatten] violates the namespace abstraction. *)
Definition namespace_map_data {A : cmraT} (N : namespace) (a : A) : namespace_map A :=
NamespaceMap {[ positives_flatten N := a ]} ε.
Definition namespace_map_token {A : cmraT} (E : coPset) : namespace_map A :=
NamespaceMap ∅ (CoPset E).
-Instance: Params (@namespace_map_data) 2 := {}.
+Global Instance: Params (@namespace_map_data) 2 := {}.
(* Ofe *)
Section ofe.
Context {A : ofeT}.
Implicit Types x y : namespace_map A.
-Instance namespace_map_equiv : Equiv (namespace_map A) := λ x y,
+Local Instance namespace_map_equiv : Equiv (namespace_map A) := λ x y,
namespace_map_data_proj x ≡ namespace_map_data_proj y ∧
namespace_map_token_proj x = namespace_map_token_proj y.
-Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
+Local Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
namespace_map_data_proj x ≡{n}≡ namespace_map_data_proj y ∧
namespace_map_token_proj x = namespace_map_token_proj y.
@@ -91,7 +91,7 @@ Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
Global Instance namespace_map_token_discrete E : Discrete (@namespace_map_token A E).
Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
-Instance namespace_map_valid : Valid (namespace_map A) := λ x,
+Local Instance namespace_map_valid : Valid (namespace_map A) := λ x,
match namespace_map_token_proj x with
| CoPset E =>
✓ (namespace_map_data_proj x) ∧
@@ -100,7 +100,7 @@ Instance namespace_map_valid : Valid (namespace_map A) := λ x,
| CoPsetBot => False
end.
Global Arguments namespace_map_valid !_ /.
-Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
+Local Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
match namespace_map_token_proj x with
| CoPset E =>
✓{n} (namespace_map_data_proj x) ∧
@@ -109,9 +109,9 @@ Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
| CoPsetBot => False
end.
Global Arguments namespace_map_validN !_ /.
-Instance namespace_map_pcore : PCore (namespace_map A) := λ x,
+Local Instance namespace_map_pcore : PCore (namespace_map A) := λ x,
Some (NamespaceMap (core (namespace_map_data_proj x)) ε).
-Instance namespace_map_op : Op (namespace_map A) := λ x y,
+Local Instance namespace_map_op : Op (namespace_map A) := λ x y,
NamespaceMap (namespace_map_data_proj x â‹… namespace_map_data_proj y)
(namespace_map_token_proj x â‹… namespace_map_token_proj y).
@@ -193,7 +193,7 @@ Proof.
by intros [?%cmra_discrete_valid ?].
Qed.
-Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
+Local Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
Lemma namespace_map_ucmra_mixin : UcmraMixin (namespace_map A).
Proof.
split; simpl.
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index fa74e1172..8fb3dd44b 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -3,10 +3,10 @@ From iris.prelude Require Import options.
(** ** Natural numbers with [add] as the operation. *)
Section nat.
- Instance nat_valid : Valid nat := λ x, True.
- Instance nat_validN : ValidN nat := λ n x, True.
- Instance nat_pcore : PCore nat := λ x, Some 0.
- Instance nat_op : Op nat := plus.
+ Local Instance nat_valid : Valid nat := λ x, True.
+ Local Instance nat_validN : ValidN nat := λ n x, True.
+ Local Instance nat_pcore : PCore nat := λ x, Some 0.
+ Local Instance nat_op : Op nat := plus.
Definition nat_op_plus x y : x â‹… y = x + y := eq_refl.
Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
Proof. by rewrite nat_le_sum. Qed.
@@ -23,7 +23,7 @@ Section nat.
Global Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
- Instance nat_unit : Unit nat := 0.
+ Local Instance nat_unit : Unit nat := 0.
Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
@@ -51,11 +51,11 @@ Add Printing Constructor max_nat.
Canonical Structure max_natO := leibnizO max_nat.
Section max_nat.
- Instance max_nat_unit : Unit max_nat := MaxNat 0.
- Instance max_nat_valid : Valid max_nat := λ x, True.
- Instance max_nat_validN : ValidN max_nat := λ n x, True.
- Instance max_nat_pcore : PCore max_nat := Some.
- Instance max_nat_op : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
+ Local Instance max_nat_unit : Unit max_nat := MaxNat 0.
+ Local Instance max_nat_valid : Valid max_nat := λ x, True.
+ Local Instance max_nat_validN : ValidN max_nat := λ n x, True.
+ Local Instance max_nat_pcore : PCore max_nat := Some.
+ Local Instance max_nat_op : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
Definition max_nat_op_max x y : MaxNat x â‹… MaxNat y = MaxNat (x `max` y) := eq_refl.
Lemma max_nat_included x y : x ≼ y ↔ max_nat_car x ≤ max_nat_car y.
@@ -107,10 +107,10 @@ Add Printing Constructor min_nat.
Canonical Structure min_natO := leibnizO min_nat.
Section min_nat.
- Instance min_nat_valid : Valid min_nat := λ x, True.
- Instance min_nat_validN : ValidN min_nat := λ n x, True.
- Instance min_nat_pcore : PCore min_nat := Some.
- Instance min_nat_op : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
+ Local Instance min_nat_valid : Valid min_nat := λ x, True.
+ Local Instance min_nat_validN : ValidN min_nat := λ n x, True.
+ Local Instance min_nat_pcore : PCore min_nat := Some.
+ Local Instance min_nat_op : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
Definition min_nat_op_min x y : MinNat x â‹… MinNat y = MinNat (x `min` y) := eq_refl.
Lemma min_nat_included (x y : min_nat) : x ≼ y ↔ min_nat_car y ≤ min_nat_car x.
@@ -159,10 +159,10 @@ End min_nat.
(** ** Positive integers with [Pos.add] as the operation. *)
Section positive.
- Instance pos_valid : Valid positive := λ x, True.
- Instance pos_validN : ValidN positive := λ n x, True.
- Instance pos_pcore : PCore positive := λ x, None.
- Instance pos_op : Op positive := Pos.add.
+ Local Instance pos_valid : Valid positive := λ x, True.
+ Local Instance pos_validN : ValidN positive := λ n x, True.
+ Local Instance pos_pcore : PCore positive := λ x, None.
+ Local Instance pos_op : Op positive := Pos.add.
Definition pos_op_plus x y : x â‹… y = (x + y)%positive := eq_refl.
Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
Proof. by rewrite Plt_sum. Qed.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 04de827ca..f8b949fdb 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -13,7 +13,7 @@ Set Primitive Projections.
(** Unbundled version *)
Class Dist A := dist : nat → relation A.
-Instance: Params (@dist) 3 := {}.
+Global Instance: Params (@dist) 3 := {}.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
@@ -102,7 +102,7 @@ Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
Class Discrete {A : ofeT} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
Arguments discrete {_} _ {_} _ _.
Global Hint Mode Discrete + ! : typeclass_instances.
-Instance: Params (@Discrete) 1 := {}.
+Global Instance: Params (@Discrete) 1 := {}.
Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
@@ -171,7 +171,7 @@ Section ofe.
Proof. intros; eauto using dist_le. Qed.
(** [ne_proper] and [ne_proper_2] are not instances to improve efficiency of
type class search during setoid rewriting.
- Instances of [NonExpansive{,2}] are hence accompanied by instances of
+ Local Instances of [NonExpansive{,2}] are hence accompanied by instances of
[Proper] built using these lemmas. *)
Lemma ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
Proper ((≡) ==> (≡)) f.
@@ -221,7 +221,7 @@ Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.
Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
-Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
+Global Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.
Section contractive.
@@ -472,11 +472,11 @@ Section fixpointAB.
Lemma fixpoint_B_unfold : fB fixpoint_A fixpoint_B ≡ fixpoint_B.
Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.
- Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
+ Local Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
Proof using fA_contractive.
apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
Qed.
- Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
+ Local Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
Proof using fB_contractive.
apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
Qed.
@@ -541,8 +541,8 @@ Section ofe_mor.
Context {A B : ofeT}.
Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, ofe_mor_ne. Qed.
- Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
- Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+ Local Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
+ Local Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
Proof.
split.
@@ -584,18 +584,18 @@ End ofe_mor.
Arguments ofe_morO : clear implicits.
Notation "A -n> B" :=
(ofe_morO A B) (at level 99, B at level 200, right associativity).
-Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
+Global Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
Inhabited (A -n> B) := populate (λne _, inhabitant).
(** Identity and composition and constant function *)
Definition cid {A} : A -n> A := OfeMor id.
-Instance: Params (@cid) 1 := {}.
+Global Instance: Params (@cid) 1 := {}.
Definition cconst {A B : ofeT} (x : B) : A -n> B := OfeMor (const x).
-Instance: Params (@cconst) 2 := {}.
+Global Instance: Params (@cconst) 2 := {}.
Definition ccompose {A B C}
(f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f ∘ g).
-Instance: Params (@ccompose) 3 := {}.
+Global Instance: Params (@ccompose) 3 := {}.
Infix "â—Ž" := ccompose (at level 40, left associativity).
Global Instance ccompose_ne {A B C} :
NonExpansive2 (@ccompose A B C).
@@ -604,13 +604,13 @@ Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
(* Function space maps *)
Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
(h : A -n> B) : A' -n> B' := g â—Ž h â—Ž f.
-Instance ofe_mor_map_ne {A A' B B'} n :
+Global Instance ofe_mor_map_ne {A A' B B'} n :
Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B').
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Definition ofe_morO_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
(A -n> B) -n> (A' -n> B') := OfeMor (ofe_mor_map f g).
-Instance ofe_morO_map_ne {A A' B B'} :
+Global Instance ofe_morO_map_ne {A A' B B'} :
NonExpansive2 (@ofe_morO_map A A' B B').
Proof.
intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
@@ -619,7 +619,7 @@ Qed.
(** * Unit type *)
Section unit.
- Instance unit_dist : Dist unit := λ _ _ _, True.
+ Local Instance unit_dist : Dist unit := λ _ _ _, True.
Definition unit_ofe_mixin : OfeMixin unit.
Proof. by repeat split; try exists 0. Qed.
Canonical Structure unitO : ofeT := OfeT unit unit_ofe_mixin.
@@ -633,7 +633,7 @@ End unit.
(** * Empty type *)
Section empty.
- Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
+ Local Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
Proof. by repeat split; try exists 0. Qed.
Canonical Structure Empty_setO : ofeT := OfeT Empty_set Empty_set_ofe_mixin.
@@ -649,7 +649,7 @@ End empty.
Section product.
Context {A B : ofeT}.
- Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
+ Local Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
Global Instance pair_ne :
NonExpansive2 (@pair A B) := _.
Global Instance fst_ne : NonExpansive (@fst A B) := _.
@@ -683,13 +683,13 @@ End product.
Arguments prodO : clear implicits.
Typeclasses Opaque prod_dist.
-Instance prod_map_ne {A A' B B' : ofeT} n :
+Global Instance prod_map_ne {A A' B B' : ofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@prod_map A A' B B').
Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
Definition prodO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
prodO A B -n> prodO A' B' := OfeMor (prod_map f g).
-Instance prodO_map_ne {A A' B B'} :
+Global Instance prodO_map_ne {A A' B B'} :
NonExpansive2 (@prodO_map A A' B B').
Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
@@ -707,7 +707,7 @@ Record oFunctor := OFunctor {
oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.
Existing Instance oFunctor_map_ne.
-Instance: Params (@oFunctor_map) 9 := {}.
+Global Instance: Params (@oFunctor_map) 9 := {}.
Declare Scope oFunctor_scope.
Delimit Scope oFunctor_scope with OF.
@@ -743,14 +743,14 @@ Next Obligation.
rewrite -oFunctor_map_compose. apply equiv_dist=> n. apply oFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
-Instance oFunctor_oFunctor_compose_contractive_1 (F1 F2 : oFunctor)
+Global Instance oFunctor_oFunctor_compose_contractive_1 (F1 F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
oFunctorContractive F1 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
-Instance oFunctor_oFunctor_compose_contractive_2 (F1 F2 : oFunctor)
+Global Instance oFunctor_oFunctor_compose_contractive_2 (F1 F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
oFunctorContractive F2 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
Proof.
@@ -763,7 +763,7 @@ Program Definition constOF (B : ofeT) : oFunctor :=
Solve Obligations with done.
Coercion constOF : ofeT >-> oFunctor.
-Instance constOF_contractive B : oFunctorContractive (constOF B).
+Global Instance constOF_contractive B : oFunctorContractive (constOF B).
Proof. rewrite /oFunctorContractive; apply _. Qed.
Program Definition idOF : oFunctor :=
@@ -786,7 +786,7 @@ Next Obligation.
Qed.
Notation "F1 * F2" := (prodOF F1%OF F2%OF) : oFunctor_scope.
-Instance prodOF_contractive F1 F2 :
+Global Instance prodOF_contractive F1 F2 :
oFunctorContractive F1 → oFunctorContractive F2 →
oFunctorContractive (prodOF F1 F2).
Proof.
@@ -813,7 +813,7 @@ Next Obligation.
Qed.
Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
-Instance ofe_morOF_contractive F1 F2 :
+Global Instance ofe_morOF_contractive F1 F2 :
oFunctorContractive F1 → oFunctorContractive F2 →
oFunctorContractive (ofe_morOF F1 F2).
Proof.
@@ -825,7 +825,7 @@ Qed.
Section sum.
Context {A B : ofeT}.
- Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
+ Local Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
Global Instance inl_ne : NonExpansive (@inl A B) := _.
Global Instance inr_ne : NonExpansive (@inr A B) := _.
Global Instance inl_ne_inj n : Inj (dist n) (dist n) (@inl A B) := _.
@@ -875,7 +875,7 @@ End sum.
Arguments sumO : clear implicits.
Typeclasses Opaque sum_dist.
-Instance sum_map_ne {A A' B B' : ofeT} n :
+Global Instance sum_map_ne {A A' B B' : ofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@sum_map A A' B B').
Proof.
@@ -883,7 +883,7 @@ Proof.
Qed.
Definition sumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
sumO A B -n> sumO A' B' := OfeMor (sum_map f g).
-Instance sumO_map_ne {A A' B B'} :
+Global Instance sumO_map_ne {A A' B B'} :
NonExpansive2 (@sumO_map A A' B B').
Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
@@ -902,7 +902,7 @@ Next Obligation.
Qed.
Notation "F1 + F2" := (sumOF F1%OF F2%OF) : oFunctor_scope.
-Instance sumOF_contractive F1 F2 :
+Global Instance sumOF_contractive F1 F2 :
oFunctorContractive F1 → oFunctorContractive F2 →
oFunctorContractive (sumOF F1 F2).
Proof.
@@ -914,7 +914,7 @@ Qed.
Section discrete_ofe.
Context `{Equiv A} (Heq : @Equivalence A (≡)).
- Instance discrete_dist : Dist A := λ n x y, x ≡ y.
+ Local Instance discrete_dist : Dist A := λ n x y, x ≡ y.
Definition discrete_ofe_mixin : OfeMixin A.
Proof using Type*.
split.
@@ -953,7 +953,7 @@ Notation discrete_ofe_equivalence_of A := ltac:(
| discrete_ofe_mixin ?H => exact H
end) (only parsing).
-Instance leibnizO_leibniz A : LeibnizEquiv (leibnizO A).
+Global Instance leibnizO_leibniz A : LeibnizEquiv (leibnizO A).
Proof. by intros x y. Qed.
(** * Basic Coq types *)
@@ -964,8 +964,8 @@ Canonical Structure NO := leibnizO N.
Canonical Structure ZO := leibnizO Z.
Section prop.
- Instance Prop_equiv : Equiv Prop := iff.
- Instance Prop_equivalence : Equivalence (≡@{Prop}) := _.
+ Local Instance Prop_equiv : Equiv Prop := iff.
+ Local Instance Prop_equivalence : Equivalence (≡@{Prop}) := _.
Canonical Structure PropO := discreteO Prop.
End prop.
@@ -973,7 +973,7 @@ End prop.
Section option.
Context {A : ofeT}.
- Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
+ Local Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
Proof. done. Qed.
@@ -1037,13 +1037,13 @@ End option.
Typeclasses Opaque option_dist.
Arguments optionO : clear implicits.
-Instance option_fmap_ne {A B : ofeT} n:
+Global Instance option_fmap_ne {A B : ofeT} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
Proof. intros f f' Hf ?? []; constructor; auto. Qed.
-Instance option_mbind_ne {A B : ofeT} n:
+Global Instance option_mbind_ne {A B : ofeT} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind option _ A B).
Proof. destruct 2; simpl; auto. Qed.
-Instance option_mjoin_ne {A : ofeT} n:
+Global Instance option_mjoin_ne {A : ofeT} n:
Proper (dist n ==> dist n) (@mjoin option _ A).
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
@@ -1056,7 +1056,7 @@ Qed.
Definition optionO_map {A B} (f : A -n> B) : optionO A -n> optionO B :=
OfeMor (fmap f : optionO A → optionO B).
-Instance optionO_map_ne A B : NonExpansive (@optionO_map A B).
+Global Instance optionO_map_ne A B : NonExpansive (@optionO_map A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
Program Definition optionOF (F : oFunctor) : oFunctor := {|
@@ -1075,7 +1075,7 @@ Next Obligation.
apply option_fmap_equiv_ext=>y; apply oFunctor_map_compose.
Qed.
-Instance optionOF_contractive F :
+Global Instance optionOF_contractive F :
oFunctorContractive F → oFunctorContractive (optionOF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
@@ -1091,12 +1091,12 @@ Record later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
Arguments later_car {_} _.
-Instance: Params (@Next) 1 := {}.
+Global Instance: Params (@Next) 1 := {}.
Section later.
Context {A : ofeT}.
- Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
- Instance later_dist : Dist (later A) := λ n x y,
+ Local Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
+ Local Instance later_dist : Dist (later A) := λ n x y,
dist_later n (later_car x) (later_car y).
Definition later_ofe_mixin : OfeMixin (later A).
Proof.
@@ -1129,7 +1129,7 @@ Section later.
Lemma Next_uninj x : ∃ a, x ≡ Next a.
Proof. by exists (later_car x). Qed.
- Instance later_car_anti_contractive n :
+ Local Instance later_car_anti_contractive n :
Proper (dist n ==> dist_later n) later_car.
Proof. move=> [x] [y] /= Hxy. done. Qed.
@@ -1148,11 +1148,11 @@ Arguments laterO : clear implicits.
Definition later_map {A B} (f : A → B) (x : later A) : later B :=
Next (f (later_car x)).
-Instance later_map_ne {A B : ofeT} (f : A → B) n :
+Global Instance later_map_ne {A B : ofeT} (f : A → B) n :
Proper (dist (pred n) ==> dist (pred n)) f →
Proper (dist n ==> dist n) (later_map f) | 0.
Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
-Instance later_map_proper {A B : ofeT} (f : A → B) :
+Global Instance later_map_proper {A B : ofeT} (f : A → B) :
Proper ((≡) ==> (≡)) f →
Proper ((≡) ==> (≡)) (later_map f).
Proof. solve_proper. Qed.
@@ -1166,7 +1166,7 @@ Lemma later_map_ext {A B : ofeT} (f g : A → B) x :
Proof. destruct x; intros Hf; apply Hf. Qed.
Definition laterO_map {A B} (f : A -n> B) : laterO A -n> laterO B :=
OfeMor (later_map f).
-Instance laterO_map_contractive (A B : ofeT) : Contractive (@laterO_map A B).
+Global Instance laterO_map_contractive (A B : ofeT) : Contractive (@laterO_map A B).
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
Program Definition laterOF (F : oFunctor) : oFunctor := {|
@@ -1187,7 +1187,7 @@ Next Obligation.
Qed.
Notation "â–¶ F" := (laterOF F%OF) (at level 20, right associativity) : oFunctor_scope.
-Instance laterOF_contractive F : oFunctorContractive (laterOF F).
+Global Instance laterOF_contractive F : oFunctorContractive (laterOF F).
Proof.
intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
destruct n as [|n]; simpl in *; first done. apply oFunctor_map_ne, Hfg.
@@ -1213,8 +1213,8 @@ Section discrete_fun.
Context {A : Type} {B : A → ofeT}.
Implicit Types f g : discrete_fun B.
- Instance discrete_fun_equiv : Equiv (discrete_fun B) := λ f g, ∀ x, f x ≡ g x.
- Instance discrete_fun_dist : Dist (discrete_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+ Local Instance discrete_fun_equiv : Equiv (discrete_fun B) := λ f g, ∀ x, f x ≡ g x.
+ Local Instance discrete_fun_dist : Dist (discrete_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
Definition discrete_fun_ofe_mixin : OfeMixin (discrete_fun B).
Proof.
split.
@@ -1268,14 +1268,14 @@ Lemma discrete_fun_map_compose {A} {B1 B2 B3 : A → ofeT}
discrete_fun_map (λ x, f2 x ∘ f1 x) g = discrete_fun_map f2 (discrete_fun_map f1 g).
Proof. done. Qed.
-Instance discrete_fun_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
+Global Instance discrete_fun_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
(∀ x, Proper (dist n ==> dist n) (f x)) →
Proper (dist n ==> dist n) (discrete_fun_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /discrete_fun_map (Hy x). Qed.
Definition discrete_funO_map {A} {B1 B2 : A → ofeT} (f : discrete_fun (λ x, B1 x -n> B2 x)) :
discrete_funO B1 -n> discrete_funO B2 := OfeMor (discrete_fun_map f).
-Instance discrete_funO_map_ne {A} {B1 B2 : A → ofeT} :
+Global Instance discrete_funO_map_ne {A} {B1 B2 : A → ofeT} :
NonExpansive (@discrete_funO_map A B1 B2).
Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
@@ -1299,7 +1299,7 @@ Qed.
Notation "T -d> F" := (@discrete_funOF T%type (λ _, F%OF)) : oFunctor_scope.
-Instance discrete_funOF_contractive {C} (F : C → oFunctor) :
+Global Instance discrete_funOF_contractive {C} (F : C → oFunctor) :
(∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
@@ -1356,8 +1356,8 @@ Section sigma.
(* TODO: Find a better place for this Equiv instance. It also
should not depend on A being an OFE. *)
- Instance sig_equiv : Equiv (sig P) := λ x1 x2, `x1 ≡ `x2.
- Instance sig_dist : Dist (sig P) := λ n x1 x2, `x1 ≡{n}≡ `x2.
+ Local Instance sig_equiv : Equiv (sig P) := λ x1 x2, `x1 ≡ `x2.
+ Local Instance sig_dist : Dist (sig P) := λ n x1 x2, `x1 ≡{n}≡ `x2.
Definition sig_equiv_alt x y : x ≡ y ↔ `x ≡ `y := reflexivity _.
Definition sig_dist_alt n x y : x ≡{n}≡ y ↔ `x ≡{n}≡ `y := reflexivity _.
@@ -1399,7 +1399,7 @@ Section sigT.
Unlike in the topos of trees, with (C)OFEs we cannot use step-indexed equality
on the first component.
*)
- Instance sigT_dist : Dist (sigT P) := λ n x1 x2,
+ Local Instance sigT_dist : Dist (sigT P) := λ n x1 x2,
∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡{n}≡ projT2 x2.
(**
@@ -1409,7 +1409,7 @@ Section sigT.
By defining [equiv] in terms of [dist], we can define an OFE
without assuming UIP, at the cost of complex reasoning on [equiv].
*)
- Instance sigT_equiv : Equiv (sigT P) := λ x1 x2,
+ Local Instance sigT_equiv : Equiv (sigT P) := λ x1 x2,
∀ n, x1 ≡{n}≡ x2.
(** Unfolding lemmas.
@@ -1599,10 +1599,10 @@ Arguments ofe_iso_21 {_ _} _ _.
Section ofe_iso.
Context {A B : ofeT}.
- Instance ofe_iso_equiv : Equiv (ofe_iso A B) := λ I1 I2,
+ Local Instance ofe_iso_equiv : Equiv (ofe_iso A B) := λ I1 I2,
ofe_iso_1 I1 ≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡ ofe_iso_2 I2.
- Instance ofe_iso_dist : Dist (ofe_iso A B) := λ n I1 I2,
+ Local Instance ofe_iso_dist : Dist (ofe_iso A B) := λ n I1 I2,
ofe_iso_1 I1 ≡{n}≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡{n}≡ ofe_iso_2 I2.
Global Instance ofe_iso_1_ne : NonExpansive (ofe_iso_1 (A:=A) (B:=B)).
@@ -1633,7 +1633,7 @@ Solve Obligations with done.
Definition iso_ofe_sym {A B : ofeT} (I : ofe_iso A B) : ofe_iso B A :=
OfeIso (ofe_iso_2 I) (ofe_iso_1 I) (ofe_iso_21 I) (ofe_iso_12 I).
-Instance iso_ofe_sym_ne {A B} : NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
+Global Instance iso_ofe_sym_ne {A B} : NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
Program Definition iso_ofe_trans {A B C}
@@ -1641,7 +1641,7 @@ Program Definition iso_ofe_trans {A B C}
OfeIso (ofe_iso_1 J â—Ž ofe_iso_1 I) (ofe_iso_2 I â—Ž ofe_iso_2 J) _ _.
Next Obligation. intros A B C I J z; simpl. by rewrite !ofe_iso_12. Qed.
Next Obligation. intros A B C I J z; simpl. by rewrite !ofe_iso_21. Qed.
-Instance iso_ofe_trans_ne {A B C} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (C:=C)).
+Global Instance iso_ofe_trans_ne {A B C} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (C:=C)).
Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.
Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
@@ -1658,9 +1658,9 @@ Next Obligation.
apply equiv_dist=> n.
apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
Qed.
-Instance iso_ofe_cong_ne (F : oFunctor) `{!Cofe A, !Cofe B} :
+Global Instance iso_ofe_cong_ne (F : oFunctor) `{!Cofe A, !Cofe B} :
NonExpansive (iso_ofe_cong F (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
-Instance iso_ofe_cong_contractive (F : oFunctor) `{!Cofe A, !Cofe B} :
+Global Instance iso_ofe_cong_contractive (F : oFunctor) `{!Cofe A, !Cofe B} :
oFunctorContractive F → Contractive (iso_ofe_cong F (A:=A) (B:=B)).
Proof. intros ? n I1 I2 HI; split; simpl; f_contractive; by destruct HI. Qed.
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index a04eb8692..26fedca2d 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -19,7 +19,7 @@ Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
Arguments is_op {_} _ _ _ {_}.
Global Hint Mode IsOp + - - - : typeclass_instances.
-Instance is_op_op {A : cmraT} (a b : A) : IsOp (a â‹… b) a b | 100.
+Global Instance is_op_op {A : cmraT} (a b : A) : IsOp (a â‹… b) a b | 100.
Proof. by rewrite /IsOp. Qed.
Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
@@ -29,7 +29,7 @@ Global Hint Mode IsOp' + - ! ! : typeclass_instances.
Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
Existing Instance is_op_lr | 0.
Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
-Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
+Global Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
(* FromOp *)
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index c35d4c75d..440147127 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -62,14 +62,14 @@ Local Hint Extern 50 (_ ⊆ _) => set_solver : sts.
Local Hint Extern 50 (_ ## _) => set_solver : sts.
(** ** Setoids *)
-Instance frame_step_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
+Local Instance frame_step_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
Proof.
intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
eauto with sts; set_solver.
Qed.
Global Instance frame_step_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /set_equiv_spec [??]; split; by apply frame_step_mono. Qed.
-Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
+Local Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
@@ -197,12 +197,12 @@ Inductive sts_equiv : Equiv (car sts) :=
| auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
| frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
Existing Instance sts_equiv.
-Instance sts_valid : Valid (car sts) := λ x,
+Local Instance sts_valid : Valid (car sts) := λ x,
match x with
| auth s T => tok s ## T
| frag S' T => closed S' T ∧ ∃ s, s ∈ S'
end.
-Instance sts_core : PCore (car sts) := λ x,
+Local Instance sts_core : PCore (car sts) := λ x,
Some match x with
| frag S' _ => frag (up_set S' ∅ ) ∅
| auth s _ => frag (up s ∅) ∅
@@ -213,7 +213,7 @@ Inductive sts_disjoint : Disjoint (car sts) :=
| auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → auth s T1 ## frag S T2
| frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → frag S T1 ## auth s T2.
Existing Instance sts_disjoint.
-Instance sts_op : Op (car sts) := λ x1 x2,
+Local Instance sts_op : Op (car sts) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
| auth s T1, frag _ T2 => auth s (T1 ∪ T2)
@@ -232,7 +232,7 @@ Proof. by constructor. Qed.
Global Instance frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@frag sts).
Proof. by constructor. Qed.
-Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
+Local Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
Proof.
split.
- by intros []; constructor.
@@ -290,9 +290,9 @@ Section sts_definitions.
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
sts_frag (sts.up s T) T.
End sts_definitions.
-Instance: Params (@sts_auth) 2 := {}.
-Instance: Params (@sts_frag) 1 := {}.
-Instance: Params (@sts_frag_up) 2 := {}.
+Global Instance: Params (@sts_auth) 2 := {}.
+Global Instance: Params (@sts_frag) 1 := {}.
+Global Instance: Params (@sts_frag_up) 2 := {}.
Section stsRA.
Import sts.
diff --git a/iris/algebra/ufrac.v b/iris/algebra/ufrac.v
index 12cb72449..821fc4ceb 100644
--- a/iris/algebra/ufrac.v
+++ b/iris/algebra/ufrac.v
@@ -14,9 +14,9 @@ Section ufrac.
Canonical Structure ufracO := leibnizO ufrac.
- Instance ufrac_valid : Valid ufrac := λ x, True.
- Instance ufrac_pcore : PCore ufrac := λ _, None.
- Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
+ Local Instance ufrac_valid : Valid ufrac := λ x, True.
+ Local Instance ufrac_pcore : PCore ufrac := λ _, None.
+ Local Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
Lemma ufrac_op' p q : p â‹… q = (p + q)%Qp.
Proof. done. Qed.
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 1a671def3..951451c34 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -8,13 +8,13 @@ From iris.prelude Require Import options.
*)
Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
-Instance: Params (@cmra_updateP) 1 := {}.
+Global Instance: Params (@cmra_updateP) 1 := {}.
Infix "~~>:" := cmra_updateP (at level 70).
Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
Infix "~~>" := cmra_update (at level 70).
-Instance: Params (@cmra_update) 1 := {}.
+Global Instance: Params (@cmra_update) 1 := {}.
Section updates.
Context {A : cmraT}.
diff --git a/iris/algebra/vector.v b/iris/algebra/vector.v
index dd2a27c39..0584ed587 100644
--- a/iris/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -6,8 +6,8 @@ From iris.prelude Require Import options.
Section ofe.
Context {A : ofeT}.
- Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A).
- Instance vec_dist m : Dist (vec A m) := dist (A:=list A).
+ Local Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A).
+ Local Instance vec_dist m : Dist (vec A m) := dist (A:=list A).
Definition vec_ofe_mixin m : OfeMixin (vec A m).
Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
@@ -76,7 +76,7 @@ Proof.
intros Hf. eapply (list_fmap_ext_ne f g v) in Hf.
by rewrite -!vec_to_list_map in Hf.
Qed.
-Instance vec_map_ne {A B : ofeT} m f n :
+Global Instance vec_map_ne {A B : ofeT} m f n :
Proper (dist n ==> dist n) f →
Proper (dist n ==> dist n) (@vec_map A B m f).
Proof.
@@ -85,7 +85,7 @@ Proof.
Qed.
Definition vecO_map {A B : ofeT} m (f : A -n> B) : vecO A m -n> vecO B m :=
OfeMor (vec_map m f).
-Instance vecO_map_ne {A A'} m :
+Global Instance vecO_map_ne {A A'} m :
NonExpansive (@vecO_map A A' m).
Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
@@ -108,7 +108,7 @@ Next Obligation.
rewrite !vec_to_list_map. by apply: (oFunctor_map_compose (listOF F) f g f' g').
Qed.
-Instance vecOF_contractive F m :
+Global Instance vecOF_contractive F m :
oFunctorContractive F → oFunctorContractive (vecOF F m).
Proof.
by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_map_contractive.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 3a02bf95a..1c5fb7d2f 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -55,15 +55,15 @@ Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel {
}.
Arguments ViewRel {_ _} _ _.
Arguments view_rel_holds {_ _} _ _ _ _.
-Instance: Params (@view_rel_holds) 4 := {}.
+Global Instance: Params (@view_rel_holds) 4 := {}.
-Instance view_rel_ne {A B} (rel : view_rel A B) n :
+Global Instance view_rel_ne {A B} (rel : view_rel A B) n :
Proper (dist n ==> dist n ==> iff) (rel n).
Proof.
intros a1 a2 Ha b1 b2 Hb.
split=> ?; (eapply view_rel_mono; [done|done|by rewrite Hb|done]).
Qed.
-Instance view_rel_proper {A B} (rel : view_rel A B) n :
+Global Instance view_rel_proper {A B} (rel : view_rel A B) n :
Proper ((≡) ==> (≡) ==> iff) (rel n).
Proof. intros a1 a2 Ha b1 b2 Hb. apply view_rel_ne; by apply equiv_dist. Qed.
@@ -80,17 +80,17 @@ Add Printing Constructor view.
Arguments View {_ _ _} _ _.
Arguments view_auth_proj {_ _ _} _.
Arguments view_frag_proj {_ _ _} _.
-Instance: Params (@View) 3 := {}.
-Instance: Params (@view_auth_proj) 3 := {}.
-Instance: Params (@view_frag_proj) 3 := {}.
+Global Instance: Params (@View) 3 := {}.
+Global Instance: Params (@view_auth_proj) 3 := {}.
+Global Instance: Params (@view_frag_proj) 3 := {}.
Definition view_auth {A B} {rel : view_rel A B} (q : Qp) (a : A) : view rel :=
View (Some (q, to_agree a)) ε.
Definition view_frag {A B} {rel : view_rel A B} (b : B) : view rel := View None b.
Typeclasses Opaque view_auth view_frag.
-Instance: Params (@view_auth) 3 := {}.
-Instance: Params (@view_frag) 3 := {}.
+Global Instance: Params (@view_auth) 3 := {}.
+Global Instance: Params (@view_frag) 3 := {}.
Notation "â—V{ q } a" := (view_auth q a) (at level 20, format "â—V{ q } a").
Notation "â—V a" := (view_auth 1 a) (at level 20).
@@ -107,9 +107,9 @@ Section ofe.
Implicit Types b : B.
Implicit Types x y : view rel.
- Instance view_equiv : Equiv (view rel) := λ x y,
+ Local Instance view_equiv : Equiv (view rel) := λ x y,
view_auth_proj x ≡ view_auth_proj y ∧ view_frag_proj x ≡ view_frag_proj y.
- Instance view_dist : Dist (view rel) := λ n x y,
+ Local Instance view_dist : Dist (view rel) := λ n x y,
view_auth_proj x ≡{n}≡ view_auth_proj y ∧
view_frag_proj x ≡{n}≡ view_frag_proj y.
@@ -173,21 +173,21 @@ Section cmra.
Global Instance view_frag_inj : Inj (≡) (≡) (@view_frag A B rel).
Proof. by intros ?? [??]. Qed.
- Instance view_valid : Valid (view rel) := λ x,
+ Local Instance view_valid : Valid (view rel) := λ x,
match view_auth_proj x with
| Some (q, ag) =>
✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
| None => ∀ n, ∃ a, rel n a (view_frag_proj x)
end.
- Instance view_validN : ValidN (view rel) := λ n x,
+ Local Instance view_validN : ValidN (view rel) := λ n x,
match view_auth_proj x with
| Some (q, ag) =>
✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
| None => ∃ a, rel n a (view_frag_proj x)
end.
- Instance view_pcore : PCore (view rel) := λ x,
+ Local Instance view_pcore : PCore (view rel) := λ x,
Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).
- Instance view_op : Op (view rel) := λ x y,
+ Local Instance view_op : Op (view rel) := λ x y,
View (view_auth_proj x â‹… view_auth_proj y) (view_frag_proj x â‹… view_frag_proj y).
Local Definition view_valid_eq :
@@ -253,7 +253,7 @@ Section cmra.
- naive_solver.
Qed.
- Instance view_empty : Unit (view rel) := View ε ε.
+ Local Instance view_empty : Unit (view rel) := View ε ε.
Lemma view_ucmra_mixin : UcmraMixin (view rel).
Proof.
split; simpl.
@@ -556,7 +556,7 @@ Proof.
intros. constructor; simpl; [|by auto].
apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Qed.
-Instance view_map_ne {A A' B B' : ofeT}
+Global Instance view_map_ne {A A' B B' : ofeT}
{rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop}
(f : A → A') (g : B → B') `{Hf : !NonExpansive f, Hg : !NonExpansive g} :
NonExpansive (view_map (rel':=rel') (rel:=rel) f g).
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 806f169d1..7cf03eccb 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -89,10 +89,10 @@ Canonical Structure uPredI (M : ucmraT) : bi :=
bi_bi_mixin := uPred_bi_mixin M;
bi_bi_later_mixin := uPred_bi_later_mixin M |}.
-Instance uPred_pure_forall M : BiPureForall (uPredI M).
+Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
Proof. exact: @pure_forall_2. Qed.
-Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
+Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
Proof. apply later_contractive. Qed.
Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
diff --git a/iris/base_logic/lib/auth.v b/iris/base_logic/lib/auth.v
index 5733f9aa4..6bed8f337 100644
--- a/iris/base_logic/lib/auth.v
+++ b/iris/base_logic/lib/auth.v
@@ -12,7 +12,7 @@ Class authG Σ (A : ucmraT) := AuthG {
}.
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
-Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
+Global Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
Proof. solve_inG. Qed.
Section definitions.
@@ -55,9 +55,9 @@ Section definitions.
End definitions.
Typeclasses Opaque auth_own auth_inv auth_ctx.
-Instance: Params (@auth_own) 4 := {}.
-Instance: Params (@auth_inv) 5 := {}.
-Instance: Params (@auth_ctx) 7 := {}.
+Global Instance: Params (@auth_own) 4 := {}.
+Global Instance: Params (@auth_inv) 5 := {}.
+Global Instance: Params (@auth_ctx) 7 := {}.
Section auth.
Context `{!invG Σ, !authG Σ A}.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 8f0620e03..56fb406b6 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -13,7 +13,7 @@ Class boxG Σ :=
Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
optionRF (agreeRF (▶ ∙)) ) ].
-Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
+Global Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
Proof. solve_inG. Qed.
Section box_defs.
@@ -40,10 +40,10 @@ Section box_defs.
inv N (slice_inv γ (Φ γ)).
End box_defs.
-Instance: Params (@box_own_prop) 3 := {}.
-Instance: Params (@slice_inv) 3 := {}.
-Instance: Params (@slice) 5 := {}.
-Instance: Params (@box) 5 := {}.
+Global Instance: Params (@box_own_prop) 3 := {}.
+Global Instance: Params (@slice_inv) 3 := {}.
+Global Instance: Params (@slice) 5 := {}.
+Global Instance: Params (@box) 5 := {}.
Section box.
Context `{!invG Σ, !boxG Σ} (N : namespace).
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 5ad576c95..c74b89b63 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -8,7 +8,7 @@ Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
-Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
+Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
Proof. solve_inG. Qed.
Section defs.
@@ -20,7 +20,7 @@ Section defs.
inv N (P ∨ cinv_own γ 1).
End defs.
-Instance: Params (@cinv) 5 := {}.
+Global Instance: Params (@cinv) 5 := {}.
Section proofs.
Context `{!invG Σ, !cinvG Σ}.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 7bdce06e5..533753fe8 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -33,13 +33,13 @@ Proof.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
-Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
+Global Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
-Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
+Global Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
-Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
+Global Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
Proof.
split.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 41c7652b2..e79954711 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -87,7 +87,7 @@ Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
GFunctor (namespace_mapR (agreeR positiveO))
].
-Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
+Global Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index ff8b540fd..d340387fc 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -44,7 +44,7 @@ Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
#[ GFunctor (authR (inv_heap_mapUR L V)) ].
-Instance subG_inv_heapPreG (L V : Type) `{Countable L} {Σ} :
+Global Instance subG_inv_heapPreG (L V : Type) `{Countable L} {Σ} :
subG (inv_heapΣ L V) Σ → inv_heapPreG L V Σ.
Proof. solve_inG. Qed.
@@ -77,8 +77,8 @@ Local Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
make them explicit. *)
Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
-Instance: Params (@inv_mapsto_own) 8 := {}.
-Instance: Params (@inv_mapsto) 7 := {}.
+Global Instance: Params (@inv_mapsto_own) 8 := {}.
+Global Instance: Params (@inv_mapsto) 7 := {}.
Section to_inv_heap.
Context {L V : Type} `{Countable L}.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index db43d867a..0142e9c1c 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -15,7 +15,7 @@ Global Hint Mode ghost_varG - ! : typeclass_instances.
Definition ghost_varΣ (A : Type) : gFunctors :=
#[ GFunctor (frac_agreeR $ leibnizO A) ].
-Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
+Global Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
Proof. solve_inG. Qed.
Definition ghost_var_def `{!ghost_varG Σ A} (γ : gname) (q : Qp) (a : A) : iProp Σ :=
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index e7cc9b638..73f0cc7e1 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -13,7 +13,7 @@ Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv := inv_aux.(unseal).
Arguments inv {Σ _} N P.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
-Instance: Params (@inv) 3 := {}.
+Global Instance: Params (@inv) 3 := {}.
(** * Invariants *)
Section inv.
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index d91c4229d..038a552ed 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -97,14 +97,14 @@ Proof.
- move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto.
Qed.
-Instance subG_refl Σ : subG Σ Σ.
+Global Instance subG_refl Σ : subG Σ Σ.
Proof. move=> i; by exists i. Qed.
-Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
+Global Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
Qed.
-Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
+Global Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 620da1cc5..5c28871bd 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -16,7 +16,7 @@ From iris.prelude Require Import options.
Class mono_natG Σ :=
MonoNatG { mono_natG_inG :> inG Σ mono_natR; }.
Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
-Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
+Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
Proof. solve_inG. Qed.
Definition mono_nat_auth_own_def `{!mono_natG Σ}
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index f4874e831..4c1faf91d 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -12,7 +12,7 @@ Class na_invG Σ :=
na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
Definition na_invΣ : gFunctors :=
#[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
-Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
+Global Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
Proof. solve_inG. Qed.
Section defs.
@@ -26,7 +26,7 @@ Section defs.
inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
End defs.
-Instance: Params (@na_inv) 3 := {}.
+Global Instance: Params (@na_inv) 3 := {}.
Typeclasses Opaque na_own na_inv.
Section proofs.
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 49bee658b..69d36e95a 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -66,7 +66,7 @@ Local Definition inG_fold {Σ A} {i : inG Σ A} :
Local Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
discrete_fun_singleton (inG_id i)
{[ γ := inG_unfold (cmra_transport inG_prf a) ]}.
-Instance: Params (@iRes_singleton) 4 := {}.
+Global Instance: Params (@iRes_singleton) 4 := {}.
Local Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index d12feb530..d1a4b9bae 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -20,7 +20,7 @@ Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
#[GFunctor (gmap_viewR P (listO $ leibnizO V))].
-Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
+Global Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 1038d4d71..0c7559332 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -15,7 +15,7 @@ Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
#[ GFunctor (agreeRF F) ].
-Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
+Global Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
Proof. solve_inG. Qed.
@@ -23,7 +23,7 @@ Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
own γ (to_agree x).
Typeclasses Opaque saved_anything_own.
-Instance: Params (@saved_anything_own) 4 := {}.
+Global Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
Context `{!savedAnythingG Σ F}.
@@ -69,7 +69,7 @@ Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
Definition saved_prop_own `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
saved_anything_own (F := ▶ ∙) γ (Next P).
-Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
+Global Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
Contractive (saved_prop_own γ).
Proof. solve_contractive. Qed.
@@ -100,7 +100,7 @@ Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ ∙)).
Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
saved_anything_own (F := A -d> ▶ ∙) γ (OfeMor Next ∘ Φ).
-Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
+Global Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).
Proof.
solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
diff --git a/iris/base_logic/lib/sts.v b/iris/base_logic/lib/sts.v
index d4e4f8680..0ed4b1390 100644
--- a/iris/base_logic/lib/sts.v
+++ b/iris/base_logic/lib/sts.v
@@ -11,7 +11,7 @@ Class stsG Σ (sts : stsT) := StsG {
}.
Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
-Instance subG_stsΣ Σ sts :
+Global Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
Proof. solve_inG. Qed.
@@ -51,10 +51,10 @@ Section definitions.
Proof. apply _. Qed.
End definitions.
-Instance: Params (@sts_inv) 4 := {}.
-Instance: Params (@sts_ownS) 4 := {}.
-Instance: Params (@sts_own) 5 := {}.
-Instance: Params (@sts_ctx) 6 := {}.
+Global Instance: Params (@sts_inv) 4 := {}.
+Global Instance: Params (@sts_ownS) 4 := {}.
+Global Instance: Params (@sts_own) 5 := {}.
+Global Instance: Params (@sts_ctx) 6 := {}.
Section sts.
Context `{!invG Σ, !stsG Σ sts}.
diff --git a/iris/base_logic/lib/viewshifts.v b/iris/base_logic/lib/viewshifts.v
index 5aa7b55e2..e323b4d03 100644
--- a/iris/base_logic/lib/viewshifts.v
+++ b/iris/base_logic/lib/viewshifts.v
@@ -6,7 +6,7 @@ Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
□ (P -∗ |={E1,E2}=> Q).
Arguments vs {_ _} _ _ _%I _%I.
-Instance: Params (@vs) 4 := {}.
+Global Instance: Params (@vs) 4 := {}.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : bi_scope.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index d33c9105b..3c1d28ee6 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -28,7 +28,7 @@ Module invG.
disabled_inPreG :> inG Σ (gset_disjR positive);
}.
- Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
+ Global Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
Proof. solve_inG. Qed.
End invG.
Import invG.
@@ -39,18 +39,18 @@ Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
-Instance: Params (@invariant_unfold) 1 := {}.
-Instance: Params (@ownI) 3 := {}.
+Global Instance: Params (@invariant_unfold) 1 := {}.
+Global Instance: Params (@ownI) 3 := {}.
Definition ownE `{!invG Σ} (E : coPset) : iProp Σ :=
own enabled_name (CoPset E).
Typeclasses Opaque ownE.
-Instance: Params (@ownE) 3 := {}.
+Global Instance: Params (@ownE) 3 := {}.
Definition ownD `{!invG Σ} (E : gset positive) : iProp Σ :=
own disabled_name (GSet E).
Typeclasses Opaque ownD.
-Instance: Params (@ownD) 3 := {}.
+Global Instance: Params (@ownD) 3 := {}.
Definition wsat `{!invG Σ} : iProp Σ :=
locked (∃ I : gmap positive (iProp Σ),
@@ -62,7 +62,7 @@ Context `{!invG Σ}.
Implicit Types P : iProp Σ.
(* Invariants *)
-Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
+Local Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
Proof. solve_contractive. Qed.
Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
Proof. solve_contractive. Qed.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 8cfae37ef..9eab3d8f4 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -113,17 +113,17 @@ Record uPred (M : ucmraT) : Type := UPred {
Bind Scope bi_scope with uPred.
Arguments uPred_holds {_} _%I _ _ : simpl never.
Add Printing Constructor uPred.
-Instance: Params (@uPred_holds) 3 := {}.
+Global Instance: Params (@uPred_holds) 3 := {}.
Section cofe.
Context {M : ucmraT}.
Inductive uPred_equiv' (P Q : uPred M) : Prop :=
{ uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
- Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
+ Local Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
{ uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
- Instance uPred_dist : Dist (uPred M) := uPred_dist'.
+ Local Instance uPred_dist : Dist (uPred M) := uPred_dist'.
Definition uPred_ofe_mixin : OfeMixin (uPred M).
Proof.
split.
@@ -156,11 +156,11 @@ Section cofe.
End cofe.
Arguments uPredO : clear implicits.
-Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
+Global Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
Qed.
-Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
+Global Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
@@ -192,7 +192,7 @@ Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
-Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
+Global Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
intros x1 x2 Hx; split=> n' y ??.
@@ -235,7 +235,7 @@ Next Obligation.
apply uPred_map_ext=>y; apply urFunctor_map_compose.
Qed.
-Instance uPredOF_contractive F :
+Global Instance uPredOF_contractive F :
urFunctorContractive F → oFunctorContractive (uPredOF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 09ac481d1..e34dd8e45 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -43,7 +43,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B}
| x1 :: l1, x2 :: l2 => Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2
| _, _ => False
end%I.
-Instance: Params (@big_sepL2) 3 := {}.
+Global Instance: Params (@big_sepL2) 3 := {}.
Arguments big_sepL2 {PROP A B} _ !_ !_ /.
Typeclasses Opaque big_sepL2.
Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
@@ -59,7 +59,7 @@ Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
Definition big_sepM2 := big_sepM2_aux.(unseal).
Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
-Instance: Params (@big_sepM2) 6 := {}.
+Global Instance: Params (@big_sepM2) 6 := {}.
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
(big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index abdfdf596..9a10af530 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -4,24 +4,24 @@ From iris.prelude Require Import options.
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_iff) 1 := {}.
+Global Instance: Params (@bi_iff) 1 := {}.
Infix "↔" := bi_iff : bi_scope.
Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
((P -∗ Q) ∧ (Q -∗ P))%I.
Arguments bi_wand_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_wand_iff) 1 := {}.
+Global Instance: Params (@bi_wand_iff) 1 := {}.
Infix "∗-∗" := bi_wand_iff : bi_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Global Hint Mode Persistent + ! : typeclass_instances.
-Instance: Params (@Persistent) 1 := {}.
+Global Instance: Params (@Persistent) 1 := {}.
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
Arguments bi_affinely {_} _%I : simpl never.
-Instance: Params (@bi_affinely) 1 := {}.
+Global Instance: Params (@bi_affinely) 1 := {}.
Typeclasses Opaque bi_affinely.
Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
@@ -40,7 +40,7 @@ Global Hint Mode BiPositive ! : typeclass_instances.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
-Instance: Params (@bi_absorbingly) 1 := {}.
+Global Instance: Params (@bi_absorbingly) 1 := {}.
Typeclasses Opaque bi_absorbingly.
Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
@@ -52,35 +52,35 @@ Global Hint Mode Absorbing + ! : typeclass_instances.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <pers> P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
-Instance: Params (@bi_persistently_if) 2 := {}.
+Global Instance: Params (@bi_persistently_if) 2 := {}.
Typeclasses Opaque bi_persistently_if.
Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <affine> P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
-Instance: Params (@bi_affinely_if) 2 := {}.
+Global Instance: Params (@bi_affinely_if) 2 := {}.
Typeclasses Opaque bi_affinely_if.
Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <absorb> P else P)%I.
Arguments bi_absorbingly_if {_} !_ _%I /.
-Instance: Params (@bi_absorbingly_if) 2 := {}.
+Global Instance: Params (@bi_absorbingly_if) 2 := {}.
Typeclasses Opaque bi_absorbingly_if.
Notation "'<absorb>?' p P" := (bi_absorbingly_if p P) : bi_scope.
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
(<affine> <pers> P)%I.
Arguments bi_intuitionistically {_} _%I : simpl never.
-Instance: Params (@bi_intuitionistically) 1 := {}.
+Global Instance: Params (@bi_intuitionistically) 1 := {}.
Typeclasses Opaque bi_intuitionistically.
Notation "â–¡ P" := (bi_intuitionistically P) : bi_scope.
Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then â–¡ P else P)%I.
Arguments bi_intuitionistically_if {_} !_ _%I /.
-Instance: Params (@bi_intuitionistically_if) 2 := {}.
+Global Instance: Params (@bi_intuitionistically_if) 2 := {}.
Typeclasses Opaque bi_intuitionistically_if.
Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
@@ -91,20 +91,20 @@ Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
end%I
where "â–·^ n P" := (bi_laterN n P) : bi_scope.
Arguments bi_laterN {_} !_%nat_scope _%I.
-Instance: Params (@bi_laterN) 2 := {}.
+Global Instance: Params (@bi_laterN) 2 := {}.
Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope.
Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I.
Arguments bi_except_0 {_} _%I : simpl never.
Notation "â—‡ P" := (bi_except_0 P) : bi_scope.
-Instance: Params (@bi_except_0) 1 := {}.
+Global Instance: Params (@bi_except_0) 1 := {}.
Typeclasses Opaque bi_except_0.
Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Global Hint Mode Timeless + ! : typeclass_instances.
-Instance: Params (@Timeless) 1 := {}.
+Global Instance: Params (@Timeless) 1 := {}.
(** An optional precondition [mP] to [Q].
TODO: We may actually consider generalizing this to a list of preconditions,
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index c6532c198..8bcfde62e 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type*".
Class Embed (A B : Type) := embed : A → B.
Arguments embed {_ _ _} _%I : simpl never.
Notation "⎡ P ⎤" := (embed P) : bi_scope.
-Instance: Params (@embed) 3 := {}.
+Global Instance: Params (@embed) 3 := {}.
Typeclasses Opaque embed.
Global Hint Mode Embed ! - : typeclass_instances.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index ca25529a2..3539069a1 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -188,18 +188,18 @@ Canonical Structure bi_ofeO.
Global Instance bi_cofe' (PROP : bi) : Cofe PROP.
Proof. apply bi_cofe. Qed.
-Instance: Params (@bi_entails) 1 := {}.
-Instance: Params (@bi_emp) 1 := {}.
-Instance: Params (@bi_pure) 1 := {}.
-Instance: Params (@bi_and) 1 := {}.
-Instance: Params (@bi_or) 1 := {}.
-Instance: Params (@bi_impl) 1 := {}.
-Instance: Params (@bi_forall) 2 := {}.
-Instance: Params (@bi_exist) 2 := {}.
-Instance: Params (@bi_sep) 1 := {}.
-Instance: Params (@bi_wand) 1 := {}.
-Instance: Params (@bi_persistently) 1 := {}.
-Instance: Params (@bi_later) 1 := {}.
+Global Instance: Params (@bi_entails) 1 := {}.
+Global Instance: Params (@bi_emp) 1 := {}.
+Global Instance: Params (@bi_pure) 1 := {}.
+Global Instance: Params (@bi_and) 1 := {}.
+Global Instance: Params (@bi_or) 1 := {}.
+Global Instance: Params (@bi_impl) 1 := {}.
+Global Instance: Params (@bi_forall) 2 := {}.
+Global Instance: Params (@bi_exist) 2 := {}.
+Global Instance: Params (@bi_sep) 1 := {}.
+Global Instance: Params (@bi_wand) 1 := {}.
+Global Instance: Params (@bi_persistently) 1 := {}.
+Global Instance: Params (@bi_later) 1 := {}.
Arguments bi_car : simpl never.
Arguments bi_dist : simpl never.
@@ -218,8 +218,8 @@ Arguments bi_persistently {PROP} _%I : simpl never, rename.
Arguments bi_later {PROP} _%I : simpl never, rename.
Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
-Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
+Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
+Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 837d60c16..6e78aed8b 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -10,7 +10,7 @@ Class InternalEq (PROP : bi) :=
internal_eq : ∀ {A : ofeT}, A → A → PROP.
Arguments internal_eq {_ _ _} _ _ : simpl never.
Global Hint Mode InternalEq ! : typeclass_instances.
-Instance: Params (@internal_eq) 3 := {}.
+Global Instance: Params (@internal_eq) 3 := {}.
Infix "≡" := internal_eq : bi_scope.
Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 3d2380430..fd13d05c1 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -10,7 +10,7 @@ Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
(* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
using conjunction/implication here. *)
(∀ Q : PROP, <affine> ■(Q -∗ <pers> Q) -∗ <affine> ■(P -∗ Q) -∗ Q)%I.
-Instance: Params (@coreP) 1 := {}.
+Global Instance: Params (@coreP) 1 := {}.
Typeclasses Opaque coreP.
Section core.
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 23a96554f..592c2aff4 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -72,9 +72,9 @@ Module savedprop. Section savedprop.
(** We assume that we cannot update to false. *)
Hypothesis consistency : ¬(⊢ |==> False).
- Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
+ Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
Proof. intros P Q ?. by apply bupd_mono. Qed.
- Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
+ Global Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
by rewrite /ElimModal bi.intuitionistically_if_elim
bupd_frame_r bi.wand_elim_r bupd_trans.
@@ -165,9 +165,9 @@ Module inv. Section inv.
iIntros "(HP & HPw)". by iApply "HPw".
Qed.
- Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E).
+ Global Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E).
Proof. intros P Q ?. by apply fupd_mono. Qed.
- Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
+ Global Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
Proof.
intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
Qed.
@@ -303,9 +303,9 @@ Module linear. Section linear.
cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
(** Some general lemmas and proof mode compatibility. *)
- Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
+ Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
Proof. intros P Q ?. by apply fupd_mono. Qed.
- Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2).
+ Global Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2).
Proof.
intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
Qed.
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 0c84e2778..68eb9228f 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -114,13 +114,13 @@ Section fractional.
- In the forward direction, they make the search not terminate
- In the backward direction, the higher order unification of Φ
with the goal does not work. *)
- Instance mul_as_fractional_l P Φ p q :
+ Local Instance mul_as_fractional_l P Φ p q :
AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q.
Proof.
intros H. split; first apply H. eapply (mul_fractional_l _ Φ p).
split; first done. apply H.
Qed.
- Instance mul_as_fractional_r P Φ p q :
+ Local Instance mul_as_fractional_r P Φ p q :
AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q.
Proof.
intros H. split; first apply H. eapply (mul_fractional_r _ Φ p).
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 1d1d09ffe..acab442ba 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -12,7 +12,7 @@ Definition bi_rtc_pre `{!BiInternalEq PROP}
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
(<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
-Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
+Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
{A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
BiMonoPred (bi_rtc_pre R x).
Proof.
@@ -28,17 +28,17 @@ Definition bi_rtc `{!BiInternalEq PROP}
{A : ofeT} (R : A → A → PROP) (x1 x2 : A) : PROP :=
bi_least_fixpoint (bi_rtc_pre R x2) x1.
-Instance: Params (@bi_rtc) 3 := {}.
+Global Instance: Params (@bi_rtc) 3 := {}.
Typeclasses Opaque bi_rtc.
-Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP) :
+Global Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP) :
NonExpansive2 (bi_rtc R).
Proof.
intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
solve_proper.
Qed.
-Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP)
+Global Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP)
: Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 39f88ff74..b0ebb3f2e 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -37,10 +37,10 @@ Implicit Types P Q : monPred.
Section Ofe_Cofe_def.
Inductive monPred_equiv' P Q : Prop :=
{ monPred_in_equiv i : P i ≡ Q i } .
- Instance monPred_equiv : Equiv monPred := monPred_equiv'.
+ Local Instance monPred_equiv : Equiv monPred := monPred_equiv'.
Inductive monPred_dist' (n : nat) (P Q : monPred) : Prop :=
{ monPred_in_dist i : P i ≡{n}≡ Q i }.
- Instance monPred_dist : Dist monPred := monPred_dist'.
+ Local Instance monPred_dist : Dist monPred := monPred_dist'.
Definition monPred_sig P : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f } :=
exist _ (monPred_at P) (monPred_mono P).
@@ -324,7 +324,7 @@ Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
Arguments Objective {_ _} _%I.
Arguments objective_at {_ _} _%I {_}.
Global Hint Mode Objective + + ! : typeclass_instances.
-Instance: Params (@Objective) 2 := {}.
+Global Instance: Params (@Objective) 2 := {}.
(** Primitive facts that cannot be deduced from the BI structure. *)
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 9f2d8bc26..cd52e2ae3 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type*".
Class Plainly (A : Type) := plainly : A → A.
Arguments plainly {A}%type_scope {_} _%I.
Global Hint Mode Plainly ! : typeclass_instances.
-Instance: Params (@plainly) 2 := {}.
+Global Instance: Params (@plainly) 2 := {}.
Notation "â– P" := (plainly P) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *)
@@ -95,12 +95,12 @@ Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■P.
Arguments Plain {_ _} _%I : simpl never.
Arguments plain {_ _} _%I {_}.
Global Hint Mode Plain + - ! : typeclass_instances.
-Instance: Params (@Plain) 1 := {}.
+Global Instance: Params (@Plain) 1 := {}.
Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
(if p then â– P else P)%I.
Arguments plainly_if {_ _} !_ _%I /.
-Instance: Params (@plainly_if) 2 := {}.
+Global Instance: Params (@plainly_if) 2 := {}.
Typeclasses Opaque plainly_if.
Notation "â– ? p P" := (plainly_if p P) : bi_scope.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index f17fc27db..5d797983f 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type*".
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
-Instance : Params (@bupd) 2 := {}.
+Global Instance : Params (@bupd) 2 := {}.
Global Hint Mode BUpd ! : typeclass_instances.
Arguments bupd {_}%type_scope {_} _%bi_scope.
@@ -18,7 +18,7 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
-Instance: Params (@fupd) 4 := {}.
+Global Instance: Params (@fupd) 4 := {}.
Global Hint Mode FUpd ! : typeclass_instances.
Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index 75963fa02..5a8d42aec 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -10,8 +10,8 @@ Definition stuckness_leb (s1 s2 : stuckness) : bool :=
| MaybeStuck, NotStuck => false
| _, _ => true
end.
-Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
-Instance stuckness_le_po : PreOrder stuckness_le.
+Global Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
+Global Instance stuckness_le_po : PreOrder stuckness_le.
Proof. split; by repeat intros []. Qed.
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
@@ -31,12 +31,12 @@ to pick a default value depending on [A]. *)
Class Wp (Λ : language) (PROP A : Type) :=
wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
Arguments wp {_ _ _ _} _ _ _%E _%I.
-Instance: Params (@wp) 7 := {}.
+Global Instance: Params (@wp) 7 := {}.
Class Twp (Λ : language) (PROP A : Type) :=
twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
Arguments twp {_ _ _ _} _ _ _%E _%I.
-Instance: Params (@twp) 7 := {}.
+Global Instance: Params (@twp) 7 := {}.
(** Notations for partial weakest preconditions *)
(** Notations without binder -- only parsing because they overlap with the
diff --git a/iris/program_logic/hoare.v b/iris/program_logic/hoare.v
index 45f9702cd..42ec59626 100644
--- a/iris/program_logic/hoare.v
+++ b/iris/program_logic/hoare.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
(□ (P -∗ WP e @ s; E {{ Φ }}))%I.
-Instance: Params (@ht) 5 := {}.
+Global Instance: Params (@ht) 5 := {}.
Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 9649a8124..b15008931 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -58,7 +58,7 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
}.
-Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
+Global Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Proof. constructor; naive_solver. Qed.
Inductive atomicity := StronglyAtomic | WeaklyAtomic.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 4c2ca48c5..b39de3365 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -20,7 +20,7 @@ Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
ownP_name : gname;
}.
-Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
+Global Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
iris_invG := ownP_invG;
state_interp σ κs _ := own ownP_name (â—E σ)%I;
fork_post _ := True%I;
@@ -36,14 +36,14 @@ Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
}.
-Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
+Global Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
Proof. solve_inG. Qed.
(** Ownership *)
Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
own ownP_name (◯E σ).
Typeclasses Opaque ownP.
-Instance: Params (@ownP) 3 := {}.
+Global Instance: Params (@ownP) 3 := {}.
(* Adequacy *)
Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 19ffe2810..60cddc202 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -46,7 +46,7 @@ Proof.
iIntros "!>" (t') "H". by iApply "IH".
Qed.
-Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
+Local Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
Proof.
iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 0c9168eeb..20a98f6bb 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -70,12 +70,12 @@ Inductive ident :=
| INamed :> string → ident.
End ident.
-Instance maybe_IAnon : Maybe IAnon := λ i,
+Global Instance maybe_IAnon : Maybe IAnon := λ i,
match i with IAnon n => Some n | _ => None end.
-Instance maybe_INamed : Maybe INamed := λ i,
+Global Instance maybe_INamed : Maybe INamed := λ i,
match i with INamed s => Some s | _ => None end.
-Instance beq_eq_dec : EqDecision ident.
+Global Instance beq_eq_dec : EqDecision ident.
Proof. solve_decision. Defined.
Definition positive_beq := Eval compute in Pos.eqb.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 3848fce3f..a532207d2 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -271,9 +271,9 @@ Class IsApp {A} (l k1 k2 : list A) := is_app : l = k1 ++ k2.
Global Hint Mode IsCons + ! - - : typeclass_instances.
Global Hint Mode IsApp + ! - - : typeclass_instances.
-Instance is_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
+Global Instance is_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
Proof. done. Qed.
-Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
+Global Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
@@ -290,14 +290,14 @@ Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Global Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
-Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
+Global Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
Frame p R P Q → MaybeFrame p R P Q true.
Proof. done. Qed.
-Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
+Global Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
MaybeFrame true R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
-Instance maybe_frame_default {PROP : bi} (R P : PROP) :
+Global Instance maybe_frame_default {PROP : bi} (R P : PROP) :
TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
@@ -459,13 +459,13 @@ Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.
-Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
+Global Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
MaybeIntoLaterN only_head n P P | 1000.
Proof. apply laterN_intro. Qed.
(* In the case both parameters are evars and n=0, we have to stop the
search and unify both evars immediately instead of looping using
other instances. *)
-Instance maybe_into_laterN_default_0 {PROP : bi} only_head (P : PROP) :
+Global Instance maybe_into_laterN_default_0 {PROP : bi} only_head (P : PROP) :
MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.
@@ -597,40 +597,40 @@ with the exception of:
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iIntuitionistic]
*)
-Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
+Global Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
IntoPure P φ → IntoPure (tc_opaque P) φ := id.
-Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
+Global Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
FromPure a P φ → FromPure a (tc_opaque P) φ := id.
-Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+Global Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
-Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
+Global Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
IntoWand p q R P Q → IntoWand p q (tc_opaque R) P Q := id.
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
-Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+Global Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
-Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
+Global Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2 := id.
-Instance into_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+Global Instance into_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
IntoSep P Q1 Q2 → IntoSep (tc_opaque P) Q1 Q2 := id.
-Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+Global Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2 := id.
-Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+Global Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
IntoOr P Q1 Q2 → IntoOr (tc_opaque P) Q1 Q2 := id.
-Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
+Global Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
FromExist P Φ → FromExist (tc_opaque P) Φ := id.
-Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
+Global Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
IntoExist P Φ name → IntoExist (tc_opaque P) Φ name := id.
-Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
+Global Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
FromForall P Φ name → FromForall (tc_opaque P) Φ name := id.
-Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
+Global Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
-Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
+Global Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
M (sel : A) (P : PROP2) (Q : PROP1) :
FromModal M sel P Q → FromModal M sel (tc_opaque P) Q := id.
-Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
+Global Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
-Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
+Global Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
IntoInv P N → IntoInv (tc_opaque P) N := id.
-Instance elim_inv_tc_opaque {PROP : bi} {X} φ Pinv Pin Pout Pclose Q Q' :
+Global Instance elim_inv_tc_opaque {PROP : bi} {X} φ Pinv Pin Pout Pclose Q Q' :
ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q' →
ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 5aee11b50..2a8f370a4 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -69,7 +69,7 @@ Proof. by constructor. Qed.
Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
Proof. induction Γ; apply _. Qed.
-Instance affine_env_spatial Δ :
+Local Instance affine_env_spatial Δ :
AffineEnv (env_spatial Δ) → Affine ([∗] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 02f3e6c48..be3fdbe4f 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -9,8 +9,8 @@ Inductive env (A : Type) : Type :=
| Esnoc : env A → ident → A → env A.
Arguments Enil {_}.
Arguments Esnoc {_} _ _ _.
-Instance: Params (@Enil) 1 := {}.
-Instance: Params (@Esnoc) 1 := {}.
+Global Instance: Params (@Enil) 1 := {}.
+Global Instance: Params (@Esnoc) 1 := {}.
Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
match Γ with
@@ -35,7 +35,7 @@ Inductive env_wf {A} : env A → Prop :=
Fixpoint env_to_list {A} (E : env A) : list A :=
match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
Coercion env_to_list : env >-> list.
-Instance: Params (@env_to_list) 1 := {}.
+Global Instance: Params (@env_to_list) 1 := {}.
Fixpoint env_dom {A} (Γ : env A) : list ident :=
match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
@@ -250,10 +250,10 @@ Definition envs_wf {PROP : bi} (Δ : envs PROP) :=
Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP :=
(⌜envs_wf' Γp Γs⌠∧ □ [∧] Γp ∗ [∗] Γs)%I.
-Instance: Params (@of_envs') 1 := {}.
+Global Instance: Params (@of_envs') 1 := {}.
Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
of_envs' (env_intuitionistic Δ) (env_spatial Δ).
-Instance: Params (@of_envs) 1 := {}.
+Global Instance: Params (@of_envs) 1 := {}.
Arguments of_envs : simpl never.
Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
@@ -269,7 +269,7 @@ Definition envs_entails_eq :
@envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
Arguments envs_entails {PROP} Δ Q%I.
-Instance: Params (@envs_entails) 1 := {}.
+Global Instance: Params (@envs_entails) 1 := {}.
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 0cf886d51..ce13a62d0 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -14,7 +14,7 @@ Global Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i ⊑ j.
Global Hint Mode IsBiIndexRel + - - : typeclass_instances.
-Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
+Global Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
Proof. by rewrite /IsBiIndexRel. Qed.
Global Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
: typeclass_instances.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 375630f1d..cc94b000c 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -121,10 +121,10 @@ Canonical Structure siPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of siProp;
bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
-Instance siProp_pure_forall : BiPureForall siPropI.
+Global Instance siProp_pure_forall : BiPureForall siPropI.
Proof. exact: @pure_forall_2. Qed.
-Instance siProp_later_contractive : BiLaterContractive siPropI.
+Global Instance siProp_later_contractive : BiLaterContractive siPropI.
Proof. apply later_contractive. Qed.
Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index f47bbc7d0..ef804c4f8 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -19,10 +19,10 @@ Bind Scope siProp_scope with siProp.
Section cofe.
Inductive siProp_equiv' (P Q : siProp) : Prop :=
{ siProp_in_equiv : ∀ n, P n ↔ Q n }.
- Instance siProp_equiv : Equiv siProp := siProp_equiv'.
+ Local Instance siProp_equiv : Equiv siProp := siProp_equiv'.
Inductive siProp_dist' (n : nat) (P Q : siProp) : Prop :=
{ siProp_in_dist : ∀ n', n' ≤ n → P n' ↔ Q n' }.
- Instance siProp_dist : Dist siProp := siProp_dist'.
+ Local Instance siProp_dist : Dist siProp := siProp_dist'.
Definition siProp_ofe_mixin : OfeMixin siProp.
Proof.
split.
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index a1d218d3d..9dfd10fed 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -13,7 +13,7 @@ Class heapPreG Σ := HeapPreG {
Definition heapΣ : gFunctors :=
#[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val); proph_mapΣ proph_id (val * val)].
-Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
+Global Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
diff --git a/iris_heap_lang/class_instances.v b/iris_heap_lang/class_instances.v
index 6887a0acb..3d5682b82 100644
--- a/iris_heap_lang/class_instances.v
+++ b/iris_heap_lang/class_instances.v
@@ -3,9 +3,9 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics notation.
From iris.prelude Require Import options.
-Instance into_val_val v : IntoVal (Val v) v.
+Global Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
-Instance as_val_val v : AsVal (Val v).
+Global Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.
(** * Instances of the [Atomic] class *)
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 1b154fa31..8b03ae742 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -181,9 +181,9 @@ Definition val_is_unboxed (v : val) : Prop :=
| _ => False
end.
-Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
+Global Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
Proof. destruct l; simpl; exact (decide _). Defined.
-Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
+Global Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.
(** We just compare the word-sized representation of two values, without looking
@@ -207,16 +207,16 @@ Proof. by destruct v. Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof. destruct e=>//=. by intros [= <-]. Qed.
-Instance of_val_inj : Inj (=) (=) of_val.
+Global Instance of_val_inj : Inj (=) (=) of_val.
Proof. intros ??. congruence. Qed.
-Instance base_lit_eq_dec : EqDecision base_lit.
+Global Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
-Instance un_op_eq_dec : EqDecision un_op.
+Global Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
-Instance bin_op_eq_dec : EqDecision bin_op.
+Global Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
-Instance expr_eq_dec : EqDecision expr.
+Global Instance expr_eq_dec : EqDecision expr.
Proof.
refine (
fix go (e1 e2 : expr) {struct e1} : Decision (e1 = e2) :=
@@ -269,10 +269,10 @@ Proof.
end
for go); try (clear go gov; abstract intuition congruence).
Defined.
-Instance val_eq_dec : EqDecision val.
+Global Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.
-Instance base_lit_countable : Countable base_lit.
+Global Instance base_lit_countable : Countable base_lit.
Proof.
refine (inj_countable' (λ l, match l with
| LitInt n => (inl (inl n), None)
@@ -290,12 +290,12 @@ Proof.
| (_, Some p) => LitProphecy p
end) _); by intros [].
Qed.
-Instance un_op_finite : Countable un_op.
+Global Instance un_op_finite : Countable un_op.
Proof.
refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
(λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
-Instance bin_op_countable : Countable bin_op.
+Global Instance bin_op_countable : Countable bin_op.
Proof.
refine (inj_countable' (λ op, match op with
| PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
@@ -307,7 +307,7 @@ Proof.
| 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
end) _); by intros [].
Qed.
-Instance expr_countable : Countable expr.
+Global Instance expr_countable : Countable expr.
Proof.
set (enc :=
fix go e :=
@@ -388,13 +388,13 @@ Proof.
[exact (gov v)|done..].
- destruct v; by f_equal.
Qed.
-Instance val_countable : Countable val.
+Global Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
-Instance state_inhabited : Inhabited state :=
+Global Instance state_inhabited : Inhabited state :=
populate {| heap := inhabitant; used_proph_id := inhabitant |}.
-Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
-Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
+Global Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Canonical Structure stateO := leibnizO state.
Canonical Structure locO := leibnizO loc.
@@ -699,7 +699,7 @@ Inductive head_step : expr → state → list observation → expr → state →
(κs ++ [(p, (v, w))]) (Val v) σ' ts.
(** Basic properties about the language *)
-Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 6efb2e241..c4a4a0357 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -16,7 +16,7 @@ Definition read : val := λ: "l", !"l".
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR max_natUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
-Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
+Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
Proof. solve_inG. Qed.
Section mono_proof.
@@ -90,7 +90,7 @@ Class ccounterG Σ :=
Definition ccounterΣ : gFunctors :=
#[GFunctor (frac_authR natR)].
-Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
+Global Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
Proof. solve_inG. Qed.
Section contrib_spec.
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index c34a77368..c50ade5de 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -38,5 +38,5 @@ Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless.
-Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
+Global Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 8be6983d5..11c2ea34f 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -22,7 +22,7 @@ Definition join : val :=
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
-Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 61afd495a..050bc4fad 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -17,7 +17,7 @@ Definition release : val := λ: "l", "l" <- #false.
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
-Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
Section proof.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index a464b44a5..05cae40e0 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -32,7 +32,7 @@ Class tlockG Σ :=
Definition tlockΣ : gFunctors :=
#[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
-Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
+Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
Proof. solve_inG. Qed.
Section proof.
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index 6da303478..26c483e65 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -4,12 +4,12 @@ From iris.prelude Require Import options.
Record loc := { loc_car : Z }.
-Instance loc_eq_decision : EqDecision loc.
+Global Instance loc_eq_decision : EqDecision loc.
Proof. solve_decision. Qed.
-Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
+Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
-Instance loc_countable : Countable loc.
+Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
Program Instance loc_infinite : Infinite loc :=
@@ -28,7 +28,7 @@ Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
Lemma loc_add_0 l : l +â‚— 0 = l.
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
-Instance loc_add_inj l : Inj eq eq (loc_add l).
+Global Instance loc_add_inj l : Inj eq eq (loc_add l).
Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.
Definition fresh_locs (ls : gset loc) : loc :=
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 748262648..271eaa855 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -17,7 +17,7 @@ Class heapG Σ := HeapG {
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
}.
-Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
+Global Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs _ :=
(gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
@@ -48,8 +48,8 @@ Section definitions.
inv_mapsto l (from_option I False).
End definitions.
-Instance: Params (@inv_mapsto_own) 4 := {}.
-Instance: Params (@inv_mapsto) 3 := {}.
+Global Instance: Params (@inv_mapsto_own) 4 := {}.
+Global Instance: Params (@inv_mapsto) 3 := {}.
Notation inv_heap_inv := (inv_heap_inv loc (option val)).
Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
diff --git a/tests/algebra.v b/tests/algebra.v
index d20708c8f..169f1b573 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -9,7 +9,7 @@ Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. reflexivity. Qed.
-Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
+Global Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests.
Context `{!invG Σ}.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index 9019204c8..4733b9f9d 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -18,8 +18,8 @@ Add Printing Constructor heapProp.
Section ofe.
Inductive heapProp_equiv' (P Q : heapProp) : Prop :=
{ heapProp_in_equiv : ∀ σ, P σ ↔ Q σ }.
- Instance heapProp_equiv : Equiv heapProp := heapProp_equiv'.
- Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
+ Local Instance heapProp_equiv : Equiv heapProp := heapProp_equiv'.
+ Local Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
Canonical Structure heapPropO := discreteO heapProp.
End ofe.
@@ -220,7 +220,7 @@ Canonical Structure heapPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of heapProp;
bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}.
-Instance heapProp_pure_forall : BiPureForall heapPropI.
+Global Instance heapProp_pure_forall : BiPureForall heapPropI.
Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
Lemma heapProp_proofmode_test {A} (P Q R : heapProp) (Φ Ψ : A → heapProp) :
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index c5b7ed824..1ed8a4882 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -134,16 +134,16 @@ Section M.
Canonical Structure M_O : ofeT := leibnizO M.
- Instance M_valid : Valid M := λ x, x ≠Bot.
- Instance M_op : Op M := λ x y,
+ Local Instance M_valid : Valid M := λ x, x ≠Bot.
+ Local Instance M_op : Op M := λ x y,
match x, y with
| Auth n, Frag j | Frag j, Auth n => if decide (j ≤ n) then Auth n else Bot
| Frag i, Frag j => Frag (max i j)
| _, _ => Bot
end.
- Instance M_pcore : PCore M := λ x,
+ Local Instance M_pcore : PCore M := λ x,
Some match x with Auth j | Frag j => Frag j | _ => Bot end.
- Instance M_unit : Unit M := Frag 0.
+ Local Instance M_unit : Unit M := Frag 0.
Definition M_ra_mixin : RAMixin M.
Proof.
@@ -184,7 +184,7 @@ End M.
Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
-Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
+Global Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Section counter_proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index b859132b9..1c2ce33d5 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -30,7 +30,7 @@ Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
-Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.
Section proof.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 5ce48658c..89c8cc4c4 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -27,7 +27,7 @@ Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
-Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.
Section proof.
--
GitLab