better tactics

logsem · Aug 12, 2024 · 390ef93 · 390ef93
1 parent 59e17e0
commit 390ef93
Show file tree

Hide file tree

Showing 3 changed files with 188 additions and 4 deletions.
diff --git a/theories/con_prob_lang/wp_tactics.v b/theories/con_prob_lang/wp_tactics.v
@@ -329,7 +329,99 @@ Tactic Notation "wp_apply" open_constr(lem) :=
                     ltac:(fun cont => fail).
 Tactic Notation "wp_smart_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl)
-                    ltac:(fun cont => wp_pure _; []; cont ()).
+                           ltac:(fun cont => wp_pure _; []; cont ()).
+
+(** Better notations :) *)
+Tactic Notation "wp_apply" open_constr(lem) "as" constr(pat) :=
+  wp_apply lem; last iIntros pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
+
+
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" constr(pat) :=
+  wp_smart_apply lem; last iIntros pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
 
 Section heap_tactics.
   Context `{GwpTacticsBase Σ A hlc gwp, GwpTacticsBind Σ A hlc gwp, !GwpTacticsHeap Σ A laters gwp}.

diff --git a/theories/coneris/lib/par.v b/theories/coneris/lib/par.v
@@ -28,8 +28,8 @@ Proof.
   iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
   wp_apply (spawn_spec parN with "Hf1"). iIntros (l) "Hl".
   wp_let. wp_bind (f2 _).
-  wp_apply (pgl_wp_wand with "Hf2"). iIntros (v) "H2". wp_let.
-  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
+  wp_apply (pgl_wp_wand with "Hf2") as (v) "H2". wp_let.
+  wp_apply (join_spec with "[$Hl]") as (w) "H1".
   iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
 Qed.
 

diff --git a/theories/prob_lang/wp_tactics.v b/theories/prob_lang/wp_tactics.v
@@ -300,7 +300,99 @@ Tactic Notation "wp_apply" open_constr(lem) :=
                     ltac:(fun cont => fail).
 Tactic Notation "wp_smart_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl)
-                    ltac:(fun cont => wp_pure _; []; cont ()).
+                           ltac:(fun cont => wp_pure _; []; cont ()).
+
+(** Better tactics :) *)
+Tactic Notation "wp_apply" open_constr(lem) "as" constr(pat) :=
+  wp_apply lem; last iIntros pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
+Tactic Notation "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
+    constr(pat) :=
+  wp_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
+
+
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" constr(pat) :=
+  wp_smart_apply lem; last iIntros pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
+Tactic Notation "wp_smart_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
+    constr(pat) :=
+  wp_smart_apply lem; last iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
 
 Section heap_tactics.
   Context `{GwpTacticsBase Σ A hlc gwp, GwpTacticsBind Σ A hlc gwp, !GwpTacticsHeap Σ A laters gwp}.