From fd2c035902ce6549ef39d2a674abc5aa3f963e5a Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 19 Sep 2024 07:01:31 +0200 Subject: [PATCH] work on soundness proofs & fix bug in translate_typing --- coq/soundness.v | 391 ++++++++++++++++++++---------------------------- coq/typing.v | 4 +- 2 files changed, 163 insertions(+), 232 deletions(-) diff --git a/coq/soundness.v b/coq/soundness.v index 5558dde..346f101 100644 --- a/coq/soundness.v +++ b/coq/soundness.v @@ -19,12 +19,27 @@ Proof. - 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 [< ∀"σ",∀"τ", (%"σ"% -> %"τ"%) -> [%"σ"%] -> [%"τ"%] @@ -32,6 +47,17 @@ Lemma map_type : forall Γ, 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 τ τ') @@ -86,75 +112,100 @@ Proof. apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)). apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')). - set (k:=[< (%"σ"% -> %"τ"%) -> <$"Seq"$ %"σ"%> -> <$"Seq"$ %"τ"%> >]). - set (k1:=[< (τ -> %"τ"%) -> <$"Seq"$ τ> -> <$"Seq"$ %"τ"%> >]). - set (k2:=[< (τ -> τ') -> <$"Seq"$ τ> -> <$"Seq"$ τ'> >]). - - set (P:=(type_subst "τ" τ' k1) = k2). - -(* apply T_TypeApp with (α:="τ"%string) (τ:=k2).*) -(* apply T_TypeApp with (α:="τ"%string) (τ:=(type_subst "τ" τ' k1)).*) -(* - apply map_type. - - apply TSubst_UnivReplace. - admit. - admit. - - apply TSubst_UnivReplace. - - apply T_MorphFun. + apply specialized_map_type. apply typing_weakening. + apply T_MorphFun. 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. + 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' τ, - ~(is_value e) -> (Γ |- e \is τ) -> (e -->β e') -> (Γ |- e' \is τ) . Proof. - intros. - induction e. + intros Γ e e' τ Typ Red. + generalize dependent e'. + induction Typ; intros e' Red. (* `e` is Variable *) - contradict H. - apply V_Abs, VAbs_Var. + - inversion Red. + + (* `e` is Let *) + - inversion Red. + subst. + apply typing_subst with (σ:=σ). + auto. + auto. (* `e` is Type-Abstraction *) - contradict H. - apply V_Abs, VAbs_TypAbs. + - inversion Red. + subst. + apply T_TypeAbs. + auto. (* `e` is Type-Application *) - admit. + - inversion Red. + admit. + (* + apply typing_tsubst. + admit. + *) - (* `e` is Abstraction *) - contradict H. - apply V_Abs, VAbs_Abs. + (* `e` is abstraction *) + - inversion Red. (* `e` is morphism *) - contradict H. - apply V_Abs, VAbs_Morph. + - inversion Red. (* `e` is Application *) - admit. + - inversion Red. - (* `e` is Let-Binding *) - admit. + * apply T_App with (σ':=σ') (σ:=σ). + apply IHTyp1. + auto. auto. auto. - (* `e` is Ascension *) - admit. + * 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 *) - admit. + - intros. + apply T_DescendImplicit with (τ:=τ). + auto. auto. + + (* `e` is descension *) + - apply T_DescendImplicit with (τ:=τ). + apply IHTyp. + admit. + auto. Admitted. (* translation of expression preserves typing *) @@ -164,170 +215,46 @@ Lemma translation_preservation : forall Γ e e' τ, (Γ |- e' \is τ) . Proof. - intros. - induction H0. + intros Γ e e' τ Typ Transl. + generalize dependent e'. + intros e' Transl. + induction Transl. (* e is Variable *) - apply H. + - apply H. (* e is Let-Binding *) - apply T_Let with (τ:=τ) (σ:=σ). - apply IHtranslate_typing1. - apply H0. - apply IHtranslate_typing2. - apply H1. + - apply T_Let with (τ:=τ) (σ:=σ). + auto. auto. - (* e is Type-Abstraction *) - apply T_TypeAbs. - apply IHtranslate_typing. - apply H0. + - auto using T_TypeAbs. (* e is Type-Application *) - admit. + - apply T_TypeApp. + admit. - (* e is Abstraction *) - apply T_Abs. - apply IHtranslate_typing. - apply H0. - - (* e is Morphism-Abstraction *) - apply T_MorphAbs. - apply IHtranslate_typing. - apply H0. + - auto using T_Abs. + - auto using T_MorphAbs. (* e is Application *) - apply T_App with (σ':=σ) (σ:=σ) (τ:=τ). - apply IHtranslate_typing1. - apply H0. - - induction H3. - - (* Repr-Subtype *) - apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ'). + - apply T_App with (σ':=σ) (σ:=σ) (τ:=τ). + auto. + apply T_App with (σ':=σ') (σ:=σ') (τ:=σ). apply T_MorphFun. - apply T_MorphAbs. - apply T_Descend 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 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` *) + auto. auto. + apply id_morphism_path. + apply id_morphism_path. (* e is Morphism *) - apply T_MorphFun. - apply IHtranslate_typing. - apply H0. + - auto using T_MorphFun. (* e is Ascension *) - apply T_Ascend. - apply IHtranslate_typing. - apply H0. + - auto using T_Ascend. (* e is Desecension *) - apply T_Descend with (τ:=τ). - apply IHtranslate_typing. - apply H0. - apply H1. + - apply T_Descend with (τ:=τ). + auto. auto. Admitted. (* e is stuck when it is neither a value, nor can it be reduced *) @@ -346,6 +273,8 @@ Lemma progress : Proof. Admitted. + + (* every well-typed expression is translated, * such that it be reduced to a value *) @@ -357,20 +286,21 @@ Theorem soundness : . Proof. intros. + induction H0. (* `e` is Variable *) - induction H0. - exists (expr_var x). - split. apply Multi_Refl. - split. apply V_Abs,VAbs_Var. - apply H. + - 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. + - 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. @@ -381,48 +311,49 @@ Proof. 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. + - 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. + - 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. + - 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. + - 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. + - admit. + + (* `e` is morphism *) + - admit. (* `e` is Ascension *) - admit. + - admit. (* `e` is Descension *) - admit. + - admit. Admitted. diff --git a/coq/typing.v b/coq/typing.v index 8f1a845..e133988 100644 --- a/coq/typing.v +++ b/coq/typing.v @@ -101,9 +101,9 @@ Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> P (Γ |- e \is (type_univ α τ)) -> (translate_typing Γ e τ e') -> (translate_typing Γ - [{ e # τ }] + [{ e # σ }] (type_subst α σ τ) - [{ e' # τ }]) + [{ e' # σ }]) | Expand_Abs : forall Γ x σ e e' τ, ((ctx_assign x σ Γ) |- e \is τ) ->