diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3330e7f258f51bc7d896b2536e59d406d42e79d9..a25e051f789583dafd45c18e8b4388e3a47b4f88 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -37,6 +37,12 @@ Coq 8.13 is no longer supported.
as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y âŒ`.
* Add constructions `bi_tc`/`bi_nsteps` to create the transitive/`n`-step
closure of a PROP-level binary relation. (by Simcha van Collem).
+* Make the `unseal` tactic of `monPred` more consistent with `uPred`:
+ + Rename `MonPred.unseal` → `monPred.unseal`
+ + No longer unfold derived BI connectives `<affine>`, `<absorb>` and `â—‡`.
+ * Make `monPred.unseal` tactic more robust by using types to unfold the right
+ BI projections.
+* Add `unseal` tactic for `siProp`.
**Changes in `proofmode`:**
@@ -62,6 +68,8 @@ Coq 8.13 is no longer supported.
* Add `IsExcept0` instance for invariants, allowing you to remove laters of
timeless hypotheses when proving an invariant (without an update).
+* Make `uPred.unseal` tactic more robust by using types to unfold the right
+ BI projections.
**Changes in `heap_lang`:**
@@ -85,6 +93,8 @@ s/\bsig_dist_alt\b/sig_dist_def/g
# Loc
s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
+# unseal
+s/\bMonPred\.unseal\b/monPred\.unseal/g
EOF
```
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index dbd09ef0551e4825d9ee441420865004d9f90558..954ab7b0d49419cd5a3eb8769be21fabbfec3354 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -249,20 +249,49 @@ Section restate.
Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
Proof. apply later_soundness. Qed.
- (** See [derived.v] for a similar soundness result for basic updates. *)
-End restate.
-
-(** New unseal tactic that also unfolds the BI layer.
- This is used by [base_logic.algebra] and [base_logic.bupd_alt].
- TODO: Can we get rid of this? *)
-Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
- unfold bi_emp; simpl;
- unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
- bi_and, bi_or, bi_impl, bi_forall, bi_exist,
- bi_sep, bi_wand, bi_persistently, bi_later; simpl;
- unfold internal_eq, bi_internal_eq_internal_eq,
- plainly, bi_plainly_plainly; simpl;
- uPred_primitive.unseal.
+ (** We restate the unsealing lemmas for the BI layer. The sealing lemmas
+ are partially applied so that they also rewrite under binders. *)
+ Local Lemma uPred_emp_unseal : bi_emp = @upred.uPred_pure_def M True.
+ Proof. by rewrite -upred.uPred_pure_unseal. Qed.
+ Local Lemma uPred_pure_unseal : bi_pure = @upred.uPred_pure_def M.
+ Proof. by rewrite -upred.uPred_pure_unseal. Qed.
+ Local Lemma uPred_and_unseal : bi_and = @upred.uPred_and_def M.
+ Proof. by rewrite -upred.uPred_and_unseal. Qed.
+ Local Lemma uPred_or_unseal : bi_or = @upred.uPred_or_def M.
+ Proof. by rewrite -upred.uPred_or_unseal. Qed.
+ Local Lemma uPred_impl_unseal : bi_impl = @upred.uPred_impl_def M.
+ Proof. by rewrite -upred.uPred_impl_unseal. Qed.
+ Local Lemma uPred_forall_unseal : @bi_forall _ = @upred.uPred_forall_def M.
+ Proof. by rewrite -upred.uPred_forall_unseal. Qed.
+ Local Lemma uPred_exist_unseal : @bi_exist _ = @upred.uPred_exist_def M.
+ Proof. by rewrite -upred.uPred_exist_unseal. Qed.
+ Local Lemma uPred_internal_eq_unseal :
+ @internal_eq _ _ = @upred.uPred_internal_eq_def M.
+ Proof. by rewrite -upred.uPred_internal_eq_unseal. Qed.
+ Local Lemma uPred_sep_unseal : bi_sep = @upred.uPred_sep_def M.
+ Proof. by rewrite -upred.uPred_sep_unseal. Qed.
+ Local Lemma uPred_wand_unseal : bi_wand = @upred.uPred_wand_def M.
+ Proof. by rewrite -upred.uPred_wand_unseal. Qed.
+ Local Lemma uPred_plainly_unseal : plainly = @upred.uPred_plainly_def M.
+ Proof. by rewrite -upred.uPred_plainly_unseal. Qed.
+ Local Lemma uPred_persistently_unseal :
+ bi_persistently = @upred.uPred_persistently_def M.
+ Proof. by rewrite -upred.uPred_persistently_unseal. Qed.
+ Local Lemma uPred_later_unseal : bi_later = @upred.uPred_later_def M.
+ Proof. by rewrite -upred.uPred_later_unseal. Qed.
+ Local Lemma uPred_bupd_unseal : bupd = @upred.uPred_bupd_def M.
+ Proof. by rewrite -upred.uPred_bupd_unseal. Qed.
+
+ Local Definition uPred_unseal :=
+ (uPred_emp_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.uPred_ownM_unseal, upred.uPred_cmra_valid_unseal, @uPred_bupd_unseal).
+End restate.
+(** A tactic for rewriting with the above lemmas. Unfolds [uPred] goals that use
+the BI layer. This is used by [base_logic.algebra] and [base_logic.bupd_alt]. *)
+Ltac unseal := rewrite !uPred_unseal /=.
End uPred.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index ebfd40b43ee4552b64cbb2aeea05a00db615bc14..fa923f412109cd974ea65c27f8fec1b94f07ae72 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -112,9 +112,9 @@ Global Arguments monPred_at {_ _} _%I _.
Local Existing Instance monPred_mono.
Global Arguments monPredO _ _ : clear implicits.
-(** BI canonical structure *)
-
-Section bi.
+(** BI canonical structure and type class instances *)
+Module Export monPred_defs.
+Section monPred_defs.
Context {I : biIndex} {PROP : bi}.
Implicit Types i : I.
Notation monPred := (monPred I PROP).
@@ -249,33 +249,68 @@ Section bi.
Definition monPred_later := monPred_later_aux.(unseal).
Local Definition monPred_later_unseal :
monPred_later = _ := monPred_later_aux.(seal_eq).
-End bi.
+
+ 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).
+ Global Arguments monPred_internal_eq {_}.
+ Local Definition monPred_internal_eq_unseal `{!BiInternalEq PROP} :
+ @internal_eq _ monPred_internal_eq = monPred_internal_eq_def.
+ Proof. by rewrite -monPred_internal_eq_aux.(seal_eq). Qed.
+
+ Local Program Definition monPred_bupd_def `{BiBUpd PROP}
+ (P : monPred) : monPred := MonPred (λ i, |==> P i)%I _.
+ Next Obligation. solve_proper. Qed.
+ Local Definition monPred_bupd_aux : seal (@monPred_bupd_def).
+ Proof. by eexists. Qed.
+ Definition monPred_bupd := monPred_bupd_aux.(unseal).
+ Global Arguments monPred_bupd {_}.
+ Local Definition monPred_bupd_unseal `{BiBUpd PROP} :
+ @bupd _ monPred_bupd = monPred_bupd_def.
+ Proof. by rewrite -monPred_bupd_aux.(seal_eq). Qed.
+
+ 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.
+ Local Definition monPred_fupd_aux : seal (@monPred_fupd_def).
+ Proof. by eexists. Qed.
+ Definition monPred_fupd := monPred_fupd_aux.(unseal).
+ Global Arguments monPred_fupd {_}.
+ Local Definition monPred_fupd_unseal `{BiFUpd PROP} :
+ @fupd _ monPred_fupd = monPred_fupd_def.
+ Proof. by rewrite -monPred_fupd_aux.(seal_eq). Qed.
+
+ Local Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
+ MonPred (λ _, ∀ i, ■(P i))%I _.
+ Local Definition monPred_plainly_aux : seal (@monPred_plainly_def).
+ Proof. by eexists. Qed.
+ Definition monPred_plainly := monPred_plainly_aux.(unseal).
+ Global Arguments monPred_plainly {_}.
+ Local Definition monPred_plainly_unseal `{BiPlainly PROP} :
+ @plainly _ monPred_plainly = monPred_plainly_def.
+ Proof. by rewrite -monPred_plainly_aux.(seal_eq). Qed.
+End monPred_defs.
+
+(** This is not the final collection of unsealing lemmas, below we redefine
+[monPred_unseal] to also unfold the BI layer (i.e., the projections of the BI
+structures/classes). *)
+Local Definition monPred_unseal :=
+ (@monPred_embed_unseal, @monPred_emp_unseal, @monPred_pure_unseal,
+ @monPred_objectively_unseal, @monPred_subjectively_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_in_unseal, @monPred_later_unseal).
+End monPred_defs.
Global Arguments monPred_objectively {_ _} _%I.
Global Arguments monPred_subjectively {_ _} _%I.
Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
-Module MonPred.
- Local 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 !monPred_unseal /=.
-End MonPred.
-
-Import MonPred.
-
-Section canonical.
+Section instances.
Context (I : biIndex) (PROP : bi).
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
@@ -283,7 +318,8 @@ Section canonical.
monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
monPred_persistently.
Proof.
- split; try unseal; try by (split=> ? /=; repeat f_equiv).
+ split; rewrite ?monPred_defs.monPred_unseal;
+ try by (split=> ? /=; repeat f_equiv).
- split.
+ intros P. by split.
+ intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
@@ -302,7 +338,7 @@ Section canonical.
apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
apply bi.impl_intro_r. by rewrite -HR /= !Hij.
- intros P Q R [HR]. split=> i /=.
- rewrite HR /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+ rewrite HR /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
apply bi.impl_elim_l.
- intros A P Ψ HΨ. split=> i. apply bi.forall_intro => ?. by apply HΨ.
- intros A Ψ. split=> i. by apply: bi.forall_elim.
@@ -328,11 +364,12 @@ Section canonical.
Qed.
Lemma monPred_bi_later_mixin :
- BiLaterMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
- monPred_or monPred_impl monPred_forall monPred_exist
- monPred_sep monPred_persistently monPred_later.
+ BiLaterMixin (PROP:=monPred I PROP)
+ monPred_entails monPred_pure
+ monPred_or monPred_impl monPred_forall monPred_exist
+ monPred_sep monPred_persistently monPred_later.
Proof.
- split; unseal.
+ split; rewrite ?monPred_defs.monPred_unseal.
- by split=> ? /=; repeat f_equiv.
- intros P Q [?]. split=> i. by apply bi.later_mono.
- intros P. split=> i /=. by apply bi.later_intro.
@@ -344,13 +381,260 @@ Section canonical.
- intros P. split=> i. by apply bi.later_persistently_2.
- intros P. split=> i /=. rewrite -bi.forall_intro.
+ apply bi.later_false_em.
- + intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij. by rewrite Hij.
+ + intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij.
+ by rewrite Hij.
Qed.
Canonical Structure monPredI : bi :=
{| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
bi_bi_later_mixin := monPred_bi_later_mixin |}.
-End canonical.
+
+ (** We restate the unsealing lemmas so that they also unfold the BI layer. The
+ sealing lemmas are partially applied so that they also work under binders. *)
+ Local Lemma monPred_emp_unseal :
+ bi_emp = @monPred_defs.monPred_emp_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_emp_unseal. Qed.
+ Local Lemma monPred_pure_unseal :
+ bi_pure = @monPred_defs.monPred_pure_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_pure_unseal. Qed.
+ Local Lemma monPred_and_unseal :
+ bi_and = @monPred_defs.monPred_and_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_and_unseal. Qed.
+ Local Lemma monPred_or_unseal :
+ bi_or = @monPred_defs.monPred_or_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_or_unseal. Qed.
+ Local Lemma monPred_impl_unseal :
+ bi_impl = @monPred_defs.monPred_impl_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_impl_unseal. Qed.
+ Local Lemma monPred_forall_unseal :
+ @bi_forall _ = @monPred_defs.monPred_forall_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_forall_unseal. Qed.
+ Local Lemma monPred_exist_unseal :
+ @bi_exist _ = @monPred_defs.monPred_exist_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_exist_unseal. Qed.
+ Local Lemma monPred_sep_unseal :
+ bi_sep = @monPred_defs.monPred_sep_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_sep_unseal. Qed.
+ Local Lemma monPred_wand_unseal :
+ bi_wand = @monPred_defs.monPred_wand_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_wand_unseal. Qed.
+ Local Lemma monPred_persistently_unseal :
+ bi_persistently = @monPred_defs.monPred_persistently_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_persistently_unseal. Qed.
+ Local Lemma monPred_later_unseal :
+ bi_later = @monPred_defs.monPred_later_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_later_unseal. Qed.
+
+ (** This definition only includes the unseal lemmas for the [bi] connectives.
+ After we have defined the right class instances, we define [monPred_unseal],
+ which also includes [embed], [internal_eq], [bupd], [fupd], [plainly],
+ [monPred_objectively], [monPred_subjectively] and [monPred_in]. *)
+ Local Definition monPred_unseal_bi :=
+ (monPred_emp_unseal, monPred_pure_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).
+
+ Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
+ Proof.
+ split; try apply _; rewrite /bi_emp_valid
+ !(monPred_defs.monPred_embed_unseal, monPred_unseal_bi); try done.
+ - move=> P /= [/(_ inhabitant) ?] //.
+ - intros PROP' ? P Q.
+ set (f P := @monPred_at I PROP P inhabitant).
+ assert (NonExpansive f) by solve_proper.
+ apply (f_equivI f).
+ - intros P Q. split=> i /=.
+ by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+ - intros P Q. split=> i /=.
+ by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+ Qed.
+ Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
+ {| bi_embed_mixin := monPred_embedding_mixin |}.
+
+ Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
+ BiInternalEqMixin monPredI monPred_internal_eq.
+ Proof.
+ split;
+ rewrite !(monPred_defs.monPred_internal_eq_unseal, monPred_unseal_bi).
+ - split=> i /=. solve_proper.
+ - intros A P a. split=> i /=. apply internal_eq_refl.
+ - intros A a b Ψ ?. split=> i /=.
+ setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
+ erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
+ - intros A1 A2 f g. split=> i /=. by apply fun_extI.
+ - intros A P x y. split=> i /=. by apply sig_equivI_1.
+ - intros A a b ?. split=> i /=. by apply discrete_eq_1.
+ - intros A x y. split=> i /=. by apply later_equivI_1.
+ - intros A x y. split=> i /=. by apply later_equivI_2.
+ Qed.
+ Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} :
+ BiInternalEq monPredI :=
+ {| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
+
+ Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
+ Proof.
+ split; rewrite !(monPred_defs.monPred_bupd_unseal, monPred_unseal_bi).
+ - split=>/= i. solve_proper.
+ - intros P. split=>/= i. apply bupd_intro.
+ - intros P Q [HPQ]. split=>/= i. by rewrite HPQ.
+ - intros P. split=>/= i. apply bupd_trans.
+ - intros P Q. split=>/= i. apply bupd_frame_r.
+ Qed.
+ Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
+ {| bi_bupd_mixin := monPred_bupd_mixin |}.
+
+ Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
+ Proof.
+ split; rewrite /bi_emp_valid /bi_except_0
+ !(monPred_defs.monPred_fupd_unseal, monPred_unseal_bi).
+ - split=>/= i. solve_proper.
+ - intros E1 E2 HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
+ - intros E1 E2 P. split=>/= i. apply except_0_fupd.
+ - intros E1 E2 P Q [HPQ]. split=>/= i. by rewrite HPQ.
+ - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
+ - intros E1 E2 Ef P HE1f. split=>/= i.
+ by rewrite (bi.forall_elim i) bi.pure_True // left_id fupd_mask_frame_r'.
+ - intros E1 E2 P Q. split=>/= i. apply fupd_frame_r.
+ Qed.
+ Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
+ {| bi_fupd_mixin := monPred_fupd_mixin |}.
+
+ Lemma monPred_plainly_mixin `{BiPlainly PROP} :
+ BiPlainlyMixin monPredI monPred_plainly.
+ Proof.
+ split; rewrite !(monPred_defs.monPred_plainly_unseal, monPred_unseal_bi).
+ - 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.
+ - intros P. split=> i /=. do 3 setoid_rewrite <-plainly_forall.
+ rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
+ - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
+ rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
+ - intros P Q. split=> i /=.
+ setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
+ do 2 setoid_rewrite <-plainly_forall.
+ setoid_rewrite plainly_impl_plainly. f_equiv.
+ do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
+ - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
+ - intros P Q. split=> i. apply bi.sep_elim_l, _.
+ - intros P. split=> i /=.
+ rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
+ - intros P. split=> i /=.
+ rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
+ Qed.
+ Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
+ {| bi_plainly_mixin := monPred_plainly_mixin |}.
+
+ Local Lemma monPred_embed_unseal :
+ embed = @monPred_defs.monPred_embed_def I PROP.
+ Proof. by rewrite -monPred_defs.monPred_embed_unseal. Qed.
+ Local Lemma monPred_internal_eq_unseal `{!BiInternalEq PROP} :
+ @internal_eq _ _ = @monPred_defs.monPred_internal_eq_def I PROP _.
+ Proof. by rewrite -monPred_defs.monPred_internal_eq_unseal. Qed.
+ Local Lemma monPred_bupd_unseal `{BiBUpd PROP} :
+ bupd = @monPred_defs.monPred_bupd_def I PROP _.
+ Proof. by rewrite -monPred_defs.monPred_bupd_unseal. Qed.
+ Local Lemma monPred_fupd_unseal `{BiFUpd PROP} :
+ fupd = @monPred_defs.monPred_fupd_def I PROP _.
+ Proof. by rewrite -monPred_defs.monPred_fupd_unseal. Qed.
+ Local Lemma monPred_plainly_unseal `{BiPlainly PROP} :
+ plainly = @monPred_defs.monPred_plainly_def I PROP _.
+ Proof. by rewrite -monPred_defs.monPred_plainly_unseal. Qed.
+
+ (** And finally the proper [unseal] tactic (which we also redefine outside
+ of the section since Ltac definitions do not outlive a section). *)
+ Local Definition monPred_unseal :=
+ (monPred_unseal_bi,
+ @monPred_defs.monPred_objectively_unseal,
+ @monPred_defs.monPred_subjectively_unseal,
+ @monPred_embed_unseal, @monPred_internal_eq_unseal,
+ @monPred_bupd_unseal, @monPred_fupd_unseal, @monPred_plainly_unseal,
+ @monPred_defs.monPred_in_unseal).
+ Ltac unseal := rewrite !monPred_unseal /=.
+
+ Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
+ Proof. split. by unseal. Qed.
+
+ Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
+ Proof. split; by unseal. Qed.
+
+ Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
+ BiEmbedInternalEq PROP monPredI.
+ Proof. split. by unseal. Qed.
+
+ Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
+ Proof. intros E P. split=> i. unseal. apply bupd_fupd. Qed.
+
+ Global Instance monPred_bi_embed_bupd `{!BiBUpd PROP} :
+ BiEmbedBUpd PROP monPredI.
+ Proof. split. by unseal. Qed.
+
+ Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
+ Proof. split. by unseal. Qed.
+
+ Global Instance monPred_bi_persistently_impl_plainly
+ `{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
+ BiPersistentlyImplPlainly monPredI.
+ Proof.
+ intros P Q. split=> i. unseal. setoid_rewrite bi.pure_impl_forall.
+ setoid_rewrite <-plainly_forall.
+ do 2 setoid_rewrite bi.persistently_forall.
+ by setoid_rewrite persistently_impl_plainly.
+ Qed.
+
+ Global Instance monPred_bi_prop_ext
+ `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
+ Proof.
+ intros P Q. split=> i /=. rewrite /bi_wand_iff. unseal.
+ rewrite -{3}(sig_monPred_sig P) -{3}(sig_monPred_sig Q)
+ -f_equivI -sig_equivI !discrete_fun_equivI /=.
+ f_equiv=> j. rewrite prop_ext.
+ by rewrite !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+ Qed.
+
+ Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP, @BiIndexBottom I bot} :
+ BiPlainlyExist PROP → BiPlainlyExist monPredI.
+ Proof.
+ split=> ? /=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1.
+ do 2 f_equiv. apply bi.forall_intro=> ?. by do 2 f_equiv.
+ Qed.
+
+ Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
+ BiEmbedPlainly PROP monPredI.
+ Proof.
+ split=> i. unseal. apply (anti_symm _).
+ - by apply bi.forall_intro.
+ - by rewrite (bi.forall_elim inhabitant).
+ Qed.
+
+ Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} :
+ BiBUpdPlainly monPredI.
+ Proof.
+ intros P. split=> /= i. unseal. by rewrite bi.forall_elim bupd_plainly.
+ Qed.
+
+ Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} :
+ BiFUpdPlainly monPredI.
+ Proof.
+ split; rewrite /bi_except_0; unseal.
+ - intros E P. split=>/= i.
+ by rewrite (bi.forall_elim i) fupd_plainly_mask_empty.
+ - intros E P R. split=>/= i.
+ rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
+ by rewrite (bi.forall_elim i) fupd_plainly_keep_l.
+ - intros E P. split=>/= i.
+ by rewrite (bi.forall_elim i) fupd_plainly_later.
+ - intros E A Φ. split=>/= i.
+ rewrite -fupd_plainly_forall_2. apply bi.forall_mono=> x.
+ by rewrite (bi.forall_elim i).
+ Qed.
+End instances.
+
+(** The final unseal tactic that also unfolds the BI layer. *)
+Module Import monPred.
+ Ltac unseal := rewrite !monPred_unseal /=.
+End monPred.
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
objective_at i j : P i -∗ P j.
@@ -408,7 +692,6 @@ Section bi_facts.
Qed.
Lemma monPred_at_intuitionistically_if i p P : (□?p P) i ⊣⊢ □?p (P i).
Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
-
Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i ⊣⊢ <absorb>?p (P i).
@@ -449,21 +732,21 @@ Section bi_facts.
Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
- Proof. split => ?. unseal. apply bi_positive. Qed.
+ Proof. split => ?. rewrite /bi_affinely. unseal. apply bi_positive. Qed.
Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
Proof. split => ?. unseal. by apply affine. Qed.
Lemma monPred_persistent P : (∀ i, Persistent (P i)) → Persistent P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
Lemma monPred_absorbing P : (∀ i, Absorbing (P i)) → Absorbing P.
- Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
+ Proof. intros HP. constructor=> i. rewrite /bi_absorbingly. unseal. apply HP. Qed.
Lemma monPred_affine P : (∀ i, Affine (P i)) → Affine P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i).
Proof. move => [] /(_ i). by unseal. Qed.
Global Instance monPred_at_absorbing P i : Absorbing P → Absorbing (P i).
- Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
+ Proof. move => [] /(_ i). rewrite /Absorbing /bi_absorbingly. by unseal. Qed.
Global Instance monPred_at_affine P i : Affine P → Affine (P i).
Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
@@ -473,30 +756,12 @@ Section bi_facts.
Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
Proof. apply monPred_absorbing=> j. rewrite monPred_at_in. apply _. Qed.
- Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
- Proof.
- split; try apply _; rewrite /bi_emp_valid; unseal; try done.
- - move=> P /= [/(_ inhabitant) ?] //.
- - intros PROP' ? P Q.
- set (f P := monPred_at P inhabitant).
- assert (NonExpansive f) by solve_proper.
- apply (f_equivI f).
- - intros P Q. split=> i /=.
- by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
- - intros P Q. split=> i /=.
- by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
- Qed.
- Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
- {| bi_embed_mixin := monPred_embedding_mixin |}.
- Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
- Proof. split. by unseal. Qed.
-
Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
Proof. by unseal. Qed.
- Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I.
+ Lemma monPred_emp_unfold : emp%I =@{monPred} ⎡emp : PROP⎤%I.
Proof. by unseal. Qed.
- Lemma monPred_pure_unfold : bi_pure = λ φ, ⎡ ⌜ φ ⌠: PROP⎤%I.
+ Lemma monPred_pure_unfold : bi_pure =@{_ → monPred} λ φ, ⎡ ⌜ φ ⌠: PROP⎤%I.
Proof. by unseal. Qed.
Lemma monPred_objectively_unfold : monPred_objectively = λ P, ⎡∀ i, P i⎤%I.
Proof. by unseal. Qed.
@@ -591,7 +856,7 @@ Section bi_facts.
apply bi.equiv_entails, conj, monPred_objectively_sep_2. unseal. split=>i /=.
rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
Qed.
- Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢ ⎡P⎤.
+ Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢@{monPredI} ⎡P⎤.
Proof.
apply bi.equiv_entails; split; unseal; split=>i /=.
- by rewrite (bi.forall_elim inhabitant).
@@ -621,13 +886,7 @@ Section bi_facts.
do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
Qed.
Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj> Q.
- Proof.
- unseal. split=>i. apply bi.equiv_entails; split=>/=.
- - apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
- - apply bi.or_elim; do 2 f_equiv.
- + apply bi.or_intro_l.
- + apply bi.or_intro_r.
- Qed.
+ Proof. split=>i. unseal. apply bi.or_exist. Qed.
Lemma monPred_subjectively_sep P Q : <subj> (P ∗ Q) ⊢ <subj> P ∗ <subj> Q.
Proof.
@@ -836,28 +1095,6 @@ Section bi_facts.
Qed.
(** BUpd *)
- Local Program Definition monPred_bupd_def `{!BiBUpd PROP} (P : monPred) : monPred :=
- MonPred (λ i, |==> P i)%I _.
- Next Obligation. solve_proper. Qed.
- Local Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
- Definition monPred_bupd := monPred_bupd_aux.(unseal).
- Local Arguments monPred_bupd {_}.
- Local Lemma monPred_bupd_unseal `{!BiBUpd PROP} :
- @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_unseal.
- - split=>/= i. solve_proper.
- - intros P. split=>/= i. apply bupd_intro.
- - intros P Q HPQ. split=>/= i. by rewrite HPQ.
- - intros P. split=>/= i. apply bupd_trans.
- - intros P Q. split=>/= i. rewrite !monPred_at_sep /=. apply bupd_frame_r.
- Qed.
- Global Instance monPred_bi_bupd `{!BiBUpd PROP} : BiBUpd monPredI :=
- {| bi_bupd_mixin := monPred_bupd_mixin |}.
-
Lemma monPred_at_bupd `{!BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
Proof. by rewrite monPred_bupd_unseal. Qed.
@@ -865,26 +1102,19 @@ Section bi_facts.
Objective (|==> P).
Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
- Global Instance monPred_bi_embed_bupd `{!BiBUpd PROP} :
- BiEmbedBUpd PROP monPredI.
- Proof. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
-
(** Later *)
- Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
- Proof. split; by unseal. Qed.
-
Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
- Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
+ Proof. move => [] /(_ i). rewrite /Timeless /bi_except_0. by unseal. Qed.
Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
- Proof. split => ? /=. unseal. apply timeless, _. Qed.
+ Proof. split => ? /=. rewrite /bi_except_0. unseal. apply timeless, _. Qed.
Global Instance monPred_objectively_timeless P : Timeless P → Timeless (<obj> P).
Proof.
- move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
+ move=>[]. rewrite /Timeless /bi_except_0. unseal=>Hti. split=> ? /=.
by apply timeless, bi.forall_timeless.
Qed.
Global Instance monPred_subjectively_timeless P : Timeless P → Timeless (<subj> P).
Proof.
- move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
+ move=>[]. rewrite /Timeless /bi_except_0. unseal=>Hti. split=> ? /=.
by apply timeless, bi.exist_timeless.
Qed.
@@ -893,7 +1123,7 @@ Section bi_facts.
Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
Proof. induction n as [|? IHn]; first done. rewrite /= monPred_at_later IHn //. Qed.
Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
- Proof. by unseal. Qed.
+ Proof. rewrite /bi_except_0. by unseal. Qed.
Global Instance later_objective P `{!Objective P} : Objective (â–· P).
Proof. intros ??. unseal. by rewrite objective_at. Qed.
@@ -903,38 +1133,6 @@ Section bi_facts.
Proof. rewrite /bi_except_0. apply _. Qed.
(** Internal equality *)
- 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 {_}.
- 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_unseal.
- - split=> i /=. solve_proper.
- - intros A P a. split=> i /=. apply internal_eq_refl.
- - intros A a b Ψ ?. split=> i /=. unseal.
- setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
- erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
- - intros A1 A2 f g. split=> i /=. unseal. by apply fun_extI.
- - intros A P x y. split=> i /=. by apply sig_equivI_1.
- - intros A a b ?. split=> i /=. unseal. by apply discrete_eq_1.
- - intros A x y. split=> i /=. unseal. by apply later_equivI_1.
- - intros A x y. split=> i /=. unseal. by apply later_equivI_2.
- Qed.
- Global Instance monPred_bi_internal_eq `{!BiInternalEq PROP} : BiInternalEq monPredI :=
- {| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
-
- Global Instance monPred_bi_embed_internal_eq `{!BiInternalEq PROP} :
- BiEmbedInternalEq PROP monPredI.
- 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_unseal. by unseal. Qed.
@@ -957,42 +1155,6 @@ Section bi_facts.
Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
(** FUpd *)
- 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.
- Local Definition monPred_fupd_aux : seal (@monPred_fupd_def).
- Proof. by eexists. Qed.
- Definition monPred_fupd := monPred_fupd_aux.(unseal).
- Local Arguments monPred_fupd {_}.
- Local Lemma monPred_fupd_unseal `{!BiFUpd PROP} :
- @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_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.
- - intros E1 E2 P Q HPQ. split=>/= i. by rewrite HPQ.
- - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
- - intros E1 E2 Ef P HE1f. split=>/= i.
- rewrite monPred_impl_force monPred_at_pure -fupd_mask_frame_r' //.
- - intros E1 E2 P Q. split=>/= i. by rewrite !monPred_at_sep /= fupd_frame_r.
- Qed.
- Global Instance monPred_bi_fupd `{!BiFUpd PROP} : BiFUpd monPredI :=
- {| bi_fupd_mixin := monPred_fupd_mixin |}.
- Global Instance monPred_bi_bupd_fupd
- `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} :
- BiBUpdFUpd monPredI.
- Proof.
- intros E P. split=>/= i.
- rewrite monPred_at_bupd monPred_fupd_unseal bupd_fupd //=.
- Qed.
- Global Instance monPred_bi_embed_fupd `{!BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
- 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_unseal. Qed.
@@ -1002,88 +1164,6 @@ Section bi_facts.
Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
(** Plainly *)
- Local Definition monPred_plainly_def `{!BiPlainly PROP} P : monPred :=
- MonPred (λ _, ∀ i, ■(P i))%I _.
- Local Definition monPred_plainly_aux : seal (@monPred_plainly_def).
- Proof. by eexists. Qed.
- Definition monPred_plainly := monPred_plainly_aux.(unseal).
- Local Arguments monPred_plainly {_}.
- Local Lemma monPred_plainly_unseal `{!BiPlainly PROP} :
- @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_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.
- - intros P. split=> i /=. do 3 setoid_rewrite <-plainly_forall.
- rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
- - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
- rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
- - intros P Q. split=> i /=.
- setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
- do 2 setoid_rewrite <-plainly_forall.
- setoid_rewrite plainly_impl_plainly. f_equiv.
- do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
- - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
- - intros P Q. split=> i. apply bi.sep_elim_l, _.
- - intros P. split=> i /=.
- rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
- - intros P. split=> i /=.
- rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
- Qed.
- Global Instance monPred_bi_plainly `{!BiPlainly PROP} : BiPlainly monPredI :=
- {| bi_plainly_mixin := monPred_plainly_mixin |}.
-
- Global Instance minPred_bi_persistently_impl_plainly
- `{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
- BiPersistentlyImplPlainly monPredI.
- Proof.
- 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.
- apply: persistently_impl_plainly.
- Qed.
-
- Global Instance monPred_bi_prop_ext
- `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
- Proof.
- 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.
-
- Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP} `{!BiIndexBottom bot} :
- BiPlainlyExist PROP → BiPlainlyExist monPredI.
- Proof.
- 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.
-
- Global Instance monPred_bi_embed_plainly `{!BiPlainly PROP} :
- BiEmbedPlainly PROP monPredI.
- Proof.
- split=> i. rewrite monPred_plainly_unseal; unseal. apply (anti_symm _).
- - by apply bi.forall_intro.
- - by rewrite (bi.forall_elim inhabitant).
- Qed.
-
- Global Instance monPred_bi_bupd_plainly
- `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly PROP} :
- BiBUpdPlainly monPredI.
- Proof.
- intros P. split=> /= i.
- 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_unseal monPred_embed_unseal. Qed.
Lemma monPred_at_plainly `{!BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
@@ -1092,23 +1172,6 @@ Section bi_facts.
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
- `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} :
- BiFUpdPlainly monPredI.
- Proof.
- 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.
- rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
- by rewrite monPred_at_plainly (bi.forall_elim i) fupd_plainly_keep_l.
- - intros E P. split=>/= i.
- by rewrite monPred_at_plainly (bi.forall_elim i) fupd_plainly_later.
- - intros E A Φ. split=>/= i.
- rewrite -fupd_plainly_forall_2. apply bi.forall_mono=> x.
- by rewrite monPred_at_plainly (bi.forall_elim i).
- Qed.
-
Global Instance plainly_objective `{!BiPlainly PROP} P : Objective (â– P).
Proof. rewrite monPred_plainly_unfold. apply _. Qed.
Global Instance plainly_if_objective `{!BiPlainly PROP} P p `{!Objective P} :
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index e0ac0abbfb7c565eb2a367d35b862d5aa0b78b71..a7839f6af9b31af557e7068a439cb8b38e65ed8e 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -185,5 +185,44 @@ Section restate.
Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
Proof. apply later_soundness. Qed.
+
+ (** We restate the unsealing lemmas so that they also unfold the BI layer. The
+ sealing lemmas are partially applied so that they also work under binders. *)
+ Local Lemma siProp_emp_unseal : bi_emp = @siprop.siProp_pure_def True.
+ Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
+ Local Lemma siProp_pure_unseal : bi_pure = @siprop.siProp_pure_def.
+ Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
+ Local Lemma siProp_and_unseal : bi_and = @siprop.siProp_and_def.
+ Proof. by rewrite -siprop.siProp_and_unseal. Qed.
+ Local Lemma siProp_or_unseal : bi_or = @siprop.siProp_or_def.
+ Proof. by rewrite -siprop.siProp_or_unseal. Qed.
+ Local Lemma siProp_impl_unseal : bi_impl = @siprop.siProp_impl_def.
+ Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
+ Local Lemma siProp_forall_unseal : @bi_forall _ = @siprop.siProp_forall_def.
+ Proof. by rewrite -siprop.siProp_forall_unseal. Qed.
+ Local Lemma siProp_exist_unseal : @bi_exist _ = @siprop.siProp_exist_def.
+ Proof. by rewrite -siprop.siProp_exist_unseal. Qed.
+ Local Lemma siProp_internal_eq_unseal :
+ @internal_eq _ _ = @siprop.siProp_internal_eq_def.
+ Proof. by rewrite -siprop.siProp_internal_eq_unseal. Qed.
+ Local Lemma siProp_sep_unseal : bi_sep = @siprop.siProp_and_def.
+ Proof. by rewrite -siprop.siProp_and_unseal. Qed.
+ Local Lemma siProp_wand_unseal : bi_wand = @siprop.siProp_impl_def.
+ Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
+ Local Lemma siProp_plainly_unseal : plainly = @id siProp.
+ Proof. done. Qed.
+ Local Lemma siProp_persistently_unseal : bi_persistently = @id siProp.
+ Proof. done. Qed.
+ Local Lemma siProp_later_unseal : bi_later = @siprop.siProp_later_def.
+ Proof. by rewrite -siprop.siProp_later_unseal. Qed.
+
+ Local Definition siProp_unseal :=
+ (siProp_emp_unseal, siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
+ siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
+ siProp_internal_eq_unseal, siProp_sep_unseal, siProp_wand_unseal,
+ siProp_plainly_unseal, siProp_persistently_unseal, siProp_later_unseal).
End restate.
+
+(** The final unseal tactic that also unfolds the BI layer. *)
+Ltac unseal := rewrite !siProp_unseal /=.
End siProp.
diff --git a/tests/monpred.ref b/tests/monpred.ref
new file mode 100644
index 0000000000000000000000000000000000000000..4cbbc11183db0ed024ec6fc7fc3c8711ccc0b83b
--- /dev/null
+++ b/tests/monpred.ref
@@ -0,0 +1,21 @@
+"monPred_unseal_test_1"
+ : string
+1 goal
+
+ I : biIndex
+ M : ucmra
+ P, Q : uPredI M
+ R : monPred
+ i : I
+ ============================
+ (P ∗ Q) ∗ R i ⊣⊢ False
+"monPred_unseal_test_2"
+ : string
+1 goal
+
+ I : biIndex
+ M : ucmra
+ P, Q : uPredI M
+ R : monPred
+ ============================
+ ⎡ upred.uPred_sep_def P Q ⎤ ∗ R ⊣⊢ False
diff --git a/tests/monpred.v b/tests/monpred.v
new file mode 100644
index 0000000000000000000000000000000000000000..26e467e11ba8304dc6458c963506ec358bb32766
--- /dev/null
+++ b/tests/monpred.v
@@ -0,0 +1,27 @@
+From stdpp Require Import strings.
+From iris.base_logic Require Import bi.
+From iris.bi Require Import embedding monpred.
+
+Section tests_unseal.
+ Context {I : biIndex} (M : ucmra).
+
+ Local Notation monPred := (monPred I (uPredI M)).
+
+ Check "monPred_unseal_test_1".
+ Lemma monPred_unseal_test_1 P Q (R : monPred) :
+ ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
+ Proof.
+ intros. split=> i. monPred.unseal.
+ (** Make sure [∗] on uPred is not unfolded *)
+ Show.
+ Abort.
+
+ Check "monPred_unseal_test_2".
+ Lemma monPred_unseal_test_2 P Q (R : monPred) :
+ ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
+ Restart.
+ uPred.unseal.
+ (** Make sure [∗] on monPred is not unfolded *)
+ Show.
+ Abort.
+End tests_unseal.
diff --git a/tests/siprop.ref b/tests/siprop.ref
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..c7ab6a8bf472dcb11e41b51cdfd0ce63b30a292a 100644
--- a/tests/siprop.ref
+++ b/tests/siprop.ref
@@ -0,0 +1,17 @@
+"unseal_test"
+ : string
+1 goal
+
+ P, Q : siProp
+ Φ : nat → siProp
+ ============================
+ siprop.siProp_and_def P
+ (siprop.siProp_and_def (siprop.siProp_later_def Q)
+ (siprop.siProp_exist_def (λ x : nat, Φ x)))
+ ⊣⊢ siprop.siProp_exist_def
+ (λ x : nat,
+ siprop.siProp_or_def
+ (siprop.siProp_and_def P
+ (siprop.siProp_and_def (siprop.siProp_later_def Q)
+ (siprop.siProp_pure_def True)))
+ (Φ x))
diff --git a/tests/siprop.v b/tests/siprop.v
index fc72d0ccce2bfc8f9b98adb2786bcbb09867b22f..9e6c6b7d5e51af448cbaa3eb0c9cf37cb4958869 100644
--- a/tests/siprop.v
+++ b/tests/siprop.v
@@ -1,4 +1,14 @@
+From stdpp Require Import strings.
From iris.si_logic Require Import bi.
+Unset Mangle Names.
+
+Check "unseal_test".
+Lemma unseal_test (P Q : siProp) (Φ : nat → siProp) :
+ P ∧ ▷ Q ∧ (∃ x, Φ x) ⊣⊢ ∃ x, P ∗ ▷ Q ∧ emp ∨ Φ x.
+Proof.
+ siProp.unseal.
+ Show.
+Abort.
(** Make sure that [siProp]s are parsed in [bi_scope]. *)
Definition test : siProp := â–· True.