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.

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

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.

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).

Notation V := (Ty.seval W).
Notation E rho A s := (L (V rho A) s).

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.

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.

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.

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.