Compare commits

...

3 commits

4 changed files with 266 additions and 46 deletions

View file

@ -29,6 +29,7 @@
* 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.
@ -41,17 +42,55 @@ Module Equiv.
(** Alpha conversion in types *)
Reserved Notation "S '-->α' T" (at level 40).
Reserved Notation "S '--->α' T" (at level 40).
Inductive type_conv_alpha : type_term -> type_term -> Prop :=
| TEq_Alpha : forall x y t,
(type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
where "S '-->α' T" := (type_conv_alpha S T).
| TAlpha_Rename : forall x y t t',
(type_subst1 x (type_var y) t t') ->
(type_univ x t) --->α (type_univ y t')
| TAlpha_SubUniv : forall x τ τ',
(τ --->α τ') ->
(type_univ x τ) --->α (type_univ x τ')
| TAlpha_SubSpec1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
(type_spec τ1 τ2) --->α (type_spec τ1' τ2)
| TAlpha_SubSpec2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
(type_spec τ1 τ2) --->α (type_spec τ1 τ2')
| TAlpha_SubFun1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
(type_fun τ1 τ2) --->α (type_fun τ1' τ2)
| TAlpha_SubFun2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
(type_fun τ1 τ2) --->α (type_fun τ1 τ2')
| TAlpha_SubMorph1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
(type_morph τ1 τ2) --->α (type_morph τ1' τ2)
| TAlpha_SubMorph2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
(type_morph τ1 τ2) --->α (type_morph τ1 τ2')
| TAlpha_SubLadder1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
(type_ladder τ1 τ2) --->α (type_ladder τ1' τ2)
| TAlpha_SubLadder2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
(type_ladder τ1 τ2) --->α (type_ladder τ1 τ2')
where "S '--->α' T" := (type_conv_alpha S T).
(** Alpha conversion is symmetric *)
Lemma type_alpha_symm :
forall σ τ,
(σ -->α τ) -> (τ -->α σ).
(σ --->α τ) -> (τ --->α σ).
Proof.
(* TODO *)
Admitted.
@ -179,8 +218,8 @@ Inductive type_eq : type_term -> type_term -> Prop :=
y === z ->
x === z
| TEq_Rename : forall x y,
x -->α y ->
| TEq_Alpha : forall x y,
x --->α y ->
x === y
| TEq_Distribute : forall x y,
@ -196,7 +235,7 @@ where "S '===' T" := (type_eq S T).
(** Symmetry of === *)
Lemma type_eq_is_symmetric :
Lemma TEq_Symm :
forall x y,
(x === y) -> (y === x).
Proof.
@ -210,7 +249,7 @@ Proof.
apply IHtype_eq1.
apply type_alpha_symm in H.
apply TEq_Rename.
apply TEq_Alpha.
apply H.
apply TEq_Condense.
@ -224,9 +263,7 @@ Qed.
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop :=
| FlatUnit : (type_is_flat type_unit)
| FlatVar : forall x, (type_is_flat (type_var x))
| FlatNum : forall x, (type_is_flat (type_num x))
| FlatId : forall x, (type_is_flat (type_id x))
| FlatApp : forall x y,
(type_is_flat x) ->
@ -270,18 +307,21 @@ Proof.
intros τ H.
induction τ.
left.
apply FlatUnit.
left.
apply FlatId.
left.
apply FlatVar.
(*
left.
apply FlatNum.
apply IHτ1 in H.
apply FlatFun.
apply H.
destruct H.
destruct H.
apply IHτ1.
*)
admit.
admit.
admit.
@ -295,22 +335,11 @@ Proof.
intros.
destruct t.
exists type_unit.
split. apply TEq_Refl.
apply LNF.
admit.
exists (type_id s).
split. apply TEq_Refl.
apply LNF.
admit.
admit.
exists (type_num n).
split. apply TEq_Refl.
apply LNF.
admit.
admit.
exists (type_univ s t).
@ -342,11 +371,11 @@ Admitted.
*)
Example example_flat_type :
(type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
(type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
Proof.
apply FlatApp.
apply FlatId.
apply FlatNum.
apply FlatId.
Qed.
Example example_lnf_type :

View file

@ -4,6 +4,59 @@ Require Import terms.
Include Terms.
Module Subst.
(* Type Variable "x" is a free variable in type *)
Inductive type_var_free (x:string) : type_term -> Prop :=
| TFree_Var :
(type_var_free x (type_var x))
| TFree_Ladder : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_ladder τ1 τ2))
| TFree_Fun : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_fun τ1 τ2))
| TFree_Morph : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_morph τ1 τ2))
| TFree_Spec : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_spec τ1 τ2))
| TFree_Univ : forall y τ,
~(y = x) ->
(type_var_free x τ) ->
(type_var_free x (type_univ y τ))
.
Open Scope ladder_type_scope.
Example ex_type_free_var1 :
(type_var_free "T" (type_univ "U" (type_var "T")))
.
Proof.
apply TFree_Univ.
easy.
apply TFree_Var.
Qed.
Open Scope ladder_type_scope.
Example ex_type_free_var2 :
~(type_var_free "T" (type_univ "T" (type_var "T")))
.
Proof.
intro H.
inversion H.
contradiction.
Qed.
(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
match t0 with
@ -15,6 +68,44 @@ Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
| 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'))
.
(* 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

View file

@ -8,10 +8,8 @@ Module Terms.
(* types *)
Inductive type_term : Type :=
| type_unit : type_term
| type_id : string -> type_term
| type_var : string -> type_term
| type_num : nat -> type_term
| type_fun : type_term -> type_term -> type_term
| type_univ : string -> type_term -> type_term
| type_spec : type_term -> type_term -> type_term

View file

@ -4,11 +4,18 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Module Typing.
(** Typing Derivation *)
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
@ -52,22 +59,68 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
Γ |- a \is σ ->
Γ |- (expr_tm_app f a) \is τ
| T_Sub : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- x \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
| T_CompatVar : forall Γ x τ,
(context_contains Γ x τ) ->
(Γ |- (expr_var x) \compatible τ)
| T_Compatible : forall Γ x τ,
(Γ |- x \is τ) ->
(Γ |- x \compatible τ)
| T_CompatLet : forall Γ s (σ:type_term) t τ x,
(Γ |- s \compatible σ) ->
(Γ |- t \compatible τ) ->
(Γ |- (expr_let x σ s t) \compatible τ)
| T_CompatTypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
Γ |- e \compatible τ ->
Γ |- (expr_ty_abs α e) \compatible (type_univ α τ)
| T_CompatTypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
Γ |- e \compatible (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ)
| T_CompatMorphAbs : forall Γ x t τ τ',
Γ |- t \compatible τ ->
(τ ~<= τ') ->
Γ |- (expr_tm_abs_morph x τ t) \compatible (type_morph τ τ')
| T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
(context_contains Γ x σ) ->
Γ |- t \compatible τ ->
Γ |- (expr_tm_abs x σ t) \compatible (type_fun σ τ)
| T_CompatApp : forall Γ f a σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- (expr_tm_app f a) \compatible τ)
| T_CompatImplicitCast : forall Γ h x τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(Γ |- x \compatible τ) ->
(Γ |- x \compatible τ')
| T_CompatSub : forall Γ x τ τ',
(Γ |- x \compatible τ) ->
(τ ~<= τ') ->
(Γ |- x \compatible τ')
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
(* Examples *)
Example typing1 :
forall Γ,
(context_contains Γ "x" (type_var "T")) ->
Γ |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
(type_univ "T" (type_fun (type_var "T") (type_var "T"))).
(context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "T", %"T"% -> %"T"% ].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof.
intros.
apply T_TypeAbs.
@ -75,15 +128,64 @@ Proof.
apply H.
apply T_Var.
apply H.
Admitted.
Qed.
Example typing2 :
ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
(type_univ "T" (type_fun (type_var "T") (type_var "T"))).
forall Γ,
(context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "U", %"U"% -> %"U"% ].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof.
intros.
apply T_Sub with (τ:=["T",(%"T"% -> %"T"%)]).
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply H.
Admitted.
apply TSubRepr_Refl.
apply TEq_Alpha.
apply TAlpha_Rename.
apply TSubst_Fun.
apply TSubst_VarReplace.
apply TSubst_VarReplace.
Qed.
Example typing3 :
forall Γ,
(context_contains Γ "x" [ %"T"% ]) ->
(context_contains Γ "y" [ %"U"% ]) ->
Γ |- [[ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"% ]] \is [ "S","T",(%"S"%->%"T"%->%"T"%) ].
Proof.
intros.
apply T_Sub with (τ:=["T","U",(%"T"%->%"U"%->%"U"%)]) (τ':=["S","T",(%"S"%->%"T"%->%"T"%)]).
apply T_TypeAbs, T_TypeAbs, T_Abs.
apply H.
apply T_Abs.
apply H0.
apply T_Var, H0.
apply TSubRepr_Refl.
apply TEq_Trans with (y:= ["S","U",(%"S"%->%"U"%->%"U"%)] ).
apply TEq_Alpha.
apply TAlpha_Rename.
apply TSubst_UnivReplace. discriminate.
easy.
apply TSubst_Fun.
apply TSubst_VarReplace.
apply TSubst_Fun.
apply TSubst_VarKeep. discriminate.
apply TSubst_VarKeep. discriminate.
apply TEq_Alpha.
apply TAlpha_SubUniv.
apply TAlpha_Rename.
apply TSubst_Fun.
apply TSubst_VarKeep. discriminate.
apply TSubst_Fun.
apply TSubst_VarReplace.
apply TSubst_VarReplace.
Qed.
End Typing.