From a5fa98331e6e5538e7a2a612b06ac9a7fc535852 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 17 Apr 2020 16:35:15 +0200
Subject: [PATCH] Added associativity rules for append subtyping
---
theories/logrel/session_types.v | 2 ++
theories/logrel/subtyping.v | 10 +++++++++-
2 files changed, 11 insertions(+), 1 deletion(-)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index cec8d95..9d8bc21 100644
--- a/theories/logrel/session_types.v
+++ b/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.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 54f5b65..4901791 100644
--- a/theories/logrel/subtyping.v
+++ b/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.
--
GitLab