From 0eb2c8f479cb18db51f87e25001b7a45ffa4251a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Nov 2019 22:56:45 +0100
Subject: [PATCH] Some missing internal equality lemmas for protocols.
---
theories/channel/proto_model.v | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index aed495a..606c496 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -115,6 +115,16 @@ Proof.
rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
by rewrite bi.discrete_fun_equivI bi.discrete_eq.
Qed.
+Lemma proto_message_end_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc :
+ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a pc ≡ proto_end ⊢@{SPROP} False.
+Proof.
+ trans (proto_unfold (proto_message a pc) ≡ proto_unfold proto_end : SPROP)%I.
+ { iIntros "Heq". by iRewrite "Heq". }
+ by rewrite /proto_message !proto_unfold_fold bi.option_equivI.
+Qed.
+Lemma proto_end_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc :
+ proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a pc ⊢@{SPROP} False.
+Proof. by rewrite bi.internal_eq_sym proto_message_end_equivI. Qed.
Definition proto_cont_map
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP', !Cofe A, !Cofe B}
--
GitLab