A brute tp_apply tactic

F_mu_ref_conc/examples/counter.v

@@ -117,7 +117,7 @@ Section CG_Counter.
     ={E}=∗ j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros (HNE) "#Hspec Hx Hl Hj".
-    iMod (steps_with_lock _ _ _ K _ _ _ _ UnitV UnitV _ _ with "Hspec Hx Hl Hj") as "Hj"; last by iFrame.
+    tp_apply j (steps_with_lock _ _ _ K _ _ _ _ UnitV UnitV _) with "Hx Hl"; last by iFrame.
     { iIntros (K') "#Hspec Hx Hj /=".
       iApply (steps_CG_increment E with "Hspec Hx"); auto. }
     Unshelve. all: trivial.
@@ -251,7 +251,8 @@ Section CG_Counter.
     rewrite ?empty_env_subst /CG_counter /FG_counter.
     iApply fupd_wp.
     tp_bind j newlock.
-    iMod (steps_newlock with "Hspec Hj") as (l) "[Hj Hl]"; eauto.
+    tp_apply j steps_newlock.
+    iDestruct "Hj" as (l) "[Hj Hl]".
     tp_rec j.
     asimpl. rewrite CG_locked_increment_subst /=.
     rewrite counter_read_subst /=.
@@ -304,7 +305,8 @@ Section CG_Counter.
       destruct (decide (n = n')) as [|Hneq]; subst.
       + (* CAS succeeds *)
         (* In this case, we perform increment in the coarse-grained one *)
-        iMod (steps_CG_locked_increment with "Hspec Hcnt' Hl Hj") as "[Hj [Hcnt' Hl]]"; first by solve_ndisj.
+        tp_apply j steps_CG_locked_increment with "Hcnt' Hl"
+            as "[Hcnt' Hl]".             
         iApply (wp_cas_suc with "[Hcnt]"); auto.
         iNext. iIntros "Hcnt".
         iMod ("Hclose" with "[Hl Hcnt Hcnt']").
@@ -330,7 +332,7 @@ Section CG_Counter.
       iNext. 
       iApply wp_atomic; eauto.
       iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
-      iMod (steps_counter_read with "Hspec Hcnt' Hj") as "[Hj Hcnt']"; first by solve_ndisj.
+      tp_apply j steps_counter_read with "Hcnt'" as "Hcnt'".
       iApply (wp_load with "[Hcnt]"); eauto. 
       iNext. iIntros "Hcnt".
       iMod ("Hclose" with "[Hl Hcnt Hcnt']").

F_mu_ref_conc/examples/lock.v

@@ -133,9 +133,8 @@ Section proof.
     iIntros (HNE H1 H2) "#Hspec HP Hl Hj".
     tp_rec j; eauto using to_of_val.
     asimpl. rewrite H1.
-    (* TODO: a tp_apply tactic similar to that of iApply *)
     tp_bind j (App acquire (Loc l)).
-    iMod (steps_acquire _ _ j with "Hspec Hl Hj") as "[Hj Hl]"; eauto.
+    tp_apply j steps_acquire with "Hl" as "Hl".
     tp_rec j.
     asimpl. rewrite H1.
     tp_bind j (App e _).
@@ -144,7 +143,7 @@ Section proof.
     tp_rec j; eauto using to_of_val.
     asimpl.
     tp_bind j (App release _).
-    iMod (steps_release with "Hspec Hl Hj") as "[Hj Hl]"; auto.
+    tp_apply j steps_release with "Hl" as "Hl".
     tp_rec j.
     tp_normalise j. asimpl.
     by iFrame.

F_mu_ref_conc/examples/stack/CG_stack.v

@@ -150,10 +150,10 @@ Section CG_Stack.
   Proof.
     iIntros (?) "#Hspec Hst Hl Hj".
     unfold CG_locked_push.
-    (* TODO would be nice to be able to determine that e := Loc l for instance *)
-    iMod (steps_with_lock _ _ _ _ _ _ _ _ UnitV with "Hspec Hst Hl Hj") as "Hj"; auto. 
-    iIntros (K') "#Hspec HQ Hj".
-    iApply (steps_CG_push with "Hspec HQ"); auto. 
+    tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ UnitV) with "Hst Hl" as "[Hst $]"; [auto | | ].
+    - iIntros (K') "#Hspec Hst Hj".
+      iApply (steps_CG_push with "Hspec Hst"); auto.
+    - by iFrame.
   Qed.
 
   Global Opaque CG_locked_push.
@@ -255,11 +255,11 @@ Section CG_Stack.
     ={E}=∗ j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop.
-    iMod (steps_with_lock _ _ _ _ _ _ _ _ (InjRV w) UnitV _ _
-          with "Hspec Hx Hl Hj") as "Hj"; auto.
-    iIntros (K') "#Hspec Hx Hj".
-    iApply (steps_CG_pop_suc with "Hspec Hx Hj"). trivial. 
-    Unshelve. all: trivial.
+    tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ (InjRV w) UnitV)
+             with "Hx Hl" as "[Hx $]"; first auto.
+    - iIntros (K') "#Hspec Hx Hj".
+      iApply (steps_CG_pop_suc with "Hspec Hx Hj"). trivial.
+    - by iFrame.
   Qed.
 
   Lemma steps_CG_locked_pop_fail E ρ j K st l :
@@ -269,11 +269,11 @@ Section CG_Stack.
     ={E}=∗ j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop.
-    iMod (steps_with_lock _ _ _ _ _ _ _ _ (InjLV UnitV) UnitV _ _
-          with "Hspec Hx Hl Hj") as "Hj"; auto.
-    iIntros (K') "#Hspec Hx Hj /=".
-    iApply (steps_CG_pop_fail with "Hspec Hx Hj"). trivial. 
-    Unshelve. all: trivial.
+    tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ (InjLV UnitV) UnitV)
+             with "Hx Hl" as "[Hx Hl]"; first auto.
+    - iIntros (K') "#Hspec Hx Hj /=".
+      iApply (steps_CG_pop_fail with "Hspec Hx Hj"). trivial.
+    - by iFrame.
   Qed.
 
   Global Opaque CG_locked_pop.
@@ -316,13 +316,13 @@ Section CG_Stack.
     ={E}=∗ j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_snap.
-    iMod (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _
-          with "Hspec Hx Hl Hj") as "Hj"; auto. 
-    iIntros (K') "#Hspec Hx Hj".
-    tp_rec j.
-    tp_load j. tp_normalise j.
-    by iFrame.
-    Unshelve. all: trivial.
+    tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ v UnitV)
+             with "Hx Hl" as "[Hx $]"; first auto.
+    - iIntros (K') "#Hspec Hx Hj".
+      tp_rec j.
+      tp_load j. tp_normalise j.
+      by iFrame.
+    - by iFrame.
   Qed.
 
   Global Opaque CG_snap.

F_mu_ref_conc/examples/stack/refinement.v

@@ -63,8 +63,7 @@ Section Stack_refinement.
        end) with (⊤ ∖ ↑stackN) by reflexivity.
     replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (rewrite CG_iter_of_val; done).        
     tp_bind j (App (CG_snap _ _) ())%E.
-    iMod (steps_CG_snap with "Hs Hst' Hl Hj") as "(Hj & Hst' & Hl)";
-      first solve_ndisj.
+    tp_apply j steps_CG_snap with "Hst' Hl" as "[Hst' Hl]".
     tp_normalise j.
     close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]".
 
@@ -88,7 +87,7 @@ Section Stack_refinement.
       iNext.
       iApply fupd_wp.
       rewrite CG_iter_of_val /=.
-      iMod (steps_CG_iter_end with "Hs Hj") as "Hj"; first solve_ndisj.
+      tp_apply j steps_CG_iter_end.
       iModIntro.
       iApply wp_value; auto.
       iExists UnitV. iFrame. eauto.
@@ -99,8 +98,8 @@ Section Stack_refinement.
       wp_bind (Fst _). iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=).
       iNext. iModIntro.
       wp_bind (App (of_val f1) _).
-      rewrite CG_iter_of_val.
-      iMod (steps_CG_iter with "Hs Hj") as "Hj"; first solve_ndisj.
+      rewrite CG_iter_of_val.      
+      tp_apply j steps_CG_iter.
       rewrite CG_iter_subst.
       tp_bind j (App (of_val f2) _).
       iSpecialize ("Hff" $! (y1, y2) with "Hy"). 
@@ -152,10 +151,11 @@ Section Stack_refinement.
     iInv stackN as (istk2 v h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".    (* TODO : why can we remove the later here?*) 
     destruct (decide (istk = istk2)) as [Heq|Hneq]; first subst istk.
     * (* Case CAS succeeds *)
-      iMod (steps_CG_locked_push _ _ j K st' v2 with "Hs Hst' Hl Hj") as "[Hj [Hst' Hl]]"; first solve_ndisj.
+      tp_apply j (steps_CG_locked_push _ _ j K st' v2)
+               with "Hst' Hl" as "[Hst' Hl]".
       iApply (wp_cas_suc with "Hst"); auto.
       iNext. iIntros "Hst".
-
+      
       iMod (stack_owns_alloc with "[$Hoe $Histk']") as "[Hoe Histk']".
       iMod ("Hclose" with "[HLK Hst Hoe Hl Hst' Histk']").
       { iNext. rewrite /sinv. iExists _,_,_.
@@ -195,8 +195,7 @@ Section Stack_refinement.
     (* Checking whether the stack is empty *)
     rewrite {2}StackLink_unfold.
     iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=.
-    + iMod (steps_CG_locked_pop_fail with "Hs Hst' Hl Hj")
-        as "(Hj & Hstk' & Hl)"; first solve_ndisj.
+    + tp_apply j steps_CG_locked_pop_fail with "Hst' Hl" as "[Hstk' Hl]".
       close_sinv "Hclose" "[Hoe Hstk' Hst Hl]".
       wp_bind (Unfold _). iApply wp_fold; first by auto using to_of_val.    iNext.
       iModIntro. iApply wp_rec; first auto using to_of_val. iNext. asimpl.
@@ -248,8 +247,8 @@ Section Stack_refinement.
         iDestruct "HLK'" as (yn1 yn2 zn1 zn2)
                                    "[% [% [#Hrel HLK'']]]"; simplify_eq/=.
         (* Now we have proven that specification can also pop. *)
-        iMod (steps_CG_locked_pop_suc with "Hs Hst' Hl Hj")
-                as "[Hj [Hst' Hl]]"; first solve_ndisj.
+        tp_apply j steps_CG_locked_pop_suc with "Hst' Hl"
+                                           as "[Hst' Hl]".
         iMod ("Hclose" with "[-Hj]") as "_".
         { iNext. 
           iPoseProof "HLK''" as "HLK2".
@@ -296,7 +295,8 @@ Section Stack_refinement.
     iApply fupd_wp.
     tp_tlam j.
     tp_bind j newlock.
-    iMod (steps_newlock with "Hspec Hj") as (l') "[Hj Hl']"; eauto.
+    tp_apply j steps_newlock.
+    iDestruct "Hj" as (l') "[Hj Hl']".
     tp_normalise j.
     tp_rec j.
     tp_alloc j as stk' "Hstk'".

F_mu_ref_conc/tactics.v

 From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Import coq_tactics sel_patterns.
 From iris.proofmode Require Export tactics.
 From iris_logrel.F_mu_ref_conc Require Import rules rules_binary.
 From iris_logrel.F_mu_ref_conc Require Export lang.
@@ -863,6 +863,77 @@ Tactic Notation "tp_alloc" constr(j) "as" ident(j') constr(H) :=
 Tactic Notation "tp_alloc" constr(j) "as" ident(j') :=
   let H := iFresh in tp_alloc j as j' H.
 
+
+(**************************)
+(* tp_apply *)
+
+Fixpoint print_sel (ss : list sel_pat) (s : string) :=
+  match ss with
+  | nil => s
+  | SelPure :: ss' => (String "%" (String " " (print_sel ss' s)))
+  | SelPersistent :: ss' =>  (String "#" (print_sel ss' s))
+  | SelSpatial :: ss' => (* no clue :( *) (print_sel ss' s)
+  | SelName n :: ss' => append n (String " " (print_sel ss' s))
+  end.
+
+Ltac print_sel ss :=
+  lazymatch type of ss with
+  | list sel_pat => eval vm_compute in (print_sel ss "")
+  | string => ss
+  end.
+
+Definition appP (ss : list sel_pat) (Hj Hs : string) :=
+  cons (SelName Hs) (app ss [SelName Hj]).
+
+Definition add_elim_pat (pat : string) (Hj : string) :=
+  match pat with
+  | EmptyString => Hj
+  | _ => append (String "[" (append Hj (String " " pat))) "]"
+  end.
+
+Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) "as" constr(Hr) :=
+  iStartProof;
+  let rec find Γ j :=
+    match Γ with
+    | Esnoc ?Γ ?Hj ?P =>
+      lazymatch P with
+      | (j ⤇ _)%I => Hj
+      | _ => find Γ j
+      end
+    | Enil => fail "tp_apply: cannot find " j " ⤇ _ "
+    end in
+  let rec findSpec Γp Γs :=
+    match Γp with
+    | Esnoc ?Γ ?Hspec ?P =>
+      lazymatch P with
+      | (spec_ctx _)%I => Hspec
+      | _ => findSpec Γ Γs
+      end
+    | Enil =>
+      match Γs with
+      | Enil => fail "tp_apply: cannot find spec_ctx _"
+      | _ => findSpec Γs Enil
+      end
+    end in
+  match goal with
+  | |- of_envs (Envs ?Γp ?Γs) ⊢ ?Q =>
+    let Hj := (find Γs j) in
+    let Hspec := findSpec Γp Γs in
+    let pat := eval vm_compute in (appP (sel_pat.parse Hs) Hj Hspec) in
+    let pats := print_sel pat in 
+    let elim_pats := eval vm_compute in (add_elim_pat Hr Hj) in
+    iMod (lem with pats) as elim_pats; first by solve_ndisj
+  end.
+
+Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) := tp_apply j lem with Hs as "".
+
+Tactic Notation "tp_apply" constr(j) open_constr(lem) "as" constr(Hr) := tp_apply j lem with "" as Hr.
+
+Tactic Notation "tp_apply" constr(j) open_constr(lem) := tp_apply j lem with "" as "".
+
+(**************************)
+(* / tp_apply *)
+
 Section test.
 Context `{heapIG Σ, !cfgSG Σ}.
 
@@ -872,15 +943,32 @@ Notation LamV e := (RecV (e.[ren (+1)])).
 
 Lemma alloc_test E K j n ρ :
   nclose specN ⊆ E →
-  j ⤇ fill K (App (Lam (Store (Var 0) (#n (n + 10)))) (Alloc (#n n))) -∗
-  spec_ctx ρ ={E}=∗ True.
+  spec_ctx ρ -∗
+  j ⤇ fill K (App (Lam (Store (Var 0) (#n (n + 10)))) (Alloc (#n n))) ={E}=∗ True.
 Proof.
-  iIntros (?) "Hj #?".
+  iIntros (?) "#? Hj".
   tp_alloc j as l. Undo.
   tp_alloc j as l "Hl". tp_normalise j.
   done.
 Qed.
 
+Lemma steps_release E ρ j K l b:
+    nclose specN ⊆ E →
+    spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App Unit (Loc l))
+    ={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ (#♭v false).
+admit. Admitted.
+
+Lemma test_apply E ρ j b K l:
+  nclose specN ⊆ E →
+  spec_ctx ρ -∗ 
+  l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App Unit (Loc l))
+  -∗ |={E}=> True.
+Proof.
+  iIntros (?) "#Hs Hst Hj".
+  tp_apply j steps_release with "Hst" as "Hl".
+  done.
+Qed.
+
 Lemma test1 E1 j K l n ρ :
   nclose specN ⊆ E1 →
   j ⤇ fill K (App (Lam (Store (Loc l) (BinOp Add (Nat 1) (Var 0)))) (Load (Loc l))) -∗