(** This file defines an operator [lty_napp] used to iteratively append a session type to itself a finite number of times. It includes lemmas for swapping a type [R] over an iteration of arbitrary length of another type [T] *) From actris.logrel Require Import term_typing_rules session_types subtyping_rules. From actris.channel Require Import proofmode. Section with_Σ. Context `{!heapGS Σ}. 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 lty_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_Σ.