Commit 8068093d authored by Ralf Jung's avatar Ralf Jung
Browse files

make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)

parent bc1afae4
......@@ -86,7 +86,7 @@ Lemma box_own_auth_update γ b1 b2 b3 :
box_own_auth γ (E b1) box_own_auth γ (E b2)
== box_own_auth γ (E b3) box_own_auth γ (E b3).
Proof.
rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
rewrite /box_own_auth -!own_op. iApply own_update. apply prod_update; last done.
apply excl_auth_update.
Qed.
......
......@@ -217,7 +217,7 @@ Section inv_heap.
+ iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton.
Qed.
Lemma inv_mapsto_own_inv l v I : l _I v - l _I .
Lemma inv_mapsto_own_inv l v I : l _I v l _I .
Proof.
apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
right. split; [apply: ucmra_unit_least|done].
......
......@@ -213,15 +213,15 @@ Section lemmas.
Lemma ghost_map_delete {γ m k v} :
ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (delete k m).
Proof.
unseal. apply bi.wand_intro_r. rewrite -own_op.
unseal. iApply bi.wand_intro_r. rewrite -own_op.
iApply own_update. apply: gmap_view_delete.
Qed.
Lemma ghost_map_update {γ m k v} w :
ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (<[k := w]> m) k [γ] w.
Proof.
unseal. apply bi.wand_intro_r. rewrite -!own_op.
apply own_update. apply: gmap_view_update.
unseal. iApply bi.wand_intro_r. rewrite -!own_op.
iApply own_update. apply: gmap_view_update.
Qed.
(** Big-op versions of above lemmas *)
......@@ -241,8 +241,8 @@ Section lemmas.
ghost_map_auth γ 1 m ==
ghost_map_auth γ 1 (m' m) ([ map] k v m', k [γ] v).
Proof.
unseal. intros ?. rewrite -big_opM_own_1 -own_op.
apply own_update. apply: gmap_view_alloc_big; done.
unseal. intros ?. rewrite -big_opM_own_1 -own_op. iApply own_update.
apply: gmap_view_alloc_big; done.
Qed.
Lemma ghost_map_insert_persist_big {γ m} m' :
m' ## m
......
......@@ -109,7 +109,7 @@ Section gset_bij.
Lemma gset_bij_own_elem_get {γ q L} a b :
(a, b) L
gset_bij_own_auth γ q L - gset_bij_own_elem γ a b.
gset_bij_own_auth γ q L gset_bij_own_elem γ a b.
Proof.
intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
by apply own_mono, bij_view_included.
......
......@@ -88,12 +88,12 @@ Section mono_nat.
to the persistent context, for example with [iDestruct (mono_nat_lb_own_get
with "Hauth") as "#Hfrag"]. *)
Lemma mono_nat_lb_own_get γ q n :
mono_nat_auth_own γ q n - mono_nat_lb_own γ n.
mono_nat_auth_own γ q n mono_nat_lb_own γ n.
Proof. unseal. apply own_mono, mono_nat_included. Qed.
Lemma mono_nat_lb_own_le {γ n} n' :
n' n
mono_nat_lb_own γ n - mono_nat_lb_own γ n'.
mono_nat_lb_own γ n mono_nat_lb_own γ n'.
Proof. unseal. intros. by apply own_mono, mono_nat_lb_mono. Qed.
Lemma mono_nat_own_alloc n :
......
......@@ -58,7 +58,7 @@ Section proofs.
Lemma na_own_disjoint p E1 E2 : na_own p E1 - na_own p E2 - E1 ## E2.
Proof.
apply wand_intro_r.
iApply wand_intro_r.
rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
Qed.
......
From iris.algebra Require Import functions gmap proofmode_classes.
From iris.proofmode Require Import classes.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export iprop.
From iris.prelude Require Import options.
Import uPred.
......@@ -181,9 +181,9 @@ Proof. intros a1 a2. apply own_mono. Qed.
Lemma own_valid γ a : own γ a a.
Proof. by rewrite !own_eq /own_def ownM_valid iRes_singleton_validI. Qed.
Lemma own_valid_2 γ a1 a2 : own γ a1 - own γ a2 - (a1 a2).
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Proof. apply entails_wand, wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Proof. apply entails_wand. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a.
Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a a own γ a.
......@@ -194,7 +194,7 @@ Proof. rewrite !own_eq /own_def. apply _. Qed.
Global Instance own_core_persistent γ a : CoreId a Persistent (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Lemma later_own γ a : own γ a - b, own γ b (a b).
Lemma later_own γ a : own γ a b, own γ b (a b).
Proof.
rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
......@@ -261,7 +261,7 @@ Proof.
intros Hupd. rewrite !own_eq.
rewrite -(bupd_mono ( m,
a', m = iRes_singleton γ a' P a' uPred_ownM m)%I).
- apply bupd_ownM_updateP, (discrete_fun_singleton_updateP _ (λ m, x,
- apply entails_wand, bupd_ownM_updateP, (discrete_fun_singleton_updateP _ (λ m, x,
m = {[ γ := x ]} x',
x = inG_unfold x' a',
x' = cmra_transport inG_prf a' P a')); [|naive_solver].
......@@ -277,15 +277,17 @@ Qed.
Lemma own_update γ a a' : a ~~> a' own γ a == own γ a'.
Proof.
intros; rewrite (own_updateP (a' =.)); last by apply cmra_update_updateP.
apply bupd_mono, exist_elim=> a''. rewrite sep_and. apply pure_elim_l=> -> //.
intros. iIntros "?".
iMod (own_updateP (a' =.) with "[$]") as (a'') "[-> $]".
{ by apply cmra_update_updateP. }
done.
Qed.
Lemma own_update_2 γ a1 a2 a' :
a1 a2 ~~> a' own γ a1 - own γ a2 == own γ a'.
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
Proof. intros. apply entails_wand, wand_intro_r. rewrite -own_op. by iApply own_update. Qed.
Lemma own_update_3 γ a1 a2 a3 a' :
a1 a2 a3 ~~> a' own γ a1 - own γ a2 - own γ a3 == own γ a'.
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
Proof. intros. apply entails_wand. do 2 apply wand_intro_r. rewrite -!own_op. by iApply own_update. Qed.
End global.
Global Arguments own_valid {_ _} [_] _ _.
......
This diff is collapsed.
......@@ -519,7 +519,7 @@ Qed.
Lemma and_parallel P1 P2 Q1 Q2 :
(P1 P2) - ((P1 - Q1) (P2 - Q2)) - Q1 Q2.
Proof.
apply wand_intro_r, and_intro.
apply entails_wand, wand_intro_r, and_intro.
- rewrite !and_elim_l wand_elim_r. done.
- rewrite !and_elim_r wand_elim_r. done.
Qed.
......
......@@ -242,20 +242,6 @@ Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.
Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
Notation "'(⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
Notation "P '⊣⊢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
Notation "'(⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
Notation "( P ⊣⊢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
Notation "(.⊣⊢ Q )" := (λ P, P @{bi_car _} Q) (only parsing) : stdpp_scope.
Notation "P -∗ Q" := (P Q) : stdpp_scope.
Notation "'emp'" := (bi_emp) : bi_scope.
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
Notation "'True'" := (bi_pure True) : bi_scope.
......@@ -277,6 +263,18 @@ Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Notation "▷ P" := (bi_later P) : bi_scope.
Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
Notation "'(⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
Notation "P '⊣⊢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
Notation "'(⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
Notation "( P ⊣⊢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
Notation "(.⊣⊢ Q )" := (λ P, P @{bi_car _} Q) (only parsing) : stdpp_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp P.
Global Arguments bi_emp_valid {_} _%I : simpl never.
......@@ -289,6 +287,8 @@ Notation "'(⊢@{' PROP } Q )" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing)
Notation "(.⊢ Q )" := (λ P, P Q) (only parsing) : stdpp_scope.
Notation "( P ⊢.)" := (bi_entails P) (only parsing) : stdpp_scope.
Notation "P -∗ Q" := ( P - Q) : stdpp_scope.
Module bi.
Section bi_laws.
Context {PROP : bi}.
......
......@@ -273,8 +273,8 @@ Section lemmas.
Lemma aupd_intro P Q α β Eo Ei Φ :
Affine P Persistent P Laterable Q
(P Q - atomic_acc Eo Ei α Q β Φ)
P Q - atomic_update Eo Ei α β Φ.
(P Q atomic_acc Eo Ei α Q β Φ)
P Q atomic_update Eo Ei α β Φ.
Proof.
rewrite atomic_update_eq {1}/atomic_update_def /=.
iIntros (??? HAU) "[#HP HQ]".
......@@ -450,7 +450,7 @@ Section proof_mode.
Proof. by rewrite /FromModal. Qed.
Local Lemma make_laterable_id_elim P :
make_laterable_id P - P.
make_laterable_id P P.
Proof. rewrite make_laterable_id_eq. done. Qed.
Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
......
......@@ -41,16 +41,19 @@ Section fractional.
Lemma fractional_split_1 P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
P - P1 P2.
Proof. intros. by rewrite -(fractional_split P). Qed.
Proof. intros. apply bi.entails_wand. by rewrite -(fractional_split P). Qed.
Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
P1 - P2 - P.
Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
AsFractional P1 Φ q1 AsFractional P2 Φ q2
P1 - P2 - Φ (q1 + q2)%Qp.
Proof. move=>-[-> _] [-> _]. rewrite fractional. apply bi.wand_intro_r. done. Qed.
Proof.
move=>-[-> _] [-> _]. rewrite fractional.
apply bi.entails_wand, bi.wand_intro_r. done.
Qed.
Lemma fractional_half P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2)
......@@ -59,11 +62,11 @@ Section fractional.
Lemma fractional_half_1 P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2)
P - P12 P12.
Proof. intros. by rewrite -(fractional_half P). Qed.
Proof. intros. apply bi.entails_wand. by rewrite -(fractional_half P). Qed.
Lemma fractional_half_2 P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2)
P12 - P12 - P.
Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
(** Fractional and logical connectives *)
Global Instance persistent_fractional (P : PROP) :
......
......@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
(** The class of laterable assertions *)
Class Laterable {PROP : bi} (P : PROP) := laterable :
P - Q, Q ( Q - P).
P Q, Q ( Q - P).
Global Arguments Laterable {_} _%I : simpl never.
Global Arguments laterable {_} _%I {_}.
Global Hint Mode Laterable + ! : typeclass_instances.
......@@ -115,14 +115,14 @@ Section instances.
Proof. by intros ->. Qed.
Lemma make_laterable_except_0 Q :
make_laterable ( Q) - make_laterable Q.
make_laterable ( Q) make_laterable Q.
Proof.
iIntros "(%P & HP & #HPQ)". iExists P. iFrame.
iIntros "!# HP". iMod ("HPQ" with "HP"). done.
Qed.
Lemma make_laterable_sep Q1 Q2 :
make_laterable Q1 make_laterable Q2 - make_laterable (Q1 Q2).
make_laterable Q1 make_laterable Q2 make_laterable (Q1 Q2).
Proof.
iIntros "[HQ1 HQ2]".
iDestruct "HQ1" as (P1) "[HP1 #HQ1]".
......@@ -137,7 +137,7 @@ Section instances.
resources. We cannot keep arbitrary resources since that would let us "frame
in" non-laterable things. *)
Lemma make_laterable_wand Q1 Q2 :
make_laterable (Q1 - Q2) - (make_laterable Q1 - make_laterable Q2).
make_laterable (Q1 - Q2) (make_laterable Q1 - make_laterable Q2).
Proof.
iIntros "HQ HQ1".
iDestruct (make_laterable_sep with "[$HQ $HQ1 //]") as "HQ".
......@@ -148,7 +148,7 @@ Section instances.
(** A variant of the above for keeping arbitrary intuitionistic resources.
Sadly, this is not implied by the above for non-affine BIs. *)
Lemma make_laterable_intuitionistic_wand Q1 Q2 :
(Q1 - Q2) - (make_laterable Q1 - make_laterable Q2).
(Q1 - Q2) (make_laterable Q1 - make_laterable Q2).
Proof.
iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
iExists P. iFrame. iIntros "!> HP".
......@@ -164,7 +164,7 @@ Section instances.
Qed.
Lemma make_laterable_elim Q :
make_laterable Q - Q.
make_laterable Q Q.
Proof.
iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
Qed.
......@@ -183,7 +183,7 @@ Section instances.
Qed.
Lemma make_laterable_intro' Q :
Laterable Q
Q - make_laterable Q.
Q make_laterable Q.
Proof.
intros ?. iApply make_laterable_intro. iIntros "!# $".
Qed.
......@@ -199,7 +199,7 @@ Section instances.
Qed.
Lemma laterable_alt Q :
Laterable Q (Q - make_laterable Q).
Laterable Q (Q make_laterable Q).
Proof.
split.
- intros ?. apply make_laterable_intro'. done.
......
......@@ -319,7 +319,7 @@ Canonical Structure monPredI : bi :=
End canonical.
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
objective_at i j : P i - P j.
objective_at i j : P i P j.
Global Arguments Objective {_ _} _%I.
Global Arguments objective_at {_ _} _%I {_}.
Global Hint Mode Objective + + ! : typeclass_instances.
......@@ -379,9 +379,9 @@ Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i <absorb>?p (P i).
Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.
Lemma monPred_wand_force i P Q : (P - Q) i - (P i - Q i).
Lemma monPred_wand_force i P Q : (P - Q) i (P i - Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
Lemma monPred_impl_force i P Q : (P Q) i - (P i Q i).
Lemma monPred_impl_force i P Q : (P Q) i (P i Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
(** Instances *)
......@@ -665,7 +665,7 @@ Proof.
unseal. split=>i /=.
rewrite /= -(bi.exist_intro i). apply bi.and_intro=>//. by apply bi.pure_intro.
Qed.
Lemma monPred_in_elim P i : monPred_in i - P i P .
Lemma monPred_in_elim P i : monPred_in i P i P .
Proof.
apply bi.impl_intro_r. unseal. split=>i' /=.
eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
......
......@@ -151,7 +151,7 @@ Qed.
Lemma absorbingly_elim_plainly P : <absorb> P P.
Proof. by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently. Qed.
Lemma plainly_and_sep_elim P Q : P Q - (emp P) Q.
Lemma plainly_and_sep_elim P Q : P Q (emp P) Q.
Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
Lemma plainly_and_sep_assoc P Q R : P (Q R) ( P Q) R.
Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
......@@ -228,9 +228,9 @@ Qed.
Lemma plainly_affinely_elim P : <affine> P P.
Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
Lemma intuitionistically_plainly_elim P : P - P.
Lemma intuitionistically_plainly_elim P : P P.
Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
Lemma intuitionistically_plainly P : P - P.
Lemma intuitionistically_plainly P : P P.
Proof.
rewrite /bi_intuitionistically plainly_affinely_elim affinely_elim.
rewrite persistently_elim_plainly plainly_persistently_elim. done.
......
......@@ -14,8 +14,8 @@ Global Hint Mode BUpd ! : typeclass_instances.
Global Arguments bupd {_}%type_scope {_} _%bi_scope.
Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P |==> Q) (only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I : bi_scope.
Notation "P ==∗ Q" := (P - |==> Q) : stdpp_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset coPset PROP PROP.
Global Instance: Params (@fupd) 4 := {}.
......@@ -38,7 +38,7 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> |={Ei,Eo}=> Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P - |={Eo}[Ei]=> Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P - |={Eo}[Ei]=> Q) (only parsing) : stdpp_scope.
Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P - |={Eo}[Ei]=> Q) : stdpp_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]=> Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E}[E]= Q)%I : bi_scope.
......@@ -51,20 +51,20 @@ Notation "P ={ E }▷=∗ Q" := (P ={E}[E]▷=∗ Q) : stdpp_scope.
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]=> P) Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P - |={Eo}[Ei]=>^n Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P - |={Eo}[Ei]=>^n Q) (only parsing) : stdpp_scope.
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P - |={Eo}[Ei]=>^n Q) : stdpp_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]=>^n Q)%I : bi_scope.
Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]=^n Q)%I : bi_scope.
Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]=^n Q) (only parsing) : stdpp_scope.
Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]=^n Q) : stdpp_scope.
(** Bundled versions *)
(* Mixins allow us to create instances easily without having to use Program *)
Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
bi_bupd_mixin_bupd_intro (P : PROP) : P == P;
bi_bupd_mixin_bupd_mono (P Q : PROP) : (P Q) (|==> P) == Q;
bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) == P;
bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) R == P R;
bi_bupd_mixin_bupd_intro (P : PROP) : P |==> P;
bi_bupd_mixin_bupd_mono (P Q : PROP) : (P Q) (|==> P) |==> Q;
bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) |==> P;
bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) R |==> P R;
}.
Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
......@@ -73,15 +73,15 @@ Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
bi_fupd_mixin_fupd_mask_subseteq E1 E2 :
E2 E1 @{PROP} |={E1,E2}=> |={E2,E1}=> emp;
bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) :
(|={E1,E2}=> P) ={E1,E2}= P;
(|={E1,E2}=> P) |={E1,E2}=> P;
bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) :
(P Q) (|={E1,E2}=> P) |={E1,E2}=> Q;
bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) :
(|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P;
bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
E1 ## Ef (|={E1,E2}=> E2 ## Ef P) ={E1 Ef,E2 Ef}= P;
E1 ## Ef (|={E1,E2}=> E2 ## Ef P) |={E1 Ef,E2 Ef}=> P;
bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) :
(|={E1,E2}=> P) R ={E1,E2}= P R;
(|={E1,E2}=> P) R |={E1,E2}=> P R;
}.
Class BiBUpd (PROP : bi) := {
......@@ -99,11 +99,11 @@ Global Hint Mode BiFUpd ! : typeclass_instances.
Global Arguments bi_fupd_fupd : simpl never.
Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
bupd_fupd E (P : PROP) : (|==> P) ={E}= P.
bupd_fupd E (P : PROP) : (|==> P) |={E}=> P.
Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
bupd_plainly (P : PROP) : (|==> P) - P.
bupd_plainly (P : PROP) : (|==> P) P.
Global Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
(** These rules for the interaction between the [■] and [|={E1,E2=>] modalities
......@@ -137,13 +137,13 @@ Section bupd_laws.
Global Instance bupd_ne : NonExpansive (@bupd PROP _).
Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.
Lemma bupd_intro P : P == P.
Lemma bupd_intro P : P |==> P.
Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed.
Lemma bupd_mono (P Q : PROP) : (P Q) (|==> P) == Q.
Lemma bupd_mono (P Q : PROP) : (P Q) (|==> P) |==> Q.
Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed.
Lemma bupd_trans (P : PROP) : (|==> |==> P) == P.
Lemma bupd_trans (P : PROP) : (|==> |==> P) |==> P.
Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
Lemma bupd_frame_r (P R : PROP) : (|==> P) R == P R.
Lemma bupd_frame_r (P R : PROP) : (|==> P) R |==> P R.
Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
End bupd_laws.
......@@ -159,16 +159,16 @@ Section fupd_laws.
specify the mask. *)
Lemma fupd_mask_subseteq {E1} E2 : E2 E1 @{PROP} |={E1,E2}=> |={E2,E1}=> emp.
Proof. eapply bi_fupd_mixin_fupd_mask_subseteq, bi_fupd_mixin. Qed.
Lemma except_0_fupd E1 E2 (P : PROP) : (|={E1,E2}=> P) ={E1,E2}= P.
Lemma except_0_fupd E1 E2 (P : PROP) : (|={E1,E2}=> P) |={E1,E2}=> P.
Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
Lemma fupd_mono E1 E2 (P Q : PROP) : (P Q) (|={E1,E2}=> P) |={E1,E2}=> Q.
Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed.
Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P.
Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed.
Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
E1 ## Ef (|={E1,E2}=> E2 ## Ef P) ={E1 Ef,E2 Ef}= P.
E1 ## Ef (|={E1,E2}=> E2 ## Ef P) |={E1 Ef,E2 Ef}=> P.
Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) R ={E1,E2}= P R.
Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) R |={E1,E2}=> P R.
Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
End fupd_laws.
......@@ -186,13 +186,13 @@ Section bupd_derived.
Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (bupd (PROP:=PROP)).
Proof. intros P Q; apply bupd_mono. Qed.
Lemma bupd_frame_l R Q : (R |==> Q) == R Q.
Lemma bupd_frame_l R Q : (R |==> Q) |==> R Q.
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
Lemma bupd_wand_l P Q : (P - Q) (|==> P) == Q.
Lemma bupd_wand_l P Q : (P - Q) (|==> P) |==> Q.
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
Lemma bupd_wand_r P Q : (|==> P) (P - Q) == Q.
Lemma bupd_wand_r P Q : (|==> P) (P - Q) |==> Q.
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
Lemma bupd_sep P Q : (|==> P) (|==> Q) == P Q.
Lemma bupd_sep P Q : (|==> P) (|==> Q) |==> P Q.
Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
Lemma bupd_idemp P : (|==> |==> P) |==> P.
Proof.
......@@ -279,9 +279,9 @@ Section fupd_derived.
rewrite fupd_mask_subseteq; last exact: HE.
rewrite !fupd_frame_r. rewrite left_id. done.
Qed.
Lemma fupd_intro E P : P ={E}= P.
Lemma fupd_intro E P : P |={E}=> P.