From 25f6a014baeec51310fe266774a01295e08a411b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 17 Apr 2020 16:52:36 +0200
Subject: [PATCH] Added identity rules for subtyping

---
 theories/logrel/session_types.v |  6 +++++-
 theories/logrel/subtyping.v     | 16 ++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 9d8bc21..a9a15d6 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -106,7 +106,11 @@ Section Propers.
   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.
+  Proof. intros S1 S2 S3. rewrite /lsty_app. by rewrite iProto_app_assoc. Qed.
+  Global Instance lsty_app_end_l : LeftId (≡) lsty_end (@lsty_app Σ).
+  Proof. intros [S]. rewrite /lsty_app. by rewrite left_id. Qed.
+  Global Instance lsty_app_end_r : RightId (≡) lsty_end (@lsty_app Σ).
+  Proof. intros [S]. rewrite /lsty_app. by rewrite right_id. Qed.
 End Propers.
 
 Notation "'END'" := lsty_end : lsty_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 9aa0108..11e4b5d 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -300,6 +300,22 @@ Section subtype.
     ⊢ ((S1 <++> S2) <++> S3) <s: (S1 <++> (S2 <++> S3)).
   Proof. rewrite lsty_app_assoc. iApply lsty_le_refl. Qed.
 
+  Lemma lsty_le_app_id_l_l S :
+    ⊢ (END <++> S) <s: S.
+  Proof. rewrite left_id. iApply lsty_le_refl. Qed.
+
+  Lemma lsty_le_app_id_l_r S :
+    ⊢ (S <++> END) <s: S.
+  Proof. rewrite right_id. iApply lsty_le_refl. Qed.
+
+  Lemma lsty_le_app_id_r_l S :
+    ⊢ S <s: (END <++> S).
+  Proof. rewrite left_id. iApply lsty_le_refl. Qed.
+
+  Lemma lsty_le_app_id_r_r S :
+    ⊢ S <s: (S <++> END).
+  Proof. rewrite right_id. 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