Skip to content
Snippets Groups Projects
Commit 661e6d86 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added type former for a type appended N times

parent a0bb670c
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
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_Σ.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment