Require Import base data.fintype f.types f.fcbvsyntax f.fcbvreduction.

Notation cvl := (vl 0 0).
Notation ctm := (tm 0 0).

Definition L (P : cvl -> Prop) (s : ctm) : Prop :=
  exists2 v, red s v & P v.

Definition D : model (cvl -> Prop) (cvl -> Prop) :=
  {| Var := id
   ; Arr := fun U V v =>
     if v isn't lam b then False else
       forall u, U u -> L V (tm_inst (@tvar 0) (u .: @var 0 0) b)
   ; All := fun F v =>
     if v isn't tlam b then False else
       forall P A, L (F P) (tm_inst (A .: @tvar 0) (@var 0 0) b)
  |}.

Definition V {m} (A : ty m) (ρ : fin m -> cvl -> Prop) (v : cvl) : Prop :=
  @eval _ _ D m ρ A v.

Definition E {m} (A : ty m) (ρ : fin m -> cvl -> Prop) (s : ctm) : Prop :=
  L (V A ρ) s.

Lemma V_to_E m (A : ty m) (ρ : fin m -> cvl -> Prop) (s : ctm) (v : cvl) :
  red s v -> V A ρ v -> E A ρ s.
Proof. move=> h1 h2. by exists v. Qed.

Lemma V_arr m (A B : ty m) (ρ : fin m -> cvl -> Prop) (b : tm 0 1) :
  V (arr A B) ρ (lam b) = forall u, V A ρ u -> E B ρ (tm_inst (@tvar 0) (u .: @var 0 0) b).
Proof. by []. Qed.

Lemma V_all m (A : ty m.+1) (ρ : fin m -> cvl -> Prop) (b : tm 1 0) :
  V (all A) ρ (tlam b) = forall P B, E A (P .: ρ) (tm_inst (B .: @tvar 0) (@var 0 0) b).
Proof. by []. Qed.

Lemma V_weaken m (A : ty m) (ρ : fin m -> cvl -> Prop) (P : cvl -> Prop) (s : cvl) :
  V (tyrename shift A) (P .: ρ) s = V A ρ s.
Proof. by rewrite/V eval_weaken. Qed.

Lemma V_beta m (A : ty m.+1) (B : ty m) (ρ : fin m -> cvl -> Prop) (s : cvl) :
  V (tyinst (B .: @tvar m) A) ρ s = V A (V B ρ .: ρ) s.
Proof. by rewrite/V eval_beta. Qed.

Lemma E_beta m (A : ty m.+1) (B : ty m) (ρ : fin m -> cvl -> Prop) (s : ctm) :
  E (tyinst (B .: @tvar m) A) ρ s = E A (V B ρ .: ρ) s.
Proof. rewrite/E; f_equal; fext=> v. exact: V_beta. Qed.

Unset Elimination Schemes.
Inductive tm_has_type {m n} (Γ : fin n -> ty m) : tm m n -> ty m -> Prop :=
| ty_val v A :
    vl_has_type Γ v A ->
    tm_has_type Γ (val v) A
| ty_app s t A B :
    tm_has_type Γ s (arr A B) ->
    tm_has_type Γ t A ->
    tm_has_type Γ (app s t) B
| ty_tapp s A B :
    tm_has_type Γ s (all A) ->
    tm_has_type Γ (tapp s B) (tyinst (B .: @tvar _) A)
with vl_has_type {m n} (Γ : fin n -> ty m) : vl m n -> ty m -> Prop :=
| ty_var i :
    vl_has_type Γ (var m i) (Γ i)
| ty_lam b A B :
    @tm_has_type m n.+1 (A .: Γ) b B ->
    vl_has_type Γ (lam b) (arr A B)
| ty_tlam b A :
    @tm_has_type m.+1 n (Γ >> tyrename shift) b A ->
    vl_has_type Γ (tlam b) (all A).
Set Elimination Schemes.

Scheme tm_has_type_ind := Minimality for tm_has_type Sort Prop
  with vl_has_type_ind := Minimality for vl_has_type Sort Prop.
Combined Scheme has_type_ind from tm_has_type_ind, vl_has_type_ind.

Definition Vl_has_type {m n} (Γ : fin n -> ty m) (v : vl m n) (A : ty m) :=
  forall (σ : tysubst m 0) (τ : vsubst 0 n 0) (ρ : fin m -> cvl -> Prop),
    (forall i, V (Γ i) ρ (τ i)) -> V A ρ (vl_inst σ τ v).

Definition Tm_has_type {m n} (Γ : fin n -> ty m) (s : tm m n) (A : ty m) :=
  forall (σ : tysubst m 0) (τ : vsubst 0 n 0) (ρ : fin m -> cvl -> Prop),
    (forall i, V (Γ i) ρ (τ i)) -> E A ρ (tm_inst σ τ s).

Theorem fundamental m n (Γ : fin n -> ty m) :
  (forall (t : tm m n) (A : ty m), tm_has_type Γ t A -> Tm_has_type Γ t A) /\
  (forall (v : vl m n) (A : ty m), vl_has_type Γ v A -> Vl_has_type Γ v A).
Proof with eauto using @red.
  move: m n Γ. apply: has_type_ind.
  - move=> m n Γ v A _ ih σ τ ρ γ /=. apply: V_to_E...
  - move=> m n Γ s t A B _ ihs _ iht σ τ ρ γ /=.
    case: (ihs σ τ ρ γ) => -[]//b red1. rewrite V_arr => l1.
    case: (iht σ τ ρ γ) => u red2 l2.
    case: (l1 u l2) => v red3 l3.
    apply: V_to_E...
  - move=> m n Γ s A B _ ih σ τ ρ γ /=.
    case: (ih σ τ ρ γ) => -[]//b red1. rewrite V_all => l1.
    case: (l1 (V B ρ) (tyinst σ B)) => v red2 l2.
    rewrite E_beta. apply: V_to_E...
  - move=> m n Γ i σ τ ρ γ /=. exact: γ.
  - move=> m n Γ b A B _ ih σ τ ρ γ. cbn=> u l1.
    have->: tm_inst (tvar (n:=0)) (u .: var 0 (n:=0)) (tm_inst σ (vup τ) b) = tm_inst σ (u .: τ) b.
    rewrite tm_inst_comp. f_equal. fext=> /=x. by rewrite ty_inst_ids.
    fext=>/=-[a|]//=. rewrite vl_ren_inst_comp. fsimpl. exact: vl_inst_ids.
    apply: ih => /=; by case.
  - move=> m n Γ b A _ ih σ τ ρ γ. cbn=> P B.
    have->:
        tm_inst (B .: tvar (n:=0)) (var 0 (n:=0)) (tm_inst (tup σ) (τ >> vl_rename shift id) b) =
        tm_inst (B .: σ) τ b.
    rewrite tm_inst_comp. f_equal. fext=>/=-[a|]//=. rewrite ty_ren_inst_comp; fsimpl.
    exact: ty_inst_ids. fext=>/=x. rewrite vl_ren_inst_comp. fsimpl. exact: vl_inst_ids.
    apply: ih => i /=. rewrite V_weaken. exact: γ.
Qed.

Corollary weak_normalization (s : ctm) (A : ty 0) :
  tm_has_type null s A -> exists v : cvl, red s v.
Proof.
  case: (@fundamental 0 0 null) => H _ /H/(_ (@tvar 0) (@var 0 0) null).
  case/(_ _) => // v. rewrite tm_inst_ids => red1 _. by exists v.
Qed.