Skip to content

GitLab

Commit 2863ad3a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Change notation of viewshifts in Coq scope. 

It used to be: (P ={E}=> Q) := (True ⊢ (P → |={E}=> Q))
Now it is: (P ={E}=> Q) := (P ⊢ |={E}=> Q)
parent c6685a3e
Hide whitespace changes
Inline Side-by-side
Showing with 78 additions and 110 deletions
heap_lang/heap.v
View file @ 2863ad3a
......@@ -97,7 +97,7 @@ Section heap.
(** Allocation *)
Lemma heap_alloc N E σ :
authG heap_lang Σ heapUR → nclose N ⊆ E →
ownP σ ⊢ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ [★ map] l↦v ∈ σ, l ↦ v).
ownP σ ={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ [★ map] l↦v ∈ σ, l ↦ v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
......
heap_lang/lib/barrier/proof.v
View file @ 2863ad3a
......@@ -170,7 +170,7 @@ Proof.
Qed.
Lemma recv_split E l P1 P2 :
nclose N ⊆ E → recv l (P1 ★ P2) ⊢ |={E}=> recv l P1 ★ recv l P2.
nclose N ⊆ E → recv l (P1 ★ P2) ={E}=> recv l P1 ★ recv l P2.
Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros {?} "Hr"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
......
heap_lang/lib/barrier/specification.v
View file @ 2863ad3a
......@@ -26,7 +26,7 @@ Proof.
iSplit; [done|]; iIntros {l} "?"; iExists l; by iSplit.
- iIntros {l P} "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
- iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl". by iIntros "?".
- iIntros {l P Q} "! Hl". by iApply recv_split.
- intros; by apply recv_split.
- apply recv_weaken.
Qed.
End spec.
program_logic/auth.v
View file @ 2863ad3a
......@@ -17,7 +17,7 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
Section definitions.
Context `{authG Λ Σ A} (γ : gname).
Definition auth_own (a : A) : iPropG Λ Σ :=
Definition auth_own (a : A) : iPropG Λ Σ :=
own γ (◯ a).
Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
(∃ a, own γ (● a) ★ φ a)%I.
......@@ -55,7 +55,7 @@ Section auth.
Lemma auth_alloc N E a :
✓ a → nclose N ⊆ E →
▷ φ a ⊢ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a.
Proof.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc (Auth (Excl' a) a)) as {γ} "Hγ"; first done.
......@@ -65,7 +65,7 @@ Section auth.
iPvsIntro; iExists γ; by iFrame "Hγ'".
Qed.
Lemma auth_empty γ E : True ⊢ |={E}=> auth_own γ ∅.
Lemma auth_empty γ E : True ={E}=> auth_own γ ∅.
Proof. by rewrite -own_empty. Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
......
program_logic/boxes.v
View file @ 2863ad3a
......@@ -69,8 +69,8 @@ Proof.
Qed.
Lemma box_own_auth_update E γ b1 b2 b3 :
(box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2))
⊢ |={E}=> (box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3)).
box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2)
={E}=> box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3).
Proof.
rewrite /box_own_prop -!own_op.
apply own_update, prod_update; simpl; last reflexivity.
......@@ -94,7 +94,7 @@ Proof.
Qed.
Lemma box_insert f P Q :
▷ box N f P ⊢ |={N}=> ∃ γ, f !! γ = None ★
▷ box N f P ={N}=> ∃ γ, f !! γ = None ★
box_slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P).
Proof.
iIntros "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
......@@ -114,7 +114,7 @@ Qed.
Lemma box_delete f P Q γ :
f !! γ = Some false →
(box_slice N γ Q ★ ▷ box N f P) ⊢ |={N}=> ∃ P',
box_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]".
......@@ -133,7 +133,7 @@ Qed.
Lemma box_fill f γ P Q :
f !! γ = Some false →
(box_slice N γ Q ★ ▷ Q ★ ▷ box N f P) ⊢ |={N}=> ▷ box N (<[γ:=true]> f) P.
box_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 & _)"; iTimeless "Hγ".
......@@ -151,7 +151,7 @@ Qed.
Lemma box_empty f P Q γ :
f !! γ = Some true →
(box_slice N γ Q ★ ▷ box N f P) ⊢ |={N}=> ▷ Q ★ ▷ box N (<[γ:=false]> f) P.
box_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)"; iTimeless "Hγ".
......@@ -170,8 +170,7 @@ Proof.
iFrame "Hγ'". by repeat iSplit.
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.
......@@ -188,7 +187,7 @@ 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.
iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
......
program_logic/ghost_ownership.v
View file @ 2863ad3a
......@@ -43,7 +43,7 @@ Proof. rewrite /own; apply _. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a E (G : gset gname) :
✓ a → True ⊢ (|={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a).
✓ a → True ={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a.
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
......@@ -54,14 +54,14 @@ Proof.
- apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv // left_id.
Qed.
Lemma own_alloc a E : ✓ a → True ⊢ (|={E}=> ∃ γ, own γ a).
Lemma own_alloc a E : ✓ a → True ={E}=> ∃ γ, own γ a.
Proof.
intros Ha. rewrite (own_alloc_strong a E ∅) //; [].
apply pvs_mono, exist_mono=>?. eauto with I.
Qed.
Lemma own_updateP P γ a E :
a ~~>: P → own γ a ⊢ (|={E}=> ∃ a', ■ P a' ∧ own γ a').
a ~~>: P → own γ a ={E}=> ∃ a', ■ P a' ∧ own γ a'.
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
......@@ -72,7 +72,7 @@ Proof.
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.
Lemma own_update γ a a' E : a ~~> a' → own γ a ⊢ (|={E}=> own γ a').
Lemma own_update γ a a' E : a ~~> a' → own γ a ={E}=> own γ a'.
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
......@@ -83,7 +83,7 @@ Section global_empty.
Context `{i : inG Λ Σ (A:ucmraT)}.
Implicit Types a : A.
Lemma own_empty γ E : True ⊢ (|={E}=> own γ ∅).
Lemma own_empty γ E : True ={E}=> own γ ∅.
Proof.
rewrite ownG_empty /own. apply pvs_ownG_update, iprod_singleton_update_empty.
apply (singleton_update_unit (cmra_transport inG_prf ∅)); last done.
......
program_logic/hoare_lifting.v
View file @ 2863ad3a
......@@ -55,7 +55,7 @@ Proof.
(λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
repeat iSplit.
- by iApply vs_reflexive.
- by iIntros "! ?".
- iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro.
iSplitL "Hown". by iSplit. iSplit. by iDestruct "Hφ" as %[_ ?]. done.
- iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
......
program_logic/invariants.v
View file @ 2863ad3a
......@@ -25,7 +25,7 @@ Proof. rewrite /inv; apply _. Qed.
Lemma always_inv N P : □ inv N P ⊣⊢ inv N P.
Proof. by rewrite always_always. Qed.
Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊢ |={E}=> inv N P.
Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ={E}=> inv N P.
Proof.
intros. rewrite -(pvs_mask_weaken N) //.
by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
......
program_logic/pviewshifts.v
View file @ 2863ad3a
......@@ -40,6 +40,13 @@ Notation "|={ E }=> Q" := (pvs E E Q%I)
Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : C_scope.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
......@@ -58,18 +65,18 @@ Qed.
Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P ⊢ |={E}=> P.
Lemma pvs_intro E P : P ={E}=> P.
Proof.
rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
apply uPred_closed with n; eauto.
Qed.
Lemma pvs_mono E1 E2 P Q : P ⊢ Q → (|={E1,E2}=> P) ⊢ (|={E1,E2}=> Q).
Lemma pvs_mono E1 E2 P Q : P ⊢ Q → (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof.
rewrite pvs_eq. intros HPQ; split=> n r ? HP rf k Ef σ ???.
destruct (HP rf k Ef σ) as (r2&?&?); eauto.
exists r2; eauto using uPred_in_entails.
Qed.
Lemma pvs_timeless E P : TimelessP P → ▷ P ⊢ (|={E}=> P).
Lemma pvs_timeless E P : TimelessP P → ▷ P ={E}=> P.
Proof.
rewrite pvs_eq uPred.timelessP_spec=> HP.
uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
......@@ -77,19 +84,19 @@ Proof.
apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
Lemma pvs_trans E1 E2 E3 P :
E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊢ (|={E1,E3}=> P).
E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Proof.
rewrite pvs_eq. intros ?; split=> n r1 ? HP1 rf k Ef σ ???.
destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
Ef ⊥ E1 ∪ E2 → (|={E1,E2}=> P) ⊢ (|={E1 ∪ Ef,E2 ∪ Ef}=> P).
Ef ⊥ E1 ∪ E2 → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof.
rewrite pvs_eq. intros ?; split=> n r ? HP rf k Ef' σ ???.
destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
by exists r'; rewrite -(assoc_L _).
Qed.
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ★ Q) ⊢ (|={E1,E2}=> P ★ Q).
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
Proof.
rewrite pvs_eq. uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
......@@ -97,7 +104,7 @@ Proof.
exists (r' ⋅ r2); split; last by rewrite -assoc.
exists r', r2; split_and?; auto. apply uPred_closed with n; auto.
Qed.
Lemma pvs_openI i P : ownI i P ⊢ (|={{[i]},∅}=> ▷ P).
Lemma pvs_openI i P : ownI i P ={{[i]},∅}=> ▷ P.
Proof.
rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
apply ownI_spec in Hinv; last auto.
......@@ -106,9 +113,10 @@ Proof.
exists (rP ⋅ r); split; last by rewrite (left_id_L _ _) -assoc.
eapply uPred_mono with rP; eauto using cmra_includedN_l.
Qed.
Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊢ (|={∅,{[i]}}=> True).
Lemma pvs_closeI i P : ownI i P ∧ ▷ P ={∅,{[i]}}=> True.
Proof.
rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
rewrite pvs_eq.
uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
exists ∅; split; [done|].
rewrite left_id; apply wsat_close with P r.
- apply ownI_spec, uPred_closed with (S n); auto.
......@@ -117,7 +125,7 @@ Proof.
- apply uPred_closed with n; auto.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ⊢ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
m ~~>: P → ownG m ={E}=> ∃ m', ■ P m' ∧ ownG m'.
Proof.
rewrite pvs_eq. intros Hup.
uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
......@@ -125,7 +133,7 @@ Proof.
{ apply cmra_includedN_le with (S n); auto. }
by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊢ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
Lemma pvs_allocI E P : ¬set_finite E → ▷ P ={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P.
Proof.
rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
......@@ -142,37 +150,37 @@ Proof. intros P Q; apply pvs_mono. Qed.
Global Instance pvs_flip_mono' E1 E2 :
Proper (flip (⊢) ==> flip (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ⊢ (|={E}=> P).
Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ={E}=> P.
Proof. apply pvs_trans; set_solver. Qed.
Lemma pvs_strip_pvs E P Q : P ⊢ (|={E}=> Q) → (|={E}=> P) ⊢ (|={E}=> Q).
Lemma pvs_strip_pvs E P Q : (P ={E}=> Q) → (|={E}=> P) ={E}=> Q.
Proof. move=>->. by rewrite pvs_trans'. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊢ (|={E1,E2}=> P ★ Q).
Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=> P ★ Q.
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!PersistentP P} :
(P ∧ |={E1,E2}=> Q) ⊢ (|={E1,E2}=> P ∧ Q).
(P ∧ |={E1,E2}=> Q) ={E1,E2}=> P ∧ Q.
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
Lemma pvs_always_r E1 E2 P Q `{!PersistentP Q} :
((|={E1,E2}=> P) ∧ Q) ⊢ (|={E1,E2}=> P ∧ Q).
(|={E1,E2}=> P) ∧ Q ={E1,E2}=> P ∧ Q.
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=> Q).
Lemma pvs_impl_l E1 E2 P Q : □ (P → Q) ∧ (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P) ∧ □ (P → Q)) ⊢ (|={E1,E2}=> Q).
Lemma pvs_impl_r E1 E2 P Q : (|={E1,E2}=> P) ∧ □ (P → Q) ={E1,E2}=> Q.
Proof. by rewrite comm pvs_impl_l. Qed.
Lemma pvs_wand_l E1 E2 P Q : ((P -★ Q) ★ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=> Q).
Lemma pvs_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q : ((|={E1,E2}=> P) ★ (P -★ Q)) ⊢ (|={E1,E2}=> Q).
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
Lemma pvs_sep E P Q : ((|={E}=> P) ★ (|={E}=> Q)) ⊢ (|={E}=> P ★ Q).
Lemma pvs_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=> P ★ Q.
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Λ Σ) (m : gmap K A) :
([★ map] k↦x ∈ m, |={E}=> Φ k x) ⊢ (|={E}=> [★ map] k↦x ∈ m, Φ k x).
([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; auto using pvs_intro.
by rewrite IH pvs_sep.
Qed.
Lemma pvs_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.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; csimpl; auto using pvs_intro.
......@@ -180,21 +188,20 @@ Proof.
Qed.
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
(|={E1',E2'}=> P) ⊢ (|={E1,E2}=> P).
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → (|={E1',E2'}=> P) ={E1,E2}=> P.
Proof.
intros HE1 HE2 HEE.
rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
by rewrite {2}HEE -!union_difference_L.
Qed.
Lemma pvs_openI' E i P : i ∈ E → ownI i P ⊢ (|={E, E ∖ {[i]}}=> ▷ P).
Lemma pvs_openI' E i P : i ∈ E → ownI i P ={E, E ∖ {[i]}}=> ▷ P.
Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_closeI' E i P : i ∈ E → (ownI i P ∧ ▷ P) ⊢ (|={E ∖ {[i]}, E}=> True).
Lemma pvs_closeI' E i P : i ∈ E → (ownI i P ∧ ▷ P) ={E ∖ {[i]}, E}=> True.
Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
P ⊢ Q → (|={E1',E2'}=> P) ⊢ (|={E1,E2}=> Q).
P ⊢ Q → (|={E1',E2'}=> P) ={E1,E2}=> Q.
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
(** It should be possible to give a stronger version of this rule
......@@ -203,13 +210,13 @@ Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
mask becomes really ugly then, and we have not found an instance
where that would be useful. *)
Lemma pvs_trans3 E1 E2 Q :
E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ⊢ (|={E1}=> Q).
E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ={E1}=> Q.
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ⊢ (|={E2}=> P).
Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=> P.
Proof. auto using pvs_mask_frame'. Qed.
Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊢ (|={E}=> ownG m').
Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ={E}=> ownG m'.
Proof.
intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
......@@ -254,14 +261,14 @@ Proof.
apply (anti_symm (⊢)); [|apply fsa_mono=> a; apply pvs_intro].
by rewrite (pvs_intro E (fsa E _)) fsa_trans3.
Qed.
Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊢ (|={E}=> Ψ a)) → fsa E Φ ⊢ fsa E Ψ.
Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ={E}=> Ψ a) → fsa E Φ ⊢ fsa E Ψ.
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
Lemma fsa_wand_l E Φ Ψ : ((∀ a, Φ a -★ Ψ a) ★ fsa E Φ) ⊢ (fsa E Ψ).
Lemma fsa_wand_l E Φ Ψ : ((∀ a, Φ a -★ Ψ a) ★ fsa E Φ) ⊢ fsa E Ψ.
Proof.
rewrite fsa_frame_l. apply fsa_mono=> a.
by rewrite (forall_elim a) wand_elim_l.
Qed.
Lemma fsa_wand_r E Φ Ψ : (fsa E Φ ★ ∀ a, Φ a -★ Ψ a) ⊢ (fsa E Ψ).
Lemma fsa_wand_r E Φ Ψ : (fsa E Φ ★ ∀ a, Φ a -★ Ψ a) ⊢ fsa E Ψ.
Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
End fsa.
......
program_logic/saved_one_shot.v
View file @ 2863ad3a
......@@ -26,16 +26,16 @@ Section one_shot.
Proof. rewrite /one_shot_own; apply _. Qed.
Lemma one_shot_alloc_strong E (G : gset gname) :
True ⊢ |={E}=> ∃ γ, ■ (γ ∉ G) ∧ one_shot_pending γ.
True ={E}=> ∃ γ, ■ (γ ∉ G) ∧ one_shot_pending γ.
Proof. by apply own_alloc_strong. Qed.
Lemma one_shot_alloc E : True ⊢ |={E}=> ∃ γ, one_shot_pending γ.
Lemma one_shot_alloc E : True ={E}=> ∃ γ, one_shot_pending γ.
Proof. by apply own_alloc. Qed.
Lemma one_shot_init E γ x : one_shot_pending γ ⊢ |={E}=> one_shot_own γ x.
Lemma one_shot_init E γ x : one_shot_pending γ ={E}=> one_shot_own γ x.
Proof. by apply own_update, one_shot_update_shoot. Qed.
Lemma one_shot_alloc_init E x : True ⊢ |={E}=> ∃ γ, one_shot_own γ x.
Lemma one_shot_alloc_init E x : True ={E}=> ∃ γ, one_shot_own γ x.
Proof.
rewrite (one_shot_alloc E). apply pvs_strip_pvs.
apply exist_elim=>γ. rewrite -(exist_intro γ).
......
program_logic/saved_prop.v
View file @ 2863ad3a
......@@ -24,10 +24,10 @@ Section saved_prop.
Proof. rewrite /saved_prop_own; apply _. Qed.
Lemma saved_prop_alloc_strong E x (G : gset gname) :
True ⊢ |={E}=> ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x.
True ={E}=> ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x.
Proof. by apply own_alloc_strong. Qed.
Lemma saved_prop_alloc E x : True ⊢ |={E}=> ∃ γ, saved_prop_own γ x.
Lemma saved_prop_alloc E x : True ={E}=> ∃ γ, saved_prop_own γ x.
Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ x y :
......
program_logic/sts.v
View file @ 2863ad3a
......@@ -64,12 +64,12 @@ Section sts.
sts_frag_included. *)
Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
sts_ownS γ S1 T1 ⊢ (|={E}=> sts_ownS γ S2 T2).
sts_ownS γ S1 T1 ={E}=> sts_ownS γ S2 T2.
Proof. intros ???. by apply own_update, sts_update_frag. Qed.
Lemma sts_own_weaken E γ s S T1 T2 :
T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
sts_own γ s T1 ⊢ (|={E}=> sts_ownS γ S T2).
sts_own γ s T1 ={E}=> sts_ownS γ S T2.
Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
Lemma sts_ownS_op γ S1 S2 T1 T2 :
......@@ -79,7 +79,7 @@ Section sts.
Lemma sts_alloc E N s :
nclose N ⊆ E →
▷ φ s ⊢ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
▷ φ s ={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
Proof.
iIntros {?} "Hφ". rewrite /sts_ctx /sts_own.
iPvs (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as {γ} "Hγ".
......
program_logic/viewshifts.v
View file @ 2863ad3a
......@@ -10,37 +10,15 @@ Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I 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" := (True ⊢ (P ={E1,E2}=> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : uPred_scope.
Notation "P ={ E }=> Q" := (True ⊢ (P ={E}=> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : C_scope.
Notation "P <={ E1 , E2 }=> Q" := ((P ={E1,E2}=> Q) ∧ (Q ={E2,E1}=> P))%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" := (True ⊢ (P <={E1,E2}=> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P <={ E1 , E2 }=> Q") : C_scope.
Notation "P <={ E }=> Q" := (P <={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=> Q") : uPred_scope.
Notation "P <={ E }=> Q" := (True ⊢ (P <={E}=> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P <={ E }=> Q") : C_scope.
Section vs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q R : iProp Λ Σ.
Implicit Types N : namespace.
Lemma vs_alt E1 E2 P Q : P ⊢ (|={E1,E2}=> Q) → P ={E1,E2}=> Q.
Proof. iIntros {Hvs} "! ?". by iApply Hvs. Qed.
Global Instance vs_ne E1 E2 n :
Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Proof. solve_proper. Qed.
......@@ -57,9 +35,9 @@ Global Instance vs_mono' E1 E2 :
Proof. solve_proper. Qed.
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
Proof. iIntros "! []". Qed.
Proof. iIntros "[]". Qed.
Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
Proof. iIntros {?} "! HP". by iApply pvs_timeless. Qed.
Proof. by apply pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
......@@ -71,7 +49,7 @@ Qed.
Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
Proof. apply vs_transitive; set_solver. Qed.
Lemma vs_reflexive E P : P ={E}=> P.
Proof. by iIntros "! HP". Qed.
Proof. by iIntros "HP". Qed.