Require Export axioms.
Require Export SystemFCBV.

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

Import CommaNotation.

Inductive eval {m n} : tm m n → vl m n → Prop :=
| eval_app (A : ty m) s t u (v1 v2 : vl m n) :
    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 m) s u v :
    eval s (tlam u) → eval u[A .: var_ty; var_vl] v →
    eval (tapp s A) v
| eval_val (v : vl m n) :
    eval (vt v) v.
Hint Resolve eval_val.

Definition ctx (m n : nat) := fin n → ty m.

Unset Elimination Schemes.
Inductive tm_ty m n (Gamma : ctx m n) : tm m n → ty m → Prop :=
| ty_app (A B : ty m) (s t : tm m n) :
    tm_ty Gamma s (arr A B) →
    tm_ty Gamma t A →
    tm_ty Gamma (app s t) B
| ty_tapp A A' B (s : tm m n) :
    tm_ty Gamma s (all A) → A' = A[B .: var_ty] →
    tm_ty Gamma (tapp s B) A'
| ty_val (A : ty m) (v : vl m n) :
    vl_ty Gamma v A →
    tm_ty Gamma (vt v) A
with vl_ty m n (Gamma : ctx m n) : vl m n → ty m → Prop :=
     | ty_var (x : fin n) s :
         s = Gamma x →
 vl_ty Gamma (var_vl x) s
| ty_lam A B (s : tm m (S n)) :
    @tm_ty m (S n) (A, Gamma) s B →
    vl_ty Gamma (lam A s) (arr A B)
| ty_tlam A (s : tm (S m) n) :
    @tm_ty (S m) n (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.

Hint Constructors tm_ty vl_ty.

 Definition lt_ctx_ren {m n m' n'} (Gamma : ctx m n) (Delta : ctx m' n') (xi: fin m → fin m') (zeta: fin n → fin n') :=
   ∀ x, (Gamma x)⟨xi⟩= Delta (zeta x).

Lemma typing_ren m n (Gamma : ctx m n):
  (∀ s A, tm_ty Gamma s A → ∀ m' n' (Delta : ctx m' n') (sigma : fin m → fin m') (tau : fin n → fin n'),
lt_ctx_ren Gamma Delta sigma tau → tm_ty Delta (s⟨sigma;tau⟩) (A⟨sigma⟩))
∧ (∀ s A, vl_ty Gamma s A → ∀ m' n' (Delta : ctx m' n') (sigma : fin m → fin m') (tau : fin n → fin n') A',
          A' = A⟨sigma⟩ → lt_ctx_ren Gamma Delta sigma tau → vl_ty Delta (s⟨sigma;tau⟩) A').
Proof.
  revert m n Gamma. apply has_ty_ind; intros; subst; asimpl; eauto.
  - econstructor. asimpl in H0. eapply H0. eauto. now asimpl.
  - constructor. eapply H0. unfold lt_ctx_ren.
    auto_case.
  - constructor. eapply H0. unfold lt_ctx_ren. intros z. asimpl. unfold funcomp.
    rewrite <- H2. now asimpl.
Qed.

Definition lt_ctx {m n m' n'} (Gamma : ctx m n) (Delta : ctx m' n') sigma tau :=
  ∀ x, vl_ty Delta (tau x) (Gamma x)[sigma].

Lemma typing_subst m n (Gamma : ctx m n):
  (∀ s A, tm_ty Gamma s A → ∀ m' n' (Delta : ctx m' n') (sigma : fin m → ty m') (tau : fin n → vl m' n'),
lt_ctx Gamma Delta sigma tau → tm_ty Delta (s[sigma;tau]) (A[sigma]))
∧ (∀ s A, vl_ty Gamma s A → ∀ m' n' (Delta : ctx m' n') (sigma : fin m → ty m') (tau : fin n → vl m' n'),
lt_ctx Gamma Delta sigma tau → vl_ty Delta (s[sigma;tau]) (A[sigma])).
Proof.
  revert m n Gamma. apply has_ty_ind; intros; subst; asimpl; eauto.
  - econstructor. asimpl in H0. apply H0. eauto. now asimpl.
  - econstructor. apply H0.
    unfold lt_ctx. intros [|].
    + cbn. eapply typing_ren. eapply H1. now asimpl.
      unfold lt_ctx_ren. intros x. now asimpl.
    + cbn. constructor. now asimpl.
  - econstructor. apply H0.
    unfold lt_ctx. intros. asimpl.
    unfold funcomp. eapply typing_ren. eapply H1. now asimpl.
    unfold lt_ctx_ren. now asimpl.
Qed.

Definition L {m n} (P : vl m n → Prop) (s : tm m n) :=
  ∃ v, eval s v ∧ P v.

Fixpoint V {m m' n'} (A : ty m) (rho : fin m → vl m' n' → Prop) (v : vl m' n' ) {struct A} : Prop :=
  match A with
  | var_ty X ⇒ rho X v
  | arr A B ⇒
    match v with
    | lam C s ⇒ ∀ u, V A rho u → L (V B rho) s[var_ty; u .: var_vl]
    | _ ⇒ False
    end
  | all A ⇒
    match v with
    | tlam s ⇒ ∀ B i, ∃ (v: vl m' n'), eval (s[B..; ids]) v
                                                                  ∧ V A (i .: rho) v
    | _ ⇒ False
    end
  end.
Notation E A rho := (L (V A rho)).

Lemma V_ren m m' m'' n' (A: ty m) (rho: fin m'' → vl m' n' → Prop) (xi: fin m → fin m'') :
  V A⟨xi⟩ rho = V A (xi >> rho).
Proof.
  revert m' m'' n' rho xi. induction A; intros; eauto.
  - fext. intros [| |]; eauto.
    simpl. fext. intros v. asimpl. now rewrite IHA1, IHA2.
  - fext. intros [| |]; eauto.
    simpl. fext. intros. asimpl. rewrite IHA. now asimpl.
Qed.

Lemma V_weak m m' n' A d (rho: fin m → vl m' n' → Prop) :
  V (ren_ty ↑ A) (d .: rho) = V A rho.
Proof. eapply V_ren. Qed.

Lemma V_subst m m' n' m'' (A : ty m) (rho: fin m'' → vl m' n' → Prop) (sigma: fin m → ty m'') :
  V (subst_ty sigma A) rho = V A (fun x ⇒ V (sigma x) rho).
Proof.
  revert m' m'' n' rho sigma. induction A; intros; eauto.
  - fext. intros [| |]; eauto.
    simpl. fext. intros v. asimpl. now rewrite IHA1, IHA2.
  - fext. intros [| |]; eauto.
    simpl. fext. intros. asimpl.
    rewrite IHA.
    f_equal. fext. intros. repeat f_equal. fext. auto_case.
    intros. asimpl. now rewrite V_weak.
Qed.

Lemma E_subst1 m m' n' (A : ty (S m)) B (rho: fin m → vl m' n' → Prop) :
  E (subst_ty (B .: var_ty) A) rho = E A (V B rho .: rho).
Proof.
  unfold E. fext. intros. f_equal. fext. intros.
  f_equal. rewrite V_subst. repeat f_equal. fext. auto_case.
Qed.

Definition VG {m n m' n'} (Gamma : ctx m n) (rho : fin m → vl m' n' → Prop) (sigma : fin n → vl m' n') :=
  ∀ x, V (Gamma x) rho (sigma x).

Theorem soundness m n (Gamma : ctx m n) :
  (∀ (s : tm m n) (A : ty m), tm_ty Gamma s A →
    ∀ m' n' (sigma: fin m → ty m') (tau: fin n → vl m' n') rho, VG Gamma rho tau → E A rho s[sigma;tau]) ∧
  (∀ (v : vl m n) (A : ty m), vl_ty Gamma v A →
    ∀ m' n' (sigma: fin m → ty m') (tau: fin n → vl m' n') rho, VG Gamma rho tau → V A rho v[sigma;tau]).
Proof.
  revert m n Gamma. apply has_ty_ind; intros; subst; asimpl in *; eauto.
  - destruct (H0 _ _ sigma _ rho H3) as ([]&ev1&h1); simpl in h1; try contradiction.
    destruct (H2 _ _ sigma _ rho H3) as (v1&ev2&h2).
    destruct (h1 _ h2) as (v2&ev3&h3).
    ∃ v2. split; eauto using eval_app.
  - rewrite E_subst1.
    destruct (H0 _ _ sigma _ rho H2) as ([]&ev1&h1); simpl in h1; try contradiction.
    destruct (h1 (B[sigma]) (V B rho)) as (v&ev2&h2).
    ∃ v. eauto using eval_tapp.
  - eexists; asimpl; eauto.
  - simpl. intros. asimpl. apply H0.
    intros [|]; cbn; asimpl; eauto.
  - simpl. intros. asimpl. asimpl in H0. apply H0.
    intros x. asimpl. rewrite V_weak. apply H1.
Qed.

Definition nilA {m n}: fin m → vl m n → Prop := fun _ _ ⇒ False.

Definition empty {m} : fin 0 → ty m := fun x ⇒ match x with end.

Corollary soundness_nil m (s: tm m 0) A :
  tm_ty empty s A → E A nilA s.
Proof.
  intros H.
  replace s with (s[ids;ids]) by now asimpl.
  eapply soundness; eauto.
  intros x. now destruct x.
Qed.

Corollary normalization m (s: tm m 0) A :
  tm_ty empty s A → ∃ v, eval s v.
Proof.
  intros H. apply soundness_nil in H.
  destruct H. eexists; eauto. eapply H.
Qed.

Corollary consistency (s: tm 0 0) :
  ¬tm_ty empty s (all (var_ty var_zero)).
Proof.
  intros H. eapply soundness_nil in H.
  destruct H as (?&?&?). simpl in H0. destruct x; eauto.
  now destruct (H0 (all (var_ty var_zero)) (fun _ ⇒ False)) as (?&?&?) .
Qed.