246 lines
5.4 KiB
Coq
246 lines
5.4 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 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.
|