# Section 10 Case Study : Strong Normalisation of System F

This file contains the Coq code corresponding to chapter 10, showing strong normalisation of System F. It is based on the previous framework.
From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Base.ARS.
Set Implicit Arguments.
Unset Strict Implicit.

The tactic repeatedly rewrites with the lemmas established for traversals and models for the types and terms of System FCBV.
Local Ltac asimpl :=
repeat progress (cbn; fsimpl; gsimpl; ty_simpl; tm_simpl).

## One-Step Reduction

Inductive step {m n} : tm m n -> tm m n -> Prop :=
| step_beta (A : ty m) (s : tm m n.+1) (t : tm m n) :
step (Tm.app (Tm.lam A s) t) s.[Ty.var, t .: Tm.var]%tm
| step_Beta (A : ty m) (s : tm m.+1 n) :
step (Tm.App (Tm.Lam s) A) s.[A .: Ty.var, Tm.var]%tm
| step_appL s1 s2 t :
step s1 s2 -> step (Tm.app s1 t) (Tm.app s2 t)
| step_appR s t1 t2 :
step t1 t2 -> step (Tm.app s t1) (Tm.app s t2)
| step_abs A s1 s2 :
@step m n.+1 s1 s2 -> step (Tm.lam A s1) (Tm.lam A s2)
| step_tapp A s1 s2 :
step s1 s2 -> step (Tm.App s1 A) (Tm.App s2 A)
| step_tabs s1 s2 :
@step m.+1 n s1 s2 -> step (Tm.Lam s1) (Tm.Lam s2).

Lemma step_ebeta {m n} A s t (u : tm m n) :
u = s.[Ty.var, t .: Tm.var]%tm -> step (Tm.app (Tm.lam A s) t) u.
Proof. move->. exact: step_beta. Qed.

Lemma step_eBeta {m n} A s (t : tm m n) :
t = s.[A .: Ty.var, Tm.var]%tm -> step (Tm.App (Tm.Lam s) A) t.
Proof. move->. exact: step_Beta. Qed.

One-step reduction is compatible with substitution.
Lemma step_inst {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) s t :
step s t -> step s.[sigma,tau]%tm t.[sigma,tau]%tm.
Proof.
move=> st. elim: st m2 n2 tau sigma => {m1 n1 s t}; asimpl; eauto using @step.
- move=> m1 n1 A s t m2 n2 tau sigma. apply: step_ebeta. by asimpl.
- move=> m1 n1 A s m2 n2 tau sigma. apply: step_eBeta. by asimpl.
Qed.

## Many-Step Reduction

Definition red {m n} := star (@step m n).

Definition sred {m n k} (sigma tau : fin m -> tm n k) :=
forall x, @red n k (sigma x) (tau x).

Congruence and compatibility of many-step reduction. This is necessary to show that beta-reduction entails the correct behaviour (Lemma red_beta). The proofs are standard.
Lemma red_app {m n} (s1 s2 t1 t2 : tm m n) :
red s1 s2 -> red t1 t2 -> red (Tm.app s1 t1) (Tm.app s2 t2).
Proof.
move=> A B. apply: (star_trans (Tm.app s2 t1)).
- apply: (star_hom (@Tm.app m n^~ t1)) A => x y. exact: step_appL.
- apply: star_hom B => x y. exact: step_appR.
Qed.

Lemma red_abs {m n} A (s1 s2 : tm m n.+1) :
red s1 s2 -> red (Tm.lam A s1) (Tm.lam A s2).
Proof. apply: star_hom => x y. exact: step_abs. Qed.

Lemma red_tapp {m n} A (s1 s2 : tm m n) :
red s1 s2 -> red (Tm.App s1 A) (Tm.App s2 A).
Proof. apply: (star_hom (@Tm.App m n^~A)) => x y. exact: step_tapp. Qed.

Lemma red_tabs {m n} (s1 s2 : tm m.+1 n) :
red s1 s2 -> red (Tm.Lam s1) (Tm.Lam s2).
Proof. apply: star_hom => x y. exact: step_tabs. Qed.

Lemma red_inst {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) s t :
red s t -> red s.[sigma,tau]%tm t.[sigma,tau]%tm.
Proof. apply: star_hom => x y. exact: step_inst. Qed.

Hint Resolve red_app red_abs red_tapp red_tabs : red_congr.

Lemma red_compat {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau1 tau2 : fin n1 -> tm m2 n2) s :
sred tau1 tau2 -> red s.[sigma,tau1]%tm s.[sigma,tau2]%tm.
Proof.
elim: s m2 n2 sigma tau1 tau2; intros; asimpl; eauto with red_congr.
- apply: red_abs. apply: H. hnf=>/=-[i|]//=. asimpl. rewrite Tm.embed [(_ (_,_))%tm]Tm.embed.
apply: red_inst. exact: H0.
- apply: red_tabs. apply: H. hnf=>/=i. asimpl. rewrite Tm.embed [(_ (_,_))%tm]Tm.embed.
apply: red_inst. exact: H0.
- exact: starR.
Qed.

Lemma red_beta {m n} s (t1 t2 : tm m n) :
step t1 t2 -> red s.[Ty.var, t1 .: Tm.var]%tm s.[Ty.var, t2 .: Tm.var]%tm.
Proof. move=> h. apply: red_compat => /=-[i|]/=; [exact: starR|exact: star1]. Qed.

## Syntactic typing

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

Inductive has_type {m n} (Gamma : ctx m n) : tm m n -> ty m -> Prop :=
| ty_var (x : fin n) :
has_type Gamma (Tm.var x) (Gamma x)
| ty_abs (A B : ty m) (s : tm m n.+1) :
@has_type m n.+1 (A .: Gamma) s B ->
has_type Gamma (Tm.lam A s) (Ty.arr A B)
| ty_app (A B : ty m) (s t : tm m n) :
has_type Gamma s (Ty.arr A B) ->
has_type Gamma t A ->
has_type Gamma (Tm.app s t) B
| ty_tabs (A : ty m.+1) (s : tm m.+1 n) :
@has_type m.+1 n (Gamma >> Ty.ren shift) s A ->
has_type Gamma (Tm.Lam s) (Ty.all A)
| ty_tapp (A : ty m.+1) (B : ty m) (s : tm m n) :
has_type Gamma s (Ty.all A) ->
has_type Gamma (Tm.App s B) A.[B .: Ty.var]%ty.

## Strong Normalization

Definition and proof of closedness / compatibility with instantiation.
Notation sn := (sn (@step _ _)).

Lemma sn_closed {m n} (t s : tm m n) :
sn (Tm.app s t) -> sn s.
Proof. apply: (sn_preimage (h := @Tm.app m n^~t)) => x y. exact: step_appL. Qed.

Lemma sn_tclosed {m n} A (s : tm m n) : sn (Tm.App s A) -> sn s.
Proof. apply: (sn_preimage (h := @Tm.App m n^~A)) => x y. exact: step_tapp. Qed.

Lemma sn_inst {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) s :
sn s.[sigma,tau]%tm -> sn s.
Proof. apply: sn_preimage. exact: step_inst. Qed.

## The Reducibility Candidates/Logical Predicate

Definition cand m n := tm m n -> Prop.

Neutral (Definition 10.1)
Definition neutral {m n} (s : tm m n) : bool :=
match s with
| Tm.lam _ _ | Tm.Lam _ => false
| _ => true
end.

Reducibility candidates (Definition 10.2)
Record reducible {m n} (P : cand m n) : Prop := {
p_sn : forall s, P s -> sn s;
p_cl : forall s t, P s -> step s t -> P t;
p_nc : forall s, neutral s -> (forall t, step s t -> P t) -> P s
}.

Definition admissible {m n k} (rho : fin m -> cand n k) :=
forall i, reducible (rho i).

S-traversal (Definition 10.3) and S evaluation.
Definition S {m n} : Ty.smodel (cand m n) (cand m n).
Proof.
apply: Ty.SModel.
- exact id.
- intros P Q f. refine (forall s, P s -> Q (Tm.app f s)).
- intros F f. refine (forall P B, reducible P -> F P (Tm.App f B)).
Defined.
Notation E := (Ty.seval S).

Lemma reducible_sn {m n} : reducible (sn : tm m n -> Prop).
Proof. constructor; eauto using ARS.sn. by move=> s t [sigma] /sigma. Qed.
Hint Resolve @reducible_sn.

Lemma reducible_const {m n} (P : cand m n) : reducible P -> P (Tm.const m n).
Proof. move/p_nc. apply=> // t st. by inversion st. Qed.

Lemma ad_cons {m n k} (P : cand n k) (rho : fin m -> cand n k) :
Proof. by move=> H1 H2 [i|] //=. Qed.

Lemma 10.4 and consequences.
Lemma L_reducible {m n k} (A : ty m) (rho : fin m -> cand n k) :
admissible rho -> reducible (E rho A).
Proof with eauto using @step.
elim: A n k rho => /={m}[m i|m A ih1 B ih2|m A ih] n k rho safe.
- exact: safe.
- constructor.
+ move=> s. asimpl=> h. apply (@sn_closed n k (Tm.const n k)).
apply: (p_sn (P := E rho B))... apply: h. apply: reducible_const...
+ move=> s t h st u la. apply: (p_cl _ (s := Tm.app s u))...
+ move=> s ns. asimpl=> h t la. have snt := p_sn (ih1 _ _ _ safe) la.
elim: snt la => {t} t _ ih3 la. apply: p_nc...
move=> v st; inversion st; clear st; subst=>//...
apply: ih3 => //. exact: (p_cl (ih1 _ _ _ safe)) la _.
- cbn. constructor.
+ move=> s /(_ sn (Ty.all (Ty.var bound)) reducible_sn)/p_sn/sn_tclosed; apply.
+ move=> s t h st P B rep. apply: p_cl (step_tapp B st)...
+ move=> s ns h P B rep. apply ih... exact: ad_cons.
move=> t st. inversion st; clear st; subst=> //. exact: h.
Qed.

Corollary L_sn {m n k} A (rho : fin m -> cand n k) s :
admissible rho -> E rho A s -> sn s.
Proof. move/L_reducible/p_sn. apply. Qed.

Corollary L_cl {m n k} T (rho : fin m -> cand n k) s t :
admissible rho -> E rho T s -> step s t -> E rho T t.
Proof. move/L_reducible/p_cl. apply. Qed.

Corollary L_nc {m n k} T (rho : fin m -> cand n k) s :
admissible rho -> neutral s -> (forall t, step s t -> E rho T t) -> E rho T s.
Proof. move/L_reducible/p_nc. apply. Qed.

Corollary L_var {m n k} T (rho : fin m -> cand n k) x :
admissible rho -> E rho T (Tm.var x).
Proof. move/L_nc. apply=> // t st. by inversion st. Qed.

Corollary L_const {m n k} T (rho : fin m -> cand n k) :
admissible rho -> E rho T (Tm.const n k).
Proof. move/L_nc. apply=> // t st. by inversion st. Qed.

Corollary L_cl_star {m n k} T (rho : fin m -> cand n k) s t :
admissible rho -> E rho T s -> red s t -> E rho T t.
Proof. move=> /L_cl cl H st. elim: st H; eauto. Qed.

## Semantic typing (Definition 10.5)

Definition tm_sty {m n} (Gamma : fin n -> ty m) (s : tm m n) (A : ty m) : Prop :=
forall k1 k2 (rho : fin m -> cand k1 k2) theta sigma,
admissible rho -> (forall i, E rho (Gamma i) (sigma i)) -> E rho A s.[theta,sigma]%tm.

## The fundamental theorem

Closure under beta expansion and Beta expansion. Special cases for the fundamental theorem.

Ltac inv H := inversion H; clear H; subst.

Lemma beta_expansion {m n k} A B (rho : fin m -> cand n k) s t :
admissible rho -> sn t -> E rho A s.[Ty.var, t .: Tm.var]%tm ->
E rho A (Tm.app (Tm.lam B s) t).
Proof with eauto.
elim: sns t snt h => {s} s sns ih1 t. elim=> {t} t snt ih2 h.
apply: L_nc => // u st. inv st => //.
- inv H2. apply: ih1 => //. apply: L_cl ad h _. exact: step_inst.
- apply: ih2 => //. apply: L_cl_star ad h _. exact: red_beta.
Qed.

Lemma inst_expansion {m n k} A B (rho : fin m -> cand n k) s :
admissible rho -> E rho A s.[B .: Ty.var, Tm.var]%tm ->
E rho A (Tm.App (Tm.Lam s) B).
Proof.
move=> ad h. have sns := sn_inst (L_sn ad h). elim: sns h.
move=> {s} s _ ih h. apply: L_nc => // t st. inv st => //.
inv H2 => //. apply: ih => //. apply: L_cl ad h _. exact: step_inst.
Qed.

The fundamental theorem (Theorem 10.6).
Syntactic typing implies semantic typing.
Theorem soundness {m n} (Gamma : fin n -> ty m) s A :
has_type Gamma s A -> tm_sty Gamma s A.
Proof with eauto using L_sn, ad_cons.
elim=> {Gamma s A m n}[m n|m n Gamma A B s _ ih|m n Gamma A B s t _ ih1 _ ih2|m n Gamma A s _ ih|m n Gamma A B s _ /=ih]
k1 k2 rho theta sigma ad el; asimpl...
- move=> t h. apply: beta_expansion... asimpl. apply: ih... by case.
- move: ih1. asimpl. apply=>//. exact: ih2.
- move=> P B h. apply: inst_expansion... asimpl. apply: ih... move=> x.
asimpl. exact: el.
- apply: ih... apply: L_reducible...
Qed.

## Strong normalisation

Lemma rho_id {m n k} : admissible (fun _ : fin m => sn : tm n k -> Prop).
Proof. move=> x /=. exact: reducible_sn. Qed.

Corollary type_E {m n} Gamma (s : tm m n) A (rho : fin m -> cand m n) :
has_type Gamma s A -> admissible rho -> E rho A s.
Proof.
move=> ty ad. move: (@soundness _ _ Gamma s A ty _ _ rho) => h.
specialize (h Ty.var Tm.var ad). move: h. asimpl. apply=> x /=. exact: L_var.
Qed.

Corollary 10.7
Corollary strong_normalisation {m n} E (s : tm m n) A :
has_type E s A -> sn s.
Proof. move=>/type_E/(_ rho_id)/L_sn. apply. exact: rho_id. Qed.