Commit 7d74f654 authored by Robbert's avatar Robbert

Merge branch 'new_star' into 'master'

Use symbol ∗ for separating conjunction.

The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk * was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to conventional practise and matches the symbol we use on paper.

See merge request !21
parents 6cb76aaa cc31476d
This diff is collapsed.
This diff is collapsed.
......@@ -13,14 +13,14 @@ Notation "▷^ n P" := (uPred_laterN n P)
format "▷^ n P") : uPred_scope.
Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
n, (P - ^n False) - ^n False.
n, (P - ^n False) - ^n False.
Notation "|=n=> Q" := (uPred_nnupd Q)
(at level 99, Q at level 200, format "|=n=> Q") : uPred_scope.
Notation "P =n=> Q" := (P |=n=> Q)
(at level 99, Q at level 200, only parsing) : C_scope.
Notation "P =n=★ Q" := (P - |=n=> Q)%I
(at level 99, Q at level 200, format "P =n= Q") : uPred_scope.
Notation "P =n=∗ Q" := (P - |=n=> Q)%I
(at level 99, Q at level 200, format "P =n= Q") : uPred_scope.
(* Our goal is to prove that:
(1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris
......@@ -62,9 +62,9 @@ Qed.
are used throughout Iris hold for nnupd.
In fact, the first three properties that follow hold for any
modality of the form (- - Q) - Q for arbitrary Q. The situation
modality of the form (- - Q) - Q for arbitrary Q. The situation
here is slightly different, because nnupd is of the form
n, (- - (Q n)) - (Q n), but the proofs carry over straightforwardly.
n, (- - (Q n)) - (Q n), but the proofs carry over straightforwardly.
*)
......@@ -77,7 +77,7 @@ Proof.
rewrite /uPred_nnupd (forall_elim n).
apply wand_elim_r.
Qed.
Lemma nnupd_frame_r P R : (|=n=> P) R =n=> P R.
Lemma nnupd_frame_r P R : (|=n=> P) R =n=> P R.
Proof.
apply forall_intro=>n. apply wand_intro_r.
rewrite (comm _ P) -wand_curry.
......@@ -106,7 +106,7 @@ Qed.
(* However, the transitivity property seems to be much harder to
prove. This is surprising, because transitivity does hold for
modalities of the form (- - Q) - Q. What goes wrong when we quantify
modalities of the form (- - Q) - Q. What goes wrong when we quantify
now over n?
*)
......@@ -115,7 +115,7 @@ Proof.
rewrite /uPred_nnupd.
apply forall_intro=>a. apply wand_intro_l.
rewrite (forall_elim a).
rewrite (nnupd_intro (P - _)).
rewrite (nnupd_intro (P - _)).
rewrite /uPred_nnupd.
(* Oops -- the exponents of the later modality don't match up! *)
Abort.
......@@ -123,9 +123,9 @@ Abort.
(* Instead, we will need to prove this in the model. We start by showing that
nnupd is the limit of a the following sequence:
(- - False) - False,
(- - False) - False (- - False) - False,
(- - ^2 False) - ^2 False (- - False) - False (- - False) - False,
(- - False) - False,
(- - False) - False (- - False) - False,
(- - ^2 False) - ^2 False (- - False) - False (- - False) - False,
...
Then, it is easy enough to show that each of the uPreds in this sequence
......@@ -134,7 +134,7 @@ Abort.
(* The definition of the sequence above: *)
Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
((P - ^k False) - ^k False)
((P - ^k False) - ^k False)
match k with
O => True
| S k' => uPred_nnupd_k k' P
......@@ -155,7 +155,7 @@ Proof.
rewrite (forall_elim (S k)) //=.
Qed.
Lemma nnupd_k_elim n k P: n k ((|=n=>_k P) (P - (^n False)) (^n False))%I.
Lemma nnupd_k_elim n k P: n k ((|=n=>_k P) (P - (^n False)) (^n False))%I.
Proof.
induction k.
- inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l.
......@@ -165,10 +165,10 @@ Proof.
Qed.
Lemma nnupd_k_unfold k P:
(|=n=>_(S k) P) ⊣⊢ ((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P).
(|=n=>_(S k) P) ⊣⊢ ((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P).
Proof. done. Qed.
Lemma nnupd_k_unfold' k P n x:
(|=n=>_(S k) P)%I n x (((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P))%I n x.
(|=n=>_(S k) P)%I n x (((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P))%I n x.
Proof. done. Qed.
Lemma nnupd_k_weaken k P: (|=n=>_(S k) P) |=n=>_k P.
......@@ -238,13 +238,13 @@ Proof.
revert P.
induction k; intros P.
- rewrite //= ?right_id. apply wand_intro_l.
rewrite {1}(nnupd_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r.
rewrite {1}(nnupd_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r.
- rewrite {2}(nnupd_k_unfold k P).
apply and_intro.
* rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
rewrite nnupd_k_unfold. rewrite and_elim_l.
apply wand_intro_l.
rewrite {1}(nnupd_k_intro (S k) (P - ^(S k) (False)%I)).
rewrite {1}(nnupd_k_intro (S k) (P - ^(S k) (False)%I)).
rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
* do 2 rewrite nnupd_k_weaken //.
Qed.
......
......@@ -21,7 +21,7 @@ Section definitions.
Definition auth_own (a : A) : iProp Σ :=
own γ ( a).
Definition auth_inv (f : T A) (φ : T iProp Σ) : iProp Σ :=
( t, own γ ( f t) φ t)%I.
( t, own γ ( f t) φ t)%I.
Definition auth_ctx (N : namespace) (f : T A) (φ : T iProp Σ) : iProp Σ :=
inv N (auth_inv f φ).
......@@ -69,7 +69,7 @@ Section auth.
Implicit Types t u : T.
Implicit Types γ : gname.
Lemma auth_own_op γ a b : auth_own γ (a b) ⊣⊢ auth_own γ a auth_own γ b.
Lemma auth_own_op γ a b : auth_own γ (a b) ⊣⊢ auth_own γ a auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Global Instance from_sep_auth_own γ a b1 b2 :
......@@ -92,7 +92,7 @@ Section auth.
Proof. intros a1 a2. apply auth_own_mono. Qed.
Lemma auth_alloc_strong N E t (G : gset gname) :
(f t) φ t ={E}= γ, (γ G) auth_ctx γ N f φ auth_own γ (f t).
(f t) φ t ={E}= γ, (γ G) auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
......@@ -103,19 +103,19 @@ Section auth.
Qed.
Lemma auth_alloc N E t :
(f t) φ t ={E}= γ, auth_ctx γ N f φ auth_own γ (f t).
(f t) φ t ={E}= γ, auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ".
iMod (auth_alloc_strong N E t with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
Lemma auth_empty γ : True == auth_own γ .
Lemma auth_empty γ : True == auth_own γ .
Proof. by rewrite /auth_own -own_empty. Qed.
Lemma auth_acc E γ a :
auth_inv γ f φ auth_own γ a ={E}= t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={E}= auth_inv γ f φ auth_own γ b.
auth_inv γ f φ auth_own γ a ={E}= t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={E}= auth_inv γ f φ auth_own γ b.
Proof.
iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
......@@ -129,9 +129,9 @@ Section auth.
Lemma auth_open E N γ a :
nclose N E
auth_ctx γ N f φ auth_own γ a ={E,EN}= t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={EN,E}= auth_own γ b.
auth_ctx γ N f φ auth_own γ a ={E,EN}= t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={EN,E}= auth_own γ b.
Proof.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
......
......@@ -22,15 +22,15 @@ Section box_defs.
own γ (:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
( b, box_own_auth γ ( Excl' b) box_own_prop γ P if b then P else True)%I.
( b, box_own_auth γ ( Excl' b) box_own_prop γ P if b then P else True)%I.
Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
inv N (slice_inv γ P).
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
( Φ : slice_name iProp Σ,
(P [ map] γ b f, Φ γ)
[ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ)
(P [ map] γ b f, Φ γ)
[ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
......@@ -55,22 +55,22 @@ Global Instance slice_persistent γ P : PersistentP (slice N γ P).
Proof. apply _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
Proof.
rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_l.
by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
Qed.
Lemma box_own_auth_update γ b1 b2 b3 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2)
== box_own_auth γ ( Excl' b3) box_own_auth γ ( Excl' b3).
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2)
== box_own_auth γ ( Excl' b3) box_own_auth γ ( Excl' b3).
Proof.
rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
by apply auth_update, option_local_update, exclusive_local_update.
Qed.
Lemma box_own_agree γ Q1 Q2 :
(box_own_prop γ Q1 box_own_prop γ Q2) (Q1 Q2).
(box_own_prop γ Q1 box_own_prop γ Q2) (Q1 Q2).
Proof.
rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
......@@ -86,8 +86,8 @@ Proof.
Qed.
Lemma box_insert f P Q :
box N f P ={N}= γ, f !! γ = None
slice N γ Q box N (<[γ:=false]> f) (Q P).
box N f P ={N}= γ, f !! γ = None
slice N γ Q box N (<[γ:=false]> f) (Q P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_strong ( Excl' false Excl' false,
......@@ -100,17 +100,17 @@ Proof.
iModIntro; iExists γ; repeat iSplit; auto.
iNext. iExists (<[γ:=Q]> Φ); iSplit.
- iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
- rewrite (big_sepM_fn_insert (λ _ _ P', _ _ _ P' _ _ (_ _ P')))%I //.
- rewrite (big_sepM_fn_insert (λ _ _ P', _ _ _ P' _ _ (_ _ P')))%I //.
iFrame; eauto.
Qed.
Lemma box_delete f P Q γ :
f !! γ = Some false
slice N γ Q box N f P ={N}= P',
(P (Q P')) box N (delete γ f) P'.
slice N γ Q box N f P ={N}= P',
(P (Q P')) box N (delete γ f) P'.
Proof.
iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([ map] γ'↦_ delete γ f, Φ γ')%I.
iExists ([ map] γ'↦_ delete γ f, Φ γ')%I.
iInv N as (b) "(Hγ & #HγQ &_)" "Hclose".
iApply fupd_trans_frame; iFrame "Hclose"; iModIntro; iNext.
iDestruct (big_sepM_delete _ f _ false with "Hf")
......@@ -125,7 +125,7 @@ Qed.
Lemma box_fill f γ P Q :
f !! γ = Some false
slice N γ Q Q box N f P ={N}= box N (<[γ:=true]> f) P.
slice N γ Q Q box N f P ={N}= box N (<[γ:=true]> f) P.
Proof.
iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose".
......@@ -143,7 +143,7 @@ Qed.
Lemma box_empty f P Q γ :
f !! γ = Some true
slice N γ Q box N f P ={N}= Q box N (<[γ:=false]> f) P.
slice N γ Q box N f P ={N}= Q box N (<[γ:=false]> f) P.
Proof.
iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose".
......@@ -160,7 +160,7 @@ Proof.
iFrame; eauto.
Qed.
Lemma box_fill_all f P Q : box N f P P ={N}= box N (const true <$> f) P.
Lemma box_fill_all f P Q : box N f P P ={N}= box N (const true <$> f) P.
Proof.
iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
......@@ -177,11 +177,11 @@ Qed.
Lemma box_empty_all f P Q :
map_Forall (λ _, (true =)) f
box N f P ={N}= P box N (const false <$> f) P.
box N f P ={N}= P box N (const false <$> f) P.
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false)
box_own_prop γ (Φ γ) inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]".
iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false)
box_own_prop γ (Φ γ) inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]".
{ iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
assert (true = b) as <- by eauto.
......
......@@ -32,19 +32,19 @@ Section proofs.
Proof. rewrite /cinv; apply _. Qed.
Lemma cinv_own_op γ q1 q2 :
cinv_own γ q1 cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2).
cinv_own γ q1 cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2).
Proof. by rewrite /cinv_own own_op. Qed.
Lemma cinv_own_half γ q : cinv_own γ (q/2) cinv_own γ (q/2) ⊣⊢ cinv_own γ q.
Lemma cinv_own_half γ q : cinv_own γ (q/2) cinv_own γ (q/2) ⊣⊢ cinv_own γ q.
Proof. by rewrite cinv_own_op Qp_div_2. Qed.
Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 cinv_own γ q2 (q1 + q2)%Qp.
Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 cinv_own γ q2 (q1 + q2)%Qp.
Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed.
Lemma cinv_own_1_l γ q : cinv_own γ 1 cinv_own γ q False.
Lemma cinv_own_1_l γ q : cinv_own γ 1 cinv_own γ q False.
Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.
Lemma cinv_alloc E N P : P ={E}= γ, cinv N γ P cinv_own γ 1.
Lemma cinv_alloc E N P : P ={E}= γ, cinv N γ P cinv_own γ 1.
Proof.
rewrite /cinv /cinv_own. iIntros "HP".
iMod (own_alloc 1%Qp) as (γ) "H1"; first done.
......@@ -52,7 +52,7 @@ Section proofs.
Qed.
Lemma cinv_cancel E N γ P :
nclose N E cinv N γ P cinv_own γ 1 ={E}= P.
nclose N E cinv N γ P cinv_own γ 1 ={E}= P.
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
......@@ -61,7 +61,7 @@ Section proofs.
Lemma cinv_open E N γ p P :
nclose N E
cinv N γ P cinv_own γ p ={E,EN}= P cinv_own γ p ( P ={EN,E}= True).
cinv N γ P cinv_own γ p ={E,EN}= P cinv_own γ p ( P ={EN,E}= True).
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose".
......
......@@ -13,13 +13,13 @@ Module savedprop. Section savedprop.
Context (sprop : Type) (saved : sprop iProp iProp).
Hypothesis sprop_persistent : i P, PersistentP (saved i P).
Hypothesis sprop_alloc_dep :
(P : sprop iProp), True == ( i, saved i (P i)).
(P : sprop iProp), True == ( i, saved i (P i)).
Hypothesis sprop_agree : i P Q, saved i P saved i Q (P Q).
(** A bad recursive reference: "Assertion with name [i] does not hold" *)
Definition A (i : sprop) : iProp := P, ¬ P saved i P.
Definition A (i : sprop) : iProp := P, ¬ P saved i P.
Lemma A_alloc : True == i, saved i (A i).
Lemma A_alloc : True == i, saved i (A i).
Proof. by apply sprop_alloc_dep. Qed.
Lemma saved_NA i : saved i (A i) ¬ A i.
......@@ -63,7 +63,7 @@ Module inv. Section inv.
Hypothesis fupd_intro : E P, P fupd E P.
Hypothesis fupd_mono : E P Q, (P Q) fupd E P fupd E Q.
Hypothesis fupd_fupd : E P, fupd E (fupd E P) fupd E P.
Hypothesis fupd_frame_l : E P Q, P fupd E Q fupd E (P Q).
Hypothesis fupd_frame_l : E P Q, P fupd E Q fupd E (P Q).
Hypothesis fupd_mask_mono : P, fupd M0 P fupd M1 P.
(** We have invariants *)
......@@ -71,7 +71,7 @@ Module inv. Section inv.
Hypothesis inv_persistent : i P, PersistentP (inv i P).
Hypothesis inv_alloc : P, P fupd M1 ( i, inv i P).
Hypothesis inv_open :
i P Q R, (P Q fupd M0 (P R)) (inv i P Q fupd M1 R).
i P Q R, (P Q fupd M0 (P R)) (inv i P Q fupd M1 R).
(* We have tokens for a little "two-state STS": [start] -> [finish].
state. [start] also asserts the exact state; it is only ever owned by the
......@@ -88,15 +88,15 @@ Module inv. Section inv.
Hypothesis sts_alloc : True fupd M0 ( γ, start γ).
Hypotheses start_finish : γ, start γ fupd M0 (finished γ).
Hypothesis finished_not_start : γ, start γ finished γ False.
Hypothesis finished_not_start : γ, start γ finished γ False.
Hypothesis finished_dup : γ, finished γ finished γ finished γ.
Hypothesis finished_dup : γ, finished γ finished γ finished γ.
(** We assume that we cannot update to false. *)
Hypothesis consistency : ¬ (True fupd M1 False).
(** Some general lemmas and proof mode compatibility. *)
Lemma inv_open' i P R : inv i P (P - fupd M0 (P fupd M1 R)) fupd M1 R.
Lemma inv_open' i P R : inv i P (P - fupd M0 (P fupd M1 R)) fupd M1 R.
Proof.
iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
{ iSplit; first done. iExact "HP". }
......@@ -110,7 +110,7 @@ Module inv. Section inv.
intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
Qed.
Lemma fupd_frame_r E P Q : (fupd E P Q) fupd E (P Q).
Lemma fupd_frame_r E P Q : (fupd E P Q) fupd E (P Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
......@@ -130,18 +130,18 @@ Module inv. Section inv.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : iProp) : iProp :=
i, inv i (start γ (finished γ P)).
i, inv i (start γ (finished γ P)).
Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
Lemma saved_alloc (P : gname iProp) : True fupd M1 ( γ, saved γ (P γ)).
Proof.
iIntros "". iMod (sts_alloc) as (γ) "Hs".
iMod (inv_alloc (start γ (finished γ (P γ))) with "[Hs]") as (i) "#Hi".
iMod (inv_alloc (start γ (finished γ (P γ))) with "[Hs]") as (i) "#Hi".
{ auto. }
iApply fupd_intro. by iExists γ, i.
Qed.
Lemma saved_cast γ P Q : saved γ P saved γ Q P fupd M1 ( Q).
Lemma saved_cast γ P Q : saved γ P saved γ Q P fupd M1 ( Q).
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
......@@ -162,8 +162,8 @@ Module inv. Section inv.
Qed.
(** And now we tie a bad knot. *)
Notation "¬ P" := ( (P - fupd M1 False))%I : uPred_scope.
Definition A i : iProp := P, ¬P saved i P.
Notation "¬ P" := ( (P - fupd M1 False))%I : uPred_scope.
Definition A i : iProp := P, ¬P saved i P.
Global Instance A_persistent i : PersistentP (A i) := _.
Lemma A_alloc : True fupd M1 ( i, saved i (A i)).
......
......@@ -9,7 +9,7 @@ Import uPred.
Program Definition fupd_def `{invG Σ}
(E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ownE E1 == (wsat ownE E2 P))%I.
(wsat ownE E1 == (wsat ownE E2 P))%I.
Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
Definition fupd := proj1_sig fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
......@@ -19,19 +19,19 @@ Instance: Params (@fupd) 4.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=★ Q" := (P - |={E1,E2}=> Q)%I
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }= Q") : uPred_scope.
Notation "P ={ E1 , E2 }= Q" := (P |={E1,E2}=> Q)
format "P ={ E1 , E2 }= Q") : uPred_scope.
Notation "P ={ E1 , E2 }= Q" := (P |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : uPred_scope.
Notation "P ={ E }=★ Q" := (P - |={E}=> Q)%I
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }= Q") : uPred_scope.
Notation "P ={ E }= Q" := (P |={E}=> Q)
format "P ={ E }= Q") : uPred_scope.
Notation "P ={ E }= Q" := (P |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
Section fupd.
......@@ -50,26 +50,26 @@ Proof.
by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
Qed.
Lemma except_0_fupd E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Lemma except_0_fupd E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
Lemma bupd_fupd E P : (|==> P) ={E}= P.
Lemma bupd_fupd E P : (|==> P) ={E}= P.
Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
Lemma fupd_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) ={E1,E2}= Q.
Lemma fupd_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) ={E1,E2}= Q.
Proof.
rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
rewrite -HPQ. by iApply "HP".
Qed.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}= P.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}= P.
Proof.
rewrite fupd_eq /fupd_def. iIntros "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
Qed.
Lemma fupd_mask_frame_r' E1 E2 Ef P :
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.
intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
......@@ -77,7 +77,7 @@ Proof.
iIntros "!> !>". by iApply "HP".
Qed.
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) Q ={E1,E2}= P Q.
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) Q ={E1,E2}= P Q.
Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
(** * Derived rules *)
......@@ -87,50 +87,50 @@ Global Instance fupd_flip_mono' E1 E2 :
Proper (flip () ==> flip ()) (@fupd Σ _ E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Lemma fupd_intro E P : P ={E}= P.
Lemma fupd_intro E P : P ={E}= P.
Proof. iIntros "HP". by iApply bupd_fupd. Qed.
Lemma fupd_intro_mask' E1 E2 : E2 E1 True |={E1,E2}=> |={E2,E1}=> True.
Proof. exact: fupd_intro_mask. Qed.
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
Lemma fupd_frame_l E1 E2 P Q : (P |={E1,E2}=> Q) ={E1,E2}= P Q.
Lemma fupd_frame_l E1 E2 P Q : (P |={E1,E2}=> Q) ={E1,E2}= P Q.
Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
Lemma fupd_wand_l E1 E2 P Q : (P - Q) (|={E1,E2}=> P) ={E1,E2}= Q.
Lemma fupd_wand_l E1 E2 P Q : (P - Q) (|={E1,E2}=> P) ={E1,E2}= Q.
Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) (P - Q) ={E1,E2}= Q.
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) (P - Q) ={E1,E2}= Q.
Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
Lemma fupd_trans_frame E1 E2 E3 P Q :
((Q ={E2,E3}= True) |={E1,E2}=> (Q P)) ={E1,E3}= P.
((Q ={E2,E3}= True) |={E1,E2}=> (Q P)) ={E1,E3}= P.
Proof.
rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
by rewrite fupd_frame_r left_id fupd_trans.
Qed.
Lemma fupd_mask_frame_r E1 E2 Ef P :
E1 Ef (|={E1,E2}=> P) ={E1 Ef,E2 Ef}= P.
E1 Ef (|={E1,E2}=> P) ={E1 Ef,E2 Ef}= P.
Proof.
iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
iApply fupd_wand_r; iFrame "H"; eauto.
Qed.
Lemma fupd_mask_mono E1 E2 P : E1 E2 (|={E1}=> P) ={E2}= P.
Lemma fupd_mask_mono E1 E2 P : E1 E2 (|={E1}=> P) ={E2}= P.
Proof.
intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
Qed.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K A iProp Σ) (m : gmap K A) :
([ map] kx m, |={E}=> Φ k x) ={E}= [ map] kx m, Φ k x.
([ map] kx m, |={E}=> Φ k x) ={E}= [ map] kx m, Φ k x.
Proof.
apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A iProp Σ) X :
([ set] x X, |={E}=> Φ x) ={E}= [ set] x X, Φ x.
([ set] x X, |={E}=> Φ x) ={E}= [ set] x X, Φ x.
Proof.
apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.