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_regular. 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. Lemma type_lc_spec_inv : forall τ, type_lc [< [τ] >] -> type_lc τ . Proof. Admitted. Lemma type_lc_ladder_inv2 : forall σ τ, type_lc [< σ ~ τ >] -> type_lc τ . Proof. Admitted. Lemma morph_regular_lc : forall Γ τ τ', env_wf Γ -> type_lc τ -> (Γ |- τ ~~> τ') -> type_lc τ' . Proof. intros. induction H1. - apply type_lc_sub with (τ1:=τ). assumption. assumption. Admitted. Lemma morph_path_inv : forall Γ τ τ' m, (Γ |- [[ τ ~~> τ' ]] = m) -> (Γ |- τ ~~> τ') . Proof. Admitted. (* * translated morphism path is locally closed *) Lemma morph_path_lc : forall Γ τ τ' m, type_lc τ -> env_wf Γ -> (Γ |- [[ τ ~~> τ' ]] = m) -> expr_lc m . Proof. intros Γ τ τ' m Wfτ WfEnv H. induction H. (* Subtype / Identity *) - apply Elc_Morph with (L:=dom Γ). assumption. intros x Fr. unfold expr_open. simpl. apply Elc_Descend. apply type_lc_sub with (τ1:=τ). assumption. assumption. apply Elc_Var. (* Lift *) - apply Elc_Morph with (L:=dom Γ). trivial. intros x Fr. unfold expr_open. simpl. apply Elc_Ascend. inversion Wfτ; assumption. apply Elc_App. rewrite expr_open_lc. apply IHtranslate_morphism_path. inversion Wfτ; assumption. inversion Wfτ; assumption. apply IHtranslate_morphism_path. inversion Wfτ; assumption. inversion Wfτ; assumption. apply Elc_Descend, Elc_Var. inversion Wfτ; 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. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). assumption. assumption. apply morph_path_inv with (m:=m1), H. assumption. apply IHtranslate_morphism_path2. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). assumption. assumption. apply morph_path_inv with (m:=m1), H. assumption. apply Elc_App. rewrite expr_open_lc. apply IHtranslate_morphism_path1. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). assumption. assumption. apply id_morphism_path. assumption. assumption. apply IHtranslate_morphism_path1. assumption. 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. apply type_lc_spec_inv; assumption. apply morph_path_inv in H. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). assumption. apply type_lc_spec_inv; assumption. assumption. rewrite expr_open_lc. apply IHtranslate_morphism_path. apply type_lc_spec_inv; assumption. assumption. apply IHtranslate_morphism_path. apply type_lc_spec_inv; assumption. assumption. Qed. (* * translated morphism path has valid typing *) Lemma morphism_path_correct : forall Γ τ τ' m, type_lc τ -> env_wf Γ -> (Γ |- [[ τ ~~> τ' ]] = m) -> (Γ |- m \is [< τ ->morph τ' >]) . Proof. intros Γ τ τ' m Lcτ WfEnv H. induction H. (* Sub *) - apply T_MorphAbs with (σ:=τ) (τ:=τ') (L:=dom Γ). intros. unfold expr_open. simpl. apply T_Descend with (τ:=τ). apply T_Var. apply env_wf_type. 1-3,5: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. apply env_wf_type; assumption. simpl_env. unfold binds. simpl. destruct (x==x). reflexivity. contradict n. reflexivity. apply TSubRepr_Ladder, TSubRepr_Refl. apply equiv.TEq_Refl. } inversion Lcτ; subst. rewrite expr_open_lc. simpl_env. apply typing_weakening. apply T_MorphFun. apply IHtranslate_morphism_path. apply type_lc_ladder_inv2 with (σ:=σ); assumption; assumption. assumption. apply env_wf_type. assumption. assumption. assumption. apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ'). assumption. assumption. assumption. apply type_lc_ladder_inv2 with (σ:=σ). all: assumption. (* Single *) - apply T_Var. assumption. 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. apply morph_path_inv in H. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). 1-3: assumption. assumption. apply env_wf_type. 1-3: assumption. apply morph_path_lc with (Γ:=Γ) (τ:=τ') (τ':=τ''). 2-3: assumption. apply morph_path_inv in H. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). all: assumption. * apply T_App with (σ':=τ) (σ:=τ) (τ:=τ'). rewrite expr_open_lc. simpl_env. apply typing_weakening. apply T_MorphFun. apply IHtranslate_morphism_path1. 3: apply env_wf_type. 1-5: assumption. apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ'). 1-3: assumption. apply T_Var. apply env_wf_type; assumption. 2: apply id_morphism_path. simpl_env; apply binds_head, binds_singleton. assumption. * apply morph_path_inv in H. apply morph_regular_lc with (Γ:=Γ) (τ:=τ). all: assumption. (* 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. 2: assumption. 2: apply env_wf_type; assumption. inversion Lcτ; assumption. apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ'). inversion Lcτ; assumption. 1-2: assumption. apply Tlc_Func. apply type_lc_spec_inv; assumption. apply morph_path_inv in H. apply morph_regular_lc in H. assumption. assumption. apply type_lc_spec_inv; assumption. apply T_Var. apply env_wf_type; assumption. simpl_env; apply binds_head, binds_singleton. assumption. Qed.