coq: add 'compatible' typing relation

This commit is contained in:
Michael Sippel 2024-08-21 20:04:20 +02:00
parent 361d03c117
commit 61f1234fcc
Signed by: senvas
GPG key ID: 060F22F65102F95C

View file

@ -4,11 +4,18 @@
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
Require Import terms. Require Import terms.
Require Import subst. Require Import subst.
Require Import equiv.
Require Import subtype.
Include Terms. Include Terms.
Include Subst. Include Subst.
Include Equiv.
Include Subtype.
Module Typing. Module Typing.
(** Typing Derivation *)
Inductive context : Type := Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context | ctx_assign : string -> type_term -> context -> context
| ctx_empty : context | ctx_empty : context
@ -52,22 +59,68 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
Γ |- a \is σ -> Γ |- a \is σ ->
Γ |- (expr_tm_app f a) \is τ Γ |- (expr_tm_app f a) \is τ
| T_Sub : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- x \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ). where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop := 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 τ, | T_CompatLet : forall Γ s (σ:type_term) t τ x,
(Γ |- x \is τ) -> (Γ |- s \compatible σ) ->
(Γ |- x \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 τ). where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
(* Examples *)
Example typing1 : Example typing1 :
forall Γ, forall Γ,
(context_contains Γ "x" (type_var "T")) -> (context_contains Γ "x" [ %"T"% ]) ->
Γ |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "T", %"T"% -> %"T"% ].
(type_univ "T" (type_fun (type_var "T") (type_var "T"))). (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof. Proof.
intros. intros.
apply T_TypeAbs. apply T_TypeAbs.
@ -75,15 +128,64 @@ Proof.
apply H. apply H.
apply T_Var. apply T_Var.
apply H. apply H.
Admitted. Qed.
Example typing2 : Example typing2 :
ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is forall Γ,
(type_univ "T" (type_fun (type_var "T") (type_var "T"))). (context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "U", %"U"% -> %"U"% ].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof. Proof.
intros.
apply T_Sub with (τ:=["T",(%"T"% -> %"T"%)]).
apply T_TypeAbs. apply T_TypeAbs.
apply T_Abs. apply T_Abs.
apply H.
Admitted. 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. End Typing.