Added associativity rules for append subtyping

theories/logrel/session_types.v

@@ -105,6 +105,8 @@ Section Propers.
   Proof. solve_proper. Qed.
   Global Instance lsty_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@lsty_app Σ).
   Proof. apply ne_proper_2, _. Qed.
+  Global Instance lsty_app_assoc : Assoc (≡) (@lsty_app Σ).
+  Proof. intros s1 s2 s3. rewrite /lsty_app. by rewrite iProto_app_assoc. Qed.
 End Propers.
 
 Notation "'END'" := lsty_end : lsty_scope.

theories/logrel/subtyping.v

@@ -224,7 +224,7 @@ Section subtype.
     iApply iProto_le_send; simpl.
     iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
     iExists x. iSplit=> //. iSplit.
-    - iNext. 
+    - iNext.
       iDestruct (big_sepM2_forall with "H1") as "[% _]".
       iPureIntro. naive_solver.
     - iNext.
@@ -292,6 +292,14 @@ Section subtype.
     (S11 <++> S12) <s: (S21 <++> S22).
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
+  Lemma lsty_le_app_assoc_l S1 S2 S3 :
+    ⊢ ((S1 <++> S2) <++> S3) <s: (S1 <++> (S2 <++> S3)).
+  Proof. rewrite lsty_app_assoc. iApply lsty_le_refl. Qed.
+
+  Lemma lsty_le_app_assoc_r S1 S2 S3 :
+    ⊢ ((S1 <++> S2) <++> S3) <s: (S1 <++> (S2 <++> S3)).
+  Proof. rewrite lsty_app_assoc. iApply lsty_le_refl. Qed.
+
   Lemma lsty_le_dual S1 S2 : S2 <s: S1 -∗ lsty_dual S1 <s: lsty_dual S2.
   Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
 

[Robbert Krebbers]

Don't use instances, but use the projection, so assoc instead of iProto_app_assoc.