Require Import base data.fintype f.types.

Unset Elimination Schemes.
Inductive tm (m n : nat) : Type :=
| val (s : vl m n)
| app (s t : tm m n)
| tapp (s : tm m n) (A : ty m)
with vl (m n : nat) : Type :=
| var (x : fin n)
| lam (s : tm m n.+1)
| tlam (s : tm m.+1 n).
Set Elimination Schemes.

Scheme tm_ind := Induction for tm Sort Prop
  with vl_ind := Induction for vl Sort Prop.
Combined Scheme tv_ind from tm_ind, vl_ind.

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

Definition vsubst m n1 n2 := fin n1 -> vl m n2.

Definition vup {m n1 n2} (σ : vsubst m n1 n2) : vsubst m n1.+1 n2.+1 :=
  var m bound .: σ >> vl_rename id shift.

Fixpoint tm_inst {m1 m2 n1 n2} (f : tysubst m1 m2) (g : vsubst m2 n1 n2) (s : tm m1 n1) : tm m2 n2 :=
  match s with
  | val s => val (vl_inst f g s)
  | app s t => app (tm_inst f g s) (tm_inst f g t)
  | tapp s A => tapp (tm_inst f g s) (tyinst f A)
  end
with vl_inst {m1 m2 n1 n2} (f : tysubst m1 m2) (g : vsubst m2 n1 n2) (s : vl m1 n1) : vl m2 n2 :=
  match s with
  | var x => g x
  | lam s => lam (tm_inst f (vup g) s)
  | tlam s => tlam (tm_inst (tup f) (g >> vl_rename shift id) s)
  end.

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

Lemma tv_ren_id m n :
  (forall s : tm m n, tm_rename id id s = s) /\
  (forall s : vl m n, vl_rename id id s = s).
Proof.
  move: m n. apply: tv_ind => //=
    [m n s->|m n s-> t->|m n s-> A|m n s ih|m n s ih] //.
  - by rewrite ty_ren_id.
  - unfold up; fsimpl; by rewrite ih.
  - unfold up; fsimpl; by rewrite ih.
Qed.

Lemma tm_ren_id m n (s : tm m n) : tm_rename id id s = s.
Proof. by case: (tv_ren_id m n). Qed.

Lemma vl_ren_id m n (s : vl m n) : vl_rename id id s = s.
Proof. by case: (tv_ren_id m n). Qed.

Lemma tv_ren_inst m1 n1 :
  (forall (s : tm m1 n1) m2 n2 (f : ren m1 m2) (g : ren n1 n2),
      tm_rename f g s = tm_inst (f >> @tvar _) (g >> @var _ _) s) /\
  (forall (s : vl m1 n1) m2 n2 (f : ren m1 m2) (g : ren n1 n2),
      vl_rename f g s = vl_inst (f >> @tvar _) (g >> @var _ _) s).
Proof.
  move: m1 n1; apply: tv_ind => //=
    [m1 n1 s ih|m1 n1 s ihs t iht|m1 n1 s ihs A|m1 n1 s ihs|m1 n1 s ihs]
      m2 n2 f g.
  - by rewrite ih.
  - by rewrite ihs iht.
  - by rewrite ihs ty_ren_inst.
  - rewrite ihs. by fsimpl.
  - rewrite ihs. by fsimpl.
Qed.

Lemma tm_ren_inst m1 m2 n1 n2 (f : ren m1 m2) (g : ren n1 n2) (s : tm m1 n1) :
  tm_rename f g s = tm_inst (f >> @tvar _) (g >> @var _ _) s.
Proof. by case: (tv_ren_inst m1 n1). Qed.

Lemma vl_ren_inst m1 m2 n1 n2 (f : ren m1 m2) (g : ren n1 n2) (s : vl m1 n1) :
  vl_rename f g s = vl_inst (f >> @tvar _) (g >> @var _ _) s.
Proof. by case: (tv_ren_inst m1 n1). Qed.

Lemma tm_inst_ids m n (s : tm m n) :
  tm_inst (@tvar _) (@var _ _) s = s.
Proof.
  by rewrite -tm_ren_inst tm_ren_id.
Qed.

Lemma vl_inst_ids m n (s : vl m n) :
  vl_inst (@tvar _) (@var _ _) s = s.
Proof.
  by rewrite -vl_ren_inst vl_ren_id.
Qed.

Lemma tv_ren_inst_comp m1 n1 :
  (forall (s : tm m1 n1) m2 m3 n2 n3 (f1 : ren m1 m2) (g1 : ren n1 n2)
    (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3),
      tm_inst f2 g2 (tm_rename f1 g1 s) = tm_inst (f1 >> f2) (g1 >> g2) s) /\
  (forall (s : vl m1 n1) m2 m3 n2 n3 (f1 : ren m1 m2) (g1 : ren n1 n2)
    (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3),
      vl_inst f2 g2 (vl_rename f1 g1 s) = vl_inst (f1 >> f2) (g1 >> g2) s).
Proof.
  move: m1 n1; apply: tv_ind => //=
    [m1 n1 s ih|m1 n1 s ihs t iht|m1 n1 s ihs A|m1 n1 s ihs|m1 n1 s ihs]
      m2 m3 n2 n3 f1 g1 f2 g2.
  - by rewrite ih.
  - by rewrite ihs iht.
  - by rewrite ihs ty_ren_inst_comp.
  - rewrite ihs. by fsimpl.
  - rewrite ihs. by fsimpl.
Qed.

Lemma tm_ren_inst_comp m1 m2 m3 n1 n2 n3 (f1 : ren m1 m2) (g1 : ren n1 n2)
      (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3) (s : tm m1 n1) :
  tm_inst f2 g2 (tm_rename f1 g1 s) = tm_inst (f1 >> f2) (g1 >> g2) s.
Proof. by case: (tv_ren_inst_comp m1 n1). Qed.

Lemma vl_ren_inst_comp m1 m2 m3 n1 n2 n3 (f1 : ren m1 m2) (g1 : ren n1 n2)
      (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3) (s : vl m1 n1) :
  vl_inst f2 g2 (vl_rename f1 g1 s) = vl_inst (f1 >> f2) (g1 >> g2) s.
Proof. by case: (tv_ren_inst_comp m1 n1). Qed.

Lemma tm_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) :
  tm_rename f2 g2 (tm_rename f1 g1 s) = tm_rename (f1 >> f2) (g1 >> g2) s.
Proof.
  by rewrite tm_ren_inst tm_ren_inst_comp tm_ren_inst.
Qed.

Lemma vl_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 : vl m1 n1) :
  vl_rename f2 g2 (vl_rename f1 g1 s) = vl_rename (f1 >> f2) (g1 >> g2) s.
Proof.
  by rewrite vl_ren_inst vl_ren_inst_comp vl_ren_inst.
Qed.

Lemma vup_up_comp m1 m2 n1 n2 n3 (f1 : vsubst m1 n1 n2) (g : ren m1 m2) (f2 : ren n2 n3) :
  vup f1 >> vl_rename g (up f2) = vup (f1 >> vl_rename g f2).
Proof.
  fext=> /=-[i|]//=. by rewrite !vl_ren_comp.
Qed.

Lemma tv_inst_ren_comp m1 n1 :
  (forall (s : tm m1 n1) m2 m3 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
    (f2 : ren m2 m3) (g2 : ren n2 n3),
      tm_rename f2 g2 (tm_inst f1 g1 s) = tm_inst (f1 >> tyrename f2) (g1 >> vl_rename f2 g2) s) /\
  (forall (s : vl m1 n1) m2 m3 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
    (f2 : ren m2 m3) (g2 : ren n2 n3),
      vl_rename f2 g2 (vl_inst f1 g1 s) = vl_inst (f1 >> tyrename f2) (g1 >> vl_rename f2 g2) s).
Proof.
  move: m1 n1; apply: tv_ind => //=
    [m1 n1 s ih|m1 n1 s ihs t iht|m1 n1 s ihs A|m1 n1 s ihs|m1 n1 s ihs]
      m2 m3 n2 n3 f1 g1 f2 g2.
  - by rewrite ih.
  - by rewrite ihs iht.
  - by rewrite ihs ty_inst_ren_comp.
  - by rewrite ihs vup_up_comp.
  - rewrite ihs ty_tup_up_comp. do 2 f_equal; fext=> i/=.
    by rewrite !vl_ren_comp.
Qed.

Lemma tm_inst_ren_comp m1 m2 m3 n1 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
      (f2 : ren m2 m3) (g2 : ren n2 n3) (s : tm m1 n1) :
  tm_rename f2 g2 (tm_inst f1 g1 s) = tm_inst (f1 >> tyrename f2) (g1 >> vl_rename f2 g2) s.
Proof. by case: (tv_inst_ren_comp m1 n1). Qed.

Lemma vl_inst_ren_comp m1 m2 m3 n1 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
      (f2 : ren m2 m3) (g2 : ren n2 n3) (s : vl m1 n1) :
  vl_rename f2 g2 (vl_inst f1 g1 s) = vl_inst (f1 >> tyrename f2) (g1 >> vl_rename f2 g2) s.
Proof. by case: (tv_inst_ren_comp m1 n1). Qed.

Lemma vup_comp m1 m2 n1 n2 n3 (f1 : vsubst m1 n1 n2) (f2 : vsubst m2 n2 n3) (g : tysubst m1 m2) :
  vup f1 >> vl_inst g (vup f2) = vup (f1 >> vl_inst g f2).
Proof.
  fext=> /=-[i|]//=. rewrite vl_ren_inst_comp vl_inst_ren_comp.
  f_equal; fext=> j/=. by rewrite ty_ren_id.
Qed.

Lemma tv_inst_comp m1 n1 :
  (forall (s : tm m1 n1) m2 m3 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
    (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3),
      tm_inst f2 g2 (tm_inst f1 g1 s) = tm_inst (f1 >> tyinst f2) (g1 >> vl_inst f2 g2) s) /\
  (forall (s : vl m1 n1) m2 m3 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
    (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3),
      vl_inst f2 g2 (vl_inst f1 g1 s) = vl_inst (f1 >> tyinst f2) (g1 >> vl_inst f2 g2) s).
Proof.
  move: m1 n1; apply: tv_ind => //=
    [m1 n1 s ih|m1 n1 s ihs t iht|m1 n1 s ihs A|m1 n1 s ihs|m1 n1 s ihs]
      m2 m3 n2 n3 f1 g1 f2 g2.
  - by rewrite ih.
  - by rewrite ihs iht.
  - by rewrite ihs ty_inst_comp.
  - by rewrite ihs vup_comp.
  - rewrite ihs ty_tup_comp. do 2 f_equal; fext=> i/=.
    by rewrite vl_ren_inst_comp vl_inst_ren_comp.
Qed.

Lemma tm_inst_comp m1 m2 m3 n1 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
      (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3) (s : tm m1 n1) :
  tm_inst f2 g2 (tm_inst f1 g1 s) = tm_inst (f1 >> tyinst f2) (g1 >> vl_inst f2 g2) s.
Proof. by case: (tv_inst_comp m1 n1). Qed.

Lemma vl_inst_comp m1 m2 m3 n1 n2 n3 (f1 : tysubst m1 m2) (g1 : vsubst m2 n1 n2)
      (f2 : tysubst m2 m3) (g2 : vsubst m3 n2 n3) (s : vl m1 n1) :
  vl_inst f2 g2 (vl_inst f1 g1 s) = vl_inst (f1 >> tyinst f2) (g1 >> vl_inst f2 g2) s.
Proof. by case: (tv_inst_comp m1 n1). Qed.