From c676b5294cd3f8f51974353acad8f589008c7c02 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 25 Nov 2020 13:19:50 +0100
Subject: [PATCH] Made equivalence lemma more applicable using typeclass
 resolution

---
 _CoqProject                     |  1 +
 theories/channel/channel.v      | 10 ++--
 theories/channel/proofmode.v    | 13 -----
 theories/channel/proto.v        | 89 ++++++++++++++++++++++-----------
 theories/examples/equivalence.v | 16 ++++++
 5 files changed, 81 insertions(+), 48 deletions(-)
 create mode 100644 theories/examples/equivalence.v

diff --git a/_CoqProject b/_CoqProject
index c846664..1c252fe 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index dabfc95..58ee99f 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -299,10 +299,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]".
@@ -314,7 +310,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".
@@ -326,7 +323,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".
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 24b5683..20d3629 100644
--- a/theories/channel/proofmode.v
+++ b/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.
 
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 3fc2018..efc3cfe 100644
--- a/theories/channel/proto.v
+++ b/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 :=
@@ -349,35 +361,6 @@ Section proto.
       (∀ 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_equiv {TT1 TT2 : tele} a1 a2
-        (v1 : TT1 → V) (v2 : TT2 → V)
-        (P1 : TT1 → iProp Σ) (P2 : TT2 → iProp Σ)
-        (prot1 : TT1 → iProto Σ V) (prot2 : TT2 → iProto Σ V) :
-    ⌜ a1 = a2 ⌝ -∗
-    (■ ∀ (xs1 : TT1), P1 xs1 -∗
-       ∃ (xs2 : TT2), ⌜v1 xs1 = v2 xs2⌝ ∗ ▷ (prot1 xs1 ≡ prot2 xs2) ∗ P2 xs2) -∗
-    (■ ∀ (xs2 : TT2), P2 xs2 -∗
-       ∃ (xs1 : TT1), ⌜v1 xs1 = v2 xs2⌝ ∗ ▷ (prot1 xs1 ≡ prot2 xs2) ∗ P1 xs1) -∗
-      (<a1 @ xs1> MSG (v1 xs1) {{ P1 xs1 }} ; prot1 xs1) ≡
-      (<a2 @ xs2> MSG (v2 xs2) {{ P2 xs2 }} ; prot2 xs2).
-  Proof.
-    iIntros (Heq) "#Heq1 #Heq2".
-    rewrite iProto_message_eq proto_message_equivI iMsg_exist_eq iMsg_base_eq /=.
-    iSplit; [ done | ].
-    iIntros (v p'). 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.
-
   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.
@@ -415,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.
@@ -422,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)%proto ≡ (<a2> m2)%proto.
+  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 →
diff --git a/theories/examples/equivalence.v b/theories/examples/equivalence.v
new file mode 100644
index 0000000..258e8ac
--- /dev/null
+++ b/theories/examples/equivalence.v
@@ -0,0 +1,16 @@
+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.
+
+End equivalence_examples.
-- 
GitLab