From b56835d0dcec6691d330c8b0d1bc40369f417c34 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 May 2018 13:54:33 +0200
Subject: [PATCH] Make uPred itself independent of BI interface and just prove
primitive laws (like in master branch)
The BI interface is then instantiated using these laws. In particular, this
shows that the rules we claim to be admissible actually are.
---
_CoqProject | 2 +
theories/base_logic/base_logic.v | 3 +-
theories/base_logic/bi.v | 150 +++++
theories/base_logic/derived.v | 68 ++-
theories/base_logic/lib/own.v | 4 +-
theories/base_logic/upred.v | 728 +++++++++++++----------
theories/bi/derived_connectives.v | 31 +-
theories/bi/derived_laws_bi.v | 2 +-
theories/bi/interface.v | 19 +-
theories/bi/notation.v | 45 ++
theories/bi/plainly.v | 9 +-
theories/bi/updates.v | 9 +-
theories/proofmode/class_instances_sbi.v | 2 +-
13 files changed, 689 insertions(+), 383 deletions(-)
create mode 100644 theories/base_logic/bi.v
create mode 100644 theories/bi/notation.v
diff --git a/_CoqProject b/_CoqProject
index 582ae30e9..c64118f9c 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 40a3d9a3e..88a6d22e2 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 000000000..c1b8e8f25
--- /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 e1c324096..f4fe5135f 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 a2bdd3d2e..a9d78acb9 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 2c628625d..a47ddc994 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 5857b235e..6cfef117e 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 123e83c1a..2abcd87d2 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 71ebd6a09..fb475c79d 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 000000000..40cae6817
--- /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 7f15fee34..012d646ea 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 43462afef..3a47ebd5f 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 37c079bcb..0d0029412 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) :
--
GitLab