From cae0572e1b2a72dec3b6e69261925e77d4b30be9 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 16 Sep 2024 15:14:53 +0200 Subject: [PATCH] wip on preservation proof --- coq/soundness.v | 399 +++++++++++++++++++++++++++++++++++++++++++++--- coq/terms.v | 55 +++---- 2 files changed, 404 insertions(+), 50 deletions(-) diff --git a/coq/soundness.v b/coq/soundness.v index 7164bd0..cbd62a9 100644 --- a/coq/soundness.v +++ b/coq/soundness.v @@ -16,40 +16,405 @@ Include Typing. Module Soundness. + +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 morphism_path_solves_type : forall Γ τ τ' m, + (translate_morphism_path Γ τ τ' m) -> + Γ |- m \is (type_morph τ τ') +. +Proof. + intros. + induction H. + + (* Sub *) + apply T_MorphAbs. + apply T_DescendImplicit with (τ:=τ). + apply T_Var. + apply C_take. + apply H. + + (* Lift *) + apply T_MorphAbs. + apply T_Ascend with (τ:=τ'). + 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 M_Sub, TSubRepr_Refl, TEq_Refl. + apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl. + + (* 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 M_Sub, TSubRepr_Refl, TEq_Refl. + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + (* 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 τ τ')). + + admit. + + apply T_MorphFun. + apply typing_weakening. + apply IHtranslate_morphism_path. + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + apply T_Var. + apply C_take. + apply M_Sub, TSubRepr_Refl, TEq_Refl. +Admitted. + +(* reduction step preserves well-typedness *) +Lemma preservation : forall Γ e e' τ, + ~(is_value e) -> + (Γ |- e \is τ) -> + (e -->β e') -> + (Γ |- e' \is τ) +. +Proof. + intros. + induction e. + + (* `e` is Variable *) + contradict H. + apply V_Abs, VAbs_Var. + + (* `e` is Type-Abstraction *) + contradict H. + apply V_Abs, VAbs_TypAbs. + + (* `e` is Type-Application *) + admit. + + (* `e` is Abstraction *) + contradict H. + apply V_Abs, VAbs_Abs. + + (* `e` is morphism *) + contradict H. + apply V_Abs, VAbs_Morph. + + (* `e` is Application *) + admit. + + (* `e` is Let-Binding *) + admit. + + (* `e` is Ascension *) + admit. + + (* `e` is Descension *) + admit. +Admitted. + +(* translation of expression preserves typing *) +Lemma translation_preservation : forall Γ e e' τ, + (Γ |- e \is τ) -> + (translate_typing Γ e τ e') -> + (Γ |- e' \is τ) +. +Proof. + intros. + induction H0. + + (* e is Variable *) + apply H. + + (* e is Let-Binding *) + apply T_Let with (τ:=τ) (σ:=σ). + apply IHtranslate_typing1. + apply H0. + apply IHtranslate_typing2. + apply H1. + + (* e is Type-Abstraction *) + apply T_TypeAbs. + apply IHtranslate_typing. + apply H0. + + (* e is Type-Application *) + admit. + + (* e is Abstraction *) + apply T_Abs. + apply IHtranslate_typing. + apply H0. + + (* e is Morphism-Abstraction *) + apply T_MorphAbs. + apply IHtranslate_typing. + apply H0. + + (* e is Application *) + apply T_App with (σ':=σ) (σ:=σ) (τ:=τ). + apply IHtranslate_typing1. + apply H0. + + induction H3. + + (* Repr-Subtype *) + apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ'). + apply T_MorphFun. + apply T_MorphAbs. + apply T_DescendImplicit with (τ:=τ0). + apply T_Var. + apply C_take. + apply H3. + + apply T_DescendImplicit with (τ:=τ0). + apply IHtranslate_typing2. + apply H1. + apply TSubRepr_Refl, TEq_Refl. + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + (* Lifted Morphism *) + apply T_App with (σ':=(type_ladder σ τ0)) (σ:=(type_ladder σ τ0)) (τ:=(type_ladder σ τ')). + apply T_MorphFun. + apply T_MorphAbs. + apply T_Ascend with (τ:=τ'). + apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ'). + apply T_MorphFun. + apply typing_weakening. + apply morphism_path_solves_type. + apply H4. + + apply T_Descend with (τ:=(type_ladder σ τ0)). + apply T_Var. + apply C_take. + + apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl. + apply M_Sub, TSubRepr_Refl, TEq_Refl. + apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl. + apply IHtranslate_typing2. + apply H1. + + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + (* argument coecrion is single function variable *) + apply T_App with (σ':= τ0) (σ:=τ0). + apply T_MorphFun. + apply T_Var. + apply H3. + apply IHtranslate_typing2. + apply H1. + (* lemma: every context implies identity morphism *) + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + (* argument coecrion is chain of coercions *) + apply T_App with (σ':=τ0) (σ:=τ0). + apply T_MorphFun. + apply T_MorphAbs. + apply T_App with (σ':=τ') (σ:=τ'). + apply T_MorphFun. + apply typing_weakening. + apply morphism_path_solves_type. + apply H3_0. + apply T_App with (σ':=τ0) (σ:=τ0). + apply T_MorphFun. + apply typing_weakening. + apply morphism_path_solves_type. + apply H3_. + apply T_Var. + apply C_take. + (* lemma: every context implies identity morphism *) + apply M_Sub, TSubRepr_Refl, TEq_Refl. + (* lemma: every context implies identity morphism *) + apply M_Sub, TSubRepr_Refl, TEq_Refl. + apply IHtranslate_typing2. + apply H1. + (* lemma: every context implies identity morphism *) + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + (* argument coercion is is map *) +(* + apply T_App with (σ':=(type_spec (type_id "Seq") τ0)) (σ:=(type_spec (type_id "Seq") τ0)). + apply T_MorphFun. + apply T_MorphAbs. + apply T_App with (σ':=(type_spec (type_id "Seq") τ0)) (σ:=(type_spec (type_id "Seq") τ0)). + apply T_App with (σ':=(type_fun τ0 τ')) (σ:=(type_fun τ0 τ')). + apply T_TypeApp with + (α:="T2"%string) + (e:=(expr_ty_app (expr_var "map") τ0)) + (τ:=(type_fun + (type_fun τ0 τ') + (type_fun + (type_spec (type_id "Seq") τ0) + (type_spec (type_id "Seq") τ')))). + + apply T_TypeApp with + (α:="T1"%string) + (e:=(expr_var "map")) + (τ:=(type_univ "T2" + (type_fun + (type_fun τ0 τ') + (type_fun + (type_spec (type_id "Seq") (type_var "T1")) + (type_spec (type_id "Seq") (type_var "T2")))))). + + apply T_Var. + admit. + + apply TSubst_VarReplace. + apply TSubst_UnivReplace. +*) + admit. + + (* argument coercion *) + apply M_Sub, TSubRepr_Refl, TEq_Refl. + + (* end case `e application` *) + + (* e is Morphism *) + apply T_MorphFun. + apply IHtranslate_typing. + apply H0. + + (* e is Ascension *) + apply T_Ascend with (τ:=τ). + apply IHtranslate_typing. + apply H0. + apply H1. + + (* e is Desecension *) + apply T_DescendImplicit with (τ:=τ). + apply IHtranslate_typing. + apply H0. + apply H1. +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') . -(* every well typed term is not stuck *) +(* the translation any well typed term is not stuck *) Lemma progress : - forall (e:expr_term), - (is_well_typed e) -> ~(is_stuck e) + forall Γ e τ e', + (Γ |- e \is τ) -> + (translate_typing Γ e τ e') -> + ~(is_stuck e') . Proof. - Admitted. -(* reduction step preserves well-typedness *) -Lemma preservation : +(* every well-typed expression is translated, + * such that it be reduced to a value + *) +Theorem soundness : forall Γ e e' τ, (Γ |- e \is τ) -> - (e -->β e') -> - (Γ |- e' \is τ) -. -Proof. -Admitted. - -(* every well-typed expression can be reduced to a value *) -Theorem soundness : - forall (e:expr_term), - (is_well_typed e) -> - (exists e', e -->β* e' /\ (is_value e')) + (translate_typing Γ e τ e') -> + (exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \is τ)) . Proof. intros. + + (* `e` is Variable *) + induction H0. + 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. +(* + split. + unfold expr_subst. + induction t'. + exists (expr_subst x e' (expr_var s)). + split. + unfold expr_subst. + apply E_Let. + *) + admit. + + (* `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. + admit. + + (* `e` is Ascension *) + admit. + + (* `e` is Descension *) + admit. Admitted. End Soundness. diff --git a/coq/terms.v b/coq/terms.v index a48ff29..1e38a9d 100644 --- a/coq/terms.v +++ b/coq/terms.v @@ -30,45 +30,34 @@ Inductive expr_term : Type := | expr_descend : type_term -> expr_term -> expr_term . -(* TODO - -Inductive type_DeBruijn : Type := - | id : nat -> type_DeBruijn - | var : nat -> type_DeBruijn - | fun : type_DeBruijn -> type_DeBruijn -> type_DeBruijn - | univ : type_DeBruijn -> type_DeBruijn - | spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn - | morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn - | ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn - -Inductive expr_DeBruijn : Type := - | var : nat -> expr_DeBruijn - | ty_abs : expr_DeBruijn -> expr_DeBruijn - | ty_app : expr_DeBruijn -> type_DeBruijn -> expr_Debruijn - | abs : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn - | morph : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn - | app : expr_DeBruijn -> expr_DeBruijn -> expr_Debruijn - | let : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn -> expr_Debruijn - | ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn - | descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -. -*) - - - (* values *) -Inductive is_value : expr_term -> Prop := - | V_Abs : forall x τ e, - (is_value (expr_abs x τ e)) +Inductive is_abs_value : expr_term -> Prop := + | VAbs_Var : forall x, + (is_abs_value (expr_var x)) - | V_TypAbs : forall τ e, - (is_value (expr_ty_abs τ e)) + | VAbs_Abs : forall x τ e, + (is_abs_value (expr_abs x τ e)) + + | VAbs_Morph : forall x τ e, + (is_abs_value (expr_morph x τ e)) + + | VAbs_TypAbs : forall τ e, + (is_abs_value (expr_ty_abs τ e)) +. + +Inductive is_value : expr_term -> Prop := + | V_Abs : forall e, + (is_abs_value e) -> + (is_value e) | V_Ascend : forall τ e, - (is_value e) -> + (is_abs_value e) -> (is_value (expr_ascend τ e)) -. + | V_Descend : forall τ e, + (is_abs_value e) -> + (is_value (expr_descend τ e)) +. Declare Scope ladder_type_scope. Declare Scope ladder_expr_scope.