Fixed contractiveness of choice

theories/logrel/session_types.v

@@ -18,7 +18,7 @@ Definition lty_message {Σ} (a : action) (M : lmsg Σ) : lsty Σ :=
   Lsty (<a> M).
 
 Definition lty_choice {Σ} (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
-  Lsty (<a@(x : Z)> MSG #x {{ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
+  Lsty (<a@(x : Z)> MSG #x {{ ▷ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
 
 Definition lty_dual {Σ} (S : lsty Σ) : lsty Σ :=
   Lsty (iProto_dual (lsty_car S)).
@@ -83,10 +83,11 @@ Section session_types.
   Proof. solve_proper. Qed.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
-(* FIXME
   Global Instance lty_choice_contractive a : Contractive (@lty_choice Σ a).
-  Proof. solve_contractive. Qed.
-*)
+  Proof.
+    intros n Ss Ts Heq. rewrite /lty_choice.
+    do 4 f_equiv; f_contractive; [ f_contractive | ]; by rewrite Heq.
+  Qed.
   Global Instance lty_dual_ne : NonExpansive (@lty_dual Σ).
   Proof. solve_proper. Qed.
   Global Instance lty_dual_proper : Proper ((≡) ==> (≡)) (@lty_dual Σ).

theories/logrel/subtyping_rules.v

@@ -298,6 +298,7 @@ Section subtyping_rules.
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
     iApply iProto_le_payload_elim_r.
+    iMod 1 as "%". revert H1.
     rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
     iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
     iModIntro. by iExists v1.
@@ -310,6 +311,7 @@ Section subtyping_rules.
     iApply iProto_le_trans;
       [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
     iApply iProto_le_payload_elim_l.
+    iMod 1 as %HSs. revert HSs.
     rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
     iApply iProto_le_trans; [|iApply iProto_le_base_swap]. iSplitL; [by eauto|].
     iModIntro. by iExists v2.
@@ -319,7 +321,7 @@ Section subtyping_rules.
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_select Ss1 <: lty_select Ss2.
   Proof.
-    iIntros "#H !>" (x); iDestruct 1 as %[S2 HSs2]. iExists x.
+    iIntros "#H !>" (x); iMod 1 as %[S2 HSs2]. iExists x.
     iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
     assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
     rewrite HSs1. iSplitR; [by eauto|].
@@ -330,7 +332,7 @@ Section subtyping_rules.
     Ss2 ⊆ Ss1 →
     ⊢ lty_select Ss1 <: lty_select Ss2.
   Proof.
-    intros; iIntros "!>" (x); iDestruct 1 as %[S HSs2]. iExists x.
+    intros; iIntros "!>" (x); iMod 1 as %[S HSs2]. iExists x.
     assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
     rewrite HSs1. iSplitR; [by eauto|].
     iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
@@ -340,7 +342,7 @@ Section subtyping_rules.
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_branch Ss1 <: lty_branch Ss2.
   Proof.
-    iIntros "#H !>" (x); iDestruct 1 as %[S1 HSs1]. iExists x.
+    iIntros "#H !>" (x); iMod 1 as %[S1 HSs1]. iExists x.
     iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
     assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
     rewrite HSs2. iSplitR; [by eauto|].
@@ -351,7 +353,7 @@ Section subtyping_rules.
     Ss1 ⊆ Ss2 →
     ⊢ lty_branch Ss1 <: lty_branch Ss2.
   Proof.
-    intros; iIntros "!>" (x); iDestruct 1 as %[S HSs1]. iExists x.
+    intros; iIntros "!>" (x); iMod 1 as %[S HSs1]. iExists x.
     assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
     rewrite HSs2. iSplitR; [by eauto|].
     iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
@@ -389,7 +391,7 @@ Section subtyping_rules.
       setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
     iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
-      iDestruct 1 as %[S ->]; iSplitR; eauto.
+      iMod 1 as %[S ->]; iSplitR; eauto.
   Qed.
   Lemma lty_le_app_select A Ss S2 :
     ⊢ lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
@@ -426,7 +428,7 @@ Section subtyping_rules.
       setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
     iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
-      iDestruct 1 as %[S ->]; iSplitR; eauto.
+      iMod 1 as %[S ->]; iSplitR; eauto.
   Qed.
 
   Lemma lty_le_dual_select (Ss : gmap Z (lsty Σ)) :