From eacb1c46a7d4dcc871472c1a14c578a9f682a0af Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 24 May 2016 13:48:45 +0200
Subject: [PATCH] Flip order of arguments of iAssert/iPvsAssert.
---
heap_lang/lib/barrier/proof.v | 8 ++++----
proofmode/pviewshifts.v | 4 ++--
proofmode/tactics.v | 4 ++--
tests/one_shot.v | 4 ++--
tests/proofmode.v | 2 +-
5 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 33225fe1..a002baa5 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. }
iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
- ★ sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "[-]".
+ ★ 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 "Hl". }
iIntros "Hγ".
- iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
+ iPvsAssert (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Φ"). by iNext.
- (* a High state: the comparison succeeds, and we perform a transition and
@@ -157,7 +157,7 @@ Proof.
iSplit; [iPureIntro; by eauto using wait_step|].
iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
- iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
+ iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
@@ -185,7 +185,7 @@ Proof.
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
- iIntros "Hγ".
iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
- ★ sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "[-]".
+ ★ 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/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 5f4823b0..e9450cda 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -186,7 +186,7 @@ Tactic Notation "iTimeless" constr(H) :=
Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
iTimeless H; iDestruct H as Hs.
-Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
+Tactic Notation "iPvsAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
let H := iFresh in
let Hs := spec_pat.parse_one Hs in
lazymatch Hs with
@@ -200,4 +200,4 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
| ?pat => fail "iPvsAssert: invalid pattern" pat
end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
- iPvsAssert Q as pat with "[]".
+ iPvsAssert Q with "[]" as pat.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 1620fd28..195995bf 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -699,7 +699,7 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
(** * Assert *)
-Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
+Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
let H := iFresh in
let Hs := spec_pat.parse Hs in
lazymatch Hs with
@@ -716,7 +716,7 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
| ?pat => fail "iAssert: invalid pattern" pat
end.
Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
- iAssert Q as pat with "[]".
+ iAssert Q with "[]" as pat.
(** * Rewrite *)
Local Ltac iRewriteFindPred :=
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 053847b1..8ca7e243 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -58,13 +58,13 @@ Proof.
+ wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
- iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ OneShotPending) ∨
- ∃ n : Z, v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "Hv" with "[-]".
+ ∃ n : Z, v = InjRV #n ★ own γ (Shot (DecAgree n))))%I with "[-]" as "Hv".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
+ iExists (InjLV #0). iFrame "Hl". iLeft; by iSplit.
+ iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l ★ (v = InjLV #0 ∨ ∃ n : Z,
- v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "[$ #Hv]" with "[-]".
+ v = InjRV #n ★ own γ (Shot (DecAgree n))))%I with "[-]" as "[$ #Hv]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". by iLeft.
+ iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3052147b..0dec1404 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -26,7 +26,7 @@ Proof.
iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)".
iPoseProof "Hc" as "foo".
iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
- iAssert (uPred_ownM (a ⋅ core a))%I as "[Ha #Hac]" with "[Ha]".
+ iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]".
{ by rewrite cmra_core_r. }
iFrame "Ha Hac".
iExists (S j + z1), z2.
--
GitLab