ladder-calculus/coq/typing.v

213 lines
5.8 KiB
Coq
Raw Normal View History

(* 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.
2024-08-21 20:04:20 +02:00
Require Import equiv.
Require Import subtype.
Include Terms.
Include Subst.
2024-08-21 20:04:20 +02:00
Include Equiv.
Include Subtype.
Module Typing.
2024-08-21 20:04:20 +02:00
(** Typing Derivation *)
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
.
Inductive context_contains : context -> string -> type_term -> Prop :=
| C_take : forall (x:string) (X:type_term) (Γ:context),
(context_contains (ctx_assign x X Γ) x X)
| C_shuffle : forall x X y Y Γ,
(context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X).
2024-07-27 13:30:12 +02:00
Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0).
Reserved Notation "Gamma '|-' x '\compatible' X" (at level 101, x at next level, X at level 0).
2024-07-27 13:30:12 +02:00
Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Var : forall Γ x τ,
(context_contains Γ x τ) ->
(Γ |- (expr_var x) \is τ)
2024-07-27 13:30:12 +02:00
| T_Let : forall Γ s (σ:type_term) t τ x,
(Γ |- s \is σ) ->
(Γ |- t \is τ) ->
(Γ |- (expr_let x σ s t) \is τ)
| T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
Γ |- e \is τ ->
Γ |- (expr_ty_abs α e) \is (type_univ α τ)
| T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
Γ |- e \is (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)
| T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
(context_contains Γ x σ) ->
Γ |- t \is τ ->
Γ |- (expr_abs x σ t) \is (type_fun σ τ)
2024-07-27 13:30:12 +02:00
| T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
Γ |- f \is (type_fun σ τ) ->
Γ |- a \is σ ->
Γ |- (expr_app f a) \is τ
2024-08-21 20:04:20 +02:00
| T_Sub : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- x \is τ'
2024-07-27 13:30:12 +02:00
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
2024-07-27 13:30:12 +02:00
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
2024-08-21 20:04:20 +02:00
| T_CompatVar : forall Γ x τ,
(context_contains Γ x τ) ->
(Γ |- (expr_var 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 α σ τ)
2024-08-21 20:04:20 +02:00
| T_CompatMorphAbs : forall Γ x t τ τ',
Γ |- t \compatible τ ->
(τ ~<= τ') ->
Γ |- (expr_morph x τ t) \compatible (type_morph τ τ')
2024-08-21 20:04:20 +02:00
| T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
(context_contains Γ x σ) ->
Γ |- t \compatible τ ->
Γ |- (expr_abs x σ t) \compatible (type_fun σ τ)
2024-08-21 20:04:20 +02:00
| T_CompatApp : forall Γ f a σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- (expr_app f a) \compatible τ)
2024-08-21 20:04:20 +02:00
| T_CompatImplicitCast : forall Γ h x τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(Γ |- x \compatible τ) ->
(Γ |- x \compatible τ')
| T_CompatSub : forall Γ x τ τ',
(Γ |- x \compatible τ) ->
(τ ~<= τ') ->
(Γ |- x \compatible τ')
2024-07-27 13:30:12 +02:00
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
Definition is_well_typed (e:expr_term) : Prop :=
exists Γ τ,
Γ |- e \compatible τ
.
2024-08-21 20:04:20 +02:00
(* Examples *)
Example typing1 :
2024-07-27 13:30:12 +02:00
forall Γ,
2024-08-21 20:04:20 +02:00
(context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "T", %"T"% -> %"T"% ].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
2024-07-27 13:30:12 +02:00
Proof.
intros.
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply H.
2024-08-21 20:04:20 +02:00
Qed.
2024-07-27 13:30:12 +02:00
Example typing2 :
2024-08-21 20:04:20 +02:00
forall Γ,
(context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "U", %"U"% -> %"U"% ].
Proof.
2024-08-21 20:04:20 +02:00
intros.
apply T_Sub with (τ:=["T",(%"T"% -> %"T"%)]).
2024-07-27 13:30:12 +02:00
apply T_TypeAbs.
apply T_Abs.
2024-08-21 20:04:20 +02:00
apply H.
apply T_Var.
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.
2024-08-22 08:31:14 +02:00
Example typing4 : (is_well_typed
[[ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"x"% ]]
).
Proof.
unfold is_well_typed.
exists (ctx_assign "x" [%"T"%]
(ctx_assign "y" [%"U"%] ctx_empty)).
exists [ "T","U",%"T"%->%"U"%->%"T"% ].
apply T_CompatTypeAbs.
apply T_CompatTypeAbs.
apply T_CompatAbs.
apply C_take.
apply T_CompatAbs.
apply C_shuffle. apply C_take.
apply T_CompatVar.
apply C_take.
Qed.
End Typing.