Require Import base data.fintype.

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

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.

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.

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.

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.

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.