# Section 9 Case Study : Weak Normalisation of System FCBV

This file contains the Coq code corresponding to chapter 9, showing weak normalisation of System FCBV. It is based on the previous framework.
From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Framework.graded Framework.sysf_types Framework.sysf_terms.
Set Implicit Arguments.
Unset Strict Implicit.

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

## Big-step evaluation relation for FCBV

As represented in Figure 3.
Inductive eval {m n : nat} : tm m n -> vl m n -> Prop :=
| eval_val (v : vl m n) : eval (Tm.tvl v) v
| eval_app (s t : tm m n) (A : ty m) (b : tm m n.+1) (u v : vl m n) :
eval s (Vl.lam A b) -> eval t u -> eval b.[@Ty.var _, u .: @Vl.var _ _]%tm v ->
eval (Tm.app s t) v
| eval_App (s : tm m n) (A : ty m) (b : tm m.+1 n) (v : vl m n) :
eval s (Vl.Lam b) -> eval b.[A .: @Ty.var _, @Vl.var _ _]%tm v ->
eval (Tm.App s A) v.

Notation L P s := (exists2 v, eval s v & P v).
Notation cvl := (vl 0 0).
Definition cvls := cvl -> Prop.

## Simple traversal for weak normalisation (Definition 9.1)

Types are interpreted by sets of closed values, where a set is represented as predicate.
Definition W : Ty.smodel cvls cvls := Ty.SModel
(* Variables *)
id
(* Function types *)
(fun P Q v =>
if v is Vl.lam _ b then forall a, P a -> L Q b.[@Ty.var _, a .: @Vl.var _ _]%tm else False)
(* Forall *)
(fun F v =>
if v is Vl.Lam b then forall P A, L (F P) b.[A .: @Ty.var _, @Vl.var _ _]%tm else False).

W evaluation and its extension to sets of closed terms.
Notation V := (Ty.seval W).
Notation E rho A s := (L (V rho A) s).

## Typing for FCBV

The type tm_ty Gamma s A states that s has type A in context Gamma.
As represented in Figure 3.
Unset Elimination Schemes.
Inductive tm_ty {m n} (Gamma : fin n -> ty m) : tm m n -> ty m -> Prop :=
| tm_ty_vl (v : vl m n) (A : ty m) :
vl_ty Gamma v A -> tm_ty Gamma (Tm.tvl v) A
| tm_ty_app (s t : tm m n) (A B : ty m) :
tm_ty Gamma s (Ty.arr A B) -> tm_ty Gamma t A -> tm_ty Gamma (Tm.app s t) B
| tm_ty_App (s : tm m n) (A : ty m) (B : ty m.+1) :
tm_ty Gamma s (Ty.all B) -> tm_ty Gamma (Tm.App s A) B.[A .: @Ty.var _]%ty
with vl_ty {m n} (Gamma : fin n -> ty m) : vl m n -> ty m -> Prop :=
| vl_ty_var (i : fin n) :
vl_ty Gamma (Vl.var i) (Gamma i)
| vl_ty_lam (A B : ty m) (b : tm m n.+1) :
tm_ty (n := n.+1) (A .: Gamma) b B -> vl_ty Gamma (Vl.lam A b) (Ty.arr A B)
| vl_ty_Lam (b : tm m.+1 n) (A : ty m.+1) :
tm_ty (m := m.+1) (Gamma >> Ty.ren shift) b A -> vl_ty Gamma (Vl.Lam b) (Ty.all A).
Set Elimination Schemes.

Scheme tm_ty_ind := Minimality for tm_ty Sort Prop
with vl_ty_ind := Minimality for vl_ty Sort Prop.
Combined Scheme vt_ty_ind from tm_ty_ind, vl_ty_ind.

## Semantic value and term typing

The type tm_sty Gamma s A states that s has semantically type A in context Gamma, the type vl_sty Gamma v A states that v has semantically type A in context Gamma. According to Definition 9.3.
Definition Vs {m n} (rho : fin m -> cvls) (Gamma : fin n -> ty m) (sigma : fin n -> cvl) : Prop :=
forall i, V rho (Gamma i) (sigma i).

Definition tm_sty {m n} (Gamma : fin n -> ty m) (s : tm m n) (A : ty m) : Prop :=
forall (rho : fin m -> cvls) (sigma : fin m -> ty 0) (tau : fin n -> cvl),
Vs rho Gamma tau -> E rho A s.[sigma,tau]%tm.

Definition vl_sty {m n} (Gamma : fin n -> ty m) (v : vl m n) (A : ty m) : Prop :=
forall (rho : fin m -> cvls) (sigma : fin m -> ty 0) (tau : fin n -> cvl),
Vs rho Gamma tau -> V rho A v.[sigma,tau]%vl.

## Fundamental theorem (Theorem 9.4)

Syntactic typing implies semantic typing.
Theorem fundamental_theorem :
forall (m n : nat) (Gamma : fin n -> ty m),
(forall (s : tm m n) (A : ty m), tm_ty Gamma s A -> tm_sty Gamma s A) /\
(forall (v : vl m n) (A : ty m), vl_ty Gamma v A -> vl_sty Gamma v A).
Proof.
apply vt_ty_ind => [m n Gamma v A _ ih|m n Gamma s t A B _ ih1 _ ih2|m n Gamma s A B _ ih|m n Gamma i|m n Gamma A B b _ ih|m n Gamma b A _ ih] rho sigma tau ctx.
- asimpl. exists v.[sigma,tau]%vl. exact: eval_val. exact: ih ctx.
- case: (ih1 rho sigma tau ctx) => {ih1} -[]//=T b ev1 ih1.
case: (ih2 rho sigma tau ctx) => {ih2} u ev2 ih2.
hnf in ih1. case: (ih1 u ih2) => v ev3 ih.
exists v. exact: eval_app ev1 ev2 ev3. exact: ih.
- case: (ih rho sigma tau ctx) => {ih} -[]//=b ev1 ih. asimpl.
hnf in ih. case: (ih (V rho A) A.[sigma]%ty) => {ih} v ev2 ih.
exists v. exact: eval_App ev1 ev2. exact: ih.
- exact: ctx.
- move=> /= u ih2. asimpl. apply: ih. by case.
- move=> /= P B. asimpl. apply: ih => /= i. asimpl. exact: ctx.
Qed.

## Weak Normalisation

Corollary 9.5
Corollary weak_normalisation (s : tm 0 0) (A : ty 0) :
tm_ty null s A -> exists v, eval s v.
Proof.
case: (@fundamental_theorem 0 0 null) => H _ /H
/(_ (fun _ _ => False) (@Ty.var _) (@Vl.var _ _)).
case/(_ _)/Wrap => //. asimpl. case=> v. by exists v.
Qed.