From a10b384d184ad5db9328021b539e7e39fd2fcf11 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 2 Dec 2020 16:28:57 +0100
Subject: [PATCH] Used equivalence lemma for iProto_message for proof of
 choice_equiv

---
 theories/channel/channel.v | 38 ++++++++------------------------------
 theories/channel/proto.v   |  2 +-
 2 files changed, 9 insertions(+), 31 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 58ee99f..646de10 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -161,40 +161,18 @@ Section channel.
         (p11 p12 p21 p22 : iProto Σ) :
     ⌜a1 = a2⌝ -∗ ((P11 ≡ P12):iProp Σ) -∗ (P21 ≡ P22) -∗
     ▷ (p11 ≡ p12) -∗ ▷ (p21 ≡ p22) -∗
-    (iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22).
+    iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22.
   Proof.
     iIntros (->) "#HP1 #HP2 #Hp1 #Hp2".
-    rewrite iProto_message_equivI.
-    iSplit; [ done | ].
-    iIntros (v lp).
-    rewrite iMsg_exist_eq iMsg_base_eq /=.
-    iApply prop_ext; iIntros "!>"; iSplit.
-    - iDestruct 1 as (b Hbeq) "[Hp HP]".
-      iExists b. rewrite Hbeq.
-      destruct lp as [lp]. destruct b.
-      + iRewrite -"HP1".
-        iSplit; [ done | ]. iFrame "HP".
-        iIntros "!>".
-        by iRewrite -"Hp1".
-      + iRewrite -"HP2".
-        iSplit; [ done | ]. iFrame "HP".
-        iIntros "!>".
-        by iRewrite -"Hp2".
-    - iDestruct 1 as (b Hbeq) "[Hp HP]".
-      iExists b. rewrite Hbeq.
-      destruct lp as [lp].
-      destruct b.
-      + iRewrite "HP1".
-        iSplit; [ done | ]. iFrame "HP".
-        iIntros "!>".
-        by iRewrite "Hp1".
-      + iRewrite "HP2".
-        iSplit; [ done | ]. iFrame "HP".
-        iIntros "!>".
-        by iRewrite "Hp2".
+    rewrite /iProto_choice. iApply iProto_message_equiv; [ eauto | | ].
+    - iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
+      destruct b;
+        [ iRewrite -"HP1"; iFrame "H Hp1" | iRewrite -"HP2"; iFrame "H Hp2" ].
+    - iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
+      destruct b;
+        [ iRewrite "HP1"; iFrame "H Hp1" | iRewrite "HP2"; iFrame "H Hp2" ].
   Qed.
 
-
   Lemma iProto_dual_choice a P1 P2 p1 p2 :
     iProto_dual (iProto_choice a P1 P2 p1 p2)
     ≡ iProto_choice (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index efc3cfe..fdd5b27 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -429,7 +429,7 @@ Section proto.
        ∃.. (xs1 : TT1), ⌜tele_app v1 xs1 = tele_app v2 xs2⌝ ∗
                         ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
                         tele_app P1 xs1) -∗
-      (<a1> m1)%proto ≡ (<a2> m2)%proto.
+      (<a1> m1) ≡ (<a2> m2).
   Proof.
     iIntros (Hm1 Hm2 Heq) "#Heq1 #Heq2".
     unfold MsgTele in Hm1. rewrite Hm1. clear Hm1.
-- 
GitLab