coq: wip typing

coq/typing.v

@@ -21,35 +21,69 @@ Inductive context_contains : context -> string -> type_term -> Prop :=
     (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).
+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).
 
-Inductive expr_type : context -> expr -> ladder_type -> Prop :=
-  | T_Var : forall Γ x X,
-    (context_contains Γ x X) ->
-    Γ |- x \in X
+Inductive expr_type : context -> expr_term -> type_term -> Prop :=
+  | T_Var : forall Γ x τ,
+    (context_contains Γ x τ) ->
+    (Γ |- x \is τ)
 
-  | T_Let : forall Γ s (σ:ladder_type) t τ x,
-    Γ |- s \in σ ->
-    Γ |- t \in τ ->
-    Γ |- (expr_let x σ s t) \in τ
+  | T_Let : forall Γ s (σ:type_term) t τ x,
+    (Γ |- s \is σ) ->
+    (Γ |- t \is τ) ->
+    (Γ |- (expr_let x σ s t) \is τ)
 
-  | 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_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
+    Γ |- e \is τ ->
+    Γ |- (expr_ty_abs α e) \is (type_univ α τ)
 
-  | 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
+  | T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
+    Γ |- e \is (type_univ α τ) ->
+    Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)
 
-where "Γ '|-' x '\in' X" := (expr_type Γ x X).
+  | 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 σ τ)
 
+  | 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 τ
+
+where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
+
+
+Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
+
+  | T_Compatible : forall Γ x τ,
+    (Γ |- x \is τ) ->
+    (Γ |- x \compatible τ)
+
+where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
 
 Example typing1 :
-  ctx_empty |-
-  (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \in
+  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
+    (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
+Proof.
+  apply T_TypeAbs.
+  apply T_Abs.
+  
 Admitted.
 
 End Typing.