diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.observe.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.observe.html
index 61927582..61dbd630 100644
--- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.observe.html
+++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.observe.html
@@ -315,47 +315,65 @@ bedrock.lang.bi.observe
Proof. rewrite/Observe=>->. case: b => //=. iIntros "#$". Qed.
- Lemma observe_equiv_sep_True Q P `{!Persistent Q} : (P ⊢ Q ∗ True) ↔ Observe Q P.
+ Lemma observe_alt Q P : Observe Q P ↔ (P ⊢ <absorb> □ Q).
+ Proof.
+ by rewrite /Observe -bi.absorbingly_intuitionistically_into_persistently.
+ Qed.
+
+
+ Lemma observe_alt_sep_True Q P : Observe Q P ↔ (P ⊢ □ Q ∗ True).
+ Proof. by rewrite observe_alt (comm bi_sep). Qed.
+
+
+ Lemma observe_equiv_sep_True Q P `{!Persistent Q} : (P ⊢ Q ∗ True) ↔ Observe Q P.
Proof.
by rewrite (comm bi_sep Q) /Observe bi.persistently_absorbingly.
Qed.
- Lemma observe_only_provable_impl (Q P : Prop) :
- (P -> Q) -> Observe (PROP:=PROP) [| Q |] [| P |].
+ Lemma observe_only_provable_impl (Q P : Prop) :
+ (P -> Q) -> Observe (PROP:=PROP) [| Q |] [| P |].
Proof. intros HQ. iIntros "% !> !%". exact: HQ. Qed.
- Lemma observe_2_only_provable_impl (Q P1 P2 : Prop) :
- (P1 -> P2 -> Q) -> Observe2 (PROP:=PROP) [| Q |] [| P1 |] [| P2 |].
+ Lemma observe_2_only_provable_impl (Q P1 P2 : Prop) :
+ (P1 -> P2 -> Q) -> Observe2 (PROP:=PROP) [| Q |] [| P1 |] [| P2 |].
Proof. intros HQ. iIntros "% % !> !%". exact: HQ. Qed.
- Lemma observe_2_intro_persistent Q P1 P2 `{!Persistent Q} :
- (P1 ⊢ P2 -∗ Q) → Observe2 Q P1 P2.
+ Lemma observe_2_intro_persistent Q P1 P2 `{!Persistent Q} :
+ (P1 ⊢ P2 -∗ Q) → Observe2 Q P1 P2.
Proof. rewrite/Observe2=>->. f_equiv. iIntros "#$". Qed.
- Lemma observe_2_intro_only_provable (Q : Prop) (P1 P2 : PROP) : (P1 ⊢ P2 -∗ ⌜ Q ⌝) → Observe2 [| Q |] P1 P2.
+ Lemma observe_2_intro_only_provable (Q : Prop) (P1 P2 : PROP) : (P1 ⊢ P2 -∗ ⌜ Q ⌝) → Observe2 [| Q |] P1 P2.
Proof. by rewrite /Observe2 persistently_only_provable =>->. Qed.
- Lemma observe_2_intro Q P1 P2 `{!Persistent Q} :
- (P1 ⊢ P2 -∗ P1 ∗ P2 ∗ Q) → Observe2 Q P1 P2.
+ Lemma observe_2_intro Q P1 P2 `{!Persistent Q} :
+ (P1 ⊢ P2 -∗ P1 ∗ P2 ∗ Q) → Observe2 Q P1 P2.
Proof.
rewrite/Observe2 {1}(persistent Q)=>->. f_equiv. iIntros "(_ &_ & $)".
Qed.
- Lemma observe_2_intro_intuitionistically Q P1 P2 : Observe2 Q P1 P2 → Observe2 (□ Q) P1 P2.
+ Lemma observe_2_intro_intuitionistically Q P1 P2 : Observe2 Q P1 P2 → Observe2 (□ Q) P1 P2.
Proof. rewrite/Observe2=>->. f_equiv. iIntros "#$". Qed.
- Lemma observe_2_intro_intuitionistically_if b Q P1 P2 : Observe2 Q P1 P2 → Observe2 (□?b Q) P1 P2.
+ Lemma observe_2_intro_intuitionistically_if b Q P1 P2 : Observe2 Q P1 P2 → Observe2 (□?b Q) P1 P2.
Proof. rewrite/Observe2=>->. f_equiv. case: b => //=. iIntros "#$". Qed.
- Lemma observe_2_equiv_sep_True Q P1 P2 `{!Persistent Q} : (P1 ∗ P2 ⊢ Q ∗ True) ↔ Observe2 Q P1 P2.
+ Lemma observe_2_alt Q P1 P2 : Observe2 Q P1 P2 ↔ (P1 ∗ P2 ⊢ <absorb> □ Q).
+ Proof. by rewrite observe_2_observe observe_alt. Qed.
+
+
+ Lemma observe_2_alt_sep_True Q P1 P2 : Observe2 Q P1 P2 ↔ (P1 ∗ P2 ⊢ □ Q ∗ True).
+ Proof. by rewrite observe_2_observe observe_alt_sep_True. Qed.
+
+
+ Lemma observe_2_equiv_sep_True Q P1 P2 `{!Persistent Q} : (P1 ∗ P2 ⊢ Q ∗ True) ↔ Observe2 Q P1 P2.
Proof. by rewrite observe_2_observe observe_equiv_sep_True. Qed.
End observe.
@@ -367,7 +385,7 @@ bedrock.lang.bi.observe
Section bi.
-
Context {
PROP :
bi}.
+
Context {
PROP :
bi}.
Implicit Types P Q :
PROP.
@@ -375,65 +393,65 @@
bedrock.lang.bi.observe
This instance is necessary when _defining_ observations, both by itself
and as "leaf" of searches involving
observe_sep_{l,r}.
*)
-
Global Instance observe_refl Q `{
!Persistent Q} :
Observe Q Q.
+
Global Instance observe_refl Q `{
!Persistent Q} :
Observe Q Q.
Proof.
exact:
observe_intro_persistent.
Qed.
-
Global Instance observe_exist {
A}
Q (
P :
A → PROP) :
-
(∀ x, Observe Q (
P x)
) → Observe Q (
∃ x, P x).
+
Global Instance observe_exist {
A}
Q (
P :
A → PROP) :
+
(∀ x, Observe Q (
P x)
) → Observe Q (
∃ x, P x).
Proof.
intros.
iDestruct 1
as (
x) "P".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_2_exist {
A}
Q (
P1 P2 :
A → PROP) :
-
(∀ x y, Observe2 Q (
P1 x) (
P2 y)
) → Observe2 Q (
∃ x, P1 x) (
∃ y, P2 y).
+
Global Instance observe_2_exist {
A}
Q (
P1 P2 :
A → PROP) :
+
(∀ x y, Observe2 Q (
P1 x) (
P2 y)
) → Observe2 Q (
∃ x, P1 x) (
∃ y, P2 y).
Proof.
intros.
iDestruct 1
as (
x) "P1".
iDestruct 1
as (
y) "P2".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_sep_l Q P R :
Observe Q P → Observe Q (
P ∗ R).
+
Global Instance observe_sep_l Q P R :
Observe Q P → Observe Q (
P ∗ R).
Proof.
intros.
iIntros "[P _]".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_sep_r Q P R :
Observe Q P → Observe Q (
R ∗ P).
+
Global Instance observe_sep_r Q P R :
Observe Q P → Observe Q (
R ∗ P).
Proof.
intros.
iIntros "[_ P]".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_2_sep_l Q P1 P2 R1 R2 :
-
Observe2 Q P1 P2 → Observe2 Q (
P1 ∗ R1) (
P2 ∗ R2).
+
Global Instance observe_2_sep_l Q P1 P2 R1 R2 :
+
Observe2 Q P1 P2 → Observe2 Q (
P1 ∗ R1) (
P2 ∗ R2).
Proof.
intros.
iIntros "[P1 _] [P2 _]".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_2_sep_r Q P1 P2 R1 R2 :
-
Observe2 Q P1 P2 → Observe2 Q (
R1 ∗ P1) (
R2 ∗ P2).
+
Global Instance observe_2_sep_r Q P1 P2 R1 R2 :
+
Observe2 Q P1 P2 → Observe2 Q (
R1 ∗ P1) (
R2 ∗ P2).
Proof.
intros.
iIntros "[_ P1] [_ P2]".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_and_l Q P R :
Observe Q P → Observe Q (
P ∧ R).
+
Global Instance observe_and_l Q P R :
Observe Q P → Observe Q (
P ∧ R).
Proof.
intros.
iIntros "[P _]".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_and_r Q P R :
Observe Q P → Observe Q (
R ∧ P).
+
Global Instance observe_and_r Q P R :
Observe Q P → Observe Q (
R ∧ P).
Proof.
intros.
iIntros "[_ P]".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_2_and_l Q P1 P2 R1 R2 :
-
Observe2 Q P1 P2 → Observe2 Q (
P1 ∧ R1) (
P2 ∧ R2).
+
Global Instance observe_2_and_l Q P1 P2 R1 R2 :
+
Observe2 Q P1 P2 → Observe2 Q (
P1 ∧ R1) (
P2 ∧ R2).
Proof.
intros.
iIntros "[P1 _] [P2 _]".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_2_and_r Q P1 P2 R1 R2 :
-
Observe2 Q P1 P2 → Observe2 Q (
R1 ∧ P1) (
R2 ∧ P2).
+
Global Instance observe_2_and_r Q P1 P2 R1 R2 :
+
Observe2 Q P1 P2 → Observe2 Q (
R1 ∧ P1) (
R2 ∧ P2).
Proof.
intros.
iIntros "[_ P1] [_ P2]".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_or Q P R :
-
Observe Q P → Observe Q R → Observe Q (
P ∨ R).
+
Global Instance observe_or Q P R :
+
Observe Q P → Observe Q R → Observe Q (
P ∨ R).
Proof.
intros.
iIntros "[P|R]".
by iApply (observe with "P"
).
by iApply (observe with "R"
).
Qed.
-
Global Instance observe_2_or Q P1 P2 R1 R2 :
-
Observe2 Q P1 P2 → Observe2 Q P1 R2 →
-
Observe2 Q R1 P2 → Observe2 Q R1 R2 →
-
Observe2 Q (
P1 ∨ R1) (
P2 ∨ R2).
+
Global Instance observe_2_or Q P1 P2 R1 R2 :
+
Observe2 Q P1 P2 → Observe2 Q P1 R2 →
+
Observe2 Q R1 P2 → Observe2 Q R1 R2 →
+
Observe2 Q (
P1 ∨ R1) (
P2 ∨ R2).
Proof.
intros.
iIntros "[P1|R1] [P2|R2]".
-
iApply (observe_2 with "P1 P2"
).
@@ -443,51 +461,51 @@
bedrock.lang.bi.observe
Qed.
- #[
global]
Instance observe_later Q P :
Observe Q P → Observe (
▷ Q) (
▷ P).
+ #[
global]
Instance observe_later Q P :
Observe Q P → Observe (
▷ Q) (
▷ P).
Proof.
rewrite /
Observe=>->.
by rewrite bi.later_persistently.
Qed.
- #[
global]
Instance observe_2_later Q P1 P2 :
-
Observe2 Q P1 P2 → Observe2 (
▷ Q) (
▷ P1) (
▷ P2).
+ #[
global]
Instance observe_2_later Q P1 P2 :
+
Observe2 Q P1 P2 → Observe2 (
▷ Q) (
▷ P1) (
▷ P2).
Proof.
intros.
apply observe_uncurry.
rewrite -
bi.later_sep.
by apply observe_later,
observe_curry.
Qed.
-
Global Instance observe_from_false Q :
Observe Q False.
+
Global Instance observe_from_false Q :
Observe Q False.
Proof.
iDestruct 1
as "[]".
Qed.
-
Global Instance observe_2_from_false_1 Q P :
Observe2 Q False P.
+
Global Instance observe_2_from_false_1 Q P :
Observe2 Q False P.
Proof.
iDestruct 1
as "[]".
Qed.
-
Global Instance observe_2_from_false_2 Q P :
Observe2 Q P False.
+
Global Instance observe_2_from_false_2 Q P :
Observe2 Q P False.
Proof.
iDestruct 2
as "[]".
Qed.
-
Global Instance observe_persistently Q P :
-
Observe Q P → Observe Q (
<pers> P).
+
Global Instance observe_persistently Q P :
+
Observe Q P → Observe Q (
<pers> P).
Proof.
intros.
iIntros "#P".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_2_persistently Q P1 P2 :
-
Observe2 Q P1 P2 → Observe2 Q (
<pers> P1) (
<pers> P2).
+
Global Instance observe_2_persistently Q P1 P2 :
+
Observe2 Q P1 P2 → Observe2 Q (
<pers> P1) (
<pers> P2).
Proof.
intros.
iIntros "#P1 #P2".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_intuitionistically Q P :
-
Observe Q P → Observe Q (
□ P).
+
Global Instance observe_intuitionistically Q P :
+
Observe Q P → Observe Q (
□ P).
Proof.
intros.
iIntros "#P".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_2_intuitionistically Q P1 P2 :
-
Observe2 Q P1 P2 → Observe2 Q (
□ P1) (
□ P2).
+
Global Instance observe_2_intuitionistically Q P1 P2 :
+
Observe2 Q P1 P2 → Observe2 Q (
□ P1) (
□ P2).
Proof.
intros.
iIntros "#P1 #P2".
iApply (observe_2 with "P1 P2"
).
Qed.
-
Global Instance observe_intuitionistically_if b Q P :
-
Observe Q P → Observe Q (
□?b P).
+
Global Instance observe_intuitionistically_if b Q P :
+
Observe Q P → Observe Q (
□?b P).
Proof.
intros.
case:
b => //=.
iIntros "#P".
iApply (observe with "P"
).
Qed.
-
Global Instance observe_2_intuitionistically_if b Q P1 P2 :
-
Observe2 Q P1 P2 → Observe2 Q (
□?b P1) (
□?b P2).
+
Global Instance observe_2_intuitionistically_if b Q P1 P2 :
+
Observe2 Q P1 P2 → Observe2 Q (
□?b P1) (
□?b P2).
Proof.
intros.
case:
b => //=.
iIntros "#P1 #P2".
iApply (observe_2 with "P1 P2"
).
Qed.
End bi.
Section monpred.
-
Context {
I :
biIndex} {
PROP :
bi}.
+
Context {
I :
biIndex} {
PROP :
bi}.
Implicit Types i :
I.
Implicit Types P Q : (
monPred I PROP).
@@ -498,32 +516,32 @@
bedrock.lang.bi.observe
It's not clear these should be instances.
-
Lemma monPred_observe Q P :
-
(∀ i, Observe (
Q i) (
P i)
) → Observe Q P.
+
Lemma monPred_observe Q P :
+
(∀ i, Observe (
Q i) (
P i)
) → Observe Q P.
Proof.
rewrite/
Observe=>
Hobs.
constructor=>
i.
by rewrite (
Hobs i)
monPred_at_persistently.
Qed.
-
Lemma monPred_observe_2 Q P1 P2 :
-
(∀ i, Observe2 (
Q i) (
P1 i) (
P2 i)
) → Observe2 Q P1 P2.
+
Lemma monPred_observe_2 Q P1 P2 :
+
(∀ i, Observe2 (
Q i) (
P1 i) (
P2 i)
) → Observe2 Q P1 P2.
Proof.
intros Hobs.
apply observe_uncurry,
monPred_observe=>
i.
rewrite monPred_at_sep.
by apply observe_curry.
Qed.
-
Lemma monPred_observe_only_provable (
Q :
Prop)
P
- (
Hobs :
∀ i, Observe [| Q |] (
P i)) :
-
Observe [| Q |] P.
+
Lemma monPred_observe_only_provable (
Q :
Prop)
P
+ (
Hobs :
∀ i, Observe [| Q |] (
P i)) :
+
Observe [| Q |] P.
Proof.
apply monPred_observe =>
i.
by rewrite monPred_at_only_provable.
Qed.
-
Lemma monPred_observe_2_only_provable (
Q :
Prop)
P1 P2
- (
Hobs :
∀ i, Observe2 [| Q |] (
P1 i) (
P2 i)) :
-
Observe2 [| Q |] P1 P2.
+
Lemma monPred_observe_2_only_provable (
Q :
Prop)
P1 P2
+ (
Hobs :
∀ i, Observe2 [| Q |] (
P1 i) (
P2 i)) :
+
Observe2 [| Q |] P1 P2.
Proof.
apply monPred_observe_2 =>
i.
by rewrite monPred_at_only_provable.
@@ -536,38 +554,38 @@
bedrock.lang.bi.observe
These should certainly not be instances.
-
Lemma observable_sep P Q :
observable (
P ∗ Q)
⊢ observable P ∗ observable Q.
+
Lemma observable_sep P Q :
observable (
P ∗ Q)
⊢ observable P ∗ observable Q.
Proof.
rewrite observable.unlock.
iIntros "#PQ".
diff --git a/docs/_static/coqdoc/bedrock.lang.html/indexpage.html b/docs/_static/coqdoc/bedrock.lang.html/indexpage.html
index 0a608476..d93674df 100644
--- a/docs/_static/coqdoc/bedrock.lang.html/indexpage.html
+++ b/docs/_static/coqdoc/bedrock.lang.html/indexpage.html
@@ -66,7 +66,7 @@
Z |
_ |
other |
-
(9029 entries) |
+
(9033 entries) |
| Notation Index |
@@ -226,7 +226,7 @@
Z |
_ |
other |
-(2560 entries) |
+(2564 entries) |
| Constructor Index |
@@ -5031,6 +5031,8 @@ Global Index
observe_exist [instance, in bedrock.lang.bi.observe]
observe_refl [instance, in bedrock.lang.bi.observe]
observe_2_equiv_sep_True [lemma, in bedrock.lang.bi.observe]
+observe_2_alt_sep_True [lemma, in bedrock.lang.bi.observe]
+observe_2_alt [lemma, in bedrock.lang.bi.observe]
observe_2_intro_intuitionistically_if [lemma, in bedrock.lang.bi.observe]
observe_2_intro_intuitionistically [lemma, in bedrock.lang.bi.observe]
observe_2_intro [lemma, in bedrock.lang.bi.observe]
@@ -5039,6 +5041,8 @@ Global Index
observe_2_only_provable_impl [lemma, in bedrock.lang.bi.observe]
observe_only_provable_impl [lemma, in bedrock.lang.bi.observe]
observe_equiv_sep_True [lemma, in bedrock.lang.bi.observe]
+observe_alt_sep_True [lemma, in bedrock.lang.bi.observe]
+observe_alt [lemma, in bedrock.lang.bi.observe]
observe_intro_intuitionistically_if [lemma, in bedrock.lang.bi.observe]
observe_intro_intuitionistically [lemma, in bedrock.lang.bi.observe]
observe_intro [lemma, in bedrock.lang.bi.observe]
@@ -11759,6 +11763,8 @@ Lemma Index
observe_2_monPred_at [in bedrock.lang.bi.observe]
observe_monPred_at [in bedrock.lang.bi.observe]
observe_2_equiv_sep_True [in bedrock.lang.bi.observe]
+observe_2_alt_sep_True [in bedrock.lang.bi.observe]
+observe_2_alt [in bedrock.lang.bi.observe]
observe_2_intro_intuitionistically_if [in bedrock.lang.bi.observe]
observe_2_intro_intuitionistically [in bedrock.lang.bi.observe]
observe_2_intro [in bedrock.lang.bi.observe]
@@ -11767,6 +11773,8 @@ Lemma Index
observe_2_only_provable_impl [in bedrock.lang.bi.observe]
observe_only_provable_impl [in bedrock.lang.bi.observe]
observe_equiv_sep_True [in bedrock.lang.bi.observe]
+observe_alt_sep_True [in bedrock.lang.bi.observe]
+observe_alt [in bedrock.lang.bi.observe]
observe_intro_intuitionistically_if [in bedrock.lang.bi.observe]
observe_intro_intuitionistically [in bedrock.lang.bi.observe]
observe_intro [in bedrock.lang.bi.observe]
@@ -18962,7 +18970,7 @@ Definition Index
Z |
_ |
other |
-(9029 entries) |
+(9033 entries) |
| Notation Index |
@@ -19122,7 +19130,7 @@ Definition Index
Z |
_ |
other |
-(2560 entries) |
+(2564 entries) |
| Constructor Index |