From Coq Require Import Lists.List.
Require Import Atom.
Require Import Environment.
Require Import Metatheory.
Require Import debruijn.
Require Import subtype.
Require Import env.
Require Import morph.
Require Import subst_lemmas.
Require Import typing.
Require Import typing_weakening.
Require Import typing_regular.
Require Import translate_morph.

Lemma typing_inv_tabs : forall Γ t τ,
  (Γ |- [{ Λ t }] \is [< ∀ τ >]) ->
  forall L x, x `notin` L ->
  (Γ |- (expr_open_type (ty_fvar x) t) \is τ)
.
Proof.
Admitted.


Lemma typing_inv_abs : forall Γ σ t τ,
  (Γ |- [{ λ σ ↦ t }] \is [< σ -> τ >]) ->
  forall L x, x `notin` L ->
  ((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
.
Proof.
Admitted.


Lemma typing_inv_morph : forall Γ σ t τ,
  (Γ |- [{ λ σ ↦morph t }] \is [< σ ->morph τ >]) ->
  forall L x, x `notin` L ->
  ((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
.
Proof.
  intros.
  
  inversion H.
  subst.
  
Admitted.


Lemma typing_inv_let : forall Γ s σ t τ,
  (Γ |- s \is σ) ->
  (Γ |- [{ let s in t }] \is [< τ >]) ->
  forall L x, x `notin` L ->
  ((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
.
Proof.
Admitted.



(*
 * translated morphism path has valid typing
 *)
Lemma transl_preservation : forall Γ e e' τ,
  (Γ |- e \is τ) ->
  (Γ |- [[ e \is τ ]] = e') ->
  (Γ |- e' \is τ)
.
Proof.
  intros Γ e e' τ Typing Transl.
  induction Transl.

  (* free var *)
  - assumption.

  (* let *)
  - apply T_Let with (L:=L) (σ:=σ).
    * apply IHTransl.
      assumption.

    * intros x Fr.
      apply H1.
      assumption.
      apply typing_inv_let with (L:=L) (s:=e).
      1-3:assumption.
      apply typing_inv_let with (L:=L) (s:=e).
      1-3:assumption.

  (* type abs *)
  - apply T_TypeAbs with (L:=L).
    intros x Fr.
    apply H0.
    assumption.
    apply typing_inv_tabs with (L:=L).
    1-2:assumption.
    apply typing_inv_tabs with (L:=L).
    1-2:assumption.

  (* type app *)
  - apply T_TypeApp.
    apply IHTransl.
    assumption.

  (* abs *)
  - apply T_Abs with (L:=L).
    intros x Fr.
    apply H1.
    assumption.
    apply typing_inv_abs with (L:=L).
    1-2:assumption.
    apply typing_inv_abs with (L:=L).
    1-2:assumption.

  (* morph abs *)
  - apply T_MorphAbs with (L:=L).
    intros x Fr.
    apply H1.
    assumption.
    apply typing_inv_morph with (L:=L).
    1-2:assumption.
    apply typing_inv_morph with (L:=L).
    1-2:assumption.

  (* app *)
  - apply T_App with (σ':=σ) (σ:=σ); auto.
    apply T_App with (σ':=σ') (σ:=σ'); auto.
    2-3: apply id_morphism_path.
    apply T_MorphFun.
    apply morphism_path_correct with (τ:=σ') (τ':=σ).
    3: assumption.

    2:admit. (* env wf *)

    apply typing_regular_type_lc with (Γ:=Γ) (e:=a).
    assumption.
    apply typing_regular_type_lc with (Γ:=Γ) (e:=a).
    assumption.

    apply morph_regular_lc with (Γ:=Γ) (τ:=σ') (τ':=σ).
    admit. (* env wf *)

    apply typing_regular_type_lc with (Γ:=Γ) (e:=a).
    assumption.
    assumption.

  - auto with typing_hints.
  - auto with typing_hints.
  - eauto with typing_hints.
Admitted.