diff --git a/theories/examples/graphs_queue_impl.v b/theories/examples/graphs_queue_impl.v
index d78b8a6e931fe43c30b9f082c6dc9b5905848dde..e4b0f198a461a3a35daffe79577328e40c8d4dda 100644
--- a/theories/examples/graphs_queue_impl.v
+++ b/theories/examples/graphs_queue_impl.v
@@ -60,7 +60,7 @@ End iwpApply.
Declare ML Module "MetaCoqPlugin".
-Tactic Notation "iwpApply" "with" open_constr(texan) "intros" "(" simple_intropattern(i1) ")" open_constr(i2) "using" open_constr(lem) "with" open_constr(lem_goals):=
+Tactic Notation "iwpApply" "with" open_constr(texan) "using" open_constr(lem) :=
let Σ_evar := fresh "__remove_Σ" in
let TT_evar := fresh "__remove_TT" in
let Q_evar := fresh "__remove_Q" in
@@ -83,7 +83,10 @@ Tactic Notation "iwpApply" "with" open_constr(texan) "intros" "(" simple_intropa
let to_val_evar := to_val_evar' in
iApply (texan_apply_iwp_tele (TT:=TT_evar) (Q:=Q_evar) (to_val:=to_val_evar) with texan); [
|
- iIntros ( i1 ); iIntros i2;
+ let Ψ := fresh in
+ (* we can use "Pre" and "Post" because we know that we start with an empty context. *)
+ iIntros ( Ψ ); iIntros "Pre Post";
+
let H := iFresh in
iPoseProof (lem) as H;
(* (* [solve_ndisj|done|solve_ndisj|by left|by right|by right|..]. *) *)
@@ -105,8 +108,9 @@ Tactic Notation "iwpApply" "with" open_constr(texan) "intros" "(" simple_intropa
unify Q_evar (tele_app (TT:=TT) Q);
unify to_val_evar (tele_app (TT:=TT) to_val)
end;
- iApply (H with lem_goals);
- try iClear H
+ iEval (cbn) in "Post";
+ iApply (H with "Pre Post");
+ iClear H
(* iSpecialize (H with lem_goals); [..|iApply H] *)
]
|..].
@@ -596,11 +600,8 @@ Proof.
(* invoking iRC11 Texan triple for new *)
iwp_bind (new [ #2])%E.
- iwpApply with "oV sV" intros (Ψ) "_ POST" using wp_new with "[] [POST]";
+ iwpApply with "oV sV" using wp_new;
[done|done|lia|done|..].
- { iIntros "!>" (l) "Hl". iApply "POST". by iFrame "Hl". }
- { done. }
-
iIntros "!>" (n 𝓥1 Le1) "sV1 oV1 P1". iCurViewUp Le1.
iDestruct "P1" as "[[H†|%] Hn]"; [|done].
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
@@ -619,9 +620,8 @@ Proof.
(* repeat loop to find tail *)
iwp_bind (repeat: _)%E.
- iwpApply with "oV3 sV3 Queue" intros (Ψ) "Q Post" using find_tail_repeat_spec with "Q [-]";
+ iwpApply with "oV3 sV3 Queue" using find_tail_repeat_spec;
[done|..].
- { iIntros "!>" (l) "P". iApply "Post". iExact "P". }
iIntros "!>" (l' 𝓥4 Le4) "sV4 oV4 P". iCurViewUp Le4.
iDestruct "P" as (γt' γ' t') "oL'".
@@ -663,20 +663,15 @@ Proof.
own γg (ghost_emap_master (<[enqId := (Enq v, V)]> emap)) ∗
VMap_master γq (<[γt := enqId]> M) ⎤)%I.
- iwpApply with "oV4 sV4 [-H† HClose Toks]" intros (Ψ) "Pre Post" using
+ iwpApply with "oV4 sV4 [-H† HClose Toks]" using
(GPS_iPP_CAS_int_simple (msqueLN l' γt') (Link γq γg γt') _ _ _
(l' >> 0) #0 0 #n t' Null
P' Q
(λ t1 s1, Link γq γg γt' false (l' >> link) γ' t1 s1 #0)
(λ t1 s1, Link γq γg γt' true (l' >> link) γ' t1 s1 #0)
- (λ _ _ _, True)%I γ')
- with "Pre [Post]";
+ (λ _ _ _, True)%I γ');
[done|..];
[solve_ndisj|done|solve_ndisj|by left|by right|by right|..].
- { (* iRC11 proofmode *)
- iNext. iIntros (b t0 s0 v0) "PP". iApply "Post".
- iExact "PP".
- }
{ iSplitL "oL'"; [by iFrame|].
iSplitL ""; last iSplitL ""; last by iFrame.
{ iRCRevert "".
@@ -830,11 +825,9 @@ Proof.
iDestruct "Queue" as "[oH oT]".
iDestruct "oT" as (tl vl γl) "oT".
iwp_bind (_ <-ʳᵉˡ _)%E.
- iwpApply with "oV5 sV5 []" intros (Ψ) "Pre Post" using
- (GPS_iPP_Write (msqueQN q) (Tail γq γg) _ _ _ _ (() : unitProtocol) _ #n)
- with "Pre [-]";
+ iwpApply with "oV5 sV5 []" using
+ (GPS_iPP_Write (msqueQN q) (Tail γq γg) _ _ _ _ (() : unitProtocol) _ #n);
[done|solve_ndisj|done|done|by right|done|..].
- { iIntros "!>" (?) "Q". by iApply "Post". }
{ iFrame "oT". simpl. iRCRevert "PPn".
iIntros "#PPn !>" (tl2 ?) "LL !>".
iExists n. iSplit; [done|]. rewrite (shift_0 n).
@@ -861,10 +854,9 @@ Proof.
iIntros "!>". iwp_case.
(* free the node *)
iwp_bind (delete _)%E.
- iwpApply with "oV5 sV5 [H† oN oD]" intros (Ψ) "Pre POST" using
- (wp_delete _ tid 2 _ [ #0; #v]) with "Pre [-]";
+ iwpApply with "oV5 sV5 [H† oN oD]" using
+ (wp_delete _ tid 2 _ [ #0; #v]);
[done|done|done|..].
- { iIntros "!> _". by iApply "POST". }
{ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame "oN oD".
iLeft. by iFrame. }
@@ -951,11 +943,9 @@ Proof.
iDestruct "oH" as (th vh γh) "PPh".
iwp_bind (!ᵃᶜ #(q >> 0))%E.
iwpApply with
- "oTV sV" intros (Ψ) "Pre Post" using
- (GPS_iPP_Read (msqueQN q) _ (Head γq γg false (q >> head) γh))
- with "Pre [Post]";
+ "oTV sV" using
+ (GPS_iPP_Read (msqueQN q) _ (Head γq γg false (q >> head) γh));
[done|solve_ndisj|done|done|by right|..].
- { iNext. iIntros (t1 s1 v1) "PP". iApply "Post". iFrame "PP". }
{ iFrame "PPh". iRCRevert "".
(* iRC11 proofmode *)
iIntros "!>" (t' [] v' Lt') "!>". iSplit; iIntros "oH !>".
@@ -969,10 +959,9 @@ Proof.
(* read node's link *)
iwp_bind (!ᵃᶜ #(s >> 0))%E.
- iwpApply with "oTV sV" intros (Ψ) "Pre Post" using
- (GPS_iPP_Read (msqueLN s γt) _ (Link γq γg γt false (s >> link) γ'))
- with "Pre [Post]"; [done|solve_ndisj|done|done|by right|..].
- { iNext. iIntros (t2 s2 v2) "PP". iApply "Post". iFrame "PP". }
+ iwpApply with "oTV sV" using
+ (GPS_iPP_Read (msqueLN s γt) _ (Link γq γg γt false (s >> link) γ'));
+ [done|solve_ndisj|done|done|by right|..].
{ iFrame "PPs". iRCRevert "".
(* iRC11 proofmode *)
iIntros "!>" (????) "!>". iSplit; iIntros "L !>";iApply (Link_dup with "L"). }
@@ -1013,17 +1002,15 @@ Proof.
(λ _ _, ∃ v : lit, (s2 >> data) ↦{1} #v ∗
∃ γt', (∃ eid Ve, VMap_snapv γq γt' eid ∗ EMap_snap γg eid (Enq v) Ve) ∗
TokGRv γt')%I.
- iwpApply with "oTV sV" intros (Ψ) "Pre Post" using
+ iwpApply with "oTV sV" using
(GPS_iPP_CAS_live_loc (msqueQN q) (Head γq γg) _ _ _ (q >> 0%nat) _
s #s2 th () True%I True%I Q
(λ t0 s0, Head γq γg false (q >> head) γh t0 s0 #s)%I
(λ t0 s0, Head γq γg true (q >> head) γh t0 s0 #s)%I
(λ _ _ _, True)%I γh _ _ (Ei ∖ ↑msqueQN q ∖ ↑msqueLN s γt)
- (λ l', Ei ∖ ↑msqueQN q ∖ ↑(nroot.@"msqueueLN".@l')))
- with "Pre [Post]";
+ (λ l', Ei ∖ ↑msqueQN q ∖ ↑(nroot.@"msqueueLN".@l')));
[done|solve_ndisj|done|done|solve_ndisj|intros; solve_ndisj
|by left|by right|by right|..].
- { iNext. iIntros (b t0 s0 v0) "PP". iApply "Post". iExact "PP". }
{ iSplitL ""; [iFrame "PPh"|].
iSplitL ""; [done|].
iSplitR ""; [|iSplitL ""].