Solve `[Post]` subgoals automatically.

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 ""].