Compare commits
No commits in common. "44d8d401d83b524cfb7970bdd841df9c68fd5125" and "638ddf4fd1a3655264ded3852bf0074702af9e1b" have entirely different histories.
44d8d401d8
...
638ddf4fd1
7 changed files with 77 additions and 499 deletions
|
@ -69,7 +69,7 @@ Compute (expr_subst "x"
|
|||
Example example_let_reduction :
|
||||
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
|
||||
Proof.
|
||||
apply E_Let.
|
||||
apply E_AppLet.
|
||||
Qed.
|
||||
|
||||
Compute (expr_app bb_succ bb_zero) -->β bb_one.
|
||||
|
|
13
coq/equiv.v
13
coq/equiv.v
|
@ -218,16 +218,6 @@ Inductive type_eq : type_term -> type_term -> Prop :=
|
|||
y === 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,
|
||||
x --->α y ->
|
||||
x === y
|
||||
|
@ -257,9 +247,6 @@ Proof.
|
|||
apply TEq_Trans with (y:=y).
|
||||
apply IHtype_eq2.
|
||||
apply IHtype_eq1.
|
||||
|
||||
apply TEq_LadderAssocRL.
|
||||
apply TEq_LadderAssocLR.
|
||||
|
||||
apply type_alpha_symm in H.
|
||||
apply TEq_Alpha.
|
||||
|
|
|
@ -52,7 +52,7 @@ Inductive translate_morphism_path : context -> type_term -> type_term -> expr_te
|
|||
(translate_morphism_path Γ τ τ' m) ->
|
||||
(translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
|
||||
(expr_morph "x" (type_ladder σ τ)
|
||||
(expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))
|
||||
(expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
|
||||
|
||||
| Translate_Single : forall Γ h τ τ',
|
||||
(context_contains Γ h (type_morph τ τ')) ->
|
||||
|
|
|
@ -61,8 +61,8 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
|
|||
e -->β e' ->
|
||||
(expr_ty_app e τ) -->β (expr_ty_app e' τ)
|
||||
|
||||
| E_TypAppLam : forall α e τ,
|
||||
(expr_ty_app (expr_ty_abs α e) τ) -->β (expr_specialize α τ e)
|
||||
| E_TypAppLam : forall x e a,
|
||||
(expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
|
||||
|
||||
| E_AppLam : forall x τ e a,
|
||||
(expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
|
||||
|
@ -70,25 +70,8 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
|
|||
| E_AppMorph : forall x τ e a,
|
||||
(expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
|
||||
|
||||
| E_Let : forall x e a,
|
||||
(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)
|
||||
| E_AppLet : forall x t e a,
|
||||
(expr_let x t a e) -->β (expr_subst x a e)
|
||||
|
||||
where "s '-->β' t" := (beta_step s t).
|
||||
|
||||
|
@ -102,43 +85,4 @@ 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 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.
|
||||
|
|
396
coq/soundness.v
396
coq/soundness.v
|
@ -16,402 +16,40 @@ Include Typing.
|
|||
|
||||
Module Soundness.
|
||||
|
||||
|
||||
Lemma typing_weakening : forall Γ e τ x σ,
|
||||
(Γ |- e \is τ) ->
|
||||
((ctx_assign x σ Γ) |- e \is τ)
|
||||
.
|
||||
Proof.
|
||||
intros.
|
||||
induction H.
|
||||
|
||||
apply T_Var.
|
||||
apply C_shuffle.
|
||||
apply H.
|
||||
|
||||
apply T_Let with (σ:=σ0).
|
||||
apply IHexpr_type1.
|
||||
admit.
|
||||
|
||||
Admitted.
|
||||
|
||||
|
||||
Lemma morphism_path_solves_type : forall Γ τ τ' m,
|
||||
(translate_morphism_path Γ τ τ' m) ->
|
||||
Γ |- m \is (type_morph τ τ')
|
||||
.
|
||||
Proof.
|
||||
intros.
|
||||
induction H.
|
||||
|
||||
(* Sub *)
|
||||
apply T_MorphAbs.
|
||||
apply T_DescendImplicit with (τ:=τ).
|
||||
apply T_Var.
|
||||
apply C_take.
|
||||
apply H.
|
||||
|
||||
(* Lift *)
|
||||
apply T_MorphAbs.
|
||||
apply T_Ascend.
|
||||
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 *)
|
||||
Definition is_stuck (e:expr_term) : Prop :=
|
||||
~(is_value e) ->
|
||||
~(exists e', e -->β e')
|
||||
.
|
||||
|
||||
(* the translation any well typed term is not stuck *)
|
||||
(* every well typed term is not stuck *)
|
||||
Lemma progress :
|
||||
forall Γ e τ e',
|
||||
forall (e:expr_term),
|
||||
(is_well_typed e) -> ~(is_stuck e)
|
||||
.
|
||||
Proof.
|
||||
|
||||
Admitted.
|
||||
|
||||
(* reduction step preserves well-typedness *)
|
||||
Lemma preservation :
|
||||
forall Γ e e' τ,
|
||||
(Γ |- e \is τ) ->
|
||||
(translate_typing Γ e τ e') ->
|
||||
~(is_stuck e')
|
||||
(e -->β e') ->
|
||||
(Γ |- e' \is τ)
|
||||
.
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
(* every well-typed expression is translated,
|
||||
* such that it be reduced to a value
|
||||
*)
|
||||
(* every well-typed expression can 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 τ))
|
||||
forall (e:expr_term),
|
||||
(is_well_typed e) ->
|
||||
(exists e', e -->β* e' /\ (is_value e'))
|
||||
.
|
||||
Proof.
|
||||
intros.
|
||||
|
||||
(* `e` is Variable *)
|
||||
induction H0.
|
||||
exists (expr_var x).
|
||||
split. apply Multi_Refl.
|
||||
split. apply V_Abs,VAbs_Var.
|
||||
apply H.
|
||||
|
||||
(* `e` is Let-Binding *)
|
||||
exists (expr_subst x e' t').
|
||||
split.
|
||||
apply Multi_Step with (y:=(expr_subst x e' t')).
|
||||
apply E_Let with (x:=x) (a:=e') (e:=t').
|
||||
apply Multi_Refl.
|
||||
(*
|
||||
split.
|
||||
unfold expr_subst.
|
||||
induction t'.
|
||||
|
||||
exists (expr_subst x e' (expr_var s)).
|
||||
split.
|
||||
unfold expr_subst.
|
||||
apply E_Let.
|
||||
*)
|
||||
admit.
|
||||
|
||||
(* `e` is Type-Abstraction *)
|
||||
exists (expr_ty_abs α e').
|
||||
split.
|
||||
apply Multi_Refl.
|
||||
split.
|
||||
apply V_Abs, VAbs_TypAbs.
|
||||
apply T_TypeAbs.
|
||||
apply translation_preservation with (e:=e).
|
||||
apply H0.
|
||||
apply H1.
|
||||
|
||||
(* `e` is Type-Application *)
|
||||
admit.
|
||||
|
||||
(* `e`is Abstraction *)
|
||||
exists (expr_abs x σ e').
|
||||
split. apply Multi_Refl.
|
||||
split. apply V_Abs, VAbs_Abs.
|
||||
apply T_Abs.
|
||||
apply translation_preservation with (e:=e).
|
||||
apply H0.
|
||||
apply H2.
|
||||
|
||||
(* `e` is Morphism Abstraction *)
|
||||
exists (expr_morph x σ e').
|
||||
split. apply Multi_Refl.
|
||||
split. apply V_Abs, VAbs_Morph.
|
||||
apply T_MorphAbs.
|
||||
apply translation_preservation with (e:=e).
|
||||
apply H0.
|
||||
apply H2.
|
||||
|
||||
(* `e` is Application *)
|
||||
admit.
|
||||
admit.
|
||||
|
||||
(* `e` is Ascension *)
|
||||
admit.
|
||||
|
||||
(* `e` is Descension *)
|
||||
admit.
|
||||
Admitted.
|
||||
|
||||
End Soundness.
|
||||
|
|
51
coq/terms.v
51
coq/terms.v
|
@ -30,35 +30,46 @@ Inductive expr_term : Type :=
|
|||
| expr_descend : type_term -> expr_term -> expr_term
|
||||
.
|
||||
|
||||
(* values *)
|
||||
Inductive is_abs_value : expr_term -> Prop :=
|
||||
| VAbs_Var : forall x,
|
||||
(is_abs_value (expr_var x))
|
||||
(* TODO
|
||||
|
||||
| VAbs_Abs : forall x τ e,
|
||||
(is_abs_value (expr_abs x τ e))
|
||||
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
|
||||
|
||||
| VAbs_Morph : forall x τ e,
|
||||
(is_abs_value (expr_morph x τ e))
|
||||
|
||||
| VAbs_TypAbs : forall τ e,
|
||||
(is_abs_value (expr_ty_abs τ e))
|
||||
Inductive expr_DeBruijn : Type :=
|
||||
| var : nat -> expr_DeBruijn
|
||||
| ty_abs : expr_DeBruijn -> expr_DeBruijn
|
||||
| ty_app : expr_DeBruijn -> type_DeBruijn -> expr_Debruijn
|
||||
| abs : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| morph : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn
|
||||
| app : expr_DeBruijn -> expr_DeBruijn -> expr_Debruijn
|
||||
| let : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn -> expr_Debruijn
|
||||
| ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
.
|
||||
*)
|
||||
|
||||
|
||||
|
||||
(* values *)
|
||||
Inductive is_value : expr_term -> Prop :=
|
||||
| V_Abs : forall e,
|
||||
(is_abs_value e) ->
|
||||
(is_value e)
|
||||
| V_Abs : forall x τ e,
|
||||
(is_value (expr_abs x τ e))
|
||||
|
||||
| V_TypAbs : forall τ e,
|
||||
(is_value (expr_ty_abs τ e))
|
||||
|
||||
| V_Ascend : forall τ e,
|
||||
(is_abs_value e) ->
|
||||
(is_value e) ->
|
||||
(is_value (expr_ascend τ e))
|
||||
|
||||
| V_Descend : forall τ e,
|
||||
(is_abs_value e) ->
|
||||
(is_value (expr_descend τ e))
|
||||
.
|
||||
|
||||
|
||||
Declare Scope ladder_type_scope.
|
||||
Declare Scope ladder_expr_scope.
|
||||
Declare Custom Entry ladder_type.
|
||||
|
@ -97,8 +108,6 @@ 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.
|
||||
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.
|
||||
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)
|
||||
(in custom ladder_expr at level 50) : ladder_expr_scope.
|
||||
Notation "'(' e ')'" := e
|
||||
|
|
48
coq/typing.v
48
coq/typing.v
|
@ -61,7 +61,8 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
|
|||
|
||||
| T_Ascend : forall Γ e τ τ',
|
||||
(Γ |- e \is τ) ->
|
||||
(Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))
|
||||
(τ' :<= τ) ->
|
||||
(Γ |- (expr_ascend τ' e) \is τ')
|
||||
|
||||
| T_DescendImplicit : forall Γ x τ τ',
|
||||
Γ |- x \is τ ->
|
||||
|
@ -76,8 +77,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
|
|||
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
|
||||
|
||||
Definition is_well_typed (e:expr_term) : Prop :=
|
||||
forall Γ,
|
||||
exists τ,
|
||||
exists Γ τ,
|
||||
Γ |- e \is τ
|
||||
.
|
||||
|
||||
|
@ -135,9 +135,10 @@ Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> P
|
|||
|
||||
| Expand_Ascend : forall Γ e e' τ τ',
|
||||
(Γ |- e \is τ) ->
|
||||
(Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
|
||||
(τ' :<= τ) ->
|
||||
(Γ |- (expr_ascend τ' e) \is τ') ->
|
||||
(translate_typing Γ e τ e') ->
|
||||
(translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))
|
||||
(translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
|
||||
|
||||
| Expand_Descend : forall Γ e e' τ τ',
|
||||
(Γ |- e \is τ) ->
|
||||
|
@ -218,6 +219,7 @@ Example typing4 : (is_well_typed
|
|||
).
|
||||
Proof.
|
||||
unfold is_well_typed.
|
||||
exists ctx_empty.
|
||||
exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
|
||||
apply T_TypeAbs.
|
||||
apply T_TypeAbs.
|
||||
|
@ -229,29 +231,24 @@ Qed.
|
|||
|
||||
Open Scope ladder_expr_scope.
|
||||
|
||||
Example typing5 :
|
||||
(ctx_assign "60" [< $"ℝ"$ >]
|
||||
(ctx_assign "360" [< $"ℝ"$ >]
|
||||
(ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
|
||||
ctx_empty)))
|
||||
|-
|
||||
Example typing5 : (is_well_typed
|
||||
[{
|
||||
let "deg2turns" :=
|
||||
(λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
|
||||
↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
|
||||
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
|
||||
↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$"ℝ"$))
|
||||
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$"ℝ"$) )
|
||||
}]
|
||||
\is
|
||||
[<
|
||||
$"Angle"$~$"Turns"$~$"ℝ"$
|
||||
>]
|
||||
.
|
||||
).
|
||||
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_MorphAbs.
|
||||
apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Turns"$>] [<$"ℝ"$>])).
|
||||
2: apply TSubRepr_Refl, TEq_LadderAssocLR.
|
||||
apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
|
||||
apply T_Ascend with (τ:=[< $"ℝ"$ >]).
|
||||
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
|
||||
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
|
||||
apply T_Var.
|
||||
|
@ -268,15 +265,18 @@ Proof.
|
|||
apply M_Sub.
|
||||
apply TSubRepr_Refl.
|
||||
apply TEq_Refl.
|
||||
apply TSubRepr_Ladder, TSubRepr_Ladder, 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_Ascend with (τ:=[<$"ℝ"$>]).
|
||||
apply T_Var.
|
||||
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.
|
||||
Qed.
|
||||
|
||||
|
|
Loading…
Reference in a new issue