Require Import prelim fin.

Inductive act :=
| ActSend (n : nat)
| ActRecv (n : nat)
| ActTau.

Inductive exp (n : nat) :=
| Act (a : act) (s : exp n)
| Sum (s t : exp n)
| Par (s t : exp n)
| New (a : nat) (s : exp n)
| Fix (s : exp n.+1)
| Var (x : 'I_n).

Definition upr {n m} (f : 'I_n -> 'I_m) : 'I_n.+1 -> 'I_m.+1 := 0 .: S \o f.

Fixpoint rmap {n m} (f : 'I_n -> 'I_m) (s : exp n) : exp m :=
  match s with
  | Act a s => Act a (rmap f s)
  | Sum s t => Sum (rmap f s) (rmap f t)
  | Par s t => Par (rmap f s) (rmap f t)
  | New a s => New a (rmap f s)
  | Fix s => Fix (rmap (upr f) s)
  | Var x => Var (f x)
  end.

Definition up {n m} (f : 'I_n -> exp m) : 'I_n.+1 -> exp m.+1 :=
  Var 0 .: rmap S \o f.

Fixpoint rbind {n m} (f : 'I_n -> exp m) (s : exp n) : exp m :=
  match s with
  | Act a s => Act a (rbind f s)
  | Sum s t => Sum (rbind f s) (rbind f t)
  | Par s t => Par (rbind f s) (rbind f t)
  | New a s => New a (rbind f s)
  | Fix s => Fix (rbind (up f) s)
  | Var x => f x
  end.

Definition rcomp {n m k} (f : 'I_n -> exp m) (g : 'I_m -> exp k) : 'I_n -> exp k :=
  rbind g \o f.

Definition ids {n} : 'I_n -> exp n := @Var n.

Notation "f >> g" := (rcomp f g) (at level 56, left associativity).
Notation "s .[ f ]" := (rbind f s)
  (at level 2, f at level 200, left associativity,
   format "s .[ f ]" ).
Notation "s .[ t /]" := (s.[t .: ids])
  (at level 2, t at level 200, left associativity,
   format "s .[ t /]").

Notation ren f := (ids \o f).

Lemma id_inst n m (f : 'I_n -> exp m) x :
  (ids x).[f] = f x.
Proof. by []. Qed.

Lemma up_id n :
  up (@ids n) = ids.
Proof.
  by rewrite -(@scons_eta _ n ids).
Qed.

Lemma inst_id n (s : exp n) :
  s.[ids] = s.
Proof.
  elim: s => {n}; try (intros=> //=; congruence).
  move=> n s ihs /=. by rewrite up_id ihs.
Qed.

Lemma up_ren n m (f : 'I_n -> 'I_m) :
  ren (upr f) = up (ren f).
Proof.
  apply: scons_eq.
  - by rewrite/=/up/upr !scons0.
  - move=> i. by rewrite/=/up/upr !sconsS.
Qed.

Lemma map_subst n m (f : 'I_n -> 'I_m) (s : exp n) :
  rmap f s = s.[ren f].
Proof.
  elim: s m f => {n}; try (intros=> //=; congruence).
  move=> n s ihs m f /=. by rewrite ihs up_ren.
Qed.

Lemma upE n m (f : 'I_n -> exp m) :
  up f = Var 0 .: f >> ren S.
Proof.
  apply: scons_eq.
  - by rewrite/up/upr !scons0.
  - move=> i. by rewrite/up/upr/= !sconsS/= map_subst.
Qed.

Lemma up_upr n m k (f : 'I_n -> 'I_m) (g : 'I_m -> exp k) :
  up g \o upr f = up (g \o f).
Proof.
  apply: scons_eq => [|x]; by rewrite/up/upr/= !scons_simpl.
Qed.

Lemma rbind_rmap_comp n m k (f : 'I_n -> 'I_m) (g : 'I_m -> exp k) (s : exp n) :
  (rmap f s).[g] = s.[g \o f].
Proof.
  elim: s m k f g => {n}; try (intros=> //=; congruence).
  move=> n s ihs m k f g /=. by rewrite ihs up_upr.
Qed.

Lemma rmap_comp n m k (f : 'I_n -> 'I_m) (g : 'I_m -> 'I_k) (s : exp n) :
  rmap g (rmap f s) = rmap (g \o f) s.
Proof. by rewrite map_subst rbind_rmap_comp map_subst. Qed.

Lemma upr_up n m k (f : 'I_n -> exp m) (g : 'I_m -> 'I_k) :
  rmap (upr g) \o up f = up (rmap g \o f).
Proof.
  apply: scons_eq => [|x]; rewrite/up/upr/= /=!scons_simpl/=?scons_simpl//.
  rewrite !rmap_comp. congr rmap. apply: fext => {x}x /=. by rewrite sconsS.
Qed.

Lemma rmap_rbind_comp n m k (f : 'I_n -> exp m) (g : 'I_m -> 'I_k) (s : exp n) :
  rmap g (rbind f s) = rbind (rmap g \o f) s.
Proof.
  elim: s m k f g => {n}; try (intros=> //=; congruence).
  move=> n s ihs m k f g /=. by rewrite ihs upr_up.
Qed.

Lemma up_comp n m k (f : 'I_n -> exp m) (g : 'I_m -> exp k) :
  up f >> up g = up (f >> g).
Proof.
  apply: scons_eq => [|x].
  - by rewrite/rcomp/up/= !scons0 /= scons0.
  - rewrite/rcomp/up/= !sconsS /= rbind_rmap_comp rmap_rbind_comp.
    congr rbind. apply: fext => j /=. by rewrite sconsS.
Qed.

Lemma rbindA n m k (f : 'I_n -> exp m) (g : 'I_m -> exp k) (s : exp n) :
  s.[f].[g] = s.[f >> g].
Proof.
  elim: s m k f g => {n}; try (intros=> //=; congruence).
  move=> n s ihs m k f g /=. by rewrite ihs up_comp.
Qed.

Lemma scons_scomp n m k (s : exp m) (f : 'I_n -> exp m) (g : 'I_m -> exp k) :
  (s .: f) >> g = s.[g] .: (f >> g).
Proof.
  apply: scons_eq => [|x].
  - by rewrite/rcomp/= !scons0.
  - by rewrite/rcomp/= !sconsS/=.
Qed.

Lemma shift_scons n m (s : exp m) (f : 'I_n -> exp m) :
  ren S >> (s .: f) = f.
Proof.
  apply: fext => x. rewrite/rcomp/=. by rewrite sconsS.
Qed.

Lemma rcompA n m k l (f : 'I_n -> exp m) (g : 'I_m -> exp k) (h : 'I_k -> exp l) :
  f >> g >> h = f >> (g >> h).
Proof.
  apply: fext => x. by rewrite/rcomp/= rbindA.
Qed.

Lemma rcomp_id n m (f : 'I_n -> exp m) :
  f >> ids = f.
Proof.
  apply: fext => x. by rewrite/rcomp/= inst_id.
Qed.

Lemma id_rcomp n m (f : 'I_n -> exp m) :
  ids >> f = f.
Proof. exact: fext. Qed.

Definition asimpl := (scons_simpl, id_inst, inst_id, rbindA,
  scons_scomp, shift_scons, rcompA, rcomp_id, id_rcomp, upE).

Lemma subst_extend n m (f : 'I_n -> exp m) (s : exp n.+1) (t : exp m) :
  s.[up f].[t/] = s.[t .: f].
Proof. by rewrite !asimpl. Qed.

Lemma subst_up n m (s : exp n.+1) u (f : 'I_n -> exp m) :
  s.[up f].[u.[f]/] = s.[u/].[f].
Proof. by rewrite !asimpl. Qed.