Protocol equivalence

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).