From 9c36e6af517ed266f86819fa50f78da7f2da51c9 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Sun, 11 Sep 2022 22:41:49 +0200
Subject: [PATCH] finish making step-index a typeclass
---
theories/base_logic/algebra.v | 34 ++--
theories/base_logic/bi.v | 68 +++----
theories/base_logic/derived.v | 16 +-
.../base_logic/lib/cancelable_invariants.v | 20 +-
theories/base_logic/lib/fancy_updates.v | 18 +-
theories/base_logic/lib/gen_heap.v | 58 +++---
theories/base_logic/lib/invariants.v | 16 +-
theories/base_logic/lib/iprop.v | 68 +++----
theories/base_logic/lib/na_invariants.v | 24 +--
theories/base_logic/lib/own.v | 22 +--
theories/base_logic/lib/proph_map.v | 24 +--
theories/base_logic/lib/satisfiable.v | 28 +--
theories/base_logic/lib/saved_prop.v | 36 ++--
theories/base_logic/lib/wsat.v | 38 ++--
theories/base_logic/proofmode.v | 4 +-
theories/base_logic/upred.v | 148 +++++++-------
theories/bi/lib/fixpoint.v | 20 +-
theories/bi/lib/fractional.v | 6 +-
theories/proofmode/class_instances.v | 6 +-
.../proofmode/class_instances_embedding.v | 6 +-
.../proofmode/class_instances_internal_eq.v | 22 +--
theories/proofmode/class_instances_later.v | 4 +-
theories/proofmode/class_instances_plainly.v | 2 +-
theories/proofmode/class_instances_updates.v | 2 +-
theories/proofmode/classes.v | 186 +++++++++---------
theories/proofmode/coq_tactics.v | 32 +--
theories/proofmode/environments.v | 58 +++---
theories/proofmode/frame_instances.v | 20 +-
theories/proofmode/ltac_tactics.v | 2 +-
theories/proofmode/modalities.v | 22 +--
theories/proofmode/modality_instances.v | 2 +-
31 files changed, 506 insertions(+), 506 deletions(-)
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 4e7be3a2..2a0d85a9 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -7,18 +7,18 @@ From iris.prelude Require Import options.
Local Coercion uPred_holds : uPred >-> Funclass.
Section upred.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-Lemma prod_validI {A B : cmra SI} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
Proof. by uPred.unseal. Qed.
-Lemma option_validI {A : cmra SI} (mx : option A) :
+Lemma option_validI {A : cmra} (mx : option A) :
✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
Proof. uPred.unseal. by destruct mx. Qed.
-Lemma discrete_fun_validI {A} {B : A → ucmra SI} (g : discrete_fun B) :
+Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
✓ g ⊣⊢ ∀ i, ✓ g i.
Proof. by uPred.unseal. Qed.
@@ -26,7 +26,7 @@ Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1âŒ%Qp.
Proof. rewrite uPred.discrete_valid frac_valid' //. Qed.
Section gmap_ofe.
- Context `{Countable K} {A : ofe SI}.
+ Context `{Countable K} {A : ofe}.
Implicit Types m : gmap K A.
Implicit Types i : K.
@@ -35,7 +35,7 @@ Section gmap_ofe.
End gmap_ofe.
Section gmap_cmra.
- Context `{Countable K} {A : cmra SI}.
+ Context `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
@@ -52,7 +52,7 @@ Section gmap_cmra.
End gmap_cmra.
Section list_ofe.
- Context {A : ofe SI}.
+ Context {A : ofe}.
Implicit Types l : list A.
Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
@@ -60,7 +60,7 @@ Section list_ofe.
End list_ofe.
Section list_cmra.
- Context {A : ucmra SI}.
+ Context {A : ucmra}.
Implicit Types l : list A.
Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
@@ -68,7 +68,7 @@ Section list_cmra.
End list_cmra.
Section excl.
- Context {A : ofe SI}.
+ Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.
@@ -89,7 +89,7 @@ Section excl.
End excl.
Section agree.
- Context {A : ofe SI}.
+ Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
@@ -107,7 +107,7 @@ Section agree.
End agree.
Section csum_ofe.
- Context {A B : ofe SI}.
+ Context {A B : ofe}.
Implicit Types a : A.
Implicit Types b : B.
@@ -125,7 +125,7 @@ Section csum_ofe.
End csum_ofe.
Section csum_cmra.
- Context {A B : cmra SI}.
+ Context {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
@@ -139,7 +139,7 @@ Section csum_cmra.
End csum_cmra.
Section view.
- Context {A: ofe SI} {B: ucmra SI} (rel : view_rel A B).
+ Context {A: ofe} {B: ucmra} (rel : view_rel A B).
Implicit Types a : A.
Implicit Types ag : option (frac * agree A).
Implicit Types b : B.
@@ -204,7 +204,7 @@ Section view.
End view.
Section auth.
- Context {A : ucmra SI}.
+ Context {A : ucmra}.
Implicit Types a b : A.
Implicit Types x y : auth A.
@@ -236,7 +236,7 @@ Section auth.
End auth.
Section excl_auth.
- Context {A : ofe SI}.
+ Context {A : ofe}.
Implicit Types a b : A.
Lemma excl_auth_agreeI a b : ✓ (â—E a â‹… â—¯E b) ⊢ (a ≡ b).
@@ -248,7 +248,7 @@ Section excl_auth.
End excl_auth.
Section gmap_view.
- Context {K : Type} `{Countable K} {V : ofe SI}.
+ Context {K : Type} `{Countable K} {V : ofe}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
Lemma gmap_view_both_validI m k dq v :
@@ -261,7 +261,7 @@ Section gmap_view.
Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
- ✓ ((dq1: dfracR SI) ⋅ dq2) ∧ v1 ≡ v2.
+ ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
Proof.
rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index a7c9be29..65234c9d 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -6,11 +6,11 @@ Import uPred_primitive.
(** BI instances for [uPred], and re-stating the remaining primitive laws in
terms of the BI interface. This file does *not* unseal. *)
-Definition uPred_emp {SI: indexT} {M: ucmra SI} : uPred M := uPred_pure True.
+Definition uPred_emp `{SI: indexT} {M: ucmra} : uPred M := uPred_pure True.
Local Existing Instance entails_po.
-Lemma uPred_bi_mixin {SI: indexT} (M : ucmra SI) :
+Lemma uPred_bi_mixin `{SI: indexT} (M : ucmra) :
BiMixin
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall SI M) (@uPred_exist SI M) uPred_sep uPred_wand
@@ -66,7 +66,7 @@ Proof.
- exact: persistently_and_sep_l_1.
Qed.
-Lemma uPred_bi_later_mixin {SI} (M : ucmra SI) :
+Lemma uPred_bi_later_mixin `{SI: indexT} (M : ucmra) :
BiLaterMixin
uPred_entails uPred_pure uPred_or uPred_impl
(@uPred_forall SI M) uPred_sep uPred_persistently uPred_later.
@@ -82,18 +82,18 @@ Proof.
- exact: later_false_em.
Qed.
-Canonical Structure uPredI {SI} (M : ucmra SI) : bi SI :=
- {| bi_ofe_mixin := ofe_mixin_of SI (uPred M);
+Canonical Structure uPredI `{SI: indexT} (M : ucmra) : bi :=
+ {| bi_ofe_mixin := ofe_mixin_of (uPred M);
bi_bi_mixin := uPred_bi_mixin M;
bi_bi_later_mixin := uPred_bi_later_mixin M |}.
-Global Instance uPred_pure_forall {SI} (M : ucmra SI) : BiPureForall (uPredI M).
+Global Instance uPred_pure_forall `{SI: indexT} (M : ucmra) : BiPureForall (uPredI M).
Proof. exact: @pure_forall_2. Qed.
-Global Instance uPred_later_contractive {SI} (M : ucmra SI) : BiLaterContractive (uPredI M).
+Global Instance uPred_later_contractive `{SI: indexT} (M : ucmra) : BiLaterContractive (uPredI M).
Proof. apply later_contractive. Qed.
-Lemma uPred_internal_eq_mixin {SI} (M : ucmra SI) : BiInternalEqMixin (uPredI M) (@uPred_internal_eq SI M).
+Lemma uPred_internal_eq_mixin `{SI: indexT} (M : ucmra) : BiInternalEqMixin (uPredI M) (@uPred_internal_eq SI M).
Proof.
split.
- exact: internal_eq_ne.
@@ -105,10 +105,10 @@ Proof.
- exact: @later_eq_1.
- exact: @later_eq_2.
Qed.
-Global Instance uPred_internal_eq {SI} (M : ucmra SI) : BiInternalEq (uPredI M) :=
+Global Instance uPred_internal_eq `{SI: indexT} (M : ucmra) : BiInternalEq (uPredI M) :=
{| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.
-Lemma uPred_plainly_mixin {SI} (M : ucmra SI) : BiPlainlyMixin (uPredI M) uPred_plainly.
+Lemma uPred_plainly_mixin `{SI: indexT} (M : ucmra) : BiPlainlyMixin (uPredI M) uPred_plainly.
Proof.
split.
- exact: plainly_ne.
@@ -132,13 +132,13 @@ Proof.
- exact: later_plainly_1.
- exact: later_plainly_2.
Qed.
-Global Instance uPred_plainly {SI} (M : ucmra SI) : BiPlainly (uPredI M) :=
+Global Instance uPred_plainly `{SI: indexT} (M : ucmra) : BiPlainly (uPredI M) :=
{| bi_plainly_mixin := uPred_plainly_mixin M |}.
-Global Instance uPred_prop_ext {SI} (M : ucmra SI) : BiPropExt (uPredI M).
+Global Instance uPred_prop_ext `{SI: indexT} (M : ucmra) : BiPropExt (uPredI M).
Proof. exact: prop_ext_2. Qed.
-Lemma uPred_bupd_mixin {SI} (M : ucmra SI) : BiBUpdMixin (uPredI M) uPred_bupd.
+Lemma uPred_bupd_mixin `{SI: indexT} (M : ucmra) : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
split.
- exact: bupd_ne.
@@ -147,24 +147,24 @@ Proof.
- exact: bupd_trans.
- exact: bupd_frame_r.
Qed.
-Global Instance uPred_bi_bupd {SI} (M : ucmra SI) : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+Global Instance uPred_bi_bupd `{SI: indexT} (M : ucmra) : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
-Global Instance uPred_bi_bupd_plainly {SI} (M : ucmra SI) : BiBUpdPlainly (uPredI M).
+Global Instance uPred_bi_bupd_plainly `{SI: indexT} (M : ucmra) : BiBUpdPlainly (uPredI M).
Proof. exact: bupd_plainly. Qed.
-Global Instance uPred_bi_finite {SI} `{!FiniteIndex SI} (M : ucmra SI): BiFinite (uPredI M).
+Global Instance uPred_bi_finite `{SI: indexT} `{!FiniteIndex SI} (M : ucmra): BiFinite (uPredI M).
Proof.
split.
- intros; apply later_exist_false.
- exact: later_sep_1.
Qed.
-Global Instance uPred_bi_later_or {SI} `{!FiniteBoundedExistential SI} (M : ucmra SI): BiLaterOr (uPredI M).
+Global Instance uPred_bi_later_or `{SI: indexT} `{!FiniteBoundedExistential SI} (M : ucmra): BiLaterOr (uPredI M).
Proof.
split. exact: later_or_2.
Qed.
-Global Instance uPred_bi_timeless {SI} (M : ucmra SI): BiTimeless (uPredI M).
+Global Instance uPred_bi_timeless `{SI: indexT} (M : ucmra): BiTimeless (uPredI M).
Proof.
split.
- exact: pure_timeless.
@@ -172,31 +172,31 @@ Proof.
- intros X; apply: later_exist_timeless.
Qed.
-Global Instance uPred_sat_instance {SI} (M : ucmra SI): Satisfiable (@uPred_sat SI M).
+Global Instance uPred_sat_instance `{SI: indexT} (M : ucmra): Satisfiable (@uPred_sat SI M).
Proof.
split.
- apply uPred_sat_mono.
- apply uPred_sat_elim.
Qed.
-Global Instance uPred_sat_bupd_instance {SI} (M : ucmra SI): SatisfiableBUpd (@uPred_sat SI M).
+Global Instance uPred_sat_bupd_instance `{SI: indexT} (M : ucmra): SatisfiableBUpd (@uPred_sat SI M).
Proof. split. apply uPred_sat_bupd. Qed.
-Global Instance uPred_sat_later_instance {SI} (M : ucmra SI): SatisfiableLater (@uPred_sat SI M).
+Global Instance uPred_sat_later_instance `{SI: indexT} (M : ucmra): SatisfiableLater (@uPred_sat SI M).
Proof. split. apply uPred_sat_later. Qed.
-Global Instance uPred_sat_exists_instance {SI} (M : ucmra SI) {X} `{!TypeExistentialProperty X SI}: SatisfiableExists X (@uPred_sat SI M).
+Global Instance uPred_sat_exists_instance `{SI: indexT} (M : ucmra) {X} `{!TypeExistentialProperty X SI}: SatisfiableExists X (@uPred_sat SI M).
Proof. split. apply uPred_sat_exists, _. Qed.
(** extra BI instances *)
-Global Instance uPred_affine {SI} (M : ucmra SI) : BiAffine (uPredI M) | 0.
+Global Instance uPred_affine `{SI: indexT} (M : ucmra) : BiAffine (uPredI M) | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
Global Hint Immediate uPred_affine : core.
-Global Instance uPred_plainly_exist_1 {SI} (M : ucmra SI) : BiPlainlyExist (uPredI M).
+Global Instance uPred_plainly_exist_1 `{SI: indexT} (M : ucmra) : BiPlainlyExist (uPredI M).
Proof. exact: @plainly_exist_1. Qed.
(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
@@ -204,7 +204,7 @@ Proof. exact: @plainly_exist_1. Qed.
Module uPred.
Section restate.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -214,7 +214,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
Global Instance ownM_ne : NonExpansive (@uPred_ownM SI M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmra SI} : NonExpansive (@uPred_cmra_valid SI M A)
+Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid SI M A)
:= uPred_primitive.cmra_valid_ne.
(** Re-exporting primitive lemmas that are not in any interface *)
@@ -235,28 +235,28 @@ Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe SI} (a1 a2 : A) (b1 b2 : B) :
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
(∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
Proof. exact: uPred_primitive.internal_eq_entails. Qed.
Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof. exact: uPred_primitive.ownM_valid. Qed.
-Lemma cmra_valid_intro {A : cmra SI} P (a : A) : ✓ a → P ⊢ (✓ a).
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-Lemma cmra_valid_elim {A : cmra SI} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra SI} (a : A) : ✓ a ⊢ ■✓ a.
+Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■✓ a.
Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-Lemma cmra_valid_weaken {A : cmra SI} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma discrete_valid {A : cmra SI} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. exact: uPred_primitive.discrete_valid. Qed.
(** This is really just a special case of an entailment
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra SI} (a : A) (b : B) :
+Lemma valid_entails {A B : cmra} (a : A) (b : B) :
(∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
Proof. exact: uPred_primitive.valid_entails. Qed.
@@ -268,7 +268,7 @@ Proof. apply: uPred_primitive.uPred_ownM_timeless. Qed.
Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ âŒ) → φ.
Proof. apply pure_soundness. Qed.
-Lemma internal_eq_soundness {A : ofe SI} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index fc979d4a..205e9fcb 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -9,7 +9,7 @@ Import bi.bi base_logic.bi.uPred.
Module uPred.
Section derived.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -20,11 +20,11 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(** Propers *)
Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM SI M) := ne_proper _.
-Global Instance cmra_valid_proper {A : cmra SI} :
+Global Instance cmra_valid_proper {A : cmra} :
Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid SI M A) := ne_proper _.
(** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmra SI} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
@@ -38,9 +38,9 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM SI M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma plainly_cmra_valid {A : cmra SI} (a : A) : ■✓ a ⊣⊢ ✓ a.
+Lemma plainly_cmra_valid {A : cmra} (a : A) : ■✓ a ⊣⊢ ✓ a.
Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-Lemma intuitionistically_cmra_valid {A : cmra SI} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
Proof.
rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
first by rewrite persistently_elim.
@@ -53,17 +53,17 @@ Proof.
Qed.
(** Timeless instances *)
-Global Instance valid_timeless {A : cmra SI} `{!CmraDiscrete A} (a : A) :
+Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
Timeless (✓ a : uPred M)%I.
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
(** Plainness *)
-Global Instance cmra_valid_plain {A : cmra SI} (a : A) :
+Global Instance cmra_valid_plain {A : cmra} (a : A) :
Plain (✓ a : uPred M)%I.
Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
(** Persistence *)
-Global Instance cmra_valid_persistent {A : cmra SI} (a : A) :
+Global Instance cmra_valid_persistent {A : cmra} (a : A) :
Persistent (✓ a : uPred M)%I.
Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM SI M a).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index a7d47d41..74a59511 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -5,14 +5,14 @@ From iris.base_logic.lib Require Export invariants.
From iris.prelude Require Import options.
Import uPred.
-Class cinvG {SI} Σ := cinv_inG :> inG Σ (fracR SI).
-Definition cinvΣ SI : gFunctors SI := #[GFunctor (fracR SI)].
+Class cinvG `{SI: indexT} Σ := cinv_inG :> inG Σ fracR.
+Definition cinvΣ `{SI: indexT} : gFunctors := #[GFunctor fracR].
-Global Instance subG_cinvΣ {SI} {Σ} : subG (cinvΣ SI) Σ → cinvG Σ.
+Global Instance subG_cinvΣ `{SI: indexT} {Σ} : subG (cinvΣ) Σ → cinvG Σ.
Proof. solve_inG. Qed.
Section defs.
- Context {SI} {Σ : gFunctors SI} `{!invG Σ, !cinvG Σ}.
+ Context `{SI: indexT} {Σ : gFunctors} `{!invG Σ, !cinvG Σ}.
Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
@@ -23,7 +23,7 @@ End defs.
Global Instance: Params (@cinv) 6 := {}.
Section proofs.
- Context {SI} {Σ : gFunctors SI} `{!invG Σ, !cinvG Σ}.
+ Context `{SI: indexT} {Σ : gFunctors} `{!invG Σ, !cinvG Σ}.
Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed.
@@ -108,7 +108,7 @@ Section proofs.
Qed.
(*** Accessors *)
- Lemma cinv_acc_strong `{FiniteBoundedExistential SI} E N γ p P :
+ Lemma cinv_acc_strong `{!FiniteBoundedExistential SI} E N γ p P :
↑N ⊆ E →
cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
▷ P ∗ cinv_own γ p ∗ (∀ E' : coPset, ▷ P ∨ cinv_own γ 1 ={E',↑N ∪ E'}=∗ True)).
@@ -125,7 +125,7 @@ Section proofs.
- iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
Qed.
- Lemma cinv_acc `{FiniteBoundedExistential SI} E N γ p P :
+ Lemma cinv_acc `{!FiniteBoundedExistential SI} E N γ p P :
↑N ⊆ E →
cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
@@ -137,7 +137,7 @@ Section proofs.
Qed.
(*** Other *)
- Lemma cinv_cancel `{FiniteBoundedExistential SI} E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
+ Lemma cinv_cancel `{!FiniteBoundedExistential SI} E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
@@ -147,7 +147,7 @@ Section proofs.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
- Global Instance into_acc_cinv `{FiniteBoundedExistential SI} E N γ P p :
+ Global Instance into_acc_cinv `{!FiniteBoundedExistential SI} E N γ P p :
IntoAcc (X:=unit) (cinv N γ P)
(↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
(λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
@@ -158,4 +158,4 @@ Section proofs.
Qed.
End proofs.
-Typeclasses Opaque cinv_own cinv.
+Global Typeclasses Opaque cinv_own cinv.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 21b44164..f8d6af92 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -7,15 +7,15 @@ From iris.prelude Require Import options.
Export invG.
Import uPred.
-Definition uPred_fupd_def {SI} {Σ: gFunctors SI} `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Definition uPred_fupd_def `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Definition uPred_fupd := uPred_fupd_aux.(unseal).
Global Arguments uPred_fupd {SI Σ _}.
-Lemma uPred_fupd_eq {SI} {Σ: gFunctors SI} `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Lemma uPred_fupd_eq `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
-Lemma uPred_fupd_mixin {SI} {Σ: gFunctors SI} `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
split.
- rewrite uPred_fupd_eq. solve_proper.
@@ -33,13 +33,13 @@ Proof.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
-Global Instance uPred_bi_fupd {SI} {Σ: gFunctors SI} `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
+Global Instance uPred_bi_fupd `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
-Global Instance uPred_bi_bupd_fupd {SI} {Σ: gFunctors SI} `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
+Global Instance uPred_bi_bupd_fupd `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
-Global Instance uPred_bi_fupd_plainly {SI} {Σ: gFunctors SI} `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
+Global Instance uPred_bi_fupd_plainly `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
Proof.
split.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
@@ -60,7 +60,7 @@ Proof.
by iFrame.
Qed.
-Lemma fupd_plain_soundness {SI} {Σ: gFunctors SI} `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
+Lemma fupd_plain_soundness `{SI : indexT} {Σ: gFunctors} `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
(∀ `{Hinv: !invG Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
Proof.
iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
@@ -70,7 +70,7 @@ Proof.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
-Lemma step_fupdN_soundness {SI} {Σ: gFunctors SI} `{!invPreG Σ} φ n :
+Lemma step_fupdN_soundness `{SI : indexT} {Σ: gFunctors} `{!invPreG Σ} φ n :
(∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]â–·=>^n |={⊤,∅}=> ⌜ φ âŒ) →
φ.
Proof.
@@ -88,7 +88,7 @@ Proof.
iNext. by iMod "Hφ".
Qed.
-Lemma step_fupdN_soundness' {SI} {Σ: gFunctors SI} `{!invPreG Σ} φ n :
+Lemma step_fupdN_soundness' `{SI : indexT} {Σ: gFunctors} `{!invPreG Σ} φ n :
(∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]â–·=>^n ⌜ φ âŒ) →
φ.
Proof.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 8e708722..a2732f2e 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -63,13 +63,13 @@ these can be matched up with the invariant namespaces. *)
(** The CMRAs we need, and the global ghost names we are using. *)
-Class gen_heapPreG {SI} (L V : Type) (Σ : gFunctors SI) `{Countable L} := {
- gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO SI V));
- gen_meta_preG_inG :> inG Σ (gmap_viewR L (gnameO SI));
- gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR (positiveO SI)));
+Class gen_heapPreG `{SI: indexT} (L V : Type) (Σ : gFunctors) `{Countable L} := {
+ gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO V));
+ gen_meta_preG_inG :> inG Σ (gmap_viewR L gnameO);
+ gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
}.
-Class gen_heapG {SI} (L V : Type) (Σ : gFunctors SI) `{Countable L} := GenHeapG {
+Class gen_heapG `{SI: indexT} (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG :> gen_heapPreG L V Σ;
gen_heap_name : gname;
gen_meta_name : gname
@@ -78,29 +78,29 @@ Global Arguments GenHeapG {SI} L V Σ {_ _ _} _ _.
Global Arguments gen_heap_name {SI L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {SI L V Σ _ _} _ : assert.
-Definition gen_heapΣ {SI} (L V : Type) `{Countable L} : gFunctors SI := #[
- GFunctor (gmap_viewR L (leibnizO SI V));
- GFunctor (gmap_viewR L (gnameO SI));
- GFunctor (reservation_mapR (agreeR (positiveO SI)))
+Definition gen_heapΣ `{SI: indexT} (L V : Type) `{Countable L} : gFunctors := #[
+ GFunctor (gmap_viewR L (leibnizO V));
+ GFunctor (gmap_viewR L (gnameO));
+ GFunctor (reservation_mapR (agreeR (positiveO)))
].
-Global Instance subG_gen_heapPreG {SI} {Σ: gFunctors SI} {L V} `{Countable L} :
+Global Instance subG_gen_heapPreG `{SI: indexT} {Σ: gFunctors} {L V} `{Countable L} :
subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
Proof. solve_inG. Qed.
Section definitions.
- Context {SI} {Σ: gFunctors SI} `{Countable L, hG : !gen_heapG L V Σ}.
+ Context `{SI: indexT} {Σ: gFunctors} `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m: gmap L gname,
(* The [⊆] is used to avoid assigning ghost information to the locations in
the initial heap (see [gen_heap_init]). *)
⌜ dom m ⊆ dom σ ⌠∧
- own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO SI V))) ∗
- own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L (gnameO SI))).
+ own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) ∗
+ own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L (gnameO))).
Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
- own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO SI V)).
+ own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO V)).
Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
@@ -133,7 +133,7 @@ Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
(at level 20, format "l ↦ v") : bi_scope.
Section gen_heap.
- Context {SI} {Σ: gFunctors SI} {L V} `{Countable L, !gen_heapG L V Σ}.
+ Context `{SI: indexT} {Σ: gFunctors} {L V} `{Countable L, !gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V → iProp Σ.
Implicit Types σ : gmap L V.
@@ -154,12 +154,12 @@ Section gen_heap.
Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
Proof. rewrite mapsto_eq. apply _. Qed.
- Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ (dq: dfracR SI)âŒ%Qp.
+ Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dqâŒ%Qp.
Proof.
rewrite mapsto_eq. iIntros "Hl".
iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
Qed.
- Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ ((dq1: dfracR SI) â‹… dq2) ∧ v1 = v2âŒ.
+ Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 â‹… dq2) ∧ v1 = v2âŒ.
Proof.
rewrite mapsto_eq. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
@@ -174,7 +174,7 @@ Section gen_heap.
Qed.
Lemma mapsto_combine l dq1 dq2 v1 v2 :
- l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{(dq1: dfracR SI) â‹… dq2} v1 ∗ ⌜v1 = v2âŒ.
+ l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 â‹… dq2} v1 ∗ ⌜v1 = v2âŒ.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
@@ -183,7 +183,7 @@ Section gen_heap.
Qed.
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
- ¬ ✓((dq1: dfracR SI) â‹… dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠l2âŒ.
+ ¬ ✓(dq1 â‹… dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠l2âŒ.
Proof.
iIntros (?) "Hl1 Hl2"; iIntros (->).
by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
@@ -315,14 +315,14 @@ End gen_heap.
The key difference to [gen_heap_init] is that the [inG] instances in the new
[gen_heapG] instance are related to the original [gen_heapPreG] instance,
whereas [gen_heap_init] forgets about that relation. *)
-Lemma gen_heap_init_names {SI} {Σ: gFunctors SI} `{Countable L, !gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init_names `{SI: indexT} {Σ: gFunctors} `{Countable L, !gen_heapPreG L V Σ} σ :
⊢ |==> ∃ γh γm : gname,
let hG := GenHeapG L V Σ γh γm in
gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
Proof.
- iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO SI V)))) as (γh) "Hh".
+ iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO V)))) as (γh) "Hh".
{ exact: gmap_view_auth_valid. }
- iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (gnameO SI)))) as (γm) "Hm".
+ iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (gnameO)))) as (γm) "Hm".
{ exact: gmap_view_auth_valid. }
iExists γh, γm.
iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
@@ -332,7 +332,7 @@ Proof.
rewrite right_id_L. done.
Qed.
-Lemma gen_heap_init {SI} {Σ: gFunctors SI} `{Countable L, !gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init `{SI: indexT} {Σ: gFunctors} `{Countable L, !gen_heapPreG L V Σ} σ :
⊢ |==> ∃ _ : gen_heapG L V Σ,
gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
Proof.
@@ -348,17 +348,17 @@ Definition γ_gen_heap_meta : gname := encode "gen_heap.meta".
Definition gen_heap_gnames : coPset := {[ γ_gen_heap; γ_gen_heap_meta ]}.
(* mirrors gen_heapPreG but for type class inference reasons we do not reuse gen_heapPreG *)
-Class gen_heapS {SI} (L V : Type) (Σ : gFunctors SI) `{Countable L} := {
+Class gen_heapS {SI} (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heapS_inG :> inG Σ (authR (gen_heapUR SI L V));
gen_heapS_meta_inG :> inG Σ (authR (gen_metaUR SI L));
gen_heapS_data_inG :> inG Σ (reservation_mapR (agreeR (positiveO SI)))
}.
-Instance gen_heapS_gen_heapG {SI} {Σ : gFunctors SI} `{Countable L} `{gen_heapS SI L V Σ} : gen_heapG L V Σ :=
+Instance gen_heapS_gen_heapG {SI} {Σ : gFunctors} `{Countable L} `{gen_heapS SI L V Σ} : gen_heapG L V Σ :=
GenHeapG _ _ _ _ _ _ _ _ _ γ_gen_heap γ_gen_heap_meta.
-Lemma alloc_gen_heap {SI} {Σ : gFunctors SI} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
+Lemma alloc_gen_heap {SI} {Σ : gFunctors} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
sbi_emp_valid (|==> ∃ γ_gen_heap γ_gen_heap_meta, let H := GenHeapG SI L V _ _ _ _ _ _ γ_gen_heap γ_gen_heap_meta in gen_heap_interp σ)%I.
Proof.
iMod (own_alloc (◠to_gen_heap SI σ)) as (γ_gen_heap) "H1".
@@ -370,7 +370,7 @@ Proof.
iFrame "H1 H2". by rewrite dom_empty_L.
Qed.
-Lemma heap_init_to_bigOp {SI} {Σ : gFunctors SI} `{hG: gen_heapG SI L V Σ} σ:
+Lemma heap_init_to_bigOp {SI} {Σ : gFunctors} `{hG: gen_heapG SI L V Σ} σ:
own (gen_heap_name hG) (◯ (to_gen_heap SI σ)) -∗
[∗ map] i ↦ v ∈ σ, i ↦ v .
Proof.
@@ -390,7 +390,7 @@ Proof.
by iApply IHσ.
Qed.
-Lemma alloc_gen_heap_strong {SI} {Σ : gFunctors SI} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
+Lemma alloc_gen_heap_strong {SI} {Σ : gFunctors} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
sbi_emp_valid (|==> ∃ γ_gen_heap γ_gen_heap_meta, let H := GenHeapG SI L V _ _ _ _ _ _ γ_gen_heap γ_gen_heap_meta in gen_heap_interp σ ∗ [∗ map] i↦v ∈ σ, i ↦ v)%I.
Proof.
iMod (own_alloc (◠to_gen_heap SI σ ⋅ ◯ to_gen_heap SI σ)) as (γ_gen_heap) "(H1&Hfrag)".
@@ -403,7 +403,7 @@ Proof.
- by iApply heap_init_to_bigOp.
Qed.
-Lemma initial_gen_heap {SI} {Σ : gFunctors SI} L V `{Countable L} `{gen_heapS SI L V Σ} (σ: gmap L V):
+Lemma initial_gen_heap {SI} {Σ : gFunctors} L V `{Countable L} `{gen_heapS SI L V Σ} (σ: gmap L V):
initial gen_heap_gnames (gen_heap_interp σ)%I.
Proof.
feed pose proof (initial_alloc γ_gen_heap (◠to_gen_heap SI σ)) as HH.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index f6060212..466ed7f5 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
Import uPred.
(** Semantic Invariants *)
-Definition inv_def {SI} {Σ: gFunctors SI} `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
(□ ∀ E, ⌜↑N ⊆ E⌠→ |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True))%I.
Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv := inv_aux.(unseal).
@@ -17,7 +17,7 @@ Global Instance: Params (@inv) 4 := {}.
(** * Invariants *)
Section inv.
- Context {SI} {Σ: gFunctors SI} `{!invG Σ}.
+ Context `{SI : indexT} {Σ: gFunctors} `{!invG Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types E : coPset.
@@ -97,7 +97,7 @@ Section inv.
Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_eq. apply _. Qed.
- Lemma inv_alter `{FiniteIndex SI} N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
+ Lemma inv_alter `{!FiniteIndex SI} N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
Proof.
rewrite inv_eq. iIntros "#HI #HPQ !>" (E Hsub).
iMod ("HI" $! E Hsub) as "[HP Hclose]".
@@ -132,7 +132,7 @@ Section inv.
rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
Qed.
- Lemma inv_combine `{FiniteIndex SI} N1 N2 N P Q :
+ Lemma inv_combine `{!FiniteIndex SI} N1 N2 N P Q :
N1 ## N2 →
↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
@@ -145,7 +145,7 @@ Section inv.
iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
Qed.
- Lemma inv_combine_dup_l `{FiniteIndex SI} N P Q :
+ Lemma inv_combine_dup_l `{!FiniteIndex SI} N P Q :
□ (P -∗ P ∗ P) -∗
inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
Proof.
@@ -190,16 +190,16 @@ Section inv.
iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed.
- Lemma inv_split_l `{FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P.
+ Lemma inv_split_l `{!FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P.
Proof.
iIntros "#HI". iApply (inv_alter with "HI").
iIntros "!> !> [$ $] $".
Qed.
- Lemma inv_split_r `{FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N Q.
+ Lemma inv_split_r `{!FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N Q.
Proof.
rewrite (comm _ P Q). eapply inv_split_l.
Qed.
- Lemma inv_split `{FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
+ Lemma inv_split `{!FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
Proof.
iIntros "#H".
iPoseProof (inv_split_l with "H") as "$".
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 26e39d12..1606f9a3 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -24,12 +24,12 @@ the agreement CMRA. *)
(** * Locally contractive functors *)
(** The type [gFunctor] bundles a functor from the category of COFEs to the
category of CMRAs with a proof that it is locally contractive. *)
-Structure gFunctor (SI: indexT) := GFunctor {
- gFunctor_F :> rFunctor SI;
+Structure gFunctor `{SI: indexT} := GFunctor {
+ gFunctor_F :> rFunctor;
gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
Global Arguments GFunctor {_} _ {_}.
-Existing Instance gFunctor_map_contractive.
+Global Existing Instance gFunctor_map_contractive.
Add Printing Constructor gFunctor.
(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
@@ -38,16 +38,16 @@ of [gFunctor]s.
Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
alternative way to avoid universe inconsistencies with respect to the universe
monomorphic [list] type. *)
-Definition gFunctors SI := { n : nat & fin n → gFunctor SI }.
+Definition gFunctors `{SI: indexT} := { n : nat & fin n → gFunctor }.
-Definition gid {SI} (Σ : gFunctors SI) := fin (projT1 Σ).
-Definition gFunctors_lookup {SI} (Σ : gFunctors SI) : gid Σ → gFunctor SI := projT2 Σ.
+Definition gid `{SI: indexT} (Σ : gFunctors) := fin (projT1 Σ).
+Definition gFunctors_lookup `{SI: indexT} (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
Definition gname := positive.
-Canonical Structure gnameO SI := leibnizO SI gname.
+Canonical Structure gnameO `{SI: indexT} := leibnizO gname.
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
-Definition iResF {SI} (Σ : gFunctors SI) : urFunctor SI :=
+Definition iResF `{SI: indexT} (Σ : gFunctors) : urFunctor :=
discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).
@@ -55,12 +55,12 @@ Definition iResF {SI} (Σ : gFunctors SI) : urFunctor SI :=
functors, and the append operator on lists of functors. These are used to
compose [gFunctors] out of smaller pieces. *)
Module gFunctors.
- Definition nil {SI} : gFunctors SI := existT 0 (fin_0_inv _).
+ Definition nil `{SI: indexT} : gFunctors := existT 0 (fin_0_inv _).
- Definition singleton {SI} (F : gFunctor SI) : gFunctors SI :=
- existT 1 (fin_S_inv (λ _, gFunctor SI) F (fin_0_inv _)).
+ Definition singleton `{SI: indexT} (F : gFunctor) : gFunctors :=
+ existT 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
- Definition app {SI} (Σ1 Σ2 : gFunctors SI) : gFunctors SI :=
+ Definition app `{SI: indexT} (Σ1 Σ2 : gFunctors) : gFunctors :=
existT (projT1 Σ1 + projT1 Σ2) (fin_add_inv _ (projT2 Σ1) (projT2 Σ2)).
End gFunctors.
@@ -80,7 +80,7 @@ lock invariant.
The contraints to can be expressed using the type class [subG Σ1 Σ2], which
expresses that the functors [Σ1] are contained in [Σ2]. *)
-Class subG {SI} (Σ1 Σ2 : gFunctors SI) := in_subG i :
+Class subG `{SI: indexT} (Σ1 Σ2 : gFunctors) := in_subG i :
{ j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.
(** Avoid trigger happy type class search: this line ensures that type class
@@ -90,21 +90,21 @@ their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
Global Hint Mode subG - ! + : typeclass_instances.
-Lemma subG_inv {SI} (Σ1 Σ2 Σ: gFunctors SI) : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
+Lemma subG_inv `{SI: indexT} (Σ1 Σ2 Σ: gFunctors) : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
Proof.
move=> H; split.
- move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
- move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
Qed.
-Global Instance subG_refl {SI} (Σ: gFunctors SI) : subG Σ Σ.
+Global Instance subG_refl `{SI: indexT} (Σ: gFunctors) : subG Σ Σ.
Proof. move=> i; by exists i. Qed.
-Global Instance subG_app_l {SI} (Σ Σ1 Σ2: gFunctors SI) : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
+Global Instance subG_app_l `{SI: indexT} (Σ Σ1 Σ2: gFunctors) : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
Qed.
-Global Instance subG_app_r {SI} (Σ Σ1 Σ2 : gFunctors SI): subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
+Global Instance subG_app_r `{SI: indexT} (Σ Σ1 Σ2 : gFunctors): subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
@@ -116,50 +116,50 @@ Qed.
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig.
- Parameter iPrePropO : ∀ {SI: indexT}, gFunctors SI → ofe SI.
- Global Declare Instance iPreProp_cofe {SI}{Σ: gFunctors SI} : Cofe (iPrePropO Σ).
+ Parameter iPrePropO : ∀ {SI: indexT}, gFunctors → ofe.
+ Global Declare Instance iPreProp_cofe `{SI: indexT} {Σ: gFunctors} : Cofe (iPrePropO Σ).
- Definition iResUR {SI} (Σ : gFunctors SI) : ucmra SI :=
+ Definition iResUR `{SI: indexT} (Σ : gFunctors) : ucmra :=
discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
- Parameter iProp_unfold: ∀ {SI} {Σ: gFunctors SI}, iPropO Σ -n> iPrePropO Σ.
- Parameter iProp_fold: ∀ {SI} {Σ: gFunctors SI}, iPrePropO Σ -n> iPropO Σ.
- Parameter iProp_fold_unfold: ∀ {SI} {Σ: gFunctors SI} (P : iProp Σ),
+ Parameter iProp_unfold: ∀ `{SI: indexT} {Σ: gFunctors}, iPropO Σ -n> iPrePropO Σ.
+ Parameter iProp_fold: ∀ `{SI: indexT} {Σ: gFunctors}, iPrePropO Σ -n> iPropO Σ.
+ Parameter iProp_fold_unfold: ∀ `{SI: indexT} {Σ: gFunctors} (P : iProp Σ),
iProp_fold (iProp_unfold P) ≡ P.
- Parameter iProp_unfold_fold: ∀ {SI} {Σ: gFunctors SI} (P : iPrePropO Σ),
+ Parameter iProp_unfold_fold: ∀ `{SI: indexT} {Σ: gFunctors} (P : iPrePropO Σ),
iProp_unfold (iProp_fold P) ≡ P.
End iProp_solution_sig.
Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
(* TODO: checkc this *)
- Definition iProp_result {SI} (Σ : gFunctors SI) :
- solution (uPredOF (iResF Σ)) := solver.solution_F _ (uPredOF (iResF Σ)) (uPred_pure True).
- Definition iPrePropO {SI} (Σ : gFunctors SI) : ofe SI := iProp_result Σ.
- Global Instance iPreProp_cofe {SI} {Σ: gFunctors SI} : Cofe (iPrePropO Σ) := _.
+ Definition iProp_result `{SI: indexT} (Σ : gFunctors) :
+ solution (uPredOF (iResF Σ)) := solver.solution_F (uPredOF (iResF Σ)) (uPred_pure True).
+ Definition iPrePropO `{SI: indexT} (Σ : gFunctors) : ofe := iProp_result Σ.
+ Global Instance iPreProp_cofe `{SI: indexT} {Σ: gFunctors} : Cofe (iPrePropO Σ) := _.
- Definition iResUR {SI} (Σ : gFunctors SI) : ucmra SI :=
+ Definition iResUR `{SI: indexT} (Σ : gFunctors) : ucmra :=
discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
- Definition iProp_unfold {SI} {Σ: gFunctors SI} : iPropO Σ -n> iPrePropO Σ :=
+ Definition iProp_unfold `{SI: indexT} {Σ: gFunctors} : iPropO Σ -n> iPrePropO Σ :=
solution_fold _ (iProp_result Σ).
- Definition iProp_fold {SI} {Σ: gFunctors SI} : iPrePropO Σ -n> iPropO Σ := solution_unfold _ _.
- Lemma iProp_fold_unfold {SI} {Σ: gFunctors SI} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
+ Definition iProp_fold `{SI: indexT} {Σ: gFunctors} : iPrePropO Σ -n> iPropO Σ := solution_unfold _ _.
+ Lemma iProp_fold_unfold `{SI: indexT} {Σ: gFunctors} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
Proof. apply @solution_unfold_fold. Qed.
- Lemma iProp_unfold_fold {SI} {Σ: gFunctors SI} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
+ Lemma iProp_unfold_fold `{SI: indexT} {Σ: gFunctors} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
Proof. apply @solution_fold_unfold. Qed.
End iProp_solution.
(** * Properties of the solution to the recursive domain equation *)
-Lemma iProp_unfold_equivI {SI} {Σ: gFunctors SI} (P Q : iProp Σ) :
+Lemma iProp_unfold_equivI `{SI: indexT} {Σ: gFunctors} (P Q : iProp Σ) :
iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
Proof.
rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index b77660e2..adf6352e 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -8,15 +8,15 @@ Import uPred.
Definition na_inv_pool_name := gname.
-Class na_invG {SI} Σ :=
- na_inv_inG :> inG Σ (prodR (coPset_disjR SI) (gset_disjR positive)).
-Definition na_invΣ {SI} : gFunctors SI :=
- #[ GFunctor (constRF (prodR (coPset_disjR SI) (gset_disjR positive))) ].
-Global Instance subG_na_invG {SI} {Σ: gFunctors SI} : subG na_invΣ Σ → na_invG Σ.
+Class na_invG `{SI: indexT} Σ :=
+ na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+Definition na_invΣ `{SI: indexT} : gFunctors :=
+ #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
+Global Instance subG_na_invG `{SI: indexT} {Σ: gFunctors} : subG na_invΣ Σ → na_invG Σ.
Proof. solve_inG. Qed.
Section defs.
- Context {SI} {Σ: gFunctors SI} `{!invG Σ, !na_invG Σ}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ, !na_invG Σ}.
Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
own p (CoPset E, GSet ∅).
@@ -27,10 +27,10 @@ Section defs.
End defs.
Global Instance: Params (@na_inv) 3 := {}.
-Typeclasses Opaque na_own na_inv.
+Global Typeclasses Opaque na_own na_inv.
Section proofs.
- Context {SI} {Σ: gFunctors SI} `{!invG Σ, !na_invG Σ}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ, !na_invG Σ}.
Global Instance na_own_timeless p E : Timeless (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
@@ -76,7 +76,7 @@ Section proofs.
Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
Proof.
iIntros "HP".
- iMod (own_unit (prodUR (coPset_disjUR SI) (gset_disjUR positive)) p) as "Hempty".
+ iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'.
- apply cmra_updateP_id, (reflexivity (R:=eq)).
@@ -92,7 +92,7 @@ Section proofs.
iNext. iLeft. by iFrame.
Qed.
- Lemma na_inv_acc `{FiniteIndex SI} p E F N P :
+ Lemma na_inv_acc `{!FiniteIndex SI} p E F N P :
↑N ⊆ E → ↑N ⊆ F →
na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
(▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
@@ -114,7 +114,7 @@ Section proofs.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
- Global Instance into_acc_na `{FiniteIndex SI} p F E N P :
+ Global Instance into_acc_na `{!FiniteIndex SI} p F E N P :
IntoAcc (X:=unit) (na_inv p N P)
(↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
(λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
@@ -162,7 +162,7 @@ Section proofs.
intros ???. iIntros "HI Hna". iApply (na_inv_acc_open_timeless_weakening with "HI Hna"); auto.
Qed.
- Lemma na_inv_acc_open `{FiniteBoundedExistential SI} p E F N P :
+ Lemma na_inv_acc_open `{!FiniteBoundedExistential SI} p E F N P :
↑N ⊆ E → ↑N ⊆ F →
na_inv p N P -∗ na_own p F ={E}=∗ ▷ (P ∗ na_own p (F∖↑N)
∗ (▷ P ∗ na_own p (F∖↑N) -∗ |={E}=> na_own p F)).
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index bb3ba2e5..655cd325 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -10,7 +10,7 @@ Import uPred.
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
-Class inG {SI} (Σ : gFunctors SI) (A : cmra SI) := InG {
+Class inG `{SI: indexT} (Σ : gFunctors) (A : cmra) := InG {
inG_id : gid Σ;
inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
inG_prf : A = inG_apply (iPropO Σ) _;
@@ -23,7 +23,7 @@ mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
not want Coq to pick one arbitrarily. *)
Global Hint Mode inG - - ! : typeclass_instances.
-Lemma subG_inG {SI} Σ (F : gFunctor SI) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
+Lemma subG_inG `{SI: indexT} Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
@@ -58,19 +58,19 @@ Ltac solve_inG :=
split; (assumption || by apply _).
(** * Definition of the connective [own] *)
-Local Definition inG_unfold {SI} {Σ: gFunctors SI} {A} {i : inG Σ A} :
+Local Definition inG_unfold `{SI: indexT} {Σ: gFunctors} {A} {i : inG Σ A} :
inG_apply i (iPropO Σ) -n> inG_apply i (iPrePropO Σ) :=
rFunctor_map _ (iProp_fold, iProp_unfold).
-Local Definition inG_fold {SI} {Σ: gFunctors SI} {A} {i : inG Σ A} :
+Local Definition inG_fold `{SI: indexT} {Σ: gFunctors} {A} {i : inG Σ A} :
inG_apply i (iPrePropO Σ) -n> inG_apply i (iPropO Σ) :=
rFunctor_map _ (iProp_unfold, iProp_fold).
-Local Definition iRes_singleton {SI} {Σ: gFunctors SI} {A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
+Local Definition iRes_singleton `{SI: indexT} {Σ: gFunctors} {A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
discrete_fun_singleton (inG_id i)
{[ γ := inG_unfold (cmra_transport inG_prf a) ]}.
Global Instance: Params (@iRes_singleton) 4 := {}.
-Local Definition own_def {SI} {Σ: gFunctors SI} `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
+Local Definition own_def `{SI: indexT} {Σ: gFunctors} `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Local Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own := own_aux.(unseal).
@@ -80,7 +80,7 @@ Local Instance: Params (@own) 5 := {}.
(** * Properties about ghost ownership *)
Section global.
-Context {SI} {Σ: gFunctors SI} `{i : !inG Σ A}.
+Context `{SI: indexT} {Σ: gFunctors} `{i : !inG Σ A}.
Implicit Types a : A.
Local Lemma inG_unfold_fold (x : inG_apply i (iPrePropO Σ)) :
@@ -201,7 +201,7 @@ Proof. rewrite !own_eq /own_def. apply _. Qed.
Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
-Lemma later_own `{FiniteIndex SI} γ a : ▷ own γ a -∗ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
+Lemma later_own `{!FiniteIndex SI} γ a : ▷ own γ a -∗ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
Proof.
rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
@@ -305,7 +305,7 @@ Global Arguments own_update {_ _ _} [_] _ _ _ _.
Global Arguments own_update_2 {_ _ _} [_] _ _ _ _ _.
Global Arguments own_update_3 {_ _ _} [_] _ _ _ _ _ _.
-Lemma own_unit {SI} A `{i : !inG Σ (A:ucmra SI)} γ : ⊢ |==> own γ (ε:A).
+Lemma own_unit `{SI: indexT} A `{i : !inG Σ (A:ucmra)} γ : ⊢ |==> own γ (ε:A).
Proof.
rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, discrete_fun_singleton_update_empty.
@@ -319,7 +319,7 @@ Qed.
(** Big op class instances *)
Section big_op_instances.
- Context {SI} {A: ucmra SI} `{!inG Σ A}.
+ Context `{SI: indexT} {A: ucmra} `{!inG Σ A}.
Global Instance own_cmra_sep_homomorphism γ :
WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
@@ -366,7 +366,7 @@ End big_op_instances.
(** Proofmode class instances *)
Section proofmode_instances.
- Context {SI} {Σ: gFunctors SI} `{!inG Σ A}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!inG Σ A}.
Implicit Types a b : A.
Global Instance into_sep_own γ a b1 b2 :
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 18f08d9c..a8e9bee7 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -8,25 +8,25 @@ Local Notation proph_map P V := (gmap P (list V)).
Definition proph_val_list (P V : Type) := list (P * V).
(** The CMRA we need. *)
-Class proph_mapPreG {SI} (P V : Type) (Σ : gFunctors SI) `{Countable P} := {
- proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO SI V))
+Class proph_mapPreG `{SI: indexT} (P V : Type) (Σ : gFunctors) `{Countable P} := {
+ proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V))
}.
-Class proph_mapG {SI} (P V : Type) (Σ : gFunctors SI) `{Countable P} := ProphMapG {
+Class proph_mapG `{SI: indexT} (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
proph_map_inG :> proph_mapPreG P V Σ;
proph_map_name : gname
}.
Global Arguments proph_map_name {_ _ _ _ _ _} _ : assert.
-Definition proph_mapΣ {SI} (P V : Type) `{Countable P} : gFunctors SI :=
- #[GFunctor (gmap_viewR P (listO $ leibnizO SI V))].
+Definition proph_mapΣ `{SI: indexT} (P V : Type) `{Countable P} : gFunctors :=
+ #[GFunctor (gmap_viewR P (listO $ leibnizO V))].
-Global Instance subG_proph_mapPreG {SI} {Σ: gFunctors SI} {P V} `{Countable P} :
+Global Instance subG_proph_mapPreG `{SI: indexT} {Σ: gFunctors} {P V} `{Countable P} :
subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
Proof. solve_inG. Qed.
Section definitions.
- Context {SI} {Σ: gFunctors SI} `{pG : proph_mapG SI P V Σ}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!EqDecision P} `{!Countable P} `{pG : !proph_mapG P V Σ}.
Implicit Types pvs : proph_val_list P V.
Implicit Types R : proph_map P V.
Implicit Types p : P.
@@ -45,10 +45,10 @@ Section definitions.
Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
(∃ R, ⌜proph_resolves_in_list R pvs ∧
dom R ⊆ ps⌠∗
- own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO SI V) 1 R))%I.
+ own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO V) 1 R))%I.
Definition proph_def (p : P) (vs : list V) : iProp Σ :=
- own (proph_map_name pG) (gmap_view_frag (V:=listO $ leibnizO SI V) p (DfracOwn 1) vs).
+ own (proph_map_name pG) (gmap_view_frag (V:=listO $ leibnizO V) p (DfracOwn 1) vs).
Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
Definition proph := proph_aux.(unseal).
@@ -77,7 +77,7 @@ End list_resolves.
The key difference to [proph_map_init] is that the [inG] instances in the new
[proph_mapPreG] instance are related to the original [proph_mapPreG] instance,
whereas [proph_map_init] forgets about that relation. *)
-Lemma proph_map_init_names {SI: indexT} {Σ: gFunctors SI} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
+Lemma proph_map_init_names `{SI: indexT} {Σ: gFunctors} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
⊢ |==> ∃ γ, let H := ProphMapG SI P V Σ _ _ _ γ in proph_map_interp pvs ps.
Proof.
iMod (own_alloc (gmap_view_auth 1 ∅)) as (γ) "Hh".
@@ -86,7 +86,7 @@ Proof.
iPureIntro. done.
Qed.
-Lemma proph_map_init {SI: indexT} {Σ: gFunctors SI} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
+Lemma proph_map_init `{SI: indexT} {Σ: gFunctors} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
⊢ |==> ∃ _ : proph_mapG P V Σ, proph_map_interp pvs ps.
Proof.
iMod (proph_map_init_names pvs ps) as (γ) "H". iModIntro.
@@ -94,7 +94,7 @@ Proof.
Qed.
Section proph_map.
- Context {SI} {Σ: gFunctors SI} `{proph_mapG SI P V Σ}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!EqDecision P} `{!Countable P} `{!proph_mapG P V Σ}.
Implicit Types p : P.
Implicit Types v : V.
Implicit Types vs : list V.
diff --git a/theories/base_logic/lib/satisfiable.v b/theories/base_logic/lib/satisfiable.v
index 8fe85187..5d7b1696 100644
--- a/theories/base_logic/lib/satisfiable.v
+++ b/theories/base_logic/lib/satisfiable.v
@@ -8,7 +8,7 @@ Import uPred.
(* we first lift satisfiability from uPred to iProp *)
-Definition iProp_sat_def {SI: indexT} {Σ: gFunctors SI} := @uPred_primitive.uPred_sat SI (iResUR Σ).
+Definition iProp_sat_def `{SI: indexT} {Σ: gFunctors} := @uPred_primitive.uPred_sat SI (iResUR Σ).
Local Definition iProp_sat_aux : seal (@iProp_sat_def). Proof. by eexists. Qed.
Definition iProp_sat := iProp_sat_aux.(unseal).
Global Arguments iProp_sat {SI Σ} P.
@@ -16,7 +16,7 @@ Local Definition iProp_sat_eq : @iProp_sat = @iProp_sat_def := iProp_sat_aux.(se
Local Instance: Params (@iProp_sat) 2 := {}.
Section iProp_sat.
- Context {SI} {Σ: gFunctors SI}.
+ Context `{SI: indexT} {Σ: gFunctors}.
Global Instance iProp_sat_instance: Satisfiable (@iProp_sat SI Σ).
Proof. rewrite iProp_sat_eq /iProp_sat_def; apply _. Qed.
@@ -42,25 +42,25 @@ End iProp_sat.
(* We develop a validity judgement where we can explicitly control
the ghost names that are allocated *)
-Definition alloc_names_def {SI} {Σ: gFunctors SI} (G: gset gname) (P: iProp Σ): Prop :=
+Definition alloc_names_def `{SI: indexT} {Σ: gFunctors} (G: gset gname) (P: iProp Σ): Prop :=
(∃ m: iResUR Σ, ✓ m ∧ (∀ i, dom (m i) ⊆ G) ∧ (uPred_ownM m ⊢ P)).
Definition alloc_names_aux : seal (@alloc_names_def). by eexists. Qed.
Definition alloc_names := alloc_names_aux.(unseal).
Arguments alloc_names {SI Σ} _ _.
Definition alloc_names_eq : @alloc_names = @alloc_names_def := alloc_names_aux.(seal_eq).
-Instance: Params (@alloc_names) 4 := {}.
+Global Instance: Params (@alloc_names) 4 := {}.
(* we hide the names *)
-Definition alloc {SI} {Σ: gFunctors SI} (P: iProp Σ) := ∃ G, alloc_names G P.
+Definition alloc `{SI: indexT} {Σ: gFunctors} (P: iProp Σ) := ∃ G, alloc_names G P.
-Class Alloc {SI} {Σ: gFunctors SI} (X: Type) (Φ: X → iProp Σ) (φ: Type):=
+Class Alloc `{SI: indexT} {Σ: gFunctors} (X: Type) (Φ: X → iProp Σ) (φ: Type):=
can_alloc: ∀ P, φ → alloc P → ∃ x: X, alloc (P ∗ Φ x).
Global Hint Mode Alloc - - + ! - : typeclass_instances.
Global Arguments can_alloc {SI Σ X} Φ {φ _ _} _ _.
Section alloc.
- Context {SI} {Σ: gFunctors SI}.
+ Context `{SI: indexT} {Σ: gFunctors}.
Lemma alloc_names_empty : alloc_names ∅ (True%I: iProp Σ).
Proof.
@@ -133,7 +133,7 @@ Section alloc.
Qed.
(* derived *)
- Lemma alloc_names_own_fresh G (P: iProp Σ) {A: cmra SI} (a: A) `{!inG Σ A}:
+ Lemma alloc_names_own_fresh G (P: iProp Σ) {A: cmra} (a: A) `{!inG Σ A}:
alloc_names G P → ✓ a → ∃ γ, alloc_names (G ∪ {[γ]}) (P ∗ own γ a).
Proof.
intros Halloc Hv. exists (fresh G).
@@ -148,7 +148,7 @@ Section alloc.
exists ∅. apply alloc_names_empty.
Qed.
- Lemma alloc_fresh_res {A: cmra SI} `{!inG Σ A} (a: A) P:
+ Lemma alloc_fresh_res {A: cmra} `{!inG Σ A} (a: A) P:
✓ a → alloc P → ∃ γ, alloc (P ∗ own γ a).
Proof.
intros Hv [G Halloc].
@@ -176,7 +176,7 @@ Section alloc.
Proof. intros [G ?]; by eapply alloc_names_iProp_sat. Qed.
(* this instance can be used to allocate some ghost state *)
- Global Instance alloc_gname_inst {A: cmra SI} `{!inG Σ A} (a: A):
+ Global Instance alloc_gname_inst {A: cmra} `{!inG Σ A} (a: A):
Alloc gname (λ γ, own γ a) (✓ a).
Proof.
intros ???; by eapply alloc_fresh_res.
@@ -203,11 +203,11 @@ End alloc.
(* we create a notion of satisfiability which includes invariant masks *)
-Class SatisfiableAtFupd {SI} {Σ: gFunctors SI} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
+Class SatisfiableAtFupd `{SI: indexT} {Σ: gFunctors} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
sat_fupd E1 E2 P: sat_at E1 (|={E1, E2}=> P)%I → sat_at E2 P
}.
-Class SatisfiableAt {SI} {Σ: gFunctors SI} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
+Class SatisfiableAt `{SI: indexT} {Σ: gFunctors} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
sat_at_satisfiable E:> Satisfiable (sat_at E);
sat_at_bupd E:> SatisfiableBUpd (sat_at E);
sat_at_later E:> SatisfiableLater (sat_at E);
@@ -218,7 +218,7 @@ Notation SatisfiableAtExists X sat_at := (∀ E, SatisfiableExists X (sat_at E))
(* there is a canonical satisfiability instance for every notion of satisfiable *)
Section canonical_sat_at.
- Context {SI} {Σ: gFunctors SI} `{!invG Σ} {sat: iProp Σ → Prop} `{!Satisfiable sat} `{!SatisfiableBUpd sat} `{!SatisfiableLater sat}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ} {sat: iProp Σ → Prop} `{!Satisfiable sat} `{!SatisfiableBUpd sat} `{!SatisfiableLater sat}.
Definition sat_at E := (sat_frame (sat := sat) (wsat ∗ ownE E)%I).
@@ -244,7 +244,7 @@ Notation iProp_sat_at := (sat_at (sat := iProp_sat)).
(* framing preserves SatisfiableAtFUpd *)
Section sat_at_frame.
- Context {SI} {Σ: gFunctors SI} `{!invG Σ} {sat_at: coPset → iProp Σ → Prop}.
+ Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ} {sat_at: coPset → iProp Σ → Prop}.
Definition sat_at_frame F E P := sat_frame (sat := sat_at E) F P.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 30e7975e..8406b13d 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -8,25 +8,25 @@ Import uPred.
(* "Saved anything" -- this can give you saved propositions, saved predicates,
saved whatever-you-like. *)
-Class savedAnythingG {SI : indexT} (Σ : gFunctors SI) (F : oFunctor SI) := SavedAnythingG {
+Class savedAnythingG `{SI : indexT} (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
-Definition savedAnythingΣ {SI : indexT} (F : oFunctor SI) `{!oFunctorContractive F} : gFunctors SI :=
+Definition savedAnythingΣ `{SI : indexT} (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
#[ GFunctor (agreeRF F) ].
-Global Instance subG_savedAnythingΣ {SI Σ} {F : oFunctor SI} `{!oFunctorContractive F} :
+Global Instance subG_savedAnythingΣ `{SI : indexT} {Σ} {F : oFunctor} `{!oFunctorContractive F} :
subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
Proof. solve_inG. Qed.
-Definition saved_anything_own {SI} {Σ: gFunctors SI} {F} `{!savedAnythingG Σ F}
+Definition saved_anything_own `{SI : indexT} {Σ: gFunctors} {F} `{!savedAnythingG Σ F}
(γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
own γ (to_agree x).
-Typeclasses Opaque saved_anything_own.
+Global Typeclasses Opaque saved_anything_own.
Global Instance: Params (@saved_anything_own) 5 := {}.
Section saved_anything.
- Context {SI} {Σ: gFunctors SI} {F} `{!savedAnythingG Σ F}.
+ Context `{SI : indexT} {Σ: gFunctors} {F} `{!savedAnythingG Σ F}.
Implicit Types x y : oFunctor_apply F (iPropO Σ).
Implicit Types γ : gname.
@@ -66,27 +66,27 @@ End saved_anything.
Notation savedPropG Σ := (savedAnythingG Σ (▶ (∙ _))).
Notation savedPropΣ := (savedAnythingΣ (▶ (∙ _))).
-Definition saved_prop_own {SI} {Σ : gFunctors SI} `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+Definition saved_prop_own `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
saved_anything_own (F := ▶ (∙ _)) γ (Next P).
-Instance saved_prop_own_contractive {SI} {Σ : gFunctors SI} `{!savedPropG Σ} γ :
+Global Instance saved_prop_own_contractive `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} γ :
Contractive (saved_prop_own γ).
Proof. solve_contractive. Qed.
-Lemma saved_prop_alloc_strong {SI} {Σ : gFunctors SI} `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
+Lemma saved_prop_alloc_strong `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
pred_infinite I →
⊢ |==> ∃ γ, ⌜I γ⌠∗ saved_prop_own γ P.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
-Lemma saved_prop_alloc_cofinite {SI} {Σ : gFunctors SI} `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+Lemma saved_prop_alloc_cofinite `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
⊢ |==> ∃ γ, ⌜γ ∉ G⌠∗ saved_prop_own γ P.
Proof. iApply saved_anything_alloc_cofinite. Qed.
-Lemma saved_prop_alloc `{Σ : gFunctors SI} `{!savedPropG Σ} (P: iProp Σ) :
+Lemma saved_prop_alloc `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (P: iProp Σ) :
⊢ |==> ∃ γ, saved_prop_own γ P.
Proof. iApply saved_anything_alloc. Qed.
-Lemma saved_prop_agree `{Σ : gFunctors SI} `{!savedPropG Σ} γ P Q :
+Lemma saved_prop_agree `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} γ P Q :
saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
Proof.
iIntros "HP HQ". iApply later_equivI.
@@ -97,10 +97,10 @@ Qed.
Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ (∙ _))).
Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ (∙ _))).
-Definition saved_pred_own `{Σ : gFunctors SI} `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
+Definition saved_pred_own `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
saved_anything_own (F := A -d> ▶ (∙ _)) γ (OfeMor Next ∘ Φ).
-Global Instance saved_pred_own_contractive `{Σ : gFunctors SI} `{!savedPredG Σ A} γ :
+Global Instance saved_pred_own_contractive `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} γ :
Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).
Proof.
(* TODO: fix this once f_contractive is fixed *)
@@ -109,21 +109,21 @@ Proof.
intros ??. by apply H.
Qed.
-Lemma saved_pred_alloc_strong `{Σ : gFunctors SI} `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_strong `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
pred_infinite I →
⊢ |==> ∃ γ, ⌜I γ⌠∗ saved_pred_own γ Φ.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
-Lemma saved_pred_alloc_cofinite `{Σ : gFunctors SI} `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_cofinite `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
⊢ |==> ∃ γ, ⌜γ ∉ G⌠∗ saved_pred_own γ Φ.
Proof. iApply saved_anything_alloc_cofinite. Qed.
-Lemma saved_pred_alloc `{Σ : gFunctors SI} `{!savedPredG Σ A} (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (Φ : A → iProp Σ) :
⊢ |==> ∃ γ, saved_pred_own γ Φ.
Proof. iApply saved_anything_alloc. Qed.
(* We put the `x` on the outside to make this lemma easier to apply. *)
-Lemma saved_pred_agree `{Σ : gFunctors SI} `{!savedPredG Σ A} γ Φ Ψ x :
+Lemma saved_pred_agree `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} γ Φ Ψ x :
saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
Proof.
unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 55ba24a5..ba2c8959 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -8,55 +8,55 @@ From iris.prelude Require Import options.
exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
Module invG.
- Class invPreG {SI} (Σ : gFunctors SI) : Set := WsatPreG {
+ Class invPreG `{SI : indexT} (Σ : gFunctors) : Set := WsatPreG {
inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
- enabled_inPreG :> inG Σ (coPset_disjR SI);
+ enabled_inPreG :> inG Σ (coPset_disjR);
disabled_inPreG :> inG Σ (gset_disjR positive);
}.
- Class invG {SI} (Σ : gFunctors SI) : Set := InvG {
+ Class invG `{SI : indexT} (Σ : gFunctors) : Set := InvG {
inv_inG :> invPreG Σ;
invariant_name : gname;
enabled_name : gname;
disabled_name : gname;
}.
- Definition invΣ (SI: indexT) : gFunctors SI :=
- #[GFunctor (gmap_viewRF positive (laterOF (idOF SI)));
- GFunctor (coPset_disjR SI);
+ Definition invΣ `{SI : indexT} : gFunctors :=
+ #[GFunctor (gmap_viewRF positive (laterOF idOF));
+ GFunctor (coPset_disjR);
GFunctor (gset_disjR positive)].
- Global Instance subG_invΣ {SI} {Σ: gFunctors SI} : subG (invΣ SI) Σ → invPreG Σ.
+ Global Instance subG_invΣ `{SI : indexT} {Σ: gFunctors} : subG (invΣ) Σ → invPreG Σ.
Proof. solve_inG. Qed.
End invG.
Import invG.
-Definition invariant_unfold {SI} {Σ: gFunctors SI} (P : iProp Σ) : later (iProp Σ) :=
+Definition invariant_unfold `{SI : indexT} {Σ: gFunctors} (P : iProp Σ) : later (iProp Σ) :=
Next P.
-Definition ownI {SI} {Σ: gFunctors SI} `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
Global Arguments ownI {_ _ _} _ _%I.
-Typeclasses Opaque ownI.
+Global Typeclasses Opaque ownI.
Global Instance: Params (@invariant_unfold) 2 := {}.
Global Instance: Params (@ownI) 4 := {}.
-Definition ownE {SI} {Σ: gFunctors SI} `{!invG Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (E : coPset) : iProp Σ :=
own enabled_name (CoPset E).
-Typeclasses Opaque ownE.
+Global Typeclasses Opaque ownE.
Global Instance: Params (@ownE) 4 := {}.
-Definition ownD {SI} {Σ: gFunctors SI} `{!invG Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (E : gset positive) : iProp Σ :=
own disabled_name (GSet E).
-Typeclasses Opaque ownD.
+Global Typeclasses Opaque ownD.
Global Instance: Params (@ownD) 4 := {}.
-Definition wsat {SI} {Σ: gFunctors SI} `{!invG Σ} : iProp Σ :=
+Definition wsat `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : iProp Σ :=
locked (∃ I : gmap positive (iProp Σ),
own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
[∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
Section wsat.
-Context {SI} {Σ: gFunctors SI} `{!invG Σ}.
+Context `{SI : indexT} {Σ: gFunctors} `{!invG Σ}.
Implicit Types P : iProp Σ.
(* Invariants *)
@@ -70,7 +70,7 @@ Proof. rewrite /ownI. apply _. Qed.
Lemma ownE_empty : ⊢ |==> ownE ∅.
Proof.
rewrite /bi_emp_valid.
- by rewrite (own_unit (coPset_disjUR SI) enabled_name).
+ by rewrite (own_unit coPset_disjUR enabled_name).
Qed.
Lemma ownE_op E1 E2 : E1 ## E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
@@ -183,7 +183,7 @@ Qed.
End wsat.
(* Allocation of an initial wolibrld *)
-Lemma wsat_alloc_strong {SI: indexT} {Σ: gFunctors SI} `{!invPreG Σ} :
+Lemma wsat_alloc_strong {SI: indexT} {Σ: gFunctors} `{!invPreG Σ} :
⊢ |==> ∃ γI γE γD : gname, let H := InvG _ _ _ γI γE γD in wsat ∗ ownE ⊤.
Proof.
iIntros.
@@ -197,7 +197,7 @@ Proof.
Qed.
-Lemma wsat_alloc {SI: indexT} {Σ: gFunctors SI} `{!invPreG Σ} :
+Lemma wsat_alloc {SI: indexT} {Σ: gFunctors} `{!invPreG Σ} :
bi_emp_valid (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
Proof.
iIntros. iMod wsat_alloc_strong as (γI γE γD) "H". iModIntro.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index a36fa1d1..b6eca5ef 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -7,14 +7,14 @@ Import base_logic.bi.uPred.
(* Setup of the proof mode *)
Section class_instances.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
Implicit Types P Q R : uPred M.
Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
@IntoPure SI (uPredI M) (✓ a) (✓ a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
-Global Instance from_pure_cmra_valid {A : cmra SI} (a : A) :
+Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
@FromPure SI (uPredI M) false (✓ a) (✓ a).
Proof.
rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index d95a2177..afa5f6f3 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -102,8 +102,8 @@ This completes the proof.
*)
-Record uPred {SI: indexT} (M : ucmra SI) : Type := UPred {
- uPred_holds : SI → M → Prop;
+Record uPred `{SI: indexT} (M : ucmra) : Type := UPred {
+ uPred_holds : index → M → Prop;
uPred_mono n1 n2 x1 x2 :
uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ⪯ n1 → uPred_holds n2 x2
@@ -118,15 +118,15 @@ Add Printing Constructor uPred.
Global Instance: Params (@uPred_holds) 4 := {}.
Section cofe.
- Context {SI: indexT} {M : ucmra SI}.
+ Context `{SI: indexT} {M : ucmra}.
Inductive uPred_equiv' (P Q : uPred M) : Prop :=
{ uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
Local Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
- Inductive uPred_dist' (n : SI) (P Q : uPred M) : Prop :=
+ Inductive uPred_dist' (n : index) (P Q : uPred M) : Prop :=
{ uPred_in_dist : ∀ n' x, n' ⪯ n → ✓{n'} x → P n' x ↔ Q n' x }.
- Local Instance uPred_dist : Dist SI (uPred M) := uPred_dist'.
- Definition uPred_ofe_mixin : OfeMixin SI (uPred M).
+ Local Instance uPred_dist : Dist (uPred M) := uPred_dist'.
+ Definition uPred_ofe_mixin : OfeMixin (uPred M).
Proof.
split.
- intros P Q; split.
@@ -137,10 +137,10 @@ Section cofe.
+ by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
+ intros P Q Q' HP HQ; split=> i x ??.
by trans (Q i x);[apply HP|apply HQ].
- - intros α β P Q HPQ Hpre; split=> i x ??; apply HPQ; last by eauto.
+ - intros α β P Q HPQ Hpre; split=> i x ??; apply HPQ; last by eauto.
right; eapply index_le_lt_trans; eauto.
Qed.
- Canonical Structure uPredO : ofe SI := Ofe (uPred M) uPred_ofe_mixin.
+ Canonical Structure uPredO : ofe := Ofe (uPred M) uPred_ofe_mixin.
Program Definition uPred_compl : chain uPredO → uPredO := λ c,
{| uPred_holds n x := ∀ n', n' ⪯ n → ✓{n'} x → c n' n' x |}.
@@ -159,8 +159,8 @@ Section cofe.
- eapply cmra_includedN_le=>//; eauto with index.
- done.
Qed.
- Lemma uPred_bcompl'_ne α (c d : bchain uPredO α) (β : SI):
- (∀ (γ : SI) (Hγ : γ ≺ α), c γ Hγ ≡{β}≡ d γ Hγ) →
+ Lemma uPred_bcompl'_ne α (c d : bchain uPredO α) (β : index):
+ (∀ (γ : index) (Hγ : γ ≺ α), c γ Hγ ≡{β}≡ d γ Hγ) →
uPred_bcompl' α c ≡{β}≡ uPred_bcompl' α d.
Proof.
intros Hne; split=> i x Hiβ Hv; split.
@@ -180,7 +180,7 @@ Section cofe.
Next Obligation.
intros α Hα c; split=>i x Hiα Hv.
etrans; [|unshelve by symmetry; apply (bchain_cauchy α c)]; last by eapply index_le_lt_trans; eauto.
- split=>H'; [by apply H'|]. intros n' Hn' Hin' H.
+ split=>H'; [by apply H'|]. intros n' Hn' Hin' H.
unshelve eapply (bchain_cauchy α c n' i); [by eauto using index_le_lt_trans | by eauto | by eauto | by eauto | ].
by eapply uPred_mono.
Qed.
@@ -196,7 +196,7 @@ Section cofe.
Global Program Instance truncatable : ProtoTruncatable uPredO :=
{
- proto_trunc α := λne a, uPred_bcompl' (index_succ _ α) (bchain_const a (index_succ _ α) );
+ proto_trunc α := λne a, uPred_bcompl' (index_succ α) (bchain_const a (index_succ α) );
}.
Next Obligation.
intros α α' x y Heq. by apply uPred_bcompl'_ne.
@@ -220,21 +220,21 @@ Section cofe.
End cofe.
Global Arguments uPredO {_} _.
-Global Instance uPred_ne {SI} {M: ucmra SI} (P : uPred M) n : Proper (dist n ==> iff) (P n).
+Global Instance uPred_ne `{SI: indexT} {M: ucmra} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
Qed.
-Global Instance uPred_proper {SI} {M: ucmra SI} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
+Global Instance uPred_proper `{SI: indexT} {M: ucmra} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
-Lemma uPred_holds_ne {SI} {M: ucmra SI} (P Q : uPred M) n1 n2 x :
+Lemma uPred_holds_ne `{SI: indexT} {M: ucmra} (P Q : uPred M) n1 n2 x :
P ≡{n2}≡ Q → n2 ⪯ n1 → ✓{n2} x → Q n1 x → P n2 x.
Proof.
intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
Qed.
(* Equivalence to the definition of uPred in the appendix. *)
-Lemma uPred_alt {SI: indexT} {M : ucmra SI} (P: SI → M → Prop) :
+Lemma uPred_alt `{SI: indexT} {M : ucmra} (P: index → M → Prop) :
(∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ⪯ n1 → P n2 x2) ↔
( (∀ x n1 n2, n2 ⪯ n1 → P n1 x → P n2 x) (* Pointwise down-closed *)
∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ⪯ n → P m x1 ↔ P m x2) (* Non-expansive *)
@@ -251,30 +251,30 @@ Proof.
Qed.
(** functor *)
-Program Definition uPred_map {SI: indexT} {M1 M2 : ucmra SI} (f : M2 -n> M1)
+Program Definition uPred_map `{SI: indexT} {M1 M2 : ucmra} (f : M2 -n> M1)
`{!CmraMorphism f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
-Global Instance uPred_map_ne {SI: indexT} {M1 M2 : ucmra SI} (f : M2 -n> M1)
+Global Instance uPred_map_ne `{SI: indexT} {M1 M2 : ucmra} (f : M2 -n> M1)
`{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
intros x1 x2 Hx; split=> n' y ??.
split; apply Hx; auto using cmra_morphism_validN.
Qed.
-Lemma uPred_map_id {SI} {M : ucmra SI} (P : uPred M): uPred_map cid P ≡ P.
+Lemma uPred_map_id `{SI: indexT} {M : ucmra} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split=> n x ?. Qed.
-Lemma uPred_map_compose {SI} {M1 M2 M3 : ucmra SI} (f : M1 -n> M2) (g : M2 -n> M3)
+Lemma uPred_map_compose `{SI: indexT} {M1 M2 M3 : ucmra} (f : M1 -n> M2) (g : M2 -n> M3)
`{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
Proof. by split=> n x Hx. Qed.
-Lemma uPred_map_ext {SI} {M1 M2 : ucmra SI} (f g : M1 -n> M2)
+Lemma uPred_map_ext `{SI: indexT} {M1 M2 : ucmra} (f g : M1 -n> M2)
`{!CmraMorphism f} `{!CmraMorphism g}:
(∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredO_map {SI} {M1 M2 : ucmra SI} (f : M2 -n> M1) `{!CmraMorphism f} :
+Definition uPredO_map `{SI: indexT} {M1 M2 : ucmra} (f : M2 -n> M1) `{!CmraMorphism f} :
uPredO M1 -n> uPredO M2 := OfeMor (uPred_map f : uPredO M1 → uPredO M2).
-Lemma uPredO_map_ne {SI} {M1 M2 : ucmra SI} (f g : M2 -n> M1)
+Lemma uPredO_map_ne `{SI: indexT} {M1 M2 : ucmra} (f g : M2 -n> M1)
`{!CmraMorphism f, !CmraMorphism g} n :
f ≡{n}≡ g → uPredO_map f ≡{n}≡ uPredO_map g.
Proof.
@@ -282,7 +282,7 @@ Proof.
rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)).
Qed.
-Program Definition uPredOF {SI} (F : urFunctor SI) : oFunctor SI := {|
+Program Definition uPredOF `{SI: indexT} (F : urFunctor) : oFunctor := {|
oFunctor_car A B := uPredO (urFunctor_car F B A);
oFunctor_map A1 A2 B1 B2 fg := uPredO_map (urFunctor_map F (fg.2, fg.1))
|}.
@@ -299,7 +299,7 @@ Next Obligation.
apply uPred_map_ext=>y; apply urFunctor_map_compose.
Qed.
-Instance uPredOF_contractive {SI} (F: urFunctor SI) :
+Global Instance uPredOF_contractive `{SI: indexT} (F: urFunctor) :
urFunctorContractive F → oFunctorContractive (uPredOF F).
Proof.
intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredO_map_ne, urFunctor_map_contractive.
@@ -307,12 +307,12 @@ Proof.
Qed.
(** logical entailement *)
-Inductive uPred_entails {SI} {M: ucmra SI} (P Q : uPred M) : Prop :=
+Inductive uPred_entails `{SI: indexT} {M: ucmra} (P Q : uPred M) : Prop :=
{ uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
Global Hint Resolve uPred_mono : uPred_def.
(** logical connectives *)
-Program Definition uPred_pure_def {SI} {M: ucmra SI} (φ : Prop) : uPred M :=
+Program Definition uPred_pure_def `{SI: indexT} {M: ucmra} (φ : Prop) : uPred M :=
{| uPred_holds n x := φ |}.
Solve Obligations with done.
Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
@@ -321,7 +321,7 @@ Global Arguments uPred_pure {SI M}.
Definition uPred_pure_eq :
@uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
-Program Definition uPred_and_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_and_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x ∧ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
@@ -329,7 +329,7 @@ Definition uPred_and := uPred_and_aux.(unseal).
Global Arguments uPred_and {SI M}.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
-Program Definition uPred_or_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_or_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x ∨ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
@@ -337,7 +337,7 @@ Definition uPred_or := uPred_or_aux.(unseal).
Global Arguments uPred_or {SI M}.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
-Program Definition uPred_impl_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_impl_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
x ≼ x' → n' ⪯ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Next Obligation.
@@ -351,7 +351,7 @@ Global Arguments uPred_impl {SI M}.
Definition uPred_impl_eq :
@uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
-Program Definition uPred_forall_def {SI} {M: ucmra SI} {A} (Ψ : A → uPred M) : uPred M :=
+Program Definition uPred_forall_def `{SI: indexT} {M: ucmra} {A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := ∀ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
@@ -360,7 +360,7 @@ Global Arguments uPred_forall {SI M A}.
Definition uPred_forall_eq :
@uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
-Program Definition uPred_exist_def {SI} {M: ucmra SI} {A} (Ψ : A → uPred M) : uPred M :=
+Program Definition uPred_exist_def `{SI: indexT} {M: ucmra} {A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := ∃ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
@@ -368,7 +368,7 @@ Definition uPred_exist := uPred_exist_aux.(unseal).
Global Arguments uPred_exist {SI M A}.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
-Program Definition uPred_internal_eq_def {SI} {M: ucmra SI} {A : ofe SI} (a1 a2 : A) : uPred M :=
+Program Definition uPred_internal_eq_def `{SI: indexT} {M: ucmra} {A : ofe} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
@@ -377,7 +377,7 @@ Global Arguments uPred_internal_eq {SI M A}.
Definition uPred_internal_eq_eq:
@uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
-Program Definition uPred_sep_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_sep_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Next Obligation.
intros SI M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
@@ -389,12 +389,12 @@ Definition uPred_sep := uPred_sep_aux.(unseal).
Global Arguments uPred_sep {SI M}.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
-Program Definition uPred_wand_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_wand_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
n' ⪯ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Next Obligation.
intros SI M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in *.
- eapply uPred_mono with n3 (x1 â‹… x3); last reflexivity; first eapply HPQ; first by etrans.
+ eapply uPred_mono with n3 (x1 â‹… x3); last reflexivity; first eapply HPQ; first by etrans.
all: eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
@@ -406,7 +406,7 @@ Definition uPred_wand_eq :
(* Equivalently, this could be `∀ y, P n y`. That's closer to the intuition
of "embedding the step-indexed logic in Iris", but the two are equivalent
because Iris is afine. The following is easier to work with. *)
-Program Definition uPred_plainly_def {SI} {M: ucmra SI} (P : uPred M) : uPred M :=
+Program Definition uPred_plainly_def `{SI: indexT} {M: ucmra} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
@@ -415,7 +415,7 @@ Global Arguments uPred_plainly {SI M}.
Definition uPred_plainly_eq :
@uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
-Program Definition uPred_persistently_def {SI} {M: ucmra SI} (P : uPred M) : uPred M :=
+Program Definition uPred_persistently_def `{SI: indexT} {M: ucmra} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
Solve Obligations with naive_solver eauto using uPred_mono, @cmra_core_monoN.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
@@ -424,14 +424,14 @@ Global Arguments uPred_persistently {SI M}.
Definition uPred_persistently_eq :
@uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
-Program Definition uPred_later_def {SI} {M: ucmra SI} (P : uPred M) : uPred M :=
+Program Definition uPred_later_def `{SI: indexT} {M: ucmra} (P : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n', n' ≺ n → P n' x |}.
Next Obligation.
intros SI M P n1 n2 x1 x2 H1 H2 Hle n' Hlt; simpl in *.
- eapply uPred_mono; first eapply H1.
- - eauto using index_lt_le_trans.
+ eapply uPred_mono; first eapply H1.
+ - eauto using index_lt_le_trans.
- eauto using cmra_includedN_le.
- - reflexivity.
+ - reflexivity.
Qed.
Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
Definition uPred_later := uPred_later_aux.(unseal).
@@ -439,7 +439,7 @@ Global Arguments uPred_later {SI M}.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
-Program Definition uPred_ownM_def {SI} {M: ucmra SI} (a : M) : uPred M :=
+Program Definition uPred_ownM_def `{SI: indexT} {M: ucmra} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
Next Obligation.
intros SI M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn.
@@ -451,7 +451,7 @@ Global Arguments uPred_ownM {SI M}.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
-Program Definition uPred_cmra_valid_def {SI} {M: ucmra SI} {A : cmra SI} (a : A) : uPred M :=
+Program Definition uPred_cmra_valid_def `{SI: indexT} {M: ucmra} {A : cmra} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
@@ -460,7 +460,7 @@ Global Arguments uPred_cmra_valid {SI M A}.
Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
-Program Definition uPred_bupd_def {SI} {M: ucmra SI} (Q : uPred M) : uPred M :=
+Program Definition uPred_bupd_def `{SI: indexT} {M: ucmra} (Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ k yf,
k ⪯ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
Next Obligation.
@@ -492,7 +492,7 @@ Ltac unseal :=
rewrite !unseal_eqs /=.
Section primitive.
-Context {SI: indexT} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -571,7 +571,7 @@ Lemma impl_ne :
NonExpansive2 (@uPred_impl SI M).
Proof.
intros n P P' HP Q Q' HQ; split=> x n' ??.
- unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP;
+ unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP;
match goal with |- _ ⪯ _ => first [reflexivity| by etrans] | _ => by auto end.
Qed.
@@ -588,10 +588,10 @@ Lemma wand_ne :
Proof.
intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
apply HQ, HPQ, HP;
- match goal with |- _ ⪯ _ => try reflexivity; by etrans | _ => by eauto using cmra_validN_op_r end.
+ match goal with |- _ ⪯ _ => try reflexivity; by etrans | _ => by eauto using cmra_validN_op_r end.
Qed.
-Lemma internal_eq_ne (A : ofe SI) :
+Lemma internal_eq_ne (A : ofe) :
NonExpansive2 (@uPred_internal_eq SI M A).
Proof.
intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
@@ -637,7 +637,7 @@ Proof.
by rewrite (dist_le _ _ _ _ Ha).
Qed.
-Lemma cmra_valid_ne {A : cmra SI} :
+Lemma cmra_valid_ne {A : cmra} :
NonExpansive (@uPred_cmra_valid SI M A).
Proof.
intros n a b Ha; unseal; split=> n' x ? /=.
@@ -648,9 +648,9 @@ Lemma bupd_ne : NonExpansive (@uPred_bupd SI M).
Proof.
intros n P Q HPQ.
unseal; split=> n' x; split; intros HP k yf ??;
- destruct (HP k yf) as (x'&?&?); match goal with |- ∃ _ , _ => idtac | _ => by auto end.
+ destruct (HP k yf) as (x'&?&?); match goal with |- ∃ _ , _ => idtac | _ => by auto end.
all: exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
- all: by etrans.
+ all: by etrans.
Qed.
(** Introduction and elimination rules *)
@@ -830,25 +830,25 @@ Lemma later_plainly_2 P : ■▷ P ⊢ ▷ ■P.
Proof. by unseal. Qed.
(** Internal equality *)
-Lemma internal_eq_refl {A : ofe SI} P (a : A) : P ⊢ (a ≡ a).
+Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : ofe SI} a b (Ψ : A → uPred M) :
+Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → uPred M) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
-Lemma fun_ext {A} {B : A → ofe SI} (g1 g2 : discrete_fun B) :
+Lemma fun_ext {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
(∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
Proof. by unseal. Qed.
-Lemma sig_eq {A : ofe SI} (P : A → Prop) (x y : sigO P) :
+Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
Proof. by unseal. Qed.
-Lemma later_eq_1 {A : ofe SI} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofe SI} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
Proof. by unseal. Qed.
-Lemma discrete_eq_1 {A : ofe SI} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
+Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
Proof.
unseal=> ?. split=> n x ?. by apply (discrete_iff n).
Qed.
@@ -857,7 +857,7 @@ Qed.
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe SI} (a1 a2 : A) (b1 b2 : B) :
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
(∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
@@ -909,7 +909,7 @@ Proof.
Qed.
Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
-Lemma later_ownM `{FI: FiniteIndex SI} a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Lemma later_ownM `{FI: !FiniteIndex SI} a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
Proof.
unseal; split=> -n x /= ? Hax.
destruct (finite_index n) as [->|[m ->]].
@@ -937,23 +937,23 @@ Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof.
unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
Qed.
-Lemma cmra_valid_intro {A : cmra SI} P (a : A) : ✓ a → P ⊢ (✓ a).
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmra SI} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto using index_zero_minimum. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra SI} (a : A) : ✓ a ⊢ ■✓ a.
+Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■✓ a.
Proof. by unseal. Qed.
-Lemma cmra_valid_weaken {A : cmra SI} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-Lemma discrete_valid {A : cmra SI} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
(** This is really just a special case of an entailment
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra SI} (a : A) (b : B) :
+Lemma valid_entails {A B : cmra} (a : A) (b : B) :
(∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
@@ -963,7 +963,7 @@ instance of [siProp] soundness in the future. *)
Lemma pure_soundness φ : (True ⊢ ⌜ φ âŒ) → φ.
Proof. unseal=> -[H]. by apply (H zero ε); eauto using ucmra_unit_validN. Qed.
-Lemma internal_eq_soundness {A : ofe SI} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
Proof.
unseal=> -[H]. apply equiv_dist=> n.
by apply (H n ε); eauto using ucmra_unit_validN.
@@ -973,13 +973,13 @@ Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
Proof.
unseal=> -[HP]; split=> n x Hx _.
apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
- apply (HP (index_succ _ n)); eauto using ucmra_unit_validN.
+ apply (HP (index_succ n)); eauto using ucmra_unit_validN.
constructor.
Qed.
(* satisfiabiity for uPred *)
Definition uPred_sat (P: uPred M) :=
- ∀ n: SI, ∃ x: M, ✓{n} x ∧ P n x.
+ ∀ n: index, ∃ x: M, ✓{n} x ∧ P n x.
Lemma uPred_sat_intro: uPred_sat True.
Proof.
@@ -1030,7 +1030,7 @@ Qed.
(* the finite rules for BiFinite *)
-Lemma later_exist_false `{FI: FiniteIndex SI} {A} (Φ : A → uPred M) :
+Lemma later_exist_false `{FI: !FiniteIndex SI} {A} (Φ : A → uPred M) :
(▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
Proof.
unseal; split=> -n x Hv /= H; eauto.
@@ -1040,7 +1040,7 @@ Proof.
intros; eauto using uPred_mono.
Qed.
-Lemma later_sep_1 `{FI: FiniteIndex SI} P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
+Lemma later_sep_1 `{FI: !FiniteIndex SI} P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
Proof.
unseal; split=> n x ? //= H.
destruct (finite_index n) as [->|[m ->]]; eauto.
@@ -1052,7 +1052,7 @@ Proof.
Qed.
(* the later or rule for BiLaterOr *)
-Lemma later_or_2 `{FBE: FiniteBoundedExistential SI} (P Q: uPred M):
+Lemma later_or_2 `{FBE: !FiniteBoundedExistential SI} (P Q: uPred M):
▷ (P ∨ Q) ⊢ ▷ P ∨ ▷ Q.
Proof.
unseal; split=> -n x Hv /= H; eauto.
@@ -1070,7 +1070,7 @@ Definition timeless (P: uPred M) := ▷ P ⊢ ▷ False ∨ P.
Lemma timeless_alt P: (timeless P) ↔ ((▷ False → P) ⊢ P).
Proof.
unfold timeless; unseal; split; intros [H]; split=> n x Hv //= HP; simpl in *.
- - induction n as [n IH] using (well_founded_ind (index_lt_wf SI)).
+ - induction n as [n IH] using (well_founded_ind (index_lt_wf)).
destruct (index_lt_dec_minimum n) as [H'|[m ?]]; eauto.
edestruct H; eauto.
intros; eapply IH; eauto using cmra_validN_le, index_le_lt_trans.
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index ffcdb254..16ee4510 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -5,34 +5,34 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
-Class BiMonoPred {SI} {PROP : bi SI} {A : ofe SI} (F : (A → PROP) → (A → PROP)) := {
+Class BiMonoPred `{SI: indexT} {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) := {
bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
Global Arguments bi_mono_pred {_ _ _ _ _} _ _.
Local Existing Instance bi_mono_pred_ne.
-Definition bi_least_fixpoint {SI} {PROP : bi SI} {A : ofe SI}
+Definition bi_least_fixpoint `{SI: indexT} {PROP : bi} {A : ofe}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
tc_opaque (∀ Φ : A -n> PROP, <pers> (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
Global Arguments bi_least_fixpoint : simpl never.
-Definition bi_greatest_fixpoint {SI} {PROP : bi SI} {A : ofe SI}
+Definition bi_greatest_fixpoint `{SI: indexT} {PROP : bi} {A : ofe}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
tc_opaque (∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
Global Arguments bi_greatest_fixpoint : simpl never.
-Global Instance least_fixpoint_ne {SI} {PROP : bi SI} {A : ofe SI} n :
+Global Instance least_fixpoint_ne `{SI: indexT} {PROP : bi} {A : ofe} n :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
dist n ==> dist n) bi_least_fixpoint.
Proof. solve_proper. Qed.
-Global Instance least_fixpoint_proper {SI} {PROP : bi SI} {A : ofe SI} :
+Global Instance least_fixpoint_proper `{SI: indexT} {PROP : bi} {A : ofe} :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
(≡) ==> (≡)) bi_least_fixpoint.
Proof. solve_proper. Qed.
Section least.
- Context {SI} {PROP : bi SI} {A : ofe SI} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+ Context `{SI: indexT} {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
Proof using Type*.
@@ -74,7 +74,7 @@ Section least.
Qed.
End least.
-Lemma greatest_fixpoint_ne_outer {SI} {PROP : bi SI} {A : ofe SI}
+Lemma greatest_fixpoint_ne_outer `{SI: indexT} {PROP : bi} {A : ofe}
(F1 : (A → PROP) → (A → PROP)) (F2 : (A → PROP) → (A → PROP)):
(∀ Φ x n, F1 Φ x ≡{n}≡ F2 Φ x) → ∀ x1 x2 n,
x1 ≡{n}≡ x2 → bi_greatest_fixpoint F1 x1 ≡{n}≡ bi_greatest_fixpoint F2 x2.
@@ -83,17 +83,17 @@ Proof.
do 3 f_equiv; last solve_proper. repeat f_equiv. apply HF.
Qed.
-Global Instance greatest_fixpoint_ne {SI} {PROP : bi SI} {A : ofe SI} n :
+Global Instance greatest_fixpoint_ne `{SI: indexT} {PROP : bi} {A : ofe} n :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
dist n ==> dist n) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
-Global Instance greatest_fixpoint_proper {SI} {PROP : bi SI} {A : ofe SI} :
+Global Instance greatest_fixpoint_proper `{SI: indexT} {PROP : bi} {A : ofe} :
Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
(≡) ==> (≡)) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
Section greatest.
- Context {SI} {PROP : bi SI} {A : ofe SI} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+ Context `{SI: indexT} {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
Lemma greatest_fixpoint_unfold_1 x :
bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x.
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 8a18fdc6..94c4f08e 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -2,11 +2,11 @@ From iris.bi Require Export bi.
From iris.proofmode Require Import classes class_instances.
From iris.prelude Require Import options.
-Class Fractional {SI} {PROP : bi SI} (Φ : Qp → PROP) :=
+Class Fractional `{SI: indexT} {PROP : bi} (Φ : Qp → PROP) :=
fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
Arguments Fractional {_ _} _%I : simpl never.
-Class AsFractional {SI} {PROP : bi SI} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
+Class AsFractional `{SI: indexT} {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
as_fractional : P ⊣⊢ Φ q;
as_fractional_fractional :> Fractional Φ
}.
@@ -20,7 +20,7 @@ allow [q] to be an evar. *)
Global Hint Mode AsFractional - - - + - : typeclass_instances.
Section fractional.
- Context {SI} {PROP : bi SI}.
+ Context `{SI: indexT} {PROP : bi}.
Implicit Types P Q : PROP.
Implicit Types Φ : Qp → PROP.
Implicit Types q : Qp.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 22d45400..4795bb92 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -12,7 +12,7 @@ algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
by [refine], which otherwise causes TC search to fail. Such unshelved goals are
created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
[?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
-Lemma from_assumption_exact {SI} {PROP : bi SI} p (P : PROP) : FromAssumption p P P.
+Lemma from_assumption_exact `{SI: indexT} {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Global Hint Extern 0 (FromAssumption _ _ _) =>
notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
@@ -21,13 +21,13 @@ Global Hint Extern 0 (FromAssumption _ _ _) =>
(** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
enable the better unification algorithm.
See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
-Lemma from_exist_exist {SI} {PROP : bi SI} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
+Lemma from_exist_exist `{SI: indexT} {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Hint Extern 0 (FromExist _ _) =>
notypeclasses refine (from_exist_exist _) : typeclass_instances.
Section class_instances.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
Implicit Types P Q R : PROP.
Implicit Types mP : option PROP.
diff --git a/theories/proofmode/class_instances_embedding.v b/theories/proofmode/class_instances_embedding.v
index 644b3d10..c2dcfe83 100644
--- a/theories/proofmode/class_instances_embedding.v
+++ b/theories/proofmode/class_instances_embedding.v
@@ -7,13 +7,13 @@ Import bi.
instance is not used when there is no embedding between [PROP] and [PROP']. The
first [`{BiEmbed PROP PROP'}] is not considered as a premise by Coq TC search
mechanism because the rest of the hypothesis is dependent on it. *)
-Global Instance as_emp_valid_embed {SI} {PROP PROP': bi SI} `{!BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
+Global Instance as_emp_valid_embed `{SI: indexT} {PROP PROP': bi} `{!BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
BiEmbed PROP PROP' →
AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
Section class_instances_embedding.
-Context {SI} {PROP PROP': bi SI} `{!BiEmbed PROP PROP'}.
+Context `{SI: indexT} {PROP PROP': bi} `{!BiEmbed PROP PROP'}.
Implicit Types P Q R : PROP.
Global Instance into_pure_embed P φ :
@@ -152,7 +152,7 @@ Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
Global Instance into_internal_eq_embed
`{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
- {A : ofe SI} (x y : A) (P : PROP) :
+ {A : ofe} (x y : A) (P : PROP) :
IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
diff --git a/theories/proofmode/class_instances_internal_eq.v b/theories/proofmode/class_instances_internal_eq.v
index d226c821..3a3b5d46 100644
--- a/theories/proofmode/class_instances_internal_eq.v
+++ b/theories/proofmode/class_instances_internal_eq.v
@@ -5,23 +5,23 @@ From iris.prelude Require Import options.
Import bi.
Section class_instances_internal_eq.
-Context {SI} {PROP: bi SI} `{!BiInternalEq PROP}.
+Context `{SI: indexT} {PROP: bi} `{!BiInternalEq PROP}.
Implicit Types P Q R : PROP.
-Global Instance from_pure_internal_eq {A : ofe SI} (a b : A) :
+Global Instance from_pure_internal_eq {A : ofe} (a b : A) :
@FromPure SI PROP false (a ≡ b) (a ≡ b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
-Global Instance into_pure_eq {A : ofe SI} (a b : A) :
+Global Instance into_pure_eq {A : ofe} (a b : A) :
Discrete a → @IntoPure SI PROP (a ≡ b) (a ≡ b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
-Global Instance from_modal_Next {A : ofe SI} (x y : A) :
+Global Instance from_modal_Next {A : ofe} (x y : A) :
FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
(▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
Proof. by rewrite /FromModal /= later_equivI. Qed.
-Global Instance into_laterN_Next {A : ofe SI} only_head n n' (x y : A) :
+Global Instance into_laterN_Next {A : ofe} only_head n n' (x y : A) :
NatCancel n 1 n' 0 →
IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
@@ -29,22 +29,22 @@ Proof.
move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
Qed.
-Global Instance into_internal_eq_internal_eq {A : ofe SI} (x y : A) :
+Global Instance into_internal_eq_internal_eq {A : ofe} (x y : A) :
@IntoInternalEq SI PROP _ A (x ≡ y) x y.
Proof. by rewrite /IntoInternalEq. Qed.
-Global Instance into_internal_eq_affinely {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_affinely {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_intuitionistically {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_intuitionistically {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (□ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofe SI} (x y : A) P :
+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 SI} (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 SI} (x y : A) P :
+Global Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
End class_instances_internal_eq.
\ No newline at end of file
diff --git a/theories/proofmode/class_instances_later.v b/theories/proofmode/class_instances_later.v
index f9915fcd..f77465ac 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
Import bi.
Section class_instances_later.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
Implicit Types P Q R : PROP.
(** FromAssumption *)
@@ -338,7 +338,7 @@ Global Instance into_later_intuitionistically n P Q :
IntoLaterN false n P Q → IntoLaterN false n (□ P) (□ Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_intuitionistically_2. Qed.
(* FIXME: currently depends on BiAffine because of laterN_absorbingly *)
-Global Instance into_later_absorbingly `{BiAffine SI PROP} n P Q :
+Global Instance into_later_absorbingly `{!BiAffine PROP} n P Q :
IntoLaterN false n P Q → IntoLaterN false n (<absorb> P) (<absorb> Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
Global Instance into_later_persistently n P Q :
diff --git a/theories/proofmode/class_instances_plainly.v b/theories/proofmode/class_instances_plainly.v
index 72d2410b..30064237 100644
--- a/theories/proofmode/class_instances_plainly.v
+++ b/theories/proofmode/class_instances_plainly.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
Import bi.
Section class_instances_plainly.
-Context {SI} {PROP: bi SI} `{!BiPlainly PROP}.
+Context `{SI: indexT} {PROP: bi} `{!BiPlainly PROP}.
Implicit Types P Q R : PROP.
Global Instance from_assumption_plainly_l_true P Q :
diff --git a/theories/proofmode/class_instances_updates.v b/theories/proofmode/class_instances_updates.v
index 57cf1540..c85ce47f 100644
--- a/theories/proofmode/class_instances_updates.v
+++ b/theories/proofmode/class_instances_updates.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
Import bi.
Section class_instances_updates.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
Implicit Types P Q R : PROP.
Global Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index edf0e79c..d7199bc5 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -5,25 +5,25 @@ From iris.proofmode Require Export ident_name modalities.
From iris.prelude Require Import options.
Import bi.
-Class FromAssumption {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class FromAssumption `{SI: indexT} {PROP : bi} (p : bool) (P Q : PROP) :=
from_assumption : □?p P ⊢ Q.
Global Arguments FromAssumption {_ _} _ _%I _%I : simpl never.
Global Arguments from_assumption {_ _} _ _%I _%I {_}.
Global Hint Mode FromAssumption - + + - - : typeclass_instances.
-Class KnownLFromAssumption {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class KnownLFromAssumption `{SI: indexT} {PROP : bi} (p : bool) (P Q : PROP) :=
knownl_from_assumption :> FromAssumption p P Q.
Global Arguments KnownLFromAssumption {_ _} _ _%I _%I : simpl never.
Global Arguments knownl_from_assumption {_ _} _ _%I _%I {_}.
Global Hint Mode KnownLFromAssumption - + + ! - : typeclass_instances.
-Class KnownRFromAssumption {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class KnownRFromAssumption `{SI: indexT} {PROP : bi} (p : bool) (P Q : PROP) :=
knownr_from_assumption :> FromAssumption p P Q.
Global Arguments KnownRFromAssumption {_ _} _ _%I _%I : simpl never.
Global Arguments knownr_from_assumption {_ _} _ _%I _%I {_}.
Global Hint Mode KnownRFromAssumption - + + - ! : typeclass_instances.
-Class IntoPure {SI} {PROP : bi SI} (P : PROP) (φ : Prop) :=
+Class IntoPure `{SI: indexT} {PROP : bi} (P : PROP) (φ : Prop) :=
into_pure : P ⊢ ⌜φâŒ.
Global Arguments IntoPure {_ _} _%I _%type_scope : simpl never.
Global Arguments into_pure {_ _} _%I _%type_scope {_}.
@@ -49,9 +49,9 @@ once, and use [IntoPureT] in any instance like [into_exist_and_pure].
TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
to be finished and merged someday. *)
-Class IntoPureT {SI} {PROP : bi SI} (P : PROP) (φ : Type) :=
+Class IntoPureT `{SI: indexT} {PROP : bi} (P : PROP) (φ : Type) :=
into_pureT : ∃ ψ : Prop, φ = ψ ∧ IntoPure P ψ.
-Lemma into_pureT_hint {SI} {PROP : bi SI} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
+Lemma into_pureT_hint `{SI: indexT} {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
Proof. by exists φ. Qed.
Global Hint Extern 0 (IntoPureT _ _) =>
notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
@@ -65,27 +65,27 @@ the spatial context should be empty or not.
Note that the Boolean [a] is not needed for the (dual) [IntoPure] class, because
there we can just ask that [P] is [Affine]. *)
-Class FromPure {SI} {PROP : bi SI} (a : bool) (P : PROP) (φ : Prop) :=
+Class FromPure `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
from_pure : <affine>?a ⌜φ⌠⊢ P.
Global Arguments FromPure {_ _} _ _%I _%type_scope : simpl never.
Global Arguments from_pure {_ _} _ _%I _%type_scope {_}.
Global Hint Mode FromPure - + - ! - : typeclass_instances.
-Class FromPureT {SI} {PROP : bi SI} (a : bool) (P : PROP) (φ : Type) :=
+Class FromPureT `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure a P ψ.
-Lemma from_pureT_hint {SI} {PROP : bi SI} (a : bool) (P : PROP) (φ : Prop) :
+Lemma from_pureT_hint `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
FromPure a P φ → FromPureT a P φ.
Proof. by exists φ. Qed.
Global Hint Extern 0 (FromPureT _ _ _) =>
notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
-Class IntoInternalEq {SI} {PROP : bi SI} `{!BiInternalEq PROP} {A : ofe SI} (P : PROP) (x y : A) :=
+Class IntoInternalEq `{SI: indexT} {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (P : PROP) (x y : A) :=
into_internal_eq : P ⊢ x ≡ y.
Global Arguments IntoInternalEq {_ _ _ _} _%I _%type_scope _%type_scope : simpl never.
Global Arguments into_internal_eq {_ _ _ _} _%I _%type_scope _%type_scope {_}.
Global Hint Mode IntoInternalEq - + - - ! - - : typeclass_instances.
-Class IntoPersistent {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class IntoPersistent `{SI: indexT} {PROP : bi} (p : bool) (P Q : PROP) :=
into_persistent : <pers>?p P ⊢ <pers> Q.
Global Arguments IntoPersistent {_ _} _ _%I _%I : simpl never.
Global Arguments into_persistent {_ _} _ _%I _%I {_}.
@@ -107,7 +107,7 @@ can define an instance [FromModal modality_id (N P) P]. Defining such an
instance only imposes the proof obligation [P ⊢ N P]. Examples of such
modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
[bi_absorbingly]. *)
-Class FromModal {SI} {PROP1 PROP2 : bi SI} {A}
+Class FromModal `{SI: indexT} {PROP1 PROP2 : bi} {A}
(M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
from_modal : M Q ⊢ P.
Global Arguments FromModal {_ _ _ _} _ _%I _%I _%I : simpl never.
@@ -118,7 +118,7 @@ Global Hint Mode FromModal - - + - - - ! - : typeclass_instances.
proposition [Q].
The input is [Q] and the output is [P]. *)
-Class FromAffinely {SI} {PROP : bi SI} (P Q : PROP) :=
+Class FromAffinely `{SI: indexT} {PROP : bi} (P Q : PROP) :=
from_affinely : <affine> Q ⊢ P.
Global Arguments FromAffinely {_ _} _%I _%I : simpl never.
Global Arguments from_affinely {_ _} _%I _%I {_}.
@@ -128,7 +128,7 @@ Global Hint Mode FromAffinely - + - ! : typeclass_instances.
the proposition [Q].
The input is [Q] and the output is [P]. *)
-Class IntoAbsorbingly {SI} {PROP : bi SI} (P Q : PROP) :=
+Class IntoAbsorbingly `{SI: indexT} {PROP : bi} (P Q : PROP) :=
into_absorbingly : P ⊢ <absorb> Q.
Global Arguments IntoAbsorbingly {_ _} _%I _%I.
Global Arguments into_absorbingly {_ _} _%I _%I {_}.
@@ -143,87 +143,87 @@ Global Hint Mode IntoAbsorbingly - + - ! : typeclass_instances.
hypothesis).
- Instantiate the premise of the wand or implication. *)
-Class IntoWand {SI} {PROP : bi SI} (p q : bool) (R P Q : PROP) :=
+Class IntoWand `{SI: indexT} {PROP : bi} (p q : bool) (R P Q : PROP) :=
into_wand : □?p R ⊢ □?q P -∗ Q.
Global Arguments IntoWand {_ _} _ _ _%I _%I _%I : simpl never.
Global Arguments into_wand {_ _} _ _ _%I _%I _%I {_}.
Global Hint Mode IntoWand - + + + ! - - : typeclass_instances.
-Class IntoWand' {SI} {PROP : bi SI} (p q : bool) (R P Q : PROP) :=
+Class IntoWand' `{SI: indexT} {PROP : bi} (p q : bool) (R P Q : PROP) :=
into_wand' : IntoWand p q R P Q.
Global Arguments IntoWand' {_ _} _ _ _%I _%I _%I : simpl never.
Global Hint Mode IntoWand' - + + + ! ! - : typeclass_instances.
Global Hint Mode IntoWand' - + + + ! - ! : typeclass_instances.
-Class FromWand {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
+Class FromWand `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
Global Arguments FromWand {_ _} _%I _%I _%I : simpl never.
Global Arguments from_wand {_ _} _%I _%I _%I {_}.
Global Hint Mode FromWand - + ! - - : typeclass_instances.
-Class FromImpl {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
+Class FromImpl `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
Global Arguments FromImpl {_ _} _%I _%I _%I : simpl never.
Global Arguments from_impl {_ _} _%I _%I _%I {_}.
Global Hint Mode FromImpl - + ! - - : typeclass_instances.
-Class FromSep {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
+Class FromSep `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
Global Arguments FromSep {_ _} _%I _%I _%I : simpl never.
Global Arguments from_sep {_ _} _%I _%I _%I {_}.
Global Hint Mode FromSep - + ! - - : typeclass_instances.
Global Hint Mode FromSep - + - ! ! : typeclass_instances. (* For iCombine *)
-Class FromAnd {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
+Class FromAnd `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
Global Arguments FromAnd {_ _} _%I _%I _%I : simpl never.
Global Arguments from_and {_ _} _%I _%I _%I {_}.
Global Hint Mode FromAnd - + ! - - : typeclass_instances.
Global Hint Mode FromAnd - + - ! ! : typeclass_instances. (* For iCombine *)
-Class IntoAnd {SI} {PROP : bi SI} (p : bool) (P Q1 Q2 : PROP) :=
+Class IntoAnd `{SI: indexT} {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
Global Arguments IntoAnd {_ _} _ _%I _%I _%I : simpl never.
Global Arguments into_and {_ _} _ _%I _%I _%I {_}.
Global Hint Mode IntoAnd - + + ! - - : typeclass_instances.
-Class IntoSep {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :=
+Class IntoSep `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :=
into_sep : P ⊢ Q1 ∗ Q2.
Global Arguments IntoSep {_ _} _%I _%I _%I : simpl never.
Global Arguments into_sep {_ _} _%I _%I _%I {_}.
Global Hint Mode IntoSep - + ! - - : typeclass_instances.
-Class FromOr {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
+Class FromOr `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
Global Arguments FromOr {_ _} _%I _%I _%I : simpl never.
Global Arguments from_or {_ _} _%I _%I _%I {_}.
Global Hint Mode FromOr - + ! - - : typeclass_instances.
-Class IntoOr {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.
+Class IntoOr `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.
Global Arguments IntoOr {_ _} _%I _%I _%I : simpl never.
Global Arguments into_or {_ _} _%I _%I _%I {_}.
Global Hint Mode IntoOr - + ! - - : typeclass_instances.
-Class FromExist {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :=
+Class FromExist `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
from_exist : (∃ x, Φ x) ⊢ P.
Global Arguments FromExist {_ _ _} _%I _%I : simpl never.
Global Arguments from_exist {_ _ _} _%I _%I {_}.
Global Hint Mode FromExist - + - ! - : typeclass_instances.
-Class IntoExist {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
+Class IntoExist `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
into_exist : P ⊢ ∃ x, Φ x.
Global Arguments IntoExist {_ _ _} _%I _%I _ : simpl never.
Global Arguments into_exist {_ _ _} _%I _%I _ {_}.
Global Hint Mode IntoExist - + - ! - - : typeclass_instances.
-Class IntoForall {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :=
+Class IntoForall `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
into_forall : P ⊢ ∀ x, Φ x.
Global Arguments IntoForall {_ _ _} _%I _%I : simpl never.
Global Arguments into_forall {_ _ _} _%I _%I {_}.
Global Hint Mode IntoForall - + - ! - : typeclass_instances.
-Class FromForall {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
+Class FromForall `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
from_forall : (∀ x, Φ x) ⊢ P.
Global Arguments FromForall {_ _ _} _%I _%I _ : simpl never.
Global Arguments from_forall {_ _ _} _%I _%I _ {_}.
Global Hint Mode FromForall - + - ! - - : typeclass_instances.
-Class IsExcept0 {SI} {PROP : bi SI} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
+Class IsExcept0 `{SI: indexT} {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
Global Arguments IsExcept0 {_ _} _%I : simpl never.
Global Arguments is_except_0 {_ _} _%I {_}.
Global Hint Mode IsExcept0 - + ! : typeclass_instances.
@@ -247,7 +247,7 @@ transformed from [|={E1,E3}=> Q] into [|={E2,E3}=> Q], and the resulting
hypothesis is moved into the spatial context (regardless of where it was
originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
modality, would have a side-condition [φ] on the masks. *)
-Class ElimModal {SI} {PROP : bi SI} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
+Class ElimModal `{SI: indexT} {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.
Global Arguments ElimModal {_ _} _ _ _ _%I _%I _%I _%I : simpl never.
Global Arguments elim_modal {_ _} _ _ _ _%I _%I _%I _%I {_}.
@@ -255,13 +255,13 @@ Global Hint Mode ElimModal - + - ! - ! - ! - : typeclass_instances.
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
-Class AddModal {SI} {PROP : bi SI} (P P' : PROP) (Q : PROP) :=
+Class AddModal `{SI: indexT} {PROP : bi} (P P' : PROP) (Q : PROP) :=
add_modal : P ∗ (P' -∗ Q) ⊢ Q.
Global Arguments AddModal {_ _} _%I _%I _%I : simpl never.
Global Arguments add_modal {_ _} _%I _%I _%I {_}.
Global Hint Mode AddModal - + - ! ! : typeclass_instances.
-Lemma add_modal_id {SI} {PROP : bi SI} (P Q : PROP) : AddModal P P Q.
+Lemma add_modal_id `{SI: indexT} {PROP : bi} (P Q : PROP) : AddModal P P Q.
Proof. by rewrite /AddModal wand_elim_r. Qed.
(** We use the classes [IsCons] and [IsApp] to make sure that instances such as
@@ -277,7 +277,7 @@ Proof. done. Qed.
Global Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.
-Class Frame {SI} {PROP : bi SI} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
+Class Frame `{SI: indexT} {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
Global Arguments Frame {_ _} _ _%I _%I _%I.
Global Arguments frame {_ _} _ _%I _%I _%I {_}.
Global Hint Mode Frame - + + ! ! - : typeclass_instances.
@@ -285,20 +285,20 @@ Global Hint Mode Frame - + + ! ! - : typeclass_instances.
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
-Class MaybeFrame {SI} {PROP : bi SI} (p : bool) (R P Q : PROP) (progress : bool) :=
+Class MaybeFrame `{SI: indexT} {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : □?p R ∗ Q ⊢ P.
Global Arguments MaybeFrame {_ _} _ _%I _%I _%I _.
Global Arguments maybe_frame {_ _} _ _%I _%I _%I _ {_}.
Global Hint Mode MaybeFrame - + + ! - - - : typeclass_instances.
-Global Instance maybe_frame_frame {SI} {PROP : bi SI} p (R P Q : PROP) :
+Global Instance maybe_frame_frame `{SI: indexT} {PROP : bi} p (R P Q : PROP) :
Frame p R P Q → MaybeFrame p R P Q true.
Proof. done. Qed.
-Global Instance maybe_frame_default_persistent {SI} {PROP : bi SI} (R P : PROP) :
+Global Instance maybe_frame_default_persistent `{SI: indexT} {PROP : bi} (R P : PROP) :
MaybeFrame true R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
-Global Instance maybe_frame_default {SI} {PROP : bi SI} (R P : PROP) :
+Global Instance maybe_frame_default `{SI: indexT} {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.
@@ -312,105 +312,105 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
logical constructs such as emp or True. Therefore, we use a Hint
Mode to disable all the instances that would have this behavior. *)
-Class MakeEmbed {SI} {PROP PROP' : bi SI} `{BiEmbed SI PROP PROP'} (P : PROP) (Q : PROP') :=
+Class MakeEmbed `{SI: indexT} {PROP PROP' : bi} `{!BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
Global Arguments MakeEmbed {_ _ _ _} _%I _%I.
Global Hint Mode MakeEmbed - + + + - - : typeclass_instances.
-Class KnownMakeEmbed {SI} {PROP PROP' : bi SI} `{BiEmbed SI PROP PROP'} (P : PROP) (Q : PROP') :=
+Class KnownMakeEmbed `{SI: indexT} {PROP PROP' : bi} `{!BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
known_make_embed :> MakeEmbed P Q.
Global Arguments KnownMakeEmbed {_ _ _ _} _%I _%I.
Global Hint Mode KnownMakeEmbed - + + + ! - : typeclass_instances.
-Class MakeSep {SI} {PROP : bi SI} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
+Class MakeSep `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
Global Arguments MakeSep {_ _} _%I _%I _%I.
Global Hint Mode MakeSep - + - - - : typeclass_instances.
-Class KnownLMakeSep {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownLMakeSep `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
knownl_make_sep :> MakeSep P Q PQ.
Global Arguments KnownLMakeSep {_ _} _%I _%I _%I.
Global Hint Mode KnownLMakeSep - + ! - - : typeclass_instances.
-Class KnownRMakeSep {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownRMakeSep `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
knownr_make_sep :> MakeSep P Q PQ.
Global Arguments KnownRMakeSep {_ _} _%I _%I _%I.
Global Hint Mode KnownRMakeSep - + - ! - : typeclass_instances.
-Class MakeAnd {SI} {PROP : bi SI} (P Q PQ : PROP) := make_and_l : P ∧ Q ⊣⊢ PQ.
+Class MakeAnd `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := make_and_l : P ∧ Q ⊣⊢ PQ.
Global Arguments MakeAnd {_ _} _%I _%I _%I.
Global Hint Mode MakeAnd - + - - - : typeclass_instances.
-Class KnownLMakeAnd {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownLMakeAnd `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
knownl_make_and :> MakeAnd P Q PQ.
Global Arguments KnownLMakeAnd {_ _} _%I _%I _%I.
Global Hint Mode KnownLMakeAnd - + ! - - : typeclass_instances.
-Class KnownRMakeAnd {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownRMakeAnd `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
knownr_make_and :> MakeAnd P Q PQ.
Global Arguments KnownRMakeAnd {_ _} _%I _%I _%I.
Global Hint Mode KnownRMakeAnd - + - ! - : typeclass_instances.
-Class MakeOr {SI} {PROP : bi SI} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
+Class MakeOr `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
Global Arguments MakeOr {_ _} _%I _%I _%I.
Global Hint Mode MakeOr - + - - - : typeclass_instances.
-Class KnownLMakeOr {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownLMakeOr `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
knownl_make_or :> MakeOr P Q PQ.
Global Arguments KnownLMakeOr {_ _} _%I _%I _%I.
Global Hint Mode KnownLMakeOr - + ! - - : typeclass_instances.
-Class KnownRMakeOr {SI} {PROP : bi SI} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
+Class KnownRMakeOr `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
Global Arguments KnownRMakeOr {_ _} _%I _%I _%I.
Global Hint Mode KnownRMakeOr - + - ! - : typeclass_instances.
-Class MakeAffinely {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeAffinely `{SI: indexT} {PROP : bi} (P Q : PROP) :=
make_affinely : <affine> P ⊣⊢ Q.
Global Arguments MakeAffinely {_ _} _%I _%I.
Global Hint Mode MakeAffinely - + - - : typeclass_instances.
-Class KnownMakeAffinely {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeAffinely `{SI: indexT} {PROP : bi} (P Q : PROP) :=
known_make_affinely :> MakeAffinely P Q.
Global Arguments KnownMakeAffinely {_ _} _%I _%I.
Global Hint Mode KnownMakeAffinely - + ! - : typeclass_instances.
-Class MakeIntuitionistically {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeIntuitionistically `{SI: indexT} {PROP : bi} (P Q : PROP) :=
make_intuitionistically : □ P ⊣⊢ Q.
Global Arguments MakeIntuitionistically {_ _} _%I _%I.
Global Hint Mode MakeIntuitionistically - + - - : typeclass_instances.
-Class KnownMakeIntuitionistically {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeIntuitionistically `{SI: indexT} {PROP : bi} (P Q : PROP) :=
known_make_intuitionistically :> MakeIntuitionistically P Q.
Global Arguments KnownMakeIntuitionistically {_ _} _%I _%I.
Global Hint Mode KnownMakeIntuitionistically - + ! - : typeclass_instances.
-Class MakeAbsorbingly {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeAbsorbingly `{SI: indexT} {PROP : bi} (P Q : PROP) :=
make_absorbingly : <absorb> P ⊣⊢ Q.
Global Arguments MakeAbsorbingly {_ _} _%I _%I.
Global Hint Mode MakeAbsorbingly - + - - : typeclass_instances.
-Class KnownMakeAbsorbingly {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeAbsorbingly `{SI: indexT} {PROP : bi} (P Q : PROP) :=
known_make_absorbingly :> MakeAbsorbingly P Q.
Global Arguments KnownMakeAbsorbingly {_ _} _%I _%I.
Global Hint Mode KnownMakeAbsorbingly - + ! - : typeclass_instances.
-Class MakePersistently {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakePersistently `{SI: indexT} {PROP : bi} (P Q : PROP) :=
make_persistently : <pers> P ⊣⊢ Q.
Global Arguments MakePersistently {_ _} _%I _%I.
Global Hint Mode MakePersistently - + - - : typeclass_instances.
-Class KnownMakePersistently {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakePersistently `{SI: indexT} {PROP : bi} (P Q : PROP) :=
known_make_persistently :> MakePersistently P Q.
Global Arguments KnownMakePersistently {_ _} _%I _%I.
Global Hint Mode KnownMakePersistently - + ! - : typeclass_instances.
-Class MakeLaterN {SI} {PROP : bi SI} (n : nat) (P lP : PROP) :=
+Class MakeLaterN `{SI: indexT} {PROP : bi} (n : nat) (P lP : PROP) :=
make_laterN : ▷^n P ⊣⊢ lP.
Global Arguments MakeLaterN {_ _} _%nat _%I _%I.
Global Hint Mode MakeLaterN - + + - - : typeclass_instances.
-Class KnownMakeLaterN {SI} {PROP : bi SI} (n : nat) (P lP : PROP) :=
+Class KnownMakeLaterN `{SI: indexT} {PROP : bi} (n : nat) (P lP : PROP) :=
known_make_laterN :> MakeLaterN n P lP.
Global Arguments KnownMakeLaterN {_ _} _%nat _%I _%I.
Global Hint Mode KnownMakeLaterN - + + ! - : typeclass_instances.
-Class MakeExcept0 {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeExcept0 `{SI: indexT} {PROP : bi} (P Q : PROP) :=
make_except_0 : ◇ P ⊣⊢ Q.
Global Arguments MakeExcept0 {_ _} _%I _%I.
Global Hint Mode MakeExcept0 - + - - : typeclass_instances.
-Class KnownMakeExcept0 {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeExcept0 `{SI: indexT} {PROP : bi} (P Q : PROP) :=
known_make_except_0 :> MakeExcept0 P Q.
Global Arguments KnownMakeExcept0 {_ _} _%I _%I.
Global Hint Mode KnownMakeExcept0 - + ! - : typeclass_instances.
-Class IntoExcept0 {SI} {PROP : bi SI} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
+Class IntoExcept0 `{SI: indexT} {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
Global Arguments IntoExcept0 {_ _} _%I _%I : simpl never.
Global Arguments into_except_0 {_ _} _%I _%I {_}.
Global Hint Mode IntoExcept0 - + ! - : typeclass_instances.
@@ -450,24 +450,24 @@ Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Qed.
>>
*)
-Class MaybeIntoLaterN {SI} {PROP : bi SI} (only_head : bool) (n : nat) (P Q : PROP) :=
+Class MaybeIntoLaterN `{SI: indexT} {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
maybe_into_laterN : P ⊢ ▷^n Q.
Global Arguments MaybeIntoLaterN {_ _} _ _%nat_scope _%I _%I.
Global Arguments maybe_into_laterN {_ _} _ _%nat_scope _%I _%I {_}.
Global Hint Mode MaybeIntoLaterN - + + + - - : typeclass_instances.
-Class IntoLaterN {SI} {PROP : bi SI} (only_head : bool) (n : nat) (P Q : PROP) :=
+Class IntoLaterN `{SI: indexT} {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
into_laterN :> MaybeIntoLaterN only_head n P Q.
Global Arguments IntoLaterN {_ _} _ _%nat_scope _%I _%I.
Global Hint Mode IntoLaterN - + + + ! - : typeclass_instances.
-Global Instance maybe_into_laterN_default {SI} {PROP : bi SI} only_head n (P : PROP) :
+Global Instance maybe_into_laterN_default `{SI: indexT} {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. *)
-Global Instance maybe_into_laterN_default_0 {SI} {PROP : bi SI} only_head (P : PROP) :
+Global Instance maybe_into_laterN_default_0 `{SI: indexT} {PROP : bi} only_head (P : PROP) :
MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.
@@ -475,7 +475,7 @@ Proof. apply _. Qed.
embeddings using [iModIntro].
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
-Class IntoEmbed {SI} {PROP PROP' : bi SI} `{BiEmbed SI PROP PROP'} (P : PROP') (Q : PROP) :=
+Class IntoEmbed `{SI: indexT} {PROP PROP' : bi} `{!BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
into_embed : P ⊢ ⎡Q⎤.
Global Arguments IntoEmbed {_ _ _ _} _%I _%I.
Global Arguments into_embed {_ _ _ _} _%I _%I {_}.
@@ -493,24 +493,24 @@ Global Hint Mode IntoEmbed - + + + ! - : typeclass_instances.
No Hint Modes are declared here. The appropriate one would be
[Hint Mode - - ! -], but the fact that Coq ignores primitive
projections for hints modes would make this fail.*)
-Class AsEmpValid {SI} {PROP : bi SI} (φ : Prop) (P : PROP) :=
+Class AsEmpValid `{SI: indexT} {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid : φ ↔ ⊢ P.
Global Arguments AsEmpValid {_ _} _%type _%I.
-Class AsEmpValid0 {SI} {PROP : bi SI} (φ : Prop) (P : PROP) :=
+Class AsEmpValid0 `{SI: indexT} {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_0 : AsEmpValid φ P.
Global Arguments AsEmpValid0 {_ _} _%type _%I.
-Existing Instance as_emp_valid_0 | 0.
+Global Existing Instance as_emp_valid_0 | 0.
-Lemma as_emp_valid_1 (φ : Prop) {SI} {PROP : bi SI} (P : PROP) `{!AsEmpValid φ P} :
+Lemma as_emp_valid_1 (φ : Prop) `{SI: indexT} {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
φ → ⊢ P.
Proof. by apply as_emp_valid. Qed.
-Lemma as_emp_valid_2 (φ : Prop) {SI} {PROP : bi SI} (P : PROP) `{!AsEmpValid φ P} :
+Lemma as_emp_valid_2 (φ : Prop) `{SI: indexT} {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
(⊢ P) → φ.
Proof. by apply as_emp_valid. Qed.
(* Input: [P]; Outputs: [N],
Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
-Class IntoInv {SI} {PROP : bi SI} (P: PROP) (N: namespace).
+Class IntoInv `{SI: indexT} {PROP : bi} (P: PROP) (N: namespace).
Global Arguments IntoInv {_ _} _%I _.
Global Hint Mode IntoInv - + ! - : typeclass_instances.
@@ -519,7 +519,7 @@ Global Hint Mode IntoInv - + ! - : typeclass_instances.
usable and general form would use telescopes and also allow binders for the
closing view shift. [γ] is an [option] to make it easy for ElimAcc
instances to recognize the [emp] case and make it look nicer. *)
-Definition accessor {SI} {PROP : bi SI} {X : Type} (M1 M2 : PROP → PROP)
+Definition accessor `{SI: indexT} {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
(α β : X → PROP) (mγ : X → option PROP) : PROP :=
M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
@@ -530,7 +530,7 @@ Definition accessor {SI} {PROP : bi SI} {X : Type} (M1 M2 : PROP → PROP)
Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
into [Q'] with a new assumption [α x], where [φ] is a side-condition at the
Cow level that needs to hold. *)
-Class ElimAcc {SI} {PROP : bi SI} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
+Class ElimAcc `{SI: indexT} {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
(α β : X → PROP) (mγ : X → option PROP)
(Q : PROP) (Q' : X → PROP) :=
elim_acc : φ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
@@ -548,7 +548,7 @@ Global Hint Mode ElimAcc - + ! - ! ! ! ! ! ! - : typeclass_instances.
- [M1], [M2]: the two accessor modalities (they will typically still have
some evars though, e.g. for the masks)
*)
-Class IntoAcc {SI} {PROP : bi SI} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
+Class IntoAcc `{SI: indexT} {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
(M1 M2 : PROP → PROP) (α β : X → PROP) (mγ : X → option PROP) :=
into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.
Global Arguments IntoAcc {_ _} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
@@ -575,7 +575,7 @@ Global Hint Mode IntoAcc - + - ! - - - - - - - : typeclass_instances.
TODO: Add support for a binder (like accessors have it).
*)
-Class ElimInv {SI} {PROP : bi SI} {X : Type} (φ : Prop)
+Class ElimInv `{SI: indexT} {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
(Q : PROP) (Q' : X → PROP) :=
elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
@@ -599,40 +599,40 @@ with the exception of:
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iIntuitionistic]
*)
-Global Instance into_pure_tc_opaque {SI} {PROP : bi SI} (P : PROP) φ :
+Global Instance into_pure_tc_opaque `{SI: indexT} {PROP : bi} (P : PROP) φ :
IntoPure P φ → IntoPure (tc_opaque P) φ := id.
-Global Instance from_pure_tc_opaque {SI} {PROP : bi SI} (a : bool) (P : PROP) φ :
+Global Instance from_pure_tc_opaque `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) φ :
FromPure a P φ → FromPure a (tc_opaque P) φ := id.
-Global Instance from_wand_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance from_wand_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
-Global Instance into_wand_tc_opaque {SI} {PROP : bi SI} p q (R P Q : PROP) :
+Global Instance into_wand_tc_opaque `{SI: indexT} {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. *)
-Global Instance from_and_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance from_and_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
-Global Instance into_and_tc_opaque {SI} {PROP : bi SI} p (P Q1 Q2 : PROP) :
+Global Instance into_and_tc_opaque `{SI: indexT} {PROP : bi} p (P Q1 Q2 : PROP) :
IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2 := id.
-Global Instance into_sep_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance into_sep_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
IntoSep P Q1 Q2 → IntoSep (tc_opaque P) Q1 Q2 := id.
-Global Instance from_or_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance from_or_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2 := id.
-Global Instance into_or_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance into_or_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
IntoOr P Q1 Q2 → IntoOr (tc_opaque P) Q1 Q2 := id.
-Global Instance from_exist_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :
+Global Instance from_exist_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
FromExist P Φ → FromExist (tc_opaque P) Φ := id.
-Global Instance into_exist_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
+Global Instance into_exist_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
IntoExist P Φ name → IntoExist (tc_opaque P) Φ name := id.
-Global Instance from_forall_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
+Global Instance from_forall_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
FromForall P Φ name → FromForall (tc_opaque P) Φ name := id.
-Global Instance into_forall_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :
+Global Instance into_forall_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
-Global Instance from_modal_tc_opaque {SI} {PROP1 PROP2 : bi SI} {A}
+Global Instance from_modal_tc_opaque `{SI: indexT} {PROP1 PROP2 : bi} {A}
M (sel : A) (P : PROP2) (Q : PROP1) :
FromModal M sel P Q → FromModal M sel (tc_opaque P) Q := id.
-Global Instance elim_modal_tc_opaque {SI} {PROP : bi SI} φ p p' (P P' Q Q' : PROP) :
+Global Instance elim_modal_tc_opaque `{SI: indexT} {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.
-Global Instance into_inv_tc_opaque {SI} {PROP : bi SI} (P : PROP) N :
+Global Instance into_inv_tc_opaque `{SI: indexT} {PROP : bi} (P : PROP) N :
IntoInv P N → IntoInv (tc_opaque P) N := id.
-Global Instance elim_inv_tc_opaque {SI} {PROP : bi SI} {X} φ Pinv Pin Pout Pclose Q Q' :
+Global Instance elim_inv_tc_opaque `{SI: indexT} {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/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 4ef75d32..1ff7d2aa 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -8,7 +8,7 @@ Local Open Scope lazy_bool_scope.
(* Coq versions of the tactics *)
Section tactics.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
@@ -573,7 +573,7 @@ Proof.
Qed.
(** * Combining *)
-Class FromSeps {SI} {PROP : bi SI} (P : PROP) (Qs : list PROP) :=
+Class FromSeps `{SI: indexT} {PROP : bi} (P : PROP) (Qs : list PROP) :=
from_seps : [∗] Qs ⊢ P.
Local Arguments FromSeps {_ _} _%I _%I.
Local Arguments from_seps {_ _} _%I _%I {_}.
@@ -799,7 +799,7 @@ Qed.
(** * Rewriting *)
Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy) →
- ∀ {A : ofe SI} (x y : A) (Φ : A → PROP),
+ ∀ {A : ofe} (x y : A) (Φ : A → PROP),
IntoInternalEq Pxy x y →
(Q ⊣⊢ Φ (if d is Left then y else x)) →
NonExpansive Φ →
@@ -814,7 +814,7 @@ Qed.
Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
envs_lookup i Δ = Some (p, Pxy) →
envs_lookup j Δ = Some (q, P) →
- ∀ {A : ofe SI} (x y : A) (Φ : A → PROP),
+ ∀ {A : ofe} (x y : A) (Φ : A → PROP),
IntoInternalEq Pxy x y →
(P ⊣⊢ Φ (if d is Left then y else x)) →
NonExpansive Φ →
@@ -870,7 +870,7 @@ Inputs:
Outputs:
- [Γout] : the resulting environment. *)
-Class TransformIntuitionisticEnv {SI} {PROP1 PROP2: bi SI} (M : modality PROP1 PROP2)
+Class TransformIntuitionisticEnv {SI: indexT} {PROP1 PROP2: bi} (M : modality PROP1 PROP2)
(C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1) := {
transform_intuitionistic_env :
(∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
@@ -893,7 +893,7 @@ Inputs:
Outputs:
- [Γout] : the resulting environment.
- [filtered] : a Boolean indicating if non-affine hypotheses have been cleared. *)
-Class TransformSpatialEnv {SI} {PROP1 PROP2: bi SI} (M : modality PROP1 PROP2)
+Class TransformSpatialEnv {SI: indexT} {PROP1 PROP2: bi} (M : modality PROP1 PROP2)
(C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1)
(filtered : bool) := {
transform_spatial_env :
@@ -915,7 +915,7 @@ Inputs:
Outputs:
- [Γout] : the resulting environment. *)
-Inductive IntoModalIntuitionisticEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : modality PROP1 PROP2)
+Inductive IntoModalIntuitionisticEnv {SI: indexT} {PROP2: bi} : ∀ {PROP1} (M : modality PROP1 PROP2)
(Γin : env PROP2) (Γout : env PROP1), modality_action PROP1 PROP2 → Prop :=
| MIEnvIsEmpty_intuitionistic {PROP1} (M : modality PROP1 PROP2) :
IntoModalIntuitionisticEnv M Enil Enil MIEnvIsEmpty
@@ -926,12 +926,12 @@ Inductive IntoModalIntuitionisticEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : moda
(M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout :
TransformIntuitionisticEnv M C Γin Γout →
IntoModalIntuitionisticEnv M Γin Γout (MIEnvTransform C)
- | MIEnvClear_intuitionistic {PROP1 : bi SI} (M : modality PROP1 PROP2) Γ :
+ | MIEnvClear_intuitionistic {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
IntoModalIntuitionisticEnv M Γ Enil MIEnvClear
| MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
Existing Class IntoModalIntuitionisticEnv.
-Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
+Global Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
(* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
@@ -947,7 +947,7 @@ Inputs:
Outputs:
- [Γout] : the resulting environment.
- [filtered] : a Boolean indicating if non-affine hypotheses have been cleared. *)
-Inductive IntoModalSpatialEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : modality PROP1 PROP2)
+Inductive IntoModalSpatialEnv {SI: indexT} {PROP2: bi} : ∀ {PROP1} (M : modality PROP1 PROP2)
(Γin : env PROP2) (Γout : env PROP1), modality_action PROP1 PROP2 → bool → Prop :=
| MIEnvIsEmpty_spatial {PROP1} (M : modality PROP1 PROP2) :
IntoModalSpatialEnv M Enil Enil MIEnvIsEmpty false
@@ -958,16 +958,16 @@ Inductive IntoModalSpatialEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : modality PR
(M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout fi :
TransformSpatialEnv M C Γin Γout fi →
IntoModalSpatialEnv M Γin Γout (MIEnvTransform C) fi
- | MIEnvClear_spatial {PROP1 : bi SI} (M : modality PROP1 PROP2) Γ :
+ | MIEnvClear_spatial {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
IntoModalSpatialEnv M Γ Enil MIEnvClear false
| MIEnvId_spatial (M : modality PROP2 PROP2) Γ :
IntoModalSpatialEnv M Γ Γ MIEnvId false.
Existing Class IntoModalSpatialEnv.
-Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
+Global Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
MIEnvTransform_spatial MIEnvClear_spatial MIEnvId_spatial.
Section tac_modal_intro.
- Context {SI} {PROP1 PROP2 : bi SI} (M : modality PROP1 PROP2).
+ Context {SI: indexT} {PROP1 PROP2 : bi} (M : modality PROP1 PROP2).
Global Instance transform_intuitionistic_env_nil C : TransformIntuitionisticEnv M C Enil Enil.
Proof.
@@ -1079,7 +1079,7 @@ End tac_modal_intro.
(** The class [MaybeIntoLaterNEnvs] is used by tactics that need to introduce
laters, e.g., the symbolic execution tactics. *)
-Class MaybeIntoLaterNEnvs {SI} {PROP: bi SI} (n : nat) (Δ1 Δ2 : envs PROP) := {
+Class MaybeIntoLaterNEnvs {SI: indexT} {PROP: bi} (n : nat) (Δ1 Δ2 : envs PROP) := {
into_later_intuitionistic :
TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n)
(env_intuitionistic Δ1) (env_intuitionistic Δ2);
@@ -1088,13 +1088,13 @@ Class MaybeIntoLaterNEnvs {SI} {PROP: bi SI} (n : nat) (Δ1 Δ2 : envs PROP) :=
(MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
}.
-Global Instance into_laterN_envs {SI} {PROP: bi SI} n (Γp1 Γp2 Γs1 Γs2 : env PROP) m :
+Global Instance into_laterN_envs {SI: indexT} {PROP: bi} n (Γp1 Γp2 Γs1 Γs2 : env PROP) m :
TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
Proof. by split. Qed.
-Lemma into_laterN_env_sound {SI} {PROP : bi SI} n (Δ1 Δ2 : envs PROP) :
+Lemma into_laterN_env_sound {SI: indexT} {PROP : bi} n (Δ1 Δ2 : envs PROP) :
MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
Proof.
intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq /= !laterN_and -laterN_sep_2.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index d2b1d3b3..339bbc97 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -210,7 +210,7 @@ Global Instance env_to_list_subenv_proper :
Proof. induction 1; simpl; constructor; auto. Qed.
End env.
-Record envs {SI} (PROP : bi SI) := Envs {
+Record envs `{SI: indexT} (PROP : bi) := Envs {
env_intuitionistic : env PROP;
env_spatial : env PROP;
env_counter : positive (** A counter to generate fresh hypothesis names *)
@@ -240,53 +240,53 @@ We first define a version [pre_envs_entails] that takes the two contexts
[env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
crucial to make sure that the counter [env_counter] is not part of the seal. *)
-Record envs_wf' {SI} {PROP : bi SI} (Γp Γs : env PROP) := {
+Record envs_wf' `{SI: indexT} {PROP : bi} (Γp Γs : env PROP) := {
env_intuitionistic_valid : env_wf Γp;
env_spatial_valid : env_wf Γs;
envs_disjoint i : Γp !! i = None ∨ Γs !! i = None
}.
-Definition envs_wf {SI} {PROP : bi SI} (Δ : envs PROP) :=
+Definition envs_wf `{SI: indexT} {PROP : bi} (Δ : envs PROP) :=
envs_wf' (env_intuitionistic Δ) (env_spatial Δ).
-Definition of_envs' {SI} {PROP : bi SI} (Γp Γs : env PROP) : PROP :=
+Definition of_envs' `{SI: indexT} {PROP : bi} (Γp Γs : env PROP) : PROP :=
(⌜envs_wf' Γp Γs⌠∧ □ [∧] Γp ∗ [∗] Γs)%I.
Global Instance: Params (@of_envs') 2 := {}.
-Definition of_envs {SI} {PROP : bi SI} (Δ : envs PROP) : PROP :=
+Definition of_envs `{SI: indexT} {PROP : bi} (Δ : envs PROP) : PROP :=
of_envs' (env_intuitionistic Δ) (env_spatial Δ).
Global Instance: Params (@of_envs) 2 := {}.
Global Arguments of_envs : simpl never.
-Definition pre_envs_entails_def {SI} {PROP : bi SI} (Γp Γs : env PROP) (Q : PROP) :=
+Definition pre_envs_entails_def `{SI: indexT} {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
of_envs' Γp Γs ⊢ Q.
Definition pre_envs_entails_aux : seal (@pre_envs_entails_def). Proof. by eexists. Qed.
Definition pre_envs_entails := pre_envs_entails_aux.(unseal).
Definition pre_envs_entails_eq : @pre_envs_entails = @pre_envs_entails_def :=
pre_envs_entails_aux.(seal_eq).
-Definition envs_entails {SI} {PROP : bi SI} (Δ : envs PROP) (Q : PROP) : Prop :=
+Definition envs_entails `{SI: indexT} {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
pre_envs_entails SI PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
Definition envs_entails_eq :
- @envs_entails = λ SI (PROP: bi SI) (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
+ @envs_entails = λ SI (PROP: bi) (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
Global Arguments envs_entails {SI} {PROP} Δ Q%I.
Global Instance: Params (@envs_entails) 2 := {}.
-Record envs_Forall2 {SI} {PROP : bi SI} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
+Record envs_Forall2 `{SI: indexT} {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
-Definition envs_dom {SI} {PROP: bi SI} (Δ : envs PROP) : list ident :=
+Definition envs_dom `{SI: indexT} {PROP: bi} (Δ : envs PROP) : list ident :=
env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
-Definition envs_lookup {SI} {PROP: bi SI} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
+Definition envs_lookup `{SI: indexT} {PROP: bi} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
let (Γp,Γs,n) := Δ in
match env_lookup i Γp with
| Some P => Some (true, P)
| None => P ↠env_lookup i Γs; Some (false, P)
end.
-Definition envs_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
+Definition envs_delete `{SI: indexT} {PROP: bi} (remove_intuitionistic : bool)
(i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
let (Γp,Γs,n) := Δ in
match p with
@@ -294,7 +294,7 @@ Definition envs_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
| false => Envs Γp (env_delete i Γs) n
end.
-Definition envs_lookup_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
+Definition envs_lookup_delete `{SI: indexT} {PROP: bi} (remove_intuitionistic : bool)
(i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
let (Γp,Γs,n) := Δ in
match env_lookup_delete i Γp with
@@ -302,7 +302,7 @@ Definition envs_lookup_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
| None => '(P,Γs') ↠env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
end.
-Fixpoint envs_lookup_delete_list {SI} {PROP: bi SI} (remove_intuitionistic : bool)
+Fixpoint envs_lookup_delete_list `{SI: indexT} {PROP: bi} (remove_intuitionistic : bool)
(js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
match js with
| [] => Some (true, [], Δ)
@@ -312,12 +312,12 @@ Fixpoint envs_lookup_delete_list {SI} {PROP: bi SI} (remove_intuitionistic : boo
Some ((p:bool) &&& q, P :: Ps, Δ'')
end.
-Definition envs_snoc {SI} {PROP: bi SI} (Δ : envs PROP)
+Definition envs_snoc `{SI: indexT} {PROP: bi} (Δ : envs PROP)
(p : bool) (j : ident) (P : PROP) : envs PROP :=
let (Γp,Γs,n) := Δ in
if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
-Definition envs_app {SI} {PROP: bi SI} (p : bool)
+Definition envs_app `{SI: indexT} {PROP: bi} (p : bool)
(Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
let (Γp,Γs,n) := Δ in
match p with
@@ -325,7 +325,7 @@ Definition envs_app {SI} {PROP: bi SI} (p : bool)
| false => _ ↠env_app Γ Γp; Γs' ↠env_app Γ Γs; Some (Envs Γp Γs' n)
end.
-Definition envs_simple_replace {SI} {PROP: bi SI} (i : ident) (p : bool)
+Definition envs_simple_replace `{SI: indexT} {PROP: bi} (i : ident) (p : bool)
(Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
let (Γp,Γs,n) := Δ in
match p with
@@ -333,24 +333,24 @@ Definition envs_simple_replace {SI} {PROP: bi SI} (i : ident) (p : bool)
| false => _ ↠env_app Γ Γp; Γs' ↠env_replace i Γ Γs; Some (Envs Γp Γs' n)
end.
-Definition envs_replace {SI} {PROP: bi SI} (i : ident) (p q : bool)
+Definition envs_replace `{SI: indexT} {PROP: bi} (i : ident) (p q : bool)
(Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
if beq p q then envs_simple_replace i p Γ Δ
else envs_app q Γ (envs_delete true i p Δ).
-Definition env_spatial_is_nil {SI} {PROP: bi SI} (Δ : envs PROP) : bool :=
+Definition env_spatial_is_nil `{SI: indexT} {PROP: bi} (Δ : envs PROP) : bool :=
if env_spatial Δ is Enil then true else false.
-Definition envs_clear_spatial {SI} {PROP: bi SI} (Δ : envs PROP) : envs PROP :=
+Definition envs_clear_spatial `{SI: indexT} {PROP: bi} (Δ : envs PROP) : envs PROP :=
Envs (env_intuitionistic Δ) Enil (env_counter Δ).
-Definition envs_clear_intuitionistic {SI} {PROP: bi SI} (Δ : envs PROP) : envs PROP :=
+Definition envs_clear_intuitionistic `{SI: indexT} {PROP: bi} (Δ : envs PROP) : envs PROP :=
Envs Enil (env_spatial Δ) (env_counter Δ).
-Definition envs_incr_counter {SI} {PROP: bi SI} (Δ : envs PROP) : envs PROP :=
+Definition envs_incr_counter `{SI: indexT} {PROP: bi} (Δ : envs PROP) : envs PROP :=
Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
-Fixpoint envs_split_go {SI} {PROP: bi SI}
+Fixpoint envs_split_go `{SI: indexT} {PROP: bi}
(js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
match js with
| [] => Some (Δ1, Δ2)
@@ -361,23 +361,23 @@ Fixpoint envs_split_go {SI} {PROP: bi SI}
end.
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
-Definition envs_split {SI} {PROP: bi SI} (d : direction)
+Definition envs_split `{SI: indexT} {PROP: bi} (d : direction)
(js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
'(Δ1,Δ2) ↠envs_split_go js Δ (envs_clear_spatial Δ);
if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
-Fixpoint env_to_prop_go {SI} {PROP : bi SI} (acc : PROP) (Γ : env PROP) : PROP :=
+Fixpoint env_to_prop_go `{SI: indexT} {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_go (P ∗ acc)%I Γ end.
-Definition env_to_prop {SI} {PROP : bi SI} (Γ : env PROP) : PROP :=
+Definition env_to_prop `{SI: indexT} {PROP : bi} (Γ : env PROP) : PROP :=
match Γ with Enil => emp%I | Esnoc Γ _ P => env_to_prop_go P Γ end.
-Fixpoint env_to_prop_and_go {SI} {PROP : bi SI} (acc : PROP) (Γ : env PROP) : PROP :=
+Fixpoint env_to_prop_and_go `{SI: indexT} {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_and_go (P ∧ acc)%I Γ end.
-Definition env_to_prop_and {SI} {PROP : bi SI} (Γ : env PROP) : PROP :=
+Definition env_to_prop_and `{SI: indexT} {PROP : bi} (Γ : env PROP) : PROP :=
match Γ with Enil => True%I | Esnoc Γ _ P => env_to_prop_and_go P Γ end.
Section envs.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
Implicit Types Γ Γp Γs : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 37aadb59..f4da9ba4 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -16,7 +16,7 @@ but that makes framing less predictable and might have some performance impact.
Hence, we only perform such cleanup for [True] and [emp]. *)
Section bi.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
Implicit Types P Q R : PROP.
(* Frame *)
Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
@@ -51,23 +51,23 @@ Proof.
- by rewrite right_id -affinely_affinely_if affine_affinely.
Qed.
-Global Instance make_embed_pure `{BiEmbed SI PROP PROP'} φ :
+Global Instance make_embed_pure `{!BiEmbed PROP PROP'} φ :
KnownMakeEmbed (PROP:=PROP) ⌜φ⌠⌜φâŒ.
Proof. apply embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbedEmp SI PROP PROP'} :
+Global Instance make_embed_emp `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
-Global Instance make_embed_default `{BiEmbed SI PROP PROP'} P :
+Global Instance make_embed_default `{!BiEmbed PROP PROP'} P :
MakeEmbed P (⎡P⎤)%I | 100.
Proof. by rewrite /MakeEmbed. Qed.
-Global Instance frame_embed `{BiEmbed SI 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'.
Proof.
rewrite /Frame /MakeEmbed => <- <-.
rewrite embed_sep embed_intuitionistically_if_2 => //.
Qed.
-Global Instance frame_pure_embed `{BiEmbed SI 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'.
Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
@@ -302,9 +302,9 @@ Proof.
rewrite persistently_elim impl_elim_r //.
Qed.
-Global Instance frame_eq_embed {PROP': bi SI} `{!BiEmbed PROP PROP', !BiInternalEq PROP,
+Global Instance frame_eq_embed {PROP': bi} `{!BiEmbed PROP PROP', !BiInternalEq PROP,
!BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
- p P Q (Q' : PROP') {A : ofe SI} (a b : A) :
+ p P Q (Q' : PROP') {A : ofe} (a b : A) :
Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
@@ -331,10 +331,10 @@ Proof.
by rewrite laterN_intuitionistically_if_2 laterN_sep_2.
Qed.
-Global Instance frame_bupd `{BiBUpd SI 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).
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
-Global Instance frame_fupd `{BiFUpd SI 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).
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 1fb925dc..e92fbea6 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1039,7 +1039,7 @@ returns [false], then the conclusion can be moved in the intuitionistic context
even if conditions 1 and 3 do not hold. Therefore, in that case, we prefer
putting the conclusion to the intuitionistic context directly and not using
[tac_specialize_intuitionistic_helper], which requires conditions 1 and 3. *)
-Fixpoint use_tac_specialize_intuitionistic_helper {SI} {M: bi SI}
+Fixpoint use_tac_specialize_intuitionistic_helper `{SI: indexT} {M: bi}
(Δ : envs M) (pats : list spec_pat) : bool :=
match pats with
| [] => false
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index 0f28f5f6..ee01d3ac 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -49,10 +49,10 @@ it is implemented as an endomapping. On the other hand, the embedding modality
⎡-⎤ is a mapping between propositions of different BI-algebras.
*)
-Inductive modality_action {SI: indexT} (PROP1 : bi SI) : bi SI → Type :=
- | MIEnvIsEmpty {PROP2 : bi SI} : modality_action PROP1 PROP2
+Inductive modality_action `{SI: indexT} (PROP1 : bi) : bi → Type :=
+ | MIEnvIsEmpty {PROP2 : bi} : modality_action PROP1 PROP2
| MIEnvForall (C : PROP1 → Prop) : modality_action PROP1 PROP1
- | MIEnvTransform {PROP2 : bi SI} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
+ | MIEnvTransform {PROP2 : bi} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
| MIEnvClear {PROP2} : modality_action PROP1 PROP2
| MIEnvId : modality_action PROP1 PROP1.
Global Arguments MIEnvIsEmpty {_ _ _}.
@@ -63,7 +63,7 @@ Global Arguments MIEnvId {_ _}.
Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
-Definition modality_intuitionistic_action_spec {SI: indexT} {PROP1 PROP2: bi SI}
+Definition modality_intuitionistic_action_spec `{SI: indexT} {PROP1 PROP2: bi}
(s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
match s with
| MIEnvIsEmpty => λ M, True
@@ -77,7 +77,7 @@ Definition modality_intuitionistic_action_spec {SI: indexT} {PROP1 PROP2: bi SI}
| MIEnvId => λ M, ∀ P, □ P ⊢ M (□ P)
end.
-Definition modality_spatial_action_spec {SI} {PROP1 PROP2: bi SI}
+Definition modality_spatial_action_spec `{SI: indexT} {PROP1 PROP2: bi}
(s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
match s with
| MIEnvIsEmpty => λ M, True
@@ -89,7 +89,7 @@ Definition modality_spatial_action_spec {SI} {PROP1 PROP2: bi SI}
(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
-Record modality_mixin {SI} {PROP1 PROP2 : bi SI} (M : PROP1 → PROP2)
+Record modality_mixin `{SI: indexT} {PROP1 PROP2 : bi} (M : PROP1 → PROP2)
(iaction saction : modality_action PROP1 PROP2) := {
modality_mixin_intuitionistic : modality_intuitionistic_action_spec iaction M;
modality_mixin_spatial : modality_spatial_action_spec saction M;
@@ -98,7 +98,7 @@ Record modality_mixin {SI} {PROP1 PROP2 : bi SI} (M : PROP1 → PROP2)
modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
}.
-Record modality {SI} (PROP1 PROP2 : bi SI) := Modality {
+Record modality `{SI: indexT} (PROP1 PROP2 : bi) := Modality {
modality_car :> PROP1 → PROP2;
modality_intuitionistic_action : modality_action PROP1 PROP2;
modality_spatial_action : modality_action PROP1 PROP2;
@@ -110,7 +110,7 @@ Global Arguments modality_intuitionistic_action {_ _ _} _.
Global Arguments modality_spatial_action {_ _ _} _.
Section modality.
- Context {SI: indexT} {PROP1 PROP2: bi SI} (M : modality PROP1 PROP2).
+ Context {SI: indexT} {PROP1 PROP2: bi} (M : modality PROP1 PROP2).
Lemma modality_intuitionistic_transform C P Q :
modality_intuitionistic_action M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
@@ -140,7 +140,7 @@ Section modality.
End modality.
Section modality1.
- Context {SI: indexT} {PROP: bi SI} (M : modality PROP PROP).
+ Context {SI: indexT} {PROP: bi} (M : modality PROP PROP).
Lemma modality_intuitionistic_forall C P :
modality_intuitionistic_action M = MIEnvForall C → C P → □ P ⊢ M (□ P).
@@ -183,6 +183,6 @@ End modality1.
which will instruct [iModIntro] to introduce the modality without modifying the
proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
[monPred_subjectively] and [bi_absorbingly]. *)
-Lemma modality_id_mixin {SI} {PROP : bi SI} : modality_mixin (@id PROP) MIEnvId MIEnvId.
+Lemma modality_id_mixin `{SI: indexT} {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.
-Definition modality_id {SI} {PROP : bi SI} := Modality (@id PROP) modality_id_mixin.
+Definition modality_id `{SI: indexT} {PROP : bi} := Modality (@id PROP) modality_id_mixin.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index ae3e993d..97eb1fdc 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
Import bi.
Section modalities.
- Context {SI} {PROP : bi SI}.
+ Context `{SI: indexT} {PROP : bi}.
Lemma modality_persistently_mixin :
modality_mixin (@bi_persistently SI PROP) MIEnvId MIEnvClear.
--
GitLab