From f5bd0369adf78643b44ad5321d804555b03d6c0c Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 30 Apr 2019 14:19:58 +0200
Subject: [PATCH] Changed branching to be over sides

---
 theories/encodings/branching.v       | 4 ++--
 theories/examples/branching_proofs.v | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/encodings/branching.v b/theories/encodings/branching.v
index f0ce12e..d94b438 100644
--- a/theories/encodings/branching.v
+++ b/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) Φ :
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index 5d80c1e..21fb687 100644
--- a/theories/examples/branching_proofs.v
+++ b/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".
-- 
GitLab