# Syntax of System F Terms

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).

## Instantiation

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.

## Identity renaming law

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.

## Renaming as a special case of instantiation

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.

## Identity substitution law

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

## Composition law

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.