Added equivalence lemmas for iProto_message and iProto_choice

_CoqProject

@@ -17,6 +17,7 @@ theories/channel/proto.v
 theories/channel/channel.v
 theories/channel/proofmode.v
 theories/examples/basics.v
+theories/examples/equivalence.v
 theories/examples/sort.v
 theories/examples/sort_br_del.v
 theories/examples/sort_fg.v

theories/channel/channel.v

@@ -157,6 +157,22 @@ Section channel.
     Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_choice Σ a).
   Proof. solve_proper. Qed.
 
+  Lemma iProto_choice_equiv a1 a2 (P11 P12 P21 P22 : iProp Σ)
+        (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.
+  Proof.
+    iIntros (->) "#HP1 #HP2 #Hp1 #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).
@@ -261,10 +277,6 @@ Section channel.
     {{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ P x }}; p x) ∨
                   (∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
   Proof.
-    assert (∀ w lp (m : TT → iMsg Σ),
-      iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp)) as iMsg_texist.
-    { intros w lp m. clear v P p. rewrite /iMsg_texist iMsg_exist_eq.
-      induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH. }
     rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
     wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
@@ -276,7 +288,8 @@ Section channel.
         iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
       wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
       iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
-      rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
+      rewrite iMsg_base_eq.
+      iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
       wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
       iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
@@ -288,7 +301,8 @@ Section channel.
         iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
       wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
       iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
-      rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
+      rewrite iMsg_base_eq.
+      iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
       wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
       iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".

theories/channel/proofmode.v

@@ -23,11 +23,6 @@ Ltac solve_proto_contractive :=
     first [f_contractive; simpl in * | f_equiv | f_dist_le]).
 
 (** * Normalization of protocols *)
-Class MsgTele {Σ} {TT : tele} (m : iMsg Σ)
-    (tv : TT -t> val) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ) :=
-  msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
-Hint Mode MsgTele ! - ! - - - : typeclass_instances.
-
 Class ActionDualIf (d : bool) (a1 a2 : action) :=
   dual_action_if : a2 = if d then action_dual a1 else a1.
 Hint Mode ActionDualIf ! ! - : typeclass_instances.
@@ -61,14 +56,6 @@ Section classes.
   Implicit Types m : iMsg Σ.
   Implicit Types P : iProp Σ.
 
-  Global Instance msg_tele_base v P p :
-    MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
-  Proof. done. Qed.
-  Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ) tv tP tp :
-    (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
-    MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
-  Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
-
   Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
   Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
 

theories/channel/proto.v

@@ -137,6 +137,13 @@ Notation "'∃..' x .. y , m" :=
   (at level 200, x binder, y binder, right associativity,
    format "∃..  x  ..  y ,  m") : msg_scope.
 
+Lemma iMsg_texist_exist {Σ V} {TT : tele} w lp (m : TT → iMsg Σ V) :
+  iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp).
+Proof.
+  rewrite /iMsg_texist iMsg_exist_eq.
+  induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH.
+Qed.
+
 (** * Operators *)
 Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
 Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
@@ -181,6 +188,11 @@ Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
   (at level 200, x1 closed binder, xn closed binder, m at level 200,
    format "<?..  x1  ..  xn >  m") : proto_scope.
 
+Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
+    (tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
+  msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
+Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
+
 (** * Operations *)
 Program Definition iMsg_map {Σ V}
     (rec : iProto Σ V → iProto Σ V) (m : iMsg Σ V) : iMsg Σ V :=
@@ -348,6 +360,7 @@ Section proto.
     (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧
       (∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
   Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
+
   Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
     (<a> m) ≡ END ⊢@{SPROP} False.
   Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
@@ -385,6 +398,14 @@ Section proto.
     Proper (pointwise_relation _ (≡) ==> (≡)) (@iMsg_exist Σ V A).
   Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
 
+  Global Instance msg_tele_base (v:V) (P : iProp Σ) (p : iProto Σ V) :
+    MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
+  Proof. done. Qed.
+  Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ V) tv tP tp :
+  (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
+  MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
+  Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
+
   Global Instance iProto_message_ne a :
     NonExpansive (iProto_message (Σ:=Σ) (V:=V) a).
   Proof. rewrite iProto_message_eq. solve_proper. Qed.
@@ -392,6 +413,46 @@ Section proto.
     Proper ((≡) ==> (≡)) (iProto_message (Σ:=Σ) (V:=V) a).
   Proof. apply (ne_proper _). Qed.
 
+  Lemma iProto_message_equiv {TT1 TT2 : tele} a1 a2
+        (m1 m2 : iMsg Σ V)
+        (v1 : TT1 -t> V) (v2 : TT2 -t> V)
+        (P1 : TT1 -t> iProp Σ) (P2 : TT2 -t> iProp Σ)
+        (prot1 : TT1 -t> iProto Σ V) (prot2 : TT2 -t> iProto Σ V) :
+    MsgTele m1 v1 P1 prot1 →
+    MsgTele m2 v2 P2 prot2 →
+    ⌜ a1 = a2 ⌝ -∗
+    (■ ∀.. (xs1 : TT1), tele_app P1 xs1 -∗
+       ∃.. (xs2 : TT2), ⌜tele_app v1 xs1 = tele_app v2 xs2⌝ ∗
+                        ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
+                        tele_app P2 xs2) -∗
+    (■ ∀.. (xs2 : TT2), tele_app P2 xs2 -∗
+       ∃.. (xs1 : TT1), ⌜tele_app v1 xs1 = tele_app v2 xs2⌝ ∗
+                        ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
+                        tele_app P1 xs1) -∗
+      (<a1> m1) ≡ (<a2> m2).
+  Proof.
+    iIntros (Hm1 Hm2 Heq) "#Heq1 #Heq2".
+    unfold MsgTele in Hm1. rewrite Hm1. clear Hm1.
+    unfold MsgTele in Hm2. rewrite Hm2. clear Hm2.
+    rewrite iProto_message_eq proto_message_equivI.
+    iSplit; [ done | ].
+    iIntros (v p').
+    do 2 rewrite iMsg_texist_exist.
+    rewrite iMsg_base_eq /=.
+    iApply prop_ext.
+    iIntros "!>". iSplit.
+    - iDestruct 1 as (xs1 Hveq1) "[Hrec1 HP1]".
+      iDestruct ("Heq1" with "HP1") as (xs2 Hveq2) "[Hrec2 HP2]".
+      iExists xs2. rewrite -Hveq1 Hveq2.
+      iSplitR; [ done | ]. iSplitR "HP2"; [ | done ].
+      iRewrite -"Hrec1". iApply later_equivI. iIntros "!>". by iRewrite "Hrec2".
+    - iDestruct 1 as (xs2 Hveq2) "[Hrec2 HP2]".
+      iDestruct ("Heq2" with "HP2") as (xs1 Hveq1) "[Hrec1 HP1]".
+      iExists xs1. rewrite -Hveq2 Hveq1.
+      iSplitR; [ done | ]. iSplitR "HP1"; [ | done ].
+      iRewrite -"Hrec2". iApply later_equivI. iIntros "!>". by iRewrite "Hrec1".
+  Qed.
+
   (** Helpers *)
   Lemma iMsg_map_base f v P p :
     NonExpansive f →

theories/examples/equivalence.v

+From actris.channel Require Import channel proofmode.
+
+Section equivalence_examples.
+  Context `{heapG Σ, chanG Σ}.
+
+  Lemma binder_swap_equivalence_example :
+    ((<! (x y : Z)> MSG (#x,#y) ; END):iProto Σ)%proto ≡
+    ((<! (y x : Z)> MSG (#x,#y) ; END):iProto Σ)%proto.
+  Proof.
+    apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iApply iProto_message_equiv; [ done | | ].
+    - iIntros "!>" (x y) "_". iExists y, x. eauto.
+    - iIntros "!>" (y x) "_". iExists x, y. eauto.
+  Qed.
+
+  Lemma choice_equivalence_example (P1 P2 Q1 Q2: iProp Σ) (S1 S2 : iProto Σ) :
+    (S1 <{P1 ∗ Q1}+{P2 ∗ Q2}> S2)%proto ≡ (S1 <{Q1 ∗ P1}+{Q2 ∗ P2}> S2)%proto.
+  Proof.
+    apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iApply iProto_choice_equiv; [ done | | | done | done ].
+    iApply prop_ext. iSplit; iIntros "!> [$ $]".
+    iApply prop_ext. iSplit; iIntros "!> [$ $]".
+  Qed.
+
+End equivalence_examples.