From 661e6d86db071b11d59d5ca459d74f9a4f397770 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 16 Sep 2020 20:08:04 +0200
Subject: [PATCH] Added type former for a type appended N times

---
 _CoqProject            |  1 +
 theories/logrel/napp.v | 44 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 theories/logrel/napp.v

diff --git a/_CoqProject b/_CoqProject
index c484200..c966745 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,7 @@ theories/logrel/term_typing_judgment.v
 theories/logrel/subtyping_rules.v
 theories/logrel/term_typing_rules.v
 theories/logrel/session_typing_rules.v
+theories/logrel/napp.v
 theories/logrel/lib/mutex.v
 theories/logrel/lib/par_start.v
 theories/logrel/examples/double.v
diff --git a/theories/logrel/napp.v b/theories/logrel/napp.v
new file mode 100644
index 0000000..af8d233
--- /dev/null
+++ b/theories/logrel/napp.v
@@ -0,0 +1,44 @@
+From actris.logrel Require Import term_typing_rules session_types subtyping_rules.
+From actris.channel Require Import proofmode.
+
+Section with_Σ.
+  Context `{!heapG Σ}.
+
+  Fixpoint lty_napp (R : lsty Σ) (n : nat) :=
+    match n with
+    | O => END
+    | S n => R <++> lty_napp R n
+    end%lty.
+
+  Lemma lty_napp_S_l R n :
+    lty_napp R (S n) ≡ (R <++> lty_napp R n)%lty.
+  Proof. eauto. Qed.
+
+  Lemma lty_napp_S_r R n :
+    lty_napp R (S n) ≡ (lty_napp R n <++> R)%lty.
+  Proof.
+    induction n; simpl; [ by rewrite lty_app_end_l lty_app_end_r | ].
+    rewrite -(assoc _ _ (lty_napp R n) R). by rewrite -IHn.
+  Qed.
+
+  Lemma lty_napp_flip R n :
+     (lty_napp R n <++> R)%lty ≡ (R <++> lty_napp R n)%lty.
+  Proof. by rewrite -lty_napp_S_l lty_napp_S_r. Qed.
+
+  Lemma napp_swap T R n :
+    R <++> T <: T <++> R -∗
+    lty_napp R n <++> T <: T <++> lty_napp R n.
+  Proof.
+    iIntros "#Hle".
+    iInduction n as [|n] "IHn";
+      [ by rewrite lty_app_end_l lty_app_end_r | ].
+    rewrite -assoc.
+    iApply lty_le_trans.
+    { iApply lty_le_app; [ iApply lty_le_refl | iApply "IHn" ]. }
+    rewrite assoc.
+    iApply lty_le_trans.
+    { iApply lty_le_app; [ iApply "Hle" | iApply lty_le_refl ]. }
+    rewrite assoc. iApply lty_le_refl.
+  Qed.
+
+End with_Σ.
-- 
GitLab