359 lines
6.8 KiB
Coq
359 lines
6.8 KiB
Coq
From Coq Require Import Strings.String.
|
||
Require Import terms.
|
||
Require Import subst.
|
||
Require Import equiv.
|
||
Require Import subtype.
|
||
Require Import context.
|
||
Require Import morph.
|
||
Require Import smallstep.
|
||
Require Import typing.
|
||
|
||
Lemma typing_weakening : forall Γ e τ x σ,
|
||
(Γ |- e \is τ) ->
|
||
((ctx_assign x σ Γ) |- e \is τ)
|
||
.
|
||
Proof.
|
||
intros.
|
||
induction H.
|
||
|
||
- apply T_Var.
|
||
apply C_shuffle.
|
||
apply H.
|
||
|
||
- apply T_Let with (σ:=σ0).
|
||
apply IHexpr_type1.
|
||
admit.
|
||
Admitted.
|
||
|
||
Lemma typing_subst : forall Γ x σ s e τ,
|
||
(ctx_assign x σ Γ) |- e \is τ ->
|
||
Γ |- s \is σ ->
|
||
Γ |- (expr_subst x s e) \is τ.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Lemma typing_tsubst : forall Γ α σ e τ,
|
||
Γ |- e \is τ ->
|
||
Γ |- (expr_specialize α σ e) \is (type_subst α σ τ).
|
||
Proof.
|
||
Admitted.
|
||
|
||
|
||
|
||
Lemma map_type : forall Γ,
|
||
Γ |- [{ %"map"% }] \is [<
|
||
∀"σ",∀"τ", (%"σ"% -> %"τ"%) -> [%"σ"%] -> [%"τ"%]
|
||
>].
|
||
Proof.
|
||
Admitted.
|
||
|
||
Lemma specialized_map_type : forall Γ τ τ',
|
||
Γ |- [{ %"map"% # τ # τ' }] \is [<
|
||
(τ -> τ') -> [τ] -> [τ']
|
||
>].
|
||
Proof.
|
||
Admitted.
|
||
|
||
|
||
|
||
|
||
(* morphism has valid typing *)
|
||
Lemma morphism_path_solves_type : forall Γ τ τ' m,
|
||
(translate_morphism_path Γ τ τ' m) ->
|
||
Γ |- m \is (type_morph τ τ')
|
||
.
|
||
Proof.
|
||
intros.
|
||
induction H.
|
||
|
||
(* Sub *)
|
||
apply T_MorphAbs.
|
||
apply T_Descend with (τ:=τ).
|
||
apply T_Var.
|
||
apply C_take.
|
||
apply H.
|
||
|
||
(* Lift *)
|
||
apply T_MorphAbs.
|
||
apply T_Ascend.
|
||
apply T_App with (σ':=τ) (σ:=τ).
|
||
apply T_MorphFun.
|
||
apply typing_weakening.
|
||
apply IHtranslate_morphism_path.
|
||
apply T_Descend with (τ:=(type_ladder σ τ)).
|
||
apply T_Var.
|
||
apply C_take.
|
||
apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
|
||
apply id_morphism_path.
|
||
|
||
(* Single *)
|
||
apply T_Var.
|
||
apply H.
|
||
|
||
(* Chain *)
|
||
apply T_MorphAbs.
|
||
apply T_App with (σ':=τ') (σ:=τ') (τ:=τ'').
|
||
apply T_MorphFun.
|
||
apply typing_weakening.
|
||
apply IHtranslate_morphism_path2.
|
||
|
||
apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
|
||
apply T_MorphFun.
|
||
apply typing_weakening.
|
||
apply IHtranslate_morphism_path1.
|
||
|
||
apply T_Var.
|
||
apply C_take.
|
||
apply id_morphism_path.
|
||
apply id_morphism_path.
|
||
|
||
(* Map Sequence *)
|
||
apply T_MorphAbs.
|
||
apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)).
|
||
apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')).
|
||
|
||
apply specialized_map_type.
|
||
apply typing_weakening.
|
||
apply T_MorphFun.
|
||
apply IHtranslate_morphism_path.
|
||
|
||
apply id_morphism_path.
|
||
auto using T_Var, C_take.
|
||
apply id_morphism_path.
|
||
Qed.
|
||
|
||
|
||
|
||
|
||
(* reduction step preserves well-typedness *)
|
||
Lemma preservation : forall Γ e e' τ,
|
||
(Γ |- e \is τ) ->
|
||
(e -->β e') ->
|
||
(Γ |- e' \is τ)
|
||
.
|
||
Proof.
|
||
intros Γ e e' τ Typ Red.
|
||
generalize dependent e'.
|
||
induction Typ; intros e' Red.
|
||
|
||
(* `e` is Variable *)
|
||
- inversion Red.
|
||
|
||
(* `e` is Let *)
|
||
- inversion Red.
|
||
subst.
|
||
apply typing_subst with (σ:=σ).
|
||
auto.
|
||
auto.
|
||
|
||
(* `e` is Type-Abstraction *)
|
||
- inversion Red.
|
||
subst.
|
||
apply T_TypeAbs.
|
||
auto.
|
||
|
||
(* `e` is Type-Application *)
|
||
- inversion Red.
|
||
admit.
|
||
(*
|
||
apply typing_tsubst.
|
||
admit.
|
||
*)
|
||
|
||
(* `e` is abstraction *)
|
||
- inversion Red.
|
||
|
||
(* `e` is morphism *)
|
||
- inversion Red.
|
||
|
||
(* `e` is Application *)
|
||
- inversion Red.
|
||
|
||
* apply T_App with (σ':=σ') (σ:=σ).
|
||
apply IHTyp1.
|
||
auto. auto. auto.
|
||
|
||
* apply T_App with (σ':=σ') (σ:=σ).
|
||
auto using IHTyp2.
|
||
auto. auto.
|
||
|
||
* apply typing_subst with (σ:=σ').
|
||
subst.
|
||
admit.
|
||
auto.
|
||
|
||
* apply typing_subst with (σ:=σ').
|
||
admit.
|
||
auto.
|
||
|
||
(* `e` is Morphism *)
|
||
- auto using T_MorphFun.
|
||
|
||
(* `e` is Ascend *)
|
||
- admit.
|
||
(*
|
||
apply IHexpr_type.
|
||
inversion Red.
|
||
*)
|
||
|
||
(* `e` is Descension *)
|
||
- intros.
|
||
apply T_DescendImplicit with (τ:=τ).
|
||
auto. auto.
|
||
|
||
(* `e` is descension *)
|
||
- apply T_DescendImplicit with (τ:=τ).
|
||
apply IHTyp.
|
||
admit.
|
||
auto.
|
||
Admitted.
|
||
|
||
(* translation of expression preserves typing *)
|
||
Lemma translation_preservation : forall Γ e e' τ,
|
||
(Γ |- e \is τ) ->
|
||
(translate_typing Γ e τ e') ->
|
||
(Γ |- e' \is τ)
|
||
.
|
||
Proof.
|
||
intros Γ e e' τ Typ Transl.
|
||
generalize dependent e'.
|
||
intros e' Transl.
|
||
induction Transl.
|
||
|
||
(* e is Variable *)
|
||
- apply H.
|
||
|
||
(* e is Let-Binding *)
|
||
- apply T_Let with (τ:=τ) (σ:=σ).
|
||
auto. auto.
|
||
|
||
- auto using T_TypeAbs.
|
||
|
||
(* e is Type-Application *)
|
||
- apply T_TypeApp.
|
||
admit.
|
||
|
||
- auto using T_Abs.
|
||
- auto using T_MorphAbs.
|
||
|
||
(* e is Application *)
|
||
- apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
|
||
auto.
|
||
apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
|
||
apply T_MorphFun.
|
||
apply morphism_path_solves_type.
|
||
auto. auto.
|
||
apply id_morphism_path.
|
||
apply id_morphism_path.
|
||
|
||
(* e is Morphism *)
|
||
- auto using T_MorphFun.
|
||
|
||
(* e is Ascension *)
|
||
- auto using T_Ascend.
|
||
|
||
(* e is Desecension *)
|
||
- apply T_Descend with (τ:=τ).
|
||
auto. auto.
|
||
Admitted.
|
||
|
||
(* e is stuck when it is neither a value, nor can it be reduced *)
|
||
Definition is_stuck (e:expr_term) : Prop :=
|
||
~(is_value e) ->
|
||
~(exists e', e -->β e')
|
||
.
|
||
|
||
(* the translation any well typed term is not stuck *)
|
||
Lemma progress :
|
||
forall Γ e τ e',
|
||
(Γ |- e \is τ) ->
|
||
(translate_typing Γ e τ e') ->
|
||
~(is_stuck e')
|
||
.
|
||
Proof.
|
||
Admitted.
|
||
|
||
|
||
|
||
(* every well-typed expression is translated,
|
||
* such that it be reduced to a value
|
||
*)
|
||
Theorem soundness :
|
||
forall Γ e e' τ,
|
||
(Γ |- e \is τ) ->
|
||
(translate_typing Γ e τ e') ->
|
||
(exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \is τ))
|
||
.
|
||
Proof.
|
||
intros.
|
||
induction H0.
|
||
|
||
(* `e` is Variable *)
|
||
- exists (expr_var x).
|
||
split. apply Multi_Refl.
|
||
split. apply V_Abs,VAbs_Var.
|
||
apply H.
|
||
|
||
(* `e` is Let-Binding *)
|
||
- exists (expr_subst x e' t').
|
||
split.
|
||
apply Multi_Step with (y:=(expr_subst x e' t')).
|
||
apply E_Let with (x:=x) (a:=e') (e:=t').
|
||
apply Multi_Refl.
|
||
admit.
|
||
(*
|
||
split.
|
||
unfold expr_subst.
|
||
induction t'.
|
||
|
||
exists (expr_subst x e' (expr_var s)).
|
||
split.
|
||
unfold expr_subst.
|
||
apply E_Let.
|
||
*)
|
||
|
||
(* `e` is Type-Abstraction *)
|
||
- exists (expr_ty_abs α e').
|
||
split.
|
||
apply Multi_Refl.
|
||
split.
|
||
apply V_Abs, VAbs_TypAbs.
|
||
apply T_TypeAbs.
|
||
apply translation_preservation with (e:=e).
|
||
apply H0.
|
||
apply H1.
|
||
|
||
(* `e` is Type-Application *)
|
||
- admit.
|
||
|
||
(* `e`is Abstraction *)
|
||
- exists (expr_abs x σ e').
|
||
split. apply Multi_Refl.
|
||
split. apply V_Abs, VAbs_Abs.
|
||
apply T_Abs.
|
||
apply translation_preservation with (e:=e).
|
||
apply H0.
|
||
apply H2.
|
||
|
||
(* `e` is Morphism Abstraction *)
|
||
- exists (expr_morph x σ e').
|
||
split. apply Multi_Refl.
|
||
split. apply V_Abs, VAbs_Morph.
|
||
apply T_MorphAbs.
|
||
apply translation_preservation with (e:=e).
|
||
apply H0.
|
||
apply H2.
|
||
|
||
(* `e` is Application *)
|
||
- admit.
|
||
|
||
(* `e` is morphism *)
|
||
- admit.
|
||
|
||
(* `e` is Ascension *)
|
||
- admit.
|
||
|
||
(* `e` is Descension *)
|
||
- admit.
|
||
Admitted.
|
||
|