# Strong Normalization of System F

## Logical Relation

Definition active {m n} (s : tm m n) : bool :=
match s with
| lam _ | tlam _ => true
| _ => false
end.

Definition tpred := forall m n, tm m n -> Prop.

Definition M (P : tpred) : tpred :=
fun m1 n1 s => forall m2 n2 (f : ren m1 m2) (g : ren n1 n2), P m2 n2 (rename f g s).

Inductive R (P : tpred) m n (s : tm m n) : Prop :=
| RI :
(active s -> M P s) ->
(forall t, step s t -> R P t) ->
R P s.

Definition D : model tpred tpred :=
{| Var := id
; Arr := fun (U V : tpred) (m n : nat) (s : tm m n) =>
if s isn't lam b then False else
forall (u : tm m n), R U u -> R V (inst (@tvar m) (u .: @var m n) b)
; All := fun F m n v =>
if v isn't tlam b then False else
forall P A, R (F P) (inst (A .: @tvar m) (@var m n) b)
|}.

Notation V A ρ := (eval D ρ A).
Notation K A ρ := (M (V A ρ)).
Notation E A ρ := (R (V A ρ)).

## Reducibility Candidates

Lemma R_sn {m n} (P : tpred) (s : tm m n) :
R P s -> sn step s.
Proof. elim; by eauto using @sn. Qed.

Lemma R_step {m n} (P : tpred) (s t : tm m n) :
step s t -> R P s -> R P t.
Proof. move=> st [_]. by apply. Qed.

Lemma R_var {m n} (P : tpred) (i : fin n) :
R P (var m i).
Proof. apply: RI. by []. move=> t st. by inv st. Qed.

Lemma R_rename m1 m2 n1 n2 (f : ren m1 m2) (g : ren n1 n2) (P : tpred) (s : tm m1 n1) :
R P s -> R P (rename f g s).
Proof.
elim=> /={s}s ns _ ih. constructor.
- move=> hns m3 n3 f' g'. rewrite ren_comp. apply: ns. by destruct s.
- move=> t. rewrite ren_inst => /step_weak[s' st <-{t}].
rewrite -ren_inst. exact: ih.
Qed.

## Logical Relation

Lemma K_var c m1 n1 (i : fin c) (ρ : fin c -> tpred) (s : tm m1 n1) :
K (tvar i) ρ s = forall m2 n2 (f : ren m1 m2) (g : ren n1 n2), ρ i m2 n2 (rename f g s).
Proof. by []. Qed.

Lemma K_arr c m1 n1 (A B : ty c) (ρ : fin c -> tpred) (b : tm m1 n1.+1) :
K (arr A B) ρ (lam b) =
forall m2 n2 (f : ren m1 m2) (g : ren n1 n2) (u : tm m2 n2),
E A ρ u -> E B ρ (inst (f >> @tvar m2) (u .: g >> @var m2 n2) b).
Proof.
rewrite/M/=; fext=> m2 n2 f g u hu. rewrite ren_inst_comp. by fsimpl.
Qed.

Lemma K_all c m1 n (A : ty c.+1) (ρ : fin c -> tpred) (b : tm m1.+1 n) :
K (all A) ρ (tlam b) =
forall m2 (f : ren m1 m2) P B,
E A (P .: ρ) (inst (B .: f >> @tvar m2) (@var m2 n) b).
Proof.
rewrite/M/=. apply: pext=> H.
- move=> m2 f P B. move: (H m2 n f id P B). rewrite ren_inst_comp. by fsimpl.
- move=> m2 n2 f g P B.
move: (H m2 f P B). rewrite ren_inst_comp. unfold up; fsimpl=>/=.
move=> HH. move: (R_rename id g HH). rewrite inst_ren_comp.
fsimpl. rewrite ty_ren_id. exact.
Qed.

Lemma V_weaken c m n (A : ty c) (ρ : fin c -> tpred) (P : tpred) (s : tm m n) :
V (tyrename shift A) (P .: ρ) m n s = V A ρ m n s.
Proof. by rewrite eval_weaken. Qed.

Lemma K_weaken c m n (A : ty c) (ρ : fin c -> tpred) (P : tpred) (s : tm m n) :
K (tyrename shift A) (P .: ρ) s = K A ρ s.
Proof. fext=>*; by rewrite V_weaken. Qed.

Lemma E_weaken c m n (A : ty c) (ρ : fin c -> tpred) (P : tpred) (s : tm m n) :
E (tyrename shift A) (P .: ρ) s = E A ρ s.
Proof. f_equal. fext=> *; by rewrite V_weaken. Qed.

Lemma V_beta c m n (A : ty c.+1) (B : ty c) (ρ : fin c -> tpred) (s : tm m n) :
V (tyinst (B .: @tvar c) A) ρ m n s = V A (V B ρ .: ρ) m n s.
Proof. by rewrite eval_beta. Qed.

Lemma E_beta c m n (A : ty c.+1) (B : ty c) (ρ : fin c -> tpred) (s : tm m n) :
E (tyinst (B .: @tvar c) A) ρ s = E A (V B ρ .: ρ) s.
Proof. by rewrite eval_beta. Qed.

## Logical relation on contexts

Definition C {c n} (Γ : fin n -> ty c) (ρ : fin c -> tpred) : forall {m k}, subst m n k -> Prop :=
fun m k f => forall i, E (Γ i) ρ (f i).

Lemma C_scons c m n k A (Γ : fin n -> ty c) (ρ : fin c -> tpred) (f : subst m n k) (s : tm m k) :
E A ρ s -> C Γ ρ f -> C (A .: Γ) ρ (s .: f).
Proof. move=> ls cf; hnf=>/=; by case. Qed.

Lemma C_rename c m1 m2 n1 n2 n3 (Γ : fin n1 -> ty c) (ρ : fin c -> tpred) (f : subst m1 n1 n2) (g : ren m1 m2) (h : ren n2 n3) :
C Γ ρ f -> C Γ ρ (f >> rename g h).
Proof.
move=> cf i /=. apply: R_rename. exact: cf.
Qed.

Lemma C_up c m n k (A : ty c) (Γ : fin n -> ty c) (ρ : fin c -> tpred) (f : subst m n k) :
C Γ ρ f -> C (A .: Γ) ρ (upi f).
Proof.
move=> cf. apply: C_scons. exact: R_var. exact: C_rename.
Qed.

## Fundamental theorem & Strong Normalisation

Lemma E2_ind {c1 c2 m1 m2 n1 n2} (A : ty c1) (B : ty c2) (ρ1 : fin c1 -> tpred) (ρ2 : fin c2 -> tpred)
(P : tm m1 n1 -> tm m2 n2 -> Prop) :
(forall (s : tm m1 n1) (t : tm m2 n2),
E A ρ1 s ->
E B ρ2 t ->
(forall s', step s s' -> P s' t) ->
(forall t', step t t' -> P s t') ->
P s t) ->
forall (s : tm m1 n1) (t : tm m2 n2),
E A ρ1 s -> E B ρ2 t -> P s t.
Proof.
move=> h s t ls. elim: ls t => {s} s ns ls ihs t.
elim=> {t} t nt lt iht. apply: h. constructor. exact: ns. exact: ls.
constructor. exact: nt. exact: lt.
move=> u /ihs. apply. constructor. exact: nt. exact: lt.
move=> u. exact: iht.
Qed.

Lemma E_app c m n A B (s t : tm m n) (ρ : fin c -> tpred) :
E (arr A B) ρ s -> E A ρ t -> E B ρ (app s t).
Proof.
move: s t. apply: E2_ind => s t ns nt ihs iht. constructor. by [].
move=> u st. inv st.
- case: ns. rewrite K_arr => /(_ erefl)/=H _.
exact: (H m n id id t nt).
- exact: ihs.
- exact: iht.
Qed.

Lemma E_lam c m1 n1 (A B : ty c) (ρ : fin c -> tpred) (s : tm m1 n1.+1) :
sn step s ->
(forall m2 n2 (f : ren m1 m2) (g : ren n1 n2) (a : tm m2 n2),
E A ρ a -> E B ρ (inst (f >> @tvar _) (a .: g >> @var _ _) s)) ->
E (arr A B) ρ (lam s).
Proof.
elim=>{s} s _ ih h. constructor.
- move=> _. rewrite K_arr. exact: h.
- move=> t st. inv st. apply: ih. exact: H0. move=> m2 n2 f g a la.
apply: R_step (h _ _ f g _ la). exact: step_inst.
Qed.

Lemma E_tapp c m n (A : ty c.+1) (B : ty c) (ρ : fin c -> tpred) (s : tm m n) (C : ty m) :
E (all A) ρ s -> E (tyinst (B .: @tvar _) A) ρ (tapp s C).
Proof.
elim=> {s} s h1 ih h2. rewrite E_beta. constructor => [//|t st]. inv st.
specialize (h1 erefl). rewrite K_all in h1. exact: h1.
Qed.

Lemma E_tlam c m1 n (A : ty c.+1) (ρ : fin c -> tpred) (s : tm m1.+1 n) :
sn step s ->
(forall m2 (f : ren m1 m2) P B, E A (P .: ρ) (inst (B .: f >> @tvar _) (@var _ _) s)) ->
E (all A) ρ (tlam s).
Proof.
elim=> {s} s _ ih h. constructor.
- rewrite K_all => _. exact: h.
- move=> t st. inv st. apply: ih => [//|m2 f P B]. move: (h m2 f P B).
apply: R_step. exact: step_inst.
Qed.

Theorem fundamental m1 n1 Γ A (s : tm m1 n1) :
has_type Γ s A ->
forall m2 n2 (σ : tysubst m1 m2) (f : subst m2 n1 n2) (ρ : fin m1 -> tpred),
C Γ ρ f -> E A ρ (inst σ f s).
Proof.
elim=> {m1 n1 Γ s A} [m1 n1 Γ i|m1 n1 Γ s t A B _ ihA _ ihB|m1 n1 Γ s A B _ ih|m1 n1 Γ s A B _ ih|m1 n1 Γ s A _ ih] m2 n2 σ τ ρ ct.
- exact: ct.
- cbn. apply: E_app. exact: ihA. exact: ihB.
- cbn. apply: E_lam. apply: R_sn. apply: ih. exact: C_up.
move=> m3 n3 f g a la.
have->: inst (f >> tvar (n:=m3)) (a .: g >> var m3 (n:=n3)) (inst σ (upi τ) s)
= inst>> tyrename f) (a .: τ >> rename f g) s.
{ rewrite inst_comp. unfold upi; fsimpl=> /=. f_equal.
fext=> t /=. by rewrite ty_ren_inst.
fext=> /=; case=> //=i. rewrite ren_inst. fsimpl=>/=.
rewrite inst_comp. by rewrite ren_inst. }
apply: ih. apply: C_scons. exact: la. exact: C_rename.
- cbn. apply: E_tapp. exact: ih.
- cbn. apply: E_tlam.
+ case/(_ _)/Wrap: (ih _ _ (tup σ) (τ >> rename shift id) ((fun _ _ _ => False) .: ρ)).
move=> i /=. rewrite E_weaken. apply: R_rename. exact: ct.
exact: R_sn.
+ move=> m3 f P B. rewrite inst_comp. apply: ih.
move=> i /=. rewrite ren_inst_comp. fsimpl. rewrite E_weaken.
rewrite -ren_inst. apply: R_rename. exact: ct.
Qed.

Theorem strong_normalization m n Γ A (s : tm m n) : has_type Γ s A -> sn step s.
Proof.
move=> tp. move: (@fundamental m n Γ A s tp m n (@tvar m) (@var m n) (fun _ _ _ _ => False)). case/(_ _)/Wrap.
- move=> i. exact: R_var.
- rewrite inst_ids. exact: R_sn.
Qed.