diff --git a/CHANGELOG.md b/CHANGELOG.md
index c15d3c9c279f97b8f2966c3182b6e81550c48158..d9dda024277d5ae9097d786793cb706a6e689168 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -166,6 +166,32 @@ Coq development, but not every API-breaking change is listed. Changes marked
+ Add instance `coreP_affine P : Affine P → Affine (coreP P)` and
lemma `coreP_wand P Q : <affine> ■(P -∗ Q) -∗ coreP P -∗ coreP Q`.
* Add lemma `mapsto_mapsto_ne : ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠l2âŒ`.
+* Flatten the BI hierarchy by merging the `bi` and `sbi` canonical structures.
+ This gives significant performance benefits on developments that construct BIs
+ from BIs (e.g., use `monPred`). For, example it gives a performance gain of 37%
+ overall on lambdarust-weak, with improvements for individual files up to 72%,
+ see Iris issue #303. The concrete changes are as follows:
+ + The `sbi` canonical structure has been removed.
+ + The `bi` canonical structure contains the later modality. It does not
+ require the later modality to be contractive or to satisfy the Löb rule, so
+ we provide a smart constructor `bi_later_mixin_id` to get the later axioms
+ "for free" if later is defined to be the identity function.
+ + There is a separate class `BiLöb`, and a "free" instance of that class if
+ the later modality is contractive. A `BiLöb` instance is required for the
+ `iLöb` tactic, and for timeless instances of implication and wand.
+ + There is a separate type class `BiInternalEq` for BIs with a notion of
+ internal equality (internal equality was part of `sbi`). An instance of this
+ class is needed for the `iRewrite` tactic, and the various lemmas about
+ internal equality.
+ + The class `SbiEmbed` has been removed and been replaced by classes
+ `BiEmbedLater` and `BiEmbedInternalEq`.
+ + The class `BiPlainly` has been generalized to BIs without internal equality.
+ As a consequence, there is a separate class `BiPropExt` for BIs with
+ propositional extensionality (i.e., `■(P ∗-∗ Q) ⊢ P ≡ Q`).
+ + The class `BiEmbedPlainly` is a bi-entailment (i.e., `⎡■P⎤ ⊣⊢ ■⎡P⎤`
+ instead of `■⎡P⎤ ⊢ ⎡■P⎤`) as it has been generalized to BIs without a
+ internal equality. In the past, the left-to-right direction was obtained for
+ "free" using the rules of internal equality.
The following `sed` script should perform most of the renaming (FIXME: incomplete)
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/_CoqProject b/_CoqProject
index 2bb663e11adec753a1436c12c8be1a48e2da3d7a..f01a9bc225191ea7c4f9cec35a2baf92f72ecdfa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -47,6 +47,7 @@ theories/bi/derived_connectives.v
theories/bi/derived_laws_bi.v
theories/bi/derived_laws_sbi.v
theories/bi/plainly.v
+theories/bi/internal_eq.v
theories/bi/big_op.v
theories/bi/updates.v
theories/bi/ascii.v
diff --git a/tests/heapprop.ref b/tests/heapprop.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/heapprop.v b/tests/heapprop.v
new file mode 100644
index 0000000000000000000000000000000000000000..e9c0405a23b5c4c38932b98b6e8d2bd7627f9565
--- /dev/null
+++ b/tests/heapprop.v
@@ -0,0 +1,234 @@
+From stdpp Require Import gmap.
+From iris.bi Require Import interface.
+From iris.proofmode Require Import tactics.
+
+(** This file constructs a simple non step-indexed linear separation logic as
+predicates over heaps (modeled as maps from integer locations to integer values).
+It shows that Iris's [bi] canonical structure can be inhabited, and the Iris
+proof mode can be used to prove lemmas in this separation logic. *)
+Definition loc := Z.
+Definition val := Z.
+
+Record heapProp := HeapProp {
+ heapProp_holds :> gmap loc val → Prop;
+}.
+Arguments heapProp_holds : simpl never.
+Add Printing Constructor heapProp.
+
+Section ofe.
+ Inductive heapProp_equiv' (P Q : heapProp) : Prop :=
+ { heapProp_in_equiv : ∀ σ, P σ ↔ Q σ }.
+ Instance heapProp_equiv : Equiv heapProp := heapProp_equiv'.
+ Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
+ Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
+ Canonical Structure heapPropO := discreteO heapProp.
+End ofe.
+
+(** logical entailement *)
+Inductive heapProp_entails (P Q : heapProp) : Prop :=
+ { heapProp_in_entails : ∀ σ, P σ → Q σ }.
+
+(** logical connectives *)
+Definition heapProp_emp_def : heapProp :=
+ {| heapProp_holds σ := σ = ∅ |}.
+Definition heapProp_emp_aux : seal (@heapProp_emp_def). Proof. by eexists. Qed.
+Definition heapProp_emp := unseal heapProp_emp_aux.
+Definition heapProp_emp_eq :
+ @heapProp_emp = @heapProp_emp_def := seal_eq heapProp_emp_aux.
+
+Definition heapProp_pure_def (φ : Prop) : heapProp :=
+ {| heapProp_holds _ := φ |}.
+Definition heapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.
+Definition heapProp_pure := unseal heapProp_pure_aux.
+Definition heapProp_pure_eq :
+ @heapProp_pure = @heapProp_pure_def := seal_eq heapProp_pure_aux.
+
+Definition heapProp_and_def (P Q : heapProp) : heapProp :=
+ {| heapProp_holds σ := P σ ∧ Q σ |}.
+Definition heapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.
+Definition heapProp_and := unseal heapProp_and_aux.
+Definition heapProp_and_eq:
+ @heapProp_and = @heapProp_and_def := seal_eq heapProp_and_aux.
+
+Definition heapProp_or_def (P Q : heapProp) : heapProp :=
+ {| heapProp_holds σ := P σ ∨ Q σ |}.
+Definition heapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.
+Definition heapProp_or := unseal heapProp_or_aux.
+Definition heapProp_or_eq:
+ @heapProp_or = @heapProp_or_def := seal_eq heapProp_or_aux.
+
+Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
+ {| heapProp_holds σ := P σ → Q σ |}.
+Definition heapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.
+Definition heapProp_impl := unseal heapProp_impl_aux.
+Definition heapProp_impl_eq :
+ @heapProp_impl = @heapProp_impl_def := seal_eq heapProp_impl_aux.
+
+Definition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp :=
+ {| heapProp_holds σ := ∀ a, Ψ a σ |}.
+Definition heapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.
+Definition heapProp_forall {A} := unseal heapProp_forall_aux A.
+Definition heapProp_forall_eq :
+ @heapProp_forall = @heapProp_forall_def := seal_eq heapProp_forall_aux.
+
+Definition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp :=
+ {| heapProp_holds σ := ∃ a, Ψ a σ |}.
+Definition heapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.
+Definition heapProp_exist {A} := unseal heapProp_exist_aux A.
+Definition heapProp_exist_eq :
+ @heapProp_exist = @heapProp_exist_def := seal_eq heapProp_exist_aux.
+
+Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
+ {| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
+Definition heapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.
+Definition heapProp_sep := unseal heapProp_sep_aux.
+Definition heapProp_sep_eq:
+ @heapProp_sep = @heapProp_sep_def := seal_eq heapProp_sep_aux.
+
+Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
+ {| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
+Definition heapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.
+Definition heapProp_wand := unseal heapProp_wand_aux.
+Definition heapProp_wand_eq:
+ @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
+
+Definition heapProp_persistently_def (P : heapProp) : heapProp :=
+ {| heapProp_holds σ := P ∅ |}.
+Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
+Proof. by eexists. Qed.
+Definition heapProp_persistently := unseal heapProp_persistently_aux.
+Definition heapProp_persistently_eq:
+ @heapProp_persistently = @heapProp_persistently_def := seal_eq heapProp_persistently_aux.
+
+(** Iris's [bi] class requires the presence of a later modality, but for non
+step-indexed logics, it can be defined as the identity. *)
+Definition heapProp_later (P : heapProp) : heapProp := P.
+
+Definition unseal_eqs :=
+ (heapProp_emp_eq, heapProp_pure_eq, heapProp_and_eq, heapProp_or_eq,
+ heapProp_impl_eq, heapProp_forall_eq, heapProp_exist_eq,
+ heapProp_sep_eq, heapProp_wand_eq, heapProp_persistently_eq).
+Ltac unseal := rewrite !unseal_eqs /=.
+
+Section mixins.
+ (** Enable [simpl] locally, which is useful for proofs in the model. *)
+ Local Arguments heapProp_holds !_ _ /.
+
+ Lemma heapProp_bi_mixin :
+ BiMixin
+ heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
+ heapProp_impl (@heapProp_forall) (@heapProp_exist)
+ heapProp_sep heapProp_wand heapProp_persistently.
+ Proof.
+ split.
+ - (* [PreOrder heapProp_entails] *)
+ split; repeat destruct 1; constructor; naive_solver.
+ - (* [P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P)] *)
+ intros P Q; split.
+ + intros [HPQ]; split; split; naive_solver.
+ + intros [[HPQ] [HQP]]; split; naive_solver.
+ - (* [Proper (iff ==> dist n) bi_pure] *)
+ unseal=> n φ1 φ2 Hφ; split; naive_solver.
+ - (* [NonExpansive2 bi_and] *)
+ unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+ - (* [NonExpansive2 bi_or] *)
+ unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+ - (* [NonExpansive2 bi_impl] *)
+ unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+ - (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A)] *)
+ unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> ? x; by apply HΦ.
+ - (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A)] *)
+ unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> -[x ?]; exists x; by apply HΦ.
+ - (* [NonExpansive2 bi_sep] *)
+ unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+ - (* [NonExpansive2 bi_wand] *)
+ unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+ - (* [NonExpansive2 bi_persistently] *)
+ unseal=> n P1 P2 [HP]; split; naive_solver.
+ - (* [φ → P ⊢ ⌜ φ âŒ] *)
+ unseal=> φ P ?; by split.
+ - (* [(φ → True ⊢ P) → ⌜ φ ⌠⊢ P] *)
+ unseal=> φ P HP; split=> σ ?. by apply HP.
+ - (* [(∀ a, ⌜ φ a âŒ) ⊢ ⌜ ∀ a, φ a âŒ] *)
+ unseal=> A φ; by split.
+ - (* [P ∧ Q ⊢ P] *)
+ unseal=> P Q; split=> σ [??]; done.
+ - (* [P ∧ Q ⊢ Q] *)
+ unseal=> P Q; split=> σ [??]; done.
+ - (* [(P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R] *)
+ unseal=> P Q R [HPQ] [HPR]; split=> σ; split; auto.
+ - (* [P ⊢ P ∨ Q] *)
+ unseal=> P Q; split=> σ; by left.
+ - (* [Q ⊢ P ∨ Q] *)
+ unseal=> P Q; split=> σ; by right.
+ - (* [(P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R] *)
+ unseal=> P Q R [HPQ] [HQR]; split=> σ [?|?]; auto.
+ - (* [(P ∧ Q ⊢ R) → P ⊢ Q → R] *)
+ unseal=> P Q R HPQR; split=> σ ??. by apply HPQR.
+ - (* [(P ⊢ Q → R) → P ∧ Q ⊢ R] *)
+ unseal=> P Q R HPQR; split=> σ [??]. by apply HPQR.
+ - (* [(∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a] *)
+ unseal=> A P Ψ HPΨ; split=> σ ? a. by apply HPΨ.
+ - (* [(∀ a, Ψ a) ⊢ Ψ a] *)
+ unseal=> A Ψ a; split=> σ ?; done.
+ - (* [Ψ a ⊢ ∃ a, Ψ a] *)
+ unseal=> A Ψ a; split=> σ ?. by exists a.
+ - (* [(∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q] *)
+ unseal=> A Φ Q HΦQ; split=> σ [a ?]. by apply (HΦQ a).
+ - (* [(P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'] *)
+ unseal=> P P' Q Q' [HPQ] [HP'Q']; split; naive_solver.
+ - (* [P ⊢ emp ∗ P] *)
+ unseal=> P; split=> σ ? /=. eexists ∅, σ. rewrite left_id_L.
+ split_and!; done || apply map_disjoint_empty_l.
+ - (* [emp ∗ P ⊢ P] *)
+ unseal=> P; split; intros ? (?&σ&->&?&->&?). by rewrite left_id_L.
+ - (* [P ∗ Q ⊢ Q ∗ P] *)
+ unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?).
+ exists σ2, σ1. by rewrite map_union_comm.
+ - (* [(P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R)] *)
+ unseal=> P Q R; split; intros ? (?&σ3&->&?&(σ1&σ2&->&?&?&?)&?).
+ exists σ1, (σ2 ∪ σ3). split_and!; [by rewrite assoc_L|solve_map_disjoint|done|].
+ exists σ2, σ3; split_and!; [done|solve_map_disjoint|done..].
+ - (* [(P ∗ Q ⊢ R) → P ⊢ Q -∗ R] *)
+ unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
+ - (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
+ unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
+ - (* [(P ⊢ Q) → <pers> P ⊢ <pers> Q] *)
+ unseal=> P Q [HPQ]; split=> σ. apply HPQ.
+ - (* [<pers> P ⊢ <pers> <pers> P] *)
+ unseal=> P; split=> σ; done.
+ - (* [emp ⊢ <pers> emp] *)
+ unseal; split=> σ; done.
+ - (* [(∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a)] *)
+ unseal=> A Ψ; split=> σ; done.
+ - (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a)] *)
+ unseal=> A Ψ; split=> σ; done.
+ - (* [<pers> P ∗ Q ⊢ <pers> P] *)
+ unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?); done.
+ - (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
+ unseal=> P Q; split=> σ [??]. eexists ∅, σ. rewrite left_id_L.
+ split_and!; done || apply map_disjoint_empty_l.
+ Qed.
+
+ Lemma heapProp_bi_later_mixin :
+ BiLaterMixin
+ heapProp_entails heapProp_pure heapProp_or heapProp_impl
+ (@heapProp_forall) (@heapProp_exist)
+ heapProp_sep heapProp_persistently heapProp_later.
+ Proof. eapply bi_later_mixin_id; [done|apply heapProp_bi_mixin]. Qed.
+End mixins.
+
+Canonical Structure heapPropI : bi :=
+ {| bi_ofe_mixin := ofe_mixin_of heapProp;
+ bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}.
+
+Lemma heapProp_proofmode_test {A} (P Q R : heapProp) (Φ Ψ : A → heapProp) :
+ P ∗ Q -∗
+ □ R -∗
+ □ (R -∗ ∃ x, Φ x) -∗
+ ∃ x, Φ x ∗ Φ x ∗ P ∗ Q.
+Proof.
+ iIntros "[HP HQ] #HR #HRΦ".
+ iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
+ iExists x. iFrame. by iSplitL.
+Qed.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index b22f2edf5bdfcdf81aa9a7362a9e218f9d555c5c..34d52265be0f8d05e97247815472e27f21d3c97b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -2,7 +2,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌠∨ ⌜x = 1âŒ
@@ -13,7 +13,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌠∨ ⌜x = 1âŒ
@@ -25,7 +25,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
Q : PROP
============================
"H1" : emp
@@ -36,7 +36,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
Q : PROP
============================
□ emp ∗ Q -∗ Q
@@ -44,7 +44,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
@@ -58,7 +58,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
Q : PROP
============================
"HQ" : <affine> Q
@@ -69,7 +69,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
Q : PROP
Affine0 : Affine Q
============================
@@ -81,7 +81,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
Ψ : nat → PROP
a : nat
============================
@@ -109,7 +109,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I wi
: string
1 subgoal
- PROP : sbi
+ PROP : bi
P, Q : PROP
n, m, k : nat
============================
@@ -120,7 +120,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I wi
: string
1 subgoal
- PROP : sbi
+ PROP : bi
φ : Prop
P, P2, Q, R1, R2 : PROP
H : φ
@@ -136,7 +136,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I wi
: string
1 subgoal
- PROP : sbi
+ PROP : bi
x, y : nat
============================
"H" : ⌜S (S (S x)) = yâŒ
@@ -145,7 +145,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I wi
1 subgoal
- PROP : sbi
+ PROP : bi
x, y, z : nat
============================
"H1" : ⌜S (S (S x)) = yâŒ
@@ -155,7 +155,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I wi
1 subgoal
- PROP : sbi
+ PROP : bi
x, y, z : nat
============================
"H1" : ⌜S (S (S x)) = yâŒ
@@ -172,7 +172,7 @@ Tactic failure: iEval: %: unsupported selection pattern.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
P, Q : PROP
============================
--------------------------------------∗
@@ -182,7 +182,7 @@ Tactic failure: iEval: %: unsupported selection pattern.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
P, Q : PROP
============================
--------------------------------------∗
@@ -194,7 +194,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiAffine0 : BiAffine PROP
P, Q : PROP
============================
@@ -207,7 +207,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
l : list nat
P : PROP
@@ -220,7 +220,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
l : list nat
P : PROP
@@ -235,7 +235,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
x1, x2 : nat
l1, l2 : list nat
P : PROP
@@ -248,7 +248,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
- PROP : sbi
+ PROP : bi
x1, x2 : nat
l1, l2 : list nat
P : PROP
@@ -264,7 +264,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
Φ : nat → nat → PROP
x1, x2 : nat
l1, l2 : list nat
@@ -278,7 +278,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
============================
"H" : â–¡ True
--------------------------------------∗
@@ -288,7 +288,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
============================
"H" : emp
--------------------------------------â–¡
@@ -298,7 +298,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
============================
"H" : emp
--------------------------------------â–¡
@@ -308,7 +308,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
mP : option PROP
Q, R : PROP
============================
@@ -320,7 +320,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
- PROP : sbi
+ PROP : bi
mP : option PROP
Q, R : PROP
============================
@@ -332,12 +332,11 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
X : Type
E1, E2 : coPset.coPset
- α : X → PROP
- β : X → PROP
+ α, β : X → PROP
γ : X → option PROP
============================
"Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
@@ -348,7 +347,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
@@ -359,7 +358,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
@@ -372,7 +371,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
@@ -383,7 +382,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
@@ -396,7 +395,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
@@ -408,7 +407,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
@@ -421,7 +420,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
@@ -433,7 +432,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
@@ -446,7 +445,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
E : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
@@ -459,7 +458,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
@@ -537,7 +536,7 @@ Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
: string
The command has indeed failed with message:
In environment
-PROP : sbi
+PROP : bi
P : PROP
The term "true" has type "bool" while it is expected to have type "nat".
"iStartProof_fail"
@@ -622,15 +621,15 @@ k is used in hypothesis Hk.
: string
The command has indeed failed with message:
Tactic failure: iRevert: k is used in hypothesis "Hk".
-"iLöb_no_sbi"
+"iLöb_no_BiLöb"
: string
The command has indeed failed with message:
-Tactic failure: iLöb: not a step-indexed BI entailment.
+Tactic failure: iLöb: no 'BiLöb' instance found.
"test_pure_name"
: string
1 subgoal
- PROP : sbi
+ PROP : bi
P1 : PROP
P2, P3 : Prop
Himpl : P2 → P3
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 6db8fd04f281394de05a14bf5e321d5ab35ac49c..af8ebb1eb1ee11ab1c003843fad0f8e9be0e6bb0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics intro_patterns.
Set Default Proof Using "Type".
Section tests.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
@@ -68,11 +68,11 @@ Check "test_iStopProof".
Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
-Lemma test_iRewrite {A : ofeT} (x y : A) P :
+Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofeT} (x y : A) P :
□ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
Proof.
iIntros "#H1 H2".
- iRewrite (bi.internal_eq_sym x x with "[# //]").
+ iRewrite (internal_eq_sym x x with "[# //]").
iRewrite -("H1" $! _ with "[- //]").
auto.
Qed.
@@ -127,7 +127,7 @@ Qed.
Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False âŒ.
Proof. by iIntros (?). Qed.
-Lemma test_fast_iIntros P Q :
+Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q :
⊢ ∀ x y z : nat,
⌜x = plus 0 x⌠→ ⌜y = 0⌠→ ⌜z = 0⌠→ P → □ Q → foo (x ≡ x).
Proof.
@@ -298,7 +298,7 @@ Proof.
unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅); try apply _. done.
Qed.
-Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
+Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofeT} (φ : Prop) (y z : A) :
φ → <affine> ⌜y ≡ z⌠-∗ (⌜ φ ⌠∧ ⌜ φ ⌠∧ y ≡ z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
@@ -390,7 +390,7 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
(∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.
-Lemma text_iNext_Next {A B : ofeT} (f : A -n> A) x y :
+Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofeT} (f : A -n> A) x y :
Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP).
Proof. iIntros "H". iNext. by iRewrite "H". Qed.
@@ -411,7 +411,7 @@ Proof.
iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.
-Lemma test_iLöb P : ⊢ ∃ n, ▷^n P.
+Lemma test_iLöb `{!BiLöb PROP} P : ⊢ ∃ n, ▷^n P.
Proof.
iLöb as "IH". iDestruct "IH" as (n) "IH".
by iExists (S n).
@@ -458,7 +458,8 @@ Lemma test_iIntros_let P :
∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
Proof. iIntros (Q R) "$ _ $". Qed.
-Lemma test_iNext_iRewrite P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
+Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
+ <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
Proof.
iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
Qed.
@@ -475,7 +476,8 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
x1 = x2 → (⌜ x2 = x3 ⌠∗ ⌜ x3 ≡ x4 ⌠∗ P) -∗ ⌜ x1 = x4 ⌠∗ P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
-Lemma test_iNext_affine P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
+Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
+ <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
Lemma test_iAlways P Q R :
@@ -822,7 +824,7 @@ Qed.
End tests.
Section parsing_tests.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types P : PROP.
(** Test notations for (bi)entailment and internal equality. These tests are
@@ -860,7 +862,7 @@ Lemma test_entails_annot_sections_space_close P :
(P ⊣⊢@{PROP} P ) ∧ (⊣⊢@{PROP} ) P P ∧ (.⊣⊢ P ) P.
Proof. naive_solver. Qed.
-Lemma test_sbi_internal_eq_annot_sections P :
+Lemma test_bi_internal_eq_annot_sections `{!BiInternalEq PROP} P :
⊢@{PROP}
P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧
((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧
@@ -870,7 +872,7 @@ Proof. naive_solver. Qed.
End parsing_tests.
Section printing_tests.
-Context {PROP : sbi} `{!BiFUpd PROP}.
+Context {PROP : bi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
Check "elim_mod_accessor".
@@ -944,7 +946,7 @@ End printing_tests.
(** Test error messages *)
Section error_tests.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iStopProof_not_proofmode".
@@ -1127,13 +1129,13 @@ Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
-Check "iLöb_no_sbi".
-Lemma iLöb_no_sbi P : ⊢ P.
+Check "iLöb_no_BiLöb".
+Lemma iLöb_no_BiLöb P : ⊢ P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
Section pure_name_tests.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types P Q R : PROP.
(* mock string_to_ident for just these tests *)
Ltac ltac_tactics.string_to_ident_hook ::=
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index 4c55aeb66f3c936c64319945f2e38dad225e807c..81193fd91117f55fbbbbd95faa239fbfbdbc12a1 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -45,9 +45,9 @@ Section base_logic_tests.
Lemma test_iStartProof_2 P : P -* P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_3 P : P -* P.
- Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
+ Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_4 P : P -* P.
- Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
+ Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
End base_logic_tests.
Section iris_tests.
@@ -233,7 +233,6 @@ Section monpred_tests.
Context {I : biIndex}.
Local Notation monPred := (monPred I (iPropI Σ)).
Local Notation monPredI := (monPredI I (iPropI Σ)).
- Local Notation monPredSI := (monPredSI I (iPropSI Σ)).
Implicit Types P Q R : monPred.
Implicit Types ð“Ÿ ð“ ð“¡ : iProp Σ.
@@ -261,7 +260,7 @@ End monpred_tests.
(** Test specifically if certain things parse correctly. *)
Section parsing_tests.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types P : PROP.
Lemma test_bi_emp_valid : |--@{PROP} True.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 74630ab6fc46b72533cee289187fcb1750cd5342..311380d4dcaafb514acd0ae0b9ca1dd0dc287285 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -43,9 +43,9 @@ Section base_logic_tests.
Lemma test_iStartProof_2 P : P -∗ P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_3 P : P -∗ P.
- Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
+ Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_4 P : P -∗ P.
- Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
+ Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
End base_logic_tests.
Section iris_tests.
@@ -231,7 +231,6 @@ Section monpred_tests.
Context {I : biIndex}.
Local Notation monPred := (monPred I (iPropI Σ)).
Local Notation monPredI := (monPredI I (iPropI Σ)).
- Local Notation monPredSI := (monPredSI I (iPropSI Σ)).
Implicit Types P Q R : monPred.
Implicit Types ð“Ÿ ð“ ð“¡ : iProp Σ.
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 973c967d95ffff9bad1dc6e1853814b5a83788aa..ea6b33fb27527a229500e3694b4aae8e7e92affd 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -1,8 +1,8 @@
1 subgoal
I : biIndex
- PROP : sbi
- P, Q : monpred.monPred I PROP
+ PROP : bi
+ P, Q : monPred
i : I
============================
"HW" : (P -∗ Q) i
@@ -12,8 +12,8 @@
1 subgoal
I : biIndex
- PROP : sbi
- P, Q : monpred.monPred I PROP
+ PROP : bi
+ P, Q : monPred
i, j : I
============================
"HW" : (P -∗ Q) j
@@ -24,8 +24,8 @@
1 subgoal
I : biIndex
- PROP : sbi
- P, Q : monpred.monPred I PROP
+ PROP : bi
+ P, Q : monPred
Objective0 : Objective Q
ð“Ÿ, ð“ : PROP
============================
@@ -38,9 +38,9 @@
1 subgoal
I : biIndex
- PROP : sbi
+ PROP : bi
FU0 : BiFUpd PROP * ()
- P, Q : monpred.monPred I PROP
+ P, Q : monPred
i : I
============================
--------------------------------------∗
@@ -49,9 +49,9 @@
1 subgoal
I : biIndex
- PROP : sbi
+ PROP : bi
FU0 : BiFUpd PROP * ()
- P : monpred.monPred I PROP
+ P : monPred
i : I
============================
--------------------------------------∗
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 8f46f5cedc8f9868b5236d75a0fbf6979947d691..b39d8ab7c1a5e694a3ae23b534acc337d520ffdf 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -3,10 +3,9 @@ From iris.base_logic.lib Require Import invariants.
Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
Section tests.
- Context {I : biIndex} {PROP : sbi}.
+ Context {I : biIndex} {PROP : bi}.
Local Notation monPred := (monPred I PROP).
Local Notation monPredI := (monPredI I PROP).
- Local Notation monPredSI := (monPredSI I PROP).
Implicit Types P Q R : monPred.
Implicit Types ð“Ÿ ð“ ð“¡ : PROP.
Implicit Types i j : I.
@@ -19,14 +18,14 @@ Section tests.
Lemma test_iStartProof_2 P : P -∗ P.
Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
Lemma test_iStartProof_3 P : P -∗ P.
- Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
+ Proof. iStartProof monPredI. iStartProof monPredI. iIntros "$". Qed.
Lemma test_iStartProof_4 P : P -∗ P.
- Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
+ Proof. iStartProof monPredI. iStartProof monPred. iIntros "$". Qed.
Lemma test_iStartProof_5 P : P -∗ P.
Proof. iStartProof PROP. iIntros (i) "$". Qed.
Lemma test_iStartProof_6 P : P ⊣⊢ P.
Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
- Lemma test_iStartProof_7 P : ⊢@{monPredI} P ≡ P.
+ Lemma test_iStartProof_7 `{!BiInternalEq PROP} P : ⊢@{monPredI} P ≡ P.
Proof. iStartProof PROP. done. Qed.
Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q.
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 5f4957effb35bbf563ce517031efe2ef366e810f..78bea449476f8569ef3257c881b734c623946454 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -1,6 +1,6 @@
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
@@ -15,7 +15,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
@@ -24,7 +24,7 @@
accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
@@ -37,7 +37,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
@@ -50,7 +50,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset
============================
@@ -62,7 +62,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0âŒ
@@ -71,7 +71,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0âŒ
@@ -82,7 +82,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
============================
"H" : ∃ x x0 : nat, <affine> ⌜x = x0âŒ
--------------------------------------∗
@@ -90,7 +90,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0âŒ
@@ -99,7 +99,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
============================
"H" : â–· (∃ x0 : nat, <affine> ⌜x = x0âŒ)
@@ -110,7 +110,7 @@
: string
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0âŒ
@@ -119,7 +119,7 @@
1 subgoal
- PROP : sbi
+ PROP : bi
x : nat
============================
"H" : â—‡ (∃ x0 : nat, <affine> ⌜x = x0âŒ)
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 73be62e134e7e736a8dbdb805265440251d55422..664ff6a1d3a4a67892456b597e20f2155b13064b 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section basic_tests.
- Context {PROP : sbi}.
+ Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_tforall {TT : tele} (Φ : TT → PROP) :
@@ -113,7 +113,7 @@ End accessor.
(* Robbert's tests *)
Section telescopes_and_tactics.
-Definition test1 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+Definition test1 {PROP : bi} {X : tele} (α : X → PROP) : PROP :=
(∃.. x, α x)%I.
Notation "'TEST1' {{ ∃ x1 .. xn , α } }" :=
@@ -122,7 +122,7 @@ Notation "'TEST1' {{ ∃ x1 .. xn , α } }" :=
fun x1 => .. (fun xn => α%I) ..))
(at level 20, α at level 200, x1 binder, xn binder, only parsing).
-Definition test2 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+Definition test2 {PROP : bi} {X : tele} (α : X → PROP) : PROP :=
(▷ ∃.. x, α x)%I.
Notation "'TEST2' {{ ∃ x1 .. xn , α } }" :=
@@ -131,7 +131,7 @@ Notation "'TEST2' {{ ∃ x1 .. xn , α } }" :=
fun x1 => .. (fun xn => α%I) ..))
(at level 20, α at level 200, x1 binder, xn binder, only parsing).
-Definition test3 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+Definition test3 {PROP : bi} {X : tele} (α : X → PROP) : PROP :=
(◇ ∃.. x, α x)%I.
Notation "'TEST3' {{ ∃ x1 .. xn , α } }" :=
@@ -141,7 +141,7 @@ Notation "'TEST3' {{ ∃ x1 .. xn , α } }" :=
(at level 20, α at level 200, x1 binder, xn binder, only parsing).
Check "test1_test".
-Lemma test1_test {PROP : sbi} :
+Lemma test1_test {PROP : bi} :
TEST1 {{ ∃ a b : nat, <affine> ⌜a = b⌠}} ⊢@{PROP} ▷ False.
Proof.
iIntros "H". iDestruct "H" as (x) "H". Show.
@@ -150,7 +150,7 @@ Restart.
Abort.
Check "test2_test".
-Lemma test2_test {PROP : sbi} :
+Lemma test2_test {PROP : bi} :
TEST2 {{ ∃ a b : nat, <affine> ⌜a = b⌠}} ⊢@{PROP} ▷ False.
Proof.
iIntros "H". iModIntro. Show.
@@ -160,7 +160,7 @@ Restart.
Abort.
Check "test3_test".
-Lemma test3_test {PROP : sbi} :
+Lemma test3_test {PROP : bi} :
TEST3 {{ ∃ a b : nat, <affine> ⌜a = b⌠}} ⊢@{PROP} ▷ False.
Proof.
iIntros "H". iMod "H".
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 25a06edf1ee43ff8f62ccff1cd084070ce5c5b33..5358d8dc17e5d358306be9f3e9cd1b96665c16c1 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -59,7 +59,7 @@ Section excl_auth.
Proof.
rewrite auth_both_validI bi.and_elim_r bi.and_elim_l.
apply bi.exist_elim=> -[[c|]|];
- by rewrite bi.option_equivI /= excl_equivI //= bi.False_elim.
+ by rewrite option_equivI /= excl_equivI //= bi.False_elim.
Qed.
Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 713caba78c85c41685b4bc3b9e152700c8763bad..ebb60030cf70cc7055d54e41e454bdd867cf8e14 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_connectives updates plainly.
+From iris.bi Require Export derived_connectives updates internal_eq plainly.
From iris.base_logic Require Export upred.
Import uPred_primitive.
@@ -66,21 +66,13 @@ Proof.
- 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.
+Lemma uPred_bi_later_mixin (M : ucmraT) :
+ BiLaterMixin
+ uPred_entails uPred_pure uPred_or uPred_impl
+ (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently 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.
+ - apply contractive_ne, later_contractive.
- exact: later_mono.
- exact: later_intro.
- exact: @later_forall_2.
@@ -93,12 +85,29 @@ Proof.
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 |}.
+ {| bi_ofe_mixin := ofe_mixin_of (uPred M);
+ bi_bi_mixin := uPred_bi_mixin M;
+ bi_bi_later_mixin := uPred_bi_later_mixin M |}.
+
+Instance uPred_later_contractive {M} : Contractive (bi_later (PROP:=uPredI M)).
+Proof. apply later_contractive. Qed.
+
+Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
+Proof.
+ split.
+ - 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.
+Qed.
+Global Instance uPred_internal_eq M : BiInternalEq (uPredI M) :=
+ {| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.
-Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly.
Proof.
split.
- exact: plainly_ne.
@@ -119,13 +128,15 @@ Proof.
etrans; first exact: sep_comm'.
apply sep_mono; last done.
exact: pure_intro.
- - exact: prop_ext_2.
- exact: later_plainly_1.
- exact: later_plainly_2.
Qed.
-Global Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
{| bi_plainly_mixin := uPred_plainly_mixin M |}.
+Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
+Proof. exact: prop_ext_2. Qed.
+
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
split.
@@ -137,7 +148,7 @@ Proof.
Qed.
Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
-Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
Proof. exact: bupd_plainly. Qed.
(** extra BI instances *)
@@ -148,7 +159,7 @@ Proof. intros P. exact: pure_intro. Qed.
many lemmas that have [BiAffine] as a premise. *)
Hint Immediate uPred_affine : core.
-Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredSI M).
+Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
Proof. exact: @plainly_exist_1. Qed.
(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
@@ -220,13 +231,12 @@ End restate.
This is used by [base_logic.bupd_alt].
TODO: Can we get rid of this? *)
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
- unfold bi_emp; simpl; unfold sbi_emp; simpl;
+ unfold bi_emp; simpl;
unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
- bi_and, bi_or, bi_impl, bi_forall, bi_exist,
- bi_sep, bi_wand, bi_persistently, 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;
+ bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+ bi_sep, bi_wand, bi_persistently, bi_later; simpl;
+ unfold internal_eq, bi_internal_eq_internal_eq,
+ plainly, bi_plainly_plainly; simpl;
uPred_primitive.unseal.
End uPred.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index db47402830c3fa66d59e681833a3ffa359fddb57..f4e50cb5684a4aab56d6682be3e4c052710e7501 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -14,7 +14,7 @@ Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
uPred_fupd_aux.(seal_eq).
-Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
split.
- rewrite uPred_fupd_eq. solve_proper.
@@ -32,13 +32,13 @@ Proof.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
-Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
+Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
-Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
+Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
-Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
+Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
Proof.
split.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 8f4cb5cd6902a8ef116d7da60df95847077194ca..214b72850c101e4e1f8aaf83831e9f9d114be7e3 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -125,7 +125,6 @@ Module Type iProp_solution_sig.
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
- Notation iPropSI Σ := (uPredSI (iResUR Σ)).
Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPrePropO Σ.
Parameter iProp_fold: ∀ {Σ}, iPrePropO Σ -n> iPropO Σ.
@@ -163,5 +162,5 @@ End iProp_solution.
Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
Proof.
- rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: bi.f_equiv.
+ rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: f_equivI.
Qed.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 6bfc39ba2c23d4ee28888817a60361d584ad5a6b..ce5889435a70183a6aecfddc058f941e8fe9e73e 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -119,10 +119,10 @@ Proof.
rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
{ intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id Hin)). }
- rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
+ rewrite (f_equivI (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton.
rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
- { by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
+ { by rewrite and_elim_r /bi_except_0 -or_intro_l. }
rewrite -except_0_intro -(exist_intro (cmra_transport (eq_sym inG_prf) b)).
apply and_mono.
- rewrite /iRes_singleton. assert (∀ {A A' : cmraT} (Heq : A' = A) (a : A),
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index d9cc45f05e96bd153ac9bef583f746fd8e7f3957..ea836c5104303296b18683deee4c58b6a0a25e24 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -62,7 +62,7 @@ Section saved_anything.
assert (∀ z, G2 (G1 z) ≡ z) as help.
{ intros z. rewrite /G1 /G2 -oFunctor_map_compose -{2}[z]oFunctor_map_id.
apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
- rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
+ rewrite -{2}[x]help -{2}[y]help. by iApply f_equivI.
Qed.
End saved_anything.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 0cc14c031fb7abee276ccf8ddc87d96f056feab3..1846c891253252d811f061f96c6afbed51a5bf27 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -113,7 +113,7 @@ Proof.
rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
- rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
+ rewrite lookup_fmap lookup_op lookup_singleton option_equivI.
case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
iExists Q; iSplit; first done.
iAssert (invariant_unfold Q ≡ invariant_unfold P)%I as "?".
@@ -121,7 +121,7 @@ Proof.
iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
rewrite /invariant_unfold.
- by rewrite agree_equivI bi.later_equivI iProp_unfold_equivI.
+ by rewrite agree_equivI later_equivI iProp_unfold_equivI.
Qed.
Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 9e9de7dbae24213b688f9705816f74f5d8fd6415..9fde00f1a5c85fb916f191363ba4ef5ddf431a44 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export derived_laws_bi derived_laws_sbi
- big_op updates plainly embedding.
+From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op.
+From iris.bi Require Export updates internal_eq plainly embedding.
Set Default Proof Using "Type".
Module Import bi.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 21cd47aac1d914eb44783cdcf2a58ac289544625..4bb1940211dcc1cb9beceeb6b55e8026ce9341df 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1557,7 +1557,7 @@ End bi_big_op.
(** * Properties for step-indexed BIs*)
Section sbi_big_op.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types Ps Qs : list PROP.
Implicit Types A : Type.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 28488c4faebc239206df1dd0783f78f600abb2df..4a64793a0cc79df75d0f6564b205ee2216d61097 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -83,23 +83,23 @@ Instance: Params (@bi_intuitionistically_if) 2 := {}.
Typeclasses Opaque bi_intuitionistically_if.
Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
-Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
+Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
match n with
| O => P
| S n' => â–· â–·^n' P
end%I
-where "â–·^ n P" := (sbi_laterN n P) : bi_scope.
-Arguments sbi_laterN {_} !_%nat_scope _%I.
-Instance: Params (@sbi_laterN) 2 := {}.
-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) : bi_scope.
-Instance: Params (@sbi_except_0) 1 := {}.
-Typeclasses Opaque sbi_except_0.
-
-Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
+where "â–·^ n P" := (bi_laterN n P) : bi_scope.
+Arguments bi_laterN {_} !_%nat_scope _%I.
+Instance: Params (@bi_laterN) 2 := {}.
+Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope.
+
+Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I.
+Arguments bi_except_0 {_} _%I : simpl never.
+Notation "â—‡ P" := (bi_except_0 P) : bi_scope.
+Instance: Params (@bi_except_0) 1 := {}.
+Typeclasses Opaque bi_except_0.
+
+Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Hint Mode Timeless + ! : typeclass_instances.
@@ -116,3 +116,13 @@ Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
Arguments bi_wandM {_} !_%I _%I /.
Notation "mP -∗? Q" := (bi_wandM mP Q)
(at level 99, Q at level 200, right associativity) : bi_scope.
+
+(** This class is required for the [iLöb] tactic. For most logics this class
+should not be inhabited directly, but the instance [Contractive (▷) → BiLöb PROP]
+in [derived_laws_sbi] should be used. A direct instance of the class is useful
+when considering a BI logic with a discrete OFE, instead of a OFE that takes
+step-indexing of the logic in account.*)
+Class BiLöb (PROP : bi) :=
+ löb (P : PROP) : (▷ P → P) ⊢ P.
+Hint Mode BiLöb ! : typeclass_instances.
+Arguments löb {_ _} _.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index b2d5d2de38a0b9f582ced050c659f69cabece28f..19bafd7bfde2abab9adff074be32961ce5b47cc3 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -5,7 +5,7 @@ Module bi.
Import interface.bi.
Import derived_laws_bi.bi.
Section sbi_derived.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
Implicit Types Ps : list PROP.
@@ -18,169 +18,15 @@ Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
-Global Instance internal_eq_proper (A : ofeT) :
- Proper ((≡) ==> (≡) ==> (⊣⊢)) (@sbi_internal_eq PROP A) := ne_proper_2 _.
Global Instance later_proper :
- Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_later PROP) := ne_proper _.
-
-(* Equality *)
-Hint Resolve internal_eq_refl : core.
-Hint Extern 100 (NonExpansive _) => solve_proper : core.
-
-Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
-Proof. intros ->. auto. Qed.
-Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A → PROP) P
- {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
- intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
- apply impl_elim_l'. by apply internal_eq_rewrite.
-Qed.
-
-Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
-Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
-Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
-Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
-
-Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
- x ≡ y ⊢ f x ≡ f y.
-Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
-Lemma f_equiv_contractive {A B : ofeT} (f : A → B) `{Hf : !Contractive f} x y :
- ▷ (x ≡ y) ⊢ f x ≡ f y.
-Proof.
- rewrite later_eq_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
- by apply f_equiv.
-Qed.
-
-Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
-Proof.
- apply (anti_symm _).
- - apply and_intro; apply f_equiv; apply _.
- - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
- apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
- apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
-Qed.
-Lemma sum_equivI {A B : ofeT} (x y : A + B) :
- x ≡ y ⊣⊢
- match x, y with
- | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
- end.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' x y (λ y,
- match x, y with
- | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
- end)%I); auto.
- destruct x; auto.
- - destruct x as [a|b], y as [a'|b']; auto; apply f_equiv, _.
-Qed.
-Lemma option_equivI {A : ofeT} (x y : option A) :
- x ≡ y ⊣⊢ match x, y with
- | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
- end.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' x y (λ y,
- match x, y with
- | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
- end)%I); auto.
- destruct x; auto.
- - destruct x as [a|], y as [a'|]; auto. apply f_equiv, _.
-Qed.
-
-Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
-Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.
-
-Section sigT_equivI.
-Import EqNotations.
-
-Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
- x ≡ y ⊣⊢
- ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' x y (λ y,
- ∃ eq : projT1 x = projT1 y,
- rew eq in projT2 x ≡ projT2 y))%I;
- [| done | exact: (exist_intro' _ _ eq_refl) ].
- move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
- apply exist_ne => ?. by rewrite Hab.
- - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
- apply f_equiv, _.
-Qed.
-End sigT_equivI.
-
-Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof.
- apply (anti_symm _); auto using fun_ext.
- apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
- intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
-Qed.
-Lemma ofe_morO_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
- - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
- set (h1 (f : A -n> B) :=
- exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
- set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
- @OfeMor A B (`f) (proj2_sig f)).
- assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
- assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
- by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI.
-Qed.
-
-Lemma pure_internal_eq {A : ofeT} (x y : A) : ⌜x ≡ y⌠⊢ x ≡ y.
-Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
-Proof.
- intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
-Qed.
-
-Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
-Proof.
- apply (anti_symm _), absorbingly_intro.
- apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
- apply wand_intro_l, internal_eq_refl.
-Qed.
-Lemma persistently_internal_eq {A : ofeT} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
- apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
- rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
-Qed.
-
-Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
- Absorbing (PROP:=PROP) (x ≡ y).
-Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
- Persistent (PROP:=PROP) (a ≡ b).
-Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
-
-(* Equality under a later. *)
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
- {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
-Proof.
- rewrite f_equiv_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
-Qed.
-Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
- {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
- rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
- by apply internal_eq_rewrite'.
-Qed.
-
-Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
-Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
-Lemma later_equivI_prop_2 (P Q : PROP) : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
-Proof. apply (f_equiv_contractive _). Qed.
+ Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _.
(* Later derived *)
Hint Resolve later_mono : core.
-Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@sbi_later PROP).
+Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@bi_later PROP).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
- Proper (flip (⊢) ==> flip (⊢)) (@sbi_later PROP).
+ Proper (flip (⊢) ==> flip (⊢)) (@bi_later PROP).
Proof. intros P Q; apply later_mono. Qed.
Lemma later_True : ▷ True ⊣⊢ True.
@@ -237,12 +83,13 @@ Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed
Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
-Section löb.
- (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
- Their Ψ is called Q in our proof. *)
- Lemma weak_löb P : (▷ P ⊢ P) → (True ⊢ P).
- Proof.
- pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
+(* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
+Their [Ψ] is called [Q] in our proof. *)
+Global Instance later_contractive_bi_löb :
+ Contractive (bi_later (PROP:=PROP)) → BiLöb PROP.
+Proof.
+ intros. assert (∀ P, (▷ P ⊢ P) → (True ⊢ P)) as weak_löb.
+ { intros P. pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
assert (∀ P, Contractive (flöb_pre P)) by solve_contractive.
set (Q := fixpoint (flöb_pre P)).
assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold).
@@ -251,25 +98,20 @@ Section löb.
{ rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q))%I.
by rewrite {1}HQ {1}later_impl impl_elim_l. }
rewrite -HQP HQ -2!later_intro.
- apply (entails_impl_True _ P). done.
- Qed.
-
- Lemma löb P : (▷ P → P) ⊢ P.
- Proof.
- apply entails_impl_True, weak_löb. apply impl_intro_r.
- rewrite -{2}(idemp (∧) (▷ P → P))%I.
- rewrite {2}(later_intro (▷ P → P))%I.
- rewrite later_impl.
- rewrite assoc impl_elim_l.
- rewrite impl_elim_r. done.
- Qed.
-End löb.
+ apply (entails_impl_True _ P). done. }
+ intros P. apply entails_impl_True, weak_löb. apply impl_intro_r.
+ rewrite -{2}(idemp (∧) (▷ P → P))%I.
+ rewrite {2}(later_intro (▷ P → P))%I.
+ rewrite later_impl.
+ rewrite assoc impl_elim_l.
+ rewrite impl_elim_r. done.
+Qed.
(* Iterated later modality *)
-Global Instance laterN_ne m : NonExpansive (@sbi_laterN PROP m).
+Global Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
Proof. induction m; simpl. by intros ???. solve_proper. Qed.
Global Instance laterN_proper m :
- Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_laterN PROP m) := ne_proper _.
+ Proper ((⊣⊢) ==> (⊣⊢)) (@bi_laterN PROP m) := ne_proper _.
Lemma laterN_0 P : ▷^0 P ⊣⊢ P.
Proof. done. Qed.
@@ -282,15 +124,15 @@ Proof. induction n1; f_equiv/=; auto. Qed.
Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
-Lemma laterN_iter n P : (â–·^n P)%I = Nat.iter n sbi_later P.
+Lemma laterN_iter n P : (â–·^n P)%I = Nat.iter n bi_later P.
Proof. induction n; f_equal/=; auto. Qed.
Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
Proof. induction n; simpl; auto. Qed.
-Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@sbi_laterN PROP n).
+Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@bi_laterN PROP n).
Proof. intros P Q; apply laterN_mono. Qed.
Global Instance laterN_flip_mono' n :
- Proper (flip (⊢) ==> flip (⊢)) (@sbi_laterN PROP n).
+ Proper (flip (⊢) ==> flip (⊢)) (@bi_laterN PROP n).
Proof. intros P Q; apply laterN_mono. Qed.
Lemma laterN_intro n P : P ⊢ ▷^n P.
@@ -336,34 +178,34 @@ Global Instance laterN_absorbing n P : Absorbing P → Absorbing (▷^n P).
Proof. induction n; apply _. Qed.
(* Except-0 *)
-Global Instance except_0_ne : NonExpansive (@sbi_except_0 PROP).
+Global Instance except_0_ne : NonExpansive (@bi_except_0 PROP).
Proof. solve_proper. Qed.
-Global Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_except_0 PROP).
+Global Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_except_0 PROP).
Proof. solve_proper. Qed.
-Global Instance except_0_mono' : Proper ((⊢) ==> (⊢)) (@sbi_except_0 PROP).
+Global Instance except_0_mono' : Proper ((⊢) ==> (⊢)) (@bi_except_0 PROP).
Proof. solve_proper. Qed.
Global Instance except_0_flip_mono' :
- Proper (flip (⊢) ==> flip (⊢)) (@sbi_except_0 PROP).
+ Proper (flip (⊢) ==> flip (⊢)) (@bi_except_0 PROP).
Proof. solve_proper. Qed.
Lemma except_0_intro P : P ⊢ ◇ P.
-Proof. rewrite /sbi_except_0; auto. Qed.
+Proof. rewrite /bi_except_0; auto. Qed.
Lemma except_0_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
Proof. by intros ->. Qed.
Lemma except_0_idemp P : ◇ ◇ P ⊣⊢ ◇ P.
-Proof. apply (anti_symm _); rewrite /sbi_except_0; auto. Qed.
+Proof. apply (anti_symm _); rewrite /bi_except_0; auto. Qed.
Lemma except_0_True : ◇ True ⊣⊢ True.
-Proof. rewrite /sbi_except_0. apply (anti_symm _); auto. Qed.
+Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
Lemma except_0_emp `{!BiAffine PROP} : ◇ emp ⊣⊢ emp.
Proof. by rewrite -True_emp except_0_True. Qed.
Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
-Proof. rewrite /sbi_except_0. apply (anti_symm _); auto. Qed.
+Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
Lemma except_0_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
-Proof. by rewrite /sbi_except_0 or_and_l. Qed.
+Proof. by rewrite /bi_except_0 or_and_l. Qed.
Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
Proof.
- rewrite /sbi_except_0. apply (anti_symm _).
+ rewrite /bi_except_0. apply (anti_symm _).
- apply or_elim; last by auto using sep_mono.
by rewrite -!or_intro_l -persistently_pure -later_sep -persistently_sep_dup.
- rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
@@ -391,14 +233,14 @@ Proof.
- apply exist_mono=> a. apply except_0_intro.
Qed.
Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
-Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
+Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
Lemma except_0_laterN n P : ◇ ▷^n P ⊢ ▷^n ◇ P.
Proof. by destruct n as [|n]; rewrite //= ?except_0_later -except_0_intro. Qed.
Lemma except_0_into_later P : ◇ P ⊢ ▷ P.
Proof. by rewrite -except_0_later -later_intro. Qed.
Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
Proof.
- by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.
+ by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure.
Qed.
Lemma except_0_affinely_2 P : <affine> ◇ P ⊢ ◇ <affine> P.
Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
@@ -421,9 +263,9 @@ Proof.
Qed.
Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
-Proof. rewrite /sbi_except_0; apply _. Qed.
+Proof. rewrite /bi_except_0; apply _. Qed.
Global Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
-Proof. rewrite /sbi_except_0; apply _. Qed.
+Proof. rewrite /bi_except_0; apply _. Qed.
(* Timeless instances *)
Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
@@ -431,7 +273,7 @@ Proof. solve_proper. Qed.
Global Instance pure_timeless φ : Timeless (PROP:=PROP) ⌜φâŒ.
Proof.
- rewrite /Timeless /sbi_except_0 pure_alt later_exist_false.
+ rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
Qed.
Global Instance emp_timeless `{BiAffine PROP} : Timeless (PROP:=PROP) emp.
@@ -442,12 +284,12 @@ Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
Global Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
-Global Instance impl_timeless P Q : Timeless Q → Timeless (P → Q).
+Global Instance impl_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P → Q).
Proof.
rewrite /Timeless=> HQ. rewrite later_false_em.
apply or_mono, impl_intro_l; first done.
- rewrite -{2}(löb Q); apply impl_intro_l.
- rewrite HQ /sbi_except_0 !and_or_r. apply or_elim; last auto.
+ rewrite -{2}(löb Q). apply impl_intro_l.
+ rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.
Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
@@ -455,12 +297,12 @@ Proof.
intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono.
Qed.
-Global Instance wand_timeless P Q : Timeless Q → Timeless (P -∗ Q).
+Global Instance wand_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P -∗ Q).
Proof.
rewrite /Timeless=> HQ. rewrite later_false_em.
apply or_mono, wand_intro_l; first done.
rewrite -{2}(löb Q); apply impl_intro_l.
- rewrite HQ /sbi_except_0 !and_or_r. apply or_elim; last auto.
+ rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
by rewrite (comm _ P) persistent_and_sep_assoc impl_elim_r wand_elim_l.
Qed.
Global Instance forall_timeless {A} (Ψ : A → PROP) :
@@ -473,13 +315,13 @@ Global Instance exist_timeless {A} (Ψ : A → PROP) :
(∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
Proof.
rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
- - rewrite /sbi_except_0; auto.
+ - rewrite /bi_except_0; auto.
- apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance persistently_timeless P : Timeless P → Timeless (<pers> P).
Proof.
- intros. rewrite /Timeless /sbi_except_0 later_persistently_1.
- by rewrite (timeless P) /sbi_except_0 persistently_or {1}persistently_elim.
+ intros. rewrite /Timeless /bi_except_0 later_persistently_1.
+ by rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
Qed.
Global Instance affinely_timeless P :
@@ -492,72 +334,69 @@ Global Instance intuitionistically_timeless P :
Timeless (PROP:=PROP) emp → Timeless P → Timeless (□ P).
Proof. rewrite /bi_intuitionistically; apply _. Qed.
-Global Instance eq_timeless {A : ofeT} (a b : A) :
- Discrete a → Timeless (PROP:=PROP) (a ≡ b).
-Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
(∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* Big op stuff *)
-Global Instance sbi_later_monoid_and_homomorphism :
- MonoidHomomorphism bi_and bi_and (≡) (@sbi_later PROP).
+Global Instance bi_later_monoid_and_homomorphism :
+ MonoidHomomorphism bi_and bi_and (≡) (@bi_later PROP).
Proof. split; [split|]; try apply _. apply later_and. apply later_True. Qed.
-Global Instance sbi_laterN_and_homomorphism n :
- MonoidHomomorphism bi_and bi_and (≡) (@sbi_laterN PROP n).
+Global Instance bi_laterN_and_homomorphism n :
+ MonoidHomomorphism bi_and bi_and (≡) (@bi_laterN PROP n).
Proof. split; [split|]; try apply _. apply laterN_and. apply laterN_True. Qed.
-Global Instance sbi_except_0_and_homomorphism :
- MonoidHomomorphism bi_and bi_and (≡) (@sbi_except_0 PROP).
+Global Instance bi_except_0_and_homomorphism :
+ MonoidHomomorphism bi_and bi_and (≡) (@bi_except_0 PROP).
Proof. split; [split|]; try apply _. apply except_0_and. apply except_0_True. Qed.
-Global Instance sbi_later_monoid_or_homomorphism :
- WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_later PROP).
+Global Instance bi_later_monoid_or_homomorphism :
+ WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_later PROP).
Proof. split; try apply _. apply later_or. Qed.
-Global Instance sbi_laterN_or_homomorphism n :
- WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_laterN PROP n).
+Global Instance bi_laterN_or_homomorphism n :
+ WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_or. Qed.
-Global Instance sbi_except_0_or_homomorphism :
- WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_except_0 PROP).
+Global Instance bi_except_0_or_homomorphism :
+ WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_or. Qed.
-Global Instance sbi_later_monoid_sep_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_later PROP).
+Global Instance bi_later_monoid_sep_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_later PROP).
Proof. split; try apply _. apply later_sep. Qed.
-Global Instance sbi_laterN_sep_weak_homomorphism n :
- WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_laterN PROP n).
+Global Instance bi_laterN_sep_weak_homomorphism n :
+ WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_sep. Qed.
-Global Instance sbi_except_0_sep_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_except_0 PROP).
+Global Instance bi_except_0_sep_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_sep. Qed.
-Global Instance sbi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
- MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_later PROP).
+Global Instance bi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
+ MonoidHomomorphism bi_sep bi_sep (≡) (@bi_later PROP).
Proof. split; try apply _. apply later_emp. Qed.
-Global Instance sbi_laterN_sep_homomorphism `{!BiAffine PROP} n :
- MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_laterN PROP n).
+Global Instance bi_laterN_sep_homomorphism `{!BiAffine PROP} n :
+ MonoidHomomorphism bi_sep bi_sep (≡) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_emp. Qed.
-Global Instance sbi_except_0_sep_homomorphism `{!BiAffine PROP} :
- MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_except_0 PROP).
+Global Instance bi_except_0_sep_homomorphism `{!BiAffine PROP} :
+ MonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_emp. Qed.
-Global Instance sbi_later_monoid_sep_entails_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_later PROP).
+Global Instance bi_later_monoid_sep_entails_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_later PROP).
Proof. split; try apply _. intros P Q. by rewrite later_sep. Qed.
-Global Instance sbi_laterN_sep_entails_weak_homomorphism n :
- WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_laterN PROP n).
+Global Instance bi_laterN_sep_entails_weak_homomorphism n :
+ WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_laterN PROP n).
Proof. split; try apply _. intros P Q. by rewrite laterN_sep. Qed.
-Global Instance sbi_except_0_sep_entails_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_except_0 PROP).
+Global Instance bi_except_0_sep_entails_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
Proof. split; try apply _. intros P Q. by rewrite except_0_sep. Qed.
-Global Instance sbi_later_monoid_sep_entails_homomorphism :
- MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_later PROP).
+Global Instance bi_later_monoid_sep_entails_homomorphism :
+ MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_later PROP).
Proof. split; try apply _. apply later_intro. Qed.
-Global Instance sbi_laterN_sep_entails_homomorphism n :
- MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_laterN PROP n).
+Global Instance bi_laterN_sep_entails_homomorphism n :
+ MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_intro. Qed.
-Global Instance sbi_except_0_sep_entails_homomorphism :
- MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_except_0 PROP).
+Global Instance bi_except_0_sep_entails_homomorphism :
+ MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_intro. Qed.
End sbi_derived.
End bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 5d1c0b798f8377d80b86a1582aa69cdf49653543..24f4c237f29151889720cc74c3656b67cc75e8e8 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,4 +1,5 @@
-From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
+From iris.bi Require Import interface derived_laws_sbi big_op.
+From iris.bi Require Import plainly updates internal_eq.
From iris.algebra Require Import monoid.
Class Embed (A B : Type) := embed : A → B.
@@ -16,6 +17,13 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
bi_embed_mixin_emp_valid_inj (P : PROP1) :
(⊢@{PROP2} ⎡P⎤) → ⊢ P;
+ (** The following axiom expresses that the embedding is injective in the OFE
+ sense. Instead of this axiom being expressed in terms of [siProp] or
+ externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
+ internal equality of _any other_ BI [PROP']. This is more general, as we do
+ not have any machinary to embed [siProp] into a BI with internal equality. *)
+ bi_embed_mixin_interal_inj `{BiInternalEq PROP'} (P Q : PROP1) :
+ ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
bi_embed_mixin_impl_2 (P Q : PROP1) :
(⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤;
@@ -39,38 +47,37 @@ Hint Mode BiEmbed ! - : typeclass_instances.
Hint Mode BiEmbed - ! : typeclass_instances.
Arguments bi_embed_embed : simpl never.
-Class BiEmbedEmp (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
- embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp;
-}.
+Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
+ embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp.
Hint Mode BiEmbedEmp ! - - : typeclass_instances.
Hint Mode BiEmbedEmp - ! - : typeclass_instances.
-Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
- embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y;
- embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤;
- embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
-}.
-Hint Mode SbiEmbed ! - - : typeclass_instances.
-Hint Mode SbiEmbed - ! - : typeclass_instances.
+Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
+ embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤.
+Hint Mode BiEmbedLater ! - - : typeclass_instances.
+Hint Mode BiEmbedLater - ! - : typeclass_instances.
+
+Class BiEmbedInternalEq (PROP1 PROP2 : bi)
+ `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
+ embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
+Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
+Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
Class BiEmbedBUpd (PROP1 PROP2 : bi)
- `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
- embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤
-}.
+ `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
+ embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
-Class BiEmbedFUpd (PROP1 PROP2 : sbi)
- `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
- embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤
-}.
+Class BiEmbedFUpd (PROP1 PROP2 : bi)
+ `{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2} :=
+ embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤.
Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
-Class BiEmbedPlainly (PROP1 PROP2 : sbi)
- `{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := {
- embed_plainly_2 (P : PROP1) : ■⎡P⎤ ⊢ (⎡■P⎤ : PROP2)
-}.
+Class BiEmbedPlainly (PROP1 PROP2 : bi)
+ `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
+ embed_plainly (P : PROP1) : ⎡■P⎤ ⊣⊢@{PROP2} ■⎡P⎤.
Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
@@ -86,6 +93,9 @@ Section embed_laws.
Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P.
Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
+ Lemma embed_interal_inj `{!BiInternalEq PROP'} (P Q : PROP1) :
+ ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q).
+ Proof. eapply bi_embed_mixin_interal_inj, bi_embed_mixin. Qed.
Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤.
@@ -259,66 +269,43 @@ Section embed.
⎡[∗ mset] y ∈ X, Φ y⎤ ⊣⊢ [∗ mset] y ∈ X, ⎡Φ y⎤.
Proof. apply (big_opMS_commute _). Qed.
End big_ops_emp.
-End embed.
-Section sbi_embed.
- Context `{SbiEmbed PROP1 PROP2}.
- Implicit Types P Q R : PROP1.
+ Section later.
+ Context `{!BiEmbedLater PROP1 PROP2}.
- Lemma embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
- Proof.
- apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
- etrans; [apply (bi.internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
- rewrite -(bi.internal_eq_refl True%I) embed_pure.
- eapply bi.impl_elim; [done|]. apply bi.True_intro.
- Qed.
- Lemma embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
- Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed.
- Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
- Proof. by rewrite embed_or embed_later embed_pure. Qed.
-
- (* Not an instance, since it may cause overlap *)
- Lemma bi_embed_plainly_emp `{!BiPlainly PROP1, !BiPlainly PROP2} :
- BiEmbedEmp PROP1 PROP2 → BiEmbedPlainly PROP1 PROP2.
- Proof.
- intros. constructor=> P. rewrite !plainly_alt embed_internal_eq.
- by rewrite -embed_affinely -embed_emp embed_interal_inj.
- Qed.
+ Lemma embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
+ Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed.
+ Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
+ Proof. by rewrite embed_or embed_later embed_pure. Qed.
- Lemma embed_plainly_1 `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■P⎤ ⊢ ■⎡P⎤.
- Proof.
- assert (∀ P, <affine> ⎡ P ⎤ ⊣⊢ (<affine> ⎡ <affine> P ⎤ : PROP2)) as Hhelp.
- { intros P'. apply (anti_symm _).
- - by rewrite -bi.affinely_idemp (embed_affinely_2 P').
- - by rewrite (bi.affinely_elim P'). }
- assert (<affine> ⎡ emp ⎤ ⊣⊢ (emp : PROP2)) as Hemp.
- { apply (anti_symm _).
- - apply bi.affinely_elim_emp.
- - apply bi.and_intro; auto using embed_emp_2. }
- rewrite !plainly_alt embed_internal_eq. by rewrite Hhelp -Hemp -!bi.f_equiv.
- Qed.
- Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2,
- !BiEmbedPlainly PROP1 PROP2} P : ⎡■P⎤ ⊣⊢ ■⎡P⎤.
- Proof.
- apply (anti_symm _). by apply embed_plainly_1. by apply embed_plainly_2.
- Qed.
+ Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
+ Proof.
+ intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
+ Qed.
+ End later.
+
+ Section internal_eq.
+ Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
- Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2,
- !BiEmbedPlainly PROP1 PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
- Proof. destruct p; simpl; auto using embed_plainly. Qed.
- Lemma embed_plainly_if_1 `{!BiPlainly PROP1, !BiPlainly PROP2} p P :
- ⎡■?p P⎤ ⊢ ■?p ⎡P⎤.
- Proof. destruct p; simpl; auto using embed_plainly_1. Qed.
+ Lemma embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+ Proof.
+ apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
+ etrans; [apply (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
+ rewrite -(internal_eq_refl True%I) embed_pure.
+ eapply bi.impl_elim; [done|]. apply bi.True_intro.
+ Qed.
+ End internal_eq.
- Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} (P : PROP1) :
- Plain P → Plain (PROP:=PROP2) ⎡P⎤.
- Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed.
+ Section plainly.
+ Context `{!BiPlainly PROP1, !BiPlainly PROP2, !BiEmbedPlainly PROP1 PROP2}.
- Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
- Proof.
- intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
- Qed.
-End sbi_embed.
+ Lemma embed_plainly_if p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
+ Proof. destruct p; simpl; auto using embed_plainly. Qed.
+
+ Lemma embed_plain (P : PROP1) : Plain P → Plain (PROP:=PROP2) ⎡P⎤.
+ Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly. Qed.
+ End plainly.
+End embed.
(* Not defined using an ordinary [Instance] because the default
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 845e3a33f02ebedf8d2611765609d5346c28a2ff..5a460db1ca45961fad65dd39457c41e327478644 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -15,26 +15,23 @@ Section bi_mixin.
Context (bi_sep : PROP → PROP → PROP).
Context (bi_wand : PROP → PROP → PROP).
Context (bi_persistently : PROP → PROP).
- Context (sbi_internal_eq : ∀ A : ofeT, A → A → PROP).
- Context (sbi_later : PROP → PROP).
+ Bind Scope bi_scope with PROP.
Local Infix "⊢" := bi_entails.
- Local Notation "'emp'" := bi_emp.
- Local Notation "'True'" := (bi_pure True).
- Local Notation "'False'" := (bi_pure False).
- Local Notation "'⌜' φ 'âŒ'" := (bi_pure φ%type%stdpp).
- Local Infix "∧" := bi_and.
- Local Infix "∨" := bi_or.
- Local Infix "→" := bi_impl.
+ Local Notation "'emp'" := bi_emp : bi_scope.
+ Local Notation "'True'" := (bi_pure True) : bi_scope.
+ Local Notation "'False'" := (bi_pure False) : bi_scope.
+ Local Notation "'⌜' φ 'âŒ'" := (bi_pure φ%type%stdpp) : bi_scope.
+ Local Infix "∧" := bi_and : bi_scope.
+ Local Infix "∨" := bi_or : bi_scope.
+ Local Infix "→" := bi_impl : bi_scope.
Local Notation "∀ x .. y , P" :=
- (bi_forall _ (λ x, .. (bi_forall _ (λ y, P)) ..)).
+ (bi_forall _ (λ x, .. (bi_forall _ (λ y, P%I)) ..)) : bi_scope.
Local Notation "∃ x .. y , P" :=
- (bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)).
- Local Infix "∗" := bi_sep.
- Local Infix "-∗" := bi_wand.
- Local Notation "'<pers>' P" := (bi_persistently P).
- Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
- Local Notation "â–· P" := (sbi_later P).
+ (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
+ Local Infix "∗" := bi_sep : bi_scope.
+ Local Infix "-∗" := bi_wand : bi_scope.
+ Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
(** * Axioms for a general BI (logic of bunched implications) *)
@@ -49,7 +46,7 @@ Section bi_mixin.
Record BiMixin := {
bi_mixin_entails_po : PreOrder bi_entails;
- bi_mixin_equiv_spec P Q : equiv P Q ↔ (P ⊢ Q) ∧ (Q ⊢ P);
+ bi_mixin_equiv_spec P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);
(** Non-expansiveness *)
bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
@@ -117,35 +114,51 @@ Section bi_mixin.
bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
}.
- Record SbiMixin := {
- sbi_mixin_later_contractive : Contractive sbi_later;
- sbi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (sbi_internal_eq A);
+ (** We equip any BI with a later modality. This avoids an additional layer in
+ the BI hierachy and improves performance significantly (see Iris issue #303).
- (* Equality *)
- sbi_mixin_internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a;
- sbi_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
- NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
- sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
- sbi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
- sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ;
+ For non step-indexed BIs the later modality can simply be defined as the
+ identity function, as the Löb axiom or contractiveness of later is not part of
+ [BiLaterMixin]. For step-indexed BIs one should separately prove an instance
+ of the class [BiLöb PROP] or [Contractive (▷)]. (Note that there is an
+ instance [Contractive (▷) → BiLöb PROP] in [derived_laws_sbi].)
- (* Later *)
- sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y);
- sbi_mixin_later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y;
+ For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
+ the smart constructor [bi_later_mixin_id] below. *)
+ Context (bi_later : PROP → PROP).
+ Local Notation "â–· P" := (bi_later P) : bi_scope.
- sbi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
- sbi_mixin_later_intro P : P ⊢ ▷ P;
+ Record BiLaterMixin := {
+ bi_mixin_later_ne : NonExpansive bi_later;
- sbi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
- sbi_mixin_later_exist_false {A} (Φ : A → PROP) :
+ bi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
+ bi_mixin_later_intro P : P ⊢ ▷ P;
+
+ bi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
+ bi_mixin_later_exist_false {A} (Φ : A → PROP) :
(▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
- sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
- sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
- sbi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
- sbi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;
+ bi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
+ bi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
+ bi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
+ bi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;
- sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
+ bi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
}.
+
+ Lemma bi_later_mixin_id :
+ (∀ (P : PROP), (▷ P)%I = P) →
+ BiMixin → BiLaterMixin.
+ Proof.
+ intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi).
+ split; repeat intro; rewrite ?Hlater ?Hequiv //.
+ - apply (bi_mixin_forall_intro Hbi)=> a.
+ etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater.
+ - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
+ apply (bi_mixin_exist_elim Hbi)=> a.
+ etrans; [|apply (bi_mixin_exist_intro Hbi a)]. by rewrite /= Hlater.
+ - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
+ apply (bi_mixin_impl_intro_r Hbi), (bi_mixin_and_elim_l Hbi).
+ Qed.
End bi_mixin.
Structure bi := Bi {
@@ -163,13 +176,19 @@ Structure bi := Bi {
bi_sep : bi_car → bi_car → bi_car;
bi_wand : bi_car → bi_car → bi_car;
bi_persistently : bi_car → bi_car;
+ bi_later : bi_car → bi_car;
bi_ofe_mixin : OfeMixin bi_car;
+ bi_cofe : Cofe (OfeT bi_car bi_ofe_mixin);
bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
bi_exist bi_sep bi_wand bi_persistently;
+ bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
+ bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
Coercion bi_ofeO (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.
+Global Instance bi_cofe' (PROP : bi) : Cofe PROP.
+Proof. apply bi_cofe. Qed.
Instance: Params (@bi_entails) 1 := {}.
Instance: Params (@bi_emp) 1 := {}.
@@ -182,6 +201,7 @@ Instance: Params (@bi_exist) 2 := {}.
Instance: Params (@bi_sep) 1 := {}.
Instance: Params (@bi_wand) 1 := {}.
Instance: Params (@bi_persistently) 1 := {}.
+Instance: Params (@bi_later) 1 := {}.
Arguments bi_car : simpl never.
Arguments bi_dist : simpl never.
@@ -197,63 +217,7 @@ Arguments bi_exist {PROP _} _%I : simpl never, rename.
Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments bi_persistently {PROP} _%I : simpl never, rename.
-
-Structure sbi := Sbi {
- sbi_car :> Type;
- sbi_dist : Dist sbi_car;
- sbi_equiv : Equiv sbi_car;
- sbi_entails : sbi_car → sbi_car → Prop;
- sbi_emp : sbi_car;
- sbi_pure : Prop → sbi_car;
- sbi_and : sbi_car → sbi_car → sbi_car;
- sbi_or : sbi_car → sbi_car → sbi_car;
- sbi_impl : sbi_car → sbi_car → sbi_car;
- sbi_forall : ∀ A, (A → sbi_car) → sbi_car;
- sbi_exist : ∀ A, (A → sbi_car) → sbi_car;
- sbi_sep : sbi_car → sbi_car → sbi_car;
- sbi_wand : sbi_car → sbi_car → sbi_car;
- sbi_persistently : sbi_car → sbi_car;
- sbi_internal_eq : ∀ A : ofeT, A → A → sbi_car;
- sbi_later : sbi_car → sbi_car;
- sbi_ofe_mixin : OfeMixin sbi_car;
- sbi_cofe : Cofe (OfeT sbi_car sbi_ofe_mixin);
- sbi_bi_mixin : BiMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl
- sbi_forall sbi_exist sbi_sep sbi_wand sbi_persistently;
- sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
- sbi_forall sbi_exist sbi_sep
- sbi_persistently sbi_internal_eq sbi_later;
-}.
-
-Instance: Params (@sbi_later) 1 := {}.
-Instance: Params (@sbi_internal_eq) 1 := {}.
-
-Arguments sbi_later {PROP} _%I : simpl never, rename.
-Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
-
-Coercion sbi_ofeO (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP).
-Canonical Structure sbi_ofeO.
-Coercion sbi_bi (PROP : sbi) : bi :=
- {| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}.
-Canonical Structure sbi_bi.
-Global Instance sbi_cofe' (PROP : sbi) : Cofe PROP.
-Proof. apply sbi_cofe. Qed.
-
-Arguments sbi_car : simpl never.
-Arguments sbi_dist : simpl never.
-Arguments sbi_equiv : simpl never.
-Arguments sbi_entails {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_emp {PROP} : simpl never, rename.
-Arguments sbi_pure {PROP} _%stdpp : simpl never, rename.
-Arguments sbi_and {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_or {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_impl {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_forall {PROP _} _%I : simpl never, rename.
-Arguments sbi_exist {PROP _} _%I : simpl never, rename.
-Arguments sbi_sep {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_wand {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_persistently {PROP} _%I : simpl never, rename.
-Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
-Arguments sbi_later {PROP} _%I : simpl never, rename.
+Arguments bi_later {PROP} _%I : simpl never, rename.
Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
@@ -291,14 +255,7 @@ Notation "∃ x .. y , P" :=
(bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
-Infix "≡" := sbi_internal_eq : bi_scope.
-Infix "≡@{ A }" := (sbi_internal_eq (A := A)) (only parsing) : bi_scope.
-
-Notation "( X ≡.)" := (sbi_internal_eq X) (only parsing) : bi_scope.
-Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
-Notation "(≡@{ A } )" := (sbi_internal_eq (A := A)) (only parsing) : bi_scope.
-
-Notation "â–· P" := (sbi_later P) : bi_scope.
+Notation "â–· P" := (bi_later P) : bi_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
@@ -420,63 +377,31 @@ Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
-End bi_laws.
-
-Section sbi_laws.
-Context {PROP : sbi}.
-Implicit Types φ : Prop.
-Implicit Types P Q R : PROP.
-
-(* Equality *)
-Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@sbi_internal_eq PROP A).
-Proof. eapply sbi_mixin_internal_eq_ne, sbi_sbi_mixin. Qed.
-
-Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
-Proof. eapply sbi_mixin_internal_eq_refl, sbi_sbi_mixin. Qed.
-Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
- NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-Proof. eapply sbi_mixin_internal_eq_rewrite, sbi_sbi_mixin. Qed.
-
-Lemma fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) :
- (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
-Proof. eapply sbi_mixin_fun_ext, sbi_sbi_mixin. Qed.
-Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) :
- `x ≡ `y ⊢@{PROP} x ≡ y.
-Proof. eapply sbi_mixin_sig_eq, sbi_sbi_mixin. Qed.
-Lemma discrete_eq_1 {A : ofeT} (a b : A) :
- Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ.
-Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
(* Later *)
-Global Instance later_contractive : Contractive (@sbi_later PROP).
-Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
-
-Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
-Proof. eapply sbi_mixin_later_eq_1, sbi_sbi_mixin. Qed.
-Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
-Proof. eapply sbi_mixin_later_eq_2, sbi_sbi_mixin. Qed.
+Global Instance later_ne : NonExpansive (@bi_later PROP).
+Proof. eapply bi_mixin_later_ne, bi_bi_later_mixin. Qed.
Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
-Proof. eapply sbi_mixin_later_mono, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_mono, bi_bi_later_mixin. Qed.
Lemma later_intro P : P ⊢ ▷ P.
-Proof. eapply sbi_mixin_later_intro, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_intro, bi_bi_later_mixin. Qed.
Lemma later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
-Proof. eapply sbi_mixin_later_forall_2, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_forall_2, bi_bi_later_mixin. Qed.
Lemma later_exist_false {A} (Φ : A → PROP) :
(▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
-Proof. eapply sbi_mixin_later_exist_false, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_exist_false, bi_bi_later_mixin. Qed.
Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
-Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_sep_1, bi_bi_later_mixin. Qed.
Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
-Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_sep_2, bi_bi_later_mixin. Qed.
Lemma later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P.
-Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (bi_mixin_later_persistently_1 bi_entails), bi_bi_later_mixin. Qed.
Lemma later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P.
-Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (bi_mixin_later_persistently_2 bi_entails), bi_bi_later_mixin. Qed.
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
-Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
-End sbi_laws.
-
+Proof. eapply bi_mixin_later_false_em, bi_bi_later_mixin. Qed.
+End bi_laws.
End bi.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
new file mode 100644
index 0000000000000000000000000000000000000000..6e97b92e65b31f04af244213095d902e2788b051
--- /dev/null
+++ b/theories/bi/internal_eq.v
@@ -0,0 +1,244 @@
+From iris.bi Require Import derived_laws_sbi big_op.
+Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+
+(** This file defines a type class for BIs with a notion of internal equality.
+Internal equality is not part of the [bi] canonical structure as [internal_eq]
+can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
+[▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
+Class InternalEq (PROP : bi) :=
+ internal_eq : ∀ {A : ofeT}, A → A → PROP.
+Arguments internal_eq {_ _ _} _ _ : simpl never.
+Hint Mode InternalEq ! : typeclass_instances.
+Instance: Params (@internal_eq) 3 := {}.
+Infix "≡" := internal_eq : bi_scope.
+Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
+
+Notation "( X ≡.)" := (internal_eq X) (only parsing) : bi_scope.
+Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
+Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
+
+(* Mixins allow us to create instances easily without having to use Program *)
+Record BiInternalEqMixin (PROP : bi) `(InternalEq PROP) := {
+ bi_internal_eq_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (@internal_eq PROP _ A);
+ bi_internal_eq_mixin_internal_eq_refl {A : ofeT} (P : PROP) (a : A) : P ⊢ a ≡ a;
+ bi_internal_eq_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
+ bi_internal_eq_mixin_fun_extI {A} {B : A → ofeT} (f g : discrete_fun B) :
+ (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g;
+ bi_internal_eq_mixin_sig_equivI_1 {A : ofeT} (P : A → Prop) (x y : sig P) :
+ `x ≡ `y ⊢@{PROP} x ≡ y;
+ bi_internal_eq_mixin_discrete_eq_1 {A : ofeT} (a b : A) :
+ Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ;
+ bi_internal_eq_mixin_later_equivI_1 {A : ofeT} (x y : A) :
+ Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y);
+ bi_internal_eq_mixin_later_equivI_2 {A : ofeT} (x y : A) :
+ ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y;
+}.
+
+Class BiInternalEq (PROP : bi) := {
+ bi_internal_eq_internal_eq :> InternalEq PROP;
+ bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
+}.
+Hint Mode BiInternalEq ! : typeclass_instances.
+Arguments bi_internal_eq_internal_eq : simpl never.
+
+Section internal_eq_laws.
+ Context `{BiInternalEq PROP}.
+ Implicit Types P Q : PROP.
+
+ Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@internal_eq PROP _ A).
+ Proof. eapply bi_internal_eq_mixin_internal_eq_ne, (bi_internal_eq_mixin). Qed.
+
+ Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
+ Proof. eapply bi_internal_eq_mixin_internal_eq_refl, bi_internal_eq_mixin. Qed.
+ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+ Proof. eapply bi_internal_eq_mixin_internal_eq_rewrite, bi_internal_eq_mixin. Qed.
+
+ Lemma fun_extI {A} {B : A → ofeT} (f g : discrete_fun B) :
+ (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
+ Proof. eapply bi_internal_eq_mixin_fun_extI, bi_internal_eq_mixin. Qed.
+ Lemma sig_equivI_1 {A : ofeT} (P : A → Prop) (x y : sig P) :
+ `x ≡ `y ⊢@{PROP} x ≡ y.
+ Proof. eapply bi_internal_eq_mixin_sig_equivI_1, bi_internal_eq_mixin. Qed.
+ Lemma discrete_eq_1 {A : ofeT} (a b : A) :
+ Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ.
+ Proof. eapply bi_internal_eq_mixin_discrete_eq_1, bi_internal_eq_mixin. Qed.
+
+ Lemma later_equivI_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
+ Proof. eapply bi_internal_eq_mixin_later_equivI_1, bi_internal_eq_mixin. Qed.
+ Lemma later_equivI_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
+ Proof. eapply bi_internal_eq_mixin_later_equivI_2, bi_internal_eq_mixin. Qed.
+End internal_eq_laws.
+
+(* Derived laws *)
+Section internal_eq_derived.
+Context `{BiInternalEq PROP}.
+Implicit Types P : PROP.
+
+(* Force implicit argument PROP *)
+Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+Global Instance internal_eq_proper (A : ofeT) :
+ Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
+
+(* Equality *)
+Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
+Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
+Hint Resolve internal_eq_refl : core.
+Hint Extern 100 (NonExpansive _) => solve_proper : core.
+
+Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
+Proof. intros ->. auto. Qed.
+Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A → PROP) P
+ {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+Proof.
+ intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+ apply impl_elim_l'. by apply internal_eq_rewrite.
+Qed.
+
+Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
+Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
+Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
+Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
+
+Lemma f_equivI {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
+ x ≡ y ⊢ f x ≡ f y.
+Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
+Lemma f_equivI_contractive {A B : ofeT} (f : A → B) `{Hf : !Contractive f} x y :
+ ▷ (x ≡ y) ⊢ f x ≡ f y.
+Proof.
+ rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
+ by apply f_equivI.
+Qed.
+
+Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
+Proof.
+ apply (anti_symm _).
+ - apply and_intro; apply f_equivI; apply _.
+ - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
+ apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
+ apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
+Qed.
+Lemma sum_equivI {A B : ofeT} (x y : A + B) :
+ x ≡ y ⊣⊢
+ match x, y with
+ | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
+ end.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' x y (λ y,
+ match x, y with
+ | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
+ end)%I); auto.
+ destruct x; auto.
+ - destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
+Qed.
+Lemma option_equivI {A : ofeT} (x y : option A) :
+ x ≡ y ⊣⊢ match x, y with
+ | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
+ end.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' x y (λ y,
+ match x, y with
+ | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
+ end)%I); auto.
+ destruct x; auto.
+ - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
+Qed.
+
+Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
+Proof. apply (anti_symm _). apply sig_equivI_1. apply f_equivI, _. Qed.
+
+Section sigT_equivI.
+Import EqNotations.
+
+Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
+ x ≡ y ⊣⊢
+ ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' x y (λ y,
+ ∃ eq : projT1 x = projT1 y,
+ rew eq in projT2 x ≡ projT2 y))%I;
+ [| done | exact: (exist_intro' _ _ eq_refl) ].
+ move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
+ apply exist_ne => ?. by rewrite Hab.
+ - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
+ apply f_equivI, _.
+Qed.
+End sigT_equivI.
+
+Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof.
+ apply (anti_symm _); auto using fun_extI.
+ apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
+ intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
+Qed.
+Lemma ofe_morO_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
+ - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
+ set (h1 (f : A -n> B) :=
+ exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
+ set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
+ @OfeMor A B (`f) (proj2_sig f)).
+ assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
+ assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
+ by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
+Qed.
+
+Lemma pure_internal_eq {A : ofeT} (x y : A) : ⌜x ≡ y⌠⊢ x ≡ y.
+Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
+Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
+Proof.
+ intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
+Qed.
+
+Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
+Proof.
+ apply (anti_symm _), absorbingly_intro.
+ apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
+ apply wand_intro_l, internal_eq_refl.
+Qed.
+Lemma persistently_internal_eq {A : ofeT} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
+ apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
+ rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
+Qed.
+
+Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
+ Absorbing (PROP:=PROP) (x ≡ y).
+Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
+Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
+ Persistent (PROP:=PROP) (a ≡ b).
+Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
+
+(* Equality under a later. *)
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
+ {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+Proof.
+ rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
+Qed.
+Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
+ {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+Proof.
+ rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
+ by apply internal_eq_rewrite'.
+Qed.
+
+Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
+Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
+Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
+ ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
+Proof. apply (f_equivI_contractive _). Qed.
+
+Global Instance eq_timeless {A : ofeT} (a b : A) :
+ Discrete a → Timeless (PROP:=PROP) (a ≡ b).
+Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
+End internal_eq_derived.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 1399d5fc18036ba9d01ef3bdd99d7d951a992461..bf560efa5fcc9457f5e10f9be58cee5cec2052cb 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -221,7 +221,7 @@ drop arbitrary resources (i.e., we can "defeat" linearity).
Variant 1: we assume a strong invariant creation lemma that lets us create
invariants in the "open" state. *)
Module linear1. Section linear1.
- Context {PROP: sbi}.
+ Context {PROP: bi}.
Implicit Types P : PROP.
(** Assumptions. *)
@@ -289,7 +289,7 @@ There, the stronger variant of the "unlock" rule (see Aquinas Hobor's PhD thesis
entirely into that lock.
*)
Module linear2. Section linear2.
- Context {PROP: sbi}.
+ Context {PROP: bi}.
Implicit Types P : PROP.
(** Assumptions. *)
diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 8fb0f8590b853ae41f9bfdba8d531eb601f098df..b1245dd5f149d65bb86fc0d1407aaf0402017e20 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -3,14 +3,14 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(** The class of laterable assertions *)
-Class Laterable {PROP : sbi} (P : PROP) := laterable :
+Class Laterable {PROP : bi} (P : PROP) := laterable :
P -∗ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
Arguments Laterable {_} _%I : simpl never.
Arguments laterable {_} _%I {_}.
Hint Mode Laterable + ! : typeclass_instances.
Section instances.
- Context {PROP : sbi}.
+ Context {PROP : bi}.
Implicit Types P : PROP.
Implicit Types Ps : list PROP.
diff --git a/theories/bi/lib/relations.v b/theories/bi/lib/relations.v
index 924a9908c2464aa7be5fc57b545a44e41e8e04df..a42b93d8bc7ab5079795291095fbf834420f64a6 100644
--- a/theories/bi/lib/relations.v
+++ b/theories/bi/lib/relations.v
@@ -3,13 +3,13 @@ its reflexive transitive closure. *)
From iris.bi.lib Require Export fixpoint.
From iris.proofmode Require Import tactics.
-Definition bi_rtc_pre
- {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+Definition bi_rtc_pre `{!BiInternalEq PROP}
+ {A : ofeT} (R : A → A → PROP)
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
(<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
-Instance bi_rtc_pre_mono
- {PROP : sbi} {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
+ {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
BiMonoPred (bi_rtc_pre R x).
Proof.
constructor; [|solve_proper].
@@ -20,28 +20,26 @@ Proof.
iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
Qed.
-Definition bi_rtc {PROP : sbi} {A : ofeT} (R : A → A → PROP)
- (x1 x2 : A) : PROP :=
+Definition bi_rtc `{!BiInternalEq PROP}
+ {A : ofeT} (R : A → A → PROP) (x1 x2 : A) : PROP :=
bi_least_fixpoint (bi_rtc_pre R x2) x1.
Instance: Params (@bi_rtc) 3 := {}.
Typeclasses Opaque bi_rtc.
-Instance bi_rtc_ne
- {PROP : sbi} {A : ofeT} (R : A → A → PROP)
- : NonExpansive2 (bi_rtc R).
+Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP) :
+ NonExpansive2 (bi_rtc R).
Proof.
intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
solve_proper.
Qed.
-Instance bi_rtc_proper
- {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP)
: Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
Section bi_rtc.
- Context {PROP : sbi}.
+ Context `{!BiInternalEq PROP}.
Context {A : ofeT}.
Context (R : A → A → PROP) `{NonExpansive2 R}.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index cbf453aac868c0b7ea9ca871ebd23ddafe6205ee..d6890ecbf322f35a2a65bf6c90d5f477031a55e6 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -109,7 +109,7 @@ Arguments monPred_at {_ _} _%I _.
Local Existing Instance monPred_mono.
Arguments monPredO _ _ : clear implicits.
-(** BI and SBI structures. *)
+(** BI canonical structure *)
Section Bi.
Context {I : biIndex} {PROP : bi}.
@@ -210,54 +210,37 @@ Next Obligation. solve_proper. Qed.
Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
Definition monPred_in := monPred_in_aux.(unseal).
Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
-End Bi.
-
-Arguments monPred_objectively {_ _} _%I.
-Arguments monPred_subjectively {_ _} _%I.
-Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
-Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
-
-Section Sbi.
-Context {I : biIndex} {PROP : sbi}.
-Implicit Types i : I.
-Notation monPred := (monPred I PROP).
-Implicit Types P Q : monPred.
-
-Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred :=
- MonPred (λ _, a ≡ b)%I _.
-Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). Proof. by eexists. Qed.
-Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
-Definition monPred_internal_eq_eq : @monPred_internal_eq = _ :=
- monPred_internal_eq_aux.(seal_eq).
Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_later_aux : seal monPred_later_def. Proof. by eexists. Qed.
Definition monPred_later := monPred_later_aux.(unseal).
Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
-End Sbi.
+End Bi.
+
+Arguments monPred_objectively {_ _} _%I.
+Arguments monPred_subjectively {_ _} _%I.
+Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
+Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
Module MonPred.
Definition unseal_eqs :=
(@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
@monPred_forall_eq, @monPred_exist_eq, @monPred_sep_eq, @monPred_wand_eq,
- @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
+ @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
@monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq,
@monPred_objectively_eq, @monPred_subjectively_eq).
Ltac unseal :=
- unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
+ unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
- bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
- bi_persistently, bi_affinely, 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;
+ bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
+ bi_persistently, bi_affinely, bi_later;
simpl;
rewrite !unseal_eqs /=.
End MonPred.
Import MonPred.
-Section canonical_bi.
+Section canonical.
Context (I : biIndex) (PROP : bi).
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
@@ -310,31 +293,13 @@ Proof.
- intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
Qed.
-Canonical Structure monPredI : bi :=
- {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin |}.
-End canonical_bi.
-
-Section canonical_sbi.
-Context (I : biIndex) (PROP : sbi).
-
-Lemma monPred_sbi_mixin :
- SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
- monPred_or monPred_impl monPred_forall monPred_exist
- monPred_sep monPred_persistently monPred_internal_eq monPred_later.
+Lemma monPred_bi_later_mixin :
+ BiLaterMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
+ monPred_or monPred_impl monPred_forall monPred_exist
+ monPred_sep monPred_persistently monPred_later.
Proof.
split; unseal.
- - intros n P Q HPQ. split=> i /=.
- apply bi.later_contractive. destruct n as [|n]=> //. by apply HPQ.
- by split=> ? /=; repeat f_equiv.
- - intros A P a. split=> i. by apply bi.internal_eq_refl.
- - intros A a b Ψ ?. split=> i /=.
- setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
- erewrite (bi.internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
- - intros A1 A2 f g. split=> i. by apply bi.fun_ext.
- - intros A P x y. split=> i. by apply bi.sig_eq.
- - intros A a b ?. split=> i. by apply bi.discrete_eq_1.
- - intros A x y. split=> i. by apply bi.later_eq_1.
- - intros A x y. split=> i. by apply bi.later_eq_2.
- intros P Q [?]. split=> i. by apply bi.later_mono.
- intros P. split=> i /=. by apply bi.later_intro.
- intros A Ψ. split=> i. by apply bi.later_forall_2.
@@ -347,10 +312,10 @@ Proof.
intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij. by rewrite Hij.
Qed.
-Canonical Structure monPredSI : sbi :=
- {| sbi_ofe_mixin := monPred_ofe_mixin; sbi_bi_mixin := monPred_bi_mixin I PROP;
- sbi_sbi_mixin := monPred_sbi_mixin |}.
-End canonical_sbi.
+Canonical Structure monPredI : bi :=
+ {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
+ bi_bi_later_mixin := monPred_bi_later_mixin |}.
+End canonical.
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
objective_at i j : P i -∗ P j.
@@ -435,6 +400,13 @@ Proof. unseal. split. solve_proper. Qed.
Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
Proof. solve_proper. Qed.
+Global Instance monPred_later_contractive :
+ Contractive (bi_later (PROP:=PROP)) → Contractive (bi_later (PROP:=monPredI)).
+Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
+Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
+Proof.
+ split=> i. unseal. by rewrite (bi.forall_elim i) bi.pure_True // left_id löb.
+Qed.
Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
Proof. split => ?. unseal. apply bi_positive. Qed.
Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
@@ -464,6 +436,10 @@ Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
Proof.
split; try apply _; rewrite /bi_emp_valid; unseal; try done.
- move=> P /= [/(_ inhabitant) ?] //.
+ - intros PROP' ? P Q.
+ set (f P := monPred_at P inhabitant).
+ assert (NonExpansive f) by solve_proper.
+ apply (f_equivI f).
- intros P Q. split=> i /=.
by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
- intros P Q. split=> i /=.
@@ -794,15 +770,11 @@ Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
BiEmbedBUpd PROP monPredI.
-Proof. split. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
-End bi_facts.
+Proof. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
-Section sbi_facts.
-Context {I : biIndex} {PROP : sbi}.
-Local Notation monPred := (monPred I PROP).
-Local Notation monPredSI := (monPredSI I PROP).
-Implicit Types i : I.
-Implicit Types P Q : monPred.
+(** Later *)
+Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
+Proof. split; by unseal. Qed.
Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
@@ -819,19 +791,6 @@ Proof.
by apply timeless, bi.exist_timeless.
Qed.
-Global Instance monPred_sbi_embed : SbiEmbed PROP monPredSI.
-Proof.
- split; unseal=> //. intros ? P Q.
- apply (@bi.f_equiv _ _ _ (λ P, monPred_at P inhabitant)); solve_proper.
-Qed.
-
-Lemma monPred_internal_eq_unfold : @sbi_internal_eq monPredSI = λ A x y, ⎡ x ≡ y ⎤%I.
-Proof. by unseal. Qed.
-
-(** Unfolding lemmas *)
-Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
- @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
-Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
Proof. by unseal. Qed.
Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
@@ -839,26 +798,64 @@ Proof. induction n; first done. rewrite /= monPred_at_later IHn //. Qed.
Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
Proof. by unseal. Qed.
-Lemma monPred_equivI {PROP' : sbi} P Q :
+Global Instance later_objective P `{!Objective P} : Objective (â–· P).
+Proof. intros ??. unseal. by rewrite objective_at. Qed.
+Global Instance laterN_objective P `{!Objective P} n : Objective (â–·^n P).
+Proof. induction n; apply _. Qed.
+Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
+Proof. rewrite /bi_except_0. apply _. Qed.
+
+(** Internal equality *)
+Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : monPred :=
+ MonPred (λ _, a ≡ b)%I _.
+Definition monPred_internal_eq_aux `{!BiInternalEq PROP} : seal (@monPred_internal_eq_def _).
+Proof. by eexists. Qed.
+Definition monPred_internal_eq `{!BiInternalEq PROP} := monPred_internal_eq_aux.(unseal).
+Definition monPred_internal_eq_eq `{!BiInternalEq PROP} :
+ @internal_eq _ (@monPred_internal_eq _) = _ := monPred_internal_eq_aux.(seal_eq).
+
+Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
+ BiInternalEqMixin monPredI (@monPred_internal_eq _).
+Proof.
+ split; rewrite monPred_internal_eq_eq.
+ - split=> i /=. solve_proper.
+ - intros A P a. split=> i /=. apply internal_eq_refl.
+ - intros A a b Ψ ?. split=> i /=. unseal.
+ setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
+ erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
+ - intros A1 A2 f g. split=> i /=. unseal. by apply fun_extI.
+ - intros A P x y. split=> i /=. by apply sig_equivI_1.
+ - intros A a b ?. split=> i /=. unseal. by apply discrete_eq_1.
+ - intros A x y. split=> i /=. unseal. by apply later_equivI_1.
+ - intros A x y. split=> i /=. unseal. by apply later_equivI_2.
+Qed.
+Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} : BiInternalEq monPredI :=
+ {| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
+
+Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
+ BiEmbedInternalEq PROP monPredI.
+Proof. split=> i. rewrite monPred_internal_eq_eq. by unseal. Qed.
+
+Lemma monPred_internal_eq_unfold `{!BiInternalEq PROP} :
+ @internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
+Proof. rewrite monPred_internal_eq_eq. by unseal. Qed.
+
+Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} i (a b : A) :
+ @monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
+Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
+
+Lemma monPred_equivI `{!BiInternalEq PROP'} P Q :
P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
Proof.
apply bi.equiv_spec. split.
- - apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
+ - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
- by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
- -bi.f_equiv -bi.sig_equivI !bi.discrete_fun_equivI.
+ -f_equivI -sig_equivI !discrete_fun_equivI.
Qed.
-(** Objective *)
-Global Instance internal_eq_objective {A : ofeT} (x y : A) :
+Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
@Objective I PROP (x ≡ y).
-Proof. intros ??. by unseal. Qed.
-
-Global Instance later_objective P `{!Objective P} : Objective (â–· P).
-Proof. intros ??. unseal. by rewrite objective_at. Qed.
-Global Instance laterN_objective P `{!Objective P} n : Objective (â–·^n P).
-Proof. induction n; apply _. Qed.
-Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
-Proof. rewrite /sbi_except_0. apply _. Qed.
+Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
(** FUpd *)
Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
@@ -870,7 +867,7 @@ Definition monPred_fupd `{BiFUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = _ :=
monPred_fupd_aux.(seal_eq).
-Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd.
+Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
Proof.
split; rewrite monPred_fupd_eq.
- split=>/= i. solve_proper.
@@ -882,14 +879,14 @@ Proof.
rewrite monPred_impl_force monPred_at_pure -fupd_mask_frame_r' //.
- intros E1 E2 P Q. split=>/= i. by rewrite !monPred_at_sep /= fupd_frame_r.
Qed.
-Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI :=
+Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
{| bi_fupd_mixin := monPred_fupd_mixin |}.
-Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredSI.
+Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
Proof.
intros E P. split=>/= i. rewrite monPred_at_bupd monPred_fupd_eq bupd_fupd //=.
Qed.
-Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredSI.
-Proof. split. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
+Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
+Proof. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
(|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
@@ -906,7 +903,7 @@ Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. Pro
Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := monPred_plainly_aux.(unseal).
Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := monPred_plainly_aux.(seal_eq).
-Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredSI monPred_plainly.
+Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredI monPred_plainly.
Proof.
split; rewrite monPred_plainly_eq; try unseal.
- by (split=> ? /=; repeat f_equiv).
@@ -927,43 +924,53 @@ Proof.
do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
- intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
- intros P Q. split=> i. apply bi.sep_elim_l, _.
- - intros P Q. split=> i /=. rewrite (monPred_equivI P Q). f_equiv=> j.
- by rewrite prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
- intros P. split=> i /=.
rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
- intros P. split=> i /=.
rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
Qed.
-Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredSI :=
+Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
{| bi_plainly_mixin := monPred_plainly_mixin |}.
-Global Instance monPred_bi_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
- BiPlainlyExist PROP → BiPlainlyExist monPredSI.
+Global Instance monPred_bi_prop_ext
+ `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
+Proof.
+ intros P Q. split=> i /=. rewrite monPred_plainly_eq monPred_internal_eq_eq /=.
+ rewrite /bi_wand_iff monPred_equivI. f_equiv=> j. unseal.
+ by rewrite prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+Qed.
+
+Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP} `{!BiIndexBottom bot} :
+ BiPlainlyExist PROP → BiPlainlyExist monPredI.
Proof.
- split=>?/=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
+ split=> ? /=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.
Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
- BiEmbedPlainly PROP monPredSI.
-Proof. apply bi_embed_plainly_emp, _. Qed.
+ BiEmbedPlainly PROP monPredI.
+Proof.
+ split=> i. rewrite monPred_plainly_eq; unseal. apply (anti_symm _).
+ - by apply bi.forall_intro.
+ - by rewrite (bi.forall_elim inhabitant).
+Qed.
+
+Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredI.
+Proof.
+ intros P. split=> /= i.
+ rewrite monPred_at_bupd monPred_plainly_eq /= bi.forall_elim. apply bupd_plainly.
+Qed.
Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
Proof. by rewrite monPred_plainly_eq. Qed.
-Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredSI.
-Proof.
- intros P. split=> /= i.
- rewrite monPred_at_bupd monPred_at_plainly bi.forall_elim. apply bupd_plainly.
-Qed.
-
Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
-Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
+Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredI.
Proof.
split; rewrite !monPred_fupd_eq; try unseal.
- intros E P. split=>/= i.
@@ -988,4 +995,4 @@ Global Instance monPred_objectively_plain `{BiPlainly PROP} P : Plain P → Plai
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
Global Instance monPred_subjectively_plain `{BiPlainly PROP} P : Plain P → Plain (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
-End sbi_facts.
+End bi_facts.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 093b731bd444200e23b37944c9da484cb3207129..f99e4b68a5c74ec6909a8ca971caa2ca2f27a72e 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import derived_laws_sbi big_op.
+From iris.bi Require Import derived_laws_sbi big_op internal_eq.
From iris.algebra Require Import monoid.
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
@@ -8,7 +8,7 @@ Instance: Params (@plainly) 2 := {}.
Notation "â– P" := (plainly P) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *)
-Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
+Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
bi_plainly_mixin_plainly_mono (P Q : PROP) : (P ⊢ Q) → ■P ⊢ ■Q;
@@ -29,13 +29,11 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_emp_intro (P : PROP) : P ⊢ ■emp;
bi_plainly_mixin_plainly_absorb (P Q : PROP) : ■P ∗ Q ⊢ ■P;
- bi_plainly_mixin_prop_ext_2 (P Q : PROP) : ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
-
bi_plainly_mixin_later_plainly_1 (P : PROP) : ▷ ■P ⊢ ■▷ P;
bi_plainly_mixin_later_plainly_2 (P : PROP) : ■▷ P ⊢ ▷ ■P;
}.
-Class BiPlainly (PROP : sbi) := {
+Class BiPlainly (PROP : bi) := {
bi_plainly_plainly :> Plainly PROP;
bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
}.
@@ -50,6 +48,13 @@ Arguments BiPlainlyExist _ {_}.
Arguments plainly_exist_1 _ {_ _} _.
Hint Mode BiPlainlyExist ! - : typeclass_instances.
+Class BiPropExt `{!BiPlainly PROP, !BiInternalEq PROP} :=
+ prop_ext_2 (P Q : PROP) : ■(P ∗-∗ Q) ⊢ P ≡ Q.
+Arguments BiPropExt : clear implicits.
+Arguments BiPropExt _ {_ _}.
+Arguments prop_ext_2 _ {_ _ _} _.
+Hint Mode BiPropExt ! - - : typeclass_instances.
+
Section plainly_laws.
Context `{BiPlainly PROP}.
Implicit Types P Q : PROP.
@@ -74,9 +79,6 @@ Section plainly_laws.
Lemma plainly_emp_intro P : P ⊢ ■emp.
Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.
- Lemma prop_ext_2 P Q : ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
- Proof. eapply bi_plainly_mixin_prop_ext_2, bi_plainly_mixin. Qed.
-
Lemma later_plainly_1 P : ▷ ■P ⊢ ■(▷ P).
Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
Lemma later_plainly_2 P : ■▷ P ⊢ ▷ ■P.
@@ -540,50 +542,62 @@ Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP)
Proof. rewrite big_opMS_eq. apply _. Qed.
(* Interaction with equality *)
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■(a ≡ b) ⊣⊢@{PROP} a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite plainly_elim. }
- apply (internal_eq_rewrite' a b (λ b, ■(a ≡ b))%I); [solve_proper|done|].
- rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
-Qed.
+Section internal_eq.
+ Context `{!BiInternalEq PROP}.
-Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■(P ∗-∗ Q).
-Proof.
- apply (anti_symm (⊢)); last exact: prop_ext_2.
- apply (internal_eq_rewrite' P Q (λ Q, ■(P ∗-∗ Q))%I);
- [ solve_proper | done | ].
- rewrite (plainly_emp_intro (P ≡ Q)%I).
- apply plainly_mono, wand_iff_refl.
-Qed.
+ Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■(a ≡ b) ⊣⊢@{PROP} a ≡ b.
+ Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite plainly_elim. }
+ apply (internal_eq_rewrite' a b (λ b, ■(a ≡ b))%I); [solve_proper|done|].
+ rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+ Qed.
-Lemma plainly_alt P : ■P ⊣⊢ <affine> P ≡ emp.
-Proof.
- rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
- - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
- + by rewrite affinely_elim_emp left_id.
- + by rewrite left_id.
- - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
- by rewrite -plainly_True_emp plainly_pure True_impl.
-Qed.
+ Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+ Plain (PROP:=PROP) (a ≡ b).
+ Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+End internal_eq.
-Lemma plainly_alt_absorbing P `{!Absorbing P} : ■P ⊣⊢ P ≡ True.
-Proof.
- apply (anti_symm (⊢)).
- - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
- - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
- by rewrite plainly_pure True_impl.
-Qed.
+Section prop_ext.
+ Context `{!BiInternalEq PROP, !BiPropExt PROP}.
-Lemma plainly_True_alt P : ■(True -∗ P) ⊣⊢ P ≡ True.
-Proof.
- apply (anti_symm (⊢)).
- - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
- by rewrite wand_elim_r.
- - rewrite internal_eq_sym (internal_eq_rewrite _ _
- (λ Q, ■(True -∗ Q))%I ltac:(shelve)); last solve_proper.
- by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
-Qed.
+ Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■(P ∗-∗ Q).
+ Proof.
+ apply (anti_symm (⊢)); last exact: prop_ext_2.
+ apply (internal_eq_rewrite' P Q (λ Q, ■(P ∗-∗ Q))%I);
+ [ solve_proper | done | ].
+ rewrite (plainly_emp_intro (P ≡ Q)%I).
+ apply plainly_mono, wand_iff_refl.
+ Qed.
+
+ Lemma plainly_alt P : ■P ⊣⊢ <affine> P ≡ emp.
+ Proof.
+ rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
+ - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+ + by rewrite affinely_elim_emp left_id.
+ + by rewrite left_id.
+ - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+ by rewrite -plainly_True_emp plainly_pure True_impl.
+ Qed.
+
+ Lemma plainly_alt_absorbing P `{!Absorbing P} : ■P ⊣⊢ P ≡ True.
+ Proof.
+ apply (anti_symm (⊢)).
+ - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+ - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+ by rewrite plainly_pure True_impl.
+ Qed.
+
+ Lemma plainly_True_alt P : ■(True -∗ P) ⊣⊢ P ≡ True.
+ Proof.
+ apply (anti_symm (⊢)).
+ - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+ by rewrite wand_elim_r.
+ - rewrite internal_eq_sym (internal_eq_rewrite _ _
+ (λ Q, ■(True -∗ Q))%I ltac:(shelve)); last solve_proper.
+ by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
+ Qed.
+End prop_ext.
(* Interaction with â–· *)
Lemma later_plainly P : ▷ ■P ⊣⊢ ■▷ P.
@@ -597,26 +611,22 @@ Lemma laterN_plainly_if n p P : ▷^n ■?p P ⊣⊢ ■?p (▷^n P).
Proof. destruct p; simpl; auto using laterN_plainly. Qed.
Lemma except_0_plainly_1 P : ◇ ■P ⊢ ■◇ P.
-Proof. by rewrite /sbi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
+Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■P ⊣⊢ ■◇ P.
-Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed.
-
-Global Instance internal_eq_plain {A : ofeT} (a b : A) :
- Plain (PROP:=PROP) (a ≡ b).
-Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
Global Instance later_plain P : Plain P → Plain (▷ P).
Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
Proof. induction n; apply _. Qed.
Global Instance except_0_plain P : Plain P → Plain (◇ P).
-Proof. rewrite /sbi_except_0; apply _. Qed.
+Proof. rewrite /bi_except_0; apply _. Qed.
Global Instance plainly_timeless P `{!BiPlainlyExist PROP} :
Timeless P → Timeless (■P).
Proof.
- intros. rewrite /Timeless /sbi_except_0 later_plainly_1.
- by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim.
+ intros. rewrite /Timeless /bi_except_0 later_plainly_1.
+ by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
Qed.
End plainly_derived.
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index 5a9051edff2da7bbd2a7912899d3a6a6dd0d33b0..9c934356e8bc22395c07ca0f04e9c323fc965e96 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -20,7 +20,7 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
(at level 200, x binder, y binder, right associativity,
format "∀.. x .. y , P") : bi_scope.
-Section telescopes_bi.
+Section telescopes.
Context {PROP : bi} {TT : tele}.
Implicit Types Ψ : TT → PROP.
@@ -84,11 +84,6 @@ Section telescopes_bi.
Global Instance bi_texist_persistent Ψ :
(∀ x, Persistent (Ψ x)) → Persistent (∃.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
-End telescopes_bi.
-
-Section telescopes_sbi.
- Context {PROP : sbi} {TT : tele}.
- Implicit Types Ψ : TT → PROP.
Global Instance bi_tforall_timeless Ψ :
(∀ x, Timeless (Ψ x)) → Timeless (∀.. x, Ψ x).
@@ -97,4 +92,4 @@ Section telescopes_sbi.
Global Instance bi_texist_timeless Ψ :
(∀ x, Timeless (Ψ x)) → Timeless (∃.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
-End telescopes_sbi.
+End telescopes.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 949ca07ed3d221d9307ca7057f235d4c74c24752..7b2498dafe59a76bb95e473b08da7b811b664722 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -46,7 +46,7 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
}.
-Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
+Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
@@ -64,18 +64,18 @@ Class BiBUpd (PROP : bi) := {
Hint Mode BiBUpd ! : typeclass_instances.
Arguments bi_bupd_bupd : simpl never.
-Class BiFUpd (PROP : sbi) := {
+Class BiFUpd (PROP : bi) := {
bi_fupd_fupd :> FUpd PROP;
bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
Hint Mode BiFUpd ! : typeclass_instances.
Arguments bi_fupd_fupd : simpl never.
-Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
+Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
-Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
+Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
bupd_plainly (P : PROP) : (|==> ■P) -∗ P.
Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
@@ -83,7 +83,7 @@ Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
only make sense for affine logics. From the axioms below, one could derive
[■P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
[True ={E}=∗ emp]. *)
-Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
+Class BiFUpdPlainly (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
(** When proving a fancy update of a plain proposition, you can also prove it
while being allowed to open all invariants. *)
fupd_plainly_mask_empty E (P : PROP) :
@@ -180,20 +180,15 @@ Section bupd_derived.
Lemma big_sepMS_bupd `{Countable A} (Φ : A → PROP) l :
([∗ mset] x ∈ l, |==> Φ x) ⊢ |==> [∗ mset] x ∈ l, Φ x.
Proof. by rewrite (big_opMS_commute _). Qed.
-End bupd_derived.
-
-Section bupd_derived_sbi.
- Context {PROP : sbi} `{BiBUpd PROP}.
- Implicit Types P Q R : PROP.
Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
Proof.
- rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
+ rewrite /bi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
by rewrite -bupd_intro -or_intro_l.
Qed.
Section bupd_plainly.
- Context `{BiBUpdPlainly PROP}.
+ Context `{!BiPlainly PROP, !BiBUpdPlainly PROP}.
Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
@@ -207,7 +202,7 @@ Section bupd_derived_sbi.
by rewrite (forall_elim x) bupd_plain.
Qed.
End bupd_plainly.
-End bupd_derived_sbi.
+End bupd_derived.
Section fupd_derived.
Context `{BiFUpd PROP}.
@@ -404,7 +399,7 @@ Section fupd_derived.
Qed.
Section fupd_plainly_derived.
- Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.
+ Context `{!BiPlainly PROP, !BiFUpdPlainly PROP}.
Lemma fupd_plainly_mask E E' P : (|={E,E'}=> ■P) ⊢ |={E}=> P.
Proof.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index debfbfa98da9e6cb8815fc0cd1dcfb95e9136263..3e40fc8dcb29cd5855821f6a53570e7388984d46 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Import bi.
Section sbi_instances.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types P Q R : PROP.
(** FromAssumption *)
@@ -37,7 +37,7 @@ Proof.
Qed.
(** FromPure *)
-Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
+Global Instance from_pure_internal_eq `{!BiInternalEq PROP} {A : ofeT} (a b : A) :
@FromPure PROP false (a ≡ b) (a ≡ b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
Global Instance from_pure_later a P φ : FromPure a P φ → FromPure a (▷ P) φ.
@@ -56,7 +56,7 @@ Global Instance from_pure_plainly `{BiPlainly PROP} P φ :
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
(** IntoPure *)
-Global Instance into_pure_eq {A : ofeT} (a b : A) :
+Global Instance into_pure_eq `{!BiInternalEq PROP} {A : ofeT} (a b : A) :
Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
@@ -203,7 +203,7 @@ Global Instance into_sep_affinely_later `{!Timeless (PROP:=PROP) emp} P Q1 Q2 :
Proof.
rewrite /IntoSep /= => -> ??.
rewrite -{1}(affine_affinely Q1) -{1}(affine_affinely Q2) later_sep !later_affinely_1.
- rewrite -except_0_sep /sbi_except_0 affinely_or. apply or_elim, affinely_elim.
+ rewrite -except_0_sep /bi_except_0 affinely_or. apply or_elim, affinely_elim.
rewrite -(idemp bi_and (<affine> â–· False)%I) persistent_and_sep_1.
by rewrite -(False_elim Q1) -(False_elim Q2).
Qed.
@@ -354,7 +354,7 @@ Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 (â–· P).
Proof. by rewrite /IsExcept0 except_0_later. Qed.
-Global Instance is_except_0_embed `{SbiEmbed PROP PROP'} P :
+Global Instance is_except_0_embed `{BiEmbedLater PROP PROP'} P :
IsExcept0 P → IsExcept0 ⎡P⎤.
Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
Global Instance is_except_0_bupd `{BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P).
@@ -373,7 +373,7 @@ Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_laterN n P :
FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_Next {A : ofeT} (x y : A) :
+Global Instance from_modal_Next `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
(▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
Proof. by rewrite /FromModal /= later_equivI. Qed.
@@ -385,7 +385,7 @@ Global Instance from_modal_fupd E P `{BiFUpd PROP} :
FromModal modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.
-Global Instance from_modal_later_embed `{SbiEmbed PROP PROP'} `(sel : A) n P Q :
+Global Instance from_modal_later_embed `{BiEmbedLater PROP PROP'} `(sel : A) n P Q :
FromModal (modality_laterN n) sel P Q →
FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
@@ -394,35 +394,40 @@ Global Instance from_modal_plainly `{BiPlainly PROP} P :
FromModal modality_plainly (â– P) (â– P) P | 2.
Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
- BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
+Global Instance from_modal_plainly_embed `{!BiPlainly PROP, !BiPlainly PROP',
+ !BiEmbed PROP PROP', !BiEmbedPlainly PROP PROP'} `(sel : A) P Q :
FromModal modality_plainly sel P Q →
FromModal (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
(** IntoInternalEq *)
-Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
- @IntoInternalEq PROP A (x ≡ y) x y.
-Proof. by rewrite /IntoInternalEq. Qed.
-Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (□ P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (■P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
-Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-Global Instance into_internal_eq_embed
- `{SbiEmbed PROP PROP'} {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
+Section internal_eq.
+ Context `{!BiInternalEq PROP}.
+
+ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+ @IntoInternalEq PROP _ A (x ≡ y) x y.
+ Proof. by rewrite /IntoInternalEq. Qed.
+ Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
+ Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
+ Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
+ Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (■P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
+ Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+ Global Instance into_internal_eq_embed
+ `{!BiInternalEq PROP', BiEmbedInternalEq PROP PROP'}
+ {A : ofeT} (x y : A) (P : PROP) :
+ IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
+End internal_eq.
(** IntoExcept0 *)
Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
@@ -447,7 +452,7 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
Global Instance into_except_0_persistently P Q :
IntoExcept0 P Q → IntoExcept0 (<pers> P) (<pers> Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
-Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q :
+Global Instance into_except_0_embed `{BiEmbedLater PROP PROP'} P Q :
IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
@@ -572,7 +577,8 @@ Proof.
move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
Qed.
-Global Instance into_laterN_Next {A : ofeT} only_head n n' (x y : A) :
+Global Instance into_laterN_Next `{!BiInternalEq PROP}
+ {A : ofeT} only_head n n' (x y : A) :
NatCancel n 1 n' 0 →
IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
@@ -625,7 +631,7 @@ Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed
Global Instance into_later_persistently n P Q :
IntoLaterN false n P Q → IntoLaterN false n (<pers> P) (<pers> Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
-Global Instance into_later_embed`{SbiEmbed PROP PROP'} n P Q :
+Global Instance into_later_embed`{BiEmbedLater PROP PROP'} n P Q :
IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index daa46a7c92e584bb89591f89fef3df1c9e27cd85..01a9ae7382d77306b80a115f510de73d8f084ded 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -79,11 +79,11 @@ Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _ _) =>
notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
-Class IntoInternalEq {PROP : sbi} {A : ofeT} (P : PROP) (x y : A) :=
+Class IntoInternalEq `{BiInternalEq PROP} {A : ofeT} (P : PROP) (x y : A) :=
into_internal_eq : P ⊢ x ≡ y.
-Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
-Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
-Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
+Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
+Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
+Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
into_persistent : <pers>?p P ⊢ <pers> Q.
@@ -222,7 +222,7 @@ Arguments FromForall {_ _} _%I _%I : simpl never.
Arguments from_forall {_ _} _%I _%I {_}.
Hint Mode FromForall + - ! - : typeclass_instances.
-Class IsExcept0 {PROP : sbi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
+Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
Arguments IsExcept0 {_} _%I : simpl never.
Arguments is_except_0 {_} _%I {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.
@@ -390,25 +390,25 @@ Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
Arguments KnownMakePersistently {_} _%I _%I.
Hint Mode KnownMakePersistently + ! - : typeclass_instances.
-Class MakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
+Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
make_laterN : ▷^n P ⊣⊢ lP.
Arguments MakeLaterN {_} _%nat _%I _%I.
Hint Mode MakeLaterN + + - - : typeclass_instances.
-Class KnownMakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
+Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
known_make_laterN :> MakeLaterN n P lP.
Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
-Class MakeExcept0 {PROP : sbi} (P Q : PROP) :=
- make_except_0 : sbi_except_0 P ⊣⊢ Q.
+Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
+ make_except_0 : ◇ P ⊣⊢ Q.
Arguments MakeExcept0 {_} _%I _%I.
Hint Mode MakeExcept0 + - - : typeclass_instances.
-Class KnownMakeExcept0 {PROP : sbi} (P Q : PROP) :=
+Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
known_make_except_0 :> MakeExcept0 P Q.
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
-Class IntoExcept0 {PROP : sbi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
+Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
Arguments IntoExcept0 {_} _%I _%I : simpl never.
Arguments into_except_0 {_} _%I _%I {_}.
Hint Mode IntoExcept0 + ! - : typeclass_instances.
@@ -448,24 +448,24 @@ Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Qed.
>>
*)
-Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
+Class MaybeIntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
maybe_into_laterN : P ⊢ ▷^n Q.
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
-Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
+Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
into_laterN :> MaybeIntoLaterN only_head n P Q.
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
-Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
+Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
MaybeIntoLaterN only_head n P P | 1000.
Proof. apply laterN_intro. Qed.
(* In the case both parameters are evars and n=0, we have to stop the
search and unify both evars immediately instead of looping using
other instances. *)
-Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
+Instance maybe_into_laterN_default_0 {PROP : bi} only_head (P : PROP) :
MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.
@@ -630,6 +630,6 @@ Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
IntoInv P N → IntoInv (tc_opaque P) N := id.
-Instance elim_inv_tc_opaque {PROP : sbi} {X} φ Pinv Pin Pout Pclose Q Q' :
+Instance elim_inv_tc_opaque {PROP : bi} {X} φ Pinv Pin Pout Pclose Q Q' :
ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q' →
ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 6b8eb48ea5bd14527b81e12758fc08832d1725d2..5159c0a588fb4c3cc6b1f517bd708063a669345c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1016,13 +1016,13 @@ Section tac_modal_intro.
End tac_modal_intro.
Section sbi_tactics.
-Context {PROP : sbi}.
+Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
(** * Rewriting *)
-Lemma tac_rewrite Δ i p Pxy d Q :
+Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy) →
∀ {A : ofeT} (x y : A) (Φ : A → PROP),
IntoInternalEq Pxy x y →
@@ -1036,7 +1036,7 @@ Proof.
destruct d; auto using internal_eq_sym.
Qed.
-Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
+Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
envs_lookup i Δ = Some (p, Pxy) →
envs_lookup j Δ = Some (q, P) →
∀ {A : ofeT} (x y : A) (Φ : A → PROP),
@@ -1092,6 +1092,7 @@ Proof.
Qed.
Lemma tac_löb Δ i Q :
+ BiLöb PROP →
env_spatial_is_nil Δ = true →
match envs_app true (Esnoc Enil i (▷ Q)%I) Δ with
| None => False
@@ -1100,7 +1101,7 @@ Lemma tac_löb Δ i Q :
envs_entails Δ Q.
Proof.
destruct (envs_app _ _ _) eqn:?; last done.
- rewrite envs_entails_eq => ? HQ.
+ rewrite envs_entails_eq => ?? HQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 1399b4c6085475d6504cb97c4f57a0250359af1e..3e909d0b158d53072819476ed7a37174a0776713 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -291,15 +291,10 @@ Proof.
rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_intuitionistically_sep_l.
rewrite persistently_elim impl_elim_r //.
Qed.
-End bi.
-
-(** SBI Framing *)
-Section sbi.
-Context {PROP : sbi}.
-Implicit Types P Q R : PROP.
-Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
- {A : ofeT} (a b : A) :
+Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
+ !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
+ p P Q (Q' : PROP') {A : ofeT} (a b : A) :
Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
@@ -344,4 +339,4 @@ Proof.
rewrite /Frame /MakeExcept0=><- <-.
by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
Qed.
-End sbi.
+End bi.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index b03db6a661c56c7bca5097e878b0d778c522d094..aabad6df9cb8e5d9855c08c923165196043f1dba 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2533,10 +2533,9 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
(* apply is sometimes confused wrt. canonical structures search.
refine should use the other unification algorithm, which should
not have this issue. *)
- first
- [notypeclasses refine (tac_löb _ IH _ _ _)
- |fail 1 "iLöb: not a step-indexed BI entailment"];
- [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
+ notypeclasses refine (tac_löb _ IH _ _ _ _);
+ [iSolveTC || fail "iLöb: no 'BiLöb' instance found"
+ |reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|pm_reduce;
lazymatch goal with
| |- False =>
@@ -2743,9 +2742,7 @@ Local Ltac iRewriteFindPred :=
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true (fun Heq =>
- first
- [eapply (tac_rewrite _ Heq _ _ lr)
- |fail 1 "iRewrite: not a step-indexed BI entailment"];
+ eapply (tac_rewrite _ Heq _ _ lr);
[pm_reflexivity ||
let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found"
@@ -3245,7 +3242,7 @@ Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
(* TODO: look for a more principled way of adding trivial hints like those
below; see the discussion in !75 for further details. *)
Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
- rewrite envs_entails_eq; apply bi.internal_eq_refl : core.
+ rewrite envs_entails_eq; apply internal_eq_refl : core.
Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL_nil' : core.
Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index 2cb4571d58079a36b9aae058a7e4025d6e73718d..f586244c6c9695aad44800aa7be34b669cc3408a 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Export classes.
Set Default Proof Using "Type".
Import bi.
-Section bi_modalities.
+Section modalities.
Context {PROP : bi}.
Lemma modality_persistently_mixin :
@@ -45,10 +45,6 @@ Section bi_modalities.
Qed.
Definition modality_embed `{BiEmbed PROP PROP'} :=
Modality _ modality_embed_mixin.
-End bi_modalities.
-
-Section sbi_modalities.
- Context {PROP : sbi}.
Lemma modality_plainly_mixin `{BiPlainly PROP} :
modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
@@ -60,7 +56,7 @@ Section sbi_modalities.
Modality _ modality_plainly_mixin.
Lemma modality_laterN_mixin n :
- modality_mixin (@sbi_laterN PROP n)
+ modality_mixin (@bi_laterN PROP n)
(MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
Proof.
split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
@@ -69,4 +65,4 @@ Section sbi_modalities.
Qed.
Definition modality_laterN n :=
Modality _ (modality_laterN_mixin n).
-End sbi_modalities.
+End modalities.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 78bcee3fc53f9ffe6c542d1b8838b6d02864eac9..97dfa462f733ea953c1b89190e2f1bd0c129dfe3 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -454,37 +454,6 @@ Qed.
Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I → AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
-End bi.
-
-(* When P and/or Q are evars when doing typeclass search on [IntoWand
- (R i) P Q], we use [MakeMonPredAt] in order to normalize the
- result of unification. However, when they are not evars, we want to
- propagate the known information through typeclass search. Hence, we
- do not want to use [MakeMonPredAt].
-
- As a result, depending on P and Q being evars, we use a different
- version of [into_wand_monPred_at_xx_xx]. *)
-Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
- is_evar P; is_evar Q;
- eapply @into_wand_monPred_at_unknown_unknown
- : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
- eapply @into_wand_monPred_at_unknown_known
- : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
- eapply @into_wand_monPred_at_known_unknown_le
- : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
- eapply @into_wand_monPred_at_known_unknown_ge
- : typeclass_instances.
-
-Section sbi.
-Context {I : biIndex} {PROP : sbi}.
-Local Notation monPred := (monPred I PROP).
-Implicit Types P Q R : monPred.
-Implicit Types ð“Ÿ ð“ ð“¡ : PROP.
-Implicit Types φ : Prop.
-Implicit Types i j : I.
Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
(∀ i, MakeMonPredAt i P (Φ i)) →
@@ -505,8 +474,8 @@ Global Instance is_except_0_monPred_at i P :
IsExcept0 P → IsExcept0 (P i).
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
-Global Instance make_monPred_at_internal_eq {A : ofeT} (x y : A) i :
- @MakeMonPredAt I PROP i (x ≡ y) (x ≡ y).
+Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} (x y : A) i :
+ MakeMonPredAt i (x ≡ y) (x ≡ y).
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
Global Instance make_monPred_at_except_0 i P ð“ :
MakeMonPredAt i P ð“ → MakeMonPredAt i (â—‡ P)%I (â—‡ ð“ )%I.
@@ -521,7 +490,8 @@ Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P ð“Ÿ :
MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> ð“Ÿ)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
-Global Instance into_internal_eq_monPred_at {A : ofeT} (x y : A) P i :
+Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}
+ {A : ofeT} (x y : A) P i :
IntoInternalEq P x y → IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.
@@ -556,6 +526,36 @@ Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_laterN. Qed.
Global Instance frame_monPred_at_fupd `{BiFUpd PROP} E1 E2 p P ð“¡ ð“ i :
Frame p ð“¡ (|={E1,E2}=> P i) ð“ → FrameMonPredAt p i ð“¡ (|={E1,E2}=> P) ð“ .
Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_fupd. Qed.
+End bi.
+(* When P and/or Q are evars when doing typeclass search on [IntoWand
+ (R i) P Q], we use [MakeMonPredAt] in order to normalize the
+ result of unification. However, when they are not evars, we want to
+ propagate the known information through typeclass search. Hence, we
+ do not want to use [MakeMonPredAt].
+
+ As a result, depending on P and Q being evars, we use a different
+ version of [into_wand_monPred_at_xx_xx]. *)
+Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
+ is_evar P; is_evar Q;
+ eapply @into_wand_monPred_at_unknown_unknown
+ : typeclass_instances.
+Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
+ eapply @into_wand_monPred_at_unknown_known
+ : typeclass_instances.
+Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+ eapply @into_wand_monPred_at_known_unknown_le
+ : typeclass_instances.
+Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+ eapply @into_wand_monPred_at_known_unknown_ge
+ : typeclass_instances.
+
+Section modal.
+Context {I : biIndex} {PROP : bi}.
+Local Notation monPred := (monPred I PROP).
+Implicit Types P Q R : monPred.
+Implicit Types ð“Ÿ ð“ ð“¡ : PROP.
+Implicit Types φ : Prop.
+Implicit Types i j : I.
Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ p p' E1 E2 E3 ð“Ÿ ð“Ÿ' Q Q' i :
ElimModal φ p p' ð“Ÿ ð“Ÿ' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
@@ -567,10 +567,10 @@ Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P ð“Ÿ ð“Ÿ'
ElimModal φ p p' ((|={E1,E2}=> P) i) ð“Ÿ' ð“ ð“ '.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
-Global Instance elim_acc_at_None `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' P P'x V:
+Global Instance elim_acc_at_None `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' P P'x i :
(∀ x, MakeEmbed (α x) (α' x)) → (∀ x, MakeEmbed (β x) (β' x)) →
ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x →
- ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P V) (λ x, P'x x V).
+ ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
Proof.
rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA) "Hinner Hacc".
iApply (HEA with "[Hinner]").
@@ -578,12 +578,12 @@ Proof.
- iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
rewrite -Hα -Hβ. iFrame. iIntros (? _) "Hβ". by iApply "Hclose".
Qed.
-Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' γ γ' P P'x V:
+Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
(∀ x, MakeEmbed (α x) (α' x)) →
(∀ x, MakeEmbed (β x) (β' x)) →
(∀ x, MakeEmbed (γ x) (γ' x)) →
ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x →
- ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P V) (λ x, P'x x V).
+ ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
Proof.
rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA) "Hinner Hacc".
iApply (HEA with "[Hinner]").
@@ -599,9 +599,9 @@ Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
(* This hard-codes the fact that ElimInv with_close returns a
[(λ _, ...)] as Q'. *)
Global Instance elim_inv_embed_with_close {X : Type} φ
- ð“Ÿinv ð“Ÿin (ð“Ÿout ð“Ÿclose : X → PROP)
- Pin (Pout Pclose : X → monPred)
- Q Q' :
+ ð“Ÿinv ð“Ÿin (ð“Ÿout ð“Ÿclose : X → PROP)
+ Pin (Pout Pclose : X → monPred)
+ Q Q' :
(∀ i, ElimInv φ ð“Ÿinv ð“Ÿin ð“Ÿout (Some ð“Ÿclose) (Q i) (λ _, Q' i)) →
MakeEmbed ð“Ÿin Pin → (∀ x, MakeEmbed (ð“Ÿout x) (Pout x)) →
(∀ x, MakeEmbed (ð“Ÿclose x) (Pclose x)) →
@@ -609,16 +609,18 @@ Global Instance elim_inv_embed_with_close {X : Type} φ
Proof.
rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
- iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
+ iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?".
+ by iApply "HQ'".
Qed.
Global Instance elim_inv_embed_without_close {X : Type}
- φ ð“Ÿinv ð“Ÿin (ð“Ÿout : X → PROP) Pin (Pout : X → monPred) Q (Q' : X → monPred) :
+ φ ð“Ÿinv ð“Ÿin (ð“Ÿout : X → PROP) Pin (Pout : X → monPred) Q (Q' : X → monPred) :
(∀ i, ElimInv φ ð“Ÿinv ð“Ÿin ð“Ÿout None (Q i) (λ x, Q' x i)) →
MakeEmbed ð“Ÿin Pin → (∀ x, MakeEmbed (ð“Ÿout x) (Pout x)) →
ElimInv (X:=X) φ ⎡ð“Ÿinv⎤ Pin Pout None Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <-Hout ?. iStartProof PROP.
setoid_rewrite <-Hout.
- iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
+ iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?".
+ by iApply "HQ'".
Qed.
-End sbi.
+End modal.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 6ce3ffd9c6f798cb1d1daad4be072d3afa1fb945..b5af9b8183374a1f64cfce6f11768c1d361c3cd2 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -34,7 +34,7 @@ Declare Reduction pm_prettify := cbn [
tele_fold tele_bind tele_app
(* BI connectives *)
bi_persistently_if bi_affinely_if bi_absorbingly_if bi_intuitionistically_if
- bi_wandM sbi_laterN
+ bi_wandM bi_laterN
bi_tforall bi_texist
].
Ltac pm_prettify :=
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index d613e3f0ec9e4095a1094c005620d3566bb94757..a12d22cc42e094c91fe7d633a86fb45d7eb18b2c 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -84,21 +84,13 @@ Proof.
done.
Qed.
-Lemma siProp_sbi_mixin : SbiMixin
- siProp_entails siProp_pure siProp_or siProp_impl
- (@siProp_forall) (@siProp_exist) siProp_sep
- siProp_persistently (@siProp_internal_eq) siProp_later.
+Lemma siProp_bi_later_mixin :
+ BiLaterMixin
+ siProp_entails siProp_pure siProp_or siProp_impl
+ (@siProp_forall) (@siProp_exist) siProp_sep siProp_persistently siProp_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.
+ - apply contractive_ne, later_contractive.
- exact: later_mono.
- exact: later_intro.
- exact: @later_forall_2.
@@ -120,12 +112,28 @@ Proof.
Qed.
Canonical Structure siPropI : bi :=
- {| bi_ofe_mixin := ofe_mixin_of siProp; bi_bi_mixin := siProp_bi_mixin |}.
-Canonical Structure siPropSI : sbi :=
- {| sbi_ofe_mixin := ofe_mixin_of siProp;
- sbi_bi_mixin := siProp_bi_mixin; sbi_sbi_mixin := siProp_sbi_mixin |}.
+ {| bi_ofe_mixin := ofe_mixin_of siProp;
+ bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
+
+Instance siProp_later_contractive : Contractive (bi_later (PROP:=siPropI)).
+Proof. apply later_contractive. Qed.
+
+Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
+Proof.
+ split.
+ - 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.
+Qed.
+Global Instance siProp_internal_eq : BiInternalEq siPropI :=
+ {| bi_internal_eq_mixin := siProp_internal_eq_mixin |}.
-Lemma siProp_plainly_mixin : BiPlainlyMixin siPropSI siProp_plainly.
+Lemma siProp_plainly_mixin : BiPlainlyMixin siPropI siProp_plainly.
Proof.
split; try done.
- solve_proper.
@@ -133,12 +141,13 @@ Proof.
intros P. by apply pure_intro.
- (* ■P ∗ Q ⊢ ■P *)
intros P Q. apply and_elim_l.
- - (* ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
- intros P Q. apply prop_ext_2.
Qed.
-Global Instance siProp_plainlyC : BiPlainly siPropSI :=
+Global Instance siProp_plainlyC : BiPlainly siPropI :=
{| bi_plainly_mixin := siProp_plainly_mixin |}.
+Global Instance siProp_prop_ext : BiPropExt siPropI.
+Proof. exact: prop_ext_2. Qed.
+
(** extra BI instances *)
Global Instance siProp_affine : BiAffine siPropI | 0.
@@ -152,7 +161,7 @@ Proof. done. Qed.
Global Instance siProp_persistent (P : siProp) : Persistent P.
Proof. done. Qed.
-Global Instance siProp_plainly_exist_1 : BiPlainlyExist siPropSI.
+Global Instance siProp_plainly_exist_1 : BiPlainlyExist siPropI.
Proof. done. Qed.
(** Re-state/export soundness lemmas *)