Compare commits

...

5 commits

7 changed files with 226 additions and 58 deletions

View file

@ -4,6 +4,7 @@ equiv.v
subst.v subst.v
subtype.v subtype.v
typing.v typing.v
morph.v
smallstep.v smallstep.v
soundness.v
bbencode.v bbencode.v

68
coq/morph.v Normal file
View file

@ -0,0 +1,68 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import typing.
Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Include Typing.
Module Morph.
Reserved Notation "Γ '|-' '[[' e ']]' '=' t" (at level 101, e at next level, t at level 0).
Inductive expand_morphisms : context -> expr_term -> expr_term -> Prop :=
| Expand_Transform : forall Γ e h τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(Γ |- e \is τ) ->
(Γ |- [[ e ]] = (expr_app (expr_var h) e))
| Expand_Otherwise : forall Γ e,
(Γ |- [[ e ]] = e)
| Expand_App : forall Γ f f' a a' σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- [[ f ]] = f') ->
(Γ |- [[ a ]] = a') ->
(Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t).
(* For every well-typed term, there is an expanded exactly typed term *)
Lemma well_typed_is_expandable :
forall (e:expr_term),
(is_well_typed e) ->
exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e')
.
Proof.
Admitted.
Example expand1 :
(ctx_assign "morph-radix"
[< <%"PosInt"% %"16"%> ->morph <%"PosInt"% %"10"%> >]
(ctx_assign "fn-decimal"
[< <%"PosInt"% %"10"%> -> <%"PosInt"% %"10"%> >]
(ctx_assign "x"
[< <%"PosInt"% %"16"%> >]
ctx_empty)))
|- [[ (expr_app (expr_var "fn-decimal") (expr_var "x")) ]]
= (expr_app (expr_var "fn-decimal")
(expr_app (expr_var "morph-radix") (expr_var "x")))
.
Proof.
apply Expand_App with (f':=(expr_var "fn-decimal")) (σ:=[< < %"PosInt"% %"10"% > >]) (τ:=[< < %"PosInt"% %"10"% > >]).
apply TCompat_Native.
Admitted.
End Morph.

View file

@ -52,9 +52,10 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
e1 -->β e1' -> e1 -->β e1' ->
(expr_app e1 e2) -->β (expr_app e1' e2) (expr_app e1 e2) -->β (expr_app e1' e2)
| E_App2 : forall e1 e2 e2', | E_App2 : forall v1 e2 e2',
(is_value v1) ->
e2 -->β e2' -> e2 -->β e2' ->
(expr_app e1 e2) -->β (expr_app e1 e2') (expr_app v1 e2) -->β (expr_app v1 e2')
| E_TypApp : forall e e' τ, | E_TypApp : forall e e' τ,
e -->β e' -> e -->β e' ->

83
coq/soundness.v Normal file
View file

@ -0,0 +1,83 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import smallstep.
Require Import typing.
Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Include Smallstep.
Include Typing.
Module Soundness.
(* e is stuck when it is neither a value, nor can it be reduced *)
Definition is_stuck (e:expr_term) : Prop :=
~(is_value e) ->
~(exists e', e -->β e')
.
(* every exactly typed term is not stuck *)
Lemma exact_progress :
forall (e:expr_term),
(is_exactly_typed e) -> ~(is_stuck e)
.
Proof.
Admitted.
(* every well typed term is not stuck *)
Lemma progress :
forall (e:expr_term),
(is_well_typed e) -> ~(is_stuck e)
.
Proof.
Admitted.
(* reduction step preserves the type *)
Lemma exact_preservation :
forall Γ e e' τ,
(Γ |- e \is τ) ->
(e -->β e') ->
(Γ |- e' \is τ)
.
Proof.
(*
intros.
generalize dependent e'.
induction H.
intros e' I.
inversion I.
*)
Admitted.
(* reduction step preserves well-typedness *)
Lemma preservation :
forall Γ e e' τ,
(Γ |- e \compatible τ) ->
(e -->β e') ->
(Γ |- e' \compatible τ)
.
Proof.
Admitted.
(* every well-typed expression can be reduced to a value *)
Theorem soundness :
forall (e:expr_term),
(is_well_typed e) ->
(exists e', e -->β* e' /\ (is_value e'))
.
Proof.
intros.
Admitted.
End Soundness.

View file

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

View file

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

View file

@ -59,7 +59,21 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
Γ |- a \is σ -> Γ |- a \is σ ->
Γ |- (expr_app f 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 τ ->
(τ :<= τ') -> (τ :<= τ') ->
Γ |- x \is τ' Γ |- x \is τ'
@ -68,44 +82,31 @@ 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 τ, | TCompat_Native : forall Γ e τ,
(context_contains Γ x τ) -> (Γ |- e \is τ) ->
(Γ |- (expr_var x) \compatible τ) (Γ |- e \compatible τ)
| T_CompatLet : forall Γ s (σ:type_term) t τ x, | TCompat_Let : forall Γ s (σ:type_term) t τ x,
(Γ |- s \compatible σ) -> (Γ |- s \is σ) ->
(context_contains Γ x σ) ->
(Γ |- t \compatible τ) -> (Γ |- t \compatible τ) ->
(Γ |- (expr_let x σ s 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), | T_CompatTypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
Γ |- e \compatible (type_univ α τ) -> Γ |- e \compatible (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ) Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ)
| T_CompatMorphAbs : forall Γ x t τ τ', | TCompat_App : forall Γ f a σ τ,
Γ |- 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 σ τ,
(Γ |- f \compatible (type_fun σ τ)) -> (Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) -> (Γ |- a \compatible σ) ->
(Γ |- (expr_app f a) \compatible τ) (Γ |- (expr_app f a) \compatible τ)
| T_CompatImplicitCast : forall Γ h x τ τ', | TCompat_Morph : forall Γ h x τ τ',
(context_contains Γ h (type_morph τ τ')) -> (context_contains Γ h (type_morph τ τ')) ->
(Γ |- x \compatible τ) -> (Γ |- x \compatible τ) ->
(Γ |- x \compatible τ') (Γ |- x \compatible τ')
| T_CompatSub : forall Γ x τ τ', | TCompat_Sub : forall Γ x τ τ',
(Γ |- x \compatible τ) -> (Γ |- x \compatible τ) ->
(τ ~<= τ') -> (τ ~<= τ') ->
(Γ |- x \compatible τ') (Γ |- x \compatible τ')
@ -117,12 +118,17 @@ Definition is_well_typed (e:expr_term) : Prop :=
Γ |- e \compatible τ Γ |- e \compatible τ
. .
Definition is_exactly_typed (e:expr_term) : Prop :=
exists Γ τ,
Γ |- e \is τ
.
(* Examples *) (* Examples *)
Example typing1 : Example typing1 :
forall Γ, forall Γ,
(context_contains Γ "x" [ %"T"% ]) -> (context_contains Γ "x" [< %"T"% >]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "T", %"T"% -> %"T"% ]. Γ |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *) (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof. Proof.
intros. intros.
@ -135,11 +141,11 @@ Qed.
Example typing2 : Example typing2 :
forall Γ, forall Γ,
(context_contains Γ "x" [ %"T"% ]) -> (context_contains Γ "x" [< %"T"% >]) ->
Γ |- [[ Λ"T" λ "x" %"T"% %"x"% ]] \is [ "U", %"U"% -> %"U"% ]. Γ |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >].
Proof. Proof.
intros. intros.
apply T_Sub with (τ:=["T",(%"T"% -> %"T"%)]). apply T_Descend with (τ:=[< "T",(%"T"% -> %"T"%) >]).
apply T_TypeAbs. apply T_TypeAbs.
apply T_Abs. apply T_Abs.
apply H. apply H.
@ -156,12 +162,16 @@ Qed.
Example typing3 : Example typing3 :
forall Γ, forall Γ,
(context_contains Γ "x" [ %"T"% ]) -> (context_contains Γ "x" [< %"T"% >]) ->
(context_contains Γ "y" [ %"U"% ]) -> (context_contains Γ "y" [< %"U"% >]) ->
Γ |- [[ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"% ]] \is [ "S","T",(%"S"%->%"T"%->%"T"%) ]. Γ |- [{
Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"%
}] \is [<
"S","T",(%"S"%->%"T"%->%"T"%)
>].
Proof. Proof.
intros. 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 T_TypeAbs, T_TypeAbs, T_Abs.
apply H. apply H.
apply T_Abs. apply T_Abs.
@ -169,7 +179,7 @@ Proof.
apply T_Var, H0. apply T_Var, H0.
apply TSubRepr_Refl. 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 TEq_Alpha.
apply TAlpha_Rename. apply TAlpha_Rename.
apply TSubst_UnivReplace. discriminate. apply TSubst_UnivReplace. discriminate.
@ -192,20 +202,21 @@ Qed.
Example typing4 : (is_well_typed Example typing4 : (is_well_typed
[[ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"x"% ]] [{ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"x"% }]
). ).
Proof. Proof.
unfold is_well_typed. unfold is_well_typed.
exists (ctx_assign "x" [%"T"%] exists (ctx_assign "x" [< %"T"% >]
(ctx_assign "y" [%"U"%] ctx_empty)). (ctx_assign "y" [< %"U"% >] ctx_empty)).
exists [ "T","U",%"T"%->%"U"%->%"T"% ]. exists [< "T","U",%"T"%->%"U"%->%"T"% >].
apply T_CompatTypeAbs. apply TCompat_Native.
apply T_CompatTypeAbs. apply T_TypeAbs.
apply T_CompatAbs. apply T_TypeAbs.
apply T_Abs.
apply C_take. apply C_take.
apply T_CompatAbs. apply T_Abs.
apply C_shuffle. apply C_take. apply C_shuffle. apply C_take.
apply T_CompatVar. apply T_Var.
apply C_take. apply C_take.
Qed. Qed.