work on typing rules

coq/typing.v

@@ -59,7 +59,21 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     Γ |- a \is σ ->
     Γ |- (expr_app f a) \is τ
 
-  | T_Sub : forall Γ x τ τ',
+  | T_MorphAbs : forall Γ x σ e τ,
+    (context_contains Γ x σ) ->
+    Γ |- e \is τ ->
+    Γ |- (expr_morph x σ e) \is (type_morph σ τ)
+
+  | T_MorphFun : forall Γ f σ τ,
+    Γ |- f \is (type_morph σ τ) ->
+    Γ |- f \is (type_fun σ τ)
+
+  | T_Ascend : forall Γ e τ τ',
+    (Γ |- e \is τ) ->
+    (τ' :<= τ) ->
+    (Γ |- (expr_ascend τ' e) \is τ')
+
+  | T_Descend : forall Γ x τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
     Γ |- x \is τ'
@@ -68,44 +82,31 @@ where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 
 Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
-  | T_CompatVar : forall Γ x τ,
-    (context_contains Γ x τ) ->
-    (Γ |- (expr_var x) \compatible τ)
+  | TCompat_Native : forall Γ e τ,
+    (Γ |- e \is τ) ->
+    (Γ |- e \compatible τ)
 
-  | T_CompatLet : forall Γ s (σ:type_term) t τ x,
-    (Γ |- s \compatible σ) ->
+  | TCompat_Let : forall Γ s (σ:type_term) t τ x,
+    (Γ |- s \is σ) ->
+    (context_contains Γ x σ) ->
     (Γ |- 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 α σ τ)
 
-  | T_CompatMorphAbs : forall Γ x t τ τ',
-    Γ |- t \compatible τ ->
-    (τ ~<= τ') ->
-    Γ |- (expr_morph x τ t) \compatible (type_morph τ τ')
-
-  | 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 σ τ)
-
-  | T_CompatApp : forall Γ f a σ τ,
+  | TCompat_App : forall Γ f a σ τ,
     (Γ |- f \compatible (type_fun σ τ)) ->
     (Γ |- a \compatible σ) ->
     (Γ |- (expr_app f a) \compatible τ)
 
-  | T_CompatImplicitCast : forall Γ h x τ τ',
+  | TCompat_Morph : forall Γ h x τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
     (Γ |- x \compatible τ) ->
     (Γ |- x \compatible τ')
 
-  | T_CompatSub : forall Γ x τ τ',
+  | TCompat_Sub : forall Γ x τ τ',
     (Γ |- x \compatible τ) ->
     (τ ~<= τ') ->
     (Γ |- x \compatible τ')
@@ -117,6 +118,11 @@ Definition is_well_typed (e:expr_term) : Prop :=
   Γ |- e \compatible τ
 .
 
+Definition is_exactly_typed (e:expr_term) : Prop :=
+  exists Γ τ,
+  Γ |- e \is τ
+.
+
 (* Examples *)
 
 Example typing1 :
@@ -139,7 +145,7 @@ Example typing2 :
   Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
 Proof.
   intros.
-  apply T_Sub with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
+  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
   apply T_TypeAbs.
   apply T_Abs.
   apply H.
@@ -165,7 +171,7 @@ Example typing3 :
   >].
 Proof.
   intros.
-  apply T_Sub with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
+  apply T_Descend with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
   apply T_TypeAbs, T_TypeAbs, T_Abs.
   apply H.
   apply T_Abs.
@@ -203,13 +209,14 @@ Proof.
   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 TCompat_Native.
+  apply T_TypeAbs.
+  apply T_TypeAbs.
+  apply T_Abs.
   apply C_take.
-  apply T_CompatAbs.
+  apply T_Abs.
   apply C_shuffle. apply C_take.
-  apply T_CompatVar.
+  apply T_Var.
   apply C_take.
 Qed.