Automatically unfold recursive protocols.

theories/channel/proto_channel.v

@@ -4,7 +4,6 @@ From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth excl.
 From osiris.utils Require Import auth_excl.
-Set Default Proof Using "Type*".
 Export action.
 
 Definition start_chan : val := λ: "f",
@@ -180,6 +179,9 @@ Class ProtoContNormalize {Σ TT} (d : bool) (pc : TT → val * iProp Σ * iProto
     ProtoNormalize d ((pc x).2) pas ((qc x).2).
 Hint Mode ProtoContNormalize ! ! ! ! ! - : typeclass_instances.
 
+Notation ProtoUnfold p1 p2 := (∀ d pas q,
+  ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
+
 (** Auxiliary definitions and invariants *)
 Fixpoint proto_eval `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
   match vs with
@@ -295,6 +297,10 @@ Section proto.
   Proof. solve_proper. Qed.
   Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ).
   Proof. apply (ne_proper _). Qed.
+  Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ d).
+  Proof. solve_proper. Qed.
+  Global Instance iProto_dual_if_proper d : Proper ((≡) ==> (≡)) (@iProto_dual_if Σ d).
+  Proof. apply (ne_proper _). Qed.
 
   Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ).
   Proof.
@@ -357,6 +363,9 @@ Section proto.
   Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
 
   (** Classes *)
+  Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
+  Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed.
+
   Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
   Proof. by rewrite /ProtoNormalize /= right_id. Qed. 
   Global Instance proto_normalize_done_dual p :

theories/examples/list_sort_elem.v

@@ -63,9 +63,9 @@ Section list_sort_elem.
   Qed.
   Definition tail_protocol (xs : list (A * val)) : list (A * val) → iProto Σ :=
     fixpoint (tail_protocol_aux xs).
-  Lemma tail_protocol_unfold xs ys:
-    tail_protocol xs ys ≡ tail_protocol_aux xs (tail_protocol xs) ys.
-  Proof. apply (fixpoint_unfold (tail_protocol_aux _)). Qed.
+  Global Instance tail_protocol_unfold xs ys :
+    ProtoUnfold (tail_protocol xs ys) (tail_protocol_aux xs (tail_protocol xs) ys).
+  Proof. apply proto_unfold_eq, (fixpoint_unfold (tail_protocol_aux _)). Qed.
 
   Definition head_protocol_aux
       (rec : list (A * val) -d> iProto Σ) : list (A * val) -d> iProto Σ := λ xs,
@@ -79,9 +79,9 @@ Section list_sort_elem.
   Qed.
 
   Definition head_protocol : list (A * val) → iProto Σ := fixpoint head_protocol_aux.
-  Lemma head_protocol_unfold xs :
-    head_protocol xs ≡ head_protocol_aux head_protocol xs.
-  Proof. apply (fixpoint_unfold head_protocol_aux). Qed.
+  Global Instance head_protocol_unfold xs :
+    ProtoUnfold (head_protocol xs) (head_protocol_aux head_protocol xs).
+  Proof. apply proto_unfold_eq, (fixpoint_unfold head_protocol_aux). Qed.
 
   Definition list_sort_elem_protocol : iProto Σ := head_protocol [].
 
@@ -98,11 +98,8 @@ Section list_sort_elem.
     }}}.
   Proof.
     iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
-    wp_rec.
-    rewrite head_protocol_unfold.
-    wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
+    wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
     - wp_apply (recv_proto_spec with "Hc"); iIntros (x v) "/= Hc HI".
-      rewrite (head_protocol_unfold xs1).
       wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
       wp_apply (send_proto_spec with "Hc1"); simpl.
       iExists x, v. iSplit; [done|]. iIntros "{$HI} !> Hc1".
@@ -110,8 +107,7 @@ Section list_sort_elem.
       iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
       rewrite -!(assoc_L (++)).
       iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
-    - rewrite (head_protocol_unfold xs1) (head_protocol_unfold xs2).
-      wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
+    - wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
       wp_apply (select_spec with "[$Hc2]")=> //=; iIntros "Hc2".
       iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
   Qed.
@@ -130,13 +126,10 @@ Section list_sort_elem.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
     iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
-    wp_rec.
-    rewrite (tail_protocol_unfold xs').
-    wp_apply (branch_spec with "Hcin"); iIntros ([]) "[Hcin Hys']".
+    wp_rec. wp_apply (branch_spec with "Hcin"); iIntros ([]) "[Hcin Hys']".
     - iClear "Hys'".
       wp_apply (recv_proto_spec with "Hcin"); iIntros (x v) "/= Hcin".
       iDestruct 1 as (Hx) "HI".
-      rewrite (tail_protocol_unfold xs).
       wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
       wp_apply (send_proto_spec with "Hc"); simpl.
       iExists x, v. iFrame "HI". do 2 (iSplit; [by auto|]); iIntros "!> Hc".
@@ -146,8 +139,7 @@ Section list_sort_elem.
       { rewrite fmap_app /=. apply Sorted_snoc; auto. }
       { intros x'. rewrite !fmap_app.
         inversion 1; discriminate_list || simplify_list_eq. by constructor. }
-    - iDestruct "Hys'" as %Hys'. rewrite (tail_protocol_unfold xs).
-      wp_apply (select_spec with "[$Hc]")=> //=.
+    - iDestruct "Hys'" as %Hys'. wp_apply (select_spec with "[$Hc]")=> //=.
       { by rewrite Hys Hxs Hys'. }
       iIntros "Hc". iApply "HΨ". iFrame.
   Qed.
@@ -170,9 +162,7 @@ Section list_sort_elem.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
     iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
     iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
-    wp_rec.
-    rewrite (tail_protocol_unfold xs) (tail_protocol_unfold xs2).
-    wp_apply (branch_spec with "[$Hc2]"); iIntros ([]) "[Hc2 Hys2]".
+    wp_rec. wp_apply (branch_spec with "[$Hc2]"); iIntros ([]) "[Hc2 Hys2]".
     - iClear "Hys2".
       wp_apply (recv_proto_spec with "Hc2"); iIntros (x v) "/= Hc2".
       iDestruct 1 as (Htl2) "HIx".
@@ -220,10 +210,9 @@ Section list_sort_elem.
     {{{ RET #(); c ↣ END @ N }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
-    wp_rec; wp_pures. rewrite /list_sort_elem_protocol {2}head_protocol_unfold.
+    wp_rec; wp_pures.
     wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
     - wp_apply (recv_proto_spec with "Hc"); iIntros (x1 v1) "/= Hc HIx1".
-      rewrite (head_protocol_unfold [_]).
       wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
       + wp_apply (recv_proto_spec with "Hc"); iIntros (x2 v2) "/= Hc HIx2".
         wp_apply (start_chan_proto_spec N list_sort_elem_protocol).
@@ -232,7 +221,6 @@ Section list_sort_elem.
         wp_apply (start_chan_proto_spec N list_sort_elem_protocol).
         { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz".
-        rewrite /list_sort_elem_protocol {2 3}(head_protocol_unfold []).
         wp_apply (select_spec with "[$Hcy]")=> //; iIntros "Hcy".
         wp_apply (send_proto_spec with "Hcy")=> //=.
         iExists x1, v1. iFrame "HIx1". iSplit; [done|]; iIntros "!> Hcy".
@@ -241,7 +229,6 @@ Section list_sort_elem.
         iExists x2, v2. iFrame "HIx2". iSplit; [done|]; iIntros "!> Hcz".
         wp_apply (list_sort_elem_service_split_spec with "[$Hc $Hcy $Hcz]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
-        rewrite (tail_protocol_unfold (_ :: xs1')).
         wp_apply (branch_spec with "Hcy"); iIntros (b) "[Hcy Hnil]".
         destruct b; last first.
         { by iDestruct "Hnil" as %?%Permutation_nil_cons. }
@@ -251,14 +238,10 @@ Section list_sort_elem.
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
         { by rewrite Hxs' Permutation_middle. }
         iIntros "(Hc & Hcy & Hcz)". by iApply "HΨ".
-      + rewrite (tail_protocol_unfold [_]).
-        wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
+      + wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
         wp_apply (send_proto_spec with "Hc"); simpl.
         iExists x1, v1. iFrame "HIx1". do 2 (iSplit; [by auto using TlRel_nil|]).
-        iIntros "!> Hc".
-        rewrite (tail_protocol_unfold [_]).
-        by wp_apply (select_spec with "[$Hc]").
-    - rewrite (tail_protocol_unfold []).
-      by wp_apply (select_spec with "[$Hc]").
+        iIntros "!> Hc". by wp_apply (select_spec with "[$Hc]").
+    - by wp_apply (select_spec with "[$Hc]").
   Qed.
 End list_sort_elem.

theories/examples/loop_sort.v

@@ -25,9 +25,9 @@ Section loop_sort.
     f_contractive; f_equiv=> //. apply iProto_message_ne=> c /=; by repeat f_equiv.
   Qed.
   Definition loop_sort_protocol : iProto Σ := fixpoint loop_sort_protocol_aux.
-  Lemma loop_sort_protocol_unfold :
-    loop_sort_protocol ≡ loop_sort_protocol_aux loop_sort_protocol.
-  Proof. apply (fixpoint_unfold loop_sort_protocol_aux). Qed.
+  Global Instance loop_sort_protocol_unfold :
+    ProtoUnfold loop_sort_protocol (loop_sort_protocol_aux loop_sort_protocol).
+  Proof. apply proto_unfold_eq, (fixpoint_unfold loop_sort_protocol_aux). Qed.
 
   Lemma loop_sort_service_spec c :
     {{{ c ↣ iProto_dual loop_sort_protocol @ N }}}
@@ -35,8 +35,7 @@ Section loop_sort.
     {{{ RET #(); c ↣ END @ N }}}.
   Proof.
     iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
-    wp_rec. rewrite {2}loop_sort_protocol_unfold.
-    wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
+    wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
     { wp_apply (list_sort_service_spec with "Hc"); iIntros "Hc".
       by wp_apply ("IH" with "Hc"). }
     wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.