Require Import base data.fintype.

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 : fin n).

Fixpoint rmap {n m} (f : ren n 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 (up f) s)
  | Var x => Var (f x)
  end.

Definition upi {n m} (f : fin n -> exp m) : fin n.+1 -> exp m.+1 :=
  Var bound .: f >> rmap shift.

Fixpoint rbind {n m} (f : fin 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 (upi f) s)
  | Var x => f x
  end.

Definition rcomp {n m k} (f : fin n -> exp m) (g : fin m -> exp k) : fin n -> exp k :=
  f >> rbind g.

Definition ids {n} : fin 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 : fin n -> exp m) x :
  (ids x).[f] = f x.
Proof. by []. Qed.

Lemma up_id n :
  upi (@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 : fin n -> fin m) :
  ren (up f) = upi (ren f).
Proof. by rewrite/up/upi; fsimpl. Qed.

Lemma map_subst n m (f : fin n -> fin 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 : fin n -> exp m) :
  upi f = Var bound .: (f >>> ren shift).
Proof.
  rewrite/upi/=. f_equal; fext=> x/=. by rewrite map_subst.
Qed.

Lemma up_upr n m k (f : fin n -> fin m) (g : fin m -> exp k) :
  up f >> upi g = upi (f >> g).
Proof. by fsimpl. Qed.

Lemma rbind_rmap_comp n m k (f : fin n -> fin m) (g : fin m -> exp k) (s : exp n) :
  (rmap f s).[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_upr.
Qed.

Lemma rmap_comp n m k (f : fin n -> fin m) (g : fin m -> fin k) (s : exp n) :
  rmap g (rmap f s) = rmap (f >> g) s.
Proof. by rewrite map_subst rbind_rmap_comp map_subst. Qed.

Lemma upr_up n m k (f : fin n -> exp m) (g : fin m -> fin k) :
  upi f >> rmap (up g) = upi (f >> rmap g).
Proof.
  fext=> /=-[i|]//=. by rewrite !rmap_comp.
Qed.

Lemma rmap_rbind_comp n m k (f : fin n -> exp m) (g : fin m -> fin k) (s : exp n) :
  rmap g (rbind f s) = rbind (f >> rmap g) 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 : fin n -> exp m) (g : fin m -> exp k) :
  upi f >>> upi g = upi (f >>> g).
Proof.
  fext=>/=-[i|]//=. by rewrite/rcomp/= rbind_rmap_comp rmap_rbind_comp.
Qed.

Lemma rbindA n m k (f : fin n -> exp m) (g : fin 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 : fin n -> exp m) (g : fin m -> exp k) :
  (s .: f) >>> g = s.[g] .: (f >>> g).
Proof. rewrite/rcomp. by fsimpl. Qed.

Lemma shift_scons n m (s : exp m) (f : fin n -> exp m) :
  ren shift >>> (s .: f) = f.
Proof. by []. Qed.

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

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

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

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

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

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