diff --git a/_CoqProject b/_CoqProject
index 582ae30e99b1093d48784ab918f0eaaab6ec6308..c64118f9c21814723843322542c2ca8231c3df65 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -26,6 +26,7 @@ theories/algebra/gmultiset.v
theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
+theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
theories/bi/derived_laws_bi.v
@@ -44,6 +45,7 @@ theories/bi/lib/laterable.v
theories/bi/lib/atomic.v
theories/bi/lib/core.v
theories/base_logic/upred.v
+theories/base_logic/bi.v
theories/base_logic/derived.v
theories/base_logic/base_logic.v
theories/base_logic/soundness.v
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 40a3d9a3eea6dde15f21c9faa89123226605d00e..88a6d22e2a44603a036e44233547a4e164eb50f1 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
another [uPred] module is by Jason Gross and described in:
https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
Module Import uPred.
- Export upred.uPred.
Export derived.uPred.
Export bi.
End uPred.
@@ -25,7 +24,7 @@ Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
@FromPure (uPredI M) af (✓ a) (✓ a).
Proof.
rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
- rewrite -cmra_valid_intro //. by apply pure_intro.
+ rewrite -cmra_valid_intro //.
Qed.
Global Instance from_sep_ownM (a b1 b2 : M) :
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
new file mode 100644
index 0000000000000000000000000000000000000000..c1b8e8f25acc72a5efd0bb8f43de5697eacefe8f
--- /dev/null
+++ b/theories/base_logic/bi.v
@@ -0,0 +1,150 @@
+From iris.bi Require Export derived_connectives updates plainly.
+From iris.base_logic Require Export upred.
+Import uPred_primitive.
+
+(** BI and other MoSeL instances for uPred. This file does *not* unseal. *)
+
+Definition uPred_emp {M} : uPred M := uPred_pure True.
+
+Local Existing Instance entails_po.
+
+Lemma uPred_bi_mixin (M : ucmraT) :
+ BiMixin
+ uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
+ (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
+ uPred_persistently.
+Proof.
+ split.
+ - exact: entails_po.
+ - exact: equiv_spec.
+ - exact: pure_ne.
+ - exact: and_ne.
+ - exact: or_ne.
+ - exact: impl_ne.
+ - exact: forall_ne.
+ - exact: exist_ne.
+ - exact: sep_ne.
+ - exact: wand_ne.
+ - exact: persistently_ne.
+ - exact: pure_intro.
+ - exact: pure_elim'.
+ - exact: @pure_forall_2.
+ - exact: and_elim_l.
+ - exact: and_elim_r.
+ - exact: and_intro.
+ - exact: or_intro_l.
+ - exact: or_intro_r.
+ - exact: or_elim.
+ - exact: impl_intro_r.
+ - exact: impl_elim_l'.
+ - exact: @forall_intro.
+ - exact: @forall_elim.
+ - exact: @exist_intro.
+ - exact: @exist_elim.
+ - exact: sep_mono.
+ - exact: True_sep_1.
+ - exact: True_sep_2.
+ - exact: sep_comm'.
+ - exact: sep_assoc'.
+ - exact: wand_intro_r.
+ - exact: wand_elim_l'.
+ - exact: persistently_mono.
+ - exact: persistently_idemp_2.
+ - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
+ trans (uPred_forall (M:=M) (fun _ : False => uPred_persistently uPred_emp)).
+ + apply forall_intro=>[[]].
+ + etrans; first exact: persistently_forall_2.
+ apply persistently_mono. exact: pure_intro.
+ - exact: @persistently_forall_2.
+ - exact: @persistently_exist_1.
+ - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
+ intros. etrans; first exact: sep_comm'.
+ etrans; last exact: True_sep_2.
+ apply sep_mono; last done.
+ exact: pure_intro.
+ - exact: persistently_and_sep_l_1.
+Qed.
+
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
+ uPred_entails uPred_pure uPred_or uPred_impl
+ (@uPred_forall M) (@uPred_exist M) uPred_sep
+ uPred_persistently (@uPred_internal_eq M) uPred_later.
+Proof.
+ split.
+ - exact: later_contractive.
+ - exact: internal_eq_ne.
+ - exact: @internal_eq_refl.
+ - exact: @internal_eq_rewrite.
+ - exact: @fun_ext.
+ - exact: @sig_eq.
+ - exact: @discrete_eq_1.
+ - exact: @later_eq_1.
+ - exact: @later_eq_2.
+ - exact: later_mono.
+ - exact: later_intro.
+ - exact: @later_forall_2.
+ - exact: @later_exist_false.
+ - exact: later_sep_1.
+ - exact: later_sep_2.
+ - exact: later_persistently_1.
+ - exact: later_persistently_2.
+ - exact: later_false_em.
+Qed.
+
+Canonical Structure uPredI (M : ucmraT) : bi :=
+ {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
+Canonical Structure uPredSI (M : ucmraT) : sbi :=
+ {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
+ sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
+
+Coercion uPred_valid {M} : uPred M → Prop := bi_emp_valid.
+
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Proof.
+ split.
+ - exact: plainly_ne.
+ - exact: plainly_mono.
+ - exact: plainly_elim_persistently.
+ - exact: plainly_idemp_2.
+ - exact: @plainly_forall_2.
+ - exact: persistently_impl_plainly.
+ - exact: plainly_impl_plainly.
+ - (* P ⊢ ■emp (ADMISSIBLE) *)
+ intros P.
+ trans (uPred_forall (M:=M) (fun _ : False => uPred_plainly uPred_emp)).
+ + apply forall_intro=>[[]].
+ + etrans; first exact: plainly_forall_2.
+ apply plainly_mono. exact: pure_intro.
+ - (* ■P ∗ Q ⊢ ■P (ADMISSIBLE) *)
+ intros P Q. etrans; last exact: True_sep_2.
+ etrans; first exact: sep_comm'.
+ apply sep_mono; last done.
+ exact: pure_intro.
+ - exact: prop_ext.
+ - exact: later_plainly_1.
+ - exact: later_plainly_2.
+Qed.
+Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+ {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+
+Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
+Proof.
+ split.
+ - exact: bupd_ne.
+ - exact: bupd_intro.
+ - exact: bupd_mono.
+ - exact: bupd_trans.
+ - exact: bupd_frame_r.
+Qed.
+Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+
+Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Proof. exact: bupd_plainly. Qed.
+
+(** extra BI instances *)
+
+Global Instance uPred_affine : BiAffine (uPredI M) | 0.
+Proof. intros P Q. exact: pure_intro. Qed.
+
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
+Proof. exact: @plainly_exist_1. Qed.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index e1c324096dbb1f37b9d3f34de057d45cf4a5987f..f4fe5135f9a484ee29cb6e53e45ed427be2866c7 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,9 +1,21 @@
-From iris.base_logic Require Export upred.
+From iris.base_logic Require Export bi.
From iris.bi Require Export bi.
Set Default Proof Using "Type".
-Import upred.uPred bi.
+Import bi.
Module uPred.
+
+(* New unseal tactic that also unfolds the BI layer *)
+Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+ unfold bi_emp; simpl; unfold sbi_emp; simpl;
+ unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
+ bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+ bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
+ unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
+ sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
+ unfold plainly, bi_plainly_plainly; simpl;
+ uPred_primitive.unseal.
+
Section derived.
Context {M : ucmraT}.
Implicit Types φ : Prop.
@@ -14,7 +26,57 @@ Implicit Types A : Type.
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-(* Own and valid derived *)
+(** Propers *)
+Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_flip_mono :
+ Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
+
+Global Existing Instance uPred_primitive.ownM_ne.
+Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
+
+Global Existing Instance uPred_primitive.cmra_valid_ne.
+Global Instance cmra_valid_proper {A : cmraT} :
+ Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
+
+(** Re-exporting primitive Own and valid lemmas *)
+Lemma ownM_op (a1 a2 : M) :
+ uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
+Proof. exact: uPred_primitive.ownM_op. Qed.
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
+Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+Proof. exact: uPred_primitive.ownM_unit. Qed.
+Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Proof. exact: uPred_primitive.later_ownM. Qed.
+Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+ x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌠∧ uPred_ownM y.
+Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
+
+Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+Proof. exact: uPred_primitive.ownM_valid. Qed.
+Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
+Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
+Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■✓ a.
+Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Proof. exact: uPred_primitive.prod_validI. Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+ ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
+Proof. exact: uPred_primitive.option_validI. Qed.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Proof. exact: uPred_primitive.discrete_valid. Qed.
+Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
+
+(** Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index a2bdd3d2e073017132e306078a23ac8a5d461ee7..a9d78acb9ff6502969e1c11c83253d1c951d4cbf 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -118,7 +118,7 @@ Lemma own_alloc_strong a (G : gset gname) :
Proof.
intros Ha.
rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌠∧ uPred_ownM m)%I).
- - rewrite /uPred_valid /bi_emp_valid ownM_unit.
+ - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
@@ -168,7 +168,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
- rewrite /uPred_valid /bi_emp_valid ownM_unit !own_eq /own_def.
+ rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, ofe_fun_singleton_update_empty.
apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
- apply cmra_transport_valid, ucmra_unit_valid.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 2c628625d0f8ae1ffbe7acfa07cbc25887121620..a47ddc9947579d076bd04ff086c36f6ee18e37e9 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra updates.
-From iris.bi Require Export derived_connectives updates plainly.
+From iris.bi Require Import notation.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -52,13 +52,11 @@ Record uPred (M : ucmraT) : Type := IProp {
uPred_mono n1 n2 x1 x2 :
uPred_holds n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.
-Arguments uPred_holds {_} _ _ _ : simpl never.
+Bind Scope bi_scope with uPred.
+Arguments uPred_holds {_} _%I _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
-Bind Scope bi_scope with uPred.
-Arguments uPred_holds {_} _%I _ _.
-
Section cofe.
Context {M : ucmraT}.
@@ -199,8 +197,6 @@ Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
Definition uPred_pure_eq :
@uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
-Definition uPred_emp {M} : uPred M := uPred_pure True.
-
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x ∧ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
@@ -278,7 +274,7 @@ Definition uPred_wand_eq :
(* Equivalently, this could be `∀ y, P n y`. That's closer to the intuition
of "embedding the step-indexed logic in Iris", but the two are equivalent
because Iris is afine. The following is easier to work with. *)
-Program Definition uPred_plainly_def {M} : Plainly (uPred M) := λ P,
+Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
@@ -335,391 +331,473 @@ Next Obligation.
exists (x' â‹… x3); split; first by rewrite -assoc.
eauto using uPred_mono, cmra_includedN_l.
Qed.
-Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
-Definition uPred_bupd {M} : BUpd (uPred M) := uPred_bupd_aux.(unseal).
-Definition uPred_bupd_eq {M} :
- @bupd _ uPred_bupd = @uPred_bupd_def M := uPred_bupd_aux.(seal_eq).
+Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
+Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M.
+Definition uPred_bupd_eq :
+ @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
+
+(** Global uPred-specific Notation *)
+Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
-Module uPred_unseal.
+(** Promitive logical rules.
+ These are not directly usable later because they do not refer to the BI
+ connectives. *)
+Module uPred_primitive.
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
uPred_cmra_valid_eq, @uPred_bupd_eq).
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
- unfold bi_emp; simpl; unfold sbi_emp; simpl;
- unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
- bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
- unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
- sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
- unfold plainly, bi_plainly_plainly; simpl;
rewrite !unseal_eqs /=.
-End uPred_unseal.
-Import uPred_unseal.
-Local Arguments uPred_holds {_} !_ _ _ /.
+Section primitive.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+Arguments uPred_holds {_} !_ _ _ /.
+Hint Immediate uPred_in_entails.
-Lemma uPred_bi_mixin (M : ucmraT) :
- BiMixin
- uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
- (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
- uPred_persistently.
+Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
+Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
+Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
+Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope.
+
+Notation "'True'" := (uPred_pure True) : bi_scope.
+Notation "'False'" := (uPred_pure False) : bi_scope.
+Notation "'⌜' φ 'âŒ'" := (uPred_pure φ%type%stdpp) : bi_scope.
+Infix "∧" := uPred_and : bi_scope.
+Infix "∨" := uPred_or : bi_scope.
+Infix "→" := uPred_impl : bi_scope.
+Notation "∀ x .. y , P" :=
+ (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
+Notation "∃ x .. y , P" :=
+ (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
+Infix "∗" := uPred_sep : bi_scope.
+Infix "-∗" := uPred_wand : bi_scope.
+Notation "â–¡ P" := (uPred_persistently P) : bi_scope.
+Notation "â– P" := (uPred_plainly P) : bi_scope.
+Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
+Notation "â–· P" := (uPred_later P) : bi_scope.
+Notation "|==> P" := (uPred_bupd P) : bi_scope.
+
+(** Entailment *)
+Lemma entails_po : PreOrder (⊢).
Proof.
split.
- - (* PreOrder uPred_entails *)
- split.
- + by intros P; split=> x i.
- + by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
- - (* (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P) *)
- intros P Q. split.
- + intros HPQ; split; split=> x i; apply HPQ.
- + intros [HPQ HQP]; split=> x n; by split; [apply HPQ|apply HQP].
- - (* Proper (iff ==> dist n) (@uPred_pure M) *)
- intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ.
- - (* NonExpansive2 uPred_and *)
- intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
- split; (intros [??]; split; [by apply HP|by apply HQ]).
- - (* NonExpansive2 uPred_or *)
- intros n P P' HP Q Q' HQ; split=> x n' ??.
- unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
- - (* NonExpansive2 uPred_impl *)
- intros n P P' HP Q Q' HQ; split=> x n' ??.
- unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
- - (* Proper (pointwise_relation A (dist n) ==> dist n) uPred_forall *)
- by intros A n Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
- - (* Proper (pointwise_relation A (dist n) ==> dist n) uPred_exist *)
- intros A n Ψ1 Ψ2 HΨ.
- unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
- - (* NonExpansive2 uPred_sep *)
- intros n P P' HP Q Q' HQ; split=> n' x ??.
- unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
- exists x1, x2; split_and!; try (apply HP || apply HQ);
- eauto using cmra_validN_op_l, cmra_validN_op_r.
- - (* NonExpansive2 uPred_wand *)
- intros n P P' HP Q Q' HQ; split=> n' x ??.
- unseal; split; intros HPQ x' n'' ???;
- apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
- - (* NonExpansive uPred_persistently *)
- intros n P1 P2 HP.
- unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
- - (* φ → P ⊢ ⌜φ⌠*)
- intros P φ ?. unseal; by split.
- - (* (φ → True ⊢ P) → ⌜φ⌠⊢ P *)
- intros φ P. unseal=> HP; split=> n x ??. by apply HP.
- - (* (∀ x : A, ⌜φ xâŒ) ⊢ ⌜∀ x : A, φ x⌠*)
- by unseal.
- - (* P ∧ Q ⊢ P *)
- intros P Q. unseal; by split=> n x ? [??].
- - (* P ∧ Q ⊢ Q *)
- intros P Q. unseal; by split=> n x ? [??].
- - (* (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R *)
- intros P Q R HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR].
- - (* P ⊢ P ∨ Q *)
- intros P Q. unseal; split=> n x ??; left; auto.
- - (* Q ⊢ P ∨ Q *)
- intros P Q. unseal; split=> n x ??; right; auto.
- - (* (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R *)
- intros P Q R HP HQ. unseal; split=> n x ? [?|?]. by apply HP. by apply HQ.
- - (* (P ∧ Q ⊢ R) → P ⊢ Q → R. *)
- intros P Q R. unseal => HQ; split=> n x ?? n' x' ????. apply HQ;
- naive_solver eauto using uPred_mono, cmra_included_includedN.
- - (* (P ⊢ Q → R) → P ∧ Q ⊢ R *)
- intros P Q R. unseal=> HP; split=> n x ? [??]. apply HP with n x; auto.
- - (* (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a *)
- intros A P Ψ. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ.
- - (* (∀ a, Ψ a) ⊢ Ψ a *)
- intros A Ψ a. unseal; split=> n x ? HP; apply HP.
- - (* Ψ a ⊢ ∃ a, Ψ a *)
- intros A Ψ a. unseal; split=> n x ??; by exists a.
- - (* (∀ a, Ψ a ⊢ Q) → (∃ a, Ψ a) ⊢ Q *)
- intros A Ψ Q. unseal; intros HΨ; split=> n x ? [a ?]; by apply HΨ with a.
- - (* (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q' *)
- intros P P' Q Q' HQ HQ'; unseal.
- split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
- eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
- - (* P ⊢ emp ∗ P *)
- intros P. rewrite /uPred_emp. unseal; split=> n x ?? /=.
- exists (core x), x. by rewrite cmra_core_l.
- - (* emp ∗ P ⊢ P *)
- intros P. unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
- eauto using uPred_mono, cmra_includedN_r.
- - (* P ∗ Q ⊢ Q ∗ P *)
- intros P Q. unseal; split; intros n x ? (x1&x2&?&?&?).
- exists x2, x1; by rewrite (comm op).
- - (* (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R) *)
- intros P Q R. unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
- exists y1, (y2 â‹… x2); split_and?; auto.
- + by rewrite (assoc op) -Hy -Hx.
- + by exists y2, x2.
- - (* (P ∗ Q ⊢ R) → P ⊢ Q -∗ R *)
- intros P Q R. unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
- exists x, x'; split_and?; auto.
- eapply uPred_mono; eauto using cmra_validN_op_l.
- - (* (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) → <pers> P ⊢ <pers> Q *)
- intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
- - (* <pers> P ⊢ <pers> <pers> P *)
- intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
- - (* P ⊢ <pers> emp (ADMISSIBLE) *)
- by unseal.
- - (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
- by unseal.
- - (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
- by unseal.
- - (* <pers> P ∗ Q ⊢ <pers> 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.
- - (* <pers> P ∧ Q ⊢ P ∗ Q *)
- intros P Q. unseal; split=> n x ? [??]; simpl in *.
- exists (core x), x; rewrite ?cmra_core_l; auto.
-Qed.
-
-Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
- uPred_entails uPred_pure uPred_or uPred_impl
- (@uPred_forall M) (@uPred_exist M) uPred_sep
- uPred_persistently (@uPred_internal_eq M) uPred_later.
+ - by intros P; split=> x i.
+ - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
+Qed.
+Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
+Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
+Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
Proof.
split.
- - (* Contractive sbi_later *)
- unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
- apply HPQ; eauto using cmra_validN_S.
- - (* NonExpansive2 (@uPred_internal_eq M A) *)
- intros A n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
- + by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
- + by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
- - (* P ⊢ a ≡ a *)
- intros A P a. unseal; by split=> n x ?? /=.
- - (* a ≡ b ⊢ Ψ a → Ψ b *)
- intros A a b Ψ Hnonexp.
- unseal; split=> n x ? Hab n' x' ??? HΨ. eapply Hnonexp with n a; auto.
- - (* (∀ x, f x ≡ g x) ⊢ f ≡ g *)
- by unseal.
- - (* `x ≡ `y ⊢ x ≡ y *)
- by unseal.
- - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌠*)
- intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
- - (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
- by unseal.
- - (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
- by unseal.
- - (* (P ⊢ Q) → ▷ P ⊢ ▷ Q *)
- intros P Q.
- unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
- - (* P ⊢ ▷ P *)
- intros P. unseal; split=> -[|n] /= x ? HP; first done.
- apply uPred_mono with (S n) x; eauto using cmra_validN_S.
- - (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *)
- intros A Φ. unseal; by split=> -[|n] x.
- - (* (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a) *)
- intros A Φ. unseal; split=> -[|[|n]] x /=; eauto.
- - (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
- intros P Q. unseal; split=> -[|n] x ? /=.
- { by exists x, (core x); rewrite cmra_core_r. }
- intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
- as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
- exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
- - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
- intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
- exists x1, x2; eauto using dist_S.
- - (* ▷ <pers> P ⊢ <pers> ▷ P *)
- by unseal.
- - (* <pers> ▷ P ⊢ ▷ <pers> P *)
- by unseal.
- - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
- intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
- intros [|n'] x' ????; [|done].
- eauto using uPred_mono, cmra_included_includedN.
-Qed.
-
-Canonical Structure uPredI (M : ucmraT) : bi :=
- {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
-Canonical Structure uPredSI (M : ucmraT) : sbi :=
- {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
- sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
-
-Coercion uPred_valid {M} : uPred M → Prop := bi_emp_valid.
-
-(* Latest notation *)
-Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
+ - intros HPQ; split; split=> x i; apply HPQ.
+ - intros [??]. exact: entails_anti_sym.
+Qed.
+Lemma entails_lim (cP cQ : chain (uPredC M)) :
+ (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
+Proof.
+ intros Hlim; split=> n m ? HP.
+ eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
+Qed.
-Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+(** Non-expansiveness and setoid morphisms *)
+Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M).
+Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|m] ?; try apply Hφ. Qed.
+
+Lemma and_ne : NonExpansive2 (@uPred_and M).
Proof.
- split.
- - (* NonExpansive uPred_plainly *)
- intros n P1 P2 HP.
- unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
- - (* (P ⊢ Q) → ■P ⊢ ■Q *)
- intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
- - (* ■P ⊢ <pers> P *)
- unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
- - (* ■P ⊢ ■■P *)
- unseal; split=> n x ?? //.
- - (* (∀ a, ■(Ψ a)) ⊢ ■(∀ a, Ψ a) *)
- by unseal.
- - (* (■P → <pers> Q) ⊢ <pers> (■P → Q) *)
- unseal; split=> /= n x ? HPQ n' x' ????.
- eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
- apply (HPQ n' x); eauto using cmra_validN_le.
- - (* (■P → ■Q) ⊢ ■(■P → Q) *)
- unseal; split=> /= n x ? HPQ n' x' ????.
- eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
- apply (HPQ n' x); eauto using cmra_validN_le.
- - (* P ⊢ ■emp (ADMISSIBLE) *)
- by unseal.
- - (* ■P ∗ Q ⊢ ■P *)
- 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) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
- unseal; split=> n x ? /= HPQ. split=> n' x' ??.
- move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
- move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
- - (* ▷ ■P ⊢ ■▷ P *)
- by unseal.
- - (* ■▷ P ⊢ ▷ ■P *)
- by unseal.
+ intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
+ split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.
-Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
- {| bi_plainly_mixin := uPred_plainly_mixin M |}.
-Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
+Lemma or_ne : NonExpansive2 (@uPred_or M).
Proof.
- split.
- - intros n P Q HPQ.
- unseal; split=> n' x; split; intros HP k yf ??;
- destruct (HP k yf) as (x'&?&?); auto;
- exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
- - unseal. split=> n x ? HP k yf ?; exists x; split; first done.
- apply uPred_mono with n x; eauto using cmra_validN_op_l.
- - unseal. intros HPQ; split=> n x ? HP k yf ??.
- destruct (HP k yf) as (x'&?&?); eauto.
- exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
- - unseal; split; naive_solver.
- - unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
- destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
- { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
- exists (x' â‹… x2); split; first by rewrite -assoc.
- exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
-
-Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
-Proof.
- rewrite /BiBUpdPlainly. unseal; split => n x Hnx /= Hng.
- destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
- eapply uPred_mono; eauto using ucmra_unit_leastN.
+ intros n P P' HP Q Q' HQ; split=> x n' ??.
+ unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.
-Module uPred.
-Include uPred_unseal.
-Section uPred.
-Context {M : ucmraT}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-Arguments uPred_holds {_} !_ _ _ /.
-Hint Immediate uPred_in_entails.
+Lemma impl_ne :
+ NonExpansive2 (@uPred_impl M).
+Proof.
+ intros n P P' HP Q Q' HQ; split=> x n' ??.
+ unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
+Qed.
-Global Instance ownM_ne : NonExpansive (@uPred_ownM M).
+Lemma sep_ne : NonExpansive2 (@uPred_sep M).
+Proof.
+ intros n P P' HP Q Q' HQ; split=> n' x ??.
+ unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
+ exists x1, x2; split_and!; try (apply HP || apply HQ);
+ eauto using cmra_validN_op_l, cmra_validN_op_r.
+Qed.
+
+Lemma wand_ne :
+ NonExpansive2 (@uPred_wand M).
+Proof.
+ intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
+ apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
+Qed.
+
+Lemma internal_eq_ne (A : ofeT) :
+ NonExpansive2 (@uPred_internal_eq M A).
+Proof.
+ intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
+ - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+ - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
+Qed.
+
+Lemma forall_ne A n :
+ Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
+Proof.
+ by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
+Qed.
+
+Lemma exist_ne A n :
+ Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
+Proof.
+ intros Ψ1 Ψ2 HΨ.
+ unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
+Qed.
+
+Lemma later_contractive : Contractive (@uPred_later M).
+Proof.
+ unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
+ apply HPQ; eauto using cmra_validN_S.
+Qed.
+
+Lemma plainly_ne : NonExpansive (@uPred_plainly M).
+Proof.
+ intros n P1 P2 HP.
+ unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
+Qed.
+
+Lemma persistently_ne : NonExpansive (@uPred_persistently M).
+Proof.
+ intros n P1 P2 HP.
+ unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
+Qed.
+
+Lemma ownM_ne : NonExpansive (@uPred_ownM M).
Proof.
intros n a b Ha.
unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
-Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-Global Instance cmra_valid_ne {A : cmraT} :
+Lemma cmra_valid_ne {A : cmraT} :
NonExpansive (@uPred_cmra_valid M A).
Proof.
intros n a b Ha; unseal; split=> n' x ? /=.
by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
-Global Instance cmra_valid_proper {A : cmraT} :
- Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
-(** BI instances *)
+Lemma bupd_ne : NonExpansive (@uPred_bupd M).
+Proof.
+ intros n P Q HPQ.
+ unseal; split=> n' x; split; intros HP k yf ??;
+ destruct (HP k yf) as (x'&?&?); auto;
+ exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
+Qed.
+
+(** Introduction and elimination rules *)
+Lemma pure_intro φ P : φ → P ⊢ ⌜φâŒ.
+Proof. by intros ?; unseal; split. Qed.
+Lemma pure_elim' φ P : (φ → True ⊢ P) → ⌜φ⌠⊢ P.
+Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
+Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ⌜φ xâŒ) ⊢ ⌜∀ x : A, φ xâŒ.
+Proof. by unseal. Qed.
-Global Instance uPred_affine : BiAffine (uPredI M) | 0.
-Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
+Lemma and_elim_l P Q : P ∧ Q ⊢ P.
+Proof. by unseal; split=> n x ? [??]. Qed.
+Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
+Proof. by unseal; split=> n x ? [??]. Qed.
+Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
+Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
+
+Lemma or_intro_l P Q : P ⊢ P ∨ Q.
+Proof. unseal; split=> n x ??; left; auto. Qed.
+Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
+Proof. unseal; split=> n x ??; right; auto. Qed.
+Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
+Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
+
+Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
+Proof.
+ unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
+ naive_solver eauto using uPred_mono, cmra_included_includedN.
+Qed.
+Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
+Proof. unseal; intros HP ; split=> n x ? [??]; apply HP with n x; auto. Qed.
-Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
-Proof. unfold BiPlainlyExist. by unseal. Qed.
+Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
+Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
+Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
+Proof. unseal; split=> n x ? HP; apply HP. Qed.
-(** Limits *)
-Lemma entails_lim (cP cQ : chain (uPredC M)) :
- (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
+Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
+Proof. unseal; split=> n x ??; by exists a. Qed.
+Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
+Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
+
+(** BI connectives *)
+Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
Proof.
- intros Hlim; split=> n m ? HP.
- eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
+ intros HQ HQ'; unseal.
+ split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
+ eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
+Qed.
+Lemma True_sep_1 P : P ⊢ True ∗ P.
+Proof.
+ unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
+Qed.
+Lemma True_sep_2 P : True ∗ P ⊢ P.
+Proof.
+ unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
+ eauto using uPred_mono, cmra_includedN_r.
+Qed.
+Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P.
+Proof.
+ unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
+Qed.
+Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
+Proof.
+ unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
+ exists y1, (y2 â‹… x2); split_and?; auto.
+ + by rewrite (assoc op) -Hy -Hx.
+ + by exists y2, x2.
+Qed.
+Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
+Proof.
+ unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
+ exists x, x'; split_and?; auto.
+ eapply uPred_mono with n x; eauto using cmra_validN_op_l.
+Qed.
+Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
+Proof.
+ unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
+ eapply HPQR; eauto using cmra_validN_op_l.
+Qed.
+
+(** Persistently *)
+Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
+Lemma persistently_elim P : □ P ⊢ P.
+Proof.
+ unseal; split=> n x ? /=.
+ eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
+Qed.
+Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
+Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+
+Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Proof. by unseal. Qed.
+Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+Proof. by unseal. Qed.
+
+Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ P ∗ Q.
+Proof.
+ unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
+ by rewrite cmra_core_l.
+Qed.
+
+(** Plainly *)
+Lemma plainly_mono P Q : (P ⊢ Q) → ■P ⊢ ■Q.
+Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
+Lemma plainly_elim_persistently P : ■P ⊢ □ P.
+Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
+Lemma plainly_idemp_2 P : ■P ⊢ ■■P.
+Proof. unseal; split=> n x ?? //. Qed.
+
+Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■Ψ a) ⊢ (■∀ a, Ψ a).
+Proof. by unseal. Qed.
+Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■∃ a, Ψ a) ⊢ (∃ a, ■Ψ a).
+Proof. by unseal. Qed.
+
+Lemma prop_ext P Q : ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+Proof.
+ unseal; split=> n x ? /= HPQ. split=> n' x' ??.
+ move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
+ move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
+Qed.
+
+(* The following two laws are very similar, and indeed they hold not just for â–¡
+ and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *)
+Lemma persistently_impl_plainly P Q : (■P → □ Q) ⊢ □ (■P → Q).
+Proof.
+ unseal; split=> /= n x ? HPQ n' x' ????.
+ eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
+ apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
+Lemma plainly_impl_plainly P Q : (■P → ■Q) ⊢ ■(■P → Q).
+Proof.
+ unseal; split=> /= n x ? HPQ n' x' ????.
+ eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
+ apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
+(** Later *)
+Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
+Proof.
+ unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
+Qed.
+Lemma later_intro P : P ⊢ ▷ P.
+Proof.
+ unseal; split=> -[|n] /= x ? HP; first done.
+ apply uPred_mono with (S n) x; eauto using cmra_validN_S.
+Qed.
+Lemma later_forall_2 {A} (Φ : A → uPred M) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
+Proof. unseal; by split=> -[|n] x. Qed.
+Lemma later_exist_false {A} (Φ : A → uPred M) :
+ (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
+Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed.
+Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
+Proof.
+ unseal; split=> n x ?.
+ destruct n as [|n]; simpl.
+ { by exists x, (core x); rewrite cmra_core_r. }
+ intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
+ as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
+ exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
+Qed.
+Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
+Proof.
+ unseal; split=> n x ?.
+ destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
+ exists x1, x2; eauto using dist_S.
+Qed.
+
+Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
+Proof.
+ unseal; split=> -[|n] x ? /= HP; [by left|right].
+ intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
+Qed.
+
+Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
+Proof. by unseal. Qed.
+Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+Proof. by unseal. Qed.
+Lemma later_plainly_1 P : ▷ ■P ⊢ ■▷ P.
+Proof. by unseal. Qed.
+Lemma later_plainly_2 P : ■▷ P ⊢ ▷ ■P.
+Proof. by unseal. Qed.
+
+(** Internal equality *)
+Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ (a ≡ a).
+Proof. unseal; by split=> n x ??; simpl. Qed.
+Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
+
+Lemma fun_ext `{B : A → ofeT} (g1 g2 : ofe_fun B) :
+ (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
+Proof. by unseal. Qed.
+Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigC P) :
+ proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
+Proof. by unseal. Qed.
+
+Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Proof. by unseal. Qed.
+Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Proof. by unseal. Qed.
+
+Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ.
+Proof.
+ unseal=> ?. split=> n x ?. by apply (discrete_iff n).
+Qed.
+
+(** Basic update modality *)
+Lemma bupd_intro P : P ⊢ |==> P.
+Proof.
+ unseal. split=> n x ? HP k yf ?; exists x; split; first done.
+ apply uPred_mono with n x; eauto using cmra_validN_op_l.
+Qed.
+Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ⊢ |==> Q.
+Proof.
+ unseal. intros HPQ; split=> n x ? HP k yf ??.
+ destruct (HP k yf) as (x'&?&?); eauto.
+ exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
+Qed.
+Lemma bupd_trans P : (|==> |==> P) ⊢ |==> P.
+Proof. unseal; split; naive_solver. Qed.
+Lemma bupd_frame_r P R : (|==> P) ∗ R ⊢ |==> P ∗ R.
+Proof.
+ unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
+ destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
+ { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
+ exists (x' â‹… x2); split; first by rewrite -assoc.
+ exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+Qed.
+Lemma bupd_plainly P : (|==> ■P) ⊢ P.
+Proof.
+ unseal; split => n x Hnx /= Hng.
+ destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
+ eapply uPred_mono; eauto using ucmra_unit_leastN.
Qed.
-(* Own *)
+(** Own *)
Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
Proof.
- rewrite /bi_sep /=; unseal. split=> n x ?; split.
+ unseal; split=> n x ?; split.
- intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
split. by exists (core a1); rewrite cmra_core_r. by exists z.
- intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
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 ⊢ <pers> uPred_ownM (core a).
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
Proof.
- rewrite /bi_persistently /=. unseal.
- split=> n x Hx /=. by apply cmra_core_monoN.
+ split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
Qed.
-Lemma ownM_unit : bi_emp_valid (uPred_ownM (ε:M)).
+Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
-Lemma later_ownM (a : M) : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
Proof.
- rewrite /bi_and /sbi_later /bi_exist /sbi_internal_eq /=; unseal.
- split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+ unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
destruct Hax as [y ?].
destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
exists a'. rewrite Hx. eauto using cmra_includedN_l.
Qed.
-(* Valid *)
-Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) :
- ✓ a ⊣⊢ (⌜✓ a⌠: uPred M).
-Proof. unseal. split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
+Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+ x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌠∧ uPred_ownM y.
+Proof.
+ unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
+ destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
+ { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
+ exists (y â‹… x3); split; first by rewrite -assoc.
+ exists y; eauto using cmra_includedN_l.
+Qed.
+
+(** Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof.
unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
Qed.
-Lemma cmra_valid_intro {A : cmraT} (a : A) :
- ✓ a → bi_emp_valid (PROP:=uPredI M) (✓ a).
+Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : uPred M).
-Proof.
- intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
-Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■(✓ a : uPred M).
+Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■✓ a.
Proof. by unseal. Qed.
-Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ (✓ a : uPred M).
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ (✓ x.1 ∧ ✓ x.2 : uPred M).
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
Proof. by unseal. Qed.
Lemma option_validI {A : cmraT} (mx : option A) :
✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
Proof. unseal. by destruct mx. Qed.
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) :
- (✓ g : uPred M) ⊣⊢ ∀ i, ✓ g i.
-Proof. by uPred.unseal. Qed.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma bupd_ownM_updateP x (Φ : M → Prop) :
- x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ⌜Φ y⌠∧ uPred_ownM y.
-Proof.
- intros Hup. unseal. split=> n x2 ? [x3 Hx] k yf ??.
- destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
- { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
- exists (y â‹… x3); split; first by rewrite -assoc.
- exists y; eauto using cmra_includedN_l.
-Qed.
-End uPred.
-End uPred.
+Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. by unseal. Qed.
+
+End primitive.
+End uPred_primitive.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 5857b235ef63233b2be00f2a7b77d64a8f883221..6cfef117eaa8da5d775c4c0dd27e382240238ff5 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -11,7 +11,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
((P -∗ Q) ∧ (Q -∗ P))%I.
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.
+Infix "∗-∗" := bi_wand_iff : bi_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
Arguments Persistent {_} _%I : simpl never.
@@ -23,8 +23,7 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
Arguments bi_affinely {_} _%I : simpl never.
Instance: Params (@bi_affinely) 1.
Typeclasses Opaque bi_affinely.
-Notation "'<affine>' P" := (bi_affinely P)
- (at level 20, right associativity) : bi_scope.
+Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
Arguments Affine {_} _%I : simpl never.
@@ -43,8 +42,7 @@ Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1.
Typeclasses Opaque bi_absorbingly.
-Notation "'<absorb>' P" := (bi_absorbingly P)
- (at level 20, right associativity) : bi_scope.
+Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
Arguments Absorbing {_} _%I : simpl never.
@@ -56,35 +54,28 @@ Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.
-Notation "'<pers>?' p P" := (bi_persistently_if p P)
- (at level 20, p at level 9, P at level 20,
- right associativity, format "'<pers>?' p P") : bi_scope.
+Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <affine> P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Typeclasses Opaque bi_affinely_if.
-Notation "'<affine>?' p P" := (bi_affinely_if p P)
- (at level 20, p at level 9, P at level 20,
- right associativity, format "'<affine>?' p P") : bi_scope.
+Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
(<affine> <pers> P)%I.
Arguments bi_intuitionistically {_} _%I : simpl never.
Instance: Params (@bi_intuitionistically) 1.
Typeclasses Opaque bi_intuitionistically.
-Notation "â–¡ P" := (bi_intuitionistically P)%I
- (at level 20, right associativity) : bi_scope.
+Notation "â–¡ P" := (bi_intuitionistically P) : bi_scope.
Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then â–¡ P else P)%I.
Arguments bi_intuitionistically_if {_} !_ _%I /.
Instance: Params (@bi_intuitionistically_if) 2.
Typeclasses Opaque bi_intuitionistically_if.
-Notation "'â–¡?' p P" := (bi_intuitionistically_if p P)
- (at level 20, p at level 9, P at level 20,
- right associativity, format "'â–¡?' p P") : bi_scope.
+Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
match As return himpl As PROP → PROP with
@@ -101,14 +92,12 @@ Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
Nat.iter n sbi_later P.
Arguments sbi_laterN {_} !_%nat_scope _%I.
Instance: Params (@sbi_laterN) 2.
-Notation "â–·^ n P" := (sbi_laterN n P)
- (at level 20, n at level 9, P at level 20, format "â–·^ n P") : bi_scope.
-Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P)
- (at level 20, p at level 9, P at level 20, format "â–·? p P") : bi_scope.
+Notation "â–·^ n P" := (sbi_laterN n P) : bi_scope.
+Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
Arguments sbi_except_0 {_} _%I : simpl never.
-Notation "â—‡ P" := (sbi_except_0 P) (at level 20, right associativity) : bi_scope.
+Notation "â—‡ P" := (sbi_except_0 P) : bi_scope.
Instance: Params (@sbi_except_0) 1.
Typeclasses Opaque sbi_except_0.
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 123e83c1a2c44940e1f65b6006af634ce875bbaf..2abcd87d22c8d2ab010cc29ff00c653d213fc254 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -531,7 +531,7 @@ Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌠-∗ P) ⊣⊢ (∀ _ :
Proof.
apply (anti_symm _).
- apply forall_intro=> Hφ.
- by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro emp%I φ) // wand_elim_r.
+ by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro φ emp%I) // wand_elim_r.
- apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
Qed.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 71ebd6a09ad190859391a68457fefba11b0f0018..fb475c79d14e0cff196709c17b32e39bb2af41c0 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,19 +1,7 @@
From iris.algebra Require Export ofe.
+From iris.bi Require Export notation.
Set Primitive Projections.
-Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "('⊢@{' PROP } )" (at level 99).
-Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
-Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
-Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
-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 "'<pers>' P" (at level 20, right associativity).
-Reserved Notation "â–· P" (at level 20, right associativity).
-
Section bi_mixin.
Context {PROP : Type} `{Dist PROP, Equiv PROP}.
Context (bi_entails : PROP → PROP → Prop).
@@ -77,7 +65,7 @@ Section bi_mixin.
bi_mixin_persistently_ne : NonExpansive bi_persistently;
(** Higher-order logic *)
- bi_mixin_pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ âŒ;
+ bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ âŒ;
bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌠⊢ P;
(* This is actually derivable if we assume excluded middle in Coq,
via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *)
@@ -195,7 +183,6 @@ Instance: Params (@bi_sep) 1.
Instance: Params (@bi_wand) 1.
Instance: Params (@bi_persistently) 1.
-Delimit Scope bi_scope with I.
Arguments bi_car : simpl never.
Arguments bi_dist : simpl never.
Arguments bi_equiv : simpl never.
@@ -347,7 +334,7 @@ Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.
(* Higher-order logic *)
-Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ âŒ.
+Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ âŒ.
Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌠⊢ P.
Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
new file mode 100644
index 0000000000000000000000000000000000000000..40cae68177a0b10cf4163433846e12f91924d7c5
--- /dev/null
+++ b/theories/bi/notation.v
@@ -0,0 +1,45 @@
+(** Just reserve the notation. *)
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "('⊢@{' PROP } )" (at level 99).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
+Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
+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 "'<pers>' P" (at level 20, right associativity).
+Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
+ right associativity, format "'<pers>?' p P").
+
+Reserved Notation "â–· P" (at level 20, right associativity).
+Reserved Notation "â–·? p P" (at level 20, p at level 9, P at level 20,
+ format "â–·? p P").
+Reserved Notation "â–·^ n P" (at level 20, n at level 9, P at level 20,
+ format "â–·^ n P").
+
+Reserved Infix "∗-∗" (at level 95, no associativity).
+
+Reserved Notation "'<affine>' P" (at level 20, right associativity).
+Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
+ right associativity, format "'<affine>?' p P").
+
+Reserved Notation "'<absorb>' P" (at level 20, right associativity).
+
+Reserved Notation "â–¡ P" (at level 20, right associativity).
+Reserved Notation "'â–¡?' p P" (at level 20, p at level 9, P at level 20,
+ right associativity, format "'â–¡?' p P").
+
+Reserved Notation "â—‡ P" (at level 20, right associativity).
+
+Reserved Notation "â– P" (at level 20, right associativity).
+Reserved Notation "â– ? p P" (at level 20, p at level 9, P at level 20,
+ right associativity, format "â– ? p P").
+
+Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==> Q").
+Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P ==∗ Q").
+
+(** Define the scope *)
+Delimit Scope bi_scope with I.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 7f15fee347ba612055377ed20a23602d1074e986..012d646ea19d91bd7f199e6bb0353a3a13016518 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -5,8 +5,7 @@ Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
Class Plainly (A : Type) := plainly : A → A.
Hint Mode Plainly ! : typeclass_instances.
Instance: Params (@plainly) 2.
-Notation "â– P" := (plainly P)%I
- (at level 20, right associativity) : bi_scope.
+Notation "â– P" := (plainly P) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *)
Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
@@ -96,9 +95,7 @@ Arguments plainly_if {_ _} !_ _%I /.
Instance: Params (@plainly_if) 2.
Typeclasses Opaque plainly_if.
-Notation "â– ? p P" := (plainly_if p P)%I
- (at level 20, p at level 9, P at level 20,
- right associativity, format "â– ? p P") : bi_scope.
+Notation "â– ? p P" := (plainly_if p P) : bi_scope.
(* Derived laws *)
Section plainly_derived.
@@ -167,7 +164,7 @@ Proof.
- by rewrite plainly_elim_persistently persistently_pure.
- apply pure_elim'=> Hφ.
trans (∀ x : False, ■True : PROP)%I; [by apply forall_intro|].
- rewrite plainly_forall_2. by rewrite -(pure_intro _ φ).
+ rewrite plainly_forall_2. by rewrite -(pure_intro φ).
Qed.
Lemma plainly_forall {A} (Ψ : A → PROP) : ■(∀ a, Ψ a) ⊣⊢ ∀ a, ■(Ψ a).
Proof.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 43462afefd41d4f74b2c4dececac823d3e62c42b..3a47ebd5f9bc9990338b8b454c7e1d33a0eff07c 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -7,12 +7,9 @@ Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
Instance : Params (@bupd) 2.
Hint Mode BUpd ! : typeclass_instances.
-Notation "|==> Q" := (bupd Q)
- (at level 99, Q at level 200, format "|==> Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
- (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
- (at level 99, Q at level 200, format "P ==∗ Q") : bi_scope.
+Notation "|==> Q" := (bupd Q) : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
Instance: Params (@fupd) 4.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 37c079bcb3e69f319c83781356f158a29a534c38..0d00294122fce3ab6e7f1f0e3941ff0cba334fe5 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -354,7 +354,7 @@ Global Instance into_forall_wand_pure φ P Q :
Proof.
rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
apply forall_intro=>? /=.
- by rewrite -(pure_intro True%I) // /bi_affinely right_id emp_wand.
+ by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
Qed.
Global Instance into_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :