56 lines
1.5 KiB
Coq
56 lines
1.5 KiB
Coq
|
(* This module defines the typing relation
|
|||
|
|
* where each expression is assigned a type.
|
|||
|
|
*)
|
|||
|
|
From Coq Require Import Strings.String.
|
|||
|
|
Require Import terms.
|
|||
|
|
|
|||
|
|
Include Terms.
|
|||
|
|
|
|||
|
|
|
|||
|
|
Module Typing.
|
|||
|
|
|
|||
|
|
Inductive context : Type :=
|
|||
|
|
| ctx_assign : string -> ladder_type -> context -> context
|
|||
|
|
| ctx_empty : context
|
|||
|
|
.
|
|||
|
|
|
|||
|
|
Inductive context_contains : context -> string -> ladder_type -> Prop :=
|
|||
|
|
| C_take : forall (x:string) (X:ladder_type) (Γ: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).
|
|||
|
|
|
|||
|
|
Reserved Notation "Gamma '|-' x '\in' X" (at level 101, x at next level, X at level 0).
|
|||
|
|
|
|||
|
|
Inductive expr_type : context -> expr -> ladder_type -> Prop :=
|
|||
|
|
| T_Var : forall Γ x X,
|
|||
|
|
(context_contains Γ x X) ->
|
|||
|
|
Γ |- x \in X
|
|||
|
|
|
|||
|
|
| T_Let : forall Γ s (σ:ladder_type) t τ x,
|
|||
|
|
Γ |- s \in σ ->
|
|||
|
|
Γ |- t \in τ ->
|
|||
|
|
Γ |- (expr_let x σ s t) \in τ
|
|||
|
|
|
|||
|
|
| T_Abs : forall (Γ:context) (x:string) (X:ladder_type) (t:expr) (T:ladder_type),
|
|||
|
|
Γ |- t \in T ->
|
|||
|
|
Γ |- (expr_tm_abs x X t) \in (type_fun X T)
|
|||
|
|
|
|||
|
|
| T_App : forall (Γ:context) (f:expr) (a:expr) (S:ladder_type) (T:ladder_type),
|
|||
|
|
Γ |- f \in (type_fun S T) ->
|
|||
|
|
Γ |- a \in S ->
|
|||
|
|
Γ |- (expr_tm_app f a) \in T
|
|||
|
|
|
|||
|
|
where "Γ '|-' x '\in' X" := (expr_type Γ x X).
|
|||
|
|
|
|||
|
|
|
|||
|
|
Example typing1 :
|
|||
|
|
ctx_empty |-
|
|||
|
|
(expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \in
|
|||
|
|
(type_abs "T" (type_fun (type_var "T") (type_var "T"))).
|
|||
|
|
Proof.
|
|||
|
|
Admitted.
|
|||
|
|
|
|||
|
|
End Typing.
|