2024-07-24 11:19:57 +02:00
|
|
|
|
(* This module defines the typing relation
|
|
|
|
|
* where each expression is assigned a type.
|
|
|
|
|
*)
|
|
|
|
|
From Coq Require Import Strings.String.
|
|
|
|
|
Require Import terms.
|
2024-07-25 11:04:56 +02:00
|
|
|
|
Require Import subst.
|
2024-07-24 11:19:57 +02:00
|
|
|
|
Include Terms.
|
2024-07-25 11:04:56 +02:00
|
|
|
|
Include Subst.
|
2024-07-24 11:19:57 +02:00
|
|
|
|
|
|
|
|
|
Module Typing.
|
|
|
|
|
|
|
|
|
|
Inductive context : Type :=
|
2024-07-25 11:04:56 +02:00
|
|
|
|
| ctx_assign : string -> type_term -> context -> context
|
2024-07-24 11:19:57 +02:00
|
|
|
|
| ctx_empty : context
|
|
|
|
|
.
|
|
|
|
|
|
2024-07-25 11:04:56 +02:00
|
|
|
|
Inductive context_contains : context -> string -> type_term -> Prop :=
|
|
|
|
|
| C_take : forall (x:string) (X:type_term) (Γ:context),
|
2024-07-24 11:19:57 +02:00
|
|
|
|
(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-24 11:19:57 +02:00
|
|
|
|
|
2024-07-27 13:30:12 +02:00
|
|
|
|
Inductive expr_type : context -> expr_term -> type_term -> Prop :=
|
|
|
|
|
| T_Var : forall Γ x τ,
|
|
|
|
|
(context_contains Γ x τ) ->
|
2024-08-18 10:27:21 +02:00
|
|
|
|
(Γ |- (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_tm_abs x σ t) \is (type_fun σ τ)
|
2024-07-24 11:19:57 +02:00
|
|
|
|
|
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_tm_app f a) \is τ
|
2024-07-24 11:19:57 +02:00
|
|
|
|
|
2024-07-27 13:30:12 +02:00
|
|
|
|
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
|
2024-07-24 11:19:57 +02:00
|
|
|
|
|
|
|
|
|
|
2024-07-27 13:30:12 +02:00
|
|
|
|
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
|
2024-07-24 11:19:57 +02:00
|
|
|
|
|
2024-07-27 13:30:12 +02:00
|
|
|
|
| T_Compatible : forall Γ x τ,
|
|
|
|
|
(Γ |- x \is τ) ->
|
|
|
|
|
(Γ |- x \compatible τ)
|
|
|
|
|
|
|
|
|
|
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
|
2024-07-24 11:19:57 +02:00
|
|
|
|
|
|
|
|
|
Example typing1 :
|
2024-07-27 13:30:12 +02:00
|
|
|
|
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"))).
|
|
|
|
|
Proof.
|
|
|
|
|
intros.
|
|
|
|
|
apply T_TypeAbs.
|
|
|
|
|
apply T_Abs.
|
|
|
|
|
apply H.
|
|
|
|
|
apply T_Var.
|
|
|
|
|
apply H.
|
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
Example typing2 :
|
|
|
|
|
ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
|
2024-07-25 11:04:56 +02:00
|
|
|
|
(type_univ "T" (type_fun (type_var "T") (type_var "T"))).
|
2024-07-24 11:19:57 +02:00
|
|
|
|
Proof.
|
2024-07-27 13:30:12 +02:00
|
|
|
|
apply T_TypeAbs.
|
|
|
|
|
apply T_Abs.
|
|
|
|
|
|
2024-07-24 11:19:57 +02:00
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
End Typing.
|