383 lines
11 KiB
Coq
383 lines
11 KiB
Coq
(* 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.
|