Compare commits

..

No commits in common. "61f1234fccee0bb836a3ff157c45005d360952e9" and "42ae93f2d7b12e800134fbc2fb8901362b974fd8" have entirely different histories.

4 changed files with 46 additions and 266 deletions

View file

@ -29,7 +29,6 @@
* rewrite-step of each other, `===` is symmetric and thus `===` * rewrite-step of each other, `===` is symmetric and thus `===`
* satisfies all properties required of an equivalence relation. * satisfies all properties required of an equivalence relation.
*) *)
Require Import terms. Require Import terms.
Require Import subst. Require Import subst.
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
@ -42,55 +41,17 @@ Module Equiv.
(** Alpha conversion in types *) (** 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 := Inductive type_conv_alpha : type_term -> type_term -> Prop :=
| TAlpha_Rename : forall x y t t', | TEq_Alpha : forall x y t,
(type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
(type_subst1 x (type_var y) t t') -> where "S '-->α' T" := (type_conv_alpha S 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 *) (** Alpha conversion is symmetric *)
Lemma type_alpha_symm : Lemma type_alpha_symm :
forall σ τ, forall σ τ,
(σ --->α τ) -> (τ --->α σ). (σ -->α τ) -> (τ -->α σ).
Proof. Proof.
(* TODO *) (* TODO *)
Admitted. Admitted.
@ -218,8 +179,8 @@ Inductive type_eq : type_term -> type_term -> Prop :=
y === z -> y === z ->
x === z x === z
| TEq_Alpha : forall x y, | TEq_Rename : forall x y,
x --->α y -> x -->α y ->
x === y x === y
| TEq_Distribute : forall x y, | TEq_Distribute : forall x y,
@ -235,7 +196,7 @@ where "S '===' T" := (type_eq S T).
(** Symmetry of === *) (** Symmetry of === *)
Lemma TEq_Symm : Lemma type_eq_is_symmetric :
forall x y, forall x y,
(x === y) -> (y === x). (x === y) -> (y === x).
Proof. Proof.
@ -249,7 +210,7 @@ Proof.
apply IHtype_eq1. apply IHtype_eq1.
apply type_alpha_symm in H. apply type_alpha_symm in H.
apply TEq_Alpha. apply TEq_Rename.
apply H. apply H.
apply TEq_Condense. apply TEq_Condense.
@ -263,7 +224,9 @@ Qed.
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *) (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop := Inductive type_is_flat : type_term -> Prop :=
| FlatUnit : (type_is_flat type_unit)
| FlatVar : forall x, (type_is_flat (type_var x)) | 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)) | FlatId : forall x, (type_is_flat (type_id x))
| FlatApp : forall x y, | FlatApp : forall x y,
(type_is_flat x) -> (type_is_flat x) ->
@ -306,22 +269,19 @@ Lemma lnf_shape :
Proof. Proof.
intros τ H. intros τ H.
induction τ. induction τ.
left.
apply FlatUnit.
left. left.
apply FlatId. apply FlatId.
left. left.
apply FlatVar. apply FlatVar.
(*
left. left.
apply IHτ1 in H. apply FlatNum.
apply FlatFun.
apply H.
destruct H.
destruct H.
apply IHτ1.
*)
admit. admit.
admit. admit.
admit. admit.
@ -335,11 +295,22 @@ Proof.
intros. intros.
destruct t. destruct t.
exists type_unit.
split. apply TEq_Refl.
apply LNF.
admit.
exists (type_id s). exists (type_id s).
split. apply TEq_Refl. split. apply TEq_Refl.
apply LNF. apply LNF.
admit. admit.
admit. admit.
exists (type_num n).
split. apply TEq_Refl.
apply LNF.
admit.
admit. admit.
exists (type_univ s t). exists (type_univ s t).
@ -371,11 +342,11 @@ Admitted.
*) *)
Example example_flat_type : Example example_flat_type :
(type_is_flat (type_spec (type_id "PosInt") (type_id "10"))). (type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
Proof. Proof.
apply FlatApp. apply FlatApp.
apply FlatId. apply FlatId.
apply FlatId. apply FlatNum.
Qed. Qed.
Example example_lnf_type : Example example_lnf_type :

View file

@ -1,62 +1,9 @@
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
Require Import terms. Require Import terms.
Include Terms. Include Terms.
Module Subst. 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}$ *) (* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) := Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
match t0 with match t0 with
@ -68,44 +15,6 @@ Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
| t => t | t => t
end. 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 *) (* scoped variable substitution, replaces free occurences of v with n in expression e *)
Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) := Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
match e0 with match e0 with

View file

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

View file

@ -4,18 +4,11 @@
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
Require Import terms. Require Import terms.
Require Import subst. Require Import subst.
Require Import equiv.
Require Import subtype.
Include Terms. Include Terms.
Include Subst. Include Subst.
Include Equiv.
Include Subtype.
Module Typing. Module Typing.
(** Typing Derivation *)
Inductive context : Type := Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context | ctx_assign : string -> type_term -> context -> context
| ctx_empty : context | ctx_empty : context
@ -59,68 +52,22 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
Γ |- a \is σ -> Γ |- a \is σ ->
Γ |- (expr_tm_app f a) \is τ Γ |- (expr_tm_app f a) \is τ
| T_Sub : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- x \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ). where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop := Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
| T_CompatVar : forall Γ x τ,
(context_contains Γ x τ) ->
(Γ |- (expr_var x) \compatible τ)
| T_CompatLet : forall Γ s (σ:type_term) t τ x, | T_Compatible : forall Γ x τ,
(Γ |- s \compatible σ) -> (Γ |- x \is τ) ->
(Γ |- t \compatible τ) -> (Γ |- x \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 τ). where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
(* Examples *)
Example typing1 : Example typing1 :
forall Γ, forall Γ,
(context_contains Γ "x" [ %"T"% ]) -> (context_contains Γ "x" (type_var "T")) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "T", %"T"% -> %"T"% ]. Γ |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *) (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
Proof. Proof.
intros. intros.
apply T_TypeAbs. apply T_TypeAbs.
@ -128,64 +75,15 @@ Proof.
apply H. apply H.
apply T_Var. apply T_Var.
apply H. apply H.
Qed. Admitted.
Example typing2 : Example typing2 :
forall Γ, ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
(context_contains Γ "x" [ %"T"% ]) -> (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "U", %"U"% -> %"U"% ].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof. Proof.
intros.
apply T_Sub with (τ:=["T",(%"T"% -> %"T"%)]).
apply T_TypeAbs. apply T_TypeAbs.
apply T_Abs. apply T_Abs.
apply H.
apply T_Var. Admitted.
apply H.
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. End Typing.