Commit 695c9baa authored by Robbert Krebbers's avatar Robbert Krebbers

Use |==> syntax for 'preserve pvs' specialization pattern.

We used => before, which is strange, because it has another meaning
in ssreflect.
parent a467cde4
Pipeline #1244 passed with stage
......@@ -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γ");
......
......@@ -193,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 (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.
......
......@@ -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 [] "".
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment