Require Import base ord data.fintype ccomega.sorts.

Inductive tm (n : nat) : Type :=
| var (x : fin n)
| univ (s : sort)
| app (s t : tm n)
| lam (s : tm n.+1)
| prod (s : tm n) (t : tm n.+1).

Fixpoint rename {m n} (f : ren m n) (s : tm m) : tm n :=
  match s with
  | var x => var (f x)
  | univ s => univ n s
  | app s t => app (rename f s) (rename f t)
  | lam s => lam (rename (up f) s)
  | prod s t => prod (rename f s) (rename (up f) t)
  end.

Definition subst m n := fin m -> tm n.

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

Fixpoint inst {m n} (f : subst m n) (s : tm m) : tm n :=
  match s with
  | var x => f x
  | univ s => univ n s
  | app s t => app (inst f s) (inst f t)
  | lam s => lam (inst (upi f) s)
  | prod s t => prod (inst f s) (inst (upi f) t)
  end.

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

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

Lemma ren_inst m n (f : ren m n) (s : tm m) :
  rename f s = inst (f >> @var _) s.
Proof.
  elim: s n f => //={m}[m s ihs t iht|m s ihs|m s ihs t iht] n f.
  - by rewrite ihs iht.
  - rewrite ihs. by fsimpl.
  - rewrite ihs iht. by fsimpl.
Qed.

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

Lemma ren_inst_comp m n k (f : ren m n) (g : subst n k) (s : tm m) :
  inst g (rename f s) = inst (f >> g) s.
Proof.
  elim: s n k f g => //={m}[m s ihs t iht|m s ihs|m s ihs t iht] n k f g.
  - by rewrite ihs iht.
  - rewrite ihs. by fsimpl.
  - rewrite ihs iht. by fsimpl.
Qed.

Lemma ren_comp m n k (f : ren m n) (g : ren n k) (s : tm m) :
  rename g (rename f s) = rename (f >> g) s.
Proof.
  by rewrite ren_inst ren_inst_comp ren_inst.
Qed.

Lemma upi_up_comp m n k (f : subst m n) (g : ren n k) :
  upi f >> rename (up g) = upi (f >> rename g).
Proof.
  fext=> /=-[i|]//=. by rewrite !ren_comp.
Qed.

Lemma inst_ren_comp m n k (f : subst m n) (g : ren n k) (s : tm m) :
  rename g (inst f s) = inst (f >> rename g) s.
Proof.
  elim: s n k f g => //={m}[m s ihs t iht|m s ihs|m s ihs t iht] n k f g.
  - by rewrite ihs iht.
  - by rewrite ihs upi_up_comp.
  - by rewrite ihs iht upi_up_comp.
Qed.

Lemma upi_comp m n k (f : subst m n) (g : subst n k) :
  upi f >> inst (upi g) = upi (f >> inst g).
Proof.
  fext=> /=-[i|]//=. by rewrite ren_inst_comp inst_ren_comp.
Qed.

Lemma inst_comp m n k (f : subst m n) (g : subst n k) (s : tm m) :
  inst g (inst f s) = inst (f >> inst g) s.
Proof.
  elim: s n k f g => //={m}[m s ihs t iht|m s ihs|m s ihs t iht] n k f g.
  - by rewrite ihs iht.
  - by rewrite ihs upi_comp.
  - by rewrite ihs iht upi_comp.
Qed.