Require Import base data.fintype f.types.

Inductive tm (m n : nat) : Type :=
| var (x : fin n)
| app (s t : tm m n)
| lam (s : tm m n.+1)
| tapp (s : tm m n) (A : ty m)
| tlam (s : tm m.+1 n).

Fixpoint rename {m1 m2 n1 n2} (f : ren m1 m2) (g : ren n1 n2) (s : tm m1 n1) : tm m2 n2 :=
  match s with
  | var x => var m2 (g x)
  | app s t => app (rename f g s) (rename f g t)
  | lam s => lam (rename f (up g) s)
  | tapp s A => tapp (rename f g s) (tyrename f A)
  | tlam s => tlam (rename (up f) g s)
  end.

Definition subst m n1 n2 := fin n1 -> tm m n2.

Definition upi {m n1 n2} (σ : subst m n1 n2) : subst m n1.+1 n2.+1 :=
  var m bound .: σ >> rename id shift.

Fixpoint inst {m1 m2 n1 n2} (f : tysubst m1 m2) (g : subst m2 n1 n2) (s : tm m1 n1) : tm m2 n2 :=
  match s with
  | var x => g x
  | app s t => app (inst f g s) (inst f g t)
  | lam s => lam (inst f (upi g) s)
  | tapp s A => tapp (inst f g s) (tyinst f A)
  | tlam s => tlam (inst (tup f) (g >> rename shift id) s)
  end.

Lemma upi_ids m n : upi (@var m n) = @var m n.+1.
Proof. fext=>/=. by case. Qed.

Lemma ren_id m n (s : tm m n) : rename id id s = s.
Proof.
  elim: s => {m n} //=.
  - by move=> m n s-> t->.
  - move=> m n s e. unfold up. fsimpl. by rewrite e.
  - move=> m n s -> A. by rewrite ty_ren_id.
  - move=> m n s e. unfold up. fsimpl. by rewrite e.
Qed.

Lemma ren_inst m1 m2 n1 n2 (f : ren m1 m2) (g : ren n1 n2) (s : tm m1 n1) :
  rename f g s = inst (f >> @tvar _) (g >> @var _ _) s.
Proof.
  elim: s m2 n2 f g => //={m1 n1}
    [m1 n1 s ihs t iht|m1 n1 s ihs|m1 n1 s ihs A|m1 n1 s ihs] m2 n2 f g.
  - by rewrite ihs iht.
  - rewrite ihs. by fsimpl.
  - by rewrite ihs ty_ren_inst.
  - rewrite ihs. by fsimpl.
Qed.

Lemma inst_ids m n (s : tm m n) :
  inst (@tvar _) (@var _ _) s = s.
Proof.
  by rewrite -ren_inst ren_id.
Qed.

Lemma ren_inst_comp m1 m2 m3 n1 n2 n3 (f1 : ren m1 m2) (g1 : ren n1 n2)
      (f2 : tysubst m2 m3) (g2 : subst m3 n2 n3) (s : tm m1 n1) :
  inst f2 g2 (rename f1 g1 s) = inst (f1 >> f2) (g1 >> g2) s.
Proof.
  elim: s m2 m3 n2 n3 f1 g1 f2 g2 => //={m1 n1}
    [m1 n1 s ihs t iht|m1 n1 s ihs|m1 n1 s ihs A|m1 n1 s ihs]
    m2 m3 n2 n3 f1 g1 f2 g2.
  - by rewrite ihs iht.
  - rewrite ihs. by fsimpl.
  - rewrite ihs ty_ren_inst_comp. by fsimpl.
  - rewrite ihs. by fsimpl.
Qed.

Lemma ren_comp m1 m2 m3 n1 n2 n3 (f1 : ren m1 m2) (g1 : ren n1 n2)
      (f2 : ren m2 m3) (g2 : ren n2 n3) (s : tm m1 n1) :
  rename f2 g2 (rename f1 g1 s) = rename (f1 >> f2) (g1 >> g2) s.
Proof.
  by rewrite ren_inst ren_inst_comp ren_inst.
Qed.

Lemma upi_up_comp m1 m2 n1 n2 n3 (f1 : subst m1 n1 n2) (g : ren m1 m2) (f2 : ren n2 n3) :
  upi f1 >> rename g (up f2) = upi (f1 >> rename g f2).
Proof.
  fext=> /=-[i|]//=. by rewrite !ren_comp.
Qed.

Lemma inst_ren_comp m1 m2 m3 n1 n2 n3 (f1 : tysubst m1 m2) (g1 : subst m2 n1 n2)
      (f2 : ren m2 m3) (g2 : ren n2 n3) (s : tm m1 n1) :
  rename f2 g2 (inst f1 g1 s) = inst (f1 >> tyrename f2) (g1 >> rename f2 g2) s.
Proof.
  elim: s m2 m3 n2 n3 f1 g1 f2 g2 => //={m1 n1}
    [m1 n1 s ihs t iht|m1 n1 s ihs|m1 n1 s ihs A|m1 n1 s ihs]
    m2 m3 n2 n3 f1 g1 f2 g2.
  - by rewrite ihs iht.
  - by rewrite ihs upi_up_comp.
  - by rewrite ihs ty_inst_ren_comp.
  - rewrite ihs ty_tup_up_comp. do 2 f_equal; fext=> i/=.
    by rewrite !ren_comp.
Qed.

Lemma upi_comp m1 m2 n1 n2 n3 (f1 : subst m1 n1 n2) (f2 : subst m2 n2 n3) (g : tysubst m1 m2) :
  upi f1 >> inst g (upi f2) = upi (f1 >> inst g f2).
Proof.
  fext=> /=-[i|]//=. rewrite ren_inst_comp inst_ren_comp.
  f_equal; fext=> j/=. by rewrite ty_ren_id.
Qed.

Lemma inst_comp m1 m2 m3 n1 n2 n3 (f1 : tysubst m1 m2) (g1 : subst m2 n1 n2)
      (f2 : tysubst m2 m3) (g2 : subst m3 n2 n3) (s : tm m1 n1) :
  inst f2 g2 (inst f1 g1 s) = inst (f1 >> tyinst f2) (g1 >> inst f2 g2) s.
Proof.
  elim: s m2 m3 n2 n3 f1 g1 f2 g2 => //={m1 n1}
    [m1 n1 s ihs t iht|m1 n1 s ihs|m1 n1 s ihs A|m1 n1 s ihs]
    m2 m3 n2 n3 f1 g1 f2 g2.
  - by rewrite ihs iht.
  - by rewrite ihs upi_comp.
  - by rewrite ihs ty_inst_comp.
  - rewrite ihs ty_tup_comp. do 2 f_equal; fext=> i/=.
    by rewrite ren_inst_comp inst_ren_comp.
Qed.