From 60e20dc108bc9bb4648306843c9f3924cefce772 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 17 Apr 2020 17:49:11 +0200
Subject: [PATCH] WIP Dual Subtype rules

---
 theories/logrel/subtyping.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index f315b96..bbdb890 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -319,6 +319,28 @@ 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_send_l A S : ⊢ (lsty_dual (<!!>A;S)) <s: (<??>A;(lsty_dual S)).
+  Proof.
+    rewrite /lsty_le /lsty_dual /lsty_send /lsty_recv /lsty_message iProto_dual_message /=.
+    iIntros "!>".
+    rewrite {1}/lsty_car /=.
+    iApply iProto_le_refl.
+  Admitted.
+
+  Lemma lsty_le_dual_send_r A S : ⊢ (<!!>A;(lsty_dual S)) <s: lsty_dual (<??> A;S).
+  Proof. Admitted.
+
+  Lemma lsty_le_dual_recv_l A S : ⊢ (lsty_dual (<??> A;S)) <s: (<!!> A;(lsty_dual S)).
+  Proof. Admitted.
+  Lemma lsty_le_dual_recv_r A S : ⊢ (<??>A;(lsty_dual S)) <s: lsty_dual (<!!> A;S).
+  Proof. Admitted.
+
+  Lemma lsty_le_dual_end_l : ⊢ (lsty_dual (Σ:=Σ) END) <s: END.
+  Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. Qed.
+
+  Lemma lsty_le_dual_end_r : ⊢ END <s: (lsty_dual (Σ:=Σ) END).
+  Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. 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.
 
-- 
GitLab