From e21a5733b0d410e73b87371d5838698879828e5a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 02:36:05 +0200
Subject: [PATCH] Add rule `iProto_le_branch`.
---
theories/channel/channel.v | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 6e4bb0c..4b7295c 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -174,6 +174,21 @@ Section channel.
by apply iProto_message_proper=> /= -[].
Qed.
+ Lemma iProto_le_branch a P1 P2 p1 p2 p1' p2' :
+ ▷ (P1 -∗ P1 ∗ iProto_le p1 p1') ∧ ▷ (P2 -∗ P2 ∗ iProto_le p2 p2') -∗
+ iProto_le (iProto_branch a P1 P2 p1 p2) (iProto_branch a P1 P2 p1' p2').
+ Proof.
+ iIntros "H". rewrite /iProto_branch. destruct a.
+ - iApply iProto_le_send'; iIntros "!>" (b) "HP /=".
+ iExists b; iSplit; [done|]. destruct b.
+ + iDestruct "H" as "[H _]". by iApply "H".
+ + iDestruct "H" as "[_ H]". by iApply "H".
+ - iApply iProto_le_recv'; iIntros "!>" (b) "HP /=".
+ iExists b; iSplit; [done|]. destruct b.
+ + iDestruct "H" as "[H _]". by iApply "H".
+ + iDestruct "H" as "[_ H]". by iApply "H".
+ Qed.
+
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec p :
{{{ True }}}
--
GitLab