From a38db10857643c13567924907bb2fb332d20532e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 2 Nov 2017 00:06:57 +0100
Subject: [PATCH] Remove notations for bi_bare and bi_persistently.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
(â–¡ P) now means (bi_bare (bi_persistently P)).
This is motivated by the fact that these two modalities are rarely
used separately.
In the case of an affine BI, we keep the â–¡ notation. This means that a
bi_bare is inserted each time we use â–¡. Hence, a few adaptations need
to be done in the proof mode class instances.
---
theories/base_logic/derived.v | 16 +-
theories/base_logic/lib/viewshifts.v | 5 +-
theories/base_logic/upred.v | 24 +-
theories/bi/big_op.v | 26 +-
theories/bi/derived.v | 341 +++++++++++++++------------
theories/bi/fixpoint.v | 12 +-
theories/bi/interface.v | 48 ++--
theories/program_logic/hoare.v | 2 +-
theories/proofmode/class_instances.v | 145 +++++++-----
theories/proofmode/classes.v | 16 +-
theories/proofmode/coq_tactics.v | 83 +++----
theories/proofmode/tactics.v | 8 +-
theories/tests/proofmode.v | 32 +--
13 files changed, 421 insertions(+), 337 deletions(-)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 7389de3a6..8ac0024a1 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -36,9 +36,9 @@ Global Instance uPred_affine : AffineBI (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
(* Own and valid derived *)
-Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma bare_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
- intros; apply (anti_symm _); first by rewrite persistently_elim.
+ rewrite affine_bare=>?; apply (anti_symm _); [by rewrite persistently_elim|].
by rewrite {1}persistently_ownM_core core_id_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
@@ -47,9 +47,9 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
-Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma bare_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
Proof.
- intros; apply (anti_symm _); first by rewrite persistently_elim.
+ rewrite affine_bare. intros; apply (anti_symm _); first by rewrite persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
@@ -98,9 +98,11 @@ Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
(* Persistence *)
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
Persistent (✓ a : uPred M)%I.
-Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed.
-Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
-Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
+Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
+Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
+Proof.
+ intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
+Qed.
(* For big ops *)
Global Instance uPred_ownM_sep_homomorphism :
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 4534a0bd2..08f270489 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -81,5 +81,8 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
-Proof. rewrite bi.wand_alt. by setoid_rewrite bi.persistently_impl_wand. Qed.
+Proof.
+ rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_bare; last apply _.
+ by rewrite bi.persistently_impl_wand.
+Qed.
End vs.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 29695fe35..ecc41121e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -438,21 +438,21 @@ Proof.
- (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
eapply HPQR; eauto using cmra_validN_op_l.
- - (* (P ⊢ Q) → □ P ⊢ □ Q *)
+ - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
- - (* □ P ⊢ □ □ P *)
+ - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
- - (* (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a *)
+ - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
by unseal.
- - (* □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a *)
+ - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
by unseal.
- - (* P ⊢ □ emp (ADMISSIBLE) *)
+ - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
intros P. unfold uPred_emp; unseal; by split=> n x ? _.
- - (* □ P ∗ Q ⊢ □ P (ADMISSIBLE) *)
+ - (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
intros P Q. move: (uPred_persistently P)=> P'.
unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
eauto using uPred_mono, cmra_includedN_l.
- - (* □ P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
+ - (* bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
intros P Q. unseal; split=> n x ? [??]; simpl in *.
exists (core x), x; rewrite ?cmra_core_l; auto.
Qed.
@@ -489,9 +489,9 @@ Proof.
- (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S.
- - (* ▷ □ P ⊢ □ ▷ P *)
+ - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
by unseal.
- - (* □ ▷ P ⊢ ▷ □ P *)
+ - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
by unseal.
- (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
@@ -570,7 +570,8 @@ Proof.
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+Lemma persistently_ownM_core (a : M) :
+ uPred_ownM a ⊢ bi_persistently (uPred_ownM (core a)).
Proof.
rewrite /bi_persistently /=. unseal.
split=> n x Hx /=. by apply cmra_core_monoN.
@@ -601,7 +602,8 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u
Proof.
intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
Qed.
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
+ ✓ a ⊢ bi_persistently (✓ a : uPred M).
Proof. by unseal. Qed.
Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ (✓ a : uPred M).
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 03acdf1c7..c0c7cf886 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -126,7 +126,8 @@ Section sep_list.
Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
- (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
+ (bi_persistently ([∗ list] k↦x ∈ l, Φ k x)) ⊣⊢
+ ([∗ list] k↦x ∈ l, bi_persistently (Φ k x)).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_forall `{AffineBI PROP} Φ l :
@@ -144,12 +145,12 @@ Section sep_list.
Lemma big_sepL_impl Φ Ψ l :
([∗ list] k↦x ∈ l, Φ k x) -∗
- ⬕ (∀ k x, ⌜l !! k = Some x⌠→ Φ k x -∗ Ψ k x) -∗
+ □ (∀ k x, ⌜l !! k = Some x⌠→ Φ k x -∗ Ψ k x) -∗
[∗ list] k↦x ∈ l, Ψ k x.
Proof.
apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
{ by rewrite sep_elim_r. }
- rewrite bare_persistently_sep_dup -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc.
+ rewrite bare_persistently_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
apply sep_mono.
- rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
by rewrite bare_persistently_elim wand_elim_l.
@@ -264,7 +265,8 @@ Section and_list.
Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_andL_persistently Φ l :
- (□ [∧ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∧ list] k↦x ∈ l, □ Φ k x).
+ (bi_persistently ([∧ list] k↦x ∈ l, Φ k x)) ⊣⊢
+ ([∧ list] k↦x ∈ l, bi_persistently (Φ k x)).
Proof. apply (big_opL_commute _). Qed.
Lemma big_andL_forall `{AffineBI PROP} Φ l :
@@ -394,7 +396,8 @@ Section gmap.
Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
- (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
+ (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
+ ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_forall `{AffineBI PROP} Φ m :
@@ -416,13 +419,13 @@ Section gmap.
Lemma big_sepM_impl Φ Ψ m :
([∗ map] k↦x ∈ m, Φ k x) -∗
- ⬕ (∀ k x, ⌜m !! k = Some x⌠→ Φ k x -∗ Ψ k x) -∗
+ □ (∀ k x, ⌜m !! k = Some x⌠→ Φ k x -∗ Ψ k x) -∗
[∗ map] k↦x ∈ m, Ψ k x.
Proof.
apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
{ by rewrite sep_elim_r. }
rewrite !big_sepM_insert // bare_persistently_sep_dup.
- rewrite -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+ rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
- rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
by rewrite True_impl bare_persistently_elim wand_elim_l.
- rewrite comm -IH /=.
@@ -559,7 +562,7 @@ Section gset.
Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
- □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
+ bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, bi_persistently (Φ y)).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_forall `{AffineBI PROP} Φ X :
@@ -577,13 +580,13 @@ Section gset.
Lemma big_sepS_impl Φ Ψ X :
([∗ set] x ∈ X, Φ x) -∗
- ⬕ (∀ x, ⌜x ∈ X⌠→ Φ x -∗ Ψ x) -∗
+ □ (∀ x, ⌜x ∈ X⌠→ Φ x -∗ Ψ x) -∗
[∗ set] x ∈ X, Ψ x.
Proof.
apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
{ by rewrite sep_elim_r. }
rewrite !big_sepS_insert // bare_persistently_sep_dup.
- rewrite -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+ rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
- rewrite (forall_elim x) pure_True; last set_solver.
by rewrite True_impl bare_persistently_elim wand_elim_l.
- rewrite comm -IH /=. apply sep_mono_l, bare_mono, persistently_mono.
@@ -667,7 +670,8 @@ Section gmultiset.
Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
- □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
+ bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
+ ([∗ mset] y ∈ X, bi_persistently (Φ y)).
Proof. apply (big_opMS_commute _). Qed.
Global Instance big_sepMS_empty_persistent Φ :
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index f350f0599..94c19e04c 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
-Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ □ P.
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
@@ -23,8 +23,8 @@ Definition bi_bare {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
Arguments bi_bare {_} _%I : simpl never.
Instance: Params (@bi_bare) 1.
Typeclasses Opaque bi_bare.
-Notation "â– P" := (bi_bare P) (at level 20, right associativity) : bi_scope.
-Notation "⬕ P" := (■□ P)%I (at level 20, right associativity) : bi_scope.
+Notation "â–¡ P" := (bi_bare (bi_persistently P))%I
+ (at level 20, right associativity) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
Arguments Affine {_} _%I : simpl never.
@@ -35,7 +35,7 @@ Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Existing Instance absorbing_bi | 0.
Class PositiveBI (PROP : bi) :=
- positive_bi (P Q : PROP) : ■(P ∗ Q) ⊢ ■P ∗ Q.
+ positive_bi (P Q : PROP) : bi_bare (P ∗ Q) ⊢ bi_bare P ∗ Q.
Definition bi_sink {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
Arguments bi_sink {_} _%I : simpl never.
@@ -48,25 +48,19 @@ Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
- (if p then â–¡ P else P)%I.
+ (if p then bi_persistently P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.
-Notation "â–¡? p P" := (bi_persistently_if p P)
- (at level 20, p at level 9, P at level 20,
- right associativity, format "â–¡? p P") : bi_scope.
Definition bi_bare_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
- (if p then â– P else P)%I.
+ (if p then bi_bare P else P)%I.
Arguments bi_bare_if {_} !_ _%I /.
Instance: Params (@bi_bare_if) 2.
Typeclasses Opaque bi_bare_if.
-Notation "â– ? p P" := (bi_bare_if p P)
- (at level 20, p at level 9, P at level 20,
- right associativity, format "â– ? p P") : bi_scope.
-Notation "⬕? p P" := (■?p □?p P)%I
+Notation "â–¡? p P" := (bi_bare_if p (bi_persistently_if p P))%I
(at level 20, p at level 9, P at level 20,
- right associativity, format "⬕? p P") : bi_scope.
+ right associativity, format "â–¡? p P") : bi_scope.
Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
match As return himpl As PROP → PROP with
@@ -691,53 +685,53 @@ Global Instance bare_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@bi_bare PROP).
Proof. solve_proper. Qed.
-Lemma bare_elim_emp P : ■P ⊢ emp.
+Lemma bare_elim_emp P : bi_bare P ⊢ emp.
Proof. rewrite /bi_bare; auto. Qed.
-Lemma bare_elim P : ■P ⊢ P.
+Lemma bare_elim P : bi_bare P ⊢ P.
Proof. rewrite /bi_bare; auto. Qed.
-Lemma bare_mono P Q : (P ⊢ Q) → ■P ⊢ ■Q.
+Lemma bare_mono P Q : (P ⊢ Q) → bi_bare P ⊢ bi_bare Q.
Proof. by intros ->. Qed.
-Lemma bare_idemp P : ■■P ⊣⊢ ■P.
+Lemma bare_idemp P : bi_bare (bi_bare P) ⊣⊢ bi_bare P.
Proof. by rewrite /bi_bare assoc idemp. Qed.
-Lemma bare_intro' P Q : (■P ⊢ Q) → ■P ⊢ ■Q.
+Lemma bare_intro' P Q : (bi_bare P ⊢ Q) → bi_bare P ⊢ bi_bare Q.
Proof. intros <-. by rewrite bare_idemp. Qed.
-Lemma bare_False : ■False ⊣⊢ False.
+Lemma bare_False : bi_bare False ⊣⊢ False.
Proof. by rewrite /bi_bare right_absorb. Qed.
-Lemma bare_emp : ■emp ⊣⊢ emp.
+Lemma bare_emp : bi_bare emp ⊣⊢ emp.
Proof. by rewrite /bi_bare (idemp bi_and). Qed.
-Lemma bare_or P Q : ■(P ∨ Q) ⊣⊢ ■P ∨ ■Q.
+Lemma bare_or P Q : bi_bare (P ∨ Q) ⊣⊢ bi_bare P ∨ bi_bare Q.
Proof. by rewrite /bi_bare and_or_l. Qed.
-Lemma bare_and P Q : ■(P ∧ Q) ⊣⊢ ■P ∧ ■Q.
+Lemma bare_and P Q : bi_bare (P ∧ Q) ⊣⊢ bi_bare P ∧ bi_bare Q.
Proof.
rewrite /bi_bare -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
by rewrite idemp !assoc (comm _ P).
Qed.
-Lemma bare_sep_2 P Q : ■P ∗ ■Q ⊢ ■(P ∗ Q).
+Lemma bare_sep_2 P Q : bi_bare P ∗ bi_bare Q ⊢ bi_bare (P ∗ Q).
Proof.
rewrite /bi_bare. apply and_intro.
- by rewrite !and_elim_l right_id.
- by rewrite !and_elim_r.
Qed.
-Lemma bare_sep `{PositiveBI PROP} P Q : ■(P ∗ Q) ⊣⊢ ■P ∗ ■Q.
+Lemma bare_sep `{PositiveBI PROP} P Q : bi_bare (P ∗ Q) ⊣⊢ bi_bare P ∗ bi_bare Q.
Proof.
apply (anti_symm _), bare_sep_2.
- by rewrite -{1}bare_idemp positive_bi !(comm _ (â– P)%I) positive_bi.
+ by rewrite -{1}bare_idemp positive_bi !(comm _ (bi_bare P)%I) positive_bi.
Qed.
-Lemma bare_forall {A} (Φ : A → PROP) : ■(∀ a, Φ a) ⊢ ∀ a, ■Φ a.
+Lemma bare_forall {A} (Φ : A → PROP) : bi_bare (∀ a, Φ a) ⊢ ∀ a, bi_bare (Φ a).
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma bare_exist {A} (Φ : A → PROP) : ■(∃ a, Φ a) ⊣⊢ ∃ a, ■Φ a.
+Lemma bare_exist {A} (Φ : A → PROP) : bi_bare (∃ a, Φ a) ⊣⊢ ∃ a, bi_bare (Φ a).
Proof. by rewrite /bi_bare and_exist_l. Qed.
-Lemma bare_True_emp : ■True ⊣⊢ ■emp.
+Lemma bare_True_emp : bi_bare True ⊣⊢ bi_bare emp.
Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.
-Lemma bare_and_l P Q : ■P ∧ Q ⊣⊢ ■(P ∧ Q).
+Lemma bare_and_l P Q : bi_bare P ∧ Q ⊣⊢ bi_bare (P ∧ Q).
Proof. by rewrite /bi_bare assoc. Qed.
-Lemma bare_and_r P Q : P ∧ ■Q ⊣⊢ ■(P ∧ Q).
+Lemma bare_and_r P Q : P ∧ bi_bare Q ⊣⊢ bi_bare (P ∧ Q).
Proof. by rewrite /bi_bare !assoc (comm _ P). Qed.
-Lemma bare_and_lr P Q : ■P ∧ Q ⊣⊢ P ∧ ■Q.
+Lemma bare_and_lr P Q : bi_bare P ∧ Q ⊣⊢ P ∧ bi_bare Q.
Proof. by rewrite bare_and_l bare_and_r. Qed.
(* Properties of the sink modality *)
@@ -796,7 +790,7 @@ Proof. by rewrite /bi_sink !assoc (comm _ P). Qed.
Lemma sink_sep_lr P Q : ▲ P ∗ Q ⊣⊢ P ∗ ▲ Q.
Proof. by rewrite sink_sep_l sink_sep_r. Qed.
-Lemma bare_sink `{!PositiveBI PROP} P : ■▲ P ⊣⊢ ■P.
+Lemma bare_sink `{!PositiveBI PROP} P : bi_bare (▲ P) ⊣⊢ bi_bare P.
Proof.
apply (anti_symm _), bare_mono, sink_intro.
by rewrite /bi_sink bare_sep bare_True_emp bare_emp left_id.
@@ -823,7 +817,7 @@ Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
-Global Instance bare_affine P : Affine (â– P).
+Global Instance bare_affine P : Affine (bi_bare P).
Proof. rewrite /bi_bare. apply _. Qed.
(* Absorbing propositions *)
@@ -859,7 +853,7 @@ Global Instance sink_absorbing P : Absorbing (â–² P).
Proof. rewrite /bi_sink. apply _. Qed.
(* Properties of affine and absorbing propositions *)
-Lemma affine_bare P `{!Affine P} : ■P ⊣⊢ P.
+Lemma affine_bare P `{!Affine P} : bi_bare P ⊣⊢ P.
Proof. rewrite /bi_bare. apply (anti_symm _); auto. Qed.
Lemma absorbing_sink P `{!Absorbing P} : ▲ P ⊣⊢ P.
Proof. by apply (anti_symm _), sink_intro. Qed.
@@ -890,7 +884,7 @@ Proof.
Qed.
-Lemma bare_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ ■Q.
+Lemma bare_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ bi_bare Q.
Proof. intros <-. by rewrite affine_bare. Qed.
Lemma emp_and P `{!Affine P} : emp ∧ P ⊣⊢ P.
@@ -948,14 +942,15 @@ Global Instance persistently_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.
-Lemma sink_persistently P : ▲ □ P ⊣⊢ □ P.
+Lemma sink_persistently P : ▲ bi_persistently P ⊣⊢ bi_persistently P.
Proof.
apply (anti_symm _), sink_intro. by rewrite /bi_sink comm persistently_absorbing.
Qed.
-Global Instance persistently_absorbing P : Absorbing (â–¡ P).
+Global Instance persistently_absorbing P : Absorbing (bi_persistently P).
Proof. by rewrite /Absorbing sink_persistently. Qed.
-Lemma persistently_and_sep_assoc P Q R : □ P ∧ (Q ∗ R) ⊣⊢ (□ P ∧ Q) ∗ R.
+Lemma persistently_and_sep_assoc P Q R :
+ bi_persistently P ∧ (Q ∗ R) ⊣⊢ (bi_persistently P ∧ Q) ∗ R.
Proof.
apply (anti_symm (⊢)).
- rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
@@ -966,111 +961,129 @@ Proof.
+ by rewrite and_elim_l sep_elim_l.
+ by rewrite and_elim_r.
Qed.
-Lemma persistently_and_emp_elim P : emp ∧ □ P ⊢ P.
+Lemma persistently_and_emp_elim P : emp ∧ bi_persistently P ⊢ P.
Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
-Lemma persistently_elim_sink P : □ P ⊢ ▲ P.
+Lemma persistently_elim_sink P : bi_persistently P ⊢ ▲ P.
Proof.
- rewrite -(right_id True%I _ (â–¡ _)%I) -{1}(left_id emp%I _ True%I).
+ rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I).
by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm.
Qed.
-Lemma persistently_elim P `{!Absorbing P} : □ P ⊢ P.
+Lemma persistently_elim P `{!Absorbing P} : bi_persistently P ⊢ P.
Proof. by rewrite persistently_elim_sink absorbing_sink. Qed.
-Lemma persistently_idemp_1 P : □ □ P ⊢ □ P.
+Lemma persistently_idemp_1 P :
+ bi_persistently (bi_persistently P) ⊢ bi_persistently P.
Proof. by rewrite persistently_elim_sink sink_persistently. Qed.
-Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
+Lemma persistently_idemp P :
+ bi_persistently (bi_persistently P) ⊣⊢ bi_persistently P.
Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed.
-Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_intro' P Q :
+ (bi_persistently P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
Proof. intros <-. apply persistently_idemp_2. Qed.
-Lemma persistently_pure φ : â–¡ ⌜φ⌠⊣⊢ ⌜φâŒ.
+Lemma persistently_pure φ : bi_persistently ⌜φ⌠⊣⊢ ⌜φâŒ.
Proof.
apply (anti_symm _); first by rewrite persistently_elim.
apply pure_elim'=> Hφ.
- trans (∀ x : False, □ True : PROP)%I; [by apply forall_intro|].
+ trans (∀ x : False, bi_persistently True : PROP)%I; [by apply forall_intro|].
rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
Qed.
-Lemma persistently_forall {A} (Ψ : A → PROP) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
+Lemma persistently_forall {A} (Ψ : A → PROP) :
+ bi_persistently (∀ a, Ψ a) ⊣⊢ ∀ a, bi_persistently (Ψ a).
Proof.
apply (anti_symm _); auto using persistently_forall_2.
apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
-Lemma persistently_exist {A} (Ψ : A → PROP) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
+Lemma persistently_exist {A} (Ψ : A → PROP) :
+ bi_persistently (∃ a, Ψ a) ⊣⊢ ∃ a, bi_persistently (Ψ a).
Proof.
apply (anti_symm _); auto using persistently_exist_1.
apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
-Lemma persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
+Lemma persistently_and P Q :
+ bi_persistently (P ∧ Q) ⊣⊢ bi_persistently P ∧ bi_persistently Q.
Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
-Lemma persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
+Lemma persistently_or P Q :
+ bi_persistently (P ∨ Q) ⊣⊢ bi_persistently P ∨ bi_persistently Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
-Lemma persistently_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
+Lemma persistently_impl P Q :
+ bi_persistently (P → Q) ⊢ bi_persistently P → bi_persistently Q.
Proof.
apply impl_intro_l; rewrite -persistently_and.
apply persistently_mono, impl_elim with P; auto.
Qed.
-Lemma persistently_internal_eq {A : ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A : ofeT} (a b : A) :
+ bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
Proof.
apply (anti_symm (⊢)); first by rewrite persistently_elim.
- apply (internal_eq_rewrite' a b (λ b, □ (a ≡ b))%I); auto.
+ apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto.
rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
Qed.
-Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
+Lemma persistently_sep_dup P :
+ bi_persistently P ⊣⊢ bi_persistently P ∗ bi_persistently P.
Proof.
apply (anti_symm _); last by eauto using sep_elim_l with typeclass_instances.
- rewrite -{1}(idemp bi_and (â–¡ _)%I) -{2}(left_id emp%I _ (â–¡ _)%I).
- by rewrite persistently_and_sep_assoc and_elim_l.
+ by rewrite -{1}(idemp bi_and (bi_persistently _)%I)
+ -{2}(left_id emp%I _ (bi_persistently _)%I)
+ persistently_and_sep_assoc and_elim_l.
Qed.
-Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma persistently_and_sep_l_1 P Q : bi_persistently P ∧ Q ⊢ bi_persistently P ∗ Q.
Proof.
by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
Qed.
-Lemma persistently_and_sep_r_1 P Q : P ∧ □ Q ⊢ P ∗ □ Q.
+Lemma persistently_and_sep_r_1 P Q : P ∧ bi_persistently Q ⊢ P ∗ bi_persistently Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
-Lemma persistently_True_emp : □ True ⊣⊢ □ emp.
+Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
-Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q).
+Lemma persistently_and_sep P Q : bi_persistently (P ∧ Q) ⊢ bi_persistently (P ∗ Q).
Proof.
rewrite persistently_and.
rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
Qed.
-Lemma persistently_bare P : □ ■P ⊣⊢ □ P.
+Lemma persistently_bare P : bi_persistently (bi_bare P) ⊣⊢ bi_persistently P.
Proof.
by rewrite /bi_bare persistently_and -persistently_True_emp
persistently_pure left_id.
Qed.
-Lemma and_sep_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
+Lemma and_sep_persistently P Q :
+ bi_persistently P ∧ bi_persistently Q ⊣⊢ bi_persistently P ∗ bi_persistently Q.
Proof.
apply (anti_symm _).
- auto using persistently_and_sep_l_1.
- eauto 10 using sep_elim_l, sep_elim_r with typeclass_instances.
Qed.
-Lemma persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
+Lemma persistently_sep_2 P Q :
+ bi_persistently P ∗ bi_persistently Q ⊢ bi_persistently (P ∗ Q).
Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma persistently_sep `{PositiveBI PROP} P Q :
+ bi_persistently (P ∗ Q) ⊣⊢ bi_persistently P ∗ bi_persistently Q.
Proof.
apply (anti_symm _); auto using persistently_sep_2.
by rewrite -persistently_bare bare_sep sep_and !bare_elim persistently_and
and_sep_persistently.
Qed.
-Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
+Lemma persistently_wand P Q :
+ bi_persistently (P -∗ Q) ⊢ bi_persistently P -∗ bi_persistently Q.
Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
-Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Lemma persistently_entails_l P Q :
+ (P ⊢ bi_persistently Q) → P ⊢ bi_persistently Q ∗ P.
Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
-Lemma persistently_entails_r P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Lemma persistently_entails_r P Q :
+ (P ⊢ bi_persistently Q) → P ⊢ P ∗ bi_persistently Q.
Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
-Lemma persistently_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q).
+Lemma persistently_impl_wand_2 P Q :
+ bi_persistently (P -∗ Q) ⊢ bi_persistently (P → Q).
Proof.
apply persistently_intro', impl_intro_r.
rewrite -{2}(left_id emp%I _ P%I) persistently_and_sep_assoc.
@@ -1080,25 +1093,27 @@ Qed.
Section persistently_bare_bi.
Context `{AffineBI PROP}.
- Lemma persistently_emp : □ emp ⊣⊢ emp.
+ Lemma persistently_emp : bi_persistently emp ⊣⊢ emp.
Proof. by rewrite -!True_emp persistently_pure. Qed.
- Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
+ Lemma persistently_and_sep_l P Q :
+ bi_persistently P ∧ Q ⊣⊢ bi_persistently P ∗ Q.
Proof.
apply (anti_symm (⊢));
eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
Qed.
- Lemma persistently_and_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
+ Lemma persistently_and_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ bi_persistently Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
- Lemma persistently_impl_wand P Q : □ (P → Q) ⊣⊢ □ (P -∗ Q).
+ Lemma persistently_impl_wand P Q :
+ bi_persistently (P → Q) ⊣⊢ bi_persistently (P -∗ Q).
Proof.
apply (anti_symm (⊢)); auto using persistently_impl_wand_2.
apply persistently_intro', wand_intro_l.
by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
Qed.
- Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
+ Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ bi_persistently (P ∗ R → Q).
Proof.
apply (anti_symm (⊢)).
- rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
@@ -1109,53 +1124,54 @@ Section persistently_bare_bi.
rewrite assoc -persistently_and_sep_r.
by rewrite persistently_elim impl_elim_r.
Qed.
- Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
+ Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ bi_persistently (P ∧ R -∗ Q).
Proof.
apply (anti_symm (⊢)).
- rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
apply and_mono_r. rewrite -persistently_pure.
apply persistently_intro', wand_intro_l.
by rewrite impl_elim_r persistently_pure right_id.
- - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
- by rewrite persistently_elim wand_elim_r.
+ - apply exist_elim=> R. apply impl_intro_l.
+ by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
Qed.
End persistently_bare_bi.
(* The combined bare persistently modality *)
-Lemma bare_persistently_elim P : ⬕ P ⊢ P.
+Lemma bare_persistently_elim P : □ P ⊢ P.
Proof. apply persistently_and_emp_elim. Qed.
-Lemma bare_persistently_intro' P Q : (⬕ P ⊢ Q) → ⬕ P ⊢ ⬕ Q.
+Lemma bare_persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
Proof. intros <-. by rewrite persistently_bare persistently_idemp. Qed.
-Lemma bare_persistently_emp : ⬕ emp ⊣⊢ emp.
+Lemma bare_persistently_emp : □ emp ⊣⊢ emp.
Proof. by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp. Qed.
-Lemma bare_persistently_and P Q : ⬕ (P ∧ Q) ⊣⊢ ⬕ P ∧ ⬕ Q.
+Lemma bare_persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
Proof. by rewrite persistently_and bare_and. Qed.
-Lemma bare_persistently_or P Q : ⬕ (P ∨ Q) ⊣⊢ ⬕ P ∨ ⬕ Q.
+Lemma bare_persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
Proof. by rewrite persistently_or bare_or. Qed.
-Lemma bare_persistently_exist {A} (Φ : A → PROP) : ⬕ (∃ x, Φ x) ⊣⊢ ∃ x, ⬕ Φ x.
+Lemma bare_persistently_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x.
Proof. by rewrite persistently_exist bare_exist. Qed.
-Lemma bare_persistently_sep_2 P Q : ⬕ P ∗ ⬕ Q ⊢ ⬕ (P ∗ Q).
+Lemma bare_persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
Proof. by rewrite bare_sep_2 persistently_sep_2. Qed.
-Lemma bare_persistently_sep `{PositiveBI PROP} P Q : ⬕ (P ∗ Q) ⊣⊢ ⬕ P ∗ ⬕ Q.
+Lemma bare_persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite -bare_sep -persistently_sep. Qed.
-Lemma bare_persistently_idemp P : ⬕ ⬕ P ⊣⊢ ⬕ P.
+Lemma bare_persistently_idemp P : □ □ P ⊣⊢ □ P.
Proof. by rewrite persistently_bare persistently_idemp. Qed.
-Lemma persistently_and_bare_sep_l P Q : □ P ∧ Q ⊣⊢ ⬕ P ∗ Q.
+Lemma persistently_and_bare_sep_l P Q : bi_persistently P ∧ Q ⊣⊢ □ P ∗ Q.
Proof.
apply (anti_symm _).
- - by rewrite /bi_bare -(comm bi_and (â–¡ P)%I) -persistently_and_sep_assoc left_id.
+ - by rewrite /bi_bare -(comm bi_and (bi_persistently P)%I)
+ -persistently_and_sep_assoc left_id.
- apply and_intro. by rewrite bare_elim sep_elim_l. by rewrite sep_elim_r.
Qed.
-Lemma persistently_and_bare_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ ⬕ Q.
+Lemma persistently_and_bare_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ □ Q.
Proof. by rewrite !(comm _ P) persistently_and_bare_sep_l. Qed.
-Lemma and_sep_bare_persistently P Q : ⬕ P ∧ ⬕ Q ⊣⊢ ⬕ P ∗ ⬕ Q.
+Lemma and_sep_bare_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_r. Qed.
-Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
+Lemma bare_persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
Proof. by rewrite -persistently_and_bare_sep_l bare_and_r bare_and idemp. Qed.
(* Conditional bare modality *)
@@ -1169,30 +1185,34 @@ Global Instance bare_if_flip_mono' p :
Proper (flip (⊢) ==> flip (⊢)) (@bi_bare_if PROP p).
Proof. solve_proper. Qed.
-Lemma bare_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
+Lemma bare_if_mono p P Q : (P ⊢ Q) → bi_bare_if p P ⊢ bi_bare_if p Q.
Proof. by intros ->. Qed.
-Lemma bare_if_elim p P : ■?p P ⊢ P.
+Lemma bare_if_elim p P : bi_bare_if p P ⊢ P.
Proof. destruct p; simpl; auto using bare_elim. Qed.
-Lemma bare_bare_if p P : ■P ⊢ ■?p P.
+Lemma bare_bare_if p P : bi_bare P ⊢ bi_bare_if p P.
Proof. destruct p; simpl; auto using bare_elim. Qed.
-Lemma bare_if_intro' p P Q : (■?p P ⊢ Q) → ■?p P ⊢ ■?p Q.
+Lemma bare_if_intro' p P Q :
+ (bi_bare_if p P ⊢ Q) → bi_bare_if p P ⊢ bi_bare_if p Q.
Proof. destruct p; simpl; auto using bare_intro'. Qed.
-Lemma bare_if_emp p : ■?p emp ⊣⊢ emp.
+Lemma bare_if_emp p : bi_bare_if p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using bare_emp. Qed.
-Lemma bare_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
+Lemma bare_if_and p P Q : bi_bare_if p (P ∧ Q) ⊣⊢ bi_bare_if p P ∧ bi_bare_if p Q.
Proof. destruct p; simpl; auto using bare_and. Qed.
-Lemma bare_if_or p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+Lemma bare_if_or p P Q : bi_bare_if p (P ∨ Q) ⊣⊢ bi_bare_if p P ∨ bi_bare_if p Q.
Proof. destruct p; simpl; auto using bare_or. Qed.
-Lemma bare_if_exist {A} p (Ψ : A → PROP) : (■?p ∃ a, Ψ a) ⊣⊢ ∃ a, ■?p Ψ a.
+Lemma bare_if_exist {A} p (Ψ : A → PROP) :
+ bi_bare_if p (∃ a, Ψ a) ⊣⊢ ∃ a, bi_bare_if p (Ψ a).
Proof. destruct p; simpl; auto using bare_exist. Qed.
-Lemma bare_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
+Lemma bare_if_sep_2 p P Q :
+ bi_bare_if p P ∗ bi_bare_if p Q ⊢ bi_bare_if p (P ∗ Q).
Proof. destruct p; simpl; auto using bare_sep_2. Qed.
-Lemma bare_if_sep `{PositiveBI PROP} p P Q : ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
+Lemma bare_if_sep `{PositiveBI PROP} p P Q :
+ bi_bare_if p (P ∗ Q) ⊣⊢ bi_bare_if p P ∗ bi_bare_if p Q.
Proof. destruct p; simpl; auto using bare_sep. Qed.
-Lemma bare_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
+Lemma bare_if_idemp p P : bi_bare_if p (bi_bare_if p P) ⊣⊢ bi_bare_if p P.
Proof. destruct p; simpl; auto using bare_idemp. Qed.
(* Conditional persistently *)
@@ -1208,50 +1228,59 @@ Global Instance persistently_if_flip_mono' p :
Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
-Lemma persistently_if_mono p P Q : (P ⊢ Q) → ⬕?p P ⊢ ⬕?p Q.
+Lemma persistently_if_mono p P Q :
+ (P ⊢ Q) → bi_persistently_if p P ⊢ bi_persistently_if p Q.
Proof. by intros ->. Qed.
-Lemma persistently_if_pure p φ : â–¡?p ⌜φ⌠⊣⊢ ⌜φâŒ.
+Lemma persistently_if_pure p φ : bi_persistently_if p ⌜φ⌠⊣⊢ ⌜φâŒ.
Proof. destruct p; simpl; auto using persistently_pure. Qed.
-Lemma persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Lemma persistently_if_and p P Q :
+ bi_persistently_if p (P ∧ Q) ⊣⊢ bi_persistently_if p P ∧ bi_persistently_if p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.
-Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Lemma persistently_if_or p P Q :
+ bi_persistently_if p (P ∨ Q) ⊣⊢ bi_persistently_if p P ∨ bi_persistently_if p Q.
Proof. destruct p; simpl; auto using persistently_or. Qed.
-Lemma persistently_if_exist {A} p (Ψ : A → PROP) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
+Lemma persistently_if_exist {A} p (Ψ : A → PROP) :
+ (bi_persistently_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_persistently_if p (Ψ a).
Proof. destruct p; simpl; auto using persistently_exist. Qed.
-Lemma persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
+Lemma persistently_if_sep_2 p P Q :
+ bi_persistently_if p P ∗ bi_persistently_if p Q ⊢ bi_persistently_if p (P ∗ Q).
Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
-Lemma persistently_if_sep `{PositiveBI PROP} p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Lemma persistently_if_sep `{PositiveBI PROP} p P Q :
+ bi_persistently_if p (P ∗ Q) ⊣⊢ bi_persistently_if p P ∗ bi_persistently_if p Q.
Proof. destruct p; simpl; auto using persistently_sep. Qed.
-Lemma persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
+Lemma persistently_if_idemp p P :
+ bi_persistently_if p (bi_persistently_if p P) ⊣⊢ bi_persistently_if p P.
Proof. destruct p; simpl; auto using persistently_idemp. Qed.
(* Conditional bare persistently *)
-Lemma bare_persistently_if_mono p P Q : (P ⊢ Q) → ⬕?p P ⊢ ⬕?p Q.
+Lemma bare_persistently_if_mono p P Q : (P ⊢ Q) → □?p P ⊢ □?p Q.
Proof. by intros ->. Qed.
-Lemma bare_persistently_if_elim p P : ⬕?p P ⊢ P.
+Lemma bare_persistently_if_elim p P : □?p P ⊢ P.
Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
-Lemma bare_persistently_bare_persistently_if p P : ⬕ P ⊢ ⬕?p P.
+Lemma bare_persistently_bare_persistently_if p P : □ P ⊢ □?p P.
Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
-Lemma bare_persistently_if_intro' p P Q : (⬕?p P ⊢ Q) → ⬕?p P ⊢ ⬕?p Q.
+Lemma bare_persistently_if_intro' p P Q : (□?p P ⊢ Q) → □?p P ⊢ □?p Q.
Proof. destruct p; simpl; auto using bare_persistently_intro'. Qed.
-Lemma bare_persistently_if_emp p : ⬕?p emp ⊣⊢ emp.
+Lemma bare_persistently_if_emp p : □?p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using bare_persistently_emp. Qed.
-Lemma bare_persistently_if_and p P Q : ⬕?p (P ∧ Q) ⊣⊢ ⬕?p P ∧ ⬕?p Q.
+Lemma bare_persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
Proof. destruct p; simpl; auto using bare_persistently_and. Qed.
-Lemma bare_persistently_if_or p P Q : ⬕?p (P ∨ Q) ⊣⊢ ⬕?p P ∨ ⬕?p Q.
+Lemma bare_persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
Proof. destruct p; simpl; auto using bare_persistently_or. Qed.
-Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) : (⬕?p ∃ a, Ψ a) ⊣⊢ ∃ a, ⬕?p Ψ a.
+Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) :
+ (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
Proof. destruct p; simpl; auto using bare_persistently_exist. Qed.
-Lemma bare_persistently_if_sep_2 p P Q : ⬕?p P ∗ ⬕?p Q ⊢ ⬕?p (P ∗ Q).
+Lemma bare_persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
Proof. destruct p; simpl; auto using bare_persistently_sep_2. Qed.
-Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q : ⬕?p (P ∗ Q) ⊣⊢ ⬕?p P ∗ ⬕?p Q.
+Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q :
+ □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
Proof. destruct p; simpl; auto using bare_persistently_sep. Qed.
-Lemma bare_persistently_if_idemp p P : ⬕?p ⬕?p P ⊣⊢ ⬕?p P.
+Lemma bare_persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
Proof. destruct p; simpl; auto using bare_persistently_idemp. Qed.
(* Persistence *)
@@ -1295,9 +1324,9 @@ Global Instance sep_persistent P Q :
Persistent P → Persistent Q → Persistent (P ∗ Q).
Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
-Global Instance persistently_persistent P : Persistent (â–¡ P).
+Global Instance persistently_persistent P : Persistent (bi_persistently P).
Proof. by rewrite /Persistent persistently_idemp. Qed.
-Global Instance bare_persistent P : Persistent P → Persistent (■P).
+Global Instance bare_persistent P : Persistent P → Persistent (bi_bare P).
Proof. rewrite /bi_bare. apply _. Qed.
Global Instance sink_persistent P : Persistent P → Persistent (▲ P).
Proof. rewrite /bi_sink. apply _. Qed.
@@ -1307,26 +1336,29 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
Proof. destruct mx; apply _. Qed.
(* Properties of persistent propositions *)
-Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ □ P.
+Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ bi_persistently P.
Proof. done. Qed.
-Lemma persistent_persistently P `{!Persistent P, !Absorbing P} : □ P ⊣⊢ P.
-Proof. apply (anti_symm _); auto using persistent_persistently_2, persistently_elim. Qed.
+Lemma persistent_persistently P `{!Persistent P, !Absorbing P} :
+ bi_persistently P ⊣⊢ P.
+Proof.
+ apply (anti_symm _); auto using persistent_persistently_2, persistently_elim.
+Qed.
-Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ bi_persistently Q.
Proof. intros HP. by rewrite (persistent P) HP. Qed.
-Lemma persistent_and_bare_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ ■P ∗ Q.
+Lemma persistent_and_bare_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ bi_bare P ∗ Q.
Proof.
rewrite {1}(persistent_persistently_2 P) persistently_and_bare_sep_l.
by rewrite -bare_idemp bare_persistently_elim.
Qed.
-Lemma persistent_and_bare_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ ■Q.
+Lemma persistent_and_bare_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ bi_bare Q.
Proof. by rewrite !(comm _ P) persistent_and_bare_sep_l_1. Qed.
Lemma persistent_and_bare_sep_l P Q `{!Persistent P, !Absorbing P} :
- P ∧ Q ⊣⊢ ■P ∗ Q.
+ P ∧ Q ⊣⊢ bi_bare P ∗ Q.
Proof. by rewrite -(persistent_persistently P) persistently_and_bare_sep_l. Qed.
Lemma persistent_and_bare_sep_r P Q `{!Persistent Q, !Absorbing Q} :
- P ∧ Q ⊣⊢ P ∗ ■Q.
+ P ∧ Q ⊣⊢ P ∗ bi_bare Q.
Proof. by rewrite -(persistent_persistently Q) persistently_and_bare_sep_r. Qed.
Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
@@ -1345,7 +1377,7 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
-Lemma persistent_sink_bare P `{!Persistent P} : P ⊢ ▲ ■P.
+Lemma persistent_sink_bare P `{!Persistent P} : P ⊢ ▲ bi_bare P.
Proof.
by rewrite {1}(persistent_persistently_2 P) -persistently_bare
persistently_elim_sink.
@@ -1383,11 +1415,15 @@ Global Instance bi_sep_monoid : Monoid (@bi_sep PROP) :=
Global Instance bi_persistently_and_homomorphism :
MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP).
-Proof. split; [split|]; try apply _. apply persistently_and. apply persistently_pure. Qed.
+Proof.
+ split; [split|]; try apply _. apply persistently_and. apply persistently_pure.
+Qed.
Global Instance bi_persistently_or_homomorphism :
MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
-Proof. split; [split|]; try apply _. apply persistently_or. apply persistently_pure. Qed.
+Proof.
+ split; [split|]; try apply _. apply persistently_or. apply persistently_pure.
+Qed.
Global Instance bi_persistently_sep_weak_homomorphism `{PositiveBI PROP} :
WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
@@ -1504,13 +1540,13 @@ Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
Proof. by rewrite /bi_iff later_and !later_impl. Qed.
-Lemma later_persistently P : ▷ □ P ⊣⊢ □ ▷ P.
+Lemma later_persistently P : ▷ bi_persistently P ⊣⊢ bi_persistently (▷ P).
Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
-Lemma later_bare_2 P : ■▷ P ⊢ ▷ ■P.
+Lemma later_bare_2 P : bi_bare (▷ P) ⊢ ▷ bi_bare P.
Proof. rewrite /bi_bare later_and. auto using later_intro. Qed.
-Lemma later_bare_persistently_2 P : ⬕ ▷ P ⊢ ▷ ⬕ P.
+Lemma later_bare_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
Proof. by rewrite -later_persistently later_bare_2. Qed.
-Lemma later_bare_persistently_if_2 p P : ⬕?p ▷ P ⊢ ▷ ⬕?p P.
+Lemma later_bare_persistently_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
Proof. destruct p; simpl; auto using later_bare_persistently_2. Qed.
Lemma later_sink P : ▷ ▲ P ⊣⊢ ▲ ▷ P.
Proof. by rewrite /bi_sink later_sep later_True. Qed.
@@ -1574,13 +1610,14 @@ Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
-Lemma laterN_persistently n P : ▷^n □ P ⊣⊢ □ ▷^n P.
+Lemma laterN_persistently n P :
+ ▷^n bi_persistently P ⊣⊢ bi_persistently (▷^n P).
Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
-Lemma laterN_bare_2 n P : ■▷^n P ⊢ ▷^n ■P.
+Lemma laterN_bare_2 n P : bi_bare (▷^n P) ⊢ ▷^n bi_bare P.
Proof. rewrite /bi_bare laterN_and. auto using laterN_intro. Qed.
-Lemma laterN_bare_persistently_2 n P : ⬕ ▷^n P ⊢ ▷^n ⬕ P.
+Lemma laterN_bare_persistently_2 n P : □ ▷^n P ⊢ ▷^n □ P.
Proof. by rewrite -laterN_persistently laterN_bare_2. Qed.
-Lemma laterN_bare_persistently_if_2 n p P : ⬕?p ▷^n P ⊢ ▷^n ⬕?p P.
+Lemma laterN_bare_persistently_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
Proof. destruct p; simpl; auto using laterN_bare_persistently_2. Qed.
Lemma laterN_sink n P : ▷^n ▲ P ⊣⊢ ▲ ▷^n P.
Proof. by rewrite /bi_sink laterN_sep laterN_True. Qed.
@@ -1637,13 +1674,15 @@ Proof.
Qed.
Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
-Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
-Proof. by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure. Qed.
-Lemma except_0_bare_2 P : ■◇ P ⊢ ◇ ■P.
+Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (◇ P).
+Proof.
+ by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure.
+Qed.
+Lemma except_0_bare_2 P : bi_bare (◇ P) ⊢ ◇ bi_bare P.
Proof. rewrite /bi_bare except_0_and. auto using except_0_intro. Qed.
-Lemma except_0_bare_persistently_2 P : ⬕ ◇ P ⊢ ◇ ⬕ P.
+Lemma except_0_bare_persistently_2 P : □ ◇ P ⊢ ◇ □ P.
Proof. by rewrite -except_0_persistently except_0_bare_2. Qed.
-Lemma except_0_bare_persistently_if_2 p P : ⬕?p ◇ P ⊢ ◇ ⬕?p P.
+Lemma except_0_bare_persistently_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
Proof. destruct p; simpl; auto using except_0_bare_persistently_2. Qed.
Lemma except_0_sink P : ◇ ▲ P ⊣⊢ ▲ ◇ P.
Proof. by rewrite /bi_sink except_0_sep except_0_True. Qed.
@@ -1653,7 +1692,7 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
-Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ ■P ⊢ ◇ ■▷ P.
+Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ bi_bare P ⊢ ◇ bi_bare (▷ P).
Proof.
rewrite /bi_bare later_and (timeless emp%I) except_0_and.
by apply and_mono, except_0_intro.
@@ -1713,14 +1752,14 @@ Proof.
- rewrite /bi_except_0; auto.
- apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
-Global Instance persistently_timeless P : Timeless P → Timeless (□ P).
+Global Instance persistently_timeless P : Timeless P → Timeless (bi_persistently P).
Proof.
intros. rewrite /Timeless /bi_except_0 later_persistently_1.
by rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
Qed.
Global Instance bare_timeless P :
- Timeless (emp%I : PROP) → Timeless P → Timeless (■P).
+ Timeless (emp%I : PROP) → Timeless P → Timeless (bi_bare P).
Proof. rewrite /bi_bare; apply _. Qed.
Global Instance sink_timeless P : Timeless P → Timeless (▲ P).
Proof. rewrite /bi_sink; apply _. Qed.
diff --git a/theories/bi/fixpoint.v b/theories/bi/fixpoint.v
index 9a7d141ac..075440a9f 100644
--- a/theories/bi/fixpoint.v
+++ b/theories/bi/fixpoint.v
@@ -6,7 +6,7 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
Class BIMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
- bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
+ bi_mono_pred Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
Arguments bi_mono_pred {_ _ _ _} _ _.
@@ -14,11 +14,11 @@ Local Existing Instance bi_mono_pred_ne.
Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
- (∀ Φ : A -n> PROP, □ (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
+ (∀ Φ : A -n> PROP, bi_persistently (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
- (∃ Φ : A -n> PROP, □ (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
+ (∃ Φ : A -n> PROP, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
Section least.
Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}.
@@ -48,13 +48,13 @@ Section least.
Qed.
Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
- ⬕ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
+ □ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
Proof.
iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
Qed.
Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
- ⬕ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
+ □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
∀ x, bi_least_fixpoint F x -∗ Φ x.
Proof.
trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
@@ -96,6 +96,6 @@ Section greatest.
Qed.
Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
- ⬕ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
+ □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed.
End greatest.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 7cafc1e65..ced63e3f6 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -5,7 +5,6 @@ Reserved Notation "'emp'".
Reserved Notation "'⌜' φ 'âŒ'" (at level 1, φ at level 200, format "⌜ φ âŒ").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "â–¡ P" (at level 20, right associativity).
Reserved Notation "â–· P" (at level 20, right associativity).
Section bi_mixin.
@@ -39,7 +38,6 @@ Section bi_mixin.
Local Notation "x ≡ y" := (bi_internal_eq _ x y).
Local Infix "∗" := bi_sep.
Local Infix "-∗" := bi_wand.
- Local Notation "â–¡ P" := (bi_persistently P).
Local Notation "â–· P" := (bi_later P).
Record BIMixin := {
@@ -100,17 +98,21 @@ Section bi_mixin.
bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
(* Persistently *)
- bi_mixin_persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q;
- bi_mixin_persistently_idemp_2 P : □ P ⊢ □ □ P;
+ bi_mixin_persistently_mono P Q :
+ (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
+ bi_mixin_persistently_idemp_2 P :
+ bi_persistently P ⊢ bi_persistently (bi_persistently P);
bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
- (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a;
+ (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
- □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a;
+ bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
- bi_mixin_persistently_emp_intro P : P ⊢ □ emp;
- bi_mixin_persistently_absorbing P Q : □ P ∗ Q ⊢ □ P;
- bi_mixin_persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q;
+ bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
+ bi_mixin_persistently_absorbing P Q :
+ bi_persistently P ∗ Q ⊢ bi_persistently P;
+ bi_mixin_persistently_and_sep_elim P Q :
+ bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
}.
Record SBIMixin := {
@@ -127,8 +129,10 @@ Section bi_mixin.
(▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
- sbi_mixin_later_persistently_1 P : ▷ □ P ⊢ □ ▷ P;
- sbi_mixin_later_persistently_2 P : □ ▷ P ⊢ ▷ □ P;
+ sbi_mixin_later_persistently_1 P :
+ ▷ bi_persistently P ⊢ bi_persistently (▷ P);
+ sbi_mixin_later_persistently_2 P :
+ bi_persistently (▷ P) ⊢ ▷ bi_persistently P;
sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
}.
@@ -281,7 +285,6 @@ Notation "∀ x .. y , P" :=
(bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
Notation "∃ x .. y , P" :=
(bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
-Notation "â–¡ P" := (bi_persistently P) : bi_scope.
Infix "≡" := bi_internal_eq : bi_scope.
Notation "â–· P" := (bi_later P) : bi_scope.
@@ -399,21 +402,24 @@ Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
(* Persistently *)
-Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
-Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
+Lemma persistently_idemp_2 P :
+ bi_persistently P ⊢ bi_persistently (bi_persistently P).
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
-Lemma persistently_forall_2 {A} (Ψ : A → PROP) : (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a.
+Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
+ (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
-Lemma persistently_exist_1 {A} (Ψ : A → PROP) : □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a.
+Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
+ bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
-Lemma persistently_emp_intro P : P ⊢ □ emp.
+Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
-Lemma persistently_absorbing P Q : □ P ∗ Q ⊢ □ P.
+Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q.
+Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q.
Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed.
End bi_laws.
@@ -444,9 +450,9 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
-Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
+Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
-Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index f465765b4..7ff1a8c99 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -37,7 +37,7 @@ Global Instance ht_proper E :
Proof. solve_proper. Qed.
Lemma ht_mono E P P' Φ Φ' e :
(P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
-Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
+Proof. intros. by apply bare_mono, persistently_mono, wand_mono, wp_mono. Qed.
Global Instance ht_mono' E :
Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
Proof. solve_proper. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 4449a272b..96a456cb6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -12,19 +12,19 @@ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
@IntoInternalEq PROP A (x ≡ y) x y.
Proof. by rewrite /IntoInternalEq. Qed.
Global Instance into_internal_eq_bare {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (■P) x y.
+ IntoInternalEq P x y → IntoInternalEq (bi_bare P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite bare_elim. Qed.
Global Instance into_internal_eq_sink {A : ofeT} (x y : A) P :
IntoInternalEq P x y → IntoInternalEq (▲ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite sink_internal_eq. Qed.
Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+ IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
(* FromBare *)
Global Instance from_bare_affine P : Affine P → FromBare P P.
Proof. intros. by rewrite /FromBare bare_elim. Qed.
-Global Instance from_bare_default P : FromBare (â– P) P | 100.
+Global Instance from_bare_default P : FromBare (bi_bare P) P | 100.
Proof. by rewrite /FromBare. Qed.
(* IntoSink *)
@@ -40,29 +40,29 @@ Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
Global Instance from_assumption_persistently_r P Q :
- FromAssumption true P Q → FromAssumption true P (□ Q).
+ FromAssumption true P Q → FromAssumption true P (bi_persistently Q).
Proof.
rewrite /FromAssumption /= =><-.
by rewrite -{1}bare_persistently_idemp bare_elim.
Qed.
Global Instance from_assumption_bare_r P Q :
- FromAssumption true P Q → FromAssumption true P (■Q).
+ FromAssumption true P Q → FromAssumption true P (bi_bare Q).
Proof. rewrite /FromAssumption /= =><-. by rewrite bare_idemp. Qed.
Global Instance from_assumption_sink_r p P Q :
FromAssumption p P Q → FromAssumption p P (▲ Q).
Proof. rewrite /FromAssumption /= =><-. apply sink_intro. Qed.
Global Instance from_assumption_bare_persistently_l p P Q :
- FromAssumption true P Q → FromAssumption p (⬕ P) Q.
+ FromAssumption true P Q → FromAssumption p (□ P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite bare_persistently_if_elim. Qed.
Global Instance from_assumption_persistently_l_true P Q :
- FromAssumption true P Q → FromAssumption true (□ P) Q.
+ FromAssumption true P Q → FromAssumption true (bi_persistently P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
- FromAssumption true P Q → FromAssumption false (□ P) Q.
+ FromAssumption true P Q → FromAssumption false (bi_persistently P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite affine_bare. Qed.
Global Instance from_assumption_bare_l_true p P Q :
- FromAssumption p P Q → FromAssumption p (■P) Q.
+ FromAssumption p P Q → FromAssumption p (bi_bare P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite bare_elim. Qed.
Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
@@ -101,11 +101,11 @@ Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qed.
-Global Instance into_pure_bare P φ : IntoPure P φ → IntoPure (■P) φ.
+Global Instance into_pure_bare P φ : IntoPure P φ → IntoPure (bi_bare P) φ.
Proof. rewrite /IntoPure=> ->. apply bare_elim. Qed.
Global Instance into_pure_sink P φ : IntoPure P φ → IntoPure (▲ P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite sink_pure. Qed.
-Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (□ P) φ.
+Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (bi_persistently P) φ.
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
(* FromPure *)
@@ -142,20 +142,24 @@ Proof.
by rewrite pure_wand_forall pure_impl pure_impl_forall.
Qed.
-Global Instance from_pure_persistently P φ : FromPure P φ → FromPure (□ P) φ.
+Global Instance from_pure_persistently P φ :
+ FromPure P φ → FromPure (bi_persistently P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
+Global Instance from_pure_bare P φ `{!Affine P} :
+ FromPure P φ → FromPure (bi_bare P) φ.
+Proof. by rewrite /FromPure affine_bare. Qed.
Global Instance from_pure_sink P φ : FromPure P φ → FromPure (▲ P) φ.
Proof. rewrite /FromPure=> <-. by rewrite sink_pure. Qed.
(* IntoPersistent *)
Global Instance into_persistent_persistently p P Q :
- IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
+ IntoPersistent true P Q → IntoPersistent p (bi_persistently P) Q | 0.
Proof.
rewrite /IntoPersistent /= => ->.
destruct p; simpl; auto using persistently_idemp_1.
Qed.
Global Instance into_persistent_bare p P Q :
- IntoPersistent p P Q → IntoPersistent p (■P) Q | 0.
+ IntoPersistent p P Q → IntoPersistent p (bi_bare P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite bare_elim. Qed.
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.
@@ -167,12 +171,12 @@ Proof. intros. by rewrite /IntoPersistent. Qed.
Global Instance from_persistent_here P : FromPersistent false false P P | 1.
Proof. by rewrite /FromPersistent. Qed.
Global Instance from_persistent_persistently a P Q :
- FromPersistent a false P Q → FromPersistent false true (□ P) Q | 0.
+ FromPersistent a false P Q → FromPersistent false true (bi_persistently P) Q | 0.
Proof.
rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_bare.
Qed.
Global Instance from_persistent_bare a p P Q :
- FromPersistent a p P Q → FromPersistent true p (■P) Q | 0.
+ FromPersistent a p P Q → FromPersistent true p (bi_bare P) Q | 0.
Proof. rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?bare_idemp. Qed.
(* IntoWand *)
@@ -227,14 +231,14 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
Global Instance into_wand_persistently_true q R P Q :
- IntoWand true q R P Q → IntoWand true q (□ R) P Q.
+ IntoWand true q R P Q → IntoWand true q (bi_persistently R) P Q.
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
- IntoWand false q R P Q → IntoWand false q (□ R) P Q.
+ IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
Proof. by rewrite /IntoWand persistently_elim. Qed.
Global Instance into_wand_bare_persistently p q R P Q :
- IntoWand p q R P Q → IntoWand p q (⬕ R) P Q.
+ IntoWand p q R P Q → IntoWand p q (□ R) P Q.
Proof. by rewrite /IntoWand bare_persistently_elim. Qed.
(* FromAnd *)
@@ -260,10 +264,12 @@ Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌠⌜φ⌠⌜
Proof. by rewrite /FromAnd pure_and. Qed.
Global Instance from_and_persistently P Q1 Q2 :
- FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
+ FromAnd P Q1 Q2 →
+ FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
- FromSep P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2) | 11.
+ FromSep P Q1 Q2 →
+ FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
@@ -288,13 +294,14 @@ Global Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ ∧ ψ⌠⌜φ⌠⌜
Proof. by rewrite /FromSep pure_and sep_and. Qed.
Global Instance from_sep_bare P Q1 Q2 :
- FromSep P Q1 Q2 → FromSep (■P) (■Q1) (■Q2).
+ FromSep P Q1 Q2 → FromSep (bi_bare P) (bi_bare Q1) (bi_bare Q2).
Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
Global Instance from_sep_sink P Q1 Q2 :
FromSep P Q1 Q2 → FromSep (▲ P) (▲ Q1) (▲ Q2).
Proof. rewrite /FromSep=> <-. by rewrite sink_sep. Qed.
Global Instance from_sep_persistently P Q1 Q2 :
- FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
+ FromSep P Q1 Q2 →
+ FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
@@ -322,20 +329,23 @@ Proof.
Qed.
Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
-Proof. by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and. Qed.
+Proof.
+ by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
+Qed.
Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.
Global Instance into_and_bare p P Q1 Q2 :
- IntoAnd p P Q1 Q2 → IntoAnd p (■P) (■Q1) (■Q2).
+ IntoAnd p P Q1 Q2 → IntoAnd p (bi_bare P) (bi_bare Q1) (bi_bare Q2).
Proof.
rewrite /IntoAnd. destruct p; simpl.
- by rewrite -bare_and !persistently_bare.
- intros ->. by rewrite bare_and.
Qed.
Global Instance into_and_persistently p P Q1 Q2 :
- IntoAnd p P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
+ IntoAnd p P Q1 Q2 →
+ IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof.
rewrite /IntoAnd /=. destruct p; simpl.
- by rewrite -persistently_and !persistently_idemp.
@@ -348,7 +358,7 @@ Proof. by rewrite /IntoSep. Qed.
Inductive AndIntoSep : PROP → PROP → PROP → PROP → Prop :=
| and_into_sep_affine P Q Q' : Affine P → FromBare Q' Q → AndIntoSep P P Q Q'
- | and_into_sep P Q : AndIntoSep P (â– P)%I Q Q.
+ | and_into_sep P Q : AndIntoSep P (bi_bare P)%I Q Q.
Existing Class AndIntoSep.
Global Existing Instance and_into_sep_affine | 0.
Global Existing Instance and_into_sep | 2.
@@ -374,14 +384,15 @@ Qed.
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
-(* FIXME: This instance is kind of strange, it just gets rid of the â– . Also, it
+(* FIXME: This instance is kind of strange, it just gets rid of the bi_bare. Also, it
overlaps with `into_sep_bare_later`, and hence has lower precedence. *)
Global Instance into_sep_bare P Q1 Q2 :
- IntoSep P Q1 Q2 → IntoSep (■P) Q1 Q2 | 20.
+ IntoSep P Q1 Q2 → IntoSep (bi_bare P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite bare_elim. Qed.
Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
- IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2).
+ IntoSep P Q1 Q2 →
+ IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
@@ -404,13 +415,14 @@ Proof. by rewrite /FromOr. Qed.
Global Instance from_or_pure φ ψ : @FromOr PROP ⌜φ ∨ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /FromOr pure_or. Qed.
Global Instance from_or_bare P Q1 Q2 :
- FromOr P Q1 Q2 → FromOr (■P) (■Q1) (■Q2).
+ FromOr P Q1 Q2 → FromOr (bi_bare P) (bi_bare Q1) (bi_bare Q2).
Proof. rewrite /FromOr=> <-. by rewrite bare_or. Qed.
Global Instance from_or_sink P Q1 Q2 :
FromOr P Q1 Q2 → FromOr (▲ P) (▲ Q1) (▲ Q2).
Proof. rewrite /FromOr=> <-. by rewrite sink_or. Qed.
Global Instance from_or_persistently P Q1 Q2 :
- FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
+ FromOr P Q1 Q2 →
+ FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
(* IntoOr *)
@@ -419,13 +431,14 @@ Proof. by rewrite /IntoOr. Qed.
Global Instance into_or_pure φ ψ : @IntoOr PROP ⌜φ ∨ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /IntoOr pure_or. Qed.
Global Instance into_or_bare P Q1 Q2 :
- IntoOr P Q1 Q2 → IntoOr (■P) (■Q1) (■Q2).
+ IntoOr P Q1 Q2 → IntoOr (bi_bare P) (bi_bare Q1) (bi_bare Q2).
Proof. rewrite /IntoOr=>->. by rewrite bare_or. Qed.
Global Instance into_or_sink P Q1 Q2 :
IntoOr P Q1 Q2 → IntoOr (▲ P) (▲ Q1) (▲ Q2).
Proof. rewrite /IntoOr=>->. by rewrite sink_or. Qed.
Global Instance into_or_persistently P Q1 Q2 :
- IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
+ IntoOr P Q1 Q2 →
+ IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
(* FromExist *)
@@ -435,13 +448,13 @@ Global Instance from_exist_pure {A} (φ : A → Prop) :
@FromExist PROP A ⌜∃ x, φ x⌠(λ a, ⌜φ aâŒ)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
Global Instance from_exist_bare {A} P (Φ : A → PROP) :
- FromExist P Φ → FromExist (■P) (λ a, ■(Φ a))%I.
+ FromExist P Φ → FromExist (bi_bare P) (λ a, bi_bare (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite bare_exist. Qed.
Global Instance from_exist_sink {A} P (Φ : A → PROP) :
FromExist P Φ → FromExist (▲ P) (λ a, ▲ (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite sink_exist. Qed.
Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
- FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
+ FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
(* IntoExist *)
@@ -451,7 +464,7 @@ Global Instance into_exist_pure {A} (φ : A → Prop) :
@IntoExist PROP A ⌜∃ x, φ x⌠(λ a, ⌜φ aâŒ)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
Global Instance into_exist_bare {A} P (Φ : A → PROP) :
- IntoExist P Φ → IntoExist (■P) (λ a, ■(Φ a))%I.
+ IntoExist P Φ → IntoExist (bi_bare P) (λ a, bi_bare (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP bare_exist. Qed.
Global Instance into_exist_and_pure P Q φ :
IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
@@ -470,17 +483,17 @@ Global Instance into_exist_sink {A} P (Φ : A → PROP) :
IntoExist P Φ → IntoExist (▲ P) (λ a, ▲ (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP sink_exist. Qed.
Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
- IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
+ IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
Global Instance into_forall_bare {A} P (Φ : A → PROP) :
- IntoForall P Φ → IntoForall (■P) (λ a, ■(Φ a))%I.
+ IntoForall P Φ → IntoForall (bi_bare P) (λ a, bi_bare (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP bare_forall. Qed.
Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
- IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
+ IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
(* FromForall *)
@@ -505,8 +518,11 @@ Proof.
- by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.
+Global Instance from_forall_bare `{AffineBI PROP} {A} P (Φ : A → PROP) :
+ FromForall P Φ → FromForall (bi_bare P)%I (λ a, bi_bare (Φ a))%I.
+Proof. rewrite /FromForall=> <-. rewrite affine_bare. by setoid_rewrite bare_elim. Qed.
Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
- FromForall P Φ → FromForall (□ P)%I (λ a, □ (Φ a))%I.
+ FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
(* ElimModal *)
@@ -531,9 +547,10 @@ Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
Global Instance frame_here p R : Frame p R R emp | 1.
Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
-Global Instance frame_bare_here_absorbing p R : Absorbing R → Frame p (■R) R True | 0.
+Global Instance frame_bare_here_absorbing p R :
+ Absorbing R → Frame p (bi_bare R) R True | 0.
Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.
-Global Instance frame_bare_here p R : Frame p (â– R) R emp | 1.
+Global Instance frame_bare_here p R : Frame p (bi_bare R) R emp | 1.
Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.
Global Instance frame_here_pure p φ Q : FromPure Q φ → Frame p ⌜φ⌠Q True.
@@ -592,11 +609,11 @@ Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
Global Instance make_and_emp_l P : Affine P → MakeAnd emp P P.
Proof. intros. by rewrite /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_l_bare P : MakeAnd emp P (â– P) | 10.
+Global Instance make_and_emp_l_bare P : MakeAnd emp P (bi_bare P) | 10.
Proof. intros. by rewrite /MakeAnd. Qed.
Global Instance make_and_emp_r P : Affine P → MakeAnd P emp P.
Proof. intros. by rewrite /MakeAnd and_emp. Qed.
-Global Instance make_and_emp_r_bare P : MakeAnd P emp (â– P) | 10.
+Global Instance make_and_emp_r_bare P : MakeAnd P emp (bi_bare P) | 10.
Proof. intros. by rewrite /MakeAnd comm. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
@@ -661,17 +678,17 @@ Proof.
by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.
-Class MakeBare (P Q : PROP) := make_bare : ■P ⊣⊢ Q.
+Class MakeBare (P Q : PROP) := make_bare : bi_bare P ⊣⊢ Q.
Arguments MakeBare _%I _%I.
Global Instance make_bare_True : MakeBare True emp | 0.
Proof. by rewrite /MakeBare bare_True_emp bare_emp. Qed.
Global Instance make_bare_affine P : Affine P → MakeBare P P | 1.
Proof. intros. by rewrite /MakeBare affine_bare. Qed.
-Global Instance make_bare_default P : MakeBare P (â– P) | 100.
+Global Instance make_bare_default P : MakeBare P (bi_bare P) | 100.
Proof. by rewrite /MakeBare. Qed.
Global Instance frame_bare R P Q Q' :
- Frame true R P Q → MakeBare Q Q' → Frame true R (■P) Q'.
+ Frame true R P Q → MakeBare Q Q' → Frame true R (bi_bare P) Q'.
Proof.
rewrite /Frame /MakeBare=> <- <- /=.
by rewrite -{1}bare_idemp bare_sep_2.
@@ -691,17 +708,17 @@ Global Instance frame_sink p R P Q Q' :
Frame p R P Q → MakeSink Q Q' → Frame p R (▲ P) Q'.
Proof. rewrite /Frame /MakeSink=> <- <- /=. by rewrite sink_sep_r. Qed.
-Class MakePersistently (P Q : PROP) := make_persistently : □ P ⊣⊢ Q.
+Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P ⊣⊢ Q.
Arguments MakePersistently _%I _%I.
Global Instance make_persistently_true : MakePersistently True True.
Proof. by rewrite /MakePersistently persistently_pure. Qed.
Global Instance make_persistently_emp : MakePersistently emp True.
Proof. by rewrite /MakePersistently -persistently_True_emp persistently_pure. Qed.
-Global Instance make_persistently_default P : MakePersistently P (â–¡ P) | 100.
+Global Instance make_persistently_default P : MakePersistently P (bi_persistently P) | 100.
Proof. by rewrite /MakePersistently. Qed.
Global Instance frame_persistently R P Q Q' :
- Frame true R P Q → MakePersistently Q Q' → Frame true R (□ P) Q'.
+ Frame true R P Q → MakePersistently Q Q' → Frame true R (bi_persistently P) Q'.
Proof.
rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
@@ -755,7 +772,7 @@ Global Instance into_wand_later_args p q R P Q :
IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
Proof.
rewrite /IntoWand' /IntoWand /= => HR.
- by rewrite !later_bare_persistently_if_2 (later_intro (⬕?p R)%I) -later_wand HR.
+ by rewrite !later_bare_persistently_if_2 (later_intro (â–¡?p R)%I) -later_wand HR.
Qed.
Global Instance into_wand_laterN n p q R P Q :
@@ -768,7 +785,7 @@ Global Instance into_wand_laterN_args n p q R P Q :
IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
Proof.
rewrite /IntoWand' /IntoWand /= => HR.
- by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (⬕?p R)%I) -laterN_wand HR.
+ by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
Qed.
(* FromAnd *)
@@ -826,12 +843,13 @@ Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
(* FIXME: This instance is overly specific, generalize it. *)
Global Instance into_sep_bare_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
- Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 → IntoSep (■▷ P) (■▷ Q1) (■▷ Q2).
+ Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 →
+ IntoSep (bi_bare (â–· P)) (bi_bare (â–· Q1)) (bi_bare (â–· Q2)).
Proof.
rewrite /IntoSep /= => ?? ->.
rewrite -{1}(affine_bare Q1) -{1}(affine_bare Q2) later_sep !later_bare_1.
rewrite -except_0_sep /bi_except_0 bare_or. apply or_elim, bare_elim.
- rewrite -(idemp bi_and (â– â–· False)%I) persistent_and_sep_1.
+ rewrite -(idemp bi_and (bi_bare (â–· False))%I) persistent_and_sep_1.
by rewrite -(False_elim Q1) -(False_elim Q2).
Qed.
@@ -913,11 +931,13 @@ Proof. by rewrite /IntoExcept0. Qed.
Global Instance into_timeless_later_if p P : Timeless P → IntoExcept0 (▷?p P) P.
Proof. rewrite /IntoExcept0. destruct p; auto using except_0_intro. Qed.
-Global Instance into_timeless_bare P Q : IntoExcept0 P Q → IntoExcept0 (■P) (■Q).
+Global Instance into_timeless_bare P Q :
+ IntoExcept0 P Q → IntoExcept0 (bi_bare P) (bi_bare Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_bare_2. Qed.
Global Instance into_timeless_sink P Q : IntoExcept0 P Q → IntoExcept0 (▲ P) (▲ Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_sink. Qed.
-Global Instance into_timeless_persistently P Q : IntoExcept0 P Q → IntoExcept0 (□ P) (□ Q).
+Global Instance into_timeless_persistently P Q :
+ IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
(* ElimModal *)
@@ -971,7 +991,7 @@ Global Instance frame_except_0 p R P Q Q' :
Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
Proof.
rewrite /Frame /MakeExcept0=><- <-.
- by rewrite except_0_sep -(except_0_intro (⬕?p R)%I).
+ by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
Qed.
(* IntoLater *)
@@ -1014,13 +1034,13 @@ Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
Global Instance into_later_bare n P Q :
- IntoLaterN n P Q → IntoLaterN n (■P) (■Q).
+ IntoLaterN n P Q → IntoLaterN n (bi_bare P) (bi_bare Q).
Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_bare_2. Qed.
Global Instance into_later_sink n P Q :
IntoLaterN n P Q → IntoLaterN n (▲ P) (▲ Q).
Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_sink. Qed.
Global Instance into_later_persistently n P Q :
- IntoLaterN n P Q → IntoLaterN n (□ P) (□ Q).
+ IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
@@ -1093,8 +1113,11 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
+Global Instance from_later_bare n P Q `{AffineBI PROP} :
+ FromLaterN n P Q → FromLaterN n (bi_bare P) (bi_bare Q).
+Proof. rewrite /FromLaterN=><-. by rewrite bare_elim affine_bare. Qed.
Global Instance from_later_persistently n P Q :
- FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
+ FromLaterN n P Q → FromLaterN n (bi_persistently P) (bi_persistently Q).
Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
Global Instance from_later_sink n P Q :
FromLaterN n P Q → FromLaterN n (▲ P) (▲ Q).
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index ca815691f..4090d497a 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -3,7 +3,7 @@ Set Default Proof Using "Type".
Import bi.
Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
- from_assumption : ⬕?p P ⊢ Q.
+ from_assumption : □?p P ⊢ Q.
Arguments FromAssumption {_} _ _%I _%I : simpl never.
Arguments from_assumption {_} _ _%I _%I {_}.
(* No need to restrict Hint Mode, we have a default instance that will always
@@ -50,19 +50,19 @@ Arguments from_pure {_} _%I _%type_scope {_}.
Hint Mode FromPure + ! - : typeclass_instances.
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
- into_persistent : □?p P ⊢ □ Q.
+ into_persistent : bi_persistently_if p P ⊢ bi_persistently Q.
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
- from_persistent : ■?a □?p Q ⊢ P.
+ from_persistent : bi_bare_if a (bi_persistently_if p Q) ⊢ P.
Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
Arguments from_persistent {_} _ _ _%I _%I {_}.
Hint Mode FromPersistent + - - ! - : typeclass_instances.
Class FromBare {PROP : bi} (P Q : PROP) :=
- from_bare : ■Q ⊢ P.
+ from_bare : bi_bare Q ⊢ P.
Arguments FromBare {_} _%I _%type_scope : simpl never.
Arguments from_bare {_} _%I _%type_scope {_}.
Hint Mode FromBare + ! - : typeclass_instances.
@@ -91,7 +91,7 @@ Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
- Instantiate the premise of the wand or implication.
*)
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
- into_wand : ⬕?p R ⊢ ⬕?q P -∗ Q.
+ into_wand : □?p R ⊢ □?q P -∗ Q.
Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
Arguments into_wand {_} _ _ _%I _%I _%I {_}.
Hint Mode IntoWand + + + ! - - : typeclass_instances.
@@ -122,7 +122,7 @@ Hint Mode FromAnd + ! - - : typeclass_instances.
Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
- into_and : ⬕?p P ⊢ ⬕?p (Q1 ∧ Q2).
+ into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
Hint Mode IntoAnd + + ! - - : typeclass_instances.
@@ -196,13 +196,13 @@ Proof. done. Qed.
Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.
-Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ⬕?p R ∗ Q ⊢ P.
+Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.
Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
- maybe_frame : ⬕?p R ∗ Q ⊢ P.
+ maybe_frame : □?p R ∗ Q ⊢ P.
Arguments MaybeFrame {_} _ _%I _%I _%I.
Arguments maybe_frame {_} _%I _%I _%I {_}.
Hint Mode MaybeFrame + + ! ! - : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 2c65ec850..0dbfee396 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -22,7 +22,7 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
}.
Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
- (⌜envs_wf Δ⌠∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+ (⌜envs_wf Δ⌠∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
Instance: Params (@of_envs) 1.
Arguments of_envs : simpl never.
@@ -126,7 +126,7 @@ Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
Lemma of_envs_eq Δ :
- of_envs Δ = (⌜envs_wf Δ⌠∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+ of_envs Δ = (⌜envs_wf Δ⌠∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
Proof. done. Qed.
Lemma envs_lookup_delete_Some Δ Δ' i p P :
@@ -139,7 +139,7 @@ Proof.
Qed.
Lemma envs_lookup_sound Δ i p P :
- envs_lookup i Δ = Some (p,P) → Δ ⊢ ⬕?p P ∗ envs_delete i p Δ.
+ envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ envs_delete i p Δ.
Proof.
rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -153,7 +153,7 @@ Proof.
rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
Qed.
Lemma envs_lookup_persistent_sound Δ i P :
- envs_lookup i Δ = Some (true,P) → Δ ⊢ ⬕ P ∗ Δ.
+ envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
Proof.
intros. rewrite -persistently_and_bare_sep_l. apply and_intro; last done.
rewrite envs_lookup_sound //; simpl.
@@ -161,25 +161,25 @@ Proof.
Qed.
Lemma envs_lookup_split Δ i p P :
- envs_lookup i Δ = Some (p,P) → Δ ⊢ ⬕?p P ∗ (⬕?p P -∗ Δ).
+ envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ (□?p P -∗ Δ).
Proof.
rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- rewrite pure_True // left_id.
rewrite (env_lookup_perm Γp) //= bare_persistently_and and_sep_bare_persistently.
- cancel [⬕ P]%I. apply wand_intro_l. solve_sep_entails.
+ cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.
Lemma envs_lookup_delete_sound Δ Δ' i p P :
- envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ ⬕?p P ∗ Δ'.
+ envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ∗ Δ'.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') →
- Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
+ Δ ⊢ □?p [∗] Ps ∗ Δ'.
Proof.
revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
{ by rewrite bare_persistently_emp left_id. }
@@ -209,7 +209,7 @@ Proof.
Qed.
Lemma envs_snoc_sound Δ p i P :
- envs_lookup i Δ = None → Δ ⊢ ⬕?p P -∗ envs_snoc Δ p i P.
+ envs_lookup i Δ = None → Δ ⊢ □?p P -∗ envs_snoc Δ p i P.
Proof.
rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
@@ -225,7 +225,7 @@ Proof.
Qed.
Lemma envs_app_sound Δ Δ' p Γ :
- envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+ envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
Proof.
rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -248,12 +248,12 @@ Proof.
Qed.
Lemma envs_app_singleton_sound Δ Δ' p j Q :
- envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ ⬕?p Q -∗ Δ'.
+ envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ □?p Q -∗ Δ'.
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
envs_simple_replace i p Γ Δ = Some Δ' →
- envs_delete i p Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+ envs_delete i p Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
Proof.
rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -277,25 +277,25 @@ Qed.
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
- envs_delete i p Δ ⊢ ⬕?p Q -∗ Δ'.
+ envs_delete i p Δ ⊢ □?p Q -∗ Δ'.
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
- Δ ⊢ ⬕?p P ∗ ((if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
+ Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
envs_lookup i Δ = Some (p,P) →
envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
- Δ ⊢ ⬕?p P ∗ (⬕?p Q -∗ Δ').
+ Δ ⊢ □?p P ∗ (□?p Q -∗ Δ').
Proof.
intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.
Lemma envs_replace_sound' Δ Δ' i p q Γ :
envs_replace i p q Γ Δ = Some Δ' →
- envs_delete i p Δ ⊢ (if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+ envs_delete i p Δ ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ Δ'.
Proof.
rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
- apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -304,18 +304,18 @@ Qed.
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
- envs_delete i p Δ ⊢ ⬕?q Q -∗ Δ'.
+ envs_delete i p Δ ⊢ □?q Q -∗ Δ'.
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
Lemma envs_replace_sound Δ Δ' i p q P Γ :
envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
- Δ ⊢ ⬕?p P ∗ ((if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
+ Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
envs_lookup i Δ = Some (p,P) →
envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
- Δ ⊢ ⬕?p P ∗ (⬕?q Q -∗ Δ').
+ Δ ⊢ □?p P ∗ (□?q Q -∗ Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
Lemma envs_lookup_envs_clear_spatial Δ j :
@@ -336,7 +336,7 @@ Proof.
Qed.
Lemma env_spatial_is_nil_bare_persistently Δ :
- env_spatial_is_nil Δ = true → Δ ⊢ ⬕ Δ.
+ env_spatial_is_nil Δ = true → Δ ⊢ □ Δ.
Proof.
intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
rewrite !right_id {1}bare_and_r persistently_and.
@@ -387,7 +387,8 @@ Proof.
rewrite {2}envs_clear_spatial_sound.
rewrite (env_spatial_is_nil_bare_persistently (envs_clear_spatial _)) //.
rewrite -persistently_and_bare_sep_l.
- rewrite (and_elim_l (â–¡ _)%I) persistently_and_bare_sep_r bare_persistently_elim.
+ rewrite (and_elim_l (bi_persistently _)%I)
+ persistently_and_bare_sep_r bare_persistently_elim.
destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
apply envs_split_go_sound in HΔ as ->; last first.
{ intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
@@ -546,15 +547,16 @@ Proof.
destruct p; simpl.
- by rewrite -(into_persistent _ P) /= wand_elim_r.
- destruct HPQ.
- + rewrite -(affine_bare P) (_ : P = â–¡?false P)%I // (into_persistent _ P).
- by rewrite wand_elim_r.
- + rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
- by rewrite {1}(persistent_sink_bare (â–¡ _)%I) sink_sep_l wand_elim_r HQ.
+ + rewrite -(affine_bare P) (_ : P = bi_persistently_if false P)%I //
+ (into_persistent _ P) wand_elim_r //.
+ + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
+ by rewrite {1}(persistent_sink_bare (bi_persistently _)%I)
+ sink_sep_l wand_elim_r HQ.
Qed.
(** * Implication and wand *)
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
- envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ ⬕?p Q ⊢ Δ'.
+ envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ □?p Q ⊢ Δ'.
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
Lemma tac_impl_intro Δ Δ' i P P' Q :
@@ -577,7 +579,7 @@ Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
(Δ' ⊢ Q) → Δ ⊢ P → Q.
Proof.
intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
- rewrite (_ : P = â–¡?false P)%I // (into_persistent false P).
+ rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
by rewrite persistently_and_bare_sep_l wand_elim_r.
Qed.
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
@@ -604,10 +606,11 @@ Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
Proof.
intros ? HPQ ? HQ. rewrite envs_app_singleton_sound //; simpl.
apply wand_intro_l. destruct HPQ.
- - rewrite -(affine_bare P) (_ : P = â–¡?false P)%I // (into_persistent _ P).
- by rewrite wand_elim_r.
+ - rewrite -(affine_bare P) (_ : P = bi_persistently_if false P)%I //
+ (into_persistent _ P) wand_elim_r //.
- rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
- by rewrite {1}(persistent_sink_bare (â–¡ _)%I) sink_sep_l wand_elim_r HQ.
+ by rewrite {1}(persistent_sink_bare (bi_persistently _)%I) sink_sep_l
+ wand_elim_r HQ.
Qed.
Lemma tac_wand_intro_pure Δ P φ Q :
IntoPure P φ →
@@ -727,15 +730,15 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
Proof.
intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
rewrite envs_replace_singleton_sound //; destruct q; simpl.
- - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R) sink_persistently.
- by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
- - rewrite (absorbing_sink R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
- by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
+ - by rewrite (_ : R = bi_persistently_if false R)%I // (into_persistent _ R)
+ sink_persistently sep_elim_r persistently_and_bare_sep_l wand_elim_r.
+ - by rewrite (absorbing_sink R) (_ : R = bi_persistently_if false R)%I //
+ (into_persistent _ R) sep_elim_r persistently_and_bare_sep_l wand_elim_r.
Qed.
Lemma tac_revert Δ Δ' i p P Q :
envs_lookup_delete i Δ = Some (p,P,Δ') →
- (Δ' ⊢ (if p then ⬕ P else P) -∗ Q) → Δ ⊢ Q.
+ (Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q.
Proof.
intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
rewrite HQ. destruct p; simpl; auto using wand_elim_r.
@@ -755,12 +758,12 @@ Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
IntoIH φ Δ P →
env_spatial_is_nil Δ = true →
- (of_envs Δ ⊢ □ P → Q) →
+ (of_envs Δ ⊢ bi_persistently P → Q) →
(of_envs Δ ⊢ Q).
Proof.
rewrite /IntoIH. intros HP ? HPQ.
rewrite (env_spatial_is_nil_bare_persistently Δ) //.
- rewrite -(idemp bi_and (⬕ Δ)%I) {1}HP // HPQ.
+ rewrite -(idemp bi_and (□ Δ)%I) {1}HP // HPQ.
by rewrite -{1}persistently_idemp !bare_persistently_elim impl_elim_r.
Qed.
@@ -859,9 +862,9 @@ Proof.
rewrite HP HPxy (bare_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
rewrite persistent_and_bare_sep_r -assoc. apply wand_elim_r'.
rewrite -persistent_and_bare_sep_r. apply impl_elim_r'. destruct lr.
- - apply (internal_eq_rewrite x y (λ y, ⬕?q Φ y -∗ Δ')%I). solve_proper.
+ - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I). solve_proper.
- rewrite internal_eq_sym.
- eapply (internal_eq_rewrite y x (λ y, ⬕?q Φ y -∗ Δ')%I). solve_proper.
+ eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ Δ')%I). solve_proper.
Qed.
(** * Conjunction splitting *)
@@ -1081,7 +1084,7 @@ Lemma tac_löb Δ Δ' i Q :
Proof.
intros ?? HQ. rewrite (env_spatial_is_nil_bare_persistently Δ) //.
rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
- rewrite -(löb (□ Q)%I) later_persistently. apply impl_intro_l.
+ rewrite -(löb (bi_persistently Q)%I) later_persistently. apply impl_intro_l.
rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
rewrite persistently_and_bare_sep_l -{1}bare_persistently_idemp bare_persistently_sep_2.
by rewrite wand_elim_r bare_elim.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ad1b54ad7..a97e6ba1d 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1270,9 +1270,9 @@ Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
Instance copy_destruct_wand {PROP : bi} (P Q : PROP) :
CopyDestruct Q → CopyDestruct (P -∗ Q).
Instance copy_destruct_bare {PROP : bi} (P : PROP) :
- CopyDestruct P → CopyDestruct (■P).
+ CopyDestruct P → CopyDestruct (bi_bare P).
Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
- CopyDestruct P → CopyDestruct (□ P).
+ CopyDestruct P → CopyDestruct (bi_persistently P).
Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
let hyp_name :=
@@ -1770,8 +1770,8 @@ Hint Extern 0 (_ ⊢ _) => progress iIntros.
Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
-Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ ■_) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ bi_persistently _) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ bi_bare _) => iAlways.
Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c704ba30c..327767326 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -6,7 +6,7 @@ Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
-Lemma demo_0 P Q : ⬕ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌠∨ ⌜x = 1âŒ) → (Q ∨ P).
+Lemma demo_0 P Q : â–¡ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌠∨ ⌜x = 1âŒ) → (Q ∨ P).
Proof.
iIntros "H #H2". iDestruct "H" as "###H".
(* should remove the disjunction "H" *)
@@ -44,7 +44,7 @@ Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
Lemma test_iRewrite {A : ofeT} (x y : A) P :
- ⬕ (∀ z, P -∗ ■(z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
+ □ (∀ z, P -∗ bi_bare (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
Proof.
iIntros "#H1 H2".
iRewrite (bi.internal_eq_sym x x with "[# //]").
@@ -53,7 +53,7 @@ Proof.
Qed.
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
- P ∧ emp -∗ emp ∧ Q -∗ ■(P ∗ Q).
+ P ∧ emp -∗ emp ∧ Q -∗ bi_bare (P ∗ Q).
Proof. iIntros "[#? _] [_ #?]". auto. Qed.
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
@@ -110,17 +110,17 @@ Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
Proof. iIntros "H". iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done. Qed.
Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
- φ → ■⌜y ≡ z⌠-∗ (⌜ φ ⌠∧ ⌜ φ ⌠∧ y ≡ z : PROP).
+ φ → bi_bare ⌜y ≡ z⌠-∗ (⌜ φ ⌠∧ ⌜ φ ⌠∧ y ≡ z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
Proof.
iIntros "HF".
- iAssert (â– False)%I with "[> -]" as %[].
+ iAssert (bi_bare False)%I with "[> -]" as %[].
by iMod "HF".
Qed.
-Lemma test_iMod_bare_timeless P `{!Timeless P} : ■▷ P -∗ ◇ ■P.
+Lemma test_iMod_bare_timeless P `{!Timeless P} : bi_bare (▷ P) -∗ ◇ bi_bare P.
Proof. iIntros "H". iMod "H". done. Qed.
Lemma test_iAssumption_False P : False -∗ P.
@@ -166,17 +166,17 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
Proof. iIntros "H". iNext. done. Qed.
Lemma test_iFrame_persistent (P Q : PROP) :
- ⬕ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∗ Q ∨ Q).
+ □ P -∗ Q -∗ bi_persistently (P ∗ P) ∗ (P ∗ Q ∨ Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
-Lemma test_iSplit_persistently P Q : ⬕ P -∗ □ (P ∗ P).
+Lemma test_iSplit_persistently P Q : □ P -∗ bi_persistently (P ∗ P).
Proof. iIntros "#?". by iSplit. Qed.
-Lemma test_iSpecialize_persistent P Q : ⬕ P -∗ (□ P → Q) -∗ Q.
+Lemma test_iSpecialize_persistent P Q : □ P -∗ (bi_persistently P → Q) -∗ Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Lemma test_iDestruct_persistent P (Φ : nat → PROP) `{!∀ x, Persistent (Φ x)}:
- ⬕ (P -∗ ∃ x, Φ x) -∗
+ □ (P -∗ ∃ x, Φ x) -∗
P -∗ ∃ x, Φ x ∗ P.
Proof.
iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
@@ -189,7 +189,7 @@ Proof.
Qed.
Lemma test_iInduction_wf (x : nat) P Q :
- ⬕ P -∗ Q -∗ ⌜ (x + 0 = x)%nat âŒ.
+ â–¡ P -∗ Q -∗ ⌜ (x + 0 = x)%nat âŒ.
Proof.
iIntros "#HP HQ".
iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
@@ -220,22 +220,24 @@ Lemma test_iIntros_let P :
∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
Proof. iIntros (Q R) "$ _ $". Qed.
-Lemma test_foo P Q : ■▷ (Q ≡ P) -∗ ■▷ Q -∗ ■▷ P.
+Lemma test_foo P Q : bi_bare (▷ (Q ≡ P)) -∗ bi_bare (▷ Q) -∗ bi_bare (▷ P).
Proof.
iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
Qed.
Lemma test_iIntros_modalities `(!Absorbing P) :
- (□ ▷ ∀ x : nat, ⌜ x = 0 ⌠→ ⌜ x = 0 ⌠-∗ False -∗ P -∗ P)%I.
+ (bi_persistently (▷ ∀ x : nat, ⌜ x = 0 ⌠→ ⌜ x = 0 ⌠-∗ False -∗ P -∗ P))%I.
Proof.
iIntros (x ??).
iIntros "* **". (* Test that fast intros do not work under modalities *)
iIntros ([]).
Qed.
-Lemma test_iNext_affine P Q : ■▷ (Q ≡ P) -∗ ■▷ Q -∗ ■▷ P.
+Lemma test_iNext_affine P Q :
+ bi_bare (▷ (Q ≡ P)) -∗ bi_bare (▷ Q) -∗ bi_bare (▷ P).
Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
-Lemma test_iAlways P Q R : ⬕ P -∗ □ Q → R -∗ □ ■■P ∗ ■□ Q.
+Lemma test_iAlways P Q R :
+ □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_bare (bi_bare P)) ∗ □ Q.
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
End tests.
--
GitLab