From 334a07db795148a87474a51c72c327affdda0deb Mon Sep 17 00:00:00 2001
From: Simon Spies <spies@mpi-sws.org>
Date: Thu, 27 Oct 2022 12:50:56 +0000
Subject: [PATCH] Disable Implicit Generalization for Typeclass Arguments
---
iris/algebra/big_op.v | 12 ++--
iris/algebra/cmra.v | 38 ++++++------
iris/algebra/cofe_solver.v | 2 +-
iris/algebra/csum.v | 4 +-
iris/algebra/functions.v | 4 +-
iris/algebra/lib/frac_auth.v | 6 +-
iris/algebra/lib/gset_bij.v | 1 +
iris/algebra/lib/ufrac_auth.v | 6 +-
iris/algebra/list.v | 2 +-
iris/algebra/monoid.v | 8 +--
iris/algebra/ofe.v | 30 ++++-----
iris/algebra/updates.v | 6 +-
iris/algebra/vector.v | 2 +-
iris/base_logic/bupd_alt.v | 6 +-
iris/bi/big_op.v | 50 +++++++--------
iris/bi/derived_laws.v | 30 ++++-----
iris/bi/derived_laws_later.v | 4 +-
iris/bi/embedding.v | 8 +--
iris/bi/interface.v | 4 +-
iris/bi/internal_eq.v | 6 +-
iris/bi/lib/atomic.v | 2 +-
iris/bi/lib/core.v | 2 +-
iris/bi/lib/counterexamples.v | 8 +--
iris/bi/lib/relations.v | 16 ++---
iris/bi/monpred.v | 64 ++++++++++----------
iris/bi/plainly.v | 44 +++++++-------
iris/bi/updates.v | 8 +--
iris/proofmode/class_instances.v | 10 +--
iris/proofmode/class_instances_frame.v | 8 +--
iris/proofmode/class_instances_internal_eq.v | 2 +-
iris/proofmode/class_instances_make.v | 6 +-
iris/proofmode/class_instances_plainly.v | 4 +-
iris/proofmode/coq_tactics.v | 2 +-
iris/proofmode/modality_instances.v | 8 +--
iris/proofmode/monpred.v | 28 ++++-----
tests/proofmode.v | 8 +--
tests/telescopes.v | 2 +-
37 files changed, 226 insertions(+), 225 deletions(-)
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index e68312bee..90c35dc12 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -20,7 +20,7 @@ Since these big operators are like quantifiers, they have the same precedence as
[∀] and [∃]. *)
(** * Big ops over lists *)
-Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
+Fixpoint big_opL {M : ofe} {o : M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
match xs with
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
@@ -35,7 +35,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope.
-Local Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
+Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
Local Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
@@ -50,7 +50,7 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope.
-Local Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
+Local Definition big_opS_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Local Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
@@ -62,7 +62,7 @@ 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.
-Local Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
+Local Definition big_opMS_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Local Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
@@ -76,7 +76,7 @@ Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(** * Properties about big ops *)
Section big_op.
-Context `{Monoid M o}.
+Context {M : ofe} {o : M → M → M} `{!Monoid o}.
Implicit Types xs : list M.
Infix "`o`" := o (at level 50, left associativity).
@@ -786,7 +786,7 @@ Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
End big_op.
Section homomorphisms.
- Context `{Monoid M1 o1, Monoid M2 o2}.
+ Context {M1 M2 : ofe} {o1 : M1 → M1 → M1} {o2 : M2 → M2 → M2} `{!Monoid o1, !Monoid o2}.
Infix "`o1`" := o1 (at level 50, left associativity).
Infix "`o2`" := o2 (at level 50, left associativity).
(** The ssreflect rewrite tactic only works for relations that have a
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 5553a52c2..a8439c9b9 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -17,7 +17,7 @@ Notation "(â‹…)" := op (only parsing) : stdpp_scope.
hold:
x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
*)
-Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
+Definition included {A} `{!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.
@@ -34,7 +34,7 @@ Global Hint Mode Valid ! : typeclass_instances.
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.
+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.
Global Instance: Params (@includedN) 4 := {}.
@@ -42,7 +42,7 @@ Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
Section mixin.
Local Set Primitive Projections.
- Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
+ Record CmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {
(* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n (x y : A) cx :
@@ -176,7 +176,7 @@ Global Hint Mode CmraTotal ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
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).
+Definition core {A} `{!PCore A} (x : A) : A := default x (pcore x).
Global Instance: Params (@core) 2 := {}.
(** * CMRAs with a unit element *)
@@ -184,7 +184,7 @@ Class Unit (A : Type) := ε : A.
Global Hint Mode Unit ! : typeclass_instances.
Global Arguments ε {_ _}.
-Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
+Record UcmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
mixin_ucmra_unit_valid : ✓ (ε : A);
mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
@@ -473,7 +473,7 @@ Qed.
(** ** Total core *)
Section total_core.
Local Set Default Proof Using "Type*".
- Context `{CmraTotal A}.
+ Context `{!CmraTotal A}.
Lemma cmra_pcore_core x : pcore x = Some (core x).
Proof.
@@ -562,19 +562,19 @@ Proof.
Qed.
(** ** Discrete *)
-Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
+Lemma cmra_discrete_valid_iff `{!CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
-Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : ✓{0} x ↔ ✓{n} x.
+Lemma cmra_discrete_valid_iff_0 `{!CmraDiscrete A} n x : ✓{0} x ↔ ✓{n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
-Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
+Lemma cmra_discrete_included_iff `{!OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
-Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x ≼{0} y ↔ x ≼{n} y.
+Lemma cmra_discrete_included_iff_0 `{!OfeDiscrete A} n x y : x ≼{0} y ↔ x ≼{n} y.
Proof. by rewrite -!cmra_discrete_included_iff. Qed.
(** Cancelable elements *)
@@ -582,7 +582,7 @@ Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
Lemma cancelable x `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
-Lemma discrete_cancelable x `{CmraDiscrete A}:
+Lemma discrete_cancelable x `{!CmraDiscrete A}:
(∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
@@ -612,7 +612,7 @@ Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
Proof. rewrite comm. eauto using id_free_r. Qed.
-Lemma discrete_id_free x `{CmraDiscrete A}:
+Lemma discrete_id_free x `{!CmraDiscrete A}:
(∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x.
Proof.
intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
@@ -690,7 +690,7 @@ Section cmra_leibniz.
(** ** Total core *)
Section total_core.
- Context `{CmraTotal A}.
+ Context `{!CmraTotal A}.
Lemma cmra_core_r_L x : x â‹… core x = x.
Proof. unfold_leibniz. apply cmra_core_r. Qed.
@@ -720,7 +720,7 @@ End ucmra_leibniz.
(** * Constructing a CMRA with total core *)
Section cmra_total.
- Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
+ Context A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A}.
Context (total : ∀ x : A, is_Some (pcore x)).
Context (op_ne : ∀ x : A, NonExpansive (op x)).
Context (core_ne : NonExpansive (@core A _)).
@@ -1020,7 +1020,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
Section discrete.
Local Set Default Proof Using "Type*".
- Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)).
+ Context `{!Equiv A, !PCore A, !Op A, !Valid A} (Heq : @Equivalence A (≡)).
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist.
@@ -1358,7 +1358,7 @@ Section option.
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.
Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
- Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
+ Lemma Some_core `{!CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Lemma Some_op_opM a ma : Some a â‹… ma = Some (a â‹…? ma).
Proof. by destruct ma. Qed.
@@ -1498,9 +1498,9 @@ Section option.
Lemma Some_included_2 a b : a ≼ b → Some a ≼ Some b.
Proof. rewrite Some_included; eauto. Qed.
- Lemma Some_includedN_total `{CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
+ Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
- Lemma Some_included_total `{CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
+ Lemma Some_included_total `{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
@@ -1615,7 +1615,7 @@ Proof. apply optionURF_contractive. Qed.
(* Dependently-typed functions over a discrete domain *)
Section discrete_fun_cmra.
- Context `{B : A → ucmra}.
+ Context {A : Type} {B : A → ucmra}.
Implicit Types f g : discrete_fun B.
Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x,
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index f2b452fe9..60da38e9e 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -9,7 +9,7 @@ Record solution (F : oFunctor) := Solution {
Global Existing Instance solution_cofe.
Module solver. Section solver.
-Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
+Context (F : oFunctor) `{Fcontr : !oFunctorContractive F}.
Context `{Fcofe : ∀ (T : ofe) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
Notation map := (oFunctor_map F).
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 28209dfb8..1696e27be 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -81,13 +81,13 @@ Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Program Definition csum_chain_r (c : chain csumO) (b : B) : chain B :=
{| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Definition csum_compl `{Cofe A, Cofe B} : Compl csumO := λ c,
+Definition csum_compl `{!Cofe A, !Cofe B} : Compl csumO := λ c,
match c 0 with
| Cinl a => Cinl (compl (csum_chain_l c a))
| Cinr b => Cinr (compl (csum_chain_r c b))
| CsumBot => CsumBot
end.
-Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumO :=
+Global Program Instance csum_cofe `{!Cofe A, !Cofe B} : Cofe csumO :=
{| compl := csum_compl |}.
Next Obligation.
intros ?? n c; rewrite /compl /csum_compl.
diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index e16afa57a..02e36887d 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -13,7 +13,7 @@ Definition discrete_fun_singleton `{EqDecision A} {B : A → ucmra}
Global Instance: Params (@discrete_fun_singleton) 5 := {}.
Section ofe.
- Context `{Heqdec : EqDecision A} {B : A → ofe}.
+ Context {A : Type} `{Heqdec : !EqDecision A} {B : A → ofe}.
Implicit Types x : A.
Implicit Types f g : discrete_fun B.
@@ -52,7 +52,7 @@ Section ofe.
End ofe.
Section cmra.
- Context `{EqDecision A} {B : A → ucmra}.
+ Context {A : Type} `{Heqdec : !EqDecision A} {B : A → ucmra}.
Implicit Types x : A.
Implicit Types f g : discrete_fun B.
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 4ea484de6..38e07b42e 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -65,13 +65,13 @@ Section frac_auth.
Lemma frac_auth_includedN n q a b : ✓{n} (â—F a â‹… â—¯F{q} b) → Some b ≼{n} Some a.
Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
- Lemma frac_auth_included `{CmraDiscrete A} q a b :
+ Lemma frac_auth_included `{!CmraDiscrete A} q a b :
✓ (â—F a â‹… â—¯F{q} b) → Some b ≼ Some a.
Proof. by rewrite auth_both_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
- Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
+ Lemma frac_auth_includedN_total `{!CmraTotal A} n q a b :
✓{n} (â—F a â‹… â—¯F{q} b) → b ≼{n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
- Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b :
+ Lemma frac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q a b :
✓ (â—F a â‹… â—¯F{q} b) → b ≼ a.
Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
diff --git a/iris/algebra/lib/gset_bij.v b/iris/algebra/lib/gset_bij.v
index 51d079b79..1821e0532 100644
--- a/iris/algebra/lib/gset_bij.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -110,6 +110,7 @@ Definition gset_bij_auth `{Countable A, Countable B}
Definition gset_bij_elem `{Countable A, Countable B}
(a : A) (b : B) : gset_bij A B := â—¯V {[ (a, b) ]}.
+
Section gset_bij.
Context `{Countable A, Countable B}.
Implicit Types (a:A) (b:B).
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index f967c5387..9e7abad05 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -83,13 +83,13 @@ Section ufrac_auth.
Lemma ufrac_auth_includedN n p q a b : ✓{n} (â—U_p a â‹… â—¯U_q b) → Some b ≼{n} Some a.
Proof. by rewrite auth_both_validN=> -[/Some_pair_includedN [_ ?] _]. Qed.
- Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
+ Lemma ufrac_auth_included `{!CmraDiscrete A} q p a b :
✓ (â—U_p a â‹… â—¯U_q b) → Some b ≼ Some a.
Proof. rewrite auth_both_valid_discrete=> -[/Some_pair_included [_ ?] _] //. Qed.
- Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
+ Lemma ufrac_auth_includedN_total `{!CmraTotal A} n q p a b :
✓{n} (â—U_p a â‹… â—¯U_q b) → b ≼{n} a.
Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
- Lemma ufrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
+ Lemma ufrac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q p a b :
✓ (â—U_p a â‹… â—¯U_q b) → b ≼ a.
Proof. intros. by eapply Some_included_total, ufrac_auth_included. Qed.
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 039c2d751..713bf4b3f 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -128,7 +128,7 @@ Proof.
induction 1; destruct 1; simpl; [constructor..|f_equiv; try apply Hf; auto].
Qed.
-Lemma big_opL_ne_2 `{Monoid M o} {A : ofe} (f g : nat → A → M) l1 l2 n :
+Lemma big_opL_ne_2 {M : ofe} {o : M → M → M} `{!Monoid o} {A : ofe} (f g : nat → A → M) l1 l2 n :
l1 ≡{n}≡ l2 →
(∀ k y1 y2,
l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
diff --git a/iris/algebra/monoid.v b/iris/algebra/monoid.v
index 95a23c034..eb92af8fe 100644
--- a/iris/algebra/monoid.v
+++ b/iris/algebra/monoid.v
@@ -24,9 +24,9 @@ Class Monoid {M : ofe} (o : M → M → M) := {
monoid_comm : Comm (≡) o;
monoid_left_id : LeftId (≡) monoid_unit o;
}.
-Lemma monoid_proper `{Monoid M o} : Proper ((≡) ==> (≡) ==> (≡)) o.
+Lemma monoid_proper {M : ofe} {o : M → M → M} `{!Monoid o} : Proper ((≡) ==> (≡) ==> (≡)) o.
Proof. apply ne_proper_2, monoid_ne. Qed.
-Lemma monoid_right_id `{Monoid M o} : RightId (≡) monoid_unit o.
+Lemma monoid_right_id {M : ofe} {o : M → M → M} `{!Monoid o} : RightId (≡) monoid_unit o.
Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
(** The [Homomorphism] classes give rise to generic lemmas about big operators
@@ -34,7 +34,7 @@ commuting with each other. We also consider a [WeakMonoidHomomorphism] which
does not necessarily commute with unit; an example is the [own] connective: we
only have `True ==∗ own γ ∅`, not `True ↔ own γ ∅`. *)
Class WeakMonoidHomomorphism {M1 M2 : ofe}
- (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
+ (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
(R : relation M2) (f : M1 → M2) := {
monoid_homomorphism_rel_po : PreOrder R;
monoid_homomorphism_rel_proper : Proper ((≡) ==> (≡) ==> iff) R;
@@ -44,7 +44,7 @@ Class WeakMonoidHomomorphism {M1 M2 : ofe}
}.
Class MonoidHomomorphism {M1 M2 : ofe}
- (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
+ (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
(R : relation M2) (f : M1 → M2) := {
monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 R f;
monoid_homomorphism_unit : R (f monoid_unit) monoid_unit
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 61c1f1717..cb7da59e4 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -138,7 +138,7 @@ Class Cofe (A : ofe) := {
Global Arguments compl : simpl never.
Global Hint Mode Cofe ! : typeclass_instances.
-Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
+Lemma compl_chain_map `{!Cofe A, !Cofe B} (f : A → B) c `(!NonExpansive f) :
compl (chain_map f c) ≡ f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
@@ -194,7 +194,7 @@ Section ofe.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
- Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
+ Lemma conv_compl' `{!Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
Proof.
transitivity (c n); first by apply conv_compl. symmetry.
apply chain_cauchy. lia.
@@ -209,7 +209,7 @@ Section ofe.
End ofe.
(** Contractive functions *)
-Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
+Definition dist_later `{!Dist A} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x ≡{n}≡ y end.
Global Arguments dist_later _ _ !_ _ _ /.
@@ -274,7 +274,7 @@ Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
Global Hint Mode LimitPreserving + + ! : typeclass_instances.
Section limit_preserving.
- Context `{Cofe A}.
+ Context {A : ofe} `{!Cofe A}.
(* These are not instances as they will never fire automatically...
but they can still be helpful in proving things to be limit preserving. *)
@@ -352,7 +352,7 @@ Local Definition fixpoint_unseal :
@fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Section fixpoint.
- Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
+ Context `{!Cofe A, !Inhabited A} (f : A → A) `{!Contractive f}.
(** This lemma does not work well with [rewrite]; we usually define a specific
unfolding lemma for each fixpoint and then [apply fixpoint_unfold] in the
@@ -404,12 +404,12 @@ End fixpoint.
(** Fixpoint of f when f^k is contractive. **)
-Definition fixpointK `{Cofe A, Inhabited A} k (f : A → A)
+Definition fixpointK {A : ofe} `{!Cofe A, !Inhabited A} k (f : A → A)
`{!Contractive (Nat.iter k f)} := fixpoint (Nat.iter k f).
Section fixpointK.
Local Set Default Proof Using "Type*".
- Context `{Cofe A, Inhabited A} (f : A → A) (k : nat).
+ Context {A : ofe} `{!Cofe A, !Inhabited A} (f : A → A) (k : nat).
Context {f_contractive : Contractive (Nat.iter k f)} {f_ne : NonExpansive f}.
(* Note than f_ne is crucial here: there are functions f such that f^2 is contractive,
but f is not non-expansive.
@@ -477,7 +477,7 @@ End fixpointK.
(** Mutual fixpoints *)
Section fixpointAB.
- Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
+ Context {A B : ofe} `{!Cofe A, !Cofe B, !Inhabited A, !Inhabited B}.
Context (fA : A → B → A).
Context (fB : A → B → B).
Context {fA_contractive : ∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
@@ -521,7 +521,7 @@ Section fixpointAB.
End fixpointAB.
Section fixpointAB_ne.
- Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
+ Context {A B : ofe} `{!Cofe A, !Cofe B, !Inhabited A, !Inhabited B}.
Context (fA fA' : A → B → A).
Context (fB fB' : A → B → B).
Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
@@ -589,13 +589,13 @@ Section ofe_mor.
Program Definition ofe_mor_chain (c : chain ofe_morO)
(x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
- Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morO := λ c,
+ Program Definition ofe_mor_compl `{!Cofe B} : Compl ofe_morO := λ c,
{| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
Next Obligation.
intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
(conv_compl n (ofe_mor_chain c y)) /= Hx.
Qed.
- Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morO :=
+ Global Program Instance ofe_mor_cofe `{!Cofe B} : Cofe ofe_morO :=
{| compl := ofe_mor_compl |}.
Next Obligation.
intros ? n c x; simpl.
@@ -909,7 +909,7 @@ Section sum.
{| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
- Definition sum_compl `{Cofe A, Cofe B} : Compl sumO := λ c,
+ Definition sum_compl `{!Cofe A, !Cofe B} : Compl sumO := λ c,
match c 0 with
| inl a => inl (compl (inl_chain c a))
| inr b => inr (compl (inr_chain c b))
@@ -972,7 +972,7 @@ Qed.
(** * Discrete OFEs *)
Section discrete_ofe.
- Context `{Equiv A} (Heq : @Equivalence A (≡)).
+ Context {A : Type} `{!Equiv A} (Heq : @Equivalence A (≡)).
Local Instance discrete_dist : Dist A := λ n x y, x ≡ y.
Definition discrete_ofe_mixin : OfeMixin A.
@@ -1051,7 +1051,7 @@ Section option.
Program Definition option_chain (c : chain optionO) (x : A) : chain A :=
{| chain_car n := default x (c n) |}.
Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
- Definition option_compl `{Cofe A} : Compl optionO := λ c,
+ Definition option_compl `{!Cofe A} : Compl optionO := λ c,
match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
Global Program Instance option_cofe `{Cofe A} : Cofe optionO :=
{ compl := option_compl }.
@@ -1432,7 +1432,7 @@ Section sigma.
Proof. by apply (iso_ofe_mixin proj1_sig). Qed.
Canonical Structure sigO : ofe := Ofe (sig P) sig_ofe_mixin.
- Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigO.
+ Global Instance sig_cofe `{!Cofe A, !LimitPreserving P} : Cofe sigO.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
Global Instance sig_discrete (x : sig P) : Discrete (`x) → Discrete x.
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 57e076870..9807071ce 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -52,7 +52,7 @@ Lemma cmra_update_exclusive `{!Exclusive x} y:
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
(** Updates form a preorder. *)
-(** We set this rewrite relation's cost above the stdlib's
+(** We set this rewrite relation's cost above the stdlib's
([impl], [iff], [eq], ...) and [≡] but below [⊑].
[eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
Global Instance cmra_update_rewrite_relation :
@@ -119,7 +119,7 @@ Qed.
(** ** Frame preserving updates for total CMRAs *)
Section total_updates.
Local Set Default Proof Using "Type*".
- Context `{CmraTotal A}.
+ Context `{!CmraTotal A}.
Lemma cmra_total_updateP x (P : A → Prop) :
x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
@@ -132,7 +132,7 @@ Section total_updates.
Lemma cmra_total_update x y : x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.
- Context `{CmraDiscrete A}.
+ Context `{!CmraDiscrete A}.
Lemma cmra_discrete_updateP (x : A) (P : A → Prop) :
x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
diff --git a/iris/algebra/vector.v b/iris/algebra/vector.v
index d0811da9c..4ac70ea3c 100644
--- a/iris/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -13,7 +13,7 @@ Section ofe.
Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
Canonical Structure vecO m : ofe := Ofe (vec A m) (vec_ofe_mixin m).
- Global Instance list_cofe `{Cofe A} m : Cofe (vecO m).
+ Global Instance list_cofe `{!Cofe A} m : Cofe (vecO m).
Proof.
apply: (iso_cofe_subtype (λ l : list A, length l = m)
(λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //.
diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index 568b27cb9..c466e2f5d 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type*".
(** This file contains an alternative version of basic updates, that is
expression in terms of just the plain modality [â– ]. *)
-Definition bupd_alt `{BiPlainly PROP} (P : PROP) : PROP :=
+Definition bupd_alt {PROP : bi} `{!BiPlainly PROP} (P : PROP) : PROP :=
∀ R, (P -∗ ■R) -∗ ■R.
(** This definition is stated for any BI with a plain modality. The above
@@ -28,7 +28,7 @@ The first two points are shown for any BI with a plain modality. *)
Local Coercion uPred_holds : uPred >-> Funclass.
Section bupd_alt.
- Context `{BiPlainly PROP}.
+ Context {PROP : bi} `{!BiPlainly PROP}.
Implicit Types P Q R : PROP.
Notation bupd_alt := (@bupd_alt PROP _).
@@ -57,7 +57,7 @@ Section bupd_alt.
(** Any modality conforming with [BiBUpdPlainly] entails the alternative
definition *)
- Lemma bupd_bupd_alt `{!BiBUpd PROP, BiBUpdPlainly PROP} P : (|==> P) ⊢ bupd_alt P.
+ Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdPlainly PROP} P : (|==> P) ⊢ bupd_alt P.
Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.
(** We get the usual rule for frame preserving updates if we have an [own]
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index f5f422eef..fd668960c 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -265,7 +265,7 @@ Section sep_list.
rewrite big_sepL_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
- Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
+ Lemma big_sepL_persistently `{!BiAffine PROP} Φ l :
<pers> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
@@ -280,7 +280,7 @@ Section sep_list.
apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
- Lemma big_sepL_forall `{BiAffine PROP} Φ l :
+ Lemma big_sepL_forall `{!BiAffine PROP} Φ l :
(∀ k x, Persistent (Φ k x)) →
([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌠→ Φ k x).
Proof.
@@ -368,14 +368,14 @@ Section sep_list.
[∗] replicate (length l) P ⊣⊢ [∗ list] y ∈ l, P.
Proof. induction l as [|x l]=> //=; by f_equiv. Qed.
- Lemma big_sepL_later `{BiAffine PROP} Φ l :
+ Lemma big_sepL_later `{!BiAffine PROP} Φ l :
▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_later_2 Φ l :
([∗ list] k↦x ∈ l, ▷ Φ k x) ⊢ ▷ [∗ list] k↦x ∈ l, Φ k x.
Proof. by rewrite (big_opL_commute _). Qed.
- Lemma big_sepL_laterN `{BiAffine PROP} Φ n l :
+ Lemma big_sepL_laterN `{!BiAffine PROP} Φ n l :
▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_laterN_2 Φ n l :
@@ -743,7 +743,7 @@ Section sep_list2.
rewrite big_sepL2_affinely_pure_2 //. by setoid_rewrite affinely_elim.
Qed.
- Lemma big_sepL2_persistently `{BiAffine PROP} Φ l1 l2 :
+ Lemma big_sepL2_persistently `{!BiAffine PROP} Φ l1 l2 :
<pers> ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, <pers> (Φ k y1 y2).
Proof.
@@ -764,7 +764,7 @@ Section sep_list2.
by apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
- Lemma big_sepL2_forall `{BiAffine PROP} Φ l1 l2 :
+ Lemma big_sepL2_forall `{!BiAffine PROP} Φ l1 l2 :
(∀ k x1 x2, Persistent (Φ k x1 x2)) →
([∗ list] k↦x1;x2 ∈ l1;l2, Φ k x1 x2) ⊣⊢
⌜length l1 = length l2âŒ
@@ -855,7 +855,7 @@ Section sep_list2.
by rewrite pure_True //left_id intuitionistically_elim wand_elim_l.
Qed.
- Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 :
+ Lemma big_sepL2_later_1 `{!BiAffine PROP} Φ l1 l2 :
(▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
Proof.
rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ âŒ).
@@ -1448,7 +1448,7 @@ Section sep_map.
([∗ map] k ↦ x ∈ filter φ m, Φ k x) ⊣⊢
([∗ map] k ↦ x ∈ m, if decide (φ (k, x)) then Φ k x else emp).
Proof. apply: big_opM_filter'. Qed.
- Lemma big_sepM_filter `{BiAffine PROP}
+ Lemma big_sepM_filter `{!BiAffine PROP}
(φ : K * A → Prop) `{∀ kx, Decision (φ kx)} Φ m :
([∗ map] k ↦ x ∈ filter φ m, Φ k x) ⊣⊢
([∗ map] k ↦ x ∈ m, ⌜φ (k, x)⌠→ Φ k x).
@@ -1501,7 +1501,7 @@ Section sep_map.
rewrite big_sepM_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
- Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
+ Lemma big_sepM_persistently `{!BiAffine PROP} Φ m :
(<pers> ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, <pers> (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
@@ -1519,7 +1519,7 @@ Section sep_map.
by rewrite pure_True // True_impl.
Qed.
- Lemma big_sepM_forall `{BiAffine PROP} Φ m :
+ Lemma big_sepM_forall `{!BiAffine PROP} Φ m :
(∀ k x, Persistent (Φ k x)) →
([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌠→ Φ k x).
Proof.
@@ -1585,14 +1585,14 @@ Section sep_map.
do 2 f_equiv. intros ?; naive_solver.
Qed.
- Lemma big_sepM_later `{BiAffine PROP} Φ m :
+ Lemma big_sepM_later `{!BiAffine PROP} Φ m :
▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_later_2 Φ m :
([∗ map] k↦x ∈ m, ▷ Φ k x) ⊢ ▷ [∗ map] k↦x ∈ m, Φ k x.
Proof. by rewrite big_opM_commute. Qed.
- Lemma big_sepM_laterN `{BiAffine PROP} Φ n m :
+ Lemma big_sepM_laterN `{!BiAffine PROP} Φ n m :
▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_laterN_2 Φ n m :
@@ -2278,7 +2278,7 @@ Section map2.
rewrite big_sepM2_affinely_pure_2 //. by setoid_rewrite affinely_elim.
Qed.
- Lemma big_sepM2_persistently `{BiAffine PROP} Φ m1 m2 :
+ Lemma big_sepM2_persistently `{!BiAffine PROP} Φ m1 m2 :
<pers> ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
⊣⊢ [∗ map] k↦y1;y2 ∈ m1;m2, <pers> (Φ k y1 y2).
Proof.
@@ -2300,7 +2300,7 @@ Section map2.
by rewrite !pure_True // !True_impl.
Qed.
- Lemma big_sepM2_forall `{BiAffine PROP} Φ m1 m2 :
+ Lemma big_sepM2_forall `{!BiAffine PROP} Φ m1 m2 :
(∀ k x1 x2, Persistent (Φ k x1 x2)) →
([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢
⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)âŒ
@@ -2362,7 +2362,7 @@ Section map2.
do 2 f_equiv. intros ?; naive_solver.
Qed.
- Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
+ Lemma big_sepM2_later_1 `{!BiAffine PROP} Φ m1 m2 :
(▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
Proof.
@@ -2637,7 +2637,7 @@ Section gset.
([∗ set] y ∈ filter φ X, Φ y)
⊣⊢ ([∗ set] y ∈ X, if decide (φ y) then Φ y else emp).
Proof. apply: big_opS_filter'. Qed.
- Lemma big_sepS_filter `{BiAffine PROP}
+ Lemma big_sepS_filter `{!BiAffine PROP}
(φ : A → Prop) `{∀ x, Decision (φ x)} Φ X :
([∗ set] y ∈ filter φ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜φ y⌠→ Φ y).
Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
@@ -2653,7 +2653,7 @@ Section gset.
rewrite big_sepS_union // big_sepS_filter'.
by apply sep_mono_r, wand_intro_l.
Qed.
- Lemma big_sepS_filter_acc `{BiAffine PROP}
+ Lemma big_sepS_filter_acc `{!BiAffine PROP}
(φ : A → Prop) `{∀ y, Decision (φ y)} Φ X Y :
(∀ y, y ∈ Y → φ y → y ∈ X) →
([∗ set] y ∈ X, Φ y) -∗
@@ -2710,7 +2710,7 @@ Section gset.
rewrite big_sepS_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
- Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
+ Lemma big_sepS_persistently `{!BiAffine PROP} Φ X :
<pers> ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, <pers> (Φ y).
Proof. apply (big_opS_commute _). Qed.
@@ -2727,7 +2727,7 @@ Section gset.
by rewrite pure_True ?True_impl; last set_solver.
Qed.
- Lemma big_sepS_forall `{BiAffine PROP} Φ X :
+ Lemma big_sepS_forall `{!BiAffine PROP} Φ X :
(∀ x, Persistent (Φ x)) →
([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌠→ Φ x).
Proof.
@@ -2790,14 +2790,14 @@ Section gset.
rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
Qed.
- Lemma big_sepS_later `{BiAffine PROP} Φ X :
+ Lemma big_sepS_later `{!BiAffine PROP} Φ X :
▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_later_2 Φ X :
([∗ set] y ∈ X, ▷ Φ y) ⊢ ▷ ([∗ set] y ∈ X, Φ y).
Proof. by rewrite big_opS_commute. Qed.
- Lemma big_sepS_laterN `{BiAffine PROP} Φ n X :
+ Lemma big_sepS_laterN `{!BiAffine PROP} Φ n X :
▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_laterN_2 Φ n X :
@@ -2923,14 +2923,14 @@ Section gmultiset.
([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
- Lemma big_sepMS_later `{BiAffine PROP} Φ X :
+ Lemma big_sepMS_later `{!BiAffine PROP} Φ X :
▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_later_2 Φ X :
([∗ mset] y ∈ X, ▷ Φ y) ⊢ ▷ [∗ mset] y ∈ X, Φ y.
Proof. by rewrite big_opMS_commute. Qed.
- Lemma big_sepMS_laterN `{BiAffine PROP} Φ n X :
+ Lemma big_sepMS_laterN `{!BiAffine PROP} Φ n X :
▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_laterN_2 Φ n X :
@@ -2967,7 +2967,7 @@ Section gmultiset.
rewrite big_sepMS_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
- Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
+ Lemma big_sepMS_persistently `{!BiAffine PROP} Φ X :
<pers> ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, <pers> (Φ y).
Proof. apply (big_opMS_commute _). Qed.
@@ -2985,7 +2985,7 @@ Section gmultiset.
by rewrite pure_True ?True_impl; last multiset_solver.
Qed.
- Lemma big_sepMS_forall `{BiAffine PROP} Φ X :
+ Lemma big_sepMS_forall `{!BiAffine PROP} Φ X :
(∀ x, Persistent (Φ x)) →
([∗ mset] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌠→ Φ x).
Proof.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 9d6f21982..579db6d24 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -661,7 +661,7 @@ Proof.
- by rewrite !and_elim_l right_id.
- by rewrite !and_elim_r.
Qed.
-Lemma affinely_sep `{BiPositive PROP} P Q :
+Lemma affinely_sep `{!BiPositive PROP} P Q :
<affine> (P ∗ Q) ⊣⊢ <affine> P ∗ <affine> Q.
Proof.
apply (anti_symm _), affinely_sep_2.
@@ -802,7 +802,7 @@ Proof.
Qed.
Section bi_affine.
- Context `{BiAffine PROP}.
+ Context `{!BiAffine PROP}.
Global Instance bi_affine_absorbing P : Absorbing P | 0.
Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed.
@@ -968,7 +968,7 @@ Proof.
Qed.
Lemma persistently_sep_2 P Q : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q).
Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{BiPositive PROP} P Q : <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
+Lemma persistently_sep `{!BiPositive PROP} P Q : <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
Proof.
apply (anti_symm _); auto using persistently_sep_2.
rewrite -persistently_affinely_elim affinely_sep -and_sep_persistently. apply and_intro.
@@ -1010,7 +1010,7 @@ Lemma impl_wand_persistently_2 P Q : (<pers> P -∗ Q) ⊢ (<pers> P → Q).
Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
Section persistently_affine_bi.
- Context `{BiAffine PROP}.
+ Context `{!BiAffine PROP}.
Lemma persistently_emp : <pers> emp ⊣⊢ emp.
Proof. by rewrite -!True_emp persistently_pure. Qed.
@@ -1093,7 +1093,7 @@ Lemma intuitionistically_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢
Proof. by rewrite /bi_intuitionistically persistently_exist affinely_exist. Qed.
Lemma intuitionistically_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
Proof. by rewrite /bi_intuitionistically affinely_sep_2 persistently_sep_2. Qed.
-Lemma intuitionistically_sep `{BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma intuitionistically_sep `{!BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite /bi_intuitionistically -affinely_sep -persistently_sep. Qed.
Lemma intuitionistically_idemp P : □ □ P ⊣⊢ □ P.
@@ -1173,7 +1173,7 @@ Proof.
Qed.
Section bi_affine_intuitionistically.
- Context `{BiAffine PROP}.
+ Context `{!BiAffine PROP}.
Lemma intuitionistically_into_persistently P : □ P ⊣⊢ <pers> P.
Proof. rewrite /bi_intuitionistically affine_affinely //. Qed.
@@ -1213,7 +1213,7 @@ Lemma affinely_if_exist {A} p (Ψ : A → PROP) :
Proof. destruct p; simpl; auto using affinely_exist. Qed.
Lemma affinely_if_sep_2 p P Q : <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q).
Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
-Lemma affinely_if_sep `{BiPositive PROP} p P Q :
+Lemma affinely_if_sep `{!BiPositive PROP} p P Q :
<affine>?p (P ∗ Q) ⊣⊢ <affine>?p P ∗ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_sep. Qed.
@@ -1305,7 +1305,7 @@ Lemma persistently_if_exist {A} p (Ψ : A → PROP) :
Proof. destruct p; simpl; auto using persistently_exist. Qed.
Lemma persistently_if_sep_2 p P Q : <pers>?p P ∗ <pers>?p Q ⊢ <pers>?p (P ∗ Q).
Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
-Lemma persistently_if_sep `{BiPositive PROP} p P Q :
+Lemma persistently_if_sep `{!BiPositive PROP} p P Q :
<pers>?p (P ∗ Q) ⊣⊢ <pers>?p P ∗ <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_sep. Qed.
@@ -1351,7 +1351,7 @@ Lemma intuitionistically_if_exist {A} p (Ψ : A → PROP) :
Proof. destruct p; simpl; auto using intuitionistically_exist. Qed.
Lemma intuitionistically_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
Proof. destruct p; simpl; auto using intuitionistically_sep_2. Qed.
-Lemma intuitionistically_if_sep `{BiPositive PROP} p P Q :
+Lemma intuitionistically_if_sep `{!BiPositive PROP} p P Q :
□?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_sep. Qed.
@@ -1454,7 +1454,7 @@ Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
Proof. rewrite intuitionistic_intuitionistically. done. Qed.
Section persistent_bi_absorbing.
- Context `{BiAffine PROP}.
+ Context `{!BiAffine PROP}.
Lemma intuitionistically_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
Proof.
@@ -1614,11 +1614,11 @@ Proof.
- apply persistently_pure.
Qed.
-Global Instance bi_persistently_sep_weak_homomorphism `{BiPositive PROP} :
+Global Instance bi_persistently_sep_weak_homomorphism `{!BiPositive PROP} :
WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. apply persistently_sep. Qed.
-Global Instance bi_persistently_sep_homomorphism `{BiAffine PROP} :
+Global Instance bi_persistently_sep_homomorphism `{!BiAffine PROP} :
MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. apply persistently_emp. Qed.
@@ -1631,20 +1631,20 @@ Global Instance bi_persistently_sep_entails_homomorphism :
Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.
(* Limits *)
-Lemma limit_preserving_entails {A : ofe} `{Cofe A} (Φ Ψ : A → PROP) :
+Lemma limit_preserving_entails {A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x).
Proof.
intros HΦ HΨ c Hc. apply entails_eq_True, equiv_dist=>n.
rewrite conv_compl. apply equiv_dist, entails_eq_True. done.
Qed.
-Lemma limit_preserving_equiv {A : ofe} `{Cofe A} (Φ Ψ : A → PROP) :
+Lemma limit_preserving_equiv {A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
Proof.
intros HΦ HΨ. eapply limit_preserving_ext.
{ intros x. symmetry; apply equiv_entails. }
apply limit_preserving_and; by apply limit_preserving_entails.
Qed.
-Global Instance limit_preserving_Persistent {A:ofe} `{Cofe A} (Φ : A → PROP) :
+Global Instance limit_preserving_Persistent {A : ofe} `{!Cofe A} (Φ : A → PROP) :
NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index 4828ebcd5..03c8e615a 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -210,7 +210,7 @@ Lemma laterN_forall {A} n (Φ : A → PROP) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a,
Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
Lemma laterN_exist_2 {A} n (Φ : A → PROP) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a).
Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
-Lemma laterN_exist `{Inhabited A} n (Φ : A → PROP) :
+Lemma laterN_exist {A} `{!Inhabited A} n (Φ : A → PROP) :
(▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a.
Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed.
Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
@@ -340,7 +340,7 @@ Proof.
rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
Qed.
-Global Instance emp_timeless `{BiAffine PROP} : Timeless (PROP:=PROP) emp.
+Global Instance emp_timeless `{!BiAffine PROP} : Timeless (PROP:=PROP) emp.
Proof. rewrite -True_emp. apply _. Qed.
Global Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index 8a7e39e58..af9cbbdea 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -26,7 +26,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
internal equality of _any other_ BI [PROP']. This is more general, as we do
not have any machinary to embed [siProp] into a BI with internal equality. *)
- bi_embed_mixin_interal_inj `{BiInternalEq PROP'} (P Q : PROP1) :
+ bi_embed_mixin_interal_inj {PROP' : bi} `{!BiInternalEq PROP'} (P Q : PROP1) :
⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
bi_embed_mixin_impl_2 (P Q : PROP1) :
@@ -86,7 +86,7 @@ Global Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
Global Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
Section embed_laws.
- Context `{BiEmbed PROP1 PROP2}.
+ Context {PROP1 PROP2 : bi} `{!BiEmbed PROP1 PROP2}.
Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
Implicit Types P : PROP1.
@@ -117,7 +117,7 @@ Section embed_laws.
End embed_laws.
Section embed.
- Context `{BiEmbed PROP1 PROP2}.
+ Context {PROP1 PROP2 : bi} `{!BiEmbed PROP1 PROP2}.
Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
Implicit Types P Q R : PROP1.
@@ -324,7 +324,7 @@ Note that declaring these instances globally can make TC search ambiguous or
diverging. These are only defined so that a user can conveniently use them to
manually combine embeddings. *)
Section embed_embed.
- Context `{BiEmbed PROP1 PROP2, BiEmbed PROP2 PROP3}.
+ Context {PROP1 PROP2 PROP3 : bi} `{!BiEmbed PROP1 PROP2, !BiEmbed PROP2 PROP3}.
Local Instance embed_embed : Embed PROP1 PROP3 := λ P, ⎡ ⎡ P ⎤ ⎤%I.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 1ebab781a..656ce7883 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
Set Primitive Projections.
Section bi_mixin.
- Context {PROP : Type} `{Dist PROP, Equiv PROP}.
+ Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.
Context (bi_entails : PROP → PROP → Prop).
Context (bi_emp : PROP).
Context (bi_pure : Prop → PROP).
@@ -235,7 +235,7 @@ Global Arguments bi_persistently {PROP} _ : simpl never, rename.
Global Arguments bi_later {PROP} _ : simpl never, rename.
Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-(** We set this rewrite relation's cost above the stdlib's
+(** We set this rewrite relation's cost above the stdlib's
([impl], [iff], [eq], ...) and [≡] but below [⊑].
[eq] (at 100) < [≡] (at 150) < [bi_entails _] (at 170) < [⊑] (at 200)
*)
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 0cf55bb45..4ad7f1dcd 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -19,7 +19,7 @@ Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *)
-Record BiInternalEqMixin (PROP : bi) `(InternalEq PROP) := {
+Record BiInternalEqMixin (PROP : bi) `(!InternalEq PROP) := {
bi_internal_eq_mixin_internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A);
bi_internal_eq_mixin_internal_eq_refl {A : ofe} (P : PROP) (a : A) : P ⊢ a ≡ a;
bi_internal_eq_mixin_internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
@@ -44,7 +44,7 @@ Global Hint Mode BiInternalEq ! : typeclass_instances.
Global Arguments bi_internal_eq_internal_eq : simpl never.
Section internal_eq_laws.
- Context `{BiInternalEq PROP}.
+ Context {PROP : bi} `{!BiInternalEq PROP}.
Implicit Types P Q : PROP.
Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
@@ -74,7 +74,7 @@ End internal_eq_laws.
(* Derived laws *)
Section internal_eq_derived.
-Context `{BiInternalEq PROP}.
+Context {PROP : bi} `{!BiInternalEq PROP}.
Implicit Types P : PROP.
(* Force implicit argument PROP *)
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index dca9a87bb..45be2a8f7 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -9,7 +9,7 @@ Local Tactic Notation "iSplitWith" constr(H) :=
iApply (bi.and_parallel with H); iSplit; iIntros H.
Section definition.
- Context `{BiFUpd PROP} {TA TB : tele}.
+ Context {PROP : bi} `{!BiFUpd PROP} {TA TB : tele}.
Implicit Types
(Eo Ei : coPset) (* outer/inner masks *)
(α : TA → PROP) (* atomic pre-condition *)
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 0bc59a54f..def486ff0 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -14,7 +14,7 @@ Global Instance: Params (@coreP) 1 := {}.
Typeclasses Opaque coreP.
Section core.
- Context `{!BiPlainly PROP}.
+ Context {PROP : bi} `{!BiPlainly PROP}.
Implicit Types P Q : PROP.
Lemma coreP_intro P : P -∗ coreP P.
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 05995a0d4..baa171d5c 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -12,7 +12,7 @@ trivial, i.e., it gives [P -∗ P ∗ P] and [P ∧ Q -∗ P ∗ Q].
Our proof essentially follows the structure of the proof of Theorem 3 in
https://scholar.princeton.edu/sites/default/files/qinxiang/files/putting_order_to_the_separation_logic_jungle_revised_version.pdf *)
Module affine_em. Section affine_em.
- Context `{!BiAffine PROP}.
+ Context {PROP : bi} `{!BiAffine PROP}.
Context (em : ∀ P : PROP, ⊢ P ∨ ¬P).
Implicit Types P Q : PROP.
@@ -36,7 +36,7 @@ End affine_em. End affine_em.
classical excluded-middle [P ∨ ¬P] axiom makes the later operator trivial, i.e.,
it gives [▷ P] for any [P], or equivalently [▷ P ≡ True]. *)
Module löb_em. Section löb_em.
- Context `{!BiLöb PROP}.
+ Context {PROP : bi} `{!BiLöb PROP}.
Context (em : ∀ P : PROP, ⊢ P ∨ ¬P).
Implicit Types P : PROP.
@@ -51,7 +51,7 @@ End löb_em. End löb_em.
(** This proves that we need the â–· in a "Saved Proposition" construction with
name-dependent allocation. *)
Module savedprop. Section savedprop.
- Context `{BiAffine PROP}.
+ Context {PROP : bi} `{!BiAffine PROP}.
Implicit Types P : PROP.
Context (bupd : PROP → PROP).
@@ -112,7 +112,7 @@ End savedprop. End savedprop.
(** This proves that we need the â–· when opening invariants. *)
Module inv. Section inv.
- Context `{BiAffine PROP}.
+ Context {PROP : bi} `{!BiAffine PROP}.
Implicit Types P : PROP.
(** Assumptions *)
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 55b43cbd4..6c37b516a 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -7,13 +7,13 @@ From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
-Definition bi_rtc_pre `{!BiInternalEq PROP}
+Definition bi_rtc_pre {PROP : bi} `{!BiInternalEq PROP}
{A : ofe} (R : A → A → PROP)
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x'.
-Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
- {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+Global Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
+ {A : ofe} (R : A → A → PROP) `{!NonExpansive2 R} (x : A) :
BiMonoPred (bi_rtc_pre R x).
Proof.
constructor; [|solve_proper].
@@ -24,28 +24,28 @@ Proof.
iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
Qed.
-Definition bi_rtc `{!BiInternalEq PROP}
+Definition bi_rtc {PROP : bi} `{!BiInternalEq PROP}
{A : ofe} (R : A → A → PROP) (x1 x2 : A) : PROP :=
bi_least_fixpoint (bi_rtc_pre R x2) x1.
Global Instance: Params (@bi_rtc) 3 := {}.
Typeclasses Opaque bi_rtc.
-Global Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP) :
+Global Instance bi_rtc_ne {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (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.
-Global Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP)
+Global Instance bi_rtc_proper {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP)
: Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
Section bi_rtc.
- Context `{!BiInternalEq PROP}.
+ Context {PROP : bi} `{!BiInternalEq PROP}.
Context {A : ofe}.
- Context (R : A → A → PROP) `{NonExpansive2 R}.
+ Context (R : A → A → PROP) `{!NonExpansive2 R}.
Lemma bi_rtc_unfold (x1 x2 : A) :
bi_rtc R x1 x2 ≡ bi_rtc_pre R x2 (λ x1, bi_rtc R x1 x2) x1.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index d6c91746c..f8c3922a1 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -65,7 +65,7 @@ Section Ofe_Cofe_def.
Canonical Structure monPredO := Ofe monPred monPred_ofe_mixin.
- Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredO.
+ Global Instance monPred_cofe `{!Cofe PROP} : Cofe monPredO.
Proof.
unshelve refine (iso_cofe_subtype (A:=I-d>PROP) _ MonPred monPred_at _ _ _);
[apply _|by apply monPred_sig_dist|done|].
@@ -836,17 +836,17 @@ Proof.
Qed.
(** BUpd *)
-Local Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
+Local Program Definition monPred_bupd_def `{!BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Local Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Local Arguments monPred_bupd {_}.
-Local Lemma monPred_bupd_unseal `{BiBUpd PROP} :
+Local Lemma monPred_bupd_unseal `{!BiBUpd PROP} :
@bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
-Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
+Lemma monPred_bupd_mixin `{!BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
Proof.
split; rewrite monPred_bupd_unseal.
- split=>/= i. solve_proper.
@@ -855,17 +855,17 @@ Proof.
- intros P. split=>/= i. apply bupd_trans.
- intros P Q. split=>/= i. rewrite !monPred_at_sep /=. apply bupd_frame_r.
Qed.
-Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
+Global Instance monPred_bi_bupd `{!BiBUpd PROP} : BiBUpd monPredI :=
{| bi_bupd_mixin := monPred_bupd_mixin |}.
-Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
+Lemma monPred_at_bupd `{!BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
Proof. by rewrite monPred_bupd_unseal. Qed.
-Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
+Global Instance bupd_objective `{!BiBUpd PROP} P `{!Objective P} :
Objective (|==> P).
Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
-Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
+Global Instance monPred_bi_embed_bupd `{!BiBUpd PROP} :
BiEmbedBUpd PROP monPredI.
Proof. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
@@ -928,10 +928,10 @@ Proof.
- intros A x y. split=> i /=. unseal. by apply later_equivI_1.
- intros A x y. split=> i /=. unseal. by apply later_equivI_2.
Qed.
-Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} : BiInternalEq monPredI :=
+Global Instance monPred_bi_internal_eq `{!BiInternalEq PROP} : BiInternalEq monPredI :=
{| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
-Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
+Global Instance monPred_bi_embed_internal_eq `{!BiInternalEq PROP} :
BiEmbedInternalEq PROP monPredI.
Proof. split=> i. rewrite monPred_internal_eq_unseal. by unseal. Qed.
@@ -957,7 +957,7 @@ Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofe} (x y : A)
Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
(** FUpd *)
-Local Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
+Local Program Definition monPred_fupd_def `{!BiFUpd PROP} (E1 E2 : coPset)
(P : monPred) : monPred :=
MonPred (λ i, |={E1,E2}=> P i)%I _.
Next Obligation. solve_proper. Qed.
@@ -965,11 +965,11 @@ Local Definition monPred_fupd_aux : seal (@monPred_fupd_def).
Proof. by eexists. Qed.
Definition monPred_fupd := monPred_fupd_aux.(unseal).
Local Arguments monPred_fupd {_}.
-Local Lemma monPred_fupd_unseal `{BiFUpd PROP} :
+Local Lemma monPred_fupd_unseal `{!BiFUpd PROP} :
@fupd _ monPred_fupd = monPred_fupd_def.
Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
-Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
+Lemma monPred_fupd_mixin `{!BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
Proof.
split; rewrite monPred_fupd_unseal.
- split=>/= i. solve_proper.
@@ -981,36 +981,36 @@ Proof.
rewrite monPred_impl_force monPred_at_pure -fupd_mask_frame_r' //.
- intros E1 E2 P Q. split=>/= i. by rewrite !monPred_at_sep /= fupd_frame_r.
Qed.
-Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
+Global Instance monPred_bi_fupd `{!BiFUpd PROP} : BiFUpd monPredI :=
{| bi_fupd_mixin := monPred_fupd_mixin |}.
-Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
+Global Instance monPred_bi_bupd_fupd `{!BiBUpd PROP} `{!BiFUpd PROP} `{!BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
Proof.
intros E P. split=>/= i.
rewrite monPred_at_bupd monPred_fupd_unseal bupd_fupd //=.
Qed.
-Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
+Global Instance monPred_bi_embed_fupd `{!BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
Proof. split=>i /=. by rewrite monPred_fupd_unseal /= !monPred_at_embed. Qed.
-Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
+Lemma monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P :
(|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
Proof. by rewrite monPred_fupd_unseal. Qed.
-Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
+Global Instance fupd_objective E1 E2 P `{!Objective P} `{!BiFUpd PROP} :
Objective (|={E1,E2}=> P).
Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
(** Plainly *)
-Local Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
+Local Definition monPred_plainly_def `{!BiPlainly PROP} P : monPred :=
MonPred (λ _, ∀ i, ■(P i))%I _.
Local Definition monPred_plainly_aux : seal (@monPred_plainly_def).
Proof. by eexists. Qed.
Definition monPred_plainly := monPred_plainly_aux.(unseal).
Local Arguments monPred_plainly {_}.
-Local Lemma monPred_plainly_unseal `{BiPlainly PROP} :
+Local Lemma monPred_plainly_unseal `{!BiPlainly PROP} :
@plainly _ monPred_plainly = monPred_plainly_def.
Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
-Lemma monPred_plainly_mixin `{BiPlainly PROP} :
+Lemma monPred_plainly_mixin `{!BiPlainly PROP} :
BiPlainlyMixin monPredI monPred_plainly.
Proof.
split; rewrite monPred_plainly_unseal; try unseal.
@@ -1033,7 +1033,7 @@ Proof.
- intros P. split=> i /=.
rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
Qed.
-Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
+Global Instance monPred_bi_plainly `{!BiPlainly PROP} : BiPlainly monPredI :=
{| bi_plainly_mixin := monPred_plainly_mixin |}.
Global Instance minPred_bi_persistently_impl_plainly
@@ -1065,7 +1065,7 @@ Proof.
apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.
-Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
+Global Instance monPred_bi_embed_plainly `{!BiPlainly PROP} :
BiEmbedPlainly PROP monPredI.
Proof.
split=> i. rewrite monPred_plainly_unseal; unseal. apply (anti_symm _).
@@ -1073,7 +1073,7 @@ Proof.
- by rewrite (bi.forall_elim inhabitant).
Qed.
-Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} :
+Global Instance monPred_bi_bupd_plainly `{!BiBUpd PROP} `{!BiPlainly PROP} `{!BiBUpdPlainly PROP} :
BiBUpdPlainly monPredI.
Proof.
intros P. split=> /= i.
@@ -1081,15 +1081,15 @@ Proof.
apply bupd_plainly.
Qed.
-Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
+Lemma monPred_plainly_unfold `{!BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
Proof. by rewrite monPred_plainly_unseal monPred_embed_unseal. Qed.
-Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
+Lemma monPred_at_plainly `{!BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
Proof. by rewrite monPred_plainly_unseal. Qed.
-Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
+Global Instance monPred_at_plain `{!BiPlainly PROP} P i : Plain P → Plain (P i).
Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
-Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} :
+Global Instance monPred_bi_fupd_plainly `{!BiFUpd PROP} `{!BiPlainly PROP} `{!BiFUpdPlainly PROP} :
BiFUpdPlainly monPredI.
Proof.
split; rewrite !monPred_fupd_unseal; try unseal.
@@ -1105,16 +1105,16 @@ Proof.
by rewrite monPred_at_plainly (bi.forall_elim i).
Qed.
-Global Instance plainly_objective `{BiPlainly PROP} P : Objective (â– P).
+Global Instance plainly_objective `{!BiPlainly PROP} P : Objective (â– P).
Proof. rewrite monPred_plainly_unfold. apply _. Qed.
-Global Instance plainly_if_objective `{BiPlainly PROP} P p `{!Objective P} :
+Global Instance plainly_if_objective `{!BiPlainly PROP} P p `{!Objective P} :
Objective (â– ?p P).
Proof. rewrite /plainly_if. destruct p; apply _. Qed.
-Global Instance monPred_objectively_plain `{BiPlainly PROP} P :
+Global Instance monPred_objectively_plain `{!BiPlainly PROP} P :
Plain P → Plain (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
-Global Instance monPred_subjectively_plain `{BiPlainly PROP} P :
+Global Instance monPred_subjectively_plain `{!BiPlainly PROP} P :
Plain P → Plain (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
End bi_facts.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 4109333d9..4edbb20de 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -51,7 +51,7 @@ Global Arguments BiPersistentlyImplPlainly _ {_}.
Global Arguments persistently_impl_plainly _ {_ _} _.
Global Hint Mode BiPersistentlyImplPlainly ! - : typeclass_instances.
-Class BiPlainlyExist `{!BiPlainly PROP} :=
+Class BiPlainlyExist {PROP: bi} `{!BiPlainly PROP} :=
plainly_exist_1 A (Ψ : A → PROP) :
■(∃ a, Ψ a) ⊢ ∃ a, ■(Ψ a).
Global Arguments BiPlainlyExist : clear implicits.
@@ -59,7 +59,7 @@ Global Arguments BiPlainlyExist _ {_}.
Global Arguments plainly_exist_1 _ {_ _} _.
Global Hint Mode BiPlainlyExist ! - : typeclass_instances.
-Class BiPropExt `{!BiPlainly PROP, !BiInternalEq PROP} :=
+Class BiPropExt {PROP: bi} `{!BiPlainly PROP, !BiInternalEq PROP} :=
prop_ext_2 (P Q : PROP) : ■(P ∗-∗ Q) ⊢ P ≡ Q.
Global Arguments BiPropExt : clear implicits.
Global Arguments BiPropExt _ {_ _}.
@@ -67,7 +67,7 @@ Global Arguments prop_ext_2 _ {_ _ _} _.
Global Hint Mode BiPropExt ! - - : typeclass_instances.
Section plainly_laws.
- Context `{BiPlainly PROP}.
+ Context {PROP: bi} `{!BiPlainly PROP}.
Implicit Types P Q : PROP.
Global Instance plainly_ne : NonExpansive (@plainly PROP _).
@@ -95,13 +95,13 @@ Section plainly_laws.
End plainly_laws.
(* Derived properties and connectives *)
-Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■P.
+Class Plain {PROP: bi} `{!BiPlainly PROP} (P : PROP) := plain : P ⊢ ■P.
Global Arguments Plain {_ _} _%I : simpl never.
Global Arguments plain {_ _} _%I {_}.
Global Hint Mode Plain + - ! : typeclass_instances.
Global Instance: Params (@Plain) 1 := {}.
-Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
+Definition plainly_if {PROP: bi} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
(if p then â– P else P)%I.
Global Arguments plainly_if {_ _} !_ _%I /.
Global Instance: Params (@plainly_if) 2 := {}.
@@ -111,7 +111,7 @@ Notation "â– ? p P" := (plainly_if p P) : bi_scope.
(* Derived laws *)
Section plainly_derived.
-Context `{BiPlainly PROP}.
+Context {PROP: bi} `{!BiPlainly PROP}.
Implicit Types P : PROP.
Local Hint Resolve pure_intro forall_intro : core.
@@ -245,7 +245,7 @@ Proof.
Qed.
Lemma plainly_sep_2 P Q : ■P ∗ ■Q ⊢ ■(P ∗ Q).
Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
-Lemma plainly_sep `{BiPositive PROP} P Q : ■(P ∗ Q) ⊣⊢ ■P ∗ ■Q.
+Lemma plainly_sep `{!BiPositive PROP} P Q : ■(P ∗ Q) ⊣⊢ ■P ∗ ■Q.
Proof.
apply (anti_symm _); auto using plainly_sep_2.
rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
@@ -283,7 +283,7 @@ Lemma plainly_wand_affinely_plainly P Q :
Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
Section plainly_affine_bi.
- Context `{BiAffine PROP}.
+ Context `{!BiAffine PROP}.
Lemma plainly_emp : ■emp ⊣⊢@{PROP} emp.
Proof. by rewrite -!True_emp plainly_pure. Qed.
@@ -385,7 +385,7 @@ Proof.
- apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
Qed.
-Global Instance limit_preserving_Plain {A:ofe} `{Cofe A} (Φ : A → PROP) :
+Global Instance limit_preserving_Plain {A : ofe} `{!Cofe A} (Φ : A → PROP) :
NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
@@ -400,7 +400,7 @@ Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
Proof. split; try apply _. simpl. rewrite plainly_emp. done. Qed.
-Global Instance plainly_sep_homomorphism `{BiAffine PROP} :
+Global Instance plainly_sep_homomorphism `{!BiAffine PROP} :
MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
Proof. split; try apply _. apply plainly_emp. Qed.
Global Instance plainly_and_homomorphism :
@@ -425,19 +425,19 @@ Lemma big_sepL2_plainly `{!BiAffine PROP} {A B} (Φ : nat → A → B → PROP)
⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■(Φ k y1 y2).
Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed.
-Lemma big_sepM_plainly `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
+Lemma big_sepM_plainly `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
■([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■(Φ k x).
Proof. apply (big_opM_commute _). Qed.
-Lemma big_sepM2_plainly `{BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
+Lemma big_sepM2_plainly `{!BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
■([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢ [∗ map] k↦x1;x2 ∈ m1;m2, ■(Φ k x1 x2).
Proof. by rewrite !big_sepM2_alt plainly_and plainly_pure big_sepM_plainly. Qed.
-Lemma big_sepS_plainly `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+Lemma big_sepS_plainly `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
■([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■(Φ y).
Proof. apply (big_opS_commute _). Qed.
-Lemma big_sepMS_plainly `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+Lemma big_sepMS_plainly `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
■([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■(Φ y).
Proof. apply (big_opMS_commute _). Qed.
@@ -520,39 +520,39 @@ Global Instance big_sepL2_plain `{!BiAffine PROP} {A B} (Φ : nat → A → B
Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. rewrite big_sepL2_alt. apply _. Qed.
-Global Instance big_sepM_empty_plain `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) :
+Global Instance big_sepM_empty_plain `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) :
Plain ([∗ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
-Global Instance big_sepM_plain `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
+Global Instance big_sepM_plain `{!BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
(∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x).
Proof.
induction m using map_ind;
[rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
Qed.
-Global Instance big_sepM2_empty_plain `{BiAffine PROP, Countable K}
+Global Instance big_sepM2_empty_plain `{!BiAffine PROP, Countable K}
{A B} (Φ : K → A → B → PROP) :
Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
Proof. rewrite big_sepM2_empty. apply _. Qed.
-Global Instance big_sepM2_plain `{BiAffine PROP, Countable K}
+Global Instance big_sepM2_plain `{!BiAffine PROP, Countable K}
{A B} (Φ : K → A → B → PROP) m1 m2 :
(∀ k x1 x2, Plain (Φ k x1 x2)) →
Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
Proof. intros. rewrite big_sepM2_alt. apply _. Qed.
-Global Instance big_sepS_empty_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) :
+Global Instance big_sepS_empty_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) :
Plain ([∗ set] x ∈ ∅, Φ x).
Proof. rewrite big_opS_empty. apply _. Qed.
-Global Instance big_sepS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+Global Instance big_sepS_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
(∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
Proof.
induction X using set_ind_L;
[rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
Qed.
-Global Instance big_sepMS_empty_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) :
+Global Instance big_sepMS_empty_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) :
Plain ([∗ mset] x ∈ ∅, Φ x).
Proof. rewrite big_opMS_empty. apply _. Qed.
-Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
+Global Instance big_sepMS_plain `{!BiAffine PROP, Countable A} (Φ : A → PROP) X :
(∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
Proof.
induction X using gmultiset_ind;
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 2db589017..74d22bd32 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -132,7 +132,7 @@ Class BiFUpdPlainly (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Section bupd_laws.
- Context `{BiBUpd PROP}.
+ Context {PROP : bi} `{!BiBUpd PROP}.
Implicit Types P : PROP.
Global Instance bupd_ne : NonExpansive (@bupd PROP _).
@@ -148,7 +148,7 @@ Section bupd_laws.
End bupd_laws.
Section fupd_laws.
- Context `{BiFUpd PROP}.
+ Context {PROP : bi} `{!BiFUpd PROP}.
Implicit Types P : PROP.
Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
@@ -173,7 +173,7 @@ Section fupd_laws.
End fupd_laws.
Section bupd_derived.
- Context `{BiBUpd PROP}.
+ Context {PROP : bi} `{!BiBUpd PROP}.
Implicit Types P Q R : PROP.
(* FIXME: Removing the `PROP:=` diverges. *)
@@ -262,7 +262,7 @@ Section bupd_derived.
End bupd_derived.
Section fupd_derived.
- Context `{BiFUpd PROP}.
+ Context {PROP : bi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
Global Instance fupd_proper E1 E2 :
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 0d431a854..dc207ad91 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -112,7 +112,7 @@ Proof.
rewrite /KnownLFromAssumption /FromAssumption /= =><-.
rewrite intuitionistically_persistently_elim //.
Qed.
-Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
+Global Instance from_assumption_persistently_l_false `{!BiAffine PROP} P Q :
FromAssumption true P Q → KnownLFromAssumption false (<pers> P) Q.
Proof.
rewrite /KnownLFromAssumption /FromAssumption /= =><-.
@@ -703,7 +703,7 @@ Proof.
by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
Qed.
-Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P ∗ Q) P Q.
+Global Instance into_and_sep `{!BiPositive PROP} P Q : IntoAnd true (P ∗ Q) P Q.
Proof.
rewrite /IntoAnd /= intuitionistically_sep
-and_sep_intuitionistically intuitionistically_and //.
@@ -770,10 +770,10 @@ Qed.
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
-Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
+Global Instance into_sep_affinely `{!BiPositive PROP} P Q1 Q2 :
IntoSep P Q1 Q2 → IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
-Global Instance into_sep_intuitionistically `{BiPositive PROP} P Q1 Q2 :
+Global Instance into_sep_intuitionistically `{!BiPositive PROP} P Q1 Q2 :
IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite intuitionistically_sep. Qed.
(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely.
@@ -783,7 +783,7 @@ Global Instance into_sep_affinely_trim P Q1 Q2 :
IntoSep P Q1 Q2 → IntoSep (<affine> P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
-Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
+Global Instance into_sep_persistently `{!BiPositive PROP} P Q1 Q2 :
IntoSep P Q1 Q2 →
IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 2c9d71237..e3c78d51e 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -46,14 +46,14 @@ Proof.
- by rewrite right_id -affinely_affinely_if affine_affinely.
Qed.
-Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
+Global Instance frame_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
Frame p R P Q → MakeEmbed Q Q' →
Frame p ⎡R⎤ ⎡P⎤ Q' | 2. (* Same cost as default. *)
Proof.
rewrite /Frame /MakeEmbed => <- <-.
rewrite embed_sep embed_intuitionistically_if_2 => //.
Qed.
-Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
+Global Instance frame_pure_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
Frame p ⌜φ⌠P Q → MakeEmbed Q Q' →
Frame p ⌜φ⌠⎡P⎤ Q' | 2. (* Same cost as default. *)
Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
@@ -241,10 +241,10 @@ Proof.
by rewrite laterN_intuitionistically_if_2 laterN_sep.
Qed.
-Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
+Global Instance frame_bupd `{!BiBUpd PROP} p R P Q :
Frame p R P Q → Frame p R (|==> P) (|==> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
-Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
+Global Instance frame_fupd `{!BiFUpd PROP} p E1 E2 R P Q :
Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
diff --git a/iris/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
index c37e4a6ab..af546a0da 100644
--- a/iris/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -40,7 +40,7 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
Global Instance into_internal_eq_absorbingly {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofe} (x y : A) P :
+Global Instance into_internal_eq_plainly `{!BiPlainly PROP} {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (■P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
Global Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index bb638daf7..a6fc44e18 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -31,13 +31,13 @@ Global Instance persistently_quick_absorbing P : QuickAbsorbing (<pers> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
(** Embed *)
-Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
+Global Instance make_embed_pure {PROP'} `{!BiEmbed PROP PROP'} φ :
KnownMakeEmbed (PROP:=PROP) ⌜φ⌠⌜φâŒ.
Proof. apply embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
+Global Instance make_embed_emp {PROP'} `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
-Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
+Global Instance make_embed_default {PROP'} `{!BiEmbed PROP PROP'} P :
MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index efd3aa468..c87e3ff53 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
Import bi.
Section class_instances_plainly.
-Context `{!BiPlainly PROP}.
+Context {PROP} `{!BiPlainly PROP}.
Implicit Types P Q R : PROP.
Global Instance from_assumption_plainly_l_true P Q :
@@ -13,7 +13,7 @@ Proof.
rewrite /KnownLFromAssumption /FromAssumption /= =><-.
rewrite intuitionistically_plainly_elim //.
Qed.
-Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
+Global Instance from_assumption_plainly_l_false `{!BiAffine PROP} P Q :
FromAssumption true P Q → KnownLFromAssumption false (■P) Q.
Proof.
rewrite /KnownLFromAssumption /FromAssumption /= =><-.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 10bed36c0..ac576efcd 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -69,7 +69,7 @@ Global Instance affine_env_snoc Γ i P :
Proof. by constructor. Qed.
(* If the BI is affine, no need to walk on the whole environment. *)
-Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
+Global Instance affine_env_bi `(!BiAffine PROP) Γ : AffineEnv Γ | 0.
Proof. induction Γ; apply _. Qed.
Local Instance affine_env_spatial Δ :
diff --git a/iris/proofmode/modality_instances.v b/iris/proofmode/modality_instances.v
index f35432dd5..9206cd26d 100644
--- a/iris/proofmode/modality_instances.v
+++ b/iris/proofmode/modality_instances.v
@@ -34,7 +34,7 @@ Section modalities.
Definition modality_intuitionistically :=
Modality _ modality_intuitionistically_mixin.
- Lemma modality_embed_mixin `{BiEmbed PROP PROP'} :
+ Lemma modality_embed_mixin `{!BiEmbed PROP PROP'} :
modality_mixin (@embed PROP PROP' _)
(MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
Proof.
@@ -43,16 +43,16 @@ Section modalities.
- intros P Q. rewrite /IntoEmbed=> ->. by rewrite embed_intuitionistically_2.
- by intros P Q ->.
Qed.
- Definition modality_embed `{BiEmbed PROP PROP'} :=
+ Definition modality_embed `{!BiEmbed PROP PROP'} :=
Modality _ modality_embed_mixin.
- Lemma modality_plainly_mixin `{BiPlainly PROP} :
+ Lemma modality_plainly_mixin `{!BiPlainly PROP} :
modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
Proof.
split; simpl; split_and?; eauto using equiv_entails_1_2, plainly_intro,
plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
Qed.
- Definition modality_plainly `{BiPlainly PROP} :=
+ Definition modality_plainly `{!BiPlainly PROP} :=
Modality _ modality_plainly_mixin.
Lemma modality_laterN_mixin n :
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index c04c19782..a204beda2 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -146,7 +146,7 @@ Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed.
-Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P ð“Ÿ :
+Global Instance make_monPred_at_bupd `{!BiBUpd PROP} i P ð“Ÿ :
MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|==> P) (|==> ð“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
@@ -430,7 +430,7 @@ Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_objectively. Q
Global Instance frame_monPred_at_subjectively p P ð“¡ ð“ i :
Frame p ð“¡ (∃ i, P i) ð“ → FrameMonPredAt p i ð“¡ (<subj> P) ð“ .
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_subjectively. Qed.
-Global Instance frame_monPred_at_bupd `{BiBUpd PROP} p P ð“¡ ð“ i :
+Global Instance frame_monPred_at_bupd `{!BiBUpd PROP} p P ð“¡ ð“ i :
Frame p ð“¡ (|==> P i) ð“ → FrameMonPredAt p i ð“¡ (|==> P) ð“ .
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_bupd. Qed.
@@ -441,11 +441,11 @@ Proof.
by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
Qed.
-Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ p p' ð“Ÿ ð“Ÿ' Q Q' i :
+Global Instance elim_modal_at_bupd_goal `{!BiBUpd PROP} φ p p' ð“Ÿ ð“Ÿ' Q Q' i :
ElimModal φ p p' ð“Ÿ ð“Ÿ' (|==> Q i) (|==> Q' i) →
ElimModal φ p p' ð“Ÿ ð“Ÿ' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
-Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P ð“Ÿ ð“Ÿ' ð“ ð“ ' i:
+Global Instance elim_modal_at_bupd_hyp `{!BiBUpd PROP} φ p p' P ð“Ÿ ð“Ÿ' ð“ ð“ ' i:
MakeMonPredAt i P 𓟠→
ElimModal φ p p' (|==> ð“Ÿ) ð“Ÿ' ð“ ð“ ' →
ElimModal φ p p' ((|==> P) i) ð“Ÿ' ð“ ð“ '.
@@ -458,18 +458,18 @@ Proof.
by iApply "HP".
Qed.
-Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q i :
+Global Instance add_modal_at_bupd_goal `{!BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I → AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
-Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
+Global Instance from_forall_monPred_at_plainly `{!BiPlainly PROP} i P Φ :
(∀ i, MakeMonPredAt i P (Φ i)) →
FromForall ((■P) i) (λ j, ■(Φ j))%I (to_ident_name idx).
Proof.
rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
by setoid_rewrite HPΦ.
Qed.
-Global Instance into_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
+Global Instance into_forall_monPred_at_plainly `{!BiPlainly PROP} i P Φ :
(∀ i, MakeMonPredAt i P (Φ i)) →
IntoForall ((■P) i) (λ j, ■(Φ j))%I.
Proof.
@@ -493,7 +493,7 @@ Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
Global Instance make_monPred_at_laterN i n P ð“ :
MakeMonPredAt i P ð“ → MakeMonPredAt i (â–·^n P) (â–·^n ð“ ).
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
-Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P ð“Ÿ :
+Global Instance make_monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P ð“Ÿ :
MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|={E1,E2}=> P) (|={E1,E2}=> ð“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
@@ -532,7 +532,7 @@ Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_later. Qed.
Global Instance frame_monPred_at_laterN p n P ð“¡ ð“ i :
Frame p ð“¡ (â–·^n P i) ð“ → FrameMonPredAt p i ð“¡ (â–·^n P) ð“ .
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_laterN. Qed.
-Global Instance frame_monPred_at_fupd `{BiFUpd PROP} E1 E2 p P ð“¡ ð“ i :
+Global Instance frame_monPred_at_fupd `{!BiFUpd PROP} E1 E2 p P ð“¡ ð“ i :
Frame p ð“¡ (|={E1,E2}=> P i) ð“ → FrameMonPredAt p i ð“¡ (|={E1,E2}=> P) ð“ .
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_fupd. Qed.
End bi.
@@ -566,17 +566,17 @@ Implicit Types ð“Ÿ ð“ ð“¡ : PROP.
Implicit Types φ : Prop.
Implicit Types i j : I.
-Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ p p' E1 E2 E3 ð“Ÿ ð“Ÿ' Q Q' i :
+Global Instance elim_modal_at_fupd_goal `{!BiFUpd PROP} φ p p' E1 E2 E3 ð“Ÿ ð“Ÿ' Q Q' i :
ElimModal φ p p' ð“Ÿ ð“Ÿ' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
ElimModal φ p p' ð“Ÿ ð“Ÿ' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
-Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P ð“Ÿ ð“Ÿ' ð“ ð“ ' i :
+Global Instance elim_modal_at_fupd_hyp `{!BiFUpd PROP} φ p p' E1 E2 P ð“Ÿ ð“Ÿ' ð“ ð“ ' i :
MakeMonPredAt i P 𓟠→
ElimModal φ p p' (|={E1,E2}=> ð“Ÿ) ð“Ÿ' ð“ ð“ ' →
ElimModal φ p p' ((|={E1,E2}=> P) i) ð“Ÿ' ð“ ð“ '.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
-Global Instance elim_acc_at_None `{BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' P P'x i :
+Global Instance elim_acc_at_None `{!BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' P P'x i :
(∀ x, MakeEmbed (α x) (α' x)) → (∀ x, MakeEmbed (β x) (β' x)) →
ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x →
ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
@@ -587,7 +587,7 @@ Proof.
- iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
rewrite -Hα -Hβ. iFrame. iIntros (? _) "Hβ". by iApply "Hclose".
Qed.
-Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
+Global Instance elim_acc_at_Some `{!BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
(∀ x, MakeEmbed (α x) (α' x)) →
(∀ x, MakeEmbed (β x) (β' x)) →
(∀ x, MakeEmbed (γ x) (γ' x)) →
@@ -601,7 +601,7 @@ Proof.
rewrite -Hα -Hβ -Hγ. iFrame. iIntros (? _) "Hβ /=". by iApply "Hclose".
Qed.
-Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 ð“Ÿ ð“Ÿ' Q i :
+Global Instance add_modal_at_fupd_goal `{!BiFUpd PROP} E1 E2 ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|={E1,E2}=> Q i) → AddModal ð“Ÿ ð“Ÿ' ((|={E1,E2}=> Q) i).
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2d08f83fe..8a48e4930 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1237,25 +1237,25 @@ Proof.
iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
Qed.
-Lemma test_iSpecialize_bupd `{BiBUpd PROP} A (a : A) (P : A -> PROP) :
+Lemma test_iSpecialize_bupd `{!BiBUpd PROP} A (a : A) (P : A -> PROP) :
(|==> ∀ x, P x) ⊢ |==> P a.
Proof.
iIntros "H". iSpecialize ("H" $! a). done.
Qed.
-Lemma test_iSpecialize_fupd `{BiFUpd PROP} A (a : A) (P : A -> PROP) E1 E2 :
+Lemma test_iSpecialize_fupd `{!BiFUpd PROP} A (a : A) (P : A -> PROP) E1 E2 :
(|={E1, E2}=> ∀ x, P x) ⊢ |={E1, E2}=> P a.
Proof.
iIntros "H". iSpecialize ("H" $! a). done.
Qed.
-Lemma test_iDestruct_and_bupd `{BiBUpd PROP} (P Q : PROP) :
+Lemma test_iDestruct_and_bupd `{!BiBUpd PROP} (P Q : PROP) :
(|==> P ∧ Q) ⊢ |==> P.
Proof.
iIntros "[P _]". done.
Qed.
-Lemma test_iDestruct_and_fupd `{BiFUpd PROP} (P Q : PROP) E1 E2 :
+Lemma test_iDestruct_and_fupd `{!BiFUpd PROP} (P Q : PROP) E1 E2 :
(|={E1, E2}=> P ∧ Q) ⊢ |={E1, E2}=> P.
Proof.
iIntros "[P _]". done.
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 47ec40e25..4309da285 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -101,7 +101,7 @@ Qed.
End tests.
Section printing_tests.
-Context `{!BiFUpd PROP}.
+Context {PROP : bi} `{!BiFUpd PROP}.
(* Working with concrete telescopes: Testing the reduction into normal quantifiers. *)
Lemma acc_elim_test_1 E1 E2 :
--
GitLab