Compare commits
3 commits
638ddf4fd1
...
44d8d401d8
Author | SHA1 | Date | |
---|---|---|---|
44d8d401d8 | |||
12da3e97bd | |||
cae0572e1b |
7 changed files with 502 additions and 80 deletions
|
@ -69,7 +69,7 @@ Compute (expr_subst "x"
|
||||||
Example example_let_reduction :
|
Example example_let_reduction :
|
||||||
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
|
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
|
||||||
Proof.
|
Proof.
|
||||||
apply E_AppLet.
|
apply E_Let.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Compute (expr_app bb_succ bb_zero) -->β bb_one.
|
Compute (expr_app bb_succ bb_zero) -->β bb_one.
|
||||||
|
|
13
coq/equiv.v
13
coq/equiv.v
|
@ -218,6 +218,16 @@ Inductive type_eq : type_term -> type_term -> Prop :=
|
||||||
y === z ->
|
y === z ->
|
||||||
x === z
|
x === z
|
||||||
|
|
||||||
|
| TEq_LadderAssocLR : forall x y z,
|
||||||
|
(type_ladder (type_ladder x y) z)
|
||||||
|
===
|
||||||
|
(type_ladder x (type_ladder y z))
|
||||||
|
|
||||||
|
| TEq_LadderAssocRL : forall x y z,
|
||||||
|
(type_ladder x (type_ladder y z))
|
||||||
|
===
|
||||||
|
(type_ladder (type_ladder x y) z)
|
||||||
|
|
||||||
| TEq_Alpha : forall x y,
|
| TEq_Alpha : forall x y,
|
||||||
x --->α y ->
|
x --->α y ->
|
||||||
x === y
|
x === y
|
||||||
|
@ -248,6 +258,9 @@ Proof.
|
||||||
apply IHtype_eq2.
|
apply IHtype_eq2.
|
||||||
apply IHtype_eq1.
|
apply IHtype_eq1.
|
||||||
|
|
||||||
|
apply TEq_LadderAssocRL.
|
||||||
|
apply TEq_LadderAssocLR.
|
||||||
|
|
||||||
apply type_alpha_symm in H.
|
apply type_alpha_symm in H.
|
||||||
apply TEq_Alpha.
|
apply TEq_Alpha.
|
||||||
apply H.
|
apply H.
|
||||||
|
|
|
@ -52,7 +52,7 @@ Inductive translate_morphism_path : context -> type_term -> type_term -> expr_te
|
||||||
(translate_morphism_path Γ τ τ' m) ->
|
(translate_morphism_path Γ τ τ' m) ->
|
||||||
(translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
|
(translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
|
||||||
(expr_morph "x" (type_ladder σ τ)
|
(expr_morph "x" (type_ladder σ τ)
|
||||||
(expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
|
(expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))
|
||||||
|
|
||||||
| Translate_Single : forall Γ h τ τ',
|
| Translate_Single : forall Γ h τ τ',
|
||||||
(context_contains Γ h (type_morph τ τ')) ->
|
(context_contains Γ h (type_morph τ τ')) ->
|
||||||
|
|
|
@ -61,8 +61,8 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
|
||||||
e -->β e' ->
|
e -->β e' ->
|
||||||
(expr_ty_app e τ) -->β (expr_ty_app e' τ)
|
(expr_ty_app e τ) -->β (expr_ty_app e' τ)
|
||||||
|
|
||||||
| E_TypAppLam : forall x e a,
|
| E_TypAppLam : forall α e τ,
|
||||||
(expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
|
(expr_ty_app (expr_ty_abs α e) τ) -->β (expr_specialize α τ e)
|
||||||
|
|
||||||
| E_AppLam : forall x τ e a,
|
| E_AppLam : forall x τ e a,
|
||||||
(expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
|
(expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
|
||||||
|
@ -70,8 +70,25 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
|
||||||
| E_AppMorph : forall x τ e a,
|
| E_AppMorph : forall x τ e a,
|
||||||
(expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
|
(expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
|
||||||
|
|
||||||
| E_AppLet : forall x t e a,
|
| E_Let : forall x e a,
|
||||||
(expr_let x t a e) -->β (expr_subst x a e)
|
(expr_let x a e) -->β (expr_subst x a e)
|
||||||
|
|
||||||
|
| E_StripAscend : forall τ e,
|
||||||
|
(expr_ascend τ e) -->β e
|
||||||
|
|
||||||
|
| E_StripDescend : forall τ e,
|
||||||
|
(expr_descend τ e) -->β e
|
||||||
|
|
||||||
|
| E_Ascend : forall τ e e',
|
||||||
|
(e -->β e') ->
|
||||||
|
(expr_ascend τ e) -->β (expr_ascend τ e')
|
||||||
|
|
||||||
|
| E_AscendCollapse : forall τ' τ e,
|
||||||
|
(expr_ascend τ' (expr_ascend τ e)) -->β (expr_ascend (type_ladder τ' τ) e)
|
||||||
|
|
||||||
|
| E_DescendCollapse : forall τ' τ e,
|
||||||
|
(τ':<=τ) ->
|
||||||
|
(expr_descend τ (expr_descend τ' e)) -->β (expr_descend τ e)
|
||||||
|
|
||||||
where "s '-->β' t" := (beta_step s t).
|
where "s '-->β' t" := (beta_step s t).
|
||||||
|
|
||||||
|
@ -85,4 +102,43 @@ Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
|
||||||
Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
|
Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
|
||||||
Notation " s -->β* t " := (multi beta_step 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.
|
||||||
|
|
||||||
End Smallstep.
|
End Smallstep.
|
||||||
|
|
396
coq/soundness.v
396
coq/soundness.v
|
@ -16,40 +16,402 @@ Include Typing.
|
||||||
|
|
||||||
Module Soundness.
|
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.
|
||||||
|
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.
|
||||||
|
|
||||||
|
(* 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 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.
|
||||||
|
apply IHtranslate_typing.
|
||||||
|
apply H0.
|
||||||
|
|
||||||
|
(* 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 *)
|
(* e is stuck when it is neither a value, nor can it be reduced *)
|
||||||
Definition is_stuck (e:expr_term) : Prop :=
|
Definition is_stuck (e:expr_term) : Prop :=
|
||||||
~(is_value e) ->
|
~(is_value e) ->
|
||||||
~(exists e', e -->β e')
|
~(exists e', e -->β e')
|
||||||
.
|
.
|
||||||
|
|
||||||
(* every well typed term is not stuck *)
|
(* the translation any well typed term is not stuck *)
|
||||||
Lemma progress :
|
Lemma progress :
|
||||||
forall (e:expr_term),
|
forall Γ e τ e',
|
||||||
(is_well_typed e) -> ~(is_stuck e)
|
(Γ |- e \is τ) ->
|
||||||
|
(translate_typing Γ e τ e') ->
|
||||||
|
~(is_stuck e')
|
||||||
.
|
.
|
||||||
Proof.
|
Proof.
|
||||||
|
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
(* reduction step preserves well-typedness *)
|
(* every well-typed expression is translated,
|
||||||
Lemma preservation :
|
* such that it be reduced to a value
|
||||||
|
*)
|
||||||
|
Theorem soundness :
|
||||||
forall Γ e e' τ,
|
forall Γ e e' τ,
|
||||||
(Γ |- e \is τ) ->
|
(Γ |- e \is τ) ->
|
||||||
(e -->β e') ->
|
(translate_typing Γ e τ e') ->
|
||||||
(Γ |- e' \is τ)
|
(exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \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'))
|
|
||||||
.
|
.
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
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.
|
Admitted.
|
||||||
|
|
||||||
End Soundness.
|
End Soundness.
|
||||||
|
|
57
coq/terms.v
57
coq/terms.v
|
@ -30,45 +30,34 @@ Inductive expr_term : Type :=
|
||||||
| expr_descend : type_term -> expr_term -> expr_term
|
| 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 *)
|
(* values *)
|
||||||
Inductive is_value : expr_term -> Prop :=
|
Inductive is_abs_value : expr_term -> Prop :=
|
||||||
| V_Abs : forall x τ e,
|
| VAbs_Var : forall x,
|
||||||
(is_value (expr_abs x τ e))
|
(is_abs_value (expr_var x))
|
||||||
|
|
||||||
| V_TypAbs : forall τ e,
|
| VAbs_Abs : forall x τ e,
|
||||||
(is_value (expr_ty_abs τ 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,
|
| V_Ascend : forall τ e,
|
||||||
(is_value e) ->
|
(is_abs_value e) ->
|
||||||
(is_value (expr_ascend τ 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_type_scope.
|
||||||
Declare Scope ladder_expr_scope.
|
Declare Scope ladder_expr_scope.
|
||||||
|
@ -108,6 +97,8 @@ Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
|
||||||
(in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
|
(in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
|
||||||
Notation "e 'as' τ" := (expr_ascend τ e)
|
Notation "e 'as' τ" := (expr_ascend τ e)
|
||||||
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
|
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
|
||||||
|
Notation "e 'des' τ" := (expr_descend τ e)
|
||||||
|
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
|
||||||
Notation "e1 e2" := (expr_app e1 e2)
|
Notation "e1 e2" := (expr_app e1 e2)
|
||||||
(in custom ladder_expr at level 50) : ladder_expr_scope.
|
(in custom ladder_expr at level 50) : ladder_expr_scope.
|
||||||
Notation "'(' e ')'" := e
|
Notation "'(' e ')'" := e
|
||||||
|
|
48
coq/typing.v
48
coq/typing.v
|
@ -61,8 +61,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
|
||||||
|
|
||||||
| T_Ascend : forall Γ e τ τ',
|
| T_Ascend : forall Γ e τ τ',
|
||||||
(Γ |- e \is τ) ->
|
(Γ |- e \is τ) ->
|
||||||
(τ' :<= τ) ->
|
(Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))
|
||||||
(Γ |- (expr_ascend τ' e) \is τ')
|
|
||||||
|
|
||||||
| T_DescendImplicit : forall Γ x τ τ',
|
| T_DescendImplicit : forall Γ x τ τ',
|
||||||
Γ |- x \is τ ->
|
Γ |- x \is τ ->
|
||||||
|
@ -77,7 +76,8 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
|
||||||
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
|
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
|
||||||
|
|
||||||
Definition is_well_typed (e:expr_term) : Prop :=
|
Definition is_well_typed (e:expr_term) : Prop :=
|
||||||
exists Γ τ,
|
forall Γ,
|
||||||
|
exists τ,
|
||||||
Γ |- e \is τ
|
Γ |- e \is τ
|
||||||
.
|
.
|
||||||
|
|
||||||
|
@ -135,10 +135,9 @@ Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> P
|
||||||
|
|
||||||
| Expand_Ascend : forall Γ e e' τ τ',
|
| Expand_Ascend : forall Γ e e' τ τ',
|
||||||
(Γ |- e \is τ) ->
|
(Γ |- e \is τ) ->
|
||||||
(τ' :<= τ) ->
|
(Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
|
||||||
(Γ |- (expr_ascend τ' e) \is τ') ->
|
|
||||||
(translate_typing Γ e τ e') ->
|
(translate_typing Γ e τ e') ->
|
||||||
(translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
|
(translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))
|
||||||
|
|
||||||
| Expand_Descend : forall Γ e e' τ τ',
|
| Expand_Descend : forall Γ e e' τ τ',
|
||||||
(Γ |- e \is τ) ->
|
(Γ |- e \is τ) ->
|
||||||
|
@ -219,7 +218,6 @@ Example typing4 : (is_well_typed
|
||||||
).
|
).
|
||||||
Proof.
|
Proof.
|
||||||
unfold is_well_typed.
|
unfold is_well_typed.
|
||||||
exists ctx_empty.
|
|
||||||
exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
|
exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
|
||||||
apply T_TypeAbs.
|
apply T_TypeAbs.
|
||||||
apply T_TypeAbs.
|
apply T_TypeAbs.
|
||||||
|
@ -231,24 +229,29 @@ Qed.
|
||||||
|
|
||||||
Open Scope ladder_expr_scope.
|
Open Scope ladder_expr_scope.
|
||||||
|
|
||||||
Example typing5 : (is_well_typed
|
Example typing5 :
|
||||||
|
(ctx_assign "60" [< $"ℝ"$ >]
|
||||||
|
(ctx_assign "360" [< $"ℝ"$ >]
|
||||||
|
(ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
|
||||||
|
ctx_empty)))
|
||||||
|
|-
|
||||||
[{
|
[{
|
||||||
let "deg2turns" :=
|
let "deg2turns" :=
|
||||||
(λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
|
(λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
|
||||||
↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$"ℝ"$))
|
↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
|
||||||
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$"ℝ"$) )
|
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
|
||||||
}]
|
}]
|
||||||
).
|
\is
|
||||||
|
[<
|
||||||
|
$"Angle"$~$"Turns"$~$"ℝ"$
|
||||||
|
>]
|
||||||
|
.
|
||||||
Proof.
|
Proof.
|
||||||
unfold is_well_typed.
|
|
||||||
exists (ctx_assign "60" [< $"ℝ"$ >]
|
|
||||||
(ctx_assign "360" [< $"ℝ"$ >]
|
|
||||||
(ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
|
|
||||||
ctx_empty))).
|
|
||||||
exists [< $"Angle"$~$"Turns"$~$"ℝ"$ >].
|
|
||||||
apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
|
apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
|
||||||
apply T_MorphAbs.
|
apply T_MorphAbs.
|
||||||
apply T_Ascend with (τ:=[< $"ℝ"$ >]).
|
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_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
|
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
|
||||||
apply T_Var.
|
apply T_Var.
|
||||||
|
@ -265,18 +268,15 @@ Proof.
|
||||||
apply M_Sub.
|
apply M_Sub.
|
||||||
apply TSubRepr_Refl.
|
apply TSubRepr_Refl.
|
||||||
apply TEq_Refl.
|
apply TEq_Refl.
|
||||||
apply TSubRepr_Ladder, TSubRepr_Ladder, TSubRepr_Refl.
|
|
||||||
apply TEq_Refl.
|
|
||||||
apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
|
apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
|
||||||
apply T_MorphFun.
|
apply T_MorphFun.
|
||||||
apply T_Var.
|
apply T_Var.
|
||||||
apply C_take.
|
apply C_take.
|
||||||
apply T_Ascend with (τ:=[<$"ℝ"$>]).
|
apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Degrees"$>] [<$"ℝ"$>])).
|
||||||
|
2: apply TSubRepr_Refl, TEq_LadderAssocLR.
|
||||||
|
apply T_Ascend.
|
||||||
apply T_Var.
|
apply T_Var.
|
||||||
apply C_shuffle. apply C_take.
|
apply C_shuffle. 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 M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue