From 61f1234fccee0bb836a3ff157c45005d360952e9 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 21 Aug 2024 20:04:20 +0200
Subject: [PATCH] coq: add 'compatible' typing relation

---
 coq/typing.v | 124 ++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 113 insertions(+), 11 deletions(-)

diff --git a/coq/typing.v b/coq/typing.v
index a7e74e9..316a27d 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -4,11 +4,18 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import subst.
+Require Import equiv.
+Require Import subtype.
+
 Include Terms.
 Include Subst.
+Include Equiv.
+Include Subtype.
 
 Module Typing.
 
+(** Typing Derivation *)
+
 Inductive context : Type :=
   | ctx_assign : string -> type_term -> context -> context
   | ctx_empty : context
@@ -52,22 +59,68 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     Γ |- a \is σ ->
     Γ |- (expr_tm_app f a) \is τ
 
+  | T_Sub : forall Γ x τ τ',
+    Γ |- x \is τ ->
+    (τ :<= τ') ->
+    Γ |- x \is τ'
+
 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 τ)
 
-  | T_Compatible : forall Γ x τ,
-    (Γ |- x \is τ) ->
-    (Γ |- x \compatible τ)
+  | T_CompatLet : forall Γ s (σ:type_term) t τ x,
+    (Γ |- s \compatible σ) ->
+    (Γ |- 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_tm_abs_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_tm_abs x σ t) \compatible (type_fun σ τ)
+
+  | T_CompatApp : forall Γ f a σ τ,
+    (Γ |- f \compatible (type_fun σ τ)) ->
+    (Γ |- a \compatible σ) ->
+    (Γ |- (expr_tm_app f a) \compatible τ)
+
+  | T_CompatImplicitCast : forall Γ h x τ τ',
+    (context_contains Γ h (type_morph τ τ')) ->
+    (Γ |- x \compatible τ) ->
+    (Γ |- x \compatible τ')
+
+  | T_CompatSub : forall Γ x τ τ',
+    (Γ |- x \compatible τ) ->
+    (τ ~<= τ') ->
+    (Γ |- x \compatible τ')
 
 where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
 
+
+(* Examples *)
+
+
 Example typing1 :
   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"))).
+  (context_contains Γ "x" [ %"T"% ]) ->
+  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"T", %"T"% -> %"T"% ].
+   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
   intros.
   apply T_TypeAbs.
@@ -75,15 +128,64 @@ Proof.
   apply H.
   apply T_Var.
   apply H.
-Admitted.
+Qed.
 
 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"))).
+  forall Γ,
+  (context_contains Γ "x" [ %"T"% ]) ->
+  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
+   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
+  intros.
+  apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
   apply T_TypeAbs.
   apply T_Abs.
-  
-Admitted.
+  apply H.
+  apply T_Var.
+  apply H.
+
+  apply TSubRepr_Refl.
+  apply TEq_Alpha.
+  apply TAlpha_Rename.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_VarReplace.
+Qed.
+
+Example typing3 :
+  forall Γ,
+  (context_contains Γ "x" [ %"T"% ]) ->
+  (context_contains Γ "y" [ %"U"% ]) ->
+  Γ |- [[ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"% ]] \is [ ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) ].
+Proof.
+  intros.
+  apply T_Sub with (τ:=[∀"T",∀"U",(%"T"%->%"U"%->%"U"%)]) (τ':=[∀"S",∀"T",(%"S"%->%"T"%->%"T"%)]).
+  apply T_TypeAbs, T_TypeAbs, T_Abs.
+  apply H.
+  apply T_Abs.
+  apply H0.
+  apply T_Var, H0.
+
+  apply TSubRepr_Refl.
+  apply TEq_Trans with (y:= [∀"S",∀"U",(%"S"%->%"U"%->%"U"%)] ).
+  apply TEq_Alpha.
+  apply TAlpha_Rename.
+  apply TSubst_UnivReplace. discriminate.
+  easy.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_Fun.
+  apply TSubst_VarKeep. discriminate.
+  apply TSubst_VarKeep. discriminate.
+
+  apply TEq_Alpha.
+  apply TAlpha_SubUniv.
+  apply TAlpha_Rename.
+  apply TSubst_Fun.
+  apply TSubst_VarKeep. discriminate.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_VarReplace.
+Qed.
 
 End Typing.