Changed branching to be over sides

theories/encodings/branching.v

@@ -57,7 +57,7 @@ Section branching_specs.
       then "b1"
       else "b2".
 
-  Lemma select_st_spec st1 st2 γ c s (b : bool) :
+  Lemma select_st_spec st1 st2 γ c s (b : side) :
     {{{ ⟦ c @ s : st1 <+> st2 ⟧{N,γ} }}}
       select c #s #b
     {{{ RET #(); ⟦ c @ s : (if b then st1 else st2) ⟧{N,γ} }}}.
@@ -68,7 +68,7 @@ Section branching_specs.
     wp_apply (send_st_spec N bool with "[$Hst //]");
     iIntros "Hstl".
     iApply "HΦ".
-    eauto.
+    by destruct b.
   Qed.
 
   Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) Φ :

theories/examples/branching_proofs.v

@@ -14,14 +14,14 @@ Section BranchingExampleProofs.
     {{{ True }}}
       branch_example b
     {{{ v, RET v; match b with
-                  | true => ⌜v = #5⌝
-                  | false => ⌜v = #()⌝
+                  | Left => ⌜v = #5⌝
+                  | Right => ⌜v = #()⌝
                   end }}}.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /branch_example.
     wp_apply (new_chan_st_spec N
-      ((<?> v @ ⌜v = 5⌝, TEnd)  <+> (TEnd)))=> //;
+      ((<?> v @ ⌜v = 5⌝, TEnd) <+> (TEnd)))=> //;
     iIntros (c γ) "[Hstl Hstr]".
     wp_apply (select_st_spec with "Hstl");
     iIntros "Hstl".