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.



Lemma map_type : forall Γ,
  Γ |- [{ $at_map }] \is [< ∀ ∀ ((%1) -> (%0)) -> [%1] -> [%0] >]
.
Proof.
Admitted.

Lemma specialized_map_type : forall Γ τ τ',
  Γ |- [{ $at_map # τ # τ' }] \is [<
    (τ -> τ') -> [τ] -> [τ']
  >].
Proof.
  intros.
  set (u:=[< ((%1)->(%0)) -> [%1] -> [%0] >]).
  set (v:=[< (τ->(%0)) -> [τ] -> [%0] >]).
  set (x:=(type_open τ u)).
  set (y:=(type_open τ' x)).
(*
  unfold type_open in x.
  simpl in x.
  apply T_TypeApp with (Γ:=Γ) (e:=[{ $at_map # τ }]) (τ:=x) (σ:=τ').
*)
Admitted.

(*
 * translated morphism path is locally closed
 *)
Lemma morphism_path_lc : forall Γ τ τ' m,
  type_lc τ ->
  type_lc τ' ->
  env_wf Γ ->
  (Γ |- [[ τ ~~> τ' ]] = m) ->
  expr_lc m
.
Proof.
  intros Γ τ τ' m Wfτ1 Wfτ2 WfEnv H.
  induction H.

  (* Subtype / Identity *)
  - apply Elc_Morph with (L:=dom Γ).
    assumption.
    intros x Fr.
    unfold expr_open.
    simpl.
    apply Elc_Descend.
    assumption.
    apply Elc_Var.

  (* Lift *)
  - apply Elc_Morph with (L:=dom Γ).
    trivial.
    intros x Fr.
    unfold expr_open.
    simpl.
    apply Elc_Ascend.
    inversion Wfτ1; assumption.
    apply Elc_App.
    rewrite expr_open_lc.

    apply IHtranslate_morphism_path.
    inversion Wfτ1; assumption.
    inversion Wfτ2; assumption.
    assumption.

    apply IHtranslate_morphism_path.
    inversion Wfτ1; assumption.
    inversion Wfτ2; assumption.
    assumption.

    apply Elc_Descend, Elc_Var.
    inversion Wfτ1; assumption.

  (* Single Morphism *)
  - apply Elc_Var.
  
  (* Chain *)
  - apply Elc_Morph with (L:=dom Γ).
    assumption.
    intros x Fr.
    unfold expr_open; simpl.

    apply Elc_App.
    rewrite expr_open_lc.
    apply IHtranslate_morphism_path2.
    1-3:assumption.
    apply IHtranslate_morphism_path2.
    1-3:assumption.

    apply Elc_App.
    rewrite expr_open_lc.
    apply IHtranslate_morphism_path1.
    1-3:assumption.
    apply IHtranslate_morphism_path1.
    1-3:assumption.
    apply Elc_Var.

  (* Map *)
  - apply Elc_Morph with (L:=dom Γ).
    assumption.
    intros x Fr.
    unfold expr_open; simpl.
    apply Elc_App.
    2: apply Elc_Var.
    apply Elc_App.
    apply Elc_TypApp.
    apply Elc_TypApp.
    apply Elc_Var.
    inversion Wfτ1; assumption.
    inversion Wfτ2; assumption.

    rewrite expr_open_lc.
    apply IHtranslate_morphism_path.
    inversion Wfτ1; assumption.
    inversion Wfτ2; assumption.
    assumption.
    apply IHtranslate_morphism_path.
    inversion Wfτ1; assumption.
    inversion Wfτ2; assumption.
    assumption.
Qed.

(*
 * translated morphism path has valid typing
 *)
Lemma morphism_path_correct : forall Γ τ τ' m,
  type_lc τ ->
  type_lc τ' ->
  env_wf Γ ->
  (Γ |- [[ τ ~~> τ' ]] = m) ->
  (Γ |- m \is [< τ ->morph τ' >])
.
Proof.
  intros Γ τ τ' m Lcτ1 Lcτ2 Ok H.
  induction H.

  (* Sub *)
  - apply T_MorphAbs with (σ:=τ) (τ:=τ') (L:=dom Γ).
    intros.
    unfold expr_open.
    simpl.
    apply T_Descend with (τ:=τ).
    apply T_Var.
    2:assumption.
    simpl_env.
    apply binds_head, binds_singleton.

  (* Lift *)
  - apply T_MorphAbs with (σ:=[<σ~τ>]) (τ:=[<σ~τ'>]) (L:=dom Γ).
    intros x Fr.
    unfold expr_open; simpl.
    apply T_Ascend.
    apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
    3: apply id_morphism_path.
    2: {
      apply T_Descend with (τ:=[< σ ~ τ >]).
      apply T_Var.
      simpl_env.
      unfold binds. simpl.
      destruct (x==x).
      reflexivity.
      contradict n.
      reflexivity.
      apply TSubRepr_Ladder, TSubRepr_Refl.
      apply equiv.TEq_Refl.
    }

    inversion Lcτ1.
    inversion Lcτ2.
    subst.
    apply morphism_path_lc in H0.

    rewrite expr_open_lc.
    apply typing_weakening with (Γ':=(x,[< σ ~ τ >])::[]).
    apply T_MorphFun.
    apply IHtranslate_morphism_path.
    4: apply env_wf_type.
    all: assumption.

  (* Single *)
  - apply T_Var.
    apply H.

  (* Chain *)
  - apply T_MorphAbs with (L:=dom Γ).
    intros x Fr.
    unfold expr_open.
    simpl.
    apply T_App with (σ':=τ') (σ:=τ') (τ:=τ'').
    3: apply id_morphism_path.

    * apply T_MorphFun.
      rewrite expr_open_lc.
      simpl_env; apply typing_weakening.
      apply IHtranslate_morphism_path2.
      1-3: assumption.
      apply env_wf_type.
      1-3: assumption.
      apply morphism_path_lc with (Γ:=Γ) (τ:=τ') (τ':=τ'').
      1-4: assumption.

    * apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
      rewrite expr_open_lc.
      apply typing_weakening with (Γ':=(x,τ)::[]).
      apply T_MorphFun.
      apply IHtranslate_morphism_path1.
      4: apply env_wf_type.
      1-6: assumption.
      apply morphism_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
      1-4: assumption.
      apply T_Var.
      2: apply id_morphism_path.
      simpl_env; apply binds_head, binds_singleton.

  (* Map Sequence *)
  - apply T_MorphAbs with (L:=dom Γ).
    intros x Fr.
    unfold expr_open.
    simpl.
    apply T_App with (σ':=[< [τ] >]) (σ:=[< [τ] >]).
    3: apply id_morphism_path.
    apply T_App with (σ':=[< τ -> τ' >]) (σ:=[< τ -> τ' >]).
    3: apply id_morphism_path.

    apply specialized_map_type.
    rewrite expr_open_lc.
    simpl_env; apply typing_weakening.
    apply T_MorphFun.
    apply IHtranslate_morphism_path.
    3: assumption.
    3: apply env_wf_type; assumption.
    inversion Lcτ1; assumption.
    inversion Lcτ2; assumption.
    apply morphism_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
    inversion Lcτ1; assumption.
    inversion Lcτ2; assumption.
    1-2: assumption.
    apply T_Var.
    simpl_env; apply binds_head, binds_singleton.
Qed.