From ac63139c67643b7b230a22f2ab53801eb03417e7 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 24 Sep 2024 04:28:41 +0200 Subject: [PATCH] add preconditions of expr_lc in eval; use coinductive quantification in T_TypeAbs --- coq/_CoqProject | 1 + coq/lemmas/typing_regular.v | 46 ++++++++ coq/soundness/translate_morph.v | 180 ++++++++++++++++++++++++-------- coq/terms/eval.v | 14 +-- coq/typing/morph.v | 12 ++- coq/typing/subtype.v | 1 + coq/typing/typing.v | 23 ++-- 7 files changed, 214 insertions(+), 63 deletions(-) create mode 100644 coq/lemmas/typing_regular.v diff --git a/coq/_CoqProject b/coq/_CoqProject index 8a245a8..b925f8f 100644 --- a/coq/_CoqProject +++ b/coq/_CoqProject @@ -16,6 +16,7 @@ typing/morph.v typing/typing.v lemmas/subst_lemmas.v lemmas/typing_weakening.v +lemmas/typing_regular.v soundness/translate_morph.v diff --git a/coq/lemmas/typing_regular.v b/coq/lemmas/typing_regular.v new file mode 100644 index 0000000..24a8b63 --- /dev/null +++ b/coq/lemmas/typing_regular.v @@ -0,0 +1,46 @@ +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 typing. + + +Lemma type_lc_sub : forall τ1 τ2, + type_lc τ1 -> + τ1 :<= τ2 -> + type_lc τ2 +. +Proof. + intros. +Admitted. + +Lemma type_morph_lc_inv : forall τ1 τ2, + type_lc (ty_morph τ1 τ2) -> + type_lc τ1 /\ type_lc τ2 +. +Proof. + intros. + inversion H. + auto. +Qed. + +Lemma typing_regular_expr_lc : forall Γ e τ, + (Γ |- e \is τ) -> + expr_lc e. +Proof. + intros Γ e τ H. + induction H; eauto. + - apply Elc_Var. + - apply Elc_Let with (L:=L). + apply IHtyping. +Admitted. + +Lemma typing_regular_type_lc : forall Γ e τ, + (Γ |- e \is τ) -> + type_lc τ. +Proof. +Admitted. diff --git a/coq/soundness/translate_morph.v b/coq/soundness/translate_morph.v index cc6ba26..5c908d5 100644 --- a/coq/soundness/translate_morph.v +++ b/coq/soundness/translate_morph.v @@ -8,6 +8,7 @@ Require Import env. Require Import morph. Require Import subst_lemmas. Require Import typing. +Require Import typing_regular. Require Import typing_weakening. @@ -35,18 +36,52 @@ Proof. *) Admitted. +Lemma type_lc_spec_inv : forall τ, + type_lc [< [τ] >] -> + type_lc τ +. +Proof. +Admitted. + +Lemma type_lc_ladder_inv2 : forall σ τ, + type_lc [< σ ~ τ >] -> + type_lc τ +. +Proof. +Admitted. + +Lemma morph_regular_lc : forall Γ τ τ', + env_wf Γ -> + type_lc τ -> + (Γ |- τ ~~> τ') -> + type_lc τ' +. +Proof. + intros. + induction H1. + - apply type_lc_sub with (τ1:=τ). + assumption. + assumption. +Admitted. + +Lemma morph_path_inv : forall Γ τ τ' m, + (Γ |- [[ τ ~~> τ' ]] = m) -> + (Γ |- τ ~~> τ') +. +Proof. +Admitted. + (* * translated morphism path is locally closed *) -Lemma morphism_path_lc : forall Γ τ τ' m, +Lemma morph_path_lc : forall Γ τ τ' m, type_lc τ -> - type_lc τ' -> env_wf Γ -> (Γ |- [[ τ ~~> τ' ]] = m) -> expr_lc m . Proof. - intros Γ τ τ' m Wfτ1 Wfτ2 WfEnv H. + intros Γ τ τ' m Wfτ WfEnv H. induction H. (* Subtype / Identity *) @@ -56,6 +91,8 @@ Proof. unfold expr_open. simpl. apply Elc_Descend. + apply type_lc_sub with (τ1:=τ). + assumption. assumption. apply Elc_Var. @@ -66,22 +103,20 @@ Proof. unfold expr_open. simpl. apply Elc_Ascend. - inversion Wfτ1; assumption. + inversion Wfτ; assumption. apply Elc_App. rewrite expr_open_lc. apply IHtranslate_morphism_path. - inversion Wfτ1; assumption. - inversion Wfτ2; assumption. - assumption. + inversion Wfτ; assumption. + inversion Wfτ; assumption. apply IHtranslate_morphism_path. - inversion Wfτ1; assumption. - inversion Wfτ2; assumption. - assumption. + inversion Wfτ; assumption. + inversion Wfτ; assumption. apply Elc_Descend, Elc_Var. - inversion Wfτ1; assumption. + inversion Wfτ; assumption. (* Single Morphism *) - apply Elc_Var. @@ -95,16 +130,35 @@ Proof. apply Elc_App. rewrite expr_open_lc. apply IHtranslate_morphism_path2. - 1-3:assumption. + + + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). + assumption. assumption. + apply morph_path_inv with (m:=m1), H. + assumption. + apply IHtranslate_morphism_path2. - 1-3:assumption. + + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). + assumption. assumption. + apply morph_path_inv with (m:=m1), H. + assumption. + apply Elc_App. rewrite expr_open_lc. apply IHtranslate_morphism_path1. - 1-3:assumption. + + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). + assumption. assumption. + apply id_morphism_path. + assumption. + assumption. + apply IHtranslate_morphism_path1. - 1-3:assumption. + assumption. + assumption. + apply Elc_Var. (* Map *) @@ -118,17 +172,21 @@ Proof. 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. + apply type_lc_spec_inv; assumption. + apply morph_path_inv in H. + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). assumption. + apply type_lc_spec_inv; assumption. + assumption. + rewrite expr_open_lc. + apply IHtranslate_morphism_path. - inversion Wfτ1; assumption. - inversion Wfτ2; assumption. + apply type_lc_spec_inv; assumption. + assumption. + + apply IHtranslate_morphism_path. + apply type_lc_spec_inv; assumption. assumption. Qed. @@ -137,13 +195,12 @@ Qed. *) 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. + intros Γ τ τ' m Lcτ WfEnv H. induction H. (* Sub *) @@ -153,7 +210,8 @@ Proof. simpl. apply T_Descend with (τ:=τ). apply T_Var. - 2:assumption. + apply env_wf_type. + 1-3,5:assumption. simpl_env. apply binds_head, binds_singleton. @@ -167,6 +225,7 @@ Proof. 2: { apply T_Descend with (τ:=[< σ ~ τ >]). apply T_Var. + apply env_wf_type; assumption. simpl_env. unfold binds. simpl. destruct (x==x). @@ -177,20 +236,27 @@ Proof. apply equiv.TEq_Refl. } - inversion Lcτ1. - inversion Lcτ2. - subst. - apply morphism_path_lc in H0. - + inversion Lcτ; subst. rewrite expr_open_lc. apply typing_weakening with (Γ':=(x,[< σ ~ τ >])::[]). apply T_MorphFun. apply IHtranslate_morphism_path. - 4: apply env_wf_type. + apply type_lc_ladder_inv2 with (σ:=σ); assumption; assumption. + assumption. + apply env_wf_type. + assumption. + assumption. + assumption. + apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ'). + assumption. + assumption. + assumption. + apply type_lc_ladder_inv2 with (σ:=σ). all: assumption. (* Single *) - apply T_Var. + assumption. apply H. (* Chain *) @@ -205,24 +271,38 @@ Proof. rewrite expr_open_lc. simpl_env; apply typing_weakening. apply IHtranslate_morphism_path2. + + apply morph_path_inv in H. + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). 1-3: assumption. + + assumption. apply env_wf_type. 1-3: assumption. - apply morphism_path_lc with (Γ:=Γ) (τ:=τ') (τ':=τ''). - 1-4: assumption. + apply morph_path_lc with (Γ:=Γ) (τ:=τ') (τ':=τ''). + 2-3: assumption. + apply morph_path_inv in H. + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). + all: 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. + 3: apply env_wf_type. + 1-5: assumption. + apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ'). + 1-3: assumption. apply T_Var. + apply env_wf_type; assumption. 2: apply id_morphism_path. simpl_env; apply binds_head, binds_singleton. + assumption. + + * apply morph_path_inv in H. + apply morph_regular_lc with (Γ:=Γ) (τ:=τ). + all: assumption. (* Map Sequence *) - apply T_MorphAbs with (L:=dom Γ). @@ -239,14 +319,24 @@ Proof. 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. + 2: assumption. + 2: apply env_wf_type; assumption. + + inversion Lcτ; assumption. + apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ'). + inversion Lcτ; assumption. 1-2: assumption. + apply Tlc_Func. + apply type_lc_spec_inv; assumption. + + apply morph_path_inv in H. + apply morph_regular_lc in H. + assumption. + assumption. + apply type_lc_spec_inv; assumption. + apply T_Var. + apply env_wf_type; assumption. simpl_env; apply binds_head, binds_singleton. + assumption. Qed. diff --git a/coq/terms/eval.v b/coq/terms/eval.v index 506b32c..4b7c352 100644 --- a/coq/terms/eval.v +++ b/coq/terms/eval.v @@ -10,9 +10,11 @@ Open Scope ladder_expr_scope. Inductive is_value : expr_DeBruijn -> Prop := | V_TAbs : forall e, + expr_lc [{ Λ e }] -> is_value [{ Λ e }] | V_Abs : forall σ e, + expr_lc [{ λ σ ↦ e }] -> is_value [{ λ σ ↦ e }] | V_Morph : forall σ e, @@ -32,6 +34,7 @@ Reserved Notation " s '-->eval' t " (at level 40). Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop := | E_App1 : forall e1 e1' e2, + (expr_lc e2) -> e1 -->eval e1' -> [{ e1 e2 }] -->eval [{ e1' e2 }] @@ -41,27 +44,26 @@ Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop := [{ v1 e2 }] -->eval [{ v1 e2' }] | E_TypApp : forall e e', + expr_lc [{ Λ e }] -> e -->eval e' -> [{ Λ e }] -->eval [{ Λ e' }] | E_TypAppLam : forall e τ, + expr_lc [{ (Λ e ) }] -> [{ (Λ e) # τ }] -->eval (expr_open_type τ e) | E_AppLam : forall τ e a, + expr_lc [{ (λ τ ↦ e) }] -> [{ (λ τ ↦ e) a }] -->eval (expr_open a e) | E_AppMorph : forall τ e a, + expr_lc [{ (λ τ ↦morph e) }] -> [{ (λ τ ↦morph e) a }] -->eval (expr_open a e) | E_Let : forall e a, + expr_lc [{ let a in e }] -> [{ let a in e }] -->eval (expr_open a e) - | E_StripAscend : forall τ e, - [{ e as τ }] -->eval e - - | E_StripDescend : forall τ e, - [{ e des τ }] -->eval e - | E_Ascend : forall τ e e', (e -->eval e') -> [{ e as τ }] -->eval [{ e' as τ }] diff --git a/coq/typing/morph.v b/coq/typing/morph.v index f058826..b7dd49a 100644 --- a/coq/typing/morph.v +++ b/coq/typing/morph.v @@ -16,6 +16,7 @@ Reserved Notation "Γ '|-' σ '~~>' τ" (at level 101). Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop := | M_Sub : forall Γ τ τ', + type_lc τ -> τ :<= τ' -> (Γ |- τ ~~> τ') @@ -38,10 +39,14 @@ Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop := where "Γ '|-' s '~~>' t" := (morphism_path Γ s t). -Lemma id_morphism_path : forall Γ τ, Γ |- τ ~~> τ. +Create HintDb morph_path_hints. +Hint Constructors morphism_path :morph_path_hints. + +Lemma id_morphism_path : forall Γ τ, + type_lc τ -> + Γ |- τ ~~> τ. Proof. - intros. - apply M_Sub, TSubRepr_Refl, TEq_Refl. + eauto with morph_path_hints subtype_hints. Qed. @@ -68,7 +73,6 @@ Inductive translate_morphism_path : env -> type_DeBruijn -> type_DeBruijn -> exp (Γ |- [[ τ ~~> τ' ]] = [{ $h }]) | Translate_Chain : forall Γ τ τ' τ'' m1 m2, - (type_lc τ') -> (Γ |- [[ τ ~~> τ' ]] = m1) -> (Γ |- [[ τ' ~~> τ'' ]] = m2) -> (Γ |- [[ τ ~~> τ'' ]] = [{ λ τ ↦morph (m2 (m1 %0)) }]) diff --git a/coq/typing/subtype.v b/coq/typing/subtype.v index b86c38b..18d9679 100644 --- a/coq/typing/subtype.v +++ b/coq/typing/subtype.v @@ -37,6 +37,7 @@ where "s '~<=' t" := (is_conv_subtype s t). Hint Constructors is_repr_subtype :subtype_hints. Hint Constructors is_conv_subtype :subtype_hints. +Hint Constructors type_eq :subtype_hints. (* Every Representational Subtype is a Convertible Subtype *) diff --git a/coq/typing/typing.v b/coq/typing/typing.v index 6decf89..12e9549 100644 --- a/coq/typing/typing.v +++ b/coq/typing/typing.v @@ -13,6 +13,7 @@ Open Scope ladder_expr_scope. Reserved Notation "Γ '|-' x '\is' X" (at level 101). Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop := | T_Var : forall Γ x τ, + (env_wf Γ) -> (binds x τ Γ) -> (Γ |- [{ $x }] \is τ) @@ -22,8 +23,9 @@ Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop := ( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) -> (Γ |- [{ let s in t }] \is τ) - | T_TypeAbs : forall Γ e τ, - (Γ |- e \is τ) -> + | T_TypeAbs : forall Γ L e τ, + (forall x : atom, x `notin` L -> + ( Γ |- (expr_open_type (ty_fvar x) e) \is τ)) -> (Γ |- [{ Λ e }] \is [< ∀ τ >]) | T_TypeApp : forall Γ e σ τ, @@ -67,6 +69,9 @@ Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop := where "Γ '|-' x '\is' τ" := (typing Γ x τ). +Create HintDb typing_hints. +Hint Constructors typing :typing_hints. + Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f" (at level 101). @@ -80,14 +85,16 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru (Γ |- e \is σ) -> (forall x : atom, x `notin` L -> ( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ) -> - ( (x,σ)::Γ |- [[ t \is τ ]] = t' ) + ( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) t) \is τ ]] = (expr_open (ex_fvar x) t') ) ) -> (Γ |- [[ e \is σ ]] = e') -> (Γ |- [[ [{ let e in t }] \is τ ]] = [{ let e' in t' }]) - | Expand_TypeAbs : forall Γ e e' τ, - (Γ |- e \is τ) -> - (Γ |- [[ e \is τ ]] = e') -> + | Expand_TypeAbs : forall Γ L e e' τ, + (forall x : atom, x `notin` L -> + (Γ |- (expr_open_type (ty_fvar x) e) \is τ) -> + (Γ |- [[ (expr_open_type (ty_fvar x) e) \is τ ]] = (expr_open_type (ty_fvar x) e')) + ) -> (Γ |- [[ [{ Λ e }] \is [< ∀ τ >] ]] = [{ Λ e' }]) | Expand_TypeApp : forall Γ e e' σ τ, @@ -99,7 +106,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) -> (forall x : atom, x `notin` L -> ( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) -> - ( (x,σ)::Γ |- [[ e \is τ ]] = e' ) + ( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) e) \is τ ]] = (expr_open (ex_fvar x) e') ) ) -> (Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }]) @@ -107,7 +114,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) -> (forall x : atom, x `notin` L -> ( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) -> - ( (x,σ)::Γ |- [[ e \is τ ]] = e' ) + ( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) e) \is τ ]] = (expr_open (ex_fvar x) e') ) ) -> (Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }])