Require Export axioms.
From mathcomp Require Import all_ssreflect.
Require Export SystemF_cbv.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Notation "s .[ sigma , tau ]" := (s.[(sigma, tau)])
  (at level 2, sigma at level 200, left associativity,
   format "s .[ sigma , tau ]" ) : subst_scope.

Notation "'ren' xi" :=
  (xi >>> var_ty) (at level 50).

Inductive eval : tm -> vl -> Prop :=
| eval_app (A : ty) (s t u : tm) (v1 v2 : vl) :
    eval s (lam A u) -> eval t v1 -> eval u.[var_ty, v1 .: var_vl] v2 ->
    eval (app s t) v2
| eval_tapp (A : ty) (s u : tm) (v : vl) :
    eval s (tlam u) -> eval u.[A .: var_ty, var_vl] v ->
    eval (tapp s A) v
| eval_val (v : vl) :
    eval (vt v) v.
Hint Resolve eval_val.

Definition ctx := seq ty.

Definition get (Gamma : ctx) (n : index) : ty :=
  nth (var_ty 0) Gamma n.
Local Notation "Gamma `_ i" := (get Gamma i).

Lemma get_map (f : ty -> ty) Gamma n :
  n < size Gamma -> (map f Gamma)`_n = f (Gamma`_n).
Proof. exact: nth_map. Qed.

Unset Elimination Schemes.
Inductive tm_ty (Gamma : ctx) : tm -> ty -> Prop :=
| ty_app (A B : ty) (s t : tm) :
    tm_ty Gamma s (arr A B) ->
    tm_ty Gamma t A ->
    tm_ty Gamma (app s t) B
| ty_tapp (A B : ty) (s : tm) :
    tm_ty Gamma s (all A) ->
    tm_ty Gamma (tapp s B) A.[B .: var_ty]
| ty_val (A : ty) (v : vl) :
    vl_ty Gamma v A ->
    tm_ty Gamma (vt v) A
with vl_ty (Gamma : ctx) : vl -> ty -> Prop :=
| ty_var (x : index) :
    x < size Gamma -> vl_ty Gamma (var_vl x) Gamma`_x
| ty_lam (A B : ty) (s : tm) :
    tm_ty (A :: Gamma) s B ->
    vl_ty Gamma (lam A s) (arr A B)
| ty_tlam (A : ty) (s : tm) :
    tm_ty (map (fun A : ty => A.[ren (+1)]) Gamma) s A ->
    vl_ty Gamma (tlam s) (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 has_ty_ind from tm_ty_ind, vl_ty_ind.

Definition L (P : vl -> Prop) (s : tm) :=
  exists2 v, eval s v & P v.

Fixpoint V (A : ty) (rho : index -> vl -> Prop) (v : vl) {struct A} : Prop :=
  match A with
  | var_ty X => rho X v
  | arr A B =>
    match v with
    | lam C s => forall u, V A rho u -> L (V B rho) s.[var_ty, u .: var_vl]
    | _ => False
    end
  | all A =>
    match v with
    | tlam s => forall i (B : ty), L (V A (i .: rho)) s.[B .: var_ty, var_vl]
    | _ => False
    end
  end.
Notation E A rho := (L (V A rho)).

Lemma V_ren (A : ty) rho xi :
  V A.[ren xi] rho = V A (xi >>> rho).
Proof.
  elim: A rho xi => //.
  - move=> A ih1 B ih2 rho xi. fext=> -[] // C s. asimpl=>/=.
    fext=> v. by rewrite ih1 ih2.
  - move=> A ih rho xi. fext=> -[]// s.
    replace (all A).[ren xi] with (all A.[ren (0 .: (xi >>> (+1)))]) by repeat (f_equal; asimpl).
    move=>/=. fext=> i B. rewrite ih. autosubst.
Qed.

Lemma V_weak (A : ty) d rho :
  V A.[ren (+1)] (d .: rho) = V A rho.
Proof. exact: V_ren. Qed.

Lemma V_subst (A : ty) rho sigma :
  V A.[sigma] rho = V A (fun x => V (sigma x) rho).
Proof.
  elim: A rho sigma.
  - move=> x rho sigma /=. by asimpl.
  - move=> A ih1 B ih2 rho sigma. fext=> -[] // C s.
    asimpl=>/=. fext=> u. by rewrite ih1 ih2.
  - move=> A ih rho sigma. fext=> -[]//s. asimpl=>/=.
    fext=> i B. rewrite ih. repeat f_equal; fext=> -[|n] v //=.
    by rewrite V_weak.
Qed.

Lemma E_subst1 (A B : ty) rho :
  E A.[B .: var_ty] rho = E A (V B rho .: rho).
Proof.
  rewrite V_subst. repeat f_equal; by fext=> -[].
Qed.

Definition VG (Gamma : ctx) (rho : index -> vl -> Prop) (sigma : index -> vl) :=
  forall x, x < size Gamma -> V Gamma`_x rho (sigma x).

Theorem soundness (Gamma : ctx) :
  (forall (s : tm) (A : ty), tm_ty Gamma s A ->
    forall sigma tau rho, VG Gamma rho tau -> E A rho s.[sigma,tau]) /\
  (forall (v : vl) (A : ty), vl_ty Gamma v A ->
    forall sigma tau rho, VG Gamma rho tau -> V A rho v.[sigma,tau]).
Proof.
  move: Gamma. apply has_ty_ind.
  - move=> Gamma A B s t _ ih1 _ ih2 sigma tau rho vg. asimpl.
    case: (ih1 sigma tau rho vg) => {ih1} -[]// C u ev1 /= h1.
    case: (ih2 sigma tau rho vg) => {ih2} v1 ev2 h2.
    case: (h1 v1 h2) => {h1 h2} v2 ev3 h3.
    exists v2. exact: eval_app ev1 ev2 ev3. exact: h3.
  - move=> Gamma A B s _ ih sigma tau rho vg. asimpl. rewrite E_subst1.
    case: (ih sigma tau rho vg) => {ih} -[]//= u ev1 h1.
    case: (h1 (V B rho) B.[sigma]) => v ev2 h2.
    exists v. exact: eval_tapp ev1 ev2. exact: h2.
  - move=> Gamma A v _ ih sigma tau rho vg.
    eexists; asimpl. exact: eval_val. exact: ih.
  - move=> Gamma x mem sigma tau rho vg. exact: vg.
  - move=> Gamma A B s _ ih sigma tau rho vg. asimpl=> /= v h1; asimpl.
    apply: ih => -[_|x] //=. exact: vg.
  - move=> Gamma A s _ ih sigma tau rho vg. asimpl=>/= i B; asimpl.
    apply: ih => x. rewrite size_map => mem. rewrite get_map //.
    rewrite V_weak. exact: vg.
Qed.

Definition nilA : index -> vl -> Prop := fun _ _ => False.

Corollary soundness_nil s A :
  tm_ty [::] s A -> E A nilA s.
Proof.
  case: (soundness [::]) => H _ /H/(_ var_ty var_vl nilA).
  case/(_ _)/Wrap=> //. by asimpl.
Qed.

Corollary normalization s A :
  tm_ty [::] s A -> exists v, eval s v.
Proof.
  move=> /soundness_nil[v hv] _. by exists v.
Qed.

Corollary consistency s :
  ~tm_ty [::] s (all (var_ty 0)).
Proof.
  by move=> /soundness_nil[-[]//u ev /=/(_ (fun _ => False) (var_ty 0))[]].
Qed.