coq: preliminary definition of typing-relation

coq/typing.v

@@ -0,0 +1,55 @@
+(* 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.