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 eval.
Require Import typing_weakening.
Require Import typing_inv.
Require Import translate_morph.
Require Import translate_expr.
Require Import transl_inv.

Lemma typing_subst : forall Γ e τ z σ u,
  (((z,σ)::Γ) |- e \is τ) ->
  (Γ |- u \is σ) ->
  (Γ |- ([z ~ee~> u] e) \is τ)
.
Proof.
  intros E e u S T z H J.
  rewrite <- (nil_concat _ E).
Admitted.
  (*
  eapply typing_subst_strengthened.
    rewrite nil_concat. apply H.
    apply J.
Qed.
*)


Lemma subst_intro : forall (x : atom) u e,
  x `notin` (expr_fv e) ->
  expr_lc u ->
  expr_open u e = [x ~ee~> u](expr_open (ex_fvar x) e).
Proof.
  intros x u e H J.
  unfold expr_open.
  (*
  rewrite subst_open_rec; auto.
  simpl.
  destruct (x == x).
  Case "x = x".
    rewrite subst_fresh; auto.
  Case "x <> x".
    destruct n; auto.
Qed.
*)
Admitted.

Lemma typing_subst_type : forall Γ x σ e τ,
  (Γ |- e \is τ) ->
  (Γ |- ([x ~et~> σ] e) \is τ)
.
Proof.
Admitted.

Lemma subst_intro_type : forall (x : atom) τ e,
  x `notin` (expr_fv_type e) ->
  type_lc τ ->
  expr_open_type τ e = [x ~et~> τ](expr_open_type (ty_fvar x) e).
Proof.
  intros x u e H J.
  unfold expr_open.
Admitted.


Lemma preservation : forall Γ e e' e'' τ,
  (Γ |- e \is τ) ->
  (Γ |- [[ e \is τ ]] = e') ->
  (e' -->eval e'') ->
  (Γ |- e'' \is τ)
.
Proof with simpl_env.

  intros E e e' e'' τ Typing Transl Eval.
  induction Transl.

  (* Var *)
  - inversion Eval.

  (* Let *)
  - inversion Eval.
    pick fresh y.
    rewrite (subst_intro y); subst.
    2: fsetdec.
    2: inversion H5; assumption.

    apply typing_subst with (σ:=σ).
    apply transl_preservation with (e:=(expr_open [{ $y }] t)).
    apply typing_inv_let with (L:=L) (s:=e) (t:=t).
    1-2:assumption.
    fsetdec.

    apply transl_inv_let with (L:=L) (s:=e) (s':=e').
    assumption.
    2:fsetdec.
    2:apply transl_preservation with (e:=e).
    2-3:assumption.

    apply Expand_Let with (L:=L) (σ:=σ).
    assumption.
    assumption.
    assumption.

  (* Type-Abs *)
  - admit.
  (*
    inversion Eval; subst.
    pick fresh y.
    apply typing_inv_tabs.
    apply T_TypeAbs with (L:=L).
    intros x Fr.
    rewrite (subst_intro_type x); subst.
    apply typing_subst_type.
*)

  (* Type-App *)
  - inversion Eval; subst.
    pick fresh y.
    admit.

  (* func *)
  - inversion Eval.

  (* morph *)
  - inversion Eval.

  (* app *)
  - inversion Eval; subst.
    (* f is reduced *)
    * apply T_App with (σ':=σ) (σ:=σ).
      3: apply id_morphism_path.
      
      apply IHTransl1.
      assumption.
      inversion Transl1; subst; auto.
      apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
      3: apply id_morphism_path.
      apply T_MorphFun.
      apply morphism_path_correct with (τ:=σ') (τ':=σ).

      admit. (* σ' is lc *)
      admit. (* σ is lc *)
      admit. (* Γ is wf *)

      assumption.
      apply transl_preservation with (e:=a).
      assumption.
      assumption.

    (* f is value *)
    * apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
      3: apply id_morphism_path.
      -- apply transl_preservation with (e:=f).
         all:assumption.

      -- apply transl_preservation with (e:=[{m a'}]).
         apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
         3: apply id_morphism_path.
         apply T_MorphFun.
         apply morphism_path_correct.
         admit. (* σ' is lc *)
         admit. (* σ is lc *)
         admit. (* Γ is wf *)
         assumption.
         apply transl_preservation with (e:=a).
         assumption.
         assumption.

         
         admit.

    (* f is lambda *)
    * 
    * inversion Eval; subst.
      apply T_App with (σ':=σ) (σ:=σ).
      auto.
      apply T_App with (σ':=σ') (σ:=σ').
      apply T_MorphFun.
      apply morphism_path_correct.
      admit. (* σ' is lc *)
      admit. (* σ is lc *)
      admit. (* Γ is wf *)
      assumption.
      apply transl_preservation with (e:=a).
      assumption.
      assumption.
      apply id_morphism_path.
      apply id_morphism_path.
      apply T_App with (σ':=σ) (σ:=σ).
      3: apply id_morphism_path.

  (* morph-app *)
  - apply T_MorphFun.
    apply IHTransl.
    assumption.
    assumption.

  (* ascension *)
  - apply transl_preservation with (e:=[{e' as τ'}]).
    apply T_Ascend.
    apply transl_preservation with (e:=e).
    assumption.
    assumption.
    admit.
    (*
    apply Expand_Ascend with (Γ:=Γ) (e:=e) (τ':=τ') (τ:=τ) (e':=e').
    *)

  - apply transl_preservation with (e:=[{e' des τ'}]).
    apply T_Descend with (τ:=τ).
    apply transl_preservation with (e:=e).
    assumption.
    assumption.
    assumption.
    apply Expand_
    admit.

  (* descension *)
  - inversion Eval; subst.

    * apply T_DescendImplicit with (τ:=τ).
      apply transl_preservation with (e:=e).
      all: assumption.

    * inversion Eval; subst.
      apply transl_preservation with (e:=e).
      assumption.
      apply Expand_Descend with (τ:=τ).
      assumption.
      assumption.
      assumption.
      apply T_DescendImplicit with (τ:=τ').
      2: assumption.
      
      
      inversion Transl; subst.

      admit.
      apply transl_preservation with (e:=e0).
      
Admitted.