Commit 9c36e6af authored by Simon Spies's avatar Simon Spies
Browse files

finish making step-index a typeclass

parent 1df456c6
......@@ -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.
......
......@@ -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.
......
......@@ -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).
......
......@@ -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.
......@@ -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.
......
......@@ -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