diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v index 100ba776d5cae9daa499c6d181bac9ddafd7fae5..3427dd3c516f4a1c75cb41c79dca2ceefd1661cd 100644 --- a/algebra/upred_big_op.v +++ b/algebra/upred_big_op.v @@ -188,10 +188,10 @@ Section gmap. by rewrite -big_sepM_delete. Qed. - Lemma big_sepM_fn_insert (Ψ : K → A → uPred M → uPred M) (Φ : K → uPred M) m i x P : + Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b : m !! i = None → - ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=P]> Φ k)) - ⊣⊢ (Ψ i x P ★ [★ map] k↦y ∈ m, Ψ k y (Φ k)). + ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k)) + ⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)). Proof. intros. rewrite big_sepM_insert // fn_lookup_insert. apply sep_proper, big_sepM_proper; auto=> k y ??. @@ -301,10 +301,10 @@ Section gset. Lemma big_sepS_insert Φ X x : x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y). Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. - Lemma big_sepS_fn_insert (Ψ : A → uPred M → uPred M) Φ X x P : + Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b : x ∉ X → - ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=P]> Φ y)) - ⊣⊢ (Ψ x P ★ [★ set] y ∈ X, Ψ y (Φ y)). + ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y)) + ⊣⊢ (Ψ x b ★ [★ set] y ∈ X, Ψ y (f y)). Proof. intros. rewrite big_sepS_insert // fn_lookup_insert. apply sep_proper, big_sepS_proper; auto=> y ??. diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v index fb906f2e513d668c4ce132937aa9735fea4bd3c3..31ab9d3f315bffffde9649c29cb05118129a0f18 100644 --- a/heap_lang/lib/barrier/proof.v +++ b/heap_lang/lib/barrier/proof.v @@ -110,7 +110,7 @@ Proof. iAssert (barrier_ctx γ' l P)%I as "#?". { rewrite /barrier_ctx. by repeat iSplit. } iAssert (sts_ownS γ' (i_states γ) {[Change γ]} - ★ sts_ownS γ' low_states {[Send]})%I with "=>[-]" as "[Hr Hs]". + ★ sts_ownS γ' low_states {[Send]})%I with "|==>[-]" as "[Hr Hs]". { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. + set_solver. + iApply (sts_own_weaken with "Hγ'"); @@ -148,7 +148,7 @@ Proof. iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"]. { iNext. rewrite {2}/barrier_inv /=. by iFrame. } iIntros "Hγ". - iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "=>[Hγ]" as "Hγ". + iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "|==>[Hγ]" as "Hγ". { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. } wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). auto. - (* a High state: the comparison succeeds, and we perform a transition and @@ -185,7 +185,7 @@ Proof. iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. - iIntros "Hγ". iAssert (sts_ownS γ (i_states i1) {[Change i1]} - ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "=>[-]" as "[Hγ1 Hγ2]". + ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "|==>[-]" as "[Hγ1 Hγ2]". { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. + set_solver. + iApply (sts_own_weaken with "Hγ"); diff --git a/prelude/base.v b/prelude/base.v index 22752705fcfc727038368eb0053fb2d86e83e8c3..bfcb09aed3bd222aa10776452726f0578050b795 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -637,6 +637,11 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope. Notation "( X ⊄ )" := (λ Y, X ⊄ Y) (only parsing) : C_scope. Notation "( ⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope. +Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope. +Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope. +Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope. +Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope. + (** The class [Lexico A] is used for the lexicographic order on [A]. This order is used to create finite maps, finite sets, etc, and is typically different from the order [(⊆)]. *) diff --git a/program_logic/boxes.v b/program_logic/boxes.v index 3ef1749dfb6d63682f0e6b4d9fd89784fa4ee9b1..9f50539601632fac061daa55e05fd2ea1c6449e1 100644 --- a/program_logic/boxes.v +++ b/program_logic/boxes.v @@ -13,29 +13,31 @@ Section box_defs. Context `{boxG Λ Σ} (N : namespace). Notation iProp := (iPropG Λ Σ). - Definition box_own_auth (γ : gname) (a : auth (option (excl bool))) : iProp := - own γ (a, ∅). + Definition slice_name := gname. - Definition box_own_prop (γ : gname) (P : iProp) : iProp := + Definition box_own_auth (γ : slice_name) + (a : auth (option (excl bool))) : iProp := own γ (a, ∅). + + Definition box_own_prop (γ : slice_name) (P : iProp) : iProp := own γ (∅:auth _, Some (to_agree (Next (iProp_unfold P)))). - Definition box_slice_inv (γ : gname) (P : iProp) : iProp := + 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. - Definition box_slice (γ : gname) (P : iProp) : iProp := - inv N (box_slice_inv γ P). + Definition slice (γ : slice_name) (P : iProp) : iProp := + inv N (slice_inv γ P). - Definition box (f : gmap gname bool) (P : iProp) : iProp := - (∃ Φ : gname → iProp, + 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 γ (Φ γ) ★ - inv N (box_slice_inv γ (Φ γ)))%I. + inv N (slice_inv γ (Φ γ)))%I. End box_defs. Instance: Params (@box_own_auth) 4. Instance: Params (@box_own_prop) 4. -Instance: Params (@box_slice_inv) 4. -Instance: Params (@box_slice) 5. +Instance: Params (@slice_inv) 4. +Instance: Params (@slice) 5. Instance: Params (@box) 5. Section box. @@ -46,13 +48,13 @@ Implicit Types P Q : iProp. (* FIXME: solve_proper picks the eq ==> instance for Next. *) Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ). Proof. solve_proper. Qed. -Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_slice_inv γ). +Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ). Proof. solve_proper. Qed. -Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ). +Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ). Proof. solve_proper. Qed. Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f). Proof. solve_proper. Qed. -Global Instance box_slice_persistent γ P : PersistentP (box_slice N γ P). +Global Instance slice_persistent γ P : PersistentP (slice N γ P). Proof. apply _. Qed. (* This should go automatic *) @@ -95,7 +97,7 @@ Qed. Lemma box_insert f P Q : ▷ box N f P ={N}=> ∃ γ, f !! γ = None ★ - box_slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). + slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). Proof. iIntros "H"; iDestruct "H" as {Φ} "[#HeqP Hf]". iPvs (own_alloc_strong (● Excl' false ⋅ ◯ Excl' false, @@ -103,7 +105,7 @@ Proof. as {γ} "[Hdom Hγ]"; first done. rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]". iDestruct "Hdom" as % ?%not_elem_of_dom. - iPvs (inv_alloc N _ (box_slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done. + iPvs (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done. { iNext. iExists false; eauto. } iPvsIntro; iExists γ; repeat iSplit; auto. iNext. iExists (<[γ:=Q]> Φ); iSplit. @@ -114,7 +116,7 @@ Qed. Lemma box_delete f P Q γ : f !! γ = Some false → - box_slice N γ Q ★ ▷ box N f P ={N}=> ∃ 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]". @@ -133,7 +135,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. + 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 +153,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. + 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γ". @@ -191,7 +193,7 @@ Lemma box_empty_all f P Q : Proof. iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]". iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★ - box_own_prop γ (Φ γ) ★ inv N (box_slice_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]". + box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "|==>[Hf]" as "[HΦ ?]". { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf". iAlways; iIntros {γ b ?} "(Hγ' & #\$ & #\$)". assert (true = b) as <- by eauto. @@ -207,4 +209,4 @@ Proof. Qed. End box. -Typeclasses Opaque box_slice box. +Typeclasses Opaque slice_name slice box. diff --git a/program_logic/invariants.v b/program_logic/invariants.v index cb554fa42cd4bc33bd5cf9051c55429816e26512..3fb3ba6748b461a2969357512e961232af2c84cb 100644 --- a/program_logic/invariants.v +++ b/program_logic/invariants.v @@ -34,7 +34,7 @@ Qed. (** Fairly explicit form of opening invariants *) Lemma inv_open E N P : nclose N ⊆ E → - inv N P ⊢ ∃ E', ■ (E ∖ nclose N ⊆ E' ∧ E' ⊆ E) ★ + inv N P ⊢ ∃ E', ■ (E ∖ nclose N ⊆ E' ⊆ E) ★ |={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True). Proof. rewrite /inv. iIntros {?} "Hinv". iDestruct "Hinv" as {i} "[% #Hi]". diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v index 3aaa3521ab0ad958666134c36f34e89b241cf6ef..f045dc2c0199cc3d795f572ff61e9f020ec373ff 100644 --- a/program_logic/pviewshifts.v +++ b/program_logic/pviewshifts.v @@ -41,11 +41,9 @@ 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. + (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : 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. + (at level 99, E at level 50, Q at level 200, only parsing) : C_scope. Section pvs. Context {Λ : language} {Σ : iFunctor}. diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v index c6919d5fa41cf24a3a21abba68856ed45021c0cb..4ef97c10b67a210d2ab7c6787ac36b69d22a3d82 100644 --- a/proofmode/spec_patterns.v +++ b/proofmode/spec_patterns.v @@ -32,7 +32,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token := | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) "" | String "%" s => tokenize_go s (TPure :: cons_name kn k) "" | String "*" s => tokenize_go s (TForall :: cons_name kn k) "" - | String "=" (String ">" s) => tokenize_go s (TPvs :: cons_name kn k) "" + | String "|" (String "=" (String "=" (String ">" s))) => + tokenize_go s (TPvs :: cons_name kn k) "" | String a s => tokenize_go s k (String a kn) end. Definition tokenize (s : string) : list token := tokenize_go s [] "". diff --git a/tests/proofmode.v b/tests/proofmode.v index 02e9a825ccd5dafcd1b274eeb287ab102798c142..9301a91b987e1e340358babde4dc32b288316388 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -100,7 +100,7 @@ Section iris. (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q -★ |={E}=> R. Proof. iIntros {?} "H HP HQ". - iApply ("H" with "[#] HP =>[HQ] =>"). + iApply ("H" with "[#] HP |==>[HQ] |==>"). - done. - by iApply inv_alloc. - by iPvsIntro.