From 3ade9b42c38f7bd5aa3011e8d3d38e5039ff1b66 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 17 Apr 2020 13:25:00 +0200
Subject: [PATCH] Added left/right rules to dual subtyping

---
 theories/channel/proto.v    | 14 ++++++++++++++
 theories/logrel/subtyping.v |  6 ++++++
 2 files changed, 20 insertions(+)

diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 542b42d..d5b2335 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -797,6 +797,20 @@ Section proto.
       iNext. by iRewrite "Hp2d".
   Qed.
 
+  Lemma iProto_le_dual_l p1 p2 :
+    iProto_le (iProto_dual p2) p1 -∗ iProto_le (iProto_dual p1) p2.
+  Proof.
+    iIntros "H". iEval (rewrite -(iProto_dual_involutive p2)).
+    by iApply iProto_le_dual.
+  Qed.
+
+  Lemma iProto_le_dual_r p1 p2 :
+    iProto_le p2 (iProto_dual p1) -∗ iProto_le p1 (iProto_dual p2).
+  Proof.
+    iIntros "H". iEval (rewrite -(iProto_dual_involutive p1)).
+    by iApply iProto_le_dual.
+  Qed.
+
   Lemma iProto_le_app p1 p2 p3 p4 :
     iProto_le p1 p2 -∗ iProto_le p3 p4 -∗ iProto_le (p1 <++> p3) (p2 <++> p4).
   Proof.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index ab5f6f5..54f5b65 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -295,6 +295,12 @@ Section subtype.
   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.
 
+  Lemma lsty_le_dual_l S1 S2 : lsty_dual S2 <s: S1 -∗ lsty_dual S1 <s: S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
+
+  Lemma lsty_le_dual_r S1 S2 : S2 <s: lsty_dual S1 -∗ S1 <s: lsty_dual S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
+
   Lemma lsty_le_rec_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
     ⊢ lsty_rec C <s: C (lsty_rec C).
   Proof.
-- 
GitLab