diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index b22f2edf5bdfcdf81aa9a7362a9e218f9d555c5c..3275844a0cda383b53fd34509226e741202bde27 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_bi"
: string
The command has indeed failed with message:
-Tactic failure: iLöb: not a step-indexed BI entailment.
+Tactic failure: iLöb: Löb induction not supported for this BI.
"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..9670b934acc1be71146bbb1ee6563768f78632e2 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.
@@ -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).
@@ -822,7 +822,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 +860,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 P :
⊢@{PROP}
P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧
((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧
@@ -870,7 +870,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 +944,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 +1127,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_bi".
+Lemma iLöb_no_bi 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..24a606a68457ad34ec06a37a7f396d756e56ef37 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,9 +18,9 @@ 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.
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/base_logic/bi.v b/theories/base_logic/bi.v
index 713caba78c85c41685b4bc3b9e152700c8763bad..b225064adfb925681e100a8515a40e4b9bd19995 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -72,7 +72,7 @@ Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
uPred_persistently (@uPred_internal_eq M) uPred_later.
Proof.
split.
- - exact: later_contractive.
+ - apply contractive_ne, later_contractive.
- exact: internal_eq_ne.
- exact: @internal_eq_refl.
- exact: @internal_eq_rewrite.
@@ -93,12 +93,13 @@ 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_sbi_mixin := uPred_sbi_mixin M |}.
-Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Instance uPred_later_contractive {M} : Contractive (bi_later (PROP:=uPredI M)).
+Proof. apply later_contractive. Qed.
+
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly.
Proof.
split.
- exact: plainly_ne.
@@ -123,7 +124,7 @@ Proof.
- exact: later_plainly_1.
- exact: later_plainly_2.
Qed.
-Global Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+Global Instance uPred_plainlyC M : BiPlainly (uPredI M) :=
{| bi_plainly_mixin := uPred_plainly_mixin M |}.
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
@@ -137,7 +138,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 +149,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,12 +221,10 @@ 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;
+ bi_sep, bi_wand, bi_persistently, bi_internal_eq, bi_later; simpl;
unfold plainly, bi_plainly_plainly; simpl;
uPred_primitive.unseal.
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..9566152db1e7e64eabbf0d55ecaafadbf84b460a 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 Σ.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 6bfc39ba2c23d4ee28888817a60361d584ad5a6b..f9dbb70cef7e8e1ff2ea6b62a120a1b36e2a59ab 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -122,7 +122,7 @@ Proof.
rewrite (f_equiv (λ 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/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..27aad262710264e3546b1b36b158b588791386d9 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,8 @@ 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.
+
+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..16d86917b7538c8f75bcb0b626f419b25a9d1c17 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.
@@ -19,9 +19,9 @@ 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 _.
+ Proper ((≡) ==> (≡) ==> (⊣⊢)) (@bi_internal_eq PROP A) := ne_proper_2 _.
Global Instance later_proper :
- Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_later PROP) := ne_proper _.
+ Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _.
(* Equality *)
Hint Resolve internal_eq_refl : core.
@@ -172,15 +172,16 @@ 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).
+Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
+ ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
Proof. apply (f_equiv_contractive _). Qed.
(* 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 +238,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 +253,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 +279,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 +333,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 +388,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 +418,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 +428,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 +439,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 +452,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 +470,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 :
@@ -500,64 +497,64 @@ Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
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..f2bcbd6fbfce30c40ac9a293d8db648789ef3b66 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -45,10 +45,10 @@ Class BiEmbedEmp (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
Hint Mode BiEmbedEmp ! - - : typeclass_instances.
Hint Mode BiEmbedEmp - ! - : typeclass_instances.
-Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
+Class SbiEmbed (PROP1 PROP2 : bi) `{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);
+ embed_interal_inj (PROP' : bi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
}.
Hint Mode SbiEmbed ! - - : typeclass_instances.
Hint Mode SbiEmbed - ! - : typeclass_instances.
@@ -60,14 +60,14 @@ Class BiEmbedBUpd (PROP1 PROP2 : bi)
Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
-Class BiEmbedFUpd (PROP1 PROP2 : sbi)
+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)
+Class BiEmbedPlainly (PROP1 PROP2 : bi)
`{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := {
embed_plainly_2 (P : PROP1) : ■⎡P⎤ ⊢ (⎡■P⎤ : PROP2)
}.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 845e3a33f02ebedf8d2611765609d5346c28a2ff..0560df4d0f4fb29afa94f158df431ac9bd955176 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -118,33 +118,33 @@ Section bi_mixin.
}.
Record SbiMixin := {
- sbi_mixin_later_contractive : Contractive sbi_later;
- sbi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (sbi_internal_eq A);
+ bi_mixin_later_ne : NonExpansive sbi_later;
+ bi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (sbi_internal_eq A);
(* 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) :
+ bi_mixin_internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a;
+ bi_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âŒ;
+ bi_mixin_fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
+ bi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
+ bi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ;
(* 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;
+ bi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y);
+ bi_mixin_later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y;
- sbi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
- sbi_mixin_later_intro P : P ⊢ ▷ P;
+ bi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
+ bi_mixin_later_intro P : P ⊢ ▷ P;
- sbi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
- sbi_mixin_later_exist_false {A} (Φ : A → PROP) :
+ 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);
}.
End bi_mixin.
@@ -163,13 +163,21 @@ 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_internal_eq : ∀ A : ofeT, A → A → 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_sbi_mixin : SbiMixin bi_entails bi_pure bi_or bi_impl
+ bi_forall bi_exist bi_sep
+ bi_persistently bi_internal_eq 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 +190,8 @@ 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 := {}.
+Instance: Params (@bi_internal_eq) 1 := {}.
Arguments bi_car : simpl never.
Arguments bi_dist : simpl never.
@@ -197,63 +207,8 @@ 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.
+Arguments bi_internal_eq {PROP _} _ _ : simpl never, rename.
Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
@@ -291,14 +246,14 @@ 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.
+Infix "≡" := bi_internal_eq : bi_scope.
+Infix "≡@{ A }" := (bi_internal_eq (A := A)) (only parsing) : bi_scope.
-Notation "( X ≡.)" := (sbi_internal_eq X) (only parsing) : bi_scope.
+Notation "( X ≡.)" := (bi_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 "(≡@{ A } )" := (bi_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.
@@ -423,60 +378,60 @@ Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
End bi_laws.
Section sbi_laws.
-Context {PROP : sbi}.
+Context {PROP : bi}.
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.
+Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@bi_internal_eq PROP A).
+Proof. eapply bi_mixin_internal_eq_ne, bi_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.
+Proof. eapply bi_mixin_internal_eq_refl, bi_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.
+Proof. eapply bi_mixin_internal_eq_rewrite, bi_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.
+Proof. eapply bi_mixin_fun_ext, bi_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.
+Proof. eapply bi_mixin_sig_eq, bi_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.
+Proof. eapply bi_mixin_discrete_eq_1, bi_sbi_mixin. Qed.
(* Later *)
-Global Instance later_contractive : Contractive (@sbi_later PROP).
-Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
+Global Instance later_ne : NonExpansive (@bi_later PROP).
+Proof. eapply bi_mixin_later_ne, bi_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.
+Proof. eapply bi_mixin_later_eq_1, bi_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.
+Proof. eapply bi_mixin_later_eq_2, bi_sbi_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_sbi_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_sbi_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_sbi_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_sbi_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_sbi_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_sbi_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_sbi_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_sbi_mixin. Qed.
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
-Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_false_em, bi_sbi_mixin. Qed.
End sbi_laws.
End bi.
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..16b865e4820ccf454ff477c0625ba1eb1308eb2b 100644
--- a/theories/bi/lib/relations.v
+++ b/theories/bi/lib/relations.v
@@ -4,12 +4,12 @@ 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)
+ {PROP : bi} {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) :
+ {PROP : bi} {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 {PROP : bi} {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 {PROP : bi} {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)
+ {PROP : bi} {A : ofeT} (R : A → A → PROP)
: Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
Section bi_rtc.
- Context {PROP : sbi}.
+ Context {PROP : bi}.
Context {A : ofeT}.
Context (R : A → A → PROP) `{NonExpansive2 R}.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index cbf453aac868c0b7ea9ca871ebd23ddafe6205ee..a969068bce383468d16c70945d1e5cab82230555 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}.
@@ -218,7 +218,7 @@ Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
Section Sbi.
-Context {I : biIndex} {PROP : sbi}.
+Context {I : biIndex} {PROP : bi}.
Implicit Types i : I.
Notation monPred := (monPred I PROP).
Implicit Types P Q : monPred.
@@ -245,19 +245,16 @@ Definition unseal_eqs :=
@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_internal_eq, 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,21 +307,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.
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.
- by split=> ? /=; repeat f_equiv.
- intros A P a. split=> i. by apply bi.internal_eq_refl.
- intros A a b Ψ ?. split=> i /=.
@@ -347,10 +336,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_sbi_mixin := monPred_sbi_mixin |}.
+End canonical.
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
objective_at i j : P i -∗ P j.
@@ -798,9 +787,9 @@ Proof. split. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
End bi_facts.
Section sbi_facts.
-Context {I : biIndex} {PROP : sbi}.
+Context {I : biIndex} {PROP : bi}.
Local Notation monPred := (monPred I PROP).
-Local Notation monPredSI := (monPredSI I PROP).
+Local Notation monPredI := (monPredI I PROP).
Implicit Types i : I.
Implicit Types P Q : monPred.
@@ -819,13 +808,13 @@ Proof.
by apply timeless, bi.exist_timeless.
Qed.
-Global Instance monPred_sbi_embed : SbiEmbed PROP monPredSI.
+Global Instance monPred_sbi_embed : SbiEmbed PROP monPredI.
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.
+Lemma monPred_internal_eq_unfold : @bi_internal_eq monPredI = λ A x y, ⎡ x ≡ y ⎤%I.
Proof. by unseal. Qed.
(** Unfolding lemmas *)
@@ -839,7 +828,7 @@ 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 :
+Lemma monPred_equivI {PROP' : bi} P Q :
P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
Proof.
apply bi.equiv_spec. split.
@@ -858,7 +847,7 @@ 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. rewrite /bi_except_0. apply _. Qed.
(** FUpd *)
Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
@@ -870,7 +859,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,13 +871,13 @@ 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.
+Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
Proof. split. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
@@ -906,7 +895,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).
@@ -934,11 +923,11 @@ Proof.
- 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.
+ BiPlainlyExist PROP → BiPlainlyExist monPredI.
Proof.
split=>?/=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
@@ -946,7 +935,7 @@ Proof.
Qed.
Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
- BiEmbedPlainly PROP monPredSI.
+ BiEmbedPlainly PROP monPredI.
Proof. apply bi_embed_plainly_emp, _. Qed.
Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
@@ -954,7 +943,7 @@ 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.
+Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredI.
Proof.
intros P. split=> /= i.
rewrite monPred_at_bupd monPred_at_plainly bi.forall_elim. apply bupd_plainly.
@@ -963,7 +952,7 @@ 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.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 093b731bd444200e23b37944c9da484cb3207129..e501adc71b53534a57aa29f95f9c427151a4a971 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -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;
@@ -35,7 +35,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
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;
}.
@@ -597,9 +597,9 @@ 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.
+Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
Global Instance internal_eq_plain {A : ofeT} (a b : A) :
Plain (PROP:=PROP) (a ≡ b).
@@ -610,13 +610,13 @@ 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..1b335fc46105c4c35bf29bae7c587b1d9c7906b8 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 *)
@@ -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.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index daa46a7c92e584bb89591f89fef3df1c9e27cd85..be5d9bfb215eca158a41374fe266e8deb39d5e06 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -79,7 +79,7 @@ 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 {PROP : bi} {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 {_}.
@@ -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..b41702ee9bf65d8d4a810d889246e0e061bd9cdb 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1016,7 +1016,7 @@ 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.
@@ -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..3c17872f7f1ba85685e79ea13dbfc2bded1f0aef 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -291,12 +291,6 @@ 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) :
@@ -344,4 +338,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..2604bdd673d2fde3cb8d331e8fb3161b0d789e93 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: Löb induction not supported for this BI"
+ |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"
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..feb5d5f6870555141033a7b2c8aa5629966b12c0 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)) →
@@ -506,7 +475,8 @@ Global Instance is_except_0_monPred_at i P :
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).
+ 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.
@@ -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..463c90cc62e76f47bd7d11feb89c019c7e62c7d3 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -90,7 +90,7 @@ Lemma siProp_sbi_mixin : SbiMixin
siProp_persistently (@siProp_internal_eq) siProp_later.
Proof.
split.
- - exact: later_contractive.
+ - apply contractive_ne, later_contractive.
- exact: internal_eq_ne.
- exact: @internal_eq_refl.
- exact: @internal_eq_rewrite.
@@ -120,12 +120,13 @@ 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_sbi_mixin := siProp_sbi_mixin |}.
-Lemma siProp_plainly_mixin : BiPlainlyMixin siPropSI siProp_plainly.
+Instance siProp_later_contractive : Contractive (bi_later (PROP:=siPropI)).
+Proof. apply later_contractive. Qed.
+
+Lemma siProp_plainly_mixin : BiPlainlyMixin siPropI siProp_plainly.
Proof.
split; try done.
- solve_proper.
@@ -136,7 +137,7 @@ Proof.
- (* ■((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 |}.
(** extra BI instances *)
@@ -152,7 +153,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 *)