diff --git a/coq/_CoqProject b/coq/_CoqProject index 139d674..ec84ead 100644 --- a/coq/_CoqProject +++ b/coq/_CoqProject @@ -1,28 +1,17 @@ -R . LadderTypes -AdditionalTactics.v -ListFacts.v -FiniteSets.v -FSetNotin.v -Atom.v -Metatheory.v +metatheory/AdditionalTactics.v +metatheory/ListFacts.v +metatheory/FiniteSets.v +metatheory/FSetNotin.v +metatheory/Atom.v +metatheory/Metatheory.v -terms_debruijn.v -equiv_debruijn.v -subtype_debruijn.v -context_debruijn.v -morph_debruijn.v -typing_debruijn.v -eval_debruijn.v -subst_lemmas_debruijn.v +terms/debruijn.v +terms/equiv.v +terms/eval.v +typing/context.v +typing/subtype.v +typing/morph.v +typing/typing.v +lemmas/subst_lemmas.v - -terms.v -equiv.v -subst.v -subtype.v -context.v -morph.v -typing.v -smallstep.v -soundness.v -bbencode.v diff --git a/coq/context.v b/coq/context.v deleted file mode 100644 index 88e8cc3..0000000 --- a/coq/context.v +++ /dev/null @@ -1,15 +0,0 @@ -From Coq Require Import Strings.String. -Require Import terms. - - -Inductive context : Type := - | ctx_assign : string -> type_term -> context -> context - | ctx_empty : context -. - -Inductive context_contains : context -> string -> type_term -> Prop := - | C_take : forall (x:string) (X:type_term) (Γ:context), - (context_contains (ctx_assign x X Γ) x X) - | C_shuffle : forall x X y Y Γ, - (context_contains Γ x X) -> - (context_contains (ctx_assign y Y Γ) x X). diff --git a/coq/equiv.v b/coq/equiv.v deleted file mode 100644 index 09c735e..0000000 --- a/coq/equiv.v +++ /dev/null @@ -1,423 +0,0 @@ -(* This module defines an equivalence relation - * on type-terms. - * - * In general, we want distributivity of ladders - * over all other type constructors, e.g. type- - * specializations or function-types. - * - * Formally, we define two rewrite rules that - * shall define how we are able to rewrite type-terms - * such that they remain equivalent. - * - * (1) `-->distribute-ladder` which distributes - * ladder types over other type constructors, e.g. - * -->distribute-ladder ~ . - * - * (2) `-->condense-ladder` which does the - * inverse operation, e.g. - * ~ -->condense-ladder - * - * When applied exhaustively, each rewrite rule yields - * a normal form, namely *Ladder Normal Form (LNF)*, which - * is reached by exhaustive application of `-->distribute-ladder`, - * and *Parameter Normal Form (PNF)*, which is reached by exhaustive - * application of `-->condense-ladder`. - * - * The equivalence relation `===` over type-terms is then defined - * as the reflexive and transitive hull over `-->distribute-ladder` - * and `-->condense-ladder`. Since the latter two are the inverse - * rewrite-step of each other, `===` is symmetric and thus `===` - * satisfies all properties required of an equivalence relation. - *) - -Require Import terms. -Require Import subst. -From Coq Require Import Strings.String. - -(** Alpha conversion in types *) - -Reserved Notation "S '--->α' T" (at level 40). -Inductive type_conv_alpha : type_term -> type_term -> Prop := - | TAlpha_Rename : forall x y t, - (type_univ x t) --->α (type_univ y (type_subst x (type_var y) t)) - - | TAlpha_SubUniv : forall x τ τ', - (τ --->α τ') -> - [< ∀x,τ >] --->α [< ∀x,τ' >] - - | TAlpha_SubSpec1 : forall τ1 τ1' τ2, - (τ1 --->α τ1') -> - [< <τ1 τ2> >] --->α [< <τ1' τ2> >] - - | TAlpha_SubSpec2 : forall τ1 τ2 τ2', - (τ2 --->α τ2') -> - [< <τ1 τ2> >] --->α [< <τ1 τ2'> >] - - | TAlpha_SubFun1 : forall τ1 τ1' τ2, - (τ1 --->α τ1') -> - [< τ1 -> τ2 >] --->α [< τ1' -> τ2 >] - - | TAlpha_SubFun2 : forall τ1 τ2 τ2', - (τ2 --->α τ2') -> - [< τ1 -> τ2 >] --->α [< τ1 -> τ2' >] - - | TAlpha_SubMorph1 : forall τ1 τ1' τ2, - (τ1 --->α τ1') -> - [< τ1 ->morph τ2 >] --->α [< τ1' ->morph τ2 >] - - | TAlpha_SubMorph2 : forall τ1 τ2 τ2', - (τ2 --->α τ2') -> - [< τ1 ->morph τ2 >] --->α [< τ1 ->morph τ2' >] - - | TAlpha_SubLadder1 : forall τ1 τ1' τ2, - (τ1 --->α τ1') -> - [< τ1 ~ τ2 >] --->α [< τ1' ~ τ2 >] - - | TAlpha_SubLadder2 : forall τ1 τ2 τ2', - (τ2 --->α τ2') -> - [< τ1 ~ τ2 >] --->α [< τ1 ~ τ2' >] - -where "S '--->α' T" := (type_conv_alpha S T). - -(** Alpha conversion is symmetric *) -Lemma type_alpha_symm : - forall σ τ, - (σ --->α τ) -> (τ --->α σ). -Proof. - intros. - induction H. - - admit. - - auto using TAlpha_Rename,type_subst,type_subst_symm, TAlpha_SubUniv. - - auto using TAlpha_SubSpec1. - - auto using TAlpha_SubSpec2. - - auto using TAlpha_SubFun1. - - auto using TAlpha_SubFun2. - - auto using TAlpha_SubMorph1. - - auto using TAlpha_SubMorph2. - - auto using TAlpha_SubLadder1. - - auto using TAlpha_SubLadder2. -Admitted. - -(** Define all rewrite steps $\label{coq:type-dist}$ *) - -Reserved Notation "S '-->distribute-ladder' T" (at level 40). -Inductive type_distribute_ladder : type_term -> type_term -> Prop := - | L_DistributeOverSpec1 : forall x x' y, - [< >] - -->distribute-ladder - [< ~ >] - - | L_DistributeOverSpec2 : forall x y y', - [< >] - -->distribute-ladder - [< ~ >] - - | L_DistributeOverFun1 : forall x x' y, - [< (x~x' -> y) >] - -->distribute-ladder - [< (x -> y) ~ (x' -> y) >] - - | L_DistributeOverFun2 : forall x y y', - [< (x -> y~y') >] - -->distribute-ladder - [< (x -> y) ~ (x -> y') >] - - | L_DistributeOverMorph1 : forall x x' y, - [< (x~x' ->morph y) >] - -->distribute-ladder - [< (x ->morph y) ~ (x' ->morph y) >] - - | L_DistributeOverMorph2 : forall x y y', - (type_morph x (type_ladder y y')) - -->distribute-ladder - (type_ladder (type_morph x y) (type_morph x y')) - -where "S '-->distribute-ladder' T" := (type_distribute_ladder S T). - - - -Reserved Notation "S '-->condense-ladder' T" (at level 40). -Inductive type_condense_ladder : type_term -> type_term -> Prop := - | L_CondenseOverSpec1 : forall x x' y, - [< ~ >] - -->condense-ladder - [< >] - - | L_CondenseOverSpec2 : forall x y y', - [< ~ >] - -->condense-ladder - [< >] - - | L_CondenseOverFun1 : forall x x' y, - [< (x -> y) ~ (x' -> y) >] - -->condense-ladder - [< (x~x') -> y >] - - | L_CondenseOverFun2 : forall x y y', - [< (x -> y) ~ (x -> y') >] - -->condense-ladder - [< (x -> y~y') >] - - | L_CondenseOverMorph1 : forall x x' y, - [< (x ->morph y) ~ (x' ->morph y) >] - -->condense-ladder - [< (x~x' ->morph y) >] - - | L_CondenseOverMorph2 : forall x y y', - [< (x ->morph y) ~ (x ->morph y') >] - -->condense-ladder - [< (x ->morph y~y') >] - -where "S '-->condense-ladder' T" := (type_condense_ladder S T). - - -(** Inversion Lemma: - `-->distribute-ladder` is the inverse of `-->condense-ladder -*) -Lemma distribute_inverse : - forall x y, - x -->distribute-ladder y -> - y -->condense-ladder x. -Proof. - intros. - destruct H. - apply L_CondenseOverSpec1. - apply L_CondenseOverSpec2. - apply L_CondenseOverFun1. - apply L_CondenseOverFun2. - apply L_CondenseOverMorph1. - apply L_CondenseOverMorph2. -Qed. - -(** Inversion Lemma: - `-->condense-ladder` is the inverse of `-->distribute-ladder` -*) -Lemma condense_inverse : - forall x y, - x -->condense-ladder y -> - y -->distribute-ladder x. -Proof. - intros. - destruct H. - apply L_DistributeOverSpec1. - apply L_DistributeOverSpec2. - apply L_DistributeOverFun1. - apply L_DistributeOverFun2. - apply L_DistributeOverMorph1. - apply L_DistributeOverMorph2. -Qed. - - -(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *) - -Reserved Notation " S '===' T " (at level 40). -Inductive type_eq : type_term -> type_term -> Prop := - | TEq_Refl : forall x, - x === x - - | TEq_Trans : forall x y z, - x === y -> - y === z -> - x === z - - | TEq_SubFun : forall x x' y y', - x === x' -> - y === y' -> - [< x -> y >] === [< x' -> y' >] - - | TEq_SubMorph : forall x x' y y', - x === x' -> - y === y' -> - [< x ->morph y >] === [< x' ->morph y' >] - - | TEq_LadderAssocLR : forall x y z, - [< (x~y)~z >] - === - [< x~(y~z) >] - - | TEq_LadderAssocRL : forall x y z, - [< x~(y~z) >] - === - [< (x~y)~z >] - - | TEq_Alpha : forall x y, - x --->α y -> - x === y - - | TEq_Distribute : forall x y, - x -->distribute-ladder y -> - x === y - - | TEq_Condense : forall x y, - x -->condense-ladder y -> - x === y - -where "S '===' T" := (type_eq S T). - - - -(** Symmetry of === *) -Lemma TEq_Symm : - forall x y, - (x === y) -> (y === x). -Proof. - intros. - induction H. - - apply TEq_Refl. - - apply TEq_Trans with (y:=y). - apply IHtype_eq2. - apply IHtype_eq1. - - apply TEq_SubFun. - auto. auto. - apply TEq_SubMorph. - auto. auto. - apply TEq_LadderAssocRL. - apply TEq_LadderAssocLR. - - apply type_alpha_symm in H. - apply TEq_Alpha. - apply H. - - apply TEq_Condense. - apply distribute_inverse. - apply H. - - apply TEq_Distribute. - apply condense_inverse. - apply H. -Qed. - -(** "flat" types do not contain ladders $\label{coq:type-flat}$ *) -Inductive type_is_flat : type_term -> Prop := - | FlatVar : forall x, (type_is_flat (type_var x)) - | FlatId : forall x, (type_is_flat (type_id x)) - | FlatApp : forall x y, - (type_is_flat x) -> - (type_is_flat y) -> - (type_is_flat (type_spec x y)) - - | FlatFun : forall x y, - (type_is_flat x) -> - (type_is_flat y) -> - (type_is_flat (type_fun x y)) - - | FlatSub : forall x v, - (type_is_flat x) -> - (type_is_flat (type_univ v x)) -. - -(** Ladder Normal Form: - exhaustive application of -->distribute-ladder - *) -Inductive type_is_lnf : type_term -> Prop := - | LNF : forall x : type_term, - (not (exists y:type_term, x -->distribute-ladder y)) - -> (type_is_lnf x) -. - -(** Parameter Normal Form: - exhaustive application of -->condense-ladder -*) -Inductive type_is_pnf : type_term -> Prop := - | PNF : forall x : type_term, - (not (exists y:type_term, x -->condense-ladder y)) - -> (type_is_pnf x) -. - -(** Any term in LNF either is flat, or is a ladder T1~T2 where T1 is flat and T2 is in LNF *) -Lemma lnf_shape : - forall τ:type_term, - (type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_ladder τ1 τ2) /\ (type_is_flat τ1) /\ (type_is_lnf τ2))) -. -Proof. - intros τ H. - induction τ. - - left. - apply FlatId. - - left. - apply FlatVar. -(* - left. - apply IHτ1 in H. - apply FlatFun. - apply H. - destruct H. - destruct H. - - apply IHτ1. -*) - admit. - admit. - admit. - admit. -Admitted. - -(** every type has an equivalent LNF *) -Lemma lnf_normalizing : - forall t, exists t', (t === t') /\ (type_is_lnf t'). -Proof. - intros. - destruct t. - - exists (type_id s). - split. apply TEq_Refl. - apply LNF. - admit. - admit. - admit. - - exists (type_univ s t). - split. - apply TEq_Refl. - apply LNF. - -Admitted. - -(** every type has an equivalent PNF *) -Lemma pnf_normalizing : - forall t, exists t', (t === t') /\ (type_is_pnf t'). -Proof. -Admitted. - -Lemma lnf_uniqueness : - forall t t' t'', - (t === t') /\ (type_is_lnf t') /\ (t === t'') /\ (type_is_lnf t'') - -> t = t'. -Proof. -Admitted. - - - - - -(** - * Examples - *) - -Example example_flat_type : - type_is_flat [< <$"PosInt"$ $"10"$> >]. -Proof. - apply FlatApp. - apply FlatId. - apply FlatId. -Qed. - -Example example_lnf_type : - type_is_lnf [< [$"Char"$] ~ [$"Byte"$] >]. -Proof. -Admitted. - -Example example_type_eq : - [< [$"Char"$ ~ $"Byte"$] >] - === - [< [$"Char"$] ~ [$"Byte"$] >] -. -Proof. - apply TEq_Distribute. - apply L_DistributeOverSpec2. -Qed. diff --git a/coq/bbencode.v b/coq/examples/bbencode.v similarity index 100% rename from coq/bbencode.v rename to coq/examples/bbencode.v diff --git a/coq/subst_lemmas_debruijn.v b/coq/lemmas/subst_lemmas.v similarity index 99% rename from coq/subst_lemmas_debruijn.v rename to coq/lemmas/subst_lemmas.v index a3a5b53..5a2b339 100644 --- a/coq/subst_lemmas_debruijn.v +++ b/coq/lemmas/subst_lemmas.v @@ -1,7 +1,7 @@ -Require Import terms_debruijn. Require Import Atom. Require Import Metatheory. Require Import FSetNotin. +Require Import debruijn. (* * Substitution has no effect if the variable is not free diff --git a/coq/AdditionalTactics.v b/coq/metatheory/AdditionalTactics.v similarity index 100% rename from coq/AdditionalTactics.v rename to coq/metatheory/AdditionalTactics.v diff --git a/coq/Atom.v b/coq/metatheory/Atom.v similarity index 100% rename from coq/Atom.v rename to coq/metatheory/Atom.v diff --git a/coq/FSetNotin.v b/coq/metatheory/FSetNotin.v similarity index 100% rename from coq/FSetNotin.v rename to coq/metatheory/FSetNotin.v diff --git a/coq/FiniteSets.v b/coq/metatheory/FiniteSets.v similarity index 100% rename from coq/FiniteSets.v rename to coq/metatheory/FiniteSets.v diff --git a/coq/ListFacts.v b/coq/metatheory/ListFacts.v similarity index 100% rename from coq/ListFacts.v rename to coq/metatheory/ListFacts.v diff --git a/coq/Metatheory.v b/coq/metatheory/Metatheory.v similarity index 100% rename from coq/Metatheory.v rename to coq/metatheory/Metatheory.v diff --git a/coq/morph.v b/coq/morph.v deleted file mode 100644 index 4202d4a..0000000 --- a/coq/morph.v +++ /dev/null @@ -1,92 +0,0 @@ -From Coq Require Import Strings.String. -Require Import terms. -Require Import subst. -Require Import equiv. -Require Import subtype. -Require Import context. - -(* Given a context, there is a morphism path from τ to τ' *) -Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level). - -Open Scope ladder_expr_scope. - -Inductive morphism_path : context -> type_term -> type_term -> Prop := - | M_Sub : forall Γ τ τ', - (τ :<= τ') -> - (Γ |- τ ~> τ') - - | M_Single : forall Γ h τ τ', - (context_contains Γ h [< τ ->morph τ' >]) -> - (Γ |- τ ~> τ') - - | M_Chain : forall Γ τ τ' τ'', - (Γ |- τ ~> τ') -> - (Γ |- τ' ~> τ'') -> - (Γ |- τ ~> τ'') - - | M_Lift : forall Γ σ τ τ', - (Γ |- τ ~> τ') -> - (Γ |- [< σ ~ τ >] ~> [< σ ~ τ' >]) - - | M_MapSeq : forall Γ τ τ', - (Γ |- τ ~> τ') -> - (Γ |- [< [τ] >] ~> [< [τ'] >]) - -where "Γ '|-' s '~>' t" := (morphism_path Γ s t). - -Lemma id_morphism_path : forall Γ τ, Γ |- τ ~> τ. -Proof. - intros. - apply M_Sub, TSubRepr_Refl, TEq_Refl. -Qed. - -Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop := - | Translate_Descend : forall Γ τ τ', - (τ :<= τ') -> - (translate_morphism_path Γ τ τ' - (expr_morph "x" τ [{ %"x"% des τ' }])) - - | Translate_Lift : forall Γ σ τ τ' m, - (Γ |- τ ~> τ') -> - (translate_morphism_path Γ τ τ' m) -> - (translate_morphism_path Γ [< σ ~ τ >] [< σ ~ τ' >] - (expr_morph "x" [< σ ~ τ >] [{ (m (%"x"% des τ)) as σ }])) - - | Translate_Single : forall Γ h τ τ', - (context_contains Γ h [< τ ->morph τ' >]) -> - (translate_morphism_path Γ τ τ' [{ %h% }]) - - | Translate_Chain : forall Γ τ τ' τ'' m1 m2, - (translate_morphism_path Γ τ τ' m1) -> - (translate_morphism_path Γ τ' τ'' m2) -> - (translate_morphism_path Γ τ τ'' - (expr_morph "x" τ [{ m2 (m1 %"x"%) }])) - - | Translate_MapSeq : forall Γ τ τ' m, - (translate_morphism_path Γ τ τ' m) -> - (translate_morphism_path Γ [< [τ] >] [< [τ'] >] - [{ - λ"xs",[τ] ↦morph (%"map"% # τ # τ' m %"xs"%) - }]) -. - -Example morphism_paths : - (ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >] - (ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$"ℝ"$ ->morph $"Angle"$~$"Radians"$~$"ℝ"$ >] - ctx_empty)) - - |- [< [ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$ ] >] - ~> [< [ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$ ] >] -. -Proof. - intros. - apply M_MapSeq. - apply M_Lift. - apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$"ℝ"$>]). - apply M_Single with (h:="degrees-to-turns"%string). - apply C_take. - - apply M_Single with (h:="turns-to-radians"%string). - apply C_shuffle. - apply C_take. -Qed. diff --git a/coq/smallstep.v b/coq/smallstep.v deleted file mode 100644 index ab6bfe4..0000000 --- a/coq/smallstep.v +++ /dev/null @@ -1,137 +0,0 @@ -From Coq Require Import Strings.String. -Require Import terms. -Require Import subst. -Require Import subtype. -Require Import typing. - -Reserved Notation " s '-->α' t " (at level 40). -Reserved Notation " s '-->β' t " (at level 40). - -Inductive expr_alpha : expr_term -> expr_term -> Prop := - | EAlpha_Rename : forall x x' τ e, - (expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e)) - - | EAlpha_TyRename : forall α α' e, - (expr_ty_abs α e) -->α (expr_ty_abs α' (expr_specialize α (type_var α') e)) - - | EAlpha_SubAbs : forall x τ e e', - (e -->α e') -> - [{ λ x , τ ↦ e }] -->α [{ λ x , τ ↦ e' }] - - | EAlpha_SubTyAbs : forall α e e', - (e -->α e') -> - [{ Λ α ↦ e }] -->α [{ Λ α ↦ e' }] - - | EAlpha_SubApp1 : forall e1 e1' e2, - (e1 -->α e1') -> - [{ e1 e2 }] -->α [{ e1' e2 }] - - | EAlpha_SubApp2 : forall e1 e2 e2', - (e2 -->α e2') -> - [{ e1 e2 }] -->α [{ e1 e2' }] - -where "s '-->α' t" := (expr_alpha s t). - - -Example a1 : polymorphic_identity1 -->α polymorphic_identity2. -Proof. - unfold polymorphic_identity1. - unfold polymorphic_identity2. - apply EAlpha_SubTyAbs. - apply EAlpha_Rename. -Qed. - - -Inductive beta_step : expr_term -> expr_term -> Prop := - | E_App1 : forall e1 e1' e2, - e1 -->β e1' -> - [{ e1 e2 }] -->β [{ e1' e2 }] - - | E_App2 : forall v1 e2 e2', - (is_value v1) -> - e2 -->β e2' -> - [{ v1 e2 }] -->β [{ v1 e2' }] - - | E_TypApp : forall e e' τ, - e -->β e' -> - [{ Λ τ ↦ e }] -->β [{ Λ τ ↦ e' }] - - | E_TypAppLam : forall α e τ, - [{ (Λ α ↦ e) # τ }] -->β (expr_specialize α τ e) - - | E_AppLam : forall x τ e a, - [{ (λ x , τ ↦ e) a }] -->β (expr_subst x a e) - - | E_AppMorph : forall x τ e a, - [{ (λ x , τ ↦morph e) a }] -->β (expr_subst x a e) - - | E_Let : forall x e a, - [{ let x := a in e }] -->β (expr_subst x a e) - - | E_StripAscend : forall τ e, - [{ e as τ }] -->β e - - | E_StripDescend : forall τ e, - [{ e des τ }] -->β e - - | E_Ascend : forall τ e e', - (e -->β e') -> - [{ e as τ }] -->β [{ e' as τ }] - - | E_AscendCollapse : forall τ' τ e, - [{ (e as τ) as τ' }] -->β [{ e as (τ'~τ) }] - - | E_DescendCollapse : forall τ' τ e, - (τ':<=τ) -> - [{ (e des τ') des τ }] -->β [{ e des τ }] - -where "s '-->β' t" := (beta_step s t). - -Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop := - | Multi_Refl : forall (x : X), multi R x x - | Multi_Step : forall (x y z : X), - R x y -> - multi R y z -> - multi R x z. - -Notation " s -->α* t " := (multi expr_alpha s t) (at level 40). -Notation " s -->β* t " := (multi beta_step s t) (at level 40). - - - -Example reduce1 : - [{ - let "deg2turns" := - (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$ - ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) - in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) ) - }] - -->β* - [{ - ((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$ - }]. -Proof. - apply Multi_Step with (y:=[{ (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$ - ↦morph (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]). - apply E_Let. - - apply Multi_Step with (y:=(expr_subst "x" [{%"60"% as $"Angle"$~$"Degrees"$}] [{ (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$) }])). - apply E_AppMorph. - simpl. - - apply Multi_Step with (y:=[{ ((%"/"% (%"60"% as $"Angle"$~$"Degrees"$)) %"360"%) as $"Angle"$~$"Turns"$ }]). - apply E_Ascend. - apply E_App1. - apply E_App2. - apply V_Abs, VAbs_Var. - apply E_StripDescend. - - apply Multi_Step with (y:=[{ (%"/"% %"60"% %"360"%) as $"Angle"$~$"Turns"$ }]). - apply E_Ascend. - apply E_App1. - apply E_App2. - apply V_Abs, VAbs_Var. - apply E_StripAscend. - - apply Multi_Refl. -Qed. diff --git a/coq/soundness.v b/coq/soundness.v deleted file mode 100644 index 346f101..0000000 --- a/coq/soundness.v +++ /dev/null @@ -1,359 +0,0 @@ -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. - diff --git a/coq/subst.v b/coq/subst.v deleted file mode 100644 index 5b8375f..0000000 --- a/coq/subst.v +++ /dev/null @@ -1,152 +0,0 @@ -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -Import ListNotations. -Require Import terms. - - -Fixpoint type_fv (τ : type_term) {struct τ} : (list string) := - match τ with - | type_id s => [] - | type_var α => [α] - | type_univ α τ => (remove string_dec α (type_fv τ)) - | type_spec σ τ => (type_fv σ) ++ (type_fv τ) - | type_fun σ τ => (type_fv σ) ++ (type_fv τ) - | type_morph σ τ => (type_fv σ) ++ (type_fv τ) - | type_ladder σ τ => (type_fv σ) ++ (type_fv τ) - end. - -Open Scope ladder_type_scope. -Example ex_type_fv1 : - (In "T"%string (type_fv [< ∀"U",%"T"% >])) -. -Proof. simpl. left. auto. Qed. - -Open Scope ladder_type_scope. -Example ex_type_fv2 : - ~(In "T"%string (type_fv [< ∀"T",%"T"% >])) -. -Proof. simpl. auto. Qed. - -(* scoped variable substitution in type terms $\label{coq:subst-type}$ *) -Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) : type_term := - match t0 with - | type_var name => if (eqb v name) then n else t0 - | type_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2)) - | type_univ x t => if (eqb v x) then t0 else type_univ x (type_subst v n t) - | type_spec t1 t2 => (type_spec (type_subst v n t1) (type_subst v n t2)) - | type_ladder t1 t2 => (type_ladder (type_subst v n t1) (type_subst v n t2)) - | t => t - end. - -(* - -Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop := - | TSubst_VarReplace : - (type_subst1 x σ (type_var x) σ) - - | TSubst_VarKeep : forall y, - (x <> y) -> - (type_subst1 x σ (type_var y) (type_var y)) - - | TSubst_UnivReplace : forall y τ τ', - ~(x = y) -> - ~(type_var_free y σ) -> - (type_subst1 x σ τ τ') -> - (type_subst1 x σ (type_univ y τ) (type_univ y τ')) - - | TSubst_Id : forall n, - (type_subst1 x σ (type_id n) (type_id n)) - - | TSubst_Spec : forall τ1 τ2 τ1' τ2', - (type_subst1 x σ τ1 τ1') -> - (type_subst1 x σ τ2 τ2') -> - (type_subst1 x σ (type_spec τ1 τ2) (type_spec τ1' τ2')) - - | TSubst_Fun : forall τ1 τ1' τ2 τ2', - (type_subst1 x σ τ1 τ1') -> - (type_subst1 x σ τ2 τ2') -> - (type_subst1 x σ (type_fun τ1 τ2) (type_fun τ1' τ2')) - - | TSubst_Morph : forall τ1 τ1' τ2 τ2', - (type_subst1 x σ τ1 τ1') -> - (type_subst1 x σ τ2 τ2') -> - (type_subst1 x σ (type_morph τ1 τ2) (type_morph τ1' τ2')) - - | TSubst_Ladder : forall τ1 τ1' τ2 τ2', - (type_subst1 x σ τ1 τ1') -> - (type_subst1 x σ τ2 τ2') -> - (type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ2')) -. -*) - -Lemma type_subst_symm : - forall x y τ τ', - ((type_subst x (type_var y) τ) = τ') -> - ((type_subst y (type_var x) τ') = τ) -. -Proof. - intros. - induction H. - - unfold type_subst. - induction τ. - reflexivity. - - -Admitted. - -Lemma type_subst_fresh : - forall α τ u, - ~ (In α (type_fv τ)) - -> (type_subst α u τ) = τ -. -Proof. - intros. - unfold type_subst. - induction τ. - reflexivity. - - - unfold eqb. - - admit. -(* - apply TSubst_Id. - apply TSubst_VarKeep. - contradict H. - rewrite H. - apply TFree_Var. - - apply TSubst_Fun. - apply IHτ1. - - contradict H. - apply TFree_Fun. - apply H. - apply - *) -Admitted. - - -(* scoped variable substitution, replaces free occurences of v with n in expression e *) -Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) := - match e0 with - | expr_var name => if (eqb v name) then n else e0 - | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e) - | expr_ty_app e t => expr_ty_app (expr_subst v n e) t - | expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e) - | expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e) - | expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a) - | expr_let x a e => expr_let x (expr_subst v n a) (expr_subst v n e) - | expr_ascend t e => expr_ascend t (expr_subst v n e) - | expr_descend t e => expr_descend t (expr_subst v n e) - end. - -(* replace only type variables in expression *) -Fixpoint expr_specialize (v:string) (n:type_term) (e0:expr_term) := - match e0 with - | expr_ty_app e t => expr_ty_app (expr_specialize v n e) (type_subst v n t) - | expr_ascend t e => expr_ascend (type_subst v n t) (expr_specialize v n e) - | expr_descend t e => expr_descend (type_subst v n t) (expr_specialize v n e) - | e => e - end. diff --git a/coq/subtype.v b/coq/subtype.v deleted file mode 100644 index afaacd0..0000000 --- a/coq/subtype.v +++ /dev/null @@ -1,94 +0,0 @@ -(* - * This module defines the subtype relationship - * - * We distinguish between *representational* subtypes, - * where any high-level type is a subtype of its underlying - * representation type and *convertible* subtypes that - * are compatible at high level, but have a different representation - * that requires a conversion. - *) - -From Coq Require Import Strings.String. -Require Import terms. -Require Import equiv. - -(** Subtyping *) - -Reserved Notation "s ':<=' t" (at level 50). -Reserved Notation "s '~<=' t" (at level 50). - -(* Representational Subtype *) -Inductive is_repr_subtype : type_term -> type_term -> Prop := - | TSubRepr_Refl : forall t t', (t === t') -> (t :<= t') - | TSubRepr_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z) - | TSubRepr_Ladder : forall x' x y, (x :<= y) -> ((type_ladder x' x) :<= y) -where "s ':<=' t" := (is_repr_subtype s t). - -(* Convertible Subtype *) -Inductive is_conv_subtype : type_term -> type_term -> Prop := - | TSubConv_Refl : forall t t', (t === t') -> (t ~<= t') - | TSubConv_Trans : forall x y z, (x ~<= y) -> (y ~<= z) -> (x ~<= z) - | TSubConv_Ladder : forall x' x y, (x ~<= y) -> ((type_ladder x' x) ~<= y) - | TSubConv_Morph : forall x y y', (type_ladder x y) ~<= (type_ladder x y') -where "s '~<=' t" := (is_conv_subtype s t). - - -(* Every Representational Subtype is a Convertible Subtype *) - -Lemma syn_sub_is_sem_sub : forall x y, (x :<= y) -> (x ~<= y). -Proof. - intros. - induction H. - apply TSubConv_Refl. - apply H. - apply TSubConv_Trans with (x:=x) (y:=y) (z:=z). - apply IHis_repr_subtype1. - apply IHis_repr_subtype2. - apply TSubConv_Ladder. - apply IHis_repr_subtype. -Qed. - - - - -(* EXAMPLES *) - -Open Scope ladder_type_scope. -Open Scope ladder_expr_scope. - -Example sub0 : - [< - < $"Seq"$ < $"Digit"$ $"10"$ > > - ~ < $"Seq"$ $"Char"$ > - >] -:<= - [< - < $"Seq"$ $"Char"$ > - >] -. -Proof. - apply TSubRepr_Ladder. - apply TSubRepr_Refl. - apply TEq_Refl. -Qed. - - -Example sub1 : - [< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >] -:<= [< < $"Seq"$ $"Char"$ > >] -. -Proof. - set [< < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > >]. - set [< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >]. - set [< < $"Seq"$ $"Char"$ > >]. - set (t0 === t). - set (t :<= t0). - set (t :<= t1). - apply TSubRepr_Trans with t. - apply TSubRepr_Refl. - apply TEq_Distribute. - apply L_DistributeOverSpec2. - apply TSubRepr_Ladder. - apply TSubRepr_Refl. - apply TEq_Refl. -Qed. diff --git a/coq/terms_debruijn.v b/coq/terms/debruijn.v similarity index 100% rename from coq/terms_debruijn.v rename to coq/terms/debruijn.v diff --git a/coq/equiv_debruijn.v b/coq/terms/equiv.v similarity index 99% rename from coq/equiv_debruijn.v rename to coq/terms/equiv.v index a905598..c22e804 100644 --- a/coq/equiv_debruijn.v +++ b/coq/terms/equiv.v @@ -1,4 +1,4 @@ -Require Import terms_debruijn. +Require Import debruijn. Local Open Scope ladder_type_scope. Local Open Scope ladder_expr_scope. diff --git a/coq/eval_debruijn.v b/coq/terms/eval.v similarity index 91% rename from coq/eval_debruijn.v rename to coq/terms/eval.v index b86631d..a1ae5ea 100644 --- a/coq/eval_debruijn.v +++ b/coq/terms/eval.v @@ -1,11 +1,11 @@ From Coq Require Import Lists.List. Import ListNotations. Require Import Atom. -Require Import terms_debruijn. -Require Import subtype_debruijn. -Require Import context_debruijn. -Require Import morph_debruijn. -Require Import typing_debruijn. +Require Import debruijn. +Require Import subtype. +Require Import context. +Require Import morph. +Require Import typing. Open Scope ladder_expr_scope. diff --git a/coq/terms.v b/coq/terms/named.v similarity index 100% rename from coq/terms.v rename to coq/terms/named.v diff --git a/coq/typing.v b/coq/typing.v deleted file mode 100644 index e133988..0000000 --- a/coq/typing.v +++ /dev/null @@ -1,383 +0,0 @@ -(* This module defines the typing relation - * where each expression is assigned a type. - *) -From Coq Require Import Strings.String. -Require Import terms. -Require Import subst. -Require Import equiv. -Require Import subtype. -Require Import context. -Require Import morph. - -(** Typing Derivation *) - -Open Scope ladder_type_scope. -Open Scope ladder_expr_scope. - -Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0). - -Inductive expr_type : context -> expr_term -> type_term -> Prop := - | T_Var : forall Γ x τ, - context_contains Γ x τ -> - Γ |- [{ %x% }] \is τ - - | T_Let : forall Γ s σ t τ x, - Γ |- s \is σ -> - (ctx_assign x σ Γ) |- t \is τ -> - Γ |- [{ let x := s in t }] \is τ - - | T_TypeAbs : forall Γ e τ α, - Γ |- e \is τ -> - Γ |- [{ Λ α ↦ e }] \is [< ∀α,τ >] - - | T_TypeApp : forall Γ α e σ τ, - Γ |- e \is [< ∀α, τ >] -> - Γ |- [{ e # σ }] \is (type_subst α σ τ) - - | T_Abs : forall Γ x σ t τ, - (ctx_assign x σ Γ) |- t \is τ -> - Γ |- [{ λ x , σ ↦ t }] \is [< σ -> τ >] - - | T_MorphAbs : forall Γ x σ t τ, - (ctx_assign x σ Γ) |- t \is τ -> - Γ |- [{ λ x , σ ↦morph t }] \is [< σ ->morph τ >] - - | T_App : forall Γ f a σ' σ τ, - (Γ |- f \is [< σ -> τ >]) -> - (Γ |- a \is σ') -> - (Γ |- σ' ~> σ) -> - (Γ |- [{ (f a) }] \is τ) - - | T_MorphFun : forall Γ f σ τ, - Γ |- f \is (type_morph σ τ) -> - Γ |- f \is (type_fun σ τ) - - | T_Ascend : forall Γ e τ τ', - (Γ |- e \is τ) -> - (Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) - - | T_DescendImplicit : forall Γ x τ τ', - Γ |- x \is τ -> - (τ :<= τ') -> - Γ |- x \is τ' - - | T_Descend : forall Γ x τ τ', - Γ |- x \is τ -> - (τ :<= τ') -> - Γ |- [{ x des τ' }] \is τ' - -where "Γ '|-' x '\is' τ" := (expr_type Γ x τ). - -Definition is_well_typed (e:expr_term) : Prop := - forall Γ, - exists τ, - Γ |- e \is τ -. - -Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop := - | Expand_Var : forall Γ x τ, - (Γ |- (expr_var x) \is τ) -> - (translate_typing Γ [{ %x% }] τ [{ %x% }]) - - | Expand_Let : forall Γ x e e' t t' σ τ, - (Γ |- e \is σ) -> - ((ctx_assign x σ Γ) |- t \is τ) -> - (translate_typing Γ e σ e') -> - (translate_typing (ctx_assign x σ Γ) t τ t') -> - (translate_typing Γ - [{ let x := e in t }] - τ - [{ let x := e' in t' }]) - - | Expand_TypeAbs : forall Γ α e e' τ, - (Γ |- e \is τ) -> - (translate_typing Γ e τ e') -> - (translate_typing Γ - [{ Λ α ↦ e }] - [< ∀ α,τ >] - [{ Λ α ↦ e' }]) - - | Expand_TypeApp : forall Γ e e' σ α τ, - (Γ |- e \is (type_univ α τ)) -> - (translate_typing Γ e τ e') -> - (translate_typing Γ - [{ e # σ }] - (type_subst α σ τ) - [{ e' # σ }]) - - | Expand_Abs : forall Γ x σ e e' τ, - ((ctx_assign x σ Γ) |- e \is τ) -> - (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) -> - (translate_typing (ctx_assign x σ Γ) e τ e') -> - (translate_typing Γ - [{ λ x , σ ↦ e }] - [< σ -> τ >] - [{ λ x , σ ↦ e' }]) - - | Expand_MorphAbs : forall Γ x σ e e' τ, - ((ctx_assign x σ Γ) |- e \is τ) -> - (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) -> - (translate_typing (ctx_assign x σ Γ) e τ e') -> - (translate_typing Γ - [{ λ x , σ ↦morph e }] - [< σ ->morph τ >] - [{ λ x , σ ↦morph e' }]) - - | Expand_App : forall Γ f f' a a' m σ τ σ', - (Γ |- f \is (type_fun σ τ)) -> - (Γ |- a \is σ') -> - (Γ |- σ' ~> σ) -> - (translate_typing Γ f [< σ -> τ >] f') -> - (translate_typing Γ a σ' a') -> - (translate_morphism_path Γ σ' σ m) -> - (translate_typing Γ [{ f a }] τ [{ f' (m a') }]) - - | Expand_MorphFun : forall Γ f f' σ τ, - (Γ |- f \is (type_morph σ τ)) -> - (Γ |- f \is (type_fun σ τ)) -> - (translate_typing Γ f [< σ ->morph τ >] f') -> - (translate_typing Γ f [< σ -> τ >] f') - - | Expand_Ascend : forall Γ e e' τ τ', - (Γ |- e \is τ) -> - (Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) -> - (translate_typing Γ e τ e') -> - (translate_typing Γ [{ e as τ' }] [< τ' ~ τ >] [{ e' as τ' }]) - - | Expand_Descend : forall Γ e e' τ τ', - (Γ |- e \is τ) -> - (τ :<= τ') -> - (Γ |- [{ e des τ' }] \is τ') -> - (translate_typing Γ e τ e') -> - (translate_typing Γ e τ' [{ e' des τ' }]) -. - -(* Examples *) - -Example typing1 : - ctx_empty |- [{ Λ"T" ↦ λ "x",%"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >]. -Proof. - intros. - apply T_TypeAbs. - apply T_Abs. - apply T_Var. - apply C_take. -Qed. - -Example typing2 : - ctx_empty |- [{ Λ"T" ↦ λ "x",%"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >]. -Proof. - intros. - apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]). - apply T_TypeAbs. - apply T_Abs. - apply T_Var. - apply C_take. - - apply TSubRepr_Refl. - apply TEq_Alpha. - apply TAlpha_Rename. -Qed. - -Example typing3 : - ctx_empty |- [{ - Λ"T" ↦ Λ"U" ↦ λ"x",%"T"% ↦ λ"y",%"U"% ↦ %"y"% - }] \is [< - ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) - >]. -Proof. - intros. - apply T_DescendImplicit with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]). - apply T_TypeAbs, T_TypeAbs, T_Abs. - apply T_Abs. - apply T_Var. - apply C_take. - - apply TSubRepr_Refl. - apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ). - apply TEq_Alpha. - apply TAlpha_Rename. - - apply TEq_Alpha. - apply TAlpha_SubUniv. - apply TAlpha_Rename. -Qed. - -Example typing4 : (is_well_typed - [{ Λ"T" ↦ Λ"U" ↦ λ"x",%"T"% ↦ λ"y",%"U"% ↦ %"x"% }] -). -Proof. - unfold is_well_typed. - exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >]. - apply T_TypeAbs. - apply T_TypeAbs. - apply T_Abs. - apply T_Abs. - apply T_Var. - apply C_shuffle, C_take. -Qed. - -Example typing5 : - (ctx_assign "60" [< $"ℝ"$ >] - (ctx_assign "360" [< $"ℝ"$ >] - (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >] - ctx_empty))) - |- - [{ - let "deg2turns" := - (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$ - ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$)) - in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) ) - }] - \is - [< - $"Angle"$~$"Turns"$~$"ℝ"$ - >] -. -Proof. - apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]). - apply T_MorphAbs. - apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Turns"$>] [<$"ℝ"$>])). - 2: apply TSubRepr_Refl, TEq_LadderAssocLR. - apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]). - apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]). - apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]). - apply T_Var. - apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take. - apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$"ℝ"$ >]). - apply T_Var. - apply C_take. - apply TSubRepr_Ladder. apply TSubRepr_Ladder. - apply TSubRepr_Refl. apply TEq_Refl. - apply M_Sub. - apply TSubRepr_Refl. apply TEq_Refl. - apply T_Var. - apply C_shuffle, C_shuffle, C_take. - apply M_Sub. - apply TSubRepr_Refl. - apply TEq_Refl. - apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]). - apply T_MorphFun. - apply T_Var. - apply C_take. - apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Degrees"$>] [<$"ℝ"$>])). - 2: apply TSubRepr_Refl, TEq_LadderAssocLR. - apply T_Ascend. - apply T_Var. - apply C_shuffle. apply C_take. - apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl. -Qed. - - -Ltac var_typing := auto using T_Var, C_shuffle, C_take. -Ltac repr_subtype := auto using TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl, TEq_LadderAssocLR. - -Example expand1 : - (translate_typing - (ctx_assign "60" [< $"ℝ"$ >] - (ctx_assign "360" [< $"ℝ"$ >] - (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >] - ctx_empty))) - [{ - let "deg2turns" := - (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$ - ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) in - let "sin" := (λ"α",$"Angle"$~$"Turns"$~$"ℝ"$ ↦ (%"α"% des $"ℝ"$)) in - ( %"sin"% (%"60"% as $"Angle"$~$"Degrees"$) ) - }] - [< - $"ℝ"$ - >] - [{ - let "deg2turns" := - (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$ - ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) in - let "sin" := (λ"α",$"Angle"$~$"Turns"$~$"ℝ"$ ↦ (%"α"% des $"ℝ"$)) in - (%"sin"% (%"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$))) - }]) -. -Proof. - apply Expand_Let with (σ:=[< ($"Angle"$~$"Degrees"$)~$"ℝ"$ ->morph ($"Angle"$~$"Turns"$)~$"ℝ"$ >]). - - - apply T_DescendImplicit with (τ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$ ~ $"ℝ"$ >]). - 2: { - apply TSubRepr_Refl. - apply TEq_SubMorph. - apply TEq_LadderAssocRL. - apply TEq_LadderAssocRL. - } - apply T_MorphAbs. - apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]). - 2: { - apply TSubRepr_Refl. - apply TEq_LadderAssocLR. - } - apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]). - apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]). - apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]). - var_typing. - var_typing. - apply T_Descend with (τ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]). - repr_subtype. - var_typing. - repr_subtype. - apply id_morphism_path. - var_typing. - apply id_morphism_path. - - - apply T_Let with (σ:=[< $"Angle"$~$"Turns"$~$"ℝ"$ -> $"ℝ"$ >]). - apply T_Abs. - * apply T_Descend with (τ:=[<$"Angle"$~$"Turns"$~$"ℝ"$>]). - 2: repr_subtype. - var_typing. - - * apply T_App with (σ':=[<($"Angle"$~$"Degrees"$)~$"ℝ"$>]) (σ:=[<($"Angle"$~$"Turns"$)~$"ℝ"$>]) (τ:=[<$"ℝ"$>]). - apply T_DescendImplicit with (τ:=[< $"Angle"$~$"Turns"$~$"ℝ"$ -> $"ℝ"$ >]). - 2: { - apply TSubRepr_Refl. - apply TEq_SubFun. - apply TEq_LadderAssocRL. - apply TEq_Refl. - } - var_typing. - - apply T_Ascend with (τ':=[<$"Angle"$~$"Degrees"$>]) (τ:=[<$"ℝ"$>]). - var_typing. - - apply M_Single with (h:="deg2turns"%string). - var_typing. - - - admit. - (* - - apply Expand_MorphAbs. - * apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]). - 2: repr_subtype. - apply T_Ascend with (τ':=[<$"Angle"$~$"Turns"$>]) (τ:=[<$"ℝ"$>]). - apply T_App with (σ:=[<$"ℝ"$>]) (σ':=[<$"ℝ"$>]). - apply T_App with (σ:=[<$"ℝ"$>]) (σ':=[<$"ℝ"$>]). - auto using T_Var, C_shuffle, C_take. - apply T_Descend with (τ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]). - 2: repr_subtype. - var_typing. - apply id_morphism_path. - var_typing. - apply id_morphism_path. - - * apply T_Abs. - apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]). - 2: repr_subtype. - apply T_Ascend with (τ':=[<$"Angle"$~$"Turns"$>]) (τ:=[<$"ℝ"$>]). - apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]). - apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]). - var_typing. - apply T_Descend with [<$"Angle"$~$"Degrees"$~$"ℝ"$>]. - 2: repr_subtype. - var_typing. - apply id_morphism_path. - var_typing. - apply id_morphism_path. - - * apply Expand_Ascend. -*) - - admit. -Admitted. diff --git a/coq/context_debruijn.v b/coq/typing/context.v similarity index 72% rename from coq/context_debruijn.v rename to coq/typing/context.v index 45d61d0..595fa12 100644 --- a/coq/context_debruijn.v +++ b/coq/typing/context.v @@ -1,4 +1,4 @@ Require Import Atom. -Require Import terms_debruijn. +Require Import debruijn. Definition context : Type := (list (atom * type_DeBruijn)). diff --git a/coq/morph_debruijn.v b/coq/typing/morph.v similarity index 94% rename from coq/morph_debruijn.v rename to coq/typing/morph.v index 3cf03a0..b94619a 100644 --- a/coq/morph_debruijn.v +++ b/coq/typing/morph.v @@ -1,7 +1,7 @@ -Require Import terms_debruijn. -Require Import equiv_debruijn. -Require Import subtype_debruijn. -Require Import context_debruijn. +Require Import debruijn. +Require Import equiv. +Require Import subtype. +Require Import context. Require Import Atom. Import AtomImpl. From Coq Require Import Lists.List. diff --git a/coq/subtype_debruijn.v b/coq/typing/subtype.v similarity index 96% rename from coq/subtype_debruijn.v rename to coq/typing/subtype.v index caedc58..b86c38b 100644 --- a/coq/subtype_debruijn.v +++ b/coq/typing/subtype.v @@ -8,8 +8,8 @@ * that requires a conversion. *) -Require Import terms_debruijn. -Require Import equiv_debruijn. +Require Import debruijn. +Require Import equiv. (** Subtyping *) diff --git a/coq/typing_debruijn.v b/coq/typing/typing.v similarity index 97% rename from coq/typing_debruijn.v rename to coq/typing/typing.v index 51aa417..474028c 100644 --- a/coq/typing_debruijn.v +++ b/coq/typing/typing.v @@ -2,10 +2,10 @@ From Coq Require Import Lists.List. Import ListNotations. Require Import Metatheory. Require Import Atom. -Require Import terms_debruijn. -Require Import subtype_debruijn. -Require Import context_debruijn. -Require Import morph_debruijn. +Require Import debruijn. +Require Import subtype. +Require Import context. +Require Import morph. Open Scope ladder_type_scope. Open Scope ladder_expr_scope.