# Section 5: System F Terms and Values

This file contains the definition of System F Terms and Values and their multivariate traversals and models (Section 5). This part of the code is intended to be generated by Autosubst 2.

From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Framework.graded Framework.sysf_types.
Set Implicit Arguments.
Unset Strict Implicit.

Local Ltac asimpl :=
repeat progress (cbn; fsimpl; gsimpl; ty_simpl).

Module TmVl.

## Computations and Values

The type vl m n represents a value with m free type variables and n free value variables in its scope. Similarly, the type tm m n represents computations (i.e., non-value terms) with m type variables and n value variables.

Section Defs.

Unset Elimination Schemes.
Inductive tm (m n : nat) :=
| tvl (v : vl m n)
| app (s : tm m n) (t : tm m n)
| App (s : tm m n) (A : ty m)
with vl (m n : nat) :=
| var (i : fin n) : vl m n
| lam (A : ty m) (b : tm m n.+1) : vl m n
| Lam (b : tm m.+1 n) : vl m n.
Set Elimination Schemes.
Scheme vl_ind := Induction for vl Sort Prop
with tm_ind := Induction for tm Sort Prop.
Combined Scheme tv_ind from vl_ind, tm_ind.

Arguments var {m n}, m n.

## Traversals and their Evaluation

The type traversal Vty Dty Vvl Dvl Dtm represents a traversal (Definition 5.1) parameterised by semantic value domains Vty and Vvl and semantic expression domains Dty, Dvl, and Dtm.
Evaluation (Definition 5.3) requires the corresponding semantic value domains to be graded, respectively bigraded (Definition 3.2, Definition 5.2).

Structure traversal (Vty Dty : nat -> Type) (Vvl Dvl Dtm : nat -> nat -> Type) := Traversal
{ tvar : forall m n, Vvl m n -> Dvl m n
; tlam : forall m n, Dty m -> (fun m n => Vvl m n -> Dtm m n) m n -> Dvl m n
; tLam : forall m n, (fun m n => Vty m -> Dtm m n) m n -> Dvl m n
; ttvl : forall m n, Dvl m n -> Dtm m n
; tapp : forall m n, Dtm m n -> Dtm m n -> Dtm m n
; tApp : forall m n, Dtm m n -> Dty m -> Dtm m n
}.
Arguments tvar {Vty Dty Vvl Dvl Dtm} t {m n} i.
Arguments tlam {Vty Dty Vvl Dvl Dtm} t {m n} A F.
Arguments tLam {Vty Dty Vvl Dvl Dtm} t {m n} F.
Arguments ttvl {Vty Dty Vvl Dvl Dtm} t {m n} v.
Arguments tapp {Vty Dty Vvl Dvl Dtm} t {m n} f a.
Arguments tApp {Vty Dty Vvl Dvl Dtm} t {m n} f A.

Fixpoint eval_vl {Vty : graded1} {Dty : nat -> Type} {Vvl : graded2} {Dvl Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vvl Dvl Dtm)
{m1 n1 m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (v : vl m1 n1) : Dvl m2 n2 :=
match v with
| var x => tvar E (theta x)
| lam A s => tlam E (Ty.eval T rho A) (fun _ _ xi zeta v => eval_tm T E (rho >> th1 xi) (v .: theta >> th2 xi zeta) s)
| Lam s => tLam E (fun _ _ xi zeta v => eval_tm T E (v .: rho >> th1 xi) (theta >> th2 xi zeta) s)
end
with eval_tm {Vty : graded1} {Dty : nat -> Type} {Vvl : graded2} {Dvl Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vvl Dvl Dtm)
{m1 n1 m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (s : tm m1 n1) : Dtm m2 n2 :=
match s with
| tvl v => ttvl E (eval_vl T E rho theta v)
| app s t => tapp E (eval_tm T E rho theta s) (eval_tm T E rho theta t)
| App s A => tApp E (eval_tm T E rho theta s) (Ty.eval T rho A)
end.

## Models (Definition 5.4)

A traversal is a model if it satisfies additional naturality conditions.

Structure is_natural {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (E : traversal Vty Dty Vvl Dvl Dtm) := IsNatural
{ nvar : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (i : Vvl m1 n1),
(tvar E i) (xi,zeta) = tvar E (i (xi,zeta))
; nlam : forall m1 n1 (A : Dty m1) (F : (fun m n => Vvl m n -> Dtm m n) m1 n1),
(forall m2 m3 n2 n3 (xi1 : iren m1 m2) (xi2 : iren m2 m3) (zeta1 : iren n1 n2) (zeta2 : iren n2 n3) (i : Vvl m2 n2),
(F m2 n2 xi1 zeta1 i) (xi2,zeta2) = F m3 n3 (xi1 >>> xi2) (zeta1 >>> zeta2) (i (xi2,zeta2))) ->
forall m2 n2 (xi : iren m1 m2) (zeta : iren n1 n2),
(tlam E A F) (xi,zeta) = tlam E (A xi) (F (xi,zeta))
; nLam : forall m1 n1 (F : (fun m n => Vty m -> Dtm m n) m1 n1),
(forall m2 m3 n2 n3 (xi1 : iren m1 m2) (xi2 : iren m2 m3) (zeta1 : iren n1 n2) (zeta2 : iren n2 n3) (i : Vty m2),
(F m2 n2 xi1 zeta1 i) (xi2,zeta2) = F m3 n3 (xi1 >>> xi2) (zeta1 >>> zeta2) (i xi2)) ->
forall m2 n2 (xi : iren m1 m2) (zeta : iren n1 n2),
(tLam E F) (xi,zeta) = tLam E (F (xi,zeta))
; ntvl : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (v : Dvl m1 n1),
(ttvl E v) (xi,zeta) = ttvl E (v (xi,zeta))
; napp : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (a b : Dtm m1 n1),
(tapp E a b) (xi,zeta) = tapp E (a (xi,zeta)) (b (xi,zeta))
; nApp : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (a : Dtm m1 n1) (A : Dty m1),
(tApp E a A) (xi,zeta) = tApp E (a (xi,zeta)) (A xi)
}.

Structure model (Vty Dty : graded1) (Vvl Dvl Dtm : graded2) := Model
{ base : traversal Vty Dty Vvl Dvl Dtm
; _ : is_natural base
}.
Every model is a traversal.
Local Coercion base : model >-> traversal.

Definition model_of {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (Vty' Dty' : nat -> Type) (Vvl' Dvl' Dtm' : nat -> nat -> Type)
of phant_id (Vty : nat -> Type) Vty' of phant_id (Dty : nat -> Type) Dty'
of phant_id (Vvl : nat -> nat -> Type) Vvl' of phant_id (Dvl : nat -> nat -> Type) Dvl'
of phant_id (Dtm : nat -> nat -> Type) Dtm'
:= model Vty Dty Vvl Dvl Dtm.

Local Notation "'{' 'model' Vty ',' Dty ',' Vvl ',' Dvl ',' Dtm '}'" := (@model_of _ _ _ _ _ Vty Dty Vvl Dvl Dtm id id id id id) : type_scope.

Definition model_is_natural {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (E : model Vty Dty Vvl Dvl Dtm) : is_natural E :=
let: Model _ c := E in c.
Local Coercion model_is_natural : model >-> is_natural.

## Renaming (Definition 5.6)

Definition and properties.

Definition ren_traversal : traversal fin ty fin2 vl tm :=
Traversal (@var) (fun m n A F => lam A (F m n.+1 idren shift bound))
(fun m n F => Lam (F m.+1 n shift idren bound))
(@tvl) (@app) (@App).
Local Notation vl_ren := (eval_vl Ty.ren_traversal ren_traversal).
Local Notation tm_ren := (eval_tm Ty.ren_traversal ren_traversal).
Canonical vl_graded2 := Eval hnf in Graded2 vl (@eval_vl _ _ _ _ _ Ty.ren_traversal ren_traversal).
Canonical tm_graded2 := Eval hnf in Graded2 tm (@eval_tm _ _ _ _ _ Ty.ren_traversal ren_traversal).

Lemma th2_vlE {m1 m2 n1 n2} (xi : iren m1 m2) (zeta : iren n1 n2) (v : vl m1 n1) :
v (xi, zeta) = vl_ren xi zeta v.
Proof. by []. Qed.

Lemma th2_tmE {m1 m2 n1 n2} (xi : iren m1 m2) (zeta : iren n1 n2) (s : tm m1 n1) :
s (xi, zeta) = tm_ren xi zeta s.
Proof. by []. Qed.

Lemma ren_is_natural : is_natural ren_traversal.
Proof.
apply: IsNatural => //=[m1 n1 A|m1 n1] F H m2 n2 xi zeta.
- rewrite th2_vlE /=. asimpl. f_equal. rewrite -shift_up. exact: (H _ _ _ _ _ _ _ (up zeta)).
- rewrite th2_vlE /=. asimpl. f_equal. rewrite -shift_up. exact: (H _ _ _ _ _ (up xi)).
Qed.
Canonical ren_model : {model fin, ty, fin2, vl, tm} := Eval hnf in Model ren_is_natural.

Lemma ren_vl_tm_id m n :
(forall v : vl m n, vl_ren id id v = v) /\
(forall s : tm m n, tm_ren id id s = s).
Proof.
move: m n. apply tv_ind => //=[m n A b ih|m n b ih|m n v->|m n s->t->|m n s->A]//.
- asimpl. by rewrite ih.
- asimpl. by rewrite ih.
- by asimpl.
Qed.

Lemma ren_vl_id {m n : nat} (v : vl m n) : vl_ren id id v = v.
Proof. by case: (ren_vl_tm_id m n). Qed.

Lemma ren_tm_id {m n : nat} (s : tm m n) : tm_ren id id s = s.
Proof. by case: (ren_vl_tm_id m n). Qed.

Section EvalRen.
Context {Vty : graded1} {Dty : nat -> Type} {Vvl : graded2} {Dvl Dtm : nat -> nat -> Type}
(t1 : Ty.traversal Vty Dty) (t2 : traversal Vty Dty Vvl Dvl Dtm).

Lemma eval_vl_tm_ren m1 n1 :
(forall (v : vl m1 n1) m2 m3 n2 n3 (xi : ren m1 m2) (zeta : ren n1 n2) (rho1 : fin m2 -> Vty m3) (rho2 : fin n2 -> Vvl m3 n3),
eval_vl t1 t2 rho1 rho2 (vl_ren xi zeta v) = eval_vl t1 t2 (xi >> rho1) (zeta >> rho2) v) /\
(forall (s : tm m1 n1) m2 m3 n2 n3 (xi : ren m1 m2) (zeta : ren n1 n2) (rho1 : fin m2 -> Vty m3) (rho2 : fin n2 -> Vvl m3 n3),
eval_tm t1 t2 rho1 rho2 (tm_ren xi zeta s) = eval_tm t1 t2 (xi >> rho1) (zeta >> rho2) s).
Proof.
move: m1 n1. apply tv_ind => //=[m n A b ih|m n b ih|m n v ih|m n s ihs t iht|m n s ih A] m2 m3 n2 n3 xi zeta rho1 rho2.
- asimpl. f_equal;fext=> m4 n4 xi' zeta' i. rewrite ih. by asimpl.
- f_equal;fext=> m4 n4 xi' zeta' i. rewrite ih. by asimpl.
- by rewrite ih.
- by rewrite ihs iht.
- asimpl. by rewrite ih.
Qed.

Lemma eval_vl_ren {m1 m2 m3 n1 n2 n3} (v : vl m1 n1) (xi : ren m1 m2) (zeta : ren n1 n2)
(rho1 : fin m2 -> Vty m3) (rho2 : fin n2 -> Vvl m3 n3) :
eval_vl t1 t2 rho1 rho2 (vl_ren xi zeta v) = eval_vl t1 t2 (xi >> rho1) (zeta >> rho2) v.
Proof. by case: (eval_vl_tm_ren m1 n1). Qed.

Theorem 5.7
Lemma eval_tm_ren {m1 m2 m3 n1 n2 n3} (s : tm m1 n1) (xi : ren m1 m2) (zeta : ren n1 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3) :
eval_tm t1 t2 rho theta (tm_ren xi zeta s) = eval_tm t1 t2 (xi >> rho) (zeta >> theta) s.
Proof. by case: (eval_vl_tm_ren m1 n1). Qed.
End EvalRen.

Lemma ren_vl_comp {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (xi2 : ren m2 m3)
(zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (v : vl m1 n1) :
vl_ren xi2 zeta2 (vl_ren xi1 zeta1 v) = vl_ren (xi1 >> xi2) (zeta1 >> zeta2) v.
Proof. exact: eval_vl_ren. Qed.

Lemma ren_tm_comp {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (xi2 : ren m2 m3)
(zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (s : tm m1 n1) :
tm_ren xi2 zeta2 (tm_ren xi1 zeta1 s) = tm_ren (xi1 >> xi2) (zeta1 >> zeta2) s.
Proof. exact: eval_tm_ren. Qed.

Lemma ren_vl_tm_inj :
forall m1 n1,
(forall (v1 v2 : vl m1 n1) {m2 n2} (xi : ren m1 m2) (zeta : ren n1 n2),
injective xi -> injective zeta -> vl_ren xi zeta v1 = vl_ren xi zeta v2 -> v1 = v2) /\
(forall (s1 s2 : tm m1 n1) {m2 n2} (xi : ren m1 m2) (zeta : ren n1 n2),
injective xi -> injective zeta -> tm_ren xi zeta s1 = tm_ren xi zeta s2 -> s1 = s2).
Proof.
apply tv_ind => [m1 n1 i|m1 n1 A1 b1 ih|m1 n1 b1 ih|m1 n1 v1 ih|m1 n1 s1 ihs t1 iht|m1 n1 s1 ih A1].
- by move=> [j||]//= m2 n2 xi zeta fP gP [/gP->].
- move=> [|A2 b2|]//= m2 n2 xi zeta fP gP [/(Ty.ren_inj fP)->/ih->//].
by move=> /=[i|] [j|]//=[/gP->].
- by move=> [||b2]//= m2 n2 xi zeta fP gP [/ih->//] /=[i|] [j|]//=[/fP->].
- by move=> [v2||]//= m2 n2 xi zeta fP gP [/ih->].
- by move=> [|s2 t2|]//= m2 n2 xi zeta fP gP [/ihs->///iht->].
- by move=> [||s2 A2]//= m2 n2 xi zeta fP gP [/ih->///Ty.ren_inj->].
Qed.

Lemma ren_vl_inj {m1 m2 n1 n2} (xi : ren m1 m2) (zeta : ren n1 n2) (v1 v2 : vl m1 n1) :
injective xi -> injective zeta -> vl_ren xi zeta v1 = vl_ren xi zeta v2 -> v1 = v2.
Proof. case: (ren_vl_tm_inj m1 n1) => H _. exact: H. Qed.

Lemma ren_tm_inj {m1 m2 n1 n2} (xi : ren m1 m2) (zeta : ren n1 n2) (s1 s2 : tm m1 n1) :
injective xi -> injective zeta -> tm_ren xi zeta s1 = tm_ren xi zeta s2 -> s1 = s2.
Proof. case: (ren_vl_tm_inj m1 n1) => _ H. exact: H. Qed.

Canonical vl_pgraded2 := Eval hnf in PGraded2 vl (fun m1 m2 n1 n2 xi zeta v1 v2 =>
@ren_vl_inj m1 m2 n1 n2 xi zeta v1 v2 (@iren_inj _ _ xi) (@iren_inj _ _ zeta)).

Canonical tm_pgraded2 := Eval hnf in PGraded2 tm (fun m1 m2 n1 n2 xi zeta v1 v2 =>
@ren_tm_inj m1 m2 n1 n2 xi zeta v1 v2 (@iren_inj _ _ xi) (@iren_inj _ _ zeta)).

## Lifting (Definition 5.5)

Definition lift {Vty Dty : nat -> Type} {Vvl Dvl Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vvl Dvl Dtm) : traversal Dty Dty Dvl Dvl Dtm.
apply: Traversal.
- exact (fun _ _ => id).
- intros m n A F. apply (tlam E). exact A. intros m' n' xi zeta v. apply (F m' n' xi zeta).
apply (tvar E). exact v.
- intros m n F. apply (tLam E). intros m' n' xi zeta v. apply (F m' n' xi zeta).
apply (Ty.tvar T). exact v.
- exact (@ttvl _ _ _ _ _ E).
- exact (@tapp _ _ _ _ _ E).
- exact (@tApp _ _ _ _ _ E).
Defined.

Definition lift_is_natural {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty)
(E : model Vty Dty Vvl Dvl Dtm) :
is_natural (lift T E).
Proof.
apply: IsNatural => //=[m1 n1 A F H m2 n2 xi zeta|m1 n1 F H m2 n2 xi zeta|m1 m2 n1 n2 xi zeta v|m1 m2 n1 n2 xi zeta a b|m1 m2 n1 n2 xi zeta a A].
- apply: (nlam E); intros; by rewrite H (nvar E).
- apply: (nLam E); intros; by rewrite H (Ty.nvar T).
- exact: (ntvl E).
- exact: (napp E).
- exact: (nApp E).
Qed.

Canonical lift_model {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) : model Dty Dty Dvl Dvl Dtm :=
Eval hnf in Model (lift_is_natural T E).

## Theorem 5.8

Definition lift_vl_tm_embed {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) (m1 n1 : nat) :
(forall (v : vl m1 n1) {m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2),
eval_vl T E rho theta v = eval_vl (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) v) /\
(forall (s : tm m1 n1) {m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2),
eval_tm T E rho theta s = eval_tm (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) s).
Proof.
move: m1 n1. apply tv_ind => //=[m1 n1 A b ih|m1 n1 b ih|m1 n1 v ih|m1 n1 s ihs t iht|m1 n1 s ihs A] m2 n2 rho theta.
- rewrite Ty.embed. f_equal;fext=> m3 n3 xi zeta i. rewrite ih. asimpl. f_equal; fext=> j /=. symmetry. exact: (Ty.nvar T). case: j => //= j. symmetry. exact: (nvar E).
- f_equal;fext=> m3 n3 xi zeta i. rewrite ih. asimpl. f_equal;fext=>/=. case=> //= j. symmetry.
exact: (Ty.nvar T). move=> j /=. symmetry. exact: (nvar E).
- by rewrite ih.
- by rewrite ihs iht.
- by rewrite ihs Ty.embed.
Qed.

Lemma lift_vl_embed {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) {m1 m2 n1 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (v : vl m1 n1) :
eval_vl T E rho theta v =
eval_vl (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) v.
Proof. by case: (lift_vl_tm_embed T E m1 n1). Qed.

Lemma lift_tm_embed {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) {m1 m2 n1 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (s : tm m1 n1) :
eval_tm T E rho theta s =
eval_tm (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) s.
Proof. by case: (lift_vl_tm_embed T E m1 n1). Qed.

## Instantiation

Notation inst_traversal := (lift Ty.ren_traversal ren_traversal).
Notation inst_vl := (eval_vl Ty.inst_traversal inst_traversal).
Notation inst_tm := (eval_tm Ty.inst_traversal inst_traversal).
Notation "v .[ sigma , tau ]" := (inst_vl sigma tau v)
(at level 2, left associativity, format "v .[ sigma , tau ]") : vl_inst_scope.
Delimit Scope vl_inst_scope with vl.
Notation "s .[ sigma , tau ]" := (inst_tm sigma tau s)
(at level 2, left associativity, format "s .[ sigma , tau ]") : tm_inst_scope.
Delimit Scope tm_inst_scope with tm.

Definition inst_vl_id {m n : nat} (v : vl m n) :
v.[Ty.var, var]%vl = v.
Proof.
rewrite -{2}[v]th_id2/=. symmetry. exact: lift_vl_embed.
Qed.

Definition inst_tm_id {m n : nat} (s : tm m n) :
s.[Ty.var, var]%tm = s.
Proof.
rewrite -{2}[s]th_id2/=. symmetry. exact: lift_tm_embed.
Qed.

Definition vl_ren_inst {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (zeta1 : ren n1 n2) (xi2 : fin m2 -> ty m3) (zeta2 : fin n2 -> vl m3 n3) (v : vl m1 n1) :
(vl_ren xi1 zeta1 v).[xi2, zeta2]%vl = v.[xi1 >> xi2, zeta1 >> zeta2]%vl.
Proof. exact: eval_vl_ren. Qed.

Definition tm_ren_inst {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (zeta1 : ren n1 n2) (xi2 : fin m2 -> ty m3) (zeta2 : fin n2 -> vl m3 n3) (s : tm m1 n1) :
(tm_ren xi1 zeta1 s).[xi2, zeta2]%tm = s.[xi1 >> xi2, zeta1 >> zeta2]%tm.
Proof. exact: eval_tm_ren. Qed.

## Naturality

Definition naturality_vl_tm {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2} (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) (m1 n1 : nat) :
(forall (v : vl m1 n1) {m2 m3 n2 n3} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3),
(eval_vl t1 t2 rho theta v) (xi,zeta) = eval_vl t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) v)
/\
(forall (s : tm m1 n1) {m2 m3 n2 n3} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3),
(eval_tm t1 t2 rho theta s) (xi,zeta) = eval_tm t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) s).
Proof.
move: m1 n1. apply tv_ind =>[m1 n1 i|m1 n1 A b ih|m1 n1 b ih|m1 n1 v ih|m1 n1 s ihs t iht|m1 n1 s ihs A] m2 m3 n2 n3 rho theta xi zeta.
- exact: (nvar t2).
- cbn. rewrite (nlam t2). f_equal. by asimpl. fext=> m4 n4 xi' zeta' i /=. by asimpl.
intros. rewrite ih. by asimpl.
- cbn. rewrite (nLam t2). f_equal. fext=> /=m4 n4 xi' zeta' i. by asimpl.
intros. rewrite ih. by asimpl.
- by rewrite/=(ntvl t2) ih.
- by rewrite/=(napp t2) ihs iht.
- by rewrite/=(nApp t2) ihs Ty.naturality.
Qed.

(t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3}
(rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3)
(v : vl m1 n1) :
(eval_vl t1 t2 rho theta v) (xi,zeta) = eval_vl t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) v.
Proof. by case: (naturality_vl_tm t1 t2 m1 n1). Qed.

(t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3}
(rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3)
(s : tm m1 n1) :
(eval_tm t1 t2 rho theta s) (xi,zeta) = eval_tm t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) s.
Proof. by case: (naturality_vl_tm t1 t2 m1 n1). Qed.

## Compatibility with instantiation

Shown via the definition of models.
Theorem 5.9
(t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) (m1 n1 : nat) :
(forall (v : vl m1 n1) {m2 m3 n2 n3 : nat} (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3),
eval_vl t1 t2 rho theta v.[sigma, tau]%vl =
eval_vl (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) v)
/\
(forall (s : tm m1 n1) {m2 m3 n2 n3 : nat} (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3),
eval_tm t1 t2 rho theta s.[sigma, tau]%tm =
eval_tm (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) s).
Proof.
move: m1 n1. apply tv_ind => //=[m1 n1 A b ih|m1 n1 b ih|m1 n1 v ih|m1 n1 s ihs t iht|m1 n1 s ihs A] m2 m3 n2 n3 sigma tau rho theta.
- f_equal. by asimpl. fext=>/=m4 n4 sigma' tau' i. rewrite ih. f_equal.
fext=>j/=. by asimpl.
fext=>/=-[]//=j. rewrite eval_vl_ren. symmetry. exact: naturality_vl.
- f_equal;fext=>/=m4 n4 sigma' tau' i. rewrite ih /=. f_equal.
fext=>/=-[]//=j. by asimpl.
fext=>/=j. rewrite eval_vl_ren. symmetry. exact: naturality_vl.
- by rewrite ih.
- by rewrite ihs iht.
- asimpl. by rewrite ihs.
Qed.

(t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3 : nat}
(sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3)
(v : vl m1 n1) :
eval_vl t1 t2 rho theta v.[sigma, tau]%vl =
eval_vl (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) v.
Proof. by case: (eval_vl_tm_inst t1 t2 m1 n1). Qed.

(t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3 : nat}
(sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3)
(s : tm m1 n1) :
eval_tm t1 t2 rho theta s.[sigma, tau]%tm =
eval_tm (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) s.
Proof. by case: (eval_vl_tm_inst t1 t2 m1 n1). Qed.

Lemma inst_vl_comp {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2)
(sigma2 : fin m2 -> ty m3) (tau2 : fin n2 -> vl m3 n3) (v : vl m1 n1) :
v.[sigma1,tau1]%vl.[sigma2,tau2]%vl = v.[sigma1 >> Ty.inst sigma2, tau1 >> inst_vl sigma2 tau2]%vl.
Proof. exact: eval_vl_inst. Qed.

Lemma inst_tm_comp {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2)
(sigma2 : fin m2 -> ty m3) (tau2 : fin n2 -> vl m3 n3) (s : tm m1 n1) :
s.[sigma1,tau1]%tm.[sigma2,tau2]%tm = s.[sigma1 >> Ty.inst sigma2, tau1 >> inst_vl sigma2 tau2]%tm.
Proof. exact: eval_tm_inst. Qed.

Lemma vl_inst_ren {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2) (sigma2 : ren m2 m3) (tau2 : ren n2 n3) (v : vl m1 n1) :
vl_ren sigma2 tau2 v.[sigma1,tau1]%vl = v.[sigma1 >> Ty.ren sigma2, tau1 >> vl_ren sigma2 tau2]%vl.
Proof.
rewrite lift_vl_embed inst_vl_comp. f_equal; fext => i /=; symmetry.
exact: Ty.embed. exact: lift_vl_embed.
Qed.

Lemma tm_inst_ren {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2) (sigma2 : ren m2 m3) (tau2 : ren n2 n3) (s : tm m1 n1) :
tm_ren sigma2 tau2 s.[sigma1,tau1]%tm = s.[sigma1 >> Ty.ren sigma2, tau1 >> vl_ren sigma2 tau2]%tm.
Proof.
rewrite lift_tm_embed inst_tm_comp. f_equal; fext => i /=; symmetry.
exact: Ty.embed. exact: lift_vl_embed.
Qed.

End Defs.

## Exports

Exports the definitions later visible for the user.

Module Exports.
Notation vl := vl.
Notation tm := tm.

Canonical ren_model.
Canonical lift_model.

Coercion base : model >-> traversal.
Coercion model_is_natural : model >-> is_natural.

Arguments var {m n}, m n.

Arguments tvar {Vty Dty Vvl Dvl Dtm} t {m n} i.
Arguments tlam {Vty Dty Vvl Dvl Dtm} t {m n} A F.
Arguments tLam {Vty Dty Vvl Dvl Dtm} t {m n} F.
Arguments ttvl {Vty Dty Vvl Dvl Dtm} t {m n} v.
Arguments tapp {Vty Dty Vvl Dvl Dtm} t {m n} xi a.
Arguments tApp {Vty Dty Vvl Dvl Dtm} t {m n} xi A.

Module FCBV.
Notation traversal := traversal.
Notation Traversal := Traversal.
Notation tvar := tvar.
Notation tlam := tlam.
Notation tLam := tLam.
Notation ttvl := ttvl.
Notation tapp := tapp.
Notation tApp := tApp.

Notation ren_traversal := ren_traversal.
Notation inst_traversal := (lift Ty.ren_traversal ren_traversal).
Notation lift := lift.

Notation is_natural := is_natural.
Notation IsNatural := IsNatural.
Notation nvar := nvar.
Notation nlam := nlam.
Notation nLam := nLam.
Notation ntvl := ntvl.
Notation napp := napp.
Notation nApp := nApp.

Notation model := model.
End FCBV.

Module Vl.
(* Types *)
Notation var := var.
Notation lam := lam.
Notation Lam := Lam.

(* Evaluation *)
Notation eval := eval_vl.

Notation eval_ren := eval_vl_ren.
Notation eval_inst := eval_vl_inst.
Notation naturality := naturality_vl.

Notation embed := lift_vl_embed.

(* Renaming *)
Notation ren := (eval_vl Ty.ren_traversal FCBV.ren_traversal).

Notation ren_id := ren_vl_id.
Notation ren_comp := ren_vl_comp.
Notation ren_inj := ren_vl_inj.

(* Instantiation *)
Notation inst := (eval_vl Ty.inst_traversal FCBV.inst_traversal).

Notation ren_inst := vl_ren_inst.
Notation inst_ren := vl_inst_ren.

Notation inst_id := inst_vl_id.
Notation inst_comp := inst_vl_comp.
End Vl.

Module Tm.
(* Types *)
Notation tvl := tvl.
Notation app := app.
Notation App := App.

(* Evaluation *)
Notation eval := eval_tm.

Notation eval_ren := eval_tm_ren.
Notation eval_inst := eval_tm_inst.
Notation naturality := naturality_tm.

Notation embed := lift_tm_embed.

(* Renaming *)
Notation ren := (eval_tm Ty.ren_traversal FCBV.ren_traversal).

Notation ren_id := ren_tm_id.
Notation ren_comp := ren_tm_comp.
Notation ren_inj := ren_tm_inj.

(* Instantiation *)
Notation inst := (eval_tm Ty.inst_traversal FCBV.inst_traversal).

Notation ren_inst := tm_ren_inst.
Notation inst_ren := tm_inst_ren.

Notation inst_id := inst_tm_id.
Notation inst_comp := inst_tm_comp.
End Tm.

Notation "v ◁ ( xi , zeta )" := (Vl.ren xi zeta v) (at level 50,
format "v ◁ ( xi , zeta )") : vl_inst_scope.

Notation "v ◁ ( xi , zeta )" := (Tm.ren xi zeta v) (at level 50,
format "v ◁ ( xi , zeta )") : tm_inst_scope.

Notation "v .[ sigma , tau ]" := (Vl.inst sigma tau v)
(at level 2, left associativity, format "v .[ sigma , tau ]") : vl_inst_scope.
Notation "s .[ sigma , tau ]" := (Tm.inst sigma tau s)
(at level 2, left associativity, format "s .[ sigma , tau ]") : tm_inst_scope.

Delimit Scope vl_inst_scope with vl.
Delimit Scope tm_inst_scope with tm.
End Exports.

End TmVl.
Export TmVl.Exports.

## Automation

Lemmas needed for the automation for terms and values. The statements are chosen according to the lemmas of Autosubst 2 and repeatedly rewritten. See the LFMTP progress paper for more details.
Lemma vl_ren_idX {m n} : Vl.ren (id : fin m -> fin m) (id : fin n -> fin n) = id.
Proof. fext=> A. exact: Vl.ren_id. Qed.

Lemma tm_ren_idX {m n} : Tm.ren (id : fin m -> fin m) (id : fin n -> fin n) = id.
Proof. fext=> A. exact: Tm.ren_id. Qed.

Lemma vl_ren_compX {m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) :
Vl.ren xi1 zeta1 >> Vl.ren xi2 zeta2 = Vl.ren (xi1 >> xi2) (zeta1 >> zeta2).
Proof. fext=> A /=. exact: Vl.ren_comp. Qed.

Lemma tm_ren_compX {m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) :
Tm.ren xi1 zeta1 >> Tm.ren xi2 zeta2 = Tm.ren (xi1 >> xi2) (zeta1 >> zeta2).
Proof. fext=> A /=. exact: Tm.ren_comp. Qed.

Lemma vl_ren_compR {T m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (h : _ -> T) :
Vl.ren xi1 zeta1 >> (Vl.ren xi2 zeta2 >> h) = Vl.ren (xi1 >> xi2) (zeta1 >> zeta2) >> h.
Proof. fext=> A /=. by rewrite Vl.ren_comp. Qed.

Lemma tm_ren_compR {T m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (h : _ -> T) :
Tm.ren xi1 zeta1 >> (Tm.ren xi2 zeta2 >> h) = Tm.ren (xi1 >> xi2) (zeta1 >> zeta2) >> h.
Proof. fext=> A /=. by rewrite Tm.ren_comp. Qed.

Lemma vl_ren_instX {m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> vl m3 n3) :
Vl.ren xi zeta >> Vl.inst sigma tau = Vl.inst (xi >> sigma) (zeta >> tau).
Proof. fext=> A /=. exact: Vl.ren_inst. Qed.

Lemma tm_ren_instX {m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> vl m3 n3) :
Tm.ren xi zeta >> Tm.inst sigma tau = Tm.inst (xi >> sigma) (zeta >> tau).
Proof. fext=> A /=. exact: Tm.ren_inst. Qed.

Lemma vl_ren_instR {T m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> vl m3 n3) (h : _ -> T) :
Vl.ren xi zeta >> (Vl.inst sigma tau >> h) = Vl.inst (xi >> sigma) (zeta >> tau) >> h.
Proof. fext=> A /=. by rewrite Vl.ren_inst. Qed.

Lemma tm_ren_instR {T m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> vl m3 n3) (h : _ -> T) :
Tm.ren xi zeta >> (Tm.inst sigma tau >> h) = Tm.inst (xi >> sigma) (zeta >> tau) >> h.
Proof. fext=> A /=. by rewrite Tm.ren_inst. Qed.

Lemma vl_inst_renX {m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> vl m2 n2) (zeta : ren n2 n3) :
Vl.inst sigma tau >> Vl.ren xi zeta = Vl.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta).
Proof. fext=> A /=. exact: Vl.inst_ren. Qed.

Lemma tm_inst_renX {m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> vl m2 n2) (zeta : ren n2 n3) :
Tm.inst sigma tau >> Tm.ren xi zeta = Tm.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta).
Proof. fext=> A /=. exact: Tm.inst_ren. Qed.

Lemma vl_inst_renR {T m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> vl m2 n2) (zeta : ren n2 n3) (h : _ -> T) :
Vl.inst sigma tau >> (Vl.ren xi zeta >> h) = Vl.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta) >> h.
Proof. fext=> A /=. by rewrite Vl.inst_ren. Qed.

Lemma tm_inst_renR {T m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> vl m2 n2) (zeta : ren n2 n3) (h : _ -> T) :
Tm.inst sigma tau >> (Tm.ren xi zeta >> h) = Tm.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta) >> h.
Proof. fext=> A /=. by rewrite Tm.inst_ren. Qed.

Lemma vl_id_instX {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2) : Vl.var >> Vl.inst sigma tau = tau.
Proof. by []. Qed.

Lemma vl_inst_idX {m n} : Vl.inst (@Ty.var m) (@Vl.var m n) = id.
Proof. fext=> A. exact: Vl.inst_id. Qed.

Lemma tm_inst_idX {m n} : Tm.inst (@Ty.var m) (@Vl.var m n) = id.
Proof. fext=> A. exact: Tm.inst_id. Qed.

Lemma vl_inst_idR {T m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2) (h : _ -> T) : Vl.var >> (Vl.inst sigma tau >> h) = (tau >> h).
Proof. by []. Qed.

Lemma vl_inst_compX {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> vl m2 n2) (tau2 : fin n2 -> vl m3 n3) :
Vl.inst sigma1 tau1 >> Vl.inst sigma2 tau2 = Vl.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Vl.inst sigma2 tau2).
Proof. fext=> A /=. exact: Vl.inst_comp. Qed.

Lemma tm_inst_compX {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> vl m2 n2) (tau2 : fin n2 -> vl m3 n3) :
Tm.inst sigma1 tau1 >> Tm.inst sigma2 tau2 = Tm.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Vl.inst sigma2 tau2).
Proof. fext=> A /=. exact: Tm.inst_comp. Qed.

Lemma vl_inst_compR {T m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> vl m2 n2) (tau2 : fin n2 -> vl m3 n3) (h : _ -> T) :
Vl.inst sigma1 tau1 >> (Vl.inst sigma2 tau2 >> h) = Vl.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Vl.inst sigma2 tau2) >> h.
Proof. fext=> A /=. by rewrite Vl.inst_comp. Qed.

Lemma tm_inst_compR {T m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> vl m2 n2) (tau2 : fin n2 -> vl m3 n3) (h : _ -> T) :
Tm.inst sigma1 tau1 >> (Tm.inst sigma2 tau2 >> h) = Tm.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Vl.inst sigma2 tau2) >> h.
Proof. fext=> A /=. by rewrite Tm.inst_comp. Qed.

Ltac vt_simpl :=
rewrite ?vl_ren_idX ?vl_ren_compX ?vl_ren_compR
?tm_ren_idX ?tm_ren_compX ?tm_ren_compR
?vl_inst_renX ?vl_inst_renR
?tm_inst_renX ?tm_inst_renR
?vl_ren_instX ?vl_ren_instR
?tm_ren_instX ?tm_ren_instR
?vl_id_instX ?vl_inst_idX ?vl_inst_idR
?tm_inst_idX
?vl_inst_compX ?vl_inst_compR
?tm_inst_compX ?tm_inst_compR
?Vl.ren_id ?Vl.ren_comp ?Vl.ren_inst ?Vl.inst_ren ?Vl.inst_id ?Vl.inst_comp
?Tm.ren_id ?Tm.ren_comp ?Tm.ren_inst ?Tm.inst_ren ?Tm.inst_id ?Tm.inst_comp
?Vl.eval_ren ?Vl.eval_inst ?Vl.naturality
?Tm.eval_ren ?Tm.eval_inst ?Tm.naturality
?TmVl.th2_vlE ?TmVl.th2_tmE.