coq: typing relation fix ctx assignments in premisse

This commit is contained in:
Michael Sippel 2024-09-08 15:32:54 +02:00
parent b44e443879
commit 4b3358372e
Signed by: senvas
GPG key ID: F96CF119C34B64A6

View file

@ -29,25 +29,24 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Let : forall Γ s σ t τ x,
(Γ |- s \is σ) ->
(Γ |- t \is τ) ->
(Γ |- (expr_let x σ s t) \is τ)
((ctx_assign x σ Γ) |- t \is τ) ->
(Γ |- (expr_let x s t) \is τ)
| T_TypeAbs : forall Γ e τ α,
Γ |- e \is τ ->
Γ |- (expr_ty_abs α e) \is (type_univ α τ)
| T_TypeApp : forall Γ α e σ τ,
| T_TypeApp : forall Γ α e σ τ τ',
Γ |- e \is (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)
(type_subst1 α σ τ τ') ->
Γ |- (expr_ty_app e σ) \is τ'
| T_Abs : forall Γ x σ t τ,
(context_contains Γ x σ) ->
Γ |- t \is τ ->
Γ |- (expr_abs x σ t) \is (type_fun σ τ)
((ctx_assign x σ Γ) |- t \is τ) ->
(Γ |- (expr_abs x σ t) \is (type_fun σ τ))
| T_MorphAbs : forall Γ x σ e τ,
(context_contains Γ x σ) ->
Γ |- e \is τ ->
((ctx_assign x σ Γ) |- e \is τ) ->
Γ |- (expr_morph x σ e) \is (type_morph σ τ)
| T_App : forall Γ f a σ' σ τ,
@ -80,31 +79,24 @@ Definition is_well_typed (e:expr_term) : Prop :=
(* Examples *)
Example typing1 :
forall Γ,
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
ctx_empty |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >].
Proof.
intros.
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply H.
apply C_take.
Qed.
Example typing2 :
forall Γ,
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >].
ctx_empty |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >].
Proof.
intros.
apply T_Descend with (τ:=[< "T",(%"T"% -> %"T"%) >]).
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply H.
apply C_take.
apply TSubRepr_Refl.
apply TEq_Alpha.
@ -115,10 +107,7 @@ Proof.
Qed.
Example typing3 :
forall Γ,
(context_contains Γ "x" [< %"T"% >]) ->
(context_contains Γ "y" [< %"U"% >]) ->
Γ |- [{
ctx_empty |- [{
Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"%
}] \is [<
"S","T",(%"S"%->%"T"%->%"T"%)
@ -127,10 +116,9 @@ Proof.
intros.
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.
apply H0.
apply T_Var, H0.
apply T_Var.
apply C_take.
apply TSubRepr_Refl.
apply TEq_Trans with (y:= [< "S","U",(%"S"%->%"U"%->%"U"%) >] ).
@ -159,13 +147,11 @@ Example typing4 : (is_well_typed
).
Proof.
unfold is_well_typed.
exists (ctx_assign "x" [< %"T"% >]
(ctx_assign "y" [< %"U"% >] ctx_empty)).
exists ctx_empty.
exists [< "T","U",%"T"%->%"U"%->%"T"% >].
apply T_TypeAbs.
apply T_TypeAbs.
apply T_Abs.
apply C_take.
apply T_Abs.
apply C_shuffle. apply C_take.
apply T_Var.