senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

coq: change notation brackets for terms

Browse source
This commit is contained in:
Michael Sippel 2024-08-22 09:57:47 +02:00
parent 719cb8ec4a
commit b978637b57
Signed by: senvas
GPG key ID: F96CF119C34B64A6
3 changed files with 35 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
coq/subtype.v
View file

@ -61,10 +61,14 @@ Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Example sub0 :
[ < $"Seq"$ < $"Digit"$ $"10"$ > >
~ < $"Seq"$ $"Char"$ > ]
[<
< $"Seq"$ < $"Digit"$ $"10"$ > >
~ < $"Seq"$ $"Char"$ >
>]
:<=
[ < $"Seq"$ $"Char"$ > ]
[<
< $"Seq"$ $"Char"$ >
>]
.
Proof.
apply TSubRepr_Ladder.
@ -74,13 +78,13 @@ Qed.
Example sub1 :
[ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ]
:<= [ < $"Seq"$ $"Char"$ > ]
[< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >]
:<= [< < $"Seq"$ $"Char"$ > >]
.
Proof.
set [ < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > ].
set [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ].
set [ < $"Seq"$ $"Char"$ > ].
set [< < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > >].
set [< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >].
set [< < $"Seq"$ $"Char"$ > >].
set (t0 === t).
set (t :<= t0).
set (t :<= t1).

10
coq/terms.v
View file

@ -50,7 +50,7 @@ Declare Scope ladder_expr_scope.
Declare Custom Entry ladder_type.
Declare Custom Entry ladder_expr.
Notation "[ t ]" := t
Notation "[< t >]" := t
(t custom ladder_type at level 80) : ladder_type_scope.
Notation "'∀' x ',' t" := (type_univ x t)
(t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
@ -69,7 +69,7 @@ Notation "'$' x '$'" := (type_id x%string)
Notation "'%' x '%'" := (type_var x%string)
(in custom ladder_type at level 0, x constr) : ladder_type_scope.
Notation "[[ e ]]" := e
Notation "[{ e }]" := e
(e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "'%' x '%'" := (expr_var x%string)
(in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
@ -84,10 +84,10 @@ Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Check [ ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) ].
Check [< ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
Definition polymorphic_identity1 : expr_term := [[ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% ]].
Definition polymorphic_identity2 : expr_term := [[ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% ]].
Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% }].
Definition polymorphic_identity2 : expr_term := [{ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% }].
Compute polymorphic_identity1.

32
coq/typing.v
View file

@ -121,8 +121,8 @@ Definition is_well_typed (e:expr_term) : Prop :=
Example typing1 :
forall Γ,
(context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"T", %"T"% -> %"T"% ].
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof.
intros.
@ -135,11 +135,11 @@ Qed.
Example typing2 :
forall Γ,
(context_contains Γ "x" [ %"T"% ]) ->
Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
Proof.
intros.
apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
apply T_Sub with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
apply T_TypeAbs.
apply T_Abs.
apply H.
@ -156,12 +156,16 @@ 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"%) ].
(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_Sub with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
apply T_TypeAbs, T_TypeAbs, T_Abs.
apply H.
apply T_Abs.
@ -169,7 +173,7 @@ Proof.
apply T_Var, H0.
apply TSubRepr_Refl.
apply TEq_Trans with (y:= [∀"S",∀"U",(%"S"%->%"U"%->%"U"%)] ).
apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
apply TEq_Alpha.
apply TAlpha_Rename.
apply TSubst_UnivReplace. discriminate.
@ -192,13 +196,13 @@ Qed.
Example typing4 : (is_well_typed
[[ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% ]]
[{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
).
Proof.
unfold is_well_typed.
exists (ctx_assign "x" [%"T"%]
(ctx_assign "y" [%"U"%] ctx_empty)).
exists [ ∀"T",∀"U",%"T"%->%"U"%->%"T"% ].
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.