diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 0fdcaa4c0dfc87edc6767ed5eae82fa0db1f3774..e68312bee4d5c6b67d2d9c893082c6f8da7032b8 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -35,12 +35,13 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope.
-Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
+Local Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
-Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
+Local Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Global Arguments big_opM {M} o {_ K _ _ A} _ _.
-Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
+Local Definition big_opM_unseal :
+ @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Global Instance: Params (@big_opM) 7 := {}.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
@@ -49,23 +50,25 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope.
-Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
+Local Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
-Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
+Local Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Global Arguments big_opS {M} o {_ A _ _} _ _.
-Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
+Local Definition big_opS_unseal :
+ @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Global Instance: Params (@big_opS) 6 := {}.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope.
-Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
+Local Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
-Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
+Local Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
Global Arguments big_opMS {M} o {_ A _ _} _ _.
-Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
+Local Definition big_opMS_unseal :
+ @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Global Instance: Params (@big_opMS) 6 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
@@ -252,12 +255,12 @@ Proof. by apply big_opL_sep_zip_with. Qed.
Lemma big_opM_empty `{Countable K} {B} (f : K → B → M) :
([^o map] k↦x ∈ ∅, f k x) = monoid_unit.
-Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed.
+Proof. by rewrite big_opM_unseal /big_opM_def map_to_list_empty. Qed.
Lemma big_opM_insert `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
m !! i = None →
([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y.
-Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed.
+Proof. intros ?. by rewrite big_opM_unseal /big_opM_def map_to_list_insert. Qed.
Lemma big_opM_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
m !! i = Some x →
@@ -304,7 +307,7 @@ Section gmap.
(∀ k x, m !! k = Some x → R (f k x) (g k x)) →
R ([^o map] k ↦ x ∈ m, f k x) ([^o map] k ↦ x ∈ m, g k x).
Proof.
- intros ?? Hf. rewrite big_opM_eq. apply (big_opL_gen_proper R); auto.
+ intros ?? Hf. rewrite big_opM_unseal. apply (big_opL_gen_proper R); auto.
intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
Qed.
@@ -353,7 +356,7 @@ Section gmap.
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opM_map_to_list f m :
([^o map] k↦x ∈ m, f k x) ≡ [^o list] xk ∈ map_to_list m, f (xk.1) (xk.2).
- Proof. rewrite big_opM_eq. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
+ Proof. rewrite big_opM_unseal. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
Lemma big_opM_singleton f i x : ([^o map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
Proof.
@@ -363,13 +366,13 @@ Section gmap.
Lemma big_opM_unit m : ([^o map] k↦y ∈ m, monoid_unit) ≡ (monoid_unit : M).
Proof.
- by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_eq.
+ by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_unseal.
Qed.
Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m :
([^o map] k↦y ∈ h <$> m, f k y) ≡ ([^o map] k↦y ∈ m, f k (h y)).
Proof.
- rewrite big_opM_eq /big_opM_def map_to_list_fmap big_opL_fmap.
+ rewrite big_opM_unseal /big_opM_def map_to_list_fmap big_opL_fmap.
by apply big_opL_proper=> ? [??].
Qed.
@@ -445,7 +448,7 @@ Section gmap.
([^o map] k↦x ∈ m, f k x `o` g k x)
≡ ([^o map] k↦x ∈ m, f k x) `o` ([^o map] k↦x ∈ m, g k x).
Proof.
- rewrite big_opM_eq /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
+ rewrite big_opM_unseal /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
Qed.
End gmap.
@@ -483,7 +486,7 @@ Section gset.
(∀ x, x ∈ X → R (f x) (g x)) →
R ([^o set] x ∈ X, f x) ([^o set] x ∈ X, g x).
Proof.
- rewrite big_opS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
+ rewrite big_opS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
Qed.
@@ -514,10 +517,10 @@ Section gset.
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opS_elements f X :
([^o set] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
- Proof. by rewrite big_opS_eq. Qed.
+ Proof. by rewrite big_opS_unseal. Qed.
Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
- Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
+ Proof. by rewrite big_opS_unseal /big_opS_def elements_empty. Qed.
Lemma big_opS_insert f X x :
x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x `o` [^o set] y ∈ X, f y).
@@ -557,7 +560,7 @@ Section gset.
Lemma big_opS_unit X : ([^o set] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
Proof.
- by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
+ by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_unseal.
Qed.
Lemma big_opS_filter' (φ : A → Prop) `{∀ x, Decision (φ x)} f X :
@@ -605,7 +608,7 @@ Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
([^o map] k↦_ ∈ m, f k) ≡ ([^o set] k ∈ dom m, f k).
Proof.
induction m as [|i x ?? IH] using map_ind.
- { by rewrite big_opM_eq big_opS_eq dom_empty_L. }
+ { by rewrite big_opM_unseal big_opS_unseal dom_empty_L. }
by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
Qed.
@@ -620,7 +623,7 @@ Section gmultiset.
(∀ x, x ∈ X → R (f x) (g x)) →
R ([^o mset] x ∈ X, f x) ([^o mset] x ∈ X, g x).
Proof.
- rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
+ rewrite big_opMS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
Qed.
@@ -651,18 +654,18 @@ Section gmultiset.
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opMS_elements f X :
([^o mset] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
- Proof. by rewrite big_opMS_eq. Qed.
+ Proof. by rewrite big_opMS_unseal. Qed.
Lemma big_opMS_empty f : ([^o mset] x ∈ ∅, f x) = monoid_unit.
- Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
+ Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_empty. Qed.
Lemma big_opMS_disj_union f X Y :
([^o mset] y ∈ X ⊎ Y, f y) ≡ ([^o mset] y ∈ X, f y) `o` [^o mset] y ∈ Y, f y.
- Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
+ Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[+ x +]}, f y) ≡ f x.
Proof.
- intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
+ intros. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_singleton /= right_id.
Qed.
Lemma big_opMS_insert f X x :
@@ -679,12 +682,12 @@ Section gmultiset.
Lemma big_opMS_unit X : ([^o mset] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
Proof.
by induction X using gmultiset_ind;
- rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_eq.
+ rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_unseal.
Qed.
Lemma big_opMS_op f g X :
([^o mset] y ∈ X, f y `o` g y) ≡ ([^o mset] y ∈ X, f y) `o` ([^o mset] y ∈ X, g y).
- Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
+ Proof. by rewrite big_opMS_unseal /big_opMS_def -big_opL_op. Qed.
End gmultiset.
(** Commuting lemmas *)
diff --git a/iris/algebra/cmra_big_op.v b/iris/algebra/cmra_big_op.v
index 282094e776c595055e6b6f1c144de9211f32cd93..d88fef215c4254bc208f4ba2c864a2c794e226dd 100644
--- a/iris/algebra/cmra_big_op.v
+++ b/iris/algebra/cmra_big_op.v
@@ -13,7 +13,8 @@ Qed.
Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
Proof.
- induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
+ induction m as [|i x m ? IH] using map_ind=> /=.
+ { by rewrite big_opM_empty. }
rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
{ intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
intros Hm; split.
@@ -23,7 +24,8 @@ Qed.
Lemma big_opS_None {M : cmra} `{Countable A} (f : A → option M) X :
([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
- induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
+ induction X as [|x X ? IH] using set_ind_L.
+ { by rewrite big_opS_empty. }
rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
Qed.
Lemma big_opMS_None {M : cmra} `{Countable A} (f : A → option M) X :
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 1857deabf7c77c5fff97fbb9eba9f9a1b4e3e31d..a7a9657766ac14c20432a379342cd9660ce7c5af 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -623,7 +623,7 @@ Proof.
right order, namely the order in which they appear in map_to_list. Here,
we achieve this by unfolding [big_opM] and doing induction over that list
instead. *)
- rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
+ rewrite big_op.big_opM_unseal /big_op.big_opM_def -{2}(list_to_map_to_list m).
assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
intros [??]%NoDup_cons. rewrite IH //.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 57ef8b7c74cbee86d38df4cb8f0922b3c4769edc..62dda575a86a55b4a7cc7834643a2505e14b21b7 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -330,12 +330,13 @@ Next Obligation.
- apply (contractive_S f), IH; auto with lia.
Qed.
-Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
+Local Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
-Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
+Local Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Definition fixpoint := fixpoint_aux.(unseal).
Global Arguments fixpoint {A _ _} f {_}.
-Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
+Local Definition fixpoint_unseal :
+ @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Section fixpoint.
Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
@@ -346,7 +347,7 @@ Section fixpoint.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
apply equiv_dist=>n.
- rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
+ rewrite fixpoint_unseal /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
@@ -360,7 +361,7 @@ Section fixpoint.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
Proof.
- intros Hfg. rewrite fixpoint_eq /fixpoint_def
+ intros Hfg. rewrite fixpoint_unseal /fixpoint_def
(conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
rewrite Hfg; apply contractive_S, IH; auto using dist_S.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index f2f48b43a8c0a5d6faf0a3ef0123aae89886396c..bedddcc6806d3675a754b290dc455ba31e2cf71e 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -7,54 +7,56 @@ From iris.prelude Require Import options.
Export invGS.
Import uPred.
-Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Local Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
-Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
+Local Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Definition uPred_fupd := uPred_fupd_aux.(unseal).
Global Arguments uPred_fupd {Σ _}.
-Lemma uPred_fupd_eq `{!invGS Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Local Lemma uPred_fupd_unseal `{!invGS Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
Lemma uPred_fupd_mixin `{!invGS Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
split.
- - rewrite uPred_fupd_eq. solve_proper.
+ - rewrite uPred_fupd_unseal. solve_proper.
- intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
- rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
+ rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
by iIntros "($ & $ & HE) !> !> [$ $] !> !>" .
- - rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
- - rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
- - rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
+ - rewrite uPred_fupd_unseal.
+ iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
+ - rewrite uPred_fupd_unseal.
+ iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
+ - rewrite uPred_fupd_unseal. iIntros (E1 E2 E3 P) "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
- - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
+ - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
iIntros "!> !>". by iApply "HP".
- - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
+ - rewrite uPred_fupd_unseal /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
Global Instance uPred_bi_fupd `{!invGS Σ} : BiFUpd (uPredI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
Global Instance uPred_bi_bupd_fupd `{!invGS Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
-Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
+Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>". Qed.
Global Instance uPred_bi_fupd_plainly `{!invGS Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
Proof.
split.
- - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
+ - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
iAssert (â—‡ â– P)%I as "#>HP".
{ by iMod ("H" with "[$]") as "(_ & _ & HP)". }
by iFrame.
- - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
+ - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
iAssert (â—‡ â– P)%I as "#>HP".
{ by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
by iFrame.
- - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
+ - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
iAssert (â–· â—‡ â– P)%I as "#HP".
{ iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
iFrame. iIntros "!> !> !>". by iMod "HP".
- - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
+ - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
iAssert (◇ ■∀ x : A, Φ x)%I as "#>HP".
{ iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
by iFrame.
@@ -66,7 +68,7 @@ Proof.
iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
iAssert (|={⊤,E2}=> P)%I as "H".
{ iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. }
- rewrite uPred_fupd_eq /uPred_fupd_def.
+ rewrite uPred_fupd_unseal /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index c9f28145a4e306d55e53389c64ceac7f005c82bd..e81a22bc891b826a03b20247c1f35a9c36e59ae7 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -102,26 +102,27 @@ Section definitions.
ghost_map_auth (gen_heap_name hG) 1 σ ∗
ghost_map_auth (gen_meta_name hG) 1 m.
- Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
+ Local Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
l ↪[gen_heap_name hG]{dq} v.
- Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
+ Local 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).
+ Local Definition mapsto_unseal : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
- Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
+ Local Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
∃ γm, l ↪[gen_meta_name hG]□ γm ∗ own γm (reservation_map_token E).
- Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
+ Local Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
- Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
+ Local Definition meta_token_unseal :
+ @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
(** TODO: The use of [positives_flatten] violates the namespace abstraction
(see the proof of [meta_set]. *)
- Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
+ Local Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
∃ γm, l ↪[gen_meta_name hG]□ γm ∗
own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))).
- Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
+ Local Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta := meta_aux.(unseal).
- Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
+ Local Definition meta_unseal : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
@@ -147,37 +148,37 @@ Section gen_heap.
(** General properties of mapsto *)
Global Instance mapsto_timeless l dq v : Timeless (l ↦{dq} v).
- Proof. rewrite mapsto_eq. apply _. Qed.
+ Proof. rewrite mapsto_unseal. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
- Proof. rewrite mapsto_eq. apply _. Qed.
+ Proof. rewrite mapsto_unseal. apply _. Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
- Proof. rewrite mapsto_eq. apply _. Qed.
+ Proof. rewrite mapsto_unseal. apply _. Qed.
Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
- Proof. rewrite mapsto_eq. apply _. Qed.
+ Proof. rewrite mapsto_unseal. apply _. Qed.
Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dqâŒ%Qp.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_valid. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_valid. Qed.
Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 â‹… dq2) ∧ v1 = v2âŒ.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_valid_2. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_valid_2. Qed.
(** Almost all the time, this is all you really need. *)
Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2âŒ.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_agree. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_agree. Qed.
Lemma mapsto_combine l dq1 dq2 v1 v2 :
l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 â‹… dq2} v1 ∗ ⌜v1 = v2âŒ.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_combine. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_combine. Qed.
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ ✓(dq1 â‹… dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠l2âŒ.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_frac_ne. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_frac_ne. Qed.
Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠l2âŒ.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_ne. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_ne. Qed.
(** Permanently turn any points-to predicate into a persistent
points-to predicate. *)
Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
- Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
+ Proof. rewrite mapsto_unseal. apply ghost_map_elem_persist. Qed.
(** Framing support *)
Global Instance frame_mapsto p l v q1 q2 RES :
@@ -187,23 +188,23 @@ Section gen_heap.
(** General properties of [meta] and [meta_token] *)
Global Instance meta_token_timeless l N : Timeless (meta_token l N).
- Proof. rewrite meta_token_eq. apply _. Qed.
+ Proof. rewrite meta_token_unseal. apply _. Qed.
Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
- Proof. rewrite meta_eq. apply _. Qed.
+ Proof. rewrite meta_unseal. apply _. Qed.
Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
- Proof. rewrite meta_eq. apply _. Qed.
+ Proof. rewrite meta_unseal. apply _. Qed.
Lemma meta_token_union_1 l E1 E2 :
E1 ## E2 → meta_token l (E1 ∪ E2) -∗ meta_token l E1 ∗ meta_token l E2.
Proof.
- rewrite meta_token_eq /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
+ rewrite meta_token_unseal /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
iSplitL "Hm1"; eauto.
Qed.
Lemma meta_token_union_2 l E1 E2 :
meta_token l E1 -∗ meta_token l E2 -∗ meta_token l (E1 ∪ E2).
Proof.
- rewrite meta_token_eq /meta_token_def.
+ rewrite meta_token_unseal /meta_token_def.
iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
@@ -226,7 +227,7 @@ Section gen_heap.
Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
meta l i x1 -∗ meta l i x2 -∗ ⌜x1 = x2âŒ.
Proof.
- rewrite meta_eq /meta_def.
+ rewrite meta_unseal /meta_def.
iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
@@ -236,12 +237,13 @@ Section gen_heap.
Lemma meta_set `{Countable A} E l (x : A) N :
↑ N ⊆ E → meta_token l E ==∗ meta l N x.
Proof.
- rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
+ rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
iApply (own_update with "Hm").
apply reservation_map_alloc; last done.
cut (positives_flatten N ∈@{coPset} ↑N); first by set_solver.
- rewrite nclose_eq. apply elem_coPset_suffixes.
+ (* TODO: Avoid unsealing here. *)
+ rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
exists 1%positive. by rewrite left_id_L.
Qed.
@@ -250,7 +252,7 @@ Section gen_heap.
σ !! l = None →
gen_heap_interp σ ==∗ gen_heap_interp (<[l:=v]>σ) ∗ l ↦ v ∗ meta_token l ⊤.
Proof.
- iIntros (Hσl). rewrite /gen_heap_interp mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
+ iIntros (Hσl). rewrite /gen_heap_interp mapsto_unseal /mapsto_def meta_token_unseal /meta_token_def /=.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
iMod (own_alloc (reservation_map_token ⊤)) as (γm) "Hγm".
@@ -279,7 +281,7 @@ Section gen_heap.
Lemma gen_heap_valid σ l dq v : gen_heap_interp σ -∗ l ↦{dq} v -∗ ⌜σ !! l = Some vâŒ.
Proof.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
- rewrite /gen_heap_interp mapsto_eq.
+ rewrite /gen_heap_interp mapsto_unseal.
by iDestruct (ghost_map_lookup with "Hσ Hl") as %?.
Qed.
@@ -287,7 +289,7 @@ Section gen_heap.
gen_heap_interp σ -∗ l ↦ v1 ==∗ gen_heap_interp (<[l:=v2]>σ) ∗ l ↦ v2.
Proof.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
- iIntros "Hl". rewrite /gen_heap_interp mapsto_eq /mapsto_def.
+ iIntros "Hl". rewrite /gen_heap_interp mapsto_unseal /mapsto_def.
iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
iModIntro. iFrame "Hl". iExists m. iFrame.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index c0897fbdd0da01a89655fd6c44765c4daf5aaf59..5611fb729e7c5e405c768efd62e8eecc8f2bea13 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -26,17 +26,23 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{ghost_mapG Σ K V}.
- Definition ghost_map_auth_def (γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
+ Local Definition ghost_map_auth_def
+ (γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
own γ (gmap_view_auth (V:=leibnizO V) (DfracOwn q) m).
- Definition ghost_map_auth_aux : seal (@ghost_map_auth_def). Proof. by eexists. Qed.
+ Local Definition ghost_map_auth_aux : seal (@ghost_map_auth_def).
+ Proof. by eexists. Qed.
Definition ghost_map_auth := ghost_map_auth_aux.(unseal).
- Definition ghost_map_auth_eq : @ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).
+ Local Definition ghost_map_auth_unseal :
+ @ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).
- Definition ghost_map_elem_def (γ : gname) (k : K) (dq : dfrac) (v : V) : iProp Σ :=
+ Local Definition ghost_map_elem_def
+ (γ : gname) (k : K) (dq : dfrac) (v : V) : iProp Σ :=
own γ (gmap_view_frag (V:=leibnizO V) k dq v).
- Definition ghost_map_elem_aux : seal (@ghost_map_elem_def). Proof. by eexists. Qed.
+ Local Definition ghost_map_elem_aux : seal (@ghost_map_elem_def).
+ Proof. by eexists. Qed.
Definition ghost_map_elem := ghost_map_elem_aux.(unseal).
- Definition ghost_map_elem_eq : @ghost_map_elem = @ghost_map_elem_def := ghost_map_elem_aux.(seal_eq).
+ Local Definition ghost_map_elem_unseal :
+ @ghost_map_elem = @ghost_map_elem_def := ghost_map_elem_aux.(seal_eq).
End definitions.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
@@ -51,8 +57,8 @@ Notation "k ↪[ γ ]□ v" := (k ↪[γ]{DfracDiscarded} v)%I
(at level 20, γ at level 50) : bi_scope.
Local Ltac unseal := rewrite
- ?ghost_map_auth_eq /ghost_map_auth_def
- ?ghost_map_elem_eq /ghost_map_elem_def.
+ ?ghost_map_auth_unseal /ghost_map_auth_def
+ ?ghost_map_elem_unseal /ghost_map_elem_def.
Section lemmas.
Context `{ghost_mapG Σ K V}.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 2535b60c24d357e22d2eb5915fbf2affe13e22d3..937d9ac563166f83737f538546583b1b660bd822 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -19,14 +19,16 @@ Definition ghost_varΣ (A : Type) : gFunctors :=
Global Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
Proof. solve_inG. Qed.
-Definition ghost_var_def `{!ghost_varG Σ A} (γ : gname) (q : Qp) (a : A) : iProp Σ :=
+Local Definition ghost_var_def `{!ghost_varG Σ A}
+ (γ : gname) (q : Qp) (a : A) : iProp Σ :=
own γ (to_frac_agree (A:=leibnizO A) q a).
-Definition ghost_var_aux : seal (@ghost_var_def). Proof. by eexists. Qed.
+Local Definition ghost_var_aux : seal (@ghost_var_def). Proof. by eexists. Qed.
Definition ghost_var := ghost_var_aux.(unseal).
-Definition ghost_var_eq : @ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
+Local Definition ghost_var_unseal :
+ @ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
Global Arguments ghost_var {Σ A _} γ q a.
-Local Ltac unseal := rewrite ?ghost_var_eq /ghost_var_def.
+Local Ltac unseal := rewrite ?ghost_var_unseal /ghost_var_def.
Section lemmas.
Context `{!ghost_varG Σ A}.
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index a447486815982a59364f9b5bb0c334e62d0b8ca8..d13814d4085c6803ae8e08025e5523141349bd0d 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -7,12 +7,12 @@ From iris.prelude Require Import options.
Import uPred.
(** Semantic Invariants *)
-Definition inv_def `{!invGS Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Local Definition inv_def `{!invGS Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
□ ∀ E, ⌜↑N ⊆ E⌠→ |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
-Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
+Local Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv := inv_aux.(unseal).
Global Arguments inv {Σ _} N P.
-Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
+Local Definition inv_unseal : @inv = @inv_def := inv_aux.(seal_eq).
Global Instance: Params (@inv) 3 := {}.
(** * Invariants *)
@@ -30,7 +30,8 @@ Section inv.
Lemma own_inv_acc E N P :
↑N ⊆ E → own_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
- rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
+ rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
+ iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.
@@ -50,7 +51,8 @@ Section inv.
Lemma own_inv_alloc N E P : ▷ P ={E}=∗ own_inv N P.
Proof.
- rewrite uPred_fupd_eq. iIntros "HP [Hw $]".
+ rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
+ iIntros "HP [Hw $]".
iMod (ownI_alloc (.∈ (↑N : coPset)) P with "[$HP $Hw]")
as (i ?) "[$ ?]"; auto using fresh_inv_name.
do 2 iModIntro. iExists i. auto.
@@ -60,7 +62,8 @@ Section inv.
Lemma own_inv_alloc_open N E P :
↑N ⊆ E → ⊢ |={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
- rewrite uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
+ rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
+ iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open (.∈ (↑N : coPset)) P with "Hw")
as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
@@ -80,13 +83,13 @@ Section inv.
Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P.
Proof.
- iIntros "#I". rewrite inv_eq. iIntros (E H).
+ iIntros "#I". rewrite inv_unseal. iIntros (E H).
iPoseProof (own_inv_acc with "I") as "H"; eauto.
Qed.
(** ** Public API of invariants *)
Global Instance inv_contractive N : Contractive (inv N).
- Proof. rewrite inv_eq. solve_contractive. Qed.
+ Proof. rewrite inv_unseal. solve_contractive. Qed.
Global Instance inv_ne N : NonExpansive (inv N).
Proof. apply contractive_ne, _. Qed.
@@ -95,11 +98,11 @@ Section inv.
Proof. apply ne_proper, _. Qed.
Global Instance inv_persistent N P : Persistent (inv N P).
- Proof. rewrite inv_eq. apply _. Qed.
+ Proof. rewrite inv_unseal. apply _. Qed.
Lemma inv_alter N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
Proof.
- rewrite inv_eq. iIntros "#HI #HPQ !>" (E H).
+ rewrite inv_unseal. iIntros "#HI #HPQ !>" (E H).
iMod ("HI" $! E H) as "[HP Hclose]".
iDestruct ("HPQ" with "HP") as "[$ HQP]".
iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
@@ -129,7 +132,7 @@ Section inv.
Lemma inv_acc E N P :
↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
- rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
+ rewrite inv_unseal /inv_def; iIntros (?) "#HI". by iApply "HI".
Qed.
Lemma inv_combine N1 N2 N P Q :
@@ -137,7 +140,7 @@ Section inv.
↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
Proof.
- rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
+ rewrite inv_unseal. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
iApply fupd_mask_intro; first set_solver.
@@ -149,7 +152,7 @@ Section inv.
□ (P -∗ P ∗ P) -∗
inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
Proof.
- rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
+ rewrite inv_unseal. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
iMod ("HinvP" with "[//]") as "[HP HcloseP]".
iDestruct ("HPdup" with "HP") as "[$ HP]".
iMod ("HcloseP" with "HP") as %_.
@@ -165,7 +168,7 @@ Section inv.
(↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E)
(λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None).
Proof.
- rewrite inv_eq /IntoAcc /accessor bi.exist_unit.
+ rewrite inv_unseal /IntoAcc /accessor bi.exist_unit.
iIntros (?) "#Hinv _". iApply "Hinv"; done.
Qed.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 95d6555e1dfe71d49c217097fa12b9e538f2ea31..f093b3baff63b26cc562b1973978fce455fb924d 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -21,26 +21,27 @@ Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
Proof. solve_inG. Qed.
-Definition mono_nat_auth_own_def `{!mono_natG Σ}
+Local Definition mono_nat_auth_own_def `{!mono_natG Σ}
(γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (â—MN{#q} n).
-Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def). Proof. by eexists. Qed.
+Local Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def).
+Proof. by eexists. Qed.
Definition mono_nat_auth_own := mono_nat_auth_own_aux.(unseal).
-Definition mono_nat_auth_own_eq :
+Local Definition mono_nat_auth_own_unseal :
@mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).
Global Arguments mono_nat_auth_own {Σ _} γ q n.
-Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
+Local Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (◯MN n).
-Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists. Qed.
+Local Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists. Qed.
Definition mono_nat_lb_own := mono_nat_lb_own_aux.(unseal).
-Definition mono_nat_lb_own_eq :
+Local Definition mono_nat_lb_own_unseal :
@mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).
Global Arguments mono_nat_lb_own {Σ _} γ n.
Local Ltac unseal := rewrite
- ?mono_nat_auth_own_eq /mono_nat_auth_own_def
- ?mono_nat_lb_own_eq /mono_nat_lb_own_def.
+ ?mono_nat_auth_own_unseal /mono_nat_auth_own_def
+ ?mono_nat_lb_own_unseal /mono_nat_lb_own_def.
Section mono_nat.
Context `{!mono_natG Σ}.
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index f44547106efc60bd95e8088ff33bae219fed3c27..3d3e94de4be5160c686948dacd06ef55d49e18cc 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -48,12 +48,11 @@ Section definitions.
∃ R, ⌜proph_resolves_in_list R pvs ∧
dom R ⊆ ps⌠∗ ghost_map_auth (proph_map_name pG) 1 R.
- Definition proph_def (p : P) (vs : list V) : iProp Σ :=
+ Local Definition proph_def (p : P) (vs : list V) : iProp Σ :=
p ↪[proph_map_name pG] vs.
-
- Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
+ Local Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
Definition proph := proph_aux.(unseal).
- Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
+ Local Definition proph_unseal : @proph = @proph_def := proph_aux.(seal_eq).
End definitions.
Section list_resolves.
@@ -92,12 +91,12 @@ Section proph_map.
(** General properties of mapsto *)
Global Instance proph_timeless p vs : Timeless (proph p vs).
- Proof. rewrite proph_eq /proph_def. apply _. Qed.
+ Proof. rewrite proph_unseal /proph_def. apply _. Qed.
Lemma proph_exclusive p vs1 vs2 :
proph p vs1 -∗ proph p vs2 -∗ False.
Proof.
- rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
+ rewrite proph_unseal /proph_def. iIntros "Hp1 Hp2".
by iDestruct (ghost_map_elem_ne with "Hp1 Hp2") as %?.
Qed.
@@ -107,7 +106,7 @@ Section proph_map.
proph_map_interp pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
Proof.
iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] Hâ—]".
- rewrite proph_eq /proph_def.
+ rewrite proph_unseal /proph_def.
iMod (ghost_map_insert p (proph_list_resolves pvs p) with "Hâ—") as "[Hâ— Hâ—¯]".
{ apply not_elem_of_dom. set_solver. }
iModIntro. iFrame.
@@ -122,7 +121,7 @@ Section proph_map.
∃vs', ⌜vs = v::vs'⌠∗ proph_map_interp pvs ps ∗ proph p vs'.
Proof.
iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP Hâ—]". iDestruct "HP" as %[Hres Hdom].
- rewrite /proph_map_interp proph_eq /proph_def.
+ rewrite /proph_map_interp proph_unseal /proph_def.
iDestruct (ghost_map_lookup with "Hâ— Hp") as %HR.
assert (vs = v :: proph_list_resolves pvs p) as ->.
{ rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 6df52f94e3d0f32a7dd6976311b4380557e494b5..04a7712dcb7ac83c2921b055eee6c454946b3927 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -252,32 +252,34 @@ Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
Global Hint Resolve uPred_mono : uPred_def.
(** logical connectives *)
-Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
+Local Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
{| uPred_holds n x := φ |}.
Solve Obligations with done.
-Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
+Local Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
Definition uPred_pure := uPred_pure_aux.(unseal).
Global Arguments uPred_pure {M}.
-Definition uPred_pure_eq :
+Local Definition uPred_pure_unseal :
@uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
-Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
+Local Program Definition uPred_and_def {M} (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.
+Local Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
Definition uPred_and := uPred_and_aux.(unseal).
Global Arguments uPred_and {M}.
-Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
+Local Definition uPred_and_unseal :
+ @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
-Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
+Local Program Definition uPred_or_def {M} (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.
+Local Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
Definition uPred_or := uPred_or_aux.(unseal).
Global Arguments uPred_or {M}.
-Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
+Local Definition uPred_or_unseal :
+ @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
-Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
+Local Program Definition uPred_impl_def {M} (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.
@@ -285,51 +287,54 @@ Next Obligation.
rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc.
Qed.
-Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
+Local Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
Definition uPred_impl := uPred_impl_aux.(unseal).
Global Arguments uPred_impl {M}.
-Definition uPred_impl_eq :
+Local Definition uPred_impl_unseal :
@uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
-Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
+Local Program Definition uPred_forall_def {M 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.
+Local Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
Definition uPred_forall := uPred_forall_aux.(unseal).
Global Arguments uPred_forall {M A}.
-Definition uPred_forall_eq :
+Local Definition uPred_forall_unseal :
@uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
-Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
+Local Program Definition uPred_exist_def {M 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.
+Local Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
Definition uPred_exist := uPred_exist_aux.(unseal).
Global Arguments uPred_exist {M A}.
-Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
+Local Definition uPred_exist_unseal :
+ @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
-Program Definition uPred_internal_eq_def {M} {A : ofe} (a1 a2 : A) : uPred M :=
+Local Program Definition uPred_internal_eq_def {M} {A : ofe} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using dist_le.
-Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
+Local Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def).
+Proof. by eexists. Qed.
Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
Global Arguments uPred_internal_eq {M A}.
-Definition uPred_internal_eq_eq:
+Local Definition uPred_internal_eq_unseal :
@uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
-Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
+Local Program Definition uPred_sep_def {M} (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 M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
exists x1, (x2 â‹… z); split_and?; eauto using uPred_mono, cmra_includedN_l.
rewrite Hy. eapply dist_le, Hn. by rewrite Hx assoc.
Qed.
-Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
+Local Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
Definition uPred_sep := uPred_sep_aux.(unseal).
Global Arguments uPred_sep {M}.
-Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
+Local Definition uPred_sep_unseal :
+ @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
-Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
+Local Program Definition uPred_wand_def {M} (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.
@@ -337,66 +342,68 @@ Next Obligation.
eapply uPred_mono with n3 (x1 â‹… x3);
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
-Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
+Local Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
Definition uPred_wand := uPred_wand_aux.(unseal).
Global Arguments uPred_wand {M}.
-Definition uPred_wand_eq :
+Local Definition uPred_wand_unseal :
@uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_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 {M} (P : uPred M) : uPred M :=
+Local Program Definition uPred_plainly_def {M} (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.
+Local Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
Definition uPred_plainly := uPred_plainly_aux.(unseal).
Global Arguments uPred_plainly {M}.
-Definition uPred_plainly_eq :
+Local Definition uPred_plainly_unseal :
@uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
-Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
+Local Program Definition uPred_persistently_def {M} (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.
+Local Definition uPred_persistently_aux : seal (@uPred_persistently_def).
+Proof. by eexists. Qed.
Definition uPred_persistently := uPred_persistently_aux.(unseal).
Global Arguments uPred_persistently {M}.
-Definition uPred_persistently_eq :
+Local Definition uPred_persistently_unseal :
@uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
-Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
+Local Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation.
intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
Qed.
-Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
+Local Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
Definition uPred_later := uPred_later_aux.(unseal).
Global Arguments uPred_later {M}.
-Definition uPred_later_eq :
+Local Definition uPred_later_unseal :
@uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
-Program Definition uPred_ownM_def {M : ucmra} (a : M) : uPred M :=
+Local Program Definition uPred_ownM_def {M : ucmra} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
Next Obligation.
intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn.
exists (a' â‹… x2). rewrite Hx. eapply dist_le, Hn. rewrite (assoc op) -Hx1 //.
Qed.
-Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
+Local Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
Definition uPred_ownM := uPred_ownM_aux.(unseal).
Global Arguments uPred_ownM {M}.
-Definition uPred_ownM_eq :
+Local Definition uPred_ownM_unseal :
@uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
-Program Definition uPred_cmra_valid_def {M} {A : cmra} (a : A) : uPred M :=
+Local Program Definition uPred_cmra_valid_def {M} {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.
+Local Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def).
+Proof. by eexists. Qed.
Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
Global Arguments uPred_cmra_valid {M A}.
-Definition uPred_cmra_valid_eq :
+Local Definition uPred_cmra_valid_unseal :
@uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
-Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
+Local Program Definition uPred_bupd_def {M} (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.
@@ -406,10 +413,10 @@ Next Obligation.
exists (x' â‹… x3); split; first by rewrite -assoc.
eauto using uPred_mono, cmra_includedN_l.
Qed.
-Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
+Local Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
Definition uPred_bupd := uPred_bupd_aux.(unseal).
Global Arguments uPred_bupd {M}.
-Definition uPred_bupd_eq :
+Local Definition uPred_bupd_unseal :
@uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
(** Global uPred-specific Notation *)
@@ -419,13 +426,14 @@ Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
These are not directly usable later because they do not refer to the BI
connectives. *)
Module uPred_primitive.
-Definition unseal_eqs :=
- (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
- uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
- uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
- uPred_cmra_valid_eq, @uPred_bupd_eq).
+Definition uPred_unseal :=
+ (uPred_pure_unseal, uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
+ uPred_forall_unseal, uPred_exist_unseal, uPred_internal_eq_unseal,
+ uPred_sep_unseal, uPred_wand_unseal, uPred_plainly_unseal,
+ uPred_persistently_unseal, uPred_later_unseal, uPred_ownM_unseal,
+ uPred_cmra_valid_unseal, @uPred_bupd_unseal).
Ltac unseal :=
- rewrite !unseal_eqs /=.
+ rewrite !uPred_unseal /=.
Section primitive.
Context {M : ucmra}.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 3eb8e275077ada0e4b4092af57f1b803dca2af08..e31916ec5c56af247daf34b44a99e28b46639b28 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -54,14 +54,14 @@ Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
(big_sepL2 (λ _ x1 x2, P%I) l1 l2) : bi_scope.
-Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
+Local Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
(Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
(⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌠∧
[∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
-Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
+Local Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
Definition big_sepM2 := big_sepM2_aux.(unseal).
Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
-Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
+Local Definition big_sepM2_unseal : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
Global Instance: Params (@big_sepM2) 6 := {}.
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
(big_sepM2 (λ k x1 x2, P%I) m1 m2) : bi_scope.
@@ -1260,19 +1260,6 @@ Section sep_map.
Implicit Types m : gmap K A.
Implicit Types Φ Ψ : K → A → PROP.
- (* We place the [Affine] instance after [m1] and [m2], so that
- manually instantiating [m1] or [m2] in [iApply] does not also
- implicitly instantiate the [Affine] instance. If it gets
- instantiated too early, [Φ] is not known, and typeclass inference
- fails. *)
- Lemma big_sepM_subseteq Φ m1 m2 `{!∀ k x, Affine (Φ k x)} :
- m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x.
- Proof.
- assert (∀ kx, Affine (uncurry Φ kx)) by (intros []; apply _).
- rewrite big_opM_eq. intros.
- by apply (big_sepL_submseteq _), map_to_list_submseteq.
- Qed.
-
(** The lemmas [big_sepM_mono], [big_sepM_ne] and [big_sepM_proper] are more
generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_sepM_mono Φ Ψ m :
@@ -1297,24 +1284,47 @@ Section sep_map.
Global Instance big_sepM_empty_persistent Φ :
Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
- Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+ Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_sepM_persistent Φ m :
(∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
- Proof. rewrite big_opM_eq. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
+ Proof.
+ induction m using map_ind;
+ [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+ Qed.
Global Instance big_sepM_empty_affine Φ :
Affine ([∗ map] k↦x ∈ ∅, Φ k x).
- Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+ Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_sepM_affine Φ m :
(∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x).
- Proof. rewrite big_opM_eq. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
+ Proof.
+ induction m using map_ind;
+ [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+ Qed.
Global Instance big_sepM_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
- Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+ Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
(∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
- Proof. rewrite big_opM_eq. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
+ Proof.
+ induction m using map_ind;
+ [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+ Qed.
+
+ (* We place the [Affine] instance after [m1] and [m2], so that
+ manually instantiating [m1] or [m2] in [iApply] does not also
+ implicitly instantiate the [Affine] instance. If it gets
+ instantiated too early, [Φ] is not known, and typeclass inference
+ fails. *)
+ Lemma big_sepM_subseteq Φ m1 m2 `{!∀ k x, Affine (Φ k x)} :
+ m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x.
+ Proof.
+ intros ?. rewrite -(map_difference_union m2 m1) //.
+ rewrite big_opM_union; last by apply map_disjoint_difference_r.
+ assert (∀ kx, Affine (uncurry Φ kx)) by (intros []; apply _).
+ by rewrite sep_elim_l.
+ Qed.
Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ emp.
Proof. by rewrite big_opM_empty. Qed.
@@ -1668,10 +1678,6 @@ Section and_map.
Implicit Types m : gmap K A.
Implicit Types Φ Ψ : K → A → PROP.
- Lemma big_andM_subseteq Φ m1 m2 :
- m2 ⊆ m1 → ([∧ map] k ↦ x ∈ m1, Φ k x) ⊢ [∧ map] k ↦ x ∈ m2, Φ k x.
- Proof. rewrite big_opM_eq. intros. by apply big_andL_submseteq, map_to_list_submseteq. Qed.
-
(** The lemmas [big_andM_mono], [big_andM_ne] and [big_andM_proper] are more
generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_andM_mono Φ Ψ m :
@@ -1696,17 +1702,31 @@ Section and_map.
Global Instance big_andM_empty_persistent Φ :
Persistent ([∧ map] k↦x ∈ ∅, Φ k x).
- Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+ Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_andM_persistent Φ m :
(∀ k x, Persistent (Φ k x)) → Persistent ([∧ map] k↦x ∈ m, Φ k x).
- Proof. rewrite big_opM_eq. intros. apply big_andL_persistent=> _ [??]; apply _. Qed.
+ Proof.
+ induction m using map_ind;
+ [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+ Qed.
Global Instance big_andM_empty_timeless Φ :
Timeless ([∧ map] k↦x ∈ ∅, Φ k x).
- Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty /=. apply _. Qed.
+ Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_andM_timeless Φ m :
(∀ k x, Timeless (Φ k x)) → Timeless ([∧ map] k↦x ∈ m, Φ k x).
- Proof. rewrite big_opM_eq. intros. apply big_andL_timeless=> _ [??]; apply _. Qed.
+ Proof.
+ induction m using map_ind;
+ [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+ Qed.
+
+ Lemma big_andM_subseteq Φ m1 m2 :
+ m2 ⊆ m1 → ([∧ map] k ↦ x ∈ m1, Φ k x) ⊢ [∧ map] k ↦ x ∈ m2, Φ k x.
+ Proof.
+ intros ?. rewrite -(map_difference_union m2 m1) //.
+ rewrite big_opM_union; last by apply map_disjoint_difference_r.
+ by rewrite and_elim_l.
+ Qed.
Lemma big_andM_empty Φ : ([∧ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
Proof. by rewrite big_opM_empty. Qed.
@@ -1859,7 +1879,7 @@ Lemma big_sepM2_alt `{Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢
⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌠∧
[∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
-Proof. by rewrite big_sepM2_eq. Qed.
+Proof. by rewrite big_sepM2_unseal. Qed.
Section map2.
Context `{Countable K} {A B : Type}.
@@ -1868,7 +1888,7 @@ Section map2.
Lemma big_sepM2_lookup_iff Φ m1 m2 :
([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) âŒ.
- Proof. by rewrite big_sepM2_eq /big_sepM2_def and_elim_l. Qed.
+ Proof. by rewrite big_sepM2_alt and_elim_l. Qed.
Lemma big_sepM2_dom Φ m1 m2 :
([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
@@ -1881,15 +1901,14 @@ Section map2.
Lemma big_sepM2_flip Φ m1 m2 :
([∗ map] k↦y1;y2 ∈ m2; m1, Φ k y2 y1) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2).
Proof.
- rewrite big_sepM2_eq /big_sepM2_def.
- apply and_proper; [apply pure_proper; naive_solver |].
+ rewrite !big_sepM2_alt. apply and_proper; [apply pure_proper; naive_solver |].
rewrite -map_zip_with_flip map_zip_with_map_zip big_sepM_fmap.
apply big_sepM_proper. by intros k [b a].
Qed.
Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
Proof.
- rewrite big_sepM2_eq /big_sepM2_def big_opM_eq pure_True ?left_id //.
+ rewrite big_sepM2_alt map_zip_with_empty big_sepM_empty pure_True ?left_id //.
intros k. rewrite !lookup_empty; split; by inversion 1.
Qed.
Lemma big_sepM2_empty' P `{!Affine P} Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
@@ -1901,7 +1920,7 @@ Section map2.
(∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
Proof.
- intros Hm1m2. rewrite big_sepM2_eq /big_sepM2_def.
+ intros Hm1m2. rewrite !big_sepM2_alt.
apply and_mono_r, big_sepM_mono.
intros k [x1 x2]. rewrite map_lookup_zip_with.
specialize (Hm1m2 k x1 x2).
@@ -1913,7 +1932,7 @@ Section map2.
(∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ≡{n}≡ Ψ k y1 y2) →
([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2)%I.
Proof.
- intros Hm1m2. rewrite big_sepM2_eq /big_sepM2_def.
+ intros Hm1m2. rewrite !big_sepM2_alt.
f_equiv. apply big_sepM_ne=> k [x1 x2]. rewrite map_lookup_zip_with.
specialize (Hm1m2 k x1 x2).
destruct (m1 !! k) as [y1|]; last done.
@@ -1935,7 +1954,7 @@ Section map2.
Φ k y1 y2 ⊣⊢ Ψ k y1' y2') →
([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊣⊢ [∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2.
Proof.
- intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+ intros Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
{ f_equiv; split; intros Hm k.
- trans (is_Some (m1 !! k)); [symmetry; apply is_Some_proper; by f_equiv|].
rewrite Hm. apply is_Some_proper; by f_equiv.
@@ -1966,7 +1985,7 @@ Section map2.
Global Instance big_sepM2_persistent Φ m1 m2 :
(∀ k x1 x2, Persistent (Φ k x1 x2)) →
Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
- Proof. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
+ Proof. rewrite big_sepM2_alt. apply _. Qed.
Global Instance big_sepM2_empty_affine Φ :
Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
@@ -1974,15 +1993,15 @@ Section map2.
Global Instance big_sepM2_affine Φ m1 m2 :
(∀ k x1 x2, Affine (Φ k x1 x2)) →
Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
- Proof. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
+ Proof. rewrite big_sepM2_alt. apply _. Qed.
Global Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
- Proof. rewrite big_sepM2_eq /big_sepM2_def map_zip_with_empty. apply _. Qed.
+ Proof. rewrite big_sepM2_alt map_zip_with_empty. apply _. Qed.
Global Instance big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
(∀ k x1 x2, Timeless (Φ k x1 x2)) →
Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
- Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
+ Proof. intros. rewrite big_sepM2_alt. apply _. Qed.
Lemma big_sepM2_empty_l m1 Φ : ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅âŒ.
Proof.
@@ -2001,7 +2020,7 @@ Section map2.
([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
Proof.
- intros Hm1 Hm2. rewrite big_sepM2_eq /big_sepM2_def -map_insert_zip_with.
+ intros Hm1 Hm2. rewrite !big_sepM2_alt -map_insert_zip_with.
rewrite big_sepM_insert;
last by rewrite map_lookup_zip_with Hm1.
rewrite !persistent_and_affinely_sep_l /=.
@@ -2022,7 +2041,7 @@ Section map2.
([∗ map] k↦x;y ∈ m1;m2, Φ k x y) ⊣⊢
Φ i x1 x2 ∗ [∗ map] k↦x;y ∈ delete i m1;delete i m2, Φ k x y.
Proof.
- rewrite big_sepM2_eq /big_sepM2_def => Hx1 Hx2.
+ rewrite !big_sepM2_alt=> Hx1 Hx2.
rewrite !persistent_and_affinely_sep_l /=.
rewrite sep_assoc (sep_comm (Φ _ _ _)) -sep_assoc.
apply sep_proper.
@@ -2044,11 +2063,11 @@ Section map2.
(Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
Proof.
intros Hm1. apply (anti_symm _).
- - rewrite big_sepM2_eq /big_sepM2_def. apply pure_elim_l=> Hm.
+ - rewrite big_sepM2_alt. apply pure_elim_l=> Hm.
assert (is_Some (m2 !! i)) as [x2 Hm2].
{ apply Hm. by econstructor. }
rewrite -(exist_intro x2).
- rewrite (big_sepM_delete _ _ i (x1,x2)) /=;
+ rewrite big_sepM2_alt (big_sepM_delete _ _ i (x1,x2)) /=;
last by rewrite map_lookup_zip_with Hm1 Hm2.
rewrite pure_True // left_id.
f_equiv. apply and_intro.
@@ -2064,12 +2083,12 @@ Section map2.
(Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
Proof.
intros Hm2. apply (anti_symm _).
- - rewrite big_sepM2_eq /big_sepM2_def.
+ - rewrite big_sepM2_alt.
apply pure_elim_l=> Hm.
assert (is_Some (m1 !! i)) as [x1 Hm1].
{ apply Hm. by econstructor. }
rewrite -(exist_intro x1).
- rewrite (big_sepM_delete _ _ i (x1,x2)) /=;
+ rewrite big_sepM2_alt (big_sepM_delete _ _ i (x1,x2)) /=;
last by rewrite map_lookup_zip_with Hm1 Hm2.
rewrite pure_True // left_id.
f_equiv. apply and_intro.
@@ -2095,7 +2114,8 @@ Section map2.
Proof.
intros ??. rewrite {1}big_sepM2_delete //. apply sep_mono; [done|].
apply forall_intro=> x1'. apply forall_intro=> x2'.
- rewrite -(insert_delete_insert m1) -(insert_delete_insert m2) big_sepM2_insert ?lookup_delete //.
+ rewrite -(insert_delete_insert m1) -(insert_delete_insert m2)
+ big_sepM2_insert ?lookup_delete //.
by apply wand_intro_l.
Qed.
@@ -2105,7 +2125,7 @@ Section map2.
([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2).
Proof.
- rewrite big_sepM2_eq /big_sepM2_def.
+ rewrite !big_sepM2_alt.
assert (TCOr (∀ x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
{ destruct select (TCOr _ _); apply _. }
apply wand_intro_r.
@@ -2158,7 +2178,7 @@ Section map2.
Lemma big_sepM2_singleton Φ i x1 x2 :
([∗ map] k↦y1;y2 ∈ {[ i := x1 ]}; {[ i := x2 ]}, Φ k y1 y2) ⊣⊢ Φ i x1 x2.
Proof.
- rewrite big_sepM2_eq /big_sepM2_def.
+ rewrite big_sepM2_alt.
rewrite map_zip_with_singleton big_sepM_singleton.
apply (anti_symm _).
- apply and_elim_r.
@@ -2172,7 +2192,7 @@ Section map2.
([∗ map] k↦y1;y2 ∈ f <$> m1; g <$> m2, Φ k y1 y2)
⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) (g y2)).
Proof.
- rewrite big_sepM2_eq /big_sepM2_def. rewrite map_fmap_zip.
+ rewrite !big_sepM2_alt. rewrite map_fmap_zip.
apply and_proper.
- setoid_rewrite lookup_fmap. by setoid_rewrite fmap_is_Some.
- by rewrite big_sepM_fmap.
@@ -2192,7 +2212,7 @@ Section map2.
([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∗ Ψ k y1 y2)
⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
Proof.
- rewrite big_sepM2_eq /big_sepM2_def.
+ rewrite !big_sepM2_alt.
rewrite -{1}(idemp bi_and ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)âŒ%I).
rewrite -assoc.
rewrite !persistent_and_affinely_sep_l /=.
@@ -2216,7 +2236,7 @@ Section map2.
([∗ map] k↦y1;y2 ∈ m1;m2, ⌜φ k y1 y2âŒ) ⊢@{PROP}
⌜∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → φ k y1 y2âŒ.
Proof.
- rewrite big_sepM2_eq /big_sepM2_def.
+ rewrite big_sepM2_alt.
rewrite big_sepM_pure_1 -pure_and.
f_equiv=>-[Hdom Hforall] k y1 y2 Hy1 Hy2.
eapply (Hforall k (y1, y2)). clear Hforall.
@@ -2228,7 +2248,7 @@ Section map2.
([∗ map] k↦y1;y2 ∈ m1;m2, <affine> ⌜φ k y1 y2âŒ).
Proof.
intros Hdom.
- rewrite big_sepM2_eq /big_sepM2_def.
+ rewrite big_sepM2_alt.
rewrite -big_sepM_affinely_pure_2.
rewrite affinely_and_r -pure_and. f_equiv. f_equiv=>-Hforall.
split; first done.
@@ -2255,8 +2275,8 @@ Section map2.
<pers> ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
⊣⊢ [∗ map] k↦y1;y2 ∈ m1;m2, <pers> (Φ k y1 y2).
Proof.
- by rewrite big_sepM2_eq /big_sepM2_def persistently_and
- persistently_pure big_sepM_persistently.
+ by rewrite !big_sepM2_alt persistently_and
+ persistently_pure big_sepM_persistently.
Qed.
Lemma big_sepM2_intro Φ m1 m2 :
@@ -2264,7 +2284,7 @@ Section map2.
□ (∀ k x1 x2, ⌜m1 !! k = Some x1⌠→ ⌜m2 !! k = Some x2⌠→ Φ k x1 x2) ⊢
[∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
Proof.
- intros. rewrite big_sepM2_eq /big_sepM2_def.
+ intros. rewrite big_sepM2_alt.
apply and_intro; [by apply pure_intro|].
rewrite -big_sepM_intro. f_equiv; f_equiv=> k.
apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
@@ -2283,7 +2303,7 @@ Section map2.
{ apply and_intro; [apply big_sepM2_lookup_iff|].
apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepM2_lookup. }
- apply pure_elim_l=> Hdom. rewrite big_sepM2_eq /big_sepM2_def.
+ apply pure_elim_l=> Hdom. rewrite big_sepM2_alt.
apply and_intro; [by apply pure_intro|].
rewrite big_sepM_forall. f_equiv=> k.
apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
@@ -2339,7 +2359,7 @@ Section map2.
(▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
Proof.
- rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_âŒ).
+ rewrite !big_sepM2_alt later_and (timeless ⌜_âŒ).
rewrite big_sepM_later except_0_and.
auto using and_mono_r, except_0_intro.
Qed.
@@ -2347,7 +2367,7 @@ Section map2.
([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
Proof.
- rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_âŒ).
+ rewrite !big_sepM2_alt later_and -(later_intro ⌜_âŒ).
apply and_mono_r. by rewrite big_opM_commute.
Qed.
@@ -2435,7 +2455,7 @@ Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2)%I.
Proof.
- intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+ intros Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
{ f_equiv; split; intros Hm k.
- trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
rewrite Hm. apply: is_Some_ne; by f_equiv.
@@ -2452,14 +2472,6 @@ Section gset.
Implicit Types X : gset A.
Implicit Types Φ : A → PROP.
- (* See comment above [big_sepM_subseteq] as for why the [Affine]
- instance is placed late. *)
- Lemma big_sepS_subseteq Φ X Y `{!∀ x, Affine (Φ x)} :
- Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x.
- Proof.
- rewrite big_opS_eq. intros. by apply big_sepL_submseteq, elements_submseteq.
- Qed.
-
(** The lemmas [big_sepS_mono], [big_sepS_ne] and [big_sepS_proper] are more
generic than the instances as they also give [x ∈ X] in the premise. *)
Lemma big_sepS_mono Φ Ψ X :
@@ -2483,23 +2495,41 @@ Section gset.
Global Instance big_sepS_empty_persistent Φ :
Persistent ([∗ set] x ∈ ∅, Φ x).
- Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
+ Proof. rewrite big_opS_empty. apply _. Qed.
Global Instance big_sepS_persistent Φ X :
(∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
- Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
+ Proof.
+ induction X using set_ind_L;
+ [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
+ Qed.
Global Instance big_sepS_empty_affine Φ : Affine ([∗ set] x ∈ ∅, Φ x).
- Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
+ Proof. rewrite big_opS_empty. apply _. Qed.
Global Instance big_sepS_affine Φ X :
(∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
- Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
+ Proof.
+ induction X using set_ind_L;
+ [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
+ Qed.
Global Instance big_sepS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([∗ set] x ∈ ∅, Φ x).
- Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
+ Proof. rewrite big_opS_empty. apply _. Qed.
Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
(∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
- Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
+ Proof.
+ induction X using set_ind_L;
+ [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
+ Qed.
+
+ (* See comment above [big_sepM_subseteq] as for why the [Affine]
+ instance is placed late. *)
+ Lemma big_sepS_subseteq Φ X Y `{!∀ x, Affine (Φ x)} :
+ Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x.
+ Proof.
+ intros ->%union_difference_L. rewrite big_opS_union; last set_solver.
+ by rewrite sep_elim_l.
+ Qed.
Lemma big_sepS_elements Φ X :
([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ list] x ∈ elements X, Φ x).
@@ -2778,15 +2808,6 @@ Section gmultiset.
Implicit Types X : gmultiset A.
Implicit Types Φ : A → PROP.
- (* See comment above [big_sepM_subseteq] as for why the [Affine]
- instance is placed late. *)
- Lemma big_sepMS_subseteq Φ X Y `{!∀ x, Affine (Φ x)} :
- Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
- Proof.
- intros. rewrite big_opMS_eq.
- by apply big_sepL_submseteq, gmultiset_elements_submseteq.
- Qed.
-
(** The lemmas [big_sepMS_mono], [big_sepMS_ne] and [big_sepMS_proper] are more
generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_sepMS_mono Φ Ψ X :
@@ -2810,23 +2831,41 @@ Section gmultiset.
Global Instance big_sepMS_empty_persistent Φ :
Persistent ([∗ mset] x ∈ ∅, Φ x).
- Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
+ Proof. rewrite big_opMS_empty. apply _. Qed.
Global Instance big_sepMS_persistent Φ X :
(∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
- Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
+ Proof.
+ induction X using gmultiset_ind;
+ [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
+ Qed.
Global Instance big_sepMS_empty_affine Φ : Affine ([∗ mset] x ∈ ∅, Φ x).
- Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
+ Proof. rewrite big_opMS_empty. apply _. Qed.
Global Instance big_sepMS_affine Φ X :
(∀ x, Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
- Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
+ Proof.
+ induction X using gmultiset_ind;
+ [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
+ Qed.
Global Instance big_sepMS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([∗ mset] x ∈ ∅, Φ x).
- Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
+ Proof. rewrite big_opMS_empty. apply _. Qed.
Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
(∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
- Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
+ Proof.
+ induction X using gmultiset_ind;
+ [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
+ Qed.
+
+ (* See comment above [big_sepM_subseteq] as for why the [Affine]
+ instance is placed late. *)
+ Lemma big_sepMS_subseteq Φ X Y `{!∀ x, Affine (Φ x)} :
+ Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
+ Proof.
+ intros ->%gmultiset_disj_union_difference.
+ by rewrite big_opMS_disj_union sep_elim_l.
+ Qed.
Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ emp.
Proof. by rewrite big_opMS_empty. Qed.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index c4d27aadf0699486daeff49abbdb39dbd3b8cdab..d9eef29303bf81f5e8d3f89554f189038d0b6534 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -80,16 +80,18 @@ Section definition.
- intros ??. solve_proper.
Qed.
- Definition atomic_update_def :=
+ Local Definition atomic_update_def :=
bi_greatest_fixpoint atomic_update_pre ().
End definition.
(** Seal it *)
-Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
+Local Definition atomic_update_aux : seal (@atomic_update_def).
+Proof. by eexists. Qed.
Definition atomic_update := atomic_update_aux.(unseal).
Global Arguments atomic_update {PROP _ TA TB}.
-Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
+Local Definition atomic_update_unseal :
+ @atomic_update = _ := atomic_update_aux.(seal_eq).
Global Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
Global Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
@@ -223,14 +225,14 @@ Section lemmas.
dist n
) (atomic_update (PROP:=PROP) Eo Ei).
Proof.
- rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
+ rewrite atomic_update_unseal /atomic_update_def /atomic_update_pre. solve_proper.
Qed.
Lemma atomic_update_mask_weaken Eo1 Eo2 Ei α β Φ :
Eo1 ⊆ Eo2 →
atomic_update Eo1 Ei α β Φ -∗ atomic_update Eo2 Ei α β Φ.
Proof.
- rewrite atomic_update_eq {2}/atomic_update_def /=.
+ rewrite atomic_update_unseal {2}/atomic_update_def /=.
iIntros (Heo) "HAU".
iApply (greatest_fixpoint_coiter _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
@@ -243,7 +245,7 @@ Section lemmas.
atomic_update Eo Ei α β Φ -∗
atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
Proof using Type*.
- rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
+ rewrite atomic_update_unseal {1}/atomic_update_def /=. iIntros "HUpd".
iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
iDestruct (make_laterable_elim with "HUpd") as ">?". done.
Qed.
@@ -267,7 +269,7 @@ Section lemmas.
Global Instance aupd_laterable Eo Ei α β Φ :
Laterable (atomic_update Eo Ei α β Φ).
Proof.
- rewrite atomic_update_eq {1}/atomic_update_def greatest_fixpoint_unfold.
+ rewrite atomic_update_unseal {1}/atomic_update_def greatest_fixpoint_unfold.
apply _.
Qed.
@@ -276,7 +278,7 @@ Section lemmas.
(P ∗ Q -∗ atomic_acc Eo Ei α Q β Φ) →
P ∗ Q -∗ atomic_update Eo Ei α β Φ.
Proof.
- rewrite atomic_update_eq {1}/atomic_update_def /=.
+ rewrite atomic_update_unseal {1}/atomic_update_def /=.
iIntros (??? HAU) "[#HP HQ]".
iApply (greatest_fixpoint_coiter _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> HQ".
@@ -460,7 +462,7 @@ Section proof_mode.
envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) →
envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
Proof.
- intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
+ intros ? HΓs ->. rewrite environments.envs_entails_unseal of_envs_eq' /atomic_acc /=.
setoid_rewrite env_to_prop_sound =>HAU.
apply aupd_intro; [apply _..|]. done.
Qed.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index d54c3a8aa45bea7d5e64917644c52036e3776d0c..bde99d57480db8b42c97048f19f73ea514c415ca 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -126,97 +126,127 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
MonPred (λ i, (∀ j, ⌜i ⊑ j⌠→ Φ j)%I) _.
Next Obligation. solve_proper. Qed.
-Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP), MonPred (λ _, P) _.
-Definition monPred_embed_aux : seal (@monPred_embed_def). Proof. by eexists. Qed.
+Local Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP),
+ MonPred (λ _, P) _.
+Local Definition monPred_embed_aux : seal (@monPred_embed_def).
+Proof. by eexists. Qed.
Definition monPred_embed := monPred_embed_aux.(unseal).
-Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
+Local Definition monPred_embed_unseal :
+ @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
-Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
-Definition monPred_emp_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
+Local Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
+Local Definition monPred_emp_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
Definition monPred_emp := monPred_emp_aux.(unseal).
-Definition monPred_emp_eq : @monPred_emp = _ := monPred_emp_aux.(seal_eq).
+Local Definition monPred_emp_unseal :
+ @monPred_emp = _ := monPred_emp_aux.(seal_eq).
-Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φâŒ)%I _.
-Definition monPred_pure_aux : seal (@monPred_pure_def). Proof. by eexists. Qed.
+Local Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φâŒ)%I _.
+Local Definition monPred_pure_aux : seal (@monPred_pure_def).
+Proof. by eexists. Qed.
Definition monPred_pure := monPred_pure_aux.(unseal).
-Definition monPred_pure_eq : @monPred_pure = _ := monPred_pure_aux.(seal_eq).
+Local Definition monPred_pure_unseal :
+ @monPred_pure = _ := monPred_pure_aux.(seal_eq).
-Definition monPred_objectively_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
-Definition monPred_objectively_aux : seal (@monPred_objectively_def). Proof. by eexists. Qed.
+Local Definition monPred_objectively_def P : monPred :=
+ MonPred (λ _, ∀ i, P i)%I _.
+Local Definition monPred_objectively_aux : seal (@monPred_objectively_def).
+Proof. by eexists. Qed.
Definition monPred_objectively := monPred_objectively_aux.(unseal).
-Definition monPred_objectively_eq : @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).
+Local Definition monPred_objectively_unseal :
+ @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).
-Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
-Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). Proof. by eexists. Qed.
+Local Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
+Local Definition monPred_subjectively_aux : seal (@monPred_subjectively_def).
+Proof. by eexists. Qed.
Definition monPred_subjectively := monPred_subjectively_aux.(unseal).
-Definition monPred_subjectively_eq : @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).
+Local Definition monPred_subjectively_unseal :
+ @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).
-Program Definition monPred_and_def P Q : monPred :=
+Local Program Definition monPred_and_def P Q : monPred :=
MonPred (λ i, P i ∧ Q i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_and_aux : seal (@monPred_and_def). Proof. by eexists. Qed.
+Local Definition monPred_and_aux : seal (@monPred_and_def).
+Proof. by eexists. Qed.
Definition monPred_and := monPred_and_aux.(unseal).
-Definition monPred_and_eq : @monPred_and = _ := monPred_and_aux.(seal_eq).
+Local Definition monPred_and_unseal :
+ @monPred_and = _ := monPred_and_aux.(seal_eq).
-Program Definition monPred_or_def P Q : monPred :=
+Local Program Definition monPred_or_def P Q : monPred :=
MonPred (λ i, P i ∨ Q i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_or_aux : seal (@monPred_or_def). Proof. by eexists. Qed.
+Local Definition monPred_or_aux : seal (@monPred_or_def).
+Proof. by eexists. Qed.
Definition monPred_or := monPred_or_aux.(unseal).
-Definition monPred_or_eq : @monPred_or = _ := monPred_or_aux.(seal_eq).
+Local Definition monPred_or_unseal :
+ @monPred_or = _ := monPred_or_aux.(seal_eq).
-Definition monPred_impl_def P Q : monPred :=
+Local Definition monPred_impl_def P Q : monPred :=
monPred_upclosed (λ i, P i → Q i)%I.
-Definition monPred_impl_aux : seal (@monPred_impl_def). Proof. by eexists. Qed.
+Local Definition monPred_impl_aux : seal (@monPred_impl_def).
+Proof. by eexists. Qed.
Definition monPred_impl := monPred_impl_aux.(unseal).
-Definition monPred_impl_eq : @monPred_impl = _ := monPred_impl_aux.(seal_eq).
+Local Definition monPred_impl_unseal :
+ @monPred_impl = _ := monPred_impl_aux.(seal_eq).
-Program Definition monPred_forall_def A (Φ : A → monPred) : monPred :=
+Local Program Definition monPred_forall_def A (Φ : A → monPred) : monPred :=
MonPred (λ i, ∀ x : A, Φ x i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_forall_aux : seal (@monPred_forall_def). Proof. by eexists. Qed.
+Local Definition monPred_forall_aux : seal (@monPred_forall_def).
+Proof. by eexists. Qed.
Definition monPred_forall := monPred_forall_aux.(unseal).
-Definition monPred_forall_eq : @monPred_forall = _ := monPred_forall_aux.(seal_eq).
+Local Definition monPred_forall_unseal :
+ @monPred_forall = _ := monPred_forall_aux.(seal_eq).
-Program Definition monPred_exist_def A (Φ : A → monPred) : monPred :=
+Local Program Definition monPred_exist_def A (Φ : A → monPred) : monPred :=
MonPred (λ i, ∃ x : A, Φ x i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_exist_aux : seal (@monPred_exist_def). Proof. by eexists. Qed.
+Local Definition monPred_exist_aux : seal (@monPred_exist_def).
+Proof. by eexists. Qed.
Definition monPred_exist := monPred_exist_aux.(unseal).
-Definition monPred_exist_eq : @monPred_exist = _ := monPred_exist_aux.(seal_eq).
+Local Definition monPred_exist_unseal :
+ @monPred_exist = _ := monPred_exist_aux.(seal_eq).
-Program Definition monPred_sep_def P Q : monPred :=
+Local Program Definition monPred_sep_def P Q : monPred :=
MonPred (λ i, P i ∗ Q i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_sep_aux : seal (@monPred_sep_def). Proof. by eexists. Qed.
+Local Definition monPred_sep_aux : seal (@monPred_sep_def).
+Proof. by eexists. Qed.
Definition monPred_sep := monPred_sep_aux.(unseal).
-Definition monPred_sep_eq : @monPred_sep = _ := monPred_sep_aux.(seal_eq).
+Local Definition monPred_sep_unseal :
+ @monPred_sep = _ := monPred_sep_aux.(seal_eq).
-Definition monPred_wand_def P Q : monPred :=
+Local Definition monPred_wand_def P Q : monPred :=
monPred_upclosed (λ i, P i -∗ Q i)%I.
-Definition monPred_wand_aux : seal (@monPred_wand_def). Proof. by eexists. Qed.
+Local Definition monPred_wand_aux : seal (@monPred_wand_def).
+Proof. by eexists. Qed.
Definition monPred_wand := monPred_wand_aux.(unseal).
-Definition monPred_wand_eq : @monPred_wand = _ := monPred_wand_aux.(seal_eq).
+Local Definition monPred_wand_unseal :
+ @monPred_wand = _ := monPred_wand_aux.(seal_eq).
-Program Definition monPred_persistently_def P : monPred :=
+Local Program Definition monPred_persistently_def P : monPred :=
MonPred (λ i, <pers> (P i))%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_persistently_aux : seal (@monPred_persistently_def). Proof. by eexists. Qed.
+Local Definition monPred_persistently_aux : seal (@monPred_persistently_def).
+Proof. by eexists. Qed.
Definition monPred_persistently := monPred_persistently_aux.(unseal).
-Definition monPred_persistently_eq : @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).
+Local Definition monPred_persistently_unseal :
+ @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).
-Program Definition monPred_in_def (i0 : I) : monPred :=
+Local Program Definition monPred_in_def (i0 : I) : monPred :=
MonPred (λ i : I, ⌜i0 ⊑ iâŒ%I) _.
Next Obligation. solve_proper. Qed.
-Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
+Local Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
Definition monPred_in := monPred_in_aux.(unseal).
-Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
+Local Definition monPred_in_unseal :
+ @monPred_in = _ := monPred_in_aux.(seal_eq).
-Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
+Local Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_later_aux : seal monPred_later_def. Proof. by eexists. Qed.
+Local Definition monPred_later_aux : seal monPred_later_def.
+Proof. by eexists. Qed.
Definition monPred_later := monPred_later_aux.(unseal).
-Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
+Local Definition monPred_later_unseal :
+ monPred_later = _ := monPred_later_aux.(seal_eq).
End Bi.
Global Arguments monPred_objectively {_ _} _%I.
@@ -225,19 +255,20 @@ Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
Module MonPred.
-Definition unseal_eqs :=
- (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
- @monPred_forall_eq, @monPred_exist_eq, @monPred_sep_eq, @monPred_wand_eq,
- @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
- @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq,
- @monPred_objectively_eq, @monPred_subjectively_eq).
+Definition monPred_unseal :=
+ (@monPred_and_unseal, @monPred_or_unseal, @monPred_impl_unseal,
+ @monPred_forall_unseal, @monPred_exist_unseal, @monPred_sep_unseal,
+ @monPred_wand_unseal, @monPred_persistently_unseal, @monPred_later_unseal,
+ @monPred_in_unseal, @monPred_embed_unseal, @monPred_emp_unseal,
+ @monPred_pure_unseal, @monPred_objectively_unseal,
+ @monPred_subjectively_unseal).
Ltac unseal :=
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl;
- rewrite !unseal_eqs /=.
+ rewrite !monPred_unseal /=.
End MonPred.
Import MonPred.
@@ -764,18 +795,19 @@ Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at. Qed.
(** BUpd *)
-Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
+Local Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
+Local Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Local Arguments monPred_bupd {_}.
-Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
+Local Lemma monPred_bupd_unseal `{BiBUpd PROP} :
+ @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
Proof.
- split; rewrite monPred_bupd_eq.
+ split; rewrite monPred_bupd_unseal.
- split=>/= i. solve_proper.
- intros P. split=>/= i. apply bupd_intro.
- intros P Q HPQ. split=>/= i. by rewrite HPQ.
@@ -786,7 +818,7 @@ Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
{| bi_bupd_mixin := monPred_bupd_mixin |}.
Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
-Proof. by rewrite monPred_bupd_eq. Qed.
+Proof. by rewrite monPred_bupd_unseal. Qed.
Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
Objective (|==> P).
@@ -830,20 +862,20 @@ Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
Proof. rewrite /bi_except_0. apply _. Qed.
(** Internal equality *)
-Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofe) (a b : A) : monPred :=
- MonPred (λ _, a ≡ b)%I _.
-Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
+Local Definition monPred_internal_eq_def `{!BiInternalEq PROP}
+ (A : ofe) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
+Local Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
Proof. by eexists. Qed.
Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
Local Arguments monPred_internal_eq {_}.
-Lemma monPred_internal_eq_eq `{!BiInternalEq PROP} :
+Local Lemma monPred_internal_eq_unseal `{!BiInternalEq PROP} :
@internal_eq _ (@monPred_internal_eq _) = monPred_internal_eq_def.
Proof. rewrite -monPred_internal_eq_aux.(seal_eq) //. Qed.
Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
BiInternalEqMixin monPredI (@monPred_internal_eq _).
Proof.
- split; rewrite monPred_internal_eq_eq.
+ split; rewrite monPred_internal_eq_unseal.
- split=> i /=. solve_proper.
- intros A P a. split=> i /=. apply internal_eq_refl.
- intros A a b Ψ ?. split=> i /=. unseal.
@@ -860,11 +892,11 @@ Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} : BiInternalEq monPr
Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
BiEmbedInternalEq PROP monPredI.
-Proof. split=> i. rewrite monPred_internal_eq_eq. by unseal. Qed.
+Proof. split=> i. rewrite monPred_internal_eq_unseal. by unseal. Qed.
Lemma monPred_internal_eq_unfold `{!BiInternalEq PROP} :
@internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
-Proof. rewrite monPred_internal_eq_eq. by unseal. Qed.
+Proof. rewrite monPred_internal_eq_unseal. by unseal. Qed.
Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} i (a b : A) :
@monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
@@ -884,19 +916,20 @@ Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofe} (x y : A)
Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
(** FUpd *)
-Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
+Local Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
(P : monPred) : monPred :=
MonPred (λ i, |={E1,E2}=> P i)%I _.
Next Obligation. solve_proper. Qed.
-Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
+Local Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
Definition monPred_fupd := monPred_fupd_aux.(unseal).
Local Arguments monPred_fupd {_}.
-Lemma monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
+Local Lemma monPred_fupd_unseal `{BiFUpd PROP} :
+ @fupd _ monPred_fupd = monPred_fupd_def.
Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
Proof.
- split; rewrite monPred_fupd_eq.
+ split; rewrite monPred_fupd_unseal.
- split=>/= i. solve_proper.
- intros E1 E2 HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
- intros E1 E2 P. split=>/= i. by rewrite monPred_at_except_0 except_0_fupd.
@@ -910,31 +943,33 @@ Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
{| bi_fupd_mixin := monPred_fupd_mixin |}.
Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
Proof.
- intros E P. split=>/= i. rewrite monPred_at_bupd monPred_fupd_eq bupd_fupd //=.
+ intros E P. split=>/= i.
+ rewrite monPred_at_bupd monPred_fupd_unseal bupd_fupd //=.
Qed.
Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
-Proof. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
+Proof. split=>i /=. by rewrite monPred_fupd_unseal /= !monPred_at_embed. Qed.
Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
(|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
-Proof. by rewrite monPred_fupd_eq. Qed.
+Proof. by rewrite monPred_fupd_unseal. Qed.
Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
Objective (|={E1,E2}=> P).
Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
(** Plainly *)
-Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
+Local Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
MonPred (λ _, ∀ i, ■(P i))%I _.
-Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
+Local Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
Definition monPred_plainly := monPred_plainly_aux.(unseal).
Local Arguments monPred_plainly {_}.
-Lemma monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
+Local Lemma monPred_plainly_unseal `{BiPlainly PROP} :
+ @plainly _ monPred_plainly = monPred_plainly_def.
Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredI monPred_plainly.
Proof.
- split; rewrite monPred_plainly_eq; try unseal.
+ split; rewrite monPred_plainly_unseal; try unseal.
- by (split=> ? /=; repeat f_equiv).
- intros P Q [?]. split=> i /=. by do 3 f_equiv.
- intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
@@ -961,7 +996,7 @@ Global Instance minPred_bi_persistently_impl_plainly
`{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
BiPersistentlyImplPlainly monPredI.
Proof.
- intros P Q. rewrite monPred_plainly_eq. unseal.
+ intros P Q. rewrite monPred_plainly_unseal. unseal.
split=> i /=. setoid_rewrite bi.pure_impl_forall.
setoid_rewrite <-plainly_forall.
do 2 setoid_rewrite bi.persistently_forall. do 4 f_equiv.
@@ -971,7 +1006,8 @@ Qed.
Global Instance monPred_bi_prop_ext
`{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
Proof.
- intros P Q. split=> i /=. rewrite monPred_plainly_eq monPred_internal_eq_eq /=.
+ intros P Q. split=> i /=.
+ rewrite monPred_plainly_unseal monPred_internal_eq_unseal /=.
rewrite /bi_wand_iff monPred_equivI. f_equiv=> j. unseal.
by rewrite prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
Qed.
@@ -979,7 +1015,8 @@ Qed.
Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP} `{!BiIndexBottom bot} :
BiPlainlyExist PROP → BiPlainlyExist monPredI.
Proof.
- split=> ? /=. rewrite monPred_plainly_eq /=. setoid_rewrite monPred_at_exist.
+ split=> ? /=. rewrite monPred_plainly_unseal /=.
+ setoid_rewrite monPred_at_exist.
rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.
@@ -987,7 +1024,7 @@ Qed.
Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
BiEmbedPlainly PROP monPredI.
Proof.
- split=> i. rewrite monPred_plainly_eq; unseal. apply (anti_symm _).
+ split=> i. rewrite monPred_plainly_unseal; unseal. apply (anti_symm _).
- by apply bi.forall_intro.
- by rewrite (bi.forall_elim inhabitant).
Qed.
@@ -995,20 +1032,21 @@ Qed.
Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredI.
Proof.
intros P. split=> /= i.
- rewrite monPred_at_bupd monPred_plainly_eq /= bi.forall_elim. apply bupd_plainly.
+ rewrite monPred_at_bupd monPred_plainly_unseal /= bi.forall_elim.
+ apply bupd_plainly.
Qed.
Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
-Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
+Proof. by rewrite monPred_plainly_unseal monPred_embed_unseal. Qed.
Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
-Proof. by rewrite monPred_plainly_eq. Qed.
+Proof. by rewrite monPred_plainly_unseal. Qed.
Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredI.
Proof.
- split; rewrite !monPred_fupd_eq; try unseal.
+ split; rewrite !monPred_fupd_unseal; try unseal.
- intros E P. split=>/= i.
by rewrite monPred_at_plainly (bi.forall_elim i) fupd_plainly_mask_empty.
- intros E P R. split=>/= i.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index dbc5cde46b4cb31ad0ef074206a44570096ccbba..81c8c326b9ea1b8f1ae4db6c3cc3e0ae3f590adb 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -431,7 +431,7 @@ Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM2_plainly `{BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
■([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢ [∗ map] k↦x1;x2 ∈ m1;m2, ■(Φ k x1 x2).
-Proof. by rewrite big_sepM2_eq /big_sepM2_def plainly_and plainly_pure big_sepM_plainly. Qed.
+Proof. by rewrite !big_sepM2_alt plainly_and plainly_pure big_sepM_plainly. Qed.
Lemma big_sepS_plainly `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
■([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■(Φ y).
@@ -522,34 +522,42 @@ Proof. rewrite big_sepL2_alt. apply _. Qed.
Global Instance big_sepM_empty_plain `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) :
Plain ([∗ map] k↦x ∈ ∅, Φ k x).
-Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_sepM_plain `{BiAffine PROP, Countable K} {A} (Φ : K → A → PROP) m :
- (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x).
-Proof. rewrite big_opM_eq. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
+ (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x).
+Proof.
+ induction m using map_ind;
+ [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
+Qed.
Global Instance big_sepM2_empty_plain `{BiAffine PROP, Countable K}
{A B} (Φ : K → A → B → PROP) :
Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
-Proof. rewrite big_sepM2_eq /big_sepM2_def map_zip_with_empty. apply _. Qed.
+Proof. rewrite big_sepM2_empty. apply _. Qed.
Global Instance big_sepM2_plain `{BiAffine PROP, Countable K}
{A B} (Φ : K → A → B → PROP) m1 m2 :
(∀ k x1 x2, Plain (Φ k x1 x2)) →
Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
-Proof. intros. rewrite big_sepM2_eq. apply _. Qed.
+Proof. intros. rewrite big_sepM2_alt. apply _. Qed.
Global Instance big_sepS_empty_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) :
Plain ([∗ set] x ∈ ∅, Φ x).
-Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
+Proof. rewrite big_opS_empty. apply _. Qed.
Global Instance big_sepS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
(∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
-Proof. rewrite big_opS_eq. apply _. Qed.
-
+Proof.
+ induction X using set_ind_L;
+ [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
+Qed.
Global Instance big_sepMS_empty_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) :
Plain ([∗ mset] x ∈ ∅, Φ x).
-Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
+Proof. rewrite big_opMS_empty. apply _. Qed.
Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) X :
(∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
-Proof. rewrite big_opMS_eq. apply _. Qed.
+Proof.
+ induction X using gmultiset_ind;
+ [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
+Qed.
Global Instance plainly_timeless P `{!BiPlainlyExist PROP} :
Timeless P → Timeless (■P).
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index ccb1fe6b811b22301dec20171180500b15db12d9..76e9177d320201bffaf09100a05aa6508cf6ff4e 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -25,7 +25,7 @@ Definition twp_pre `{!irisGS Λ Σ} (s : stuckness)
(** This is some uninteresting bookkeeping to prove that [twp_pre_mono] is
monotone. The actual least fixpoint [twp_def] can be found below. *)
-Lemma twp_pre_mono `{!irisGS Λ Σ} s
+Local Lemma twp_pre_mono `{!irisGS Λ Σ} s
(wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
⊢ (□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ.
@@ -42,7 +42,7 @@ Proof.
Qed.
(* Uncurry [twp_pre] and equip its type with an OFE structure *)
-Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
+Local Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
(prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ :=
uncurry3 ∘ twp_pre s ∘ curry3.
@@ -57,13 +57,13 @@ Proof.
rewrite /curry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
Qed.
-Definition twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
+Local Definition twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
:= λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
-Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
+Local Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
Definition twp' := twp_aux.(unseal).
Global Arguments twp' {Λ Σ _}.
Global Existing Instance twp'.
-Lemma twp_eq `{!irisGS Λ Σ} : twp = @twp_def Λ Σ _.
+Local Lemma twp_unseal `{!irisGS Λ Σ} : twp = @twp_def Λ Σ _.
Proof. rewrite -twp_aux.(seal_eq) //. Qed.
Section twp.
@@ -76,13 +76,13 @@ Implicit Types e : expr Λ.
(* Weakest pre *)
Lemma twp_unfold s E e Φ : WP e @ s; E [{ Φ }] ⊣⊢ twp_pre s (twp s) E e Φ.
-Proof. by rewrite twp_eq /twp_def least_fixpoint_unfold. Qed.
+Proof. by rewrite twp_unseal /twp_def least_fixpoint_unfold. Qed.
Lemma twp_ind s Ψ :
(∀ n E e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
□ (∀ e E Φ, twp_pre s (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) -∗
∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
Proof.
- iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
+ iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_unseal.
set (Ψ' := uncurry3 Ψ :
prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ).
assert (NonExpansive Ψ').
@@ -95,7 +95,7 @@ Qed.
Global Instance twp_ne s E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
Proof.
- intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
+ intros Φ1 Φ2 HΦ. rewrite !twp_unseal. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed.
Global Instance twp_proper s E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (twp (PROP:=iProp Σ) s E e).
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index b918c293379f1c1bef06f481c0807cef1aa162eb..55108733874d86775c0dca1af3d95869e9e06376 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -73,13 +73,13 @@ Proof.
- by rewrite -IH.
Qed.
-Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
+Local Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
λ s : stuckness, fixpoint (wp_pre s).
-Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
+Local Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
Definition wp' := wp_aux.(unseal).
Global Arguments wp' {Λ Σ _}.
Global Existing Instance wp'.
-Lemma wp_eq `{!irisGS Λ Σ} : wp = @wp_def Λ Σ _.
+Local Lemma wp_unseal `{!irisGS Λ Σ} : wp = @wp_def Λ Σ _.
Proof. rewrite -wp_aux.(seal_eq) //. Qed.
Section wp.
@@ -93,7 +93,7 @@ Implicit Types e : expr Λ.
(* Weakest pre *)
Lemma wp_unfold s E e Φ :
WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ) s) E e Φ.
-Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
+Proof. rewrite wp_unseal. apply (fixpoint_unfold (wp_pre s)). Qed.
Global Instance wp_ne s E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 060f818cd72079f5a9826e21ab022840dcffb0cf..117714f66675cffde67f4c5c5ed9cb55acf4fc05 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -16,7 +16,7 @@ Implicit Types P Q : PROP.
(** * Starting and stopping the proof mode *)
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
Proof.
- rewrite envs_entails_eq !of_envs_eq /=.
+ rewrite environments.envs_entails_unseal !of_envs_eq /=.
rewrite intuitionistically_True_emp left_id=><-.
apply and_intro=> //. apply pure_intro; repeat constructor.
Qed.
@@ -29,7 +29,7 @@ Lemma tac_stop Δ P :
end ⊢ P) →
envs_entails Δ P.
Proof.
- rewrite envs_entails_eq !of_envs_eq. intros <-.
+ rewrite environments.envs_entails_unseal !of_envs_eq. intros <-.
rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
destruct (env_intuitionistic Δ), (env_spatial Δ);
by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
@@ -53,7 +53,7 @@ Lemma tac_eval_in Δ i p P P' Q :
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite envs_entails_eq /=. intros ? HP ?.
+ rewrite environments.envs_entails_unseal /=. intros ? HP ?.
rewrite envs_simple_replace_singleton_sound //; simpl.
by rewrite HP wand_elim_r.
Qed.
@@ -74,7 +74,7 @@ Local Instance affine_env_spatial Δ :
Proof. intros H. induction H; simpl; apply _. Qed.
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
-Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
+Proof. intros. by rewrite environments.envs_entails_unseal (affine (of_envs Δ)). Qed.
Lemma tac_assumption Δ i p P Q :
envs_lookup i Δ = Some (p,P) →
@@ -84,7 +84,7 @@ Lemma tac_assumption Δ i p P Q :
else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
envs_entails Δ Q.
Proof.
- intros ?? H. rewrite envs_entails_eq envs_lookup_sound //.
+ intros ?? H. rewrite environments.envs_entails_unseal envs_lookup_sound //.
simpl in *. destruct (env_spatial_is_nil _) eqn:?.
- by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
- rewrite from_assumption. destruct H; by rewrite sep_elim_l.
@@ -98,7 +98,7 @@ Lemma tac_assumption_coq Δ P Q :
envs_entails Δ Q.
Proof.
rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
- rewrite envs_entails_eq -(left_id emp%I bi_sep (of_envs Δ)).
+ rewrite environments.envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
rewrite -bi.intuitionistically_emp HP HPQ.
destruct (env_spatial_is_nil _) eqn:?.
- by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
@@ -114,7 +114,7 @@ Lemma tac_rename Δ i j p P Q :
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
+ rewrite environments.envs_entails_unseal=> ??. rewrite envs_simple_replace_singleton_sound //.
by rewrite wand_elim_r.
Qed.
@@ -124,20 +124,20 @@ Lemma tac_clear Δ i p P Q :
envs_entails (envs_delete true i p Δ) Q →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
+ rewrite environments.envs_entails_unseal=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
by destruct p; rewrite /= sep_elim_r.
Qed.
(** * False *)
Lemma tac_ex_falso Δ Q : envs_entails Δ False → envs_entails Δ Q.
-Proof. by rewrite envs_entails_eq -(False_elim Q). Qed.
+Proof. by rewrite environments.envs_entails_unseal -(False_elim Q). Qed.
Lemma tac_false_destruct Δ i p P Q :
envs_lookup i Δ = Some (p,P) →
P = False%I →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
+ rewrite environments.envs_entails_unseal => ??. subst. rewrite envs_lookup_sound //; simpl.
by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Qed.
@@ -148,7 +148,7 @@ Lemma tac_pure_intro Δ Q φ a :
φ →
envs_entails Δ Q.
Proof.
- intros ???. rewrite envs_entails_eq -(from_pure a Q). destruct a; simpl.
+ intros ???. rewrite environments.envs_entails_unseal -(from_pure a Q). destruct a; simpl.
- by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
- by apply pure_intro.
Qed.
@@ -159,7 +159,7 @@ Lemma tac_pure Δ i p P φ Q :
(if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
(φ → envs_entails (envs_delete true i p Δ) Q) → envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq=> ?? HPQ HQ.
+ rewrite environments.envs_entails_unseal=> ?? HPQ HQ.
rewrite envs_lookup_sound //; simpl. destruct p; simpl.
- rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
by apply pure_elim_l.
@@ -175,7 +175,7 @@ Lemma tac_pure_revert Δ φ P Q :
envs_entails Δ (P -∗ Q) →
(φ → envs_entails Δ Q).
Proof.
- rewrite /FromAffinely envs_entails_eq. intros <- -> ?.
+ rewrite /FromAffinely environments.envs_entails_unseal. intros <- -> ?.
by rewrite pure_True // affinely_True_emp affinely_emp left_id.
Qed.
@@ -191,7 +191,7 @@ Lemma tac_intuitionistic Δ i j p P P' Q :
envs_entails Δ Q.
Proof.
destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
+ rewrite environments.envs_entails_unseal=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
destruct p; simpl; rewrite /bi_intuitionistically.
- by rewrite -(into_persistent true P) /= wand_elim_r.
- destruct HPQ.
@@ -212,7 +212,7 @@ Lemma tac_spatial Δ i j p P P' Q :
envs_entails Δ Q.
Proof.
intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite envs_entails_eq=> <-. rewrite envs_replace_singleton_sound //; simpl.
+ rewrite environments.envs_entails_unseal=> <-. rewrite envs_replace_singleton_sound //; simpl.
destruct p; simpl; last destruct HP.
- by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
- by rewrite wand_elim_r.
@@ -230,7 +230,7 @@ Lemma tac_impl_intro Δ i P P' Q R :
envs_entails Δ R.
Proof.
destruct (envs_app _ _ _) eqn:?; last done.
- rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
+ rewrite /FromImpl environments.envs_entails_unseal => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
- rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
rewrite envs_app_singleton_sound //; simpl.
rewrite -(from_affinely P' P) -affinely_and_lr.
@@ -248,7 +248,7 @@ Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
envs_entails Δ R.
Proof.
destruct (envs_app _ _ _) eqn:?; last done.
- rewrite /FromImpl envs_entails_eq => <- ??.
+ rewrite /FromImpl environments.envs_entails_unseal => <- ??.
rewrite envs_app_singleton_sound //=. apply impl_intro_l.
rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
@@ -256,7 +256,7 @@ Qed.
Lemma tac_impl_intro_drop Δ P Q R :
FromImpl R P Q → envs_entails Δ Q → envs_entails Δ R.
Proof.
- rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
+ rewrite /FromImpl environments.envs_entails_unseal => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
Lemma tac_wand_intro Δ i P Q R :
@@ -268,7 +268,7 @@ Lemma tac_wand_intro Δ i P Q R :
envs_entails Δ R.
Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite /FromWand envs_entails_eq => <- HQ.
+ rewrite /FromWand environments.envs_entails_unseal => <- HQ.
rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
@@ -283,7 +283,7 @@ Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
envs_entails Δ R.
Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
+ rewrite /FromWand environments.envs_entails_unseal => <- ? HPQ HQ.
rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
- rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
(into_persistent _ P) wand_elim_r //.
@@ -297,7 +297,7 @@ Lemma tac_wand_intro_drop Δ P Q R :
envs_entails Δ Q →
envs_entails Δ R.
Proof.
- rewrite envs_entails_eq /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
+ rewrite environments.envs_entails_unseal /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Qed.
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
@@ -312,7 +312,7 @@ Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
| None => False
end → envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq /IntoWand. intros ?? HR ?.
+ rewrite environments.envs_entails_unseal /IntoWand. intros ?? HR ?.
destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
@@ -338,7 +338,7 @@ Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
| None => False
end → envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq. intros ?? Hmod HQ.
+ rewrite environments.envs_entails_unseal. intros ?? Hmod HQ.
destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
destruct HQ as [HP1 HQ].
destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
@@ -356,9 +356,9 @@ Proof.
Qed.
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
-Proof. rewrite envs_entails_eq=> ->. by rewrite -lock left_id. Qed.
+Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite -lock left_id. Qed.
Lemma tac_unlock_True Δ Q : envs_entails Δ Q → envs_entails Δ (True ∗ locked Q).
-Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
+Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite -lock -True_sep_2. Qed.
Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
Proof. by unlock. Qed.
@@ -370,7 +370,7 @@ Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
Q' = (P2 -∗ Q)%I →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq. intros ?? Hmod HPQ ->.
+ rewrite environments.envs_entails_unseal. intros ?? Hmod HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
@@ -388,7 +388,7 @@ Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
- rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
+ rewrite environments.envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp (into_wand q true) /=.
rewrite -(from_pure a P1) pure_True //.
rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
@@ -406,7 +406,7 @@ Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
| None => False
end → envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq => ???? HP1 HQ.
+ rewrite environments.envs_entails_unseal => ???? HP1 HQ.
destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
rewrite -HQ envs_lookup_sound //.
rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
@@ -428,7 +428,7 @@ Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
| None => False
end → envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq => ?? HR ??.
+ rewrite environments.envs_entails_unseal => ?? HR ??.
destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
rewrite envs_replace_singleton_sound //; destruct q; simpl.
@@ -446,7 +446,7 @@ Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
envs_lookup i Δ = Some (q,P) →
envs_entails Δ (<absorb> P).
Proof.
- rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
+ rewrite environments.envs_entails_unseal /bi_absorbingly=> /envs_lookup_sound=> ->.
rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
Qed.
@@ -457,7 +457,7 @@ Lemma tac_revert Δ i Q :
end →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq => HQ.
+ rewrite environments.envs_entails_unseal => HQ.
destruct (envs_lookup_delete _ _ _) as [[[p P] Δ']|] eqn:?; last done.
rewrite envs_lookup_delete_sound //=.
rewrite HQ. destruct p; simpl; auto using wand_elim_r.
@@ -466,7 +466,7 @@ Qed.
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
into_ih : φ → □ of_envs Δ ⊢ Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
-Proof. by rewrite envs_entails_eq /IntoIH bi.intuitionistically_elim. Qed.
+Proof. by rewrite environments.envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
(∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
@@ -516,7 +516,7 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
envs_entails Δ (<pers> P → Q) →
envs_entails Δ Q.
Proof.
- rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
+ rewrite /IntoIH environments.envs_entails_unseal. intros HP ? HPQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite -(idemp bi_and (□ (of_envs Δ))%I).
rewrite -{1}intuitionistically_idemp {1}intuitionistically_into_persistently_1.
@@ -530,7 +530,7 @@ Lemma tac_assert Δ j P Q :
end → envs_entails Δ Q.
Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
- rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
+ rewrite environments.envs_entails_unseal=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
Qed.
@@ -565,7 +565,7 @@ Lemma tac_pose_proof Δ j P Q :
envs_entails Δ Q.
Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
- rewrite envs_entails_eq => HP <-. rewrite envs_app_singleton_sound //=.
+ rewrite environments.envs_entails_unseal => HP <-. rewrite envs_app_singleton_sound //=.
by rewrite -HP /= intuitionistically_emp emp_wand.
Qed.
@@ -582,7 +582,7 @@ Lemma tac_pose_proof_hyp Δ i j Q :
Proof.
destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
- rewrite envs_entails_eq. move: Hlookup. rewrite envs_lookup_delete_Some.
+ rewrite environments.envs_entails_unseal. move: Hlookup. rewrite envs_lookup_delete_Some.
intros [? ->] <-.
rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
by rewrite wand_elim_r.
@@ -593,14 +593,14 @@ Lemma tac_apply Δ i p R P1 P2 :
IntoWand p false R P1 P2 →
envs_entails (envs_delete true i p Δ) P1 → envs_entails Δ P2.
Proof.
- rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_sound //.
+ rewrite environments.envs_entails_unseal => ?? HP1. rewrite envs_lookup_sound //.
by rewrite (into_wand p false) /= HP1 wand_elim_l.
Qed.
(** * Conjunction splitting *)
Lemma tac_and_split Δ P Q1 Q2 :
FromAnd P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.
-Proof. rewrite envs_entails_eq. intros. rewrite -(from_and P). by apply and_intro. Qed.
+Proof. rewrite environments.envs_entails_unseal. intros. rewrite -(from_and P). by apply and_intro. Qed.
(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ d js P Q1 Q2 :
@@ -611,7 +611,7 @@ Lemma tac_sep_split Δ d js P Q1 Q2 :
end → envs_entails Δ P.
Proof.
destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
- rewrite envs_entails_eq=>? [HQ1 HQ2].
+ rewrite environments.envs_entails_unseal=>? [HQ1 HQ2].
rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Qed.
@@ -635,7 +635,7 @@ Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 →
envs_entails Δ3 Q → envs_entails Δ1 Q.
Proof.
- rewrite envs_entails_eq => ??? <-. rewrite envs_lookup_delete_list_sound //.
+ rewrite environments.envs_entails_unseal => ??? <-. rewrite envs_lookup_delete_list_sound //.
rewrite from_seps. rewrite envs_app_singleton_sound //=.
by rewrite wand_elim_r.
Qed.
@@ -651,7 +651,7 @@ Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
+ rewrite environments.envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
- by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
- by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Qed.
@@ -671,7 +671,7 @@ Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
end → envs_entails Δ Q.
Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
- rewrite envs_entails_eq => ? HP HQ.
+ rewrite environments.envs_entails_unseal => ? HP HQ.
rewrite envs_simple_replace_singleton_sound //=. destruct p.
{ rewrite (into_and _ P) HQ. destruct d; simpl.
- by rewrite and_elim_l wand_elim_r.
@@ -689,7 +689,7 @@ Qed.
Lemma tac_frame_pure Δ (φ : Prop) P Q :
φ → Frame true ⌜φ⌠P Q → envs_entails Δ Q → envs_entails Δ P.
Proof.
- rewrite envs_entails_eq => ? Hframe ->. rewrite -Hframe /=.
+ rewrite environments.envs_entails_unseal => ? Hframe ->. rewrite -Hframe /=.
rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
auto using and_intro, pure_intro.
Qed.
@@ -699,7 +699,7 @@ Lemma tac_frame Δ i p R P Q :
Frame p R P Q →
envs_entails (envs_delete false i p Δ) Q → envs_entails Δ P.
Proof.
- rewrite envs_entails_eq. intros ? Hframe HQ.
+ rewrite environments.envs_entails_unseal. intros ? Hframe HQ.
rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
Qed.
@@ -707,12 +707,12 @@ Qed.
Lemma tac_or_l Δ P Q1 Q2 :
FromOr P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ P.
Proof.
- rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
+ rewrite environments.envs_entails_unseal=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
Qed.
Lemma tac_or_r Δ P Q1 Q2 :
FromOr P Q1 Q2 → envs_entails Δ Q2 → envs_entails Δ P.
Proof.
- rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
+ rewrite environments.envs_entails_unseal=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
Qed.
Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
@@ -726,7 +726,7 @@ Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
Proof.
destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; last done.
destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; last done.
- rewrite envs_entails_eq. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
+ rewrite environments.envs_entails_unseal. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
- rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
by rewrite wand_elim_r.
@@ -741,7 +741,7 @@ Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q name :
let _ := name in
∀ a, envs_entails Δ (Φ a)) →
envs_entails Δ Q.
-Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
+Proof. rewrite environments.envs_entails_unseal /FromForall=> <-. apply forall_intro. Qed.
Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
@@ -752,7 +752,7 @@ Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
end) →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq. intros ?? (x&?).
+ rewrite environments.envs_entails_unseal. intros ?? (x&?).
destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
rewrite envs_simple_replace_singleton_sound //; simpl.
by rewrite (into_forall P) (forall_elim x) wand_elim_r.
@@ -760,13 +760,13 @@ Qed.
Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
envs_entails Δ (∀ a, Φ a) → ∀ a, envs_entails Δ (Φ a).
-Proof. rewrite envs_entails_eq => HΔ a. by rewrite HΔ (forall_elim a). Qed.
+Proof. rewrite environments.envs_entails_unseal => HΔ a. by rewrite HΔ (forall_elim a). Qed.
(** * Existential *)
Lemma tac_exist {A} Δ P (Φ : A → PROP) :
FromExist P Φ → (∃ a, envs_entails Δ (Φ a)) → envs_entails Δ P.
Proof.
- rewrite envs_entails_eq => ? [a ?].
+ rewrite environments.envs_entails_unseal => ? [a ?].
rewrite -(from_exist P). eauto using exist_intro'.
Qed.
@@ -783,7 +783,7 @@ Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) (name: ident_name) Q :
end) →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq => ?? HΦ. rewrite envs_lookup_sound //.
+ rewrite environments.envs_entails_unseal => ?? HΦ. rewrite envs_lookup_sound //.
rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
apply exist_elim=> a; specialize (HΦ a) as Hmatch.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
@@ -802,7 +802,7 @@ Lemma tac_modal_elim Δ i j p p' φ P' P Q Q' :
envs_entails Δ Q.
Proof.
destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
- rewrite envs_entails_eq => ??? HΔ. rewrite envs_replace_singleton_sound //=.
+ rewrite environments.envs_entails_unseal => ??? HΔ. rewrite envs_replace_singleton_sound //=.
rewrite HΔ. by eapply elim_modal.
Qed.
@@ -811,7 +811,7 @@ Lemma tac_accu Δ P :
env_to_prop (env_spatial Δ) = P →
envs_entails Δ P.
Proof.
- rewrite envs_entails_eq=><-.
+ rewrite environments.envs_entails_unseal=><-.
rewrite env_to_prop_sound !of_envs_eq and_elim_r sep_elim_r //.
Qed.
@@ -830,7 +830,7 @@ Lemma tac_inv_elim {X : Type} Δ i j φ p Pinv Pin Pout (Pclose : option (X →
with Some Δ'' => envs_entails Δ'' R | None => False end) →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq=> ? Hinv ? /(_ Q) Hmatch.
+ rewrite environments.envs_entails_unseal=> ? Hinv ? /(_ Q) Hmatch.
destruct (envs_app _ _ _) eqn:?; last done.
rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
@@ -848,7 +848,7 @@ Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
NonExpansive Φ →
envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
Proof.
- intros ? A x y ? HPxy -> ?. rewrite envs_entails_eq.
+ intros ? A x y ? HPxy -> ?. rewrite environments.envs_entails_unseal.
apply internal_eq_rewrite'; auto. rewrite {1}envs_lookup_sound //.
rewrite (into_internal_eq Pxy x y) intuitionistically_if_elim sep_elim_l.
destruct d; auto using internal_eq_sym.
@@ -867,7 +867,7 @@ Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
end →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
+ rewrite environments.envs_entails_unseal /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
@@ -890,7 +890,7 @@ Lemma tac_löb Δ i Q :
envs_entails Δ Q.
Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
- rewrite envs_entails_eq => ?? HQ.
+ rewrite environments.envs_entails_unseal => ?? HQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite envs_app_singleton_sound //; simpl. rewrite HQ.
apply löb_wand_intuitionistically.
@@ -1080,7 +1080,7 @@ Section tac_modal_intro.
φ →
envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
Proof.
- rewrite envs_entails_eq /FromModal !of_envs_eq => HQ' HΓp HΓs ? Hφ HQ.
+ rewrite environments.envs_entails_unseal /FromModal !of_envs_eq => HQ' HΓp HΓs ? Hφ HQ.
apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
{ split; simpl in *.
- destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 5001cd299c8c19253964787baf6e11e4d2573c6e..9931c6e9a2539bdeb510db521a15dc53c6c7c06e 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -256,18 +256,19 @@ Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
Global Instance: Params (@of_envs) 1 := {}.
Global Arguments of_envs : simpl never.
-Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
+Local Definition pre_envs_entails_def {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).
+Local Definition pre_envs_entails_aux : seal (@pre_envs_entails_def).
+Proof. by eexists. Qed.
+Local Definition pre_envs_entails := pre_envs_entails_aux.(unseal).
+Local Definition pre_envs_entails_unseal :
+ @pre_envs_entails = @pre_envs_entails_def := pre_envs_entails_aux.(seal_eq).
Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
pre_envs_entails PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
-Definition envs_entails_eq :
+Local Definition envs_entails_unseal :
@envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
-Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
+Proof. by rewrite /envs_entails pre_envs_entails_unseal. Qed.
Global Arguments envs_entails {PROP} Δ Q%I.
Global Instance: Params (@envs_entails) 1 := {}.
@@ -453,13 +454,13 @@ Proof. by constructor. Qed.
Global Instance envs_entails_proper :
Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails PROP).
-Proof. rewrite envs_entails_eq. solve_proper. Qed.
+Proof. rewrite envs_entails_unseal. solve_proper. Qed.
Global Instance envs_entails_mono :
Proper (flip (envs_Forall2 (⊢)) ==> (⊢) ==> impl) (@envs_entails PROP).
-Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
+Proof. rewrite envs_entails_unseal=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
Global Instance envs_entails_flip_mono :
Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
-Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
+Proof. rewrite envs_entails_unseal=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
Lemma envs_delete_intuitionistic Δ i : envs_delete false i true Δ = Δ.
Proof. by destruct Δ. Qed.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 7097d2e6db72af942b430dad981a32a51f8d6197..661d731b3e91042ad6233a2defdac5ba6a04d6e0 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3426,19 +3426,19 @@ Global Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
(* TODO: look for a more principled way of adding trivial hints like those
below; see the discussion in !75 for further details. *)
Global Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
- rewrite envs_entails_eq; apply internal_eq_refl : core.
+ rewrite environments.envs_entails_unseal; apply internal_eq_refl : core.
Global Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
- rewrite envs_entails_eq; apply (big_sepL_nil' _) : core.
+ rewrite environments.envs_entails_unseal; apply (big_sepL_nil' _) : core.
Global Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
- rewrite envs_entails_eq; apply (big_sepL2_nil' _) : core.
+ rewrite environments.envs_entails_unseal; apply (big_sepL2_nil' _) : core.
Global Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
- rewrite envs_entails_eq; apply (big_sepM_empty' _) : core.
+ rewrite environments.envs_entails_unseal; apply (big_sepM_empty' _) : core.
Global Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
- rewrite envs_entails_eq; apply (big_sepM2_empty' _) : core.
+ rewrite environments.envs_entails_unseal; apply (big_sepM2_empty' _) : core.
Global Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
- rewrite envs_entails_eq; apply (big_sepS_empty' _) : core.
+ rewrite environments.envs_entails_unseal; apply (big_sepS_empty' _) : core.
Global Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
- rewrite envs_entails_eq; apply (big_sepMS_empty' _) : core.
+ rewrite environments.envs_entails_unseal; apply (big_sepMS_empty' _) : core.
(* These introduce as much as possible at once, for better performance. *)
Global Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index fa9af40b44ca7b0fe389c534ecfc6c03ae464bf7..70e0ba8ab51323c7317d357eae328f62e7b77ec3 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -55,75 +55,79 @@ Inductive siProp_entails (P Q : siProp) : Prop :=
Global Hint Resolve siProp_closed : siProp_def.
(** logical connectives *)
-Program Definition siProp_pure_def (φ : Prop) : siProp :=
+Local Program Definition siProp_pure_def (φ : Prop) : siProp :=
{| siProp_holds n := φ |}.
Solve Obligations with done.
-Definition siProp_pure_aux : seal (@siProp_pure_def). Proof. by eexists. Qed.
+Local Definition siProp_pure_aux : seal (@siProp_pure_def). Proof. by eexists. Qed.
Definition siProp_pure := unseal siProp_pure_aux.
-Definition siProp_pure_eq :
+Local Definition siProp_pure_unseal :
@siProp_pure = @siProp_pure_def := seal_eq siProp_pure_aux.
-Program Definition siProp_and_def (P Q : siProp) : siProp :=
+Local Program Definition siProp_and_def (P Q : siProp) : siProp :=
{| siProp_holds n := P n ∧ Q n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_and_aux : seal (@siProp_and_def). Proof. by eexists. Qed.
+Local Definition siProp_and_aux : seal (@siProp_and_def). Proof. by eexists. Qed.
Definition siProp_and := unseal siProp_and_aux.
-Definition siProp_and_eq: @siProp_and = @siProp_and_def := seal_eq siProp_and_aux.
+Local Definition siProp_and_unseal :
+ @siProp_and = @siProp_and_def := seal_eq siProp_and_aux.
-Program Definition siProp_or_def (P Q : siProp) : siProp :=
+Local Program Definition siProp_or_def (P Q : siProp) : siProp :=
{| siProp_holds n := P n ∨ Q n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_or_aux : seal (@siProp_or_def). Proof. by eexists. Qed.
+Local Definition siProp_or_aux : seal (@siProp_or_def). Proof. by eexists. Qed.
Definition siProp_or := unseal siProp_or_aux.
-Definition siProp_or_eq: @siProp_or = @siProp_or_def := seal_eq siProp_or_aux.
+Local Definition siProp_or_unseal :
+ @siProp_or = @siProp_or_def := seal_eq siProp_or_aux.
-Program Definition siProp_impl_def (P Q : siProp) : siProp :=
+Local Program Definition siProp_impl_def (P Q : siProp) : siProp :=
{| siProp_holds n := ∀ n', n' ≤ n → P n' → Q n' |}.
Next Obligation. intros P Q [|n1] [|n2]; auto with lia. Qed.
-Definition siProp_impl_aux : seal (@siProp_impl_def). Proof. by eexists. Qed.
+Local Definition siProp_impl_aux : seal (@siProp_impl_def). Proof. by eexists. Qed.
Definition siProp_impl := unseal siProp_impl_aux.
-Definition siProp_impl_eq :
+Local Definition siProp_impl_unseal :
@siProp_impl = @siProp_impl_def := seal_eq siProp_impl_aux.
-Program Definition siProp_forall_def {A} (Ψ : A → siProp) : siProp :=
+Local Program Definition siProp_forall_def {A} (Ψ : A → siProp) : siProp :=
{| siProp_holds n := ∀ a, Ψ a n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_forall_aux : seal (@siProp_forall_def). Proof. by eexists. Qed.
+Local Definition siProp_forall_aux : seal (@siProp_forall_def). Proof. by eexists. Qed.
Definition siProp_forall {A} := unseal siProp_forall_aux A.
-Definition siProp_forall_eq :
+Local Definition siProp_forall_unseal :
@siProp_forall = @siProp_forall_def := seal_eq siProp_forall_aux.
-Program Definition siProp_exist_def {A} (Ψ : A → siProp) : siProp :=
+Local Program Definition siProp_exist_def {A} (Ψ : A → siProp) : siProp :=
{| siProp_holds n := ∃ a, Ψ a n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_exist_aux : seal (@siProp_exist_def). Proof. by eexists. Qed.
+Local Definition siProp_exist_aux : seal (@siProp_exist_def). Proof. by eexists. Qed.
Definition siProp_exist {A} := unseal siProp_exist_aux A.
-Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.
+Local Definition siProp_exist_unseal :
+ @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.
-Program Definition siProp_internal_eq_def {A : ofe} (a1 a2 : A) : siProp :=
+Local Program Definition siProp_internal_eq_def {A : ofe} (a1 a2 : A) : siProp :=
{| siProp_holds n := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using dist_le.
-Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
+Local Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
Definition siProp_internal_eq {A} := unseal siProp_internal_eq_aux A.
-Definition siProp_internal_eq_eq:
+Local Definition siProp_internal_eq_unseal :
@siProp_internal_eq = @siProp_internal_eq_def := seal_eq siProp_internal_eq_aux.
-Program Definition siProp_later_def (P : siProp) : siProp :=
+Local Program Definition siProp_later_def (P : siProp) : siProp :=
{| siProp_holds n := match n return _ with 0 => True | S n' => P n' end |}.
Next Obligation. intros P [|n1] [|n2]; eauto using siProp_closed with lia. Qed.
-Definition siProp_later_aux : seal (@siProp_later_def). Proof. by eexists. Qed.
+Local Definition siProp_later_aux : seal (@siProp_later_def). Proof. by eexists. Qed.
Definition siProp_later := unseal siProp_later_aux.
-Definition siProp_later_eq :
+Local Definition siProp_later_unseal :
@siProp_later = @siProp_later_def := seal_eq siProp_later_aux.
(** Primitive logical rules.
These are not directly usable later because they do not refer to the BI
connectives. *)
Module siProp_primitive.
-Definition unseal_eqs :=
- (siProp_pure_eq, siProp_and_eq, siProp_or_eq, siProp_impl_eq, siProp_forall_eq,
- siProp_exist_eq, siProp_internal_eq_eq, siProp_later_eq).
-Ltac unseal := rewrite !unseal_eqs /=.
+Definition siProp_unseal :=
+ (siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
+ siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
+ siProp_internal_eq_unseal, siProp_later_unseal).
+Ltac unseal := rewrite !siProp_unseal /=.
Section primitive.
Local Arguments siProp_holds !_ _ /.
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index ad370a361a4761151d8cfe04f9d63d927f1118e3..db3b630099da77c15215afe97f31013874d391e9 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -35,7 +35,7 @@ Lemma tac_wp_pure `{!heapGS Σ} Δ Δ' s E K e1 e2 φ n Φ :
envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }}) →
envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+ rewrite environments.envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
(* We want [pure_exec_fill] to be available to TC search locally. *)
pose proof @pure_exec_fill.
rewrite HΔ' -lifting.wp_pure_step_later //.
@@ -46,7 +46,7 @@ Lemma tac_twp_pure `{!heapGS Σ} Δ s E K e1 e2 φ n Φ :
envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
envs_entails Δ (WP (fill K e1) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> ?? ->.
+ rewrite environments.envs_entails_unseal=> ?? ->.
(* We want [pure_exec_fill] to be available to TC search locally. *)
pose proof @pure_exec_fill.
rewrite -total_lifting.twp_pure_step //.
@@ -54,17 +54,17 @@ Qed.
Lemma tac_wp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
+Proof. rewrite environments.envs_entails_unseal=> ->. by apply wp_value. Qed.
Lemma tac_twp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
-Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
+Proof. rewrite environments.envs_entails_unseal=> ->. by apply twp_value. Qed.
Lemma tac_wp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ->. by rewrite wp_value_fupd. Qed.
+Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite wp_value_fupd. Qed.
Lemma tac_twp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
-Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
+Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite twp_value_fupd. Qed.
(** Simplify the goal if it is [WP] of a value.
If the postcondition already allows a fupd, do not add a second one.
@@ -174,12 +174,12 @@ Lemma tac_wp_bind `{!heapGS Σ} K Δ s E Φ e f :
f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
+Proof. rewrite environments.envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
Lemma tac_twp_bind `{!heapGS Σ} K Δ s E Φ e f :
f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
-Proof. rewrite envs_entails_eq=> -> ->. by apply: twp_bind. Qed.
+Proof. rewrite environments.envs_entails_unseal=> -> ->. by apply: twp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
@@ -224,7 +224,7 @@ Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
end) →
envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ? ? HΔ.
+ rewrite environments.envs_entails_unseal=> ? ? HΔ.
rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
specialize (HΔ l).
@@ -242,7 +242,7 @@ Lemma tac_twp_allocN Δ s E j K v n Φ :
end) →
envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> ? HΔ.
+ rewrite environments.envs_entails_unseal=> ? HΔ.
rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
rewrite left_id. apply forall_intro=> l.
specialize (HΔ l).
@@ -261,7 +261,7 @@ Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
end) →
envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ? HΔ.
+ rewrite environments.envs_entails_unseal=> ? HΔ.
rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
specialize (HΔ l).
@@ -278,7 +278,7 @@ Lemma tac_twp_alloc Δ s E j K v Φ :
end) →
envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> HΔ.
+ rewrite environments.envs_entails_unseal=> HΔ.
rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
rewrite left_id. apply forall_intro=> l.
specialize (HΔ l).
@@ -294,7 +294,7 @@ Lemma tac_wp_free Δ Δ' s E i K l v Φ :
envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ? Hlk Hfin.
+ rewrite environments.envs_entails_unseal=> ? Hlk Hfin.
rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
@@ -306,7 +306,7 @@ Lemma tac_twp_free Δ s E i K l v Φ :
envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }])) →
envs_entails Δ (WP fill K (Free (LitV l)) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> Hlk Hfin.
+ rewrite environments.envs_entails_unseal=> Hlk Hfin.
rewrite -twp_bind. eapply wand_apply; first exact: twp_free.
rewrite envs_lookup_split //; simpl.
rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
@@ -319,7 +319,7 @@ Lemma tac_wp_load Δ Δ' s E i K b l q v Φ :
envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ?? Hi.
+ rewrite environments.envs_entails_unseal=> ?? Hi.
rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
apply later_mono.
@@ -332,7 +332,7 @@ Lemma tac_twp_load Δ s E i K b l q v Φ :
envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> ? Hi.
+ rewrite environments.envs_entails_unseal=> ? Hi.
rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
rewrite envs_lookup_split //; simpl.
destruct b; simpl.
@@ -349,7 +349,7 @@ Lemma tac_wp_store Δ Δ' s E i K l v v' Φ :
end →
envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ???.
+ rewrite environments.envs_entails_unseal=> ???.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -363,7 +363,7 @@ Lemma tac_twp_store Δ s E i K l v v' Φ :
end →
envs_entails Δ (WP fill K (Store (LitV l) v') @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq. intros.
+ rewrite environments.envs_entails_unseal. intros.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -twp_bind. eapply wand_apply; first by eapply twp_store.
rewrite envs_simple_replace_sound //; simpl.
@@ -379,7 +379,7 @@ Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
end →
envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ???.
+ rewrite environments.envs_entails_unseal=> ???.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -394,7 +394,7 @@ Lemma tac_twp_xchg Δ s E i K l v v' Φ :
end →
envs_entails Δ (WP fill K (Xchg (LitV l) v') @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq. intros.
+ rewrite environments.envs_entails_unseal. intros.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -twp_bind. eapply wand_apply; first by eapply twp_xchg.
rewrite envs_simple_replace_sound //; simpl.
@@ -415,7 +415,7 @@ Lemma tac_wp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) →
envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ??? Hsuc Hfail.
+ rewrite environments.envs_entails_unseal=> ??? Hsuc Hfail.
destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
destruct (decide (v = v1)) as [Heq|Hne].
- rewrite -wp_bind. eapply wand_apply.
@@ -440,7 +440,7 @@ Lemma tac_twp_cmpxchg Δ s E i K l v v1 v2 Φ :
envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) →
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> ?? Hsuc Hfail.
+ rewrite environments.envs_entails_unseal=> ?? Hsuc Hfail.
destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
destruct (decide (v = v1)) as [Heq|Hne].
- rewrite -twp_bind. eapply wand_apply.
@@ -460,7 +460,7 @@ Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ?????.
+ rewrite environments.envs_entails_unseal=> ?????.
rewrite -wp_bind. eapply wand_apply; first exact: wp_cmpxchg_fail.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
@@ -471,7 +471,7 @@ Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq. intros. rewrite -twp_bind.
+ rewrite environments.envs_entails_unseal. intros. rewrite -twp_bind.
eapply wand_apply; first exact: twp_cmpxchg_fail.
(* [//] solves some evars and enables further simplification. *)
rewrite envs_lookup_split /= // /=. by do 2 f_equiv.
@@ -488,7 +488,7 @@ Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
end →
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ?????; subst.
+ rewrite environments.envs_entails_unseal=> ?????; subst.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cmpxchg_suc; eauto. }
@@ -505,7 +505,7 @@ Lemma tac_twp_cmpxchg_suc Δ s E i K l v v1 v2 Φ :
end →
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=>????; subst.
+ rewrite environments.envs_entails_unseal=>????; subst.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cmpxchg_suc; eauto. }
@@ -522,7 +522,7 @@ Lemma tac_wp_faa Δ Δ' s E i K l z1 z2 Φ :
end →
envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
Proof.
- rewrite envs_entails_eq=> ???.
+ rewrite environments.envs_entails_unseal=> ???.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -536,7 +536,7 @@ Lemma tac_twp_faa Δ s E i K l z1 z2 Φ :
end →
envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
Proof.
- rewrite envs_entails_eq=> ??.
+ rewrite environments.envs_entails_unseal=> ??.
destruct (envs_simple_replace _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ].
rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
rewrite envs_simple_replace_sound //; simpl.
diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v
index 6bb43fa67f38b78674d64ec36306d48f44bd10fd..b86424c9c62cb2bd9373a893a2d3b2c6f389b1eb 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -32,21 +32,23 @@ Global Instance subG_mono_listΣ {A Σ} :
subG (mono_listΣ A) Σ → (mono_listG A) Σ.
Proof. solve_inG. Qed.
-Definition mono_list_auth_own_def `{!mono_listG A Σ}
+Local Definition mono_list_auth_own_def `{!mono_listG A Σ}
(γ : gname) (q : Qp) (l : list A) : iProp Σ :=
own γ (â—ML{#q} (l : listO (leibnizO A))).
-Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def). Proof. by eexists. Qed.
+Local Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def).
+Proof. by eexists. Qed.
Definition mono_list_auth_own := mono_list_auth_own_aux.(unseal).
-Definition mono_list_auth_own_eq :
+Local Definition mono_list_auth_own_unseal :
@mono_list_auth_own = @mono_list_auth_own_def := mono_list_auth_own_aux.(seal_eq).
Global Arguments mono_list_auth_own {A Σ _} γ q l.
-Definition mono_list_lb_own_def `{!mono_listG A Σ}
+Local Definition mono_list_lb_own_def `{!mono_listG A Σ}
(γ : gname) (l : list A) : iProp Σ :=
own γ (◯ML (l : listO (leibnizO A))).
-Definition mono_list_lb_own_aux : seal (@mono_list_lb_own_def). Proof. by eexists. Qed.
+Local Definition mono_list_lb_own_aux : seal (@mono_list_lb_own_def).
+Proof. by eexists. Qed.
Definition mono_list_lb_own := mono_list_lb_own_aux.(unseal).
-Definition mono_list_lb_own_eq :
+Local Definition mono_list_lb_own_unseal :
@mono_list_lb_own = @mono_list_lb_own_def := mono_list_lb_own_aux.(seal_eq).
Global Arguments mono_list_lb_own {A Σ _} γ l.
@@ -55,8 +57,8 @@ Definition mono_list_idx_own `{!mono_listG A Σ}
∃ l : list A, ⌜ l !! i = Some a ⌠∗ mono_list_lb_own γ l.
Local Ltac unseal := rewrite
- /mono_list_idx_own ?mono_list_auth_own_eq /mono_list_auth_own_def
- ?mono_list_lb_own_eq /mono_list_lb_own_def.
+ /mono_list_idx_own ?mono_list_auth_own_unseal /mono_list_auth_own_def
+ ?mono_list_lb_own_unseal /mono_list_lb_own_def.
Section mono_list_own.
Context `{!mono_listG A Σ}.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index de2eaa478f72dab7fab448d322cfd1e385d35a22..0efc4745a5fa1598bd036635d3b581ea7d690c47 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -30,86 +30,87 @@ Inductive heapProp_entails (P Q : heapProp) : Prop :=
{ heapProp_in_entails : ∀ σ, P σ → Q σ }.
(** logical connectives *)
-Definition heapProp_emp_def : heapProp :=
+Local Definition heapProp_emp_def : heapProp :=
{| heapProp_holds σ := σ = ∅ |}.
-Definition heapProp_emp_aux : seal (@heapProp_emp_def). Proof. by eexists. Qed.
+Local Definition heapProp_emp_aux : seal (@heapProp_emp_def). Proof. by eexists. Qed.
Definition heapProp_emp := unseal heapProp_emp_aux.
-Definition heapProp_emp_eq :
+Local Definition heapProp_emp_unseal :
@heapProp_emp = @heapProp_emp_def := seal_eq heapProp_emp_aux.
-Definition heapProp_pure_def (φ : Prop) : heapProp :=
+Local Definition heapProp_pure_def (φ : Prop) : heapProp :=
{| heapProp_holds _ := φ |}.
-Definition heapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.
+Local Definition heapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.
Definition heapProp_pure := unseal heapProp_pure_aux.
-Definition heapProp_pure_eq :
+Local Definition heapProp_pure_unseal :
@heapProp_pure = @heapProp_pure_def := seal_eq heapProp_pure_aux.
-Definition heapProp_and_def (P Q : heapProp) : heapProp :=
+Local Definition heapProp_and_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := P σ ∧ Q σ |}.
-Definition heapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.
+Local Definition heapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.
Definition heapProp_and := unseal heapProp_and_aux.
-Definition heapProp_and_eq:
+Local Definition heapProp_and_unseal:
@heapProp_and = @heapProp_and_def := seal_eq heapProp_and_aux.
-Definition heapProp_or_def (P Q : heapProp) : heapProp :=
+Local Definition heapProp_or_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := P σ ∨ Q σ |}.
-Definition heapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.
+Local Definition heapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.
Definition heapProp_or := unseal heapProp_or_aux.
-Definition heapProp_or_eq:
+Local Definition heapProp_or_unseal:
@heapProp_or = @heapProp_or_def := seal_eq heapProp_or_aux.
-Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
+Local Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := P σ → Q σ |}.
-Definition heapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.
+Local Definition heapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.
Definition heapProp_impl := unseal heapProp_impl_aux.
-Definition heapProp_impl_eq :
+Local Definition heapProp_impl_unseal :
@heapProp_impl = @heapProp_impl_def := seal_eq heapProp_impl_aux.
-Definition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp :=
+Local Definition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp :=
{| heapProp_holds σ := ∀ a, Ψ a σ |}.
-Definition heapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.
+Local Definition heapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.
Definition heapProp_forall {A} := unseal heapProp_forall_aux A.
-Definition heapProp_forall_eq :
+Local Definition heapProp_forall_unseal :
@heapProp_forall = @heapProp_forall_def := seal_eq heapProp_forall_aux.
-Definition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp :=
+Local Definition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp :=
{| heapProp_holds σ := ∃ a, Ψ a σ |}.
-Definition heapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.
+Local Definition heapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.
Definition heapProp_exist {A} := unseal heapProp_exist_aux A.
-Definition heapProp_exist_eq :
+Local Definition heapProp_exist_unseal :
@heapProp_exist = @heapProp_exist_def := seal_eq heapProp_exist_aux.
-Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
+Local Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
-Definition heapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.
+Local Definition heapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.
Definition heapProp_sep := unseal heapProp_sep_aux.
-Definition heapProp_sep_eq:
+Local Definition heapProp_sep_unseal:
@heapProp_sep = @heapProp_sep_def := seal_eq heapProp_sep_aux.
-Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
+Local Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
-Definition heapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.
+Local Definition heapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.
Definition heapProp_wand := unseal heapProp_wand_aux.
-Definition heapProp_wand_eq:
+Local Definition heapProp_wand_unseal:
@heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
-Definition heapProp_persistently_def (P : heapProp) : heapProp :=
+Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
{| heapProp_holds σ := P ∅ |}.
-Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
+Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
Proof. by eexists. Qed.
Definition heapProp_persistently := unseal heapProp_persistently_aux.
-Definition heapProp_persistently_eq:
+Local Definition heapProp_persistently_unseal:
@heapProp_persistently = @heapProp_persistently_def := seal_eq heapProp_persistently_aux.
(** Iris's [bi] class requires the presence of a later modality, but for non
step-indexed logics, it can be defined as the identity. *)
Definition heapProp_later (P : heapProp) : heapProp := P.
-Definition unseal_eqs :=
- (heapProp_emp_eq, heapProp_pure_eq, heapProp_and_eq, heapProp_or_eq,
- heapProp_impl_eq, heapProp_forall_eq, heapProp_exist_eq,
- heapProp_sep_eq, heapProp_wand_eq, heapProp_persistently_eq).
-Ltac unseal := rewrite !unseal_eqs /=.
+Definition heapProp_unseal :=
+ (heapProp_emp_unseal, heapProp_pure_unseal, heapProp_and_unseal,
+ heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
+ heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
+ heapProp_persistently_unseal).
+Ltac unseal := rewrite !heapProp_unseal /=.
Section mixins.
(** Enable [simpl] locally, which is useful for proofs in the model. *)