Add wp_if_join tactic (#532)

I add a tactic, `wp_if_join`, that allows you to 'join' both branches of
an if-statement into a single assertion by showing that both branches
make said assertion hold.

Given the program below (and assertion `A`)
```
if b { S1; } else { S2; } // no `else` is handled trivially by Goose.
// assertion `A`
S3;
```

By using the tactic `wp_if_join <assertion> [with <ipat>]` (leaving off
the `with` to provide no spatial hypotheses), the goal is split into
three subgoals:
1. Proving that `S1` results in `A` holding,
2. Proving that `S2` results in `A` holding, and
3. Proving the remainder of the program, `S3`, assuming that `A` holds.

---------

Signed-off-by: Cody Rivera <[email protected]>

Author: codyjrivera

new/golang/theory/auto.v

@@ -343,6 +343,28 @@ Ltac wp_if_destruct :=
       end
   end.
 
+(** [wp_if_join] joins two branches of an if expression into a shared assertion
+    [asn], which becomes available for the proof of subsequent statements.
+
+    Usage:
+        wp_if_join asn with pat
+        wp_if_join asn
+
+    [asn] is the join assertion (a function from value to iProp). [pat] is an
+    optional Iris intro pattern specifying spatial hypotheses needed to prove
+    the if expression. The goal is split into three subgoals:
+        1) Prove [asn] in the true branch.
+        2) Prove [asn] in the false branch.
+        3) Prove the remainder with [asn] as an assumption.
+**)
+Tactic Notation "wp_if_join" constr(asn) "with" constr(pat) :=
+  wp_bind (if: _ then _ else _)%E;
+  wp_pures;
+  iApply (wp_wand _ _ _ asn with pat)%I;
+  [ wp_if_destruct | ].
+
+Tactic Notation "wp_if_join" constr(asn) := wp_if_join asn with "[]".
+
 Ltac wp_end :=
   wp_pures;
   repeat iModIntro;

new/proof/github_com/goose_lang/goose/testdata/examples/unittest.v

@@ -384,6 +384,47 @@ Proof.
   - wp_end.
 Qed.
 
+Lemma wp_ifJoinDemo_if_join_tactic (arg1 arg2: bool) :
+  {{{ is_pkg_init unittest }}}
+    @! unittest.ifJoinDemo #arg1 #arg2
+  {{{ RET #(); True }}}.
+Proof.
+  wp_start.
+  wp_auto.
+  iPersist "arg2".
+  wp_if_join (λ v, ⌜v = execute_val⌝ ∗
+                   ∃ (sl: slice.t) (xs: list w64),
+                       "arr" ∷ arr_ptr ↦ sl ∗
+                       "Hsl" ∷ sl ↦* xs ∗
+                       "Hsl_cap" ∷ own_slice_cap w64 sl (DfracOwn 1))%I
+             with "[arr]".
+  {
+    wp_apply (wp_slice_literal (V:=w64)) as "%sl [Hsl _]".
+    wp_apply (wp_slice_append (V:=w64) with "[Hsl]") as "%sl1 (Hsl & Hsl_cap & _)".
+    {
+      iFrame.
+      iDestruct (own_slice_nil) as "$".
+      iDestruct (own_slice_cap_nil) as "$".
+    }
+    iSplit; [ done | ].
+    iFrame.
+  }
+  {
+    iSplit; [ done | ].
+    iFrame.
+    iExists [].
+    iDestruct (own_slice_nil) as "$".
+    iDestruct (own_slice_cap_nil) as "$".
+  }
+  iIntros (v) "[% @]". subst.
+  wp_auto.
+  wp_if_destruct.
+  - wp_apply (wp_slice_literal (V:=w64)) as "%sl2 [Hsl2 _]".
+    wp_apply (wp_slice_append (V:=w64) with "[$Hsl $Hsl_cap $Hsl2]") as "%sl1 (Hsl & Hsl_cap & _)".
+    wp_end.
+  - wp_end.
+Qed.
+
 Lemma wp_repeatLocalVars :
   {{{ is_pkg_init unittest }}}
     @! unittest.repeatLocalVars #()