# Syntax of System F Types

Require Import base data.fintype.

Inductive ty (n : nat) : Type :=
| tvar (x : fin n)
| arr (A B : ty n)
| all (A : ty n.+1).

## Instantiation

Fixpoint tyrename {m n} (f : ren m n) (s : ty m) : ty n :=
match s with
| tvar x => tvar (f x)
| arr s t => arr (tyrename f s) (tyrename f t)
| all s => all (tyrename (up f) s)
end.

Definition tysubst m n := fin m -> ty n.

Definition tup {m n} (σ : tysubst m n) : tysubst m.+1 n.+1 :=
tvar bound .: σ >> tyrename shift.

Fixpoint tyinst {m n} (f : tysubst m n) (s : ty m) : ty n :=
match s with
| tvar x => f x
| arr s t => arr (tyinst f s) (tyinst f t)
| all s => all (tyinst (tup f) s)
end.

## Renaming as a special case of instantiation

Lemma ty_ren_inst m n (f : ren m n) (s : ty m) :
tyrename f s = tyinst (f >> @tvar _) s.
Proof.
elim: s n f => //={m}[m s ihs t iht|m s ihs] n f.
- by rewrite ihs iht.
- rewrite ihs. by fsimpl.
Qed.

## Identity law

Lemma tup_ids n : tup (@tvar n) = @tvar n.+1.
Proof. fext=>/=. by case. Qed.

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

Lemma ty_inst_ids n (s : ty n) :
tyinst (@tvar _) s = s.
Proof.
by rewrite -ty_ren_inst ty_ren_id.
Qed.

Lemma ty_scomp_idR m n (σ : tysubst m n) :
σ >> tyinst (@tvar n) = σ.
Proof.
fext=> i/=. exact: ty_inst_ids.
Qed.

## Composition law

Lemma ty_ren_inst_comp m n k (f : ren m n) (g : tysubst n k) (s : ty m) :
tyinst g (tyrename f s) = tyinst (f >> g) s.
Proof.
elim: s n k f g => //={m}[m s ihs t iht|m s ihs] n k f g.
- by rewrite ihs iht.
- rewrite ihs. by fsimpl.
Qed.

Lemma ty_ren_comp m n k (f : ren m n) (g : ren n k) (s : ty m) :
tyrename g (tyrename f s) = tyrename (f >> g) s.
Proof.
by rewrite ty_ren_inst ty_ren_inst_comp ty_ren_inst.
Qed.

Lemma ty_tup_up_comp m n k (f : tysubst m n) (g : ren n k) :
tup f >> tyrename (up g) = tup (f >> tyrename g).
Proof.
fext=> /=-[i|]//=. by rewrite !ty_ren_comp.
Qed.

Lemma ty_inst_ren_comp m n k (f : tysubst m n) (g : ren n k) (s : ty m) :
tyrename g (tyinst f s) = tyinst (f >> tyrename g) s.
Proof.
elim: s n k f g => //={m}[m s ihs t iht|m s ihs] n k f g.
- by rewrite ihs iht.
- by rewrite ihs ty_tup_up_comp.
Qed.

Lemma ty_tup_comp m n k (f : tysubst m n) (g : tysubst n k) :
tup f >> tyinst (tup g) = tup (f >> tyinst g).
Proof.
fext=> /=-[i|]//=. by rewrite ty_ren_inst_comp ty_inst_ren_comp.
Qed.

Lemma ty_inst_comp m n k (f : tysubst m n) (g : tysubst n k) (s : ty m) :
tyinst g (tyinst f s) = tyinst (f >> tyinst g) s.
Proof.
elim: s n k f g => //={m}[m s ihs t iht|m s ihs] n k f g.
- by rewrite ihs iht.
- by rewrite ihs ty_tup_comp.
Qed.

Lemma ty_scomp_assoc m n k l (σ : tysubst m n) (τ : tysubst n k) (θ : tysubst k l) :
(σ >> tyinst τ) >> tyinst θ = σ >> tyinst (τ >> tyinst θ).
Proof.
fext=> i /=. exact: ty_inst_comp.
Qed.

## Simple Models

Structure model (V D : Type) := mk_model
{ Var : V -> D
; Arr : D -> D -> D
; All : (V -> D) -> D
}.

Section Evaluation.
Variable (V D : Type) (M : model V D).

Fixpoint eval {m} (ρ : fin m -> V) (A : ty m) : D :=
match A with
| tvar i => Var M (ρ i)
| arr A B => Arr M (eval ρ A) (eval ρ B)
| all A => All M (fun d => eval (d .: ρ) A)
end.

Lemma eval_ren m n (ξ : ren m n) (A : ty m) (ρ : fin n -> V) :
eval ρ (tyrename ξ A) = eval (ξ >> ρ) A.
Proof.
elim: A n ξ ρ => //={m}[m A ih1 B ih2|m A ih] n ξ ρ.
- by rewrite ih1 ih2.
- f_equal; fext=> d. rewrite ih. by fsimpl.
Qed.

Lemma eval_weaken m (A : ty m) (ρ : fin m -> V) (d : V) :
eval (d .: ρ) (tyrename shift A) = eval ρ A.
Proof. by rewrite eval_ren. Qed.

Definition lift : model D D :=
mk_model id (Arr M) (fun F => All M (Var M >> F)).

End Evaluation.

Lemma eval_inst V D m n (M : model V D) (σ : tysubst m n) (A : ty m) (ρ : fin n -> V) :
eval M ρ (tyinst σ A) = eval (lift M) (σ >> eval M ρ) A.
Proof.
elim: A n σ ρ => //={m}[m A ih1 B ih2|m A ih] n σ ρ.
- by rewrite ih1 ih2.
- f_equal; fext=> d. rewrite ih /=. f_equal; fext=> /=; case=>//=i.
exact: eval_weaken.
Qed.

Lemma eval_beta V D m (M : model V D) (A : ty m.+1) (B : ty m) (ρ : fin m -> V) :
eval M ρ (tyinst (B .: @tvar m) A) = eval (lift M) (eval M ρ B .: ρ >> Var M) A.
Proof. rewrite eval_inst. by fsimpl. Qed.

Lemma eval_lift V D m (M : model V D) (A : ty m) (ρ : fin m -> V) :
eval M ρ A = eval (lift M) (ρ >> Var M) A.
Proof. by rewrite -{1}[A]ty_inst_ids eval_inst. Qed.