253 lines
5.8 KiB
Coq
253 lines
5.8 KiB
Coq
|
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.
|