Compare commits

...

5 commits

5 changed files with 232 additions and 53 deletions

View file

@ -2,6 +2,7 @@
terms.v terms.v
equiv.v equiv.v
subst.v subst.v
subtype.v
typing.v typing.v
smallstep.v smallstep.v
bbencode.v bbencode.v

View file

@ -30,18 +30,43 @@
* satisfies all properties required of an equivalence relation. * satisfies all properties required of an equivalence relation.
*) *)
Require Import terms. Require Import terms.
Require Import subst.
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
Include Terms. Include Terms.
Include Subst.
Module Equiv. Module Equiv.
(** Alpha conversion in types *)
Reserved Notation "S '-->α' T" (at level 40).
Inductive type_conv_alpha : type_term -> type_term -> Prop :=
| TEq_Alpha : forall x y t,
(type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
where "S '-->α' T" := (type_conv_alpha S T).
(** Alpha conversion is symmetric *)
Lemma type_alpha_symm :
forall σ τ,
(σ -->α τ) -> (τ -->α σ).
Proof.
(* TODO *)
Admitted.
(** Define all rewrite steps $\label{coq:type-dist}$ *) (** Define all rewrite steps $\label{coq:type-dist}$ *)
Reserved Notation "S '-->distribute-ladder' T" (at level 40). Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : type_term -> type_term -> Prop := Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
| L_DistributeOverApp : forall x y y', | L_DistributeOverSpec1 : forall x x' y,
(type_spec (type_ladder x x') y)
-->distribute-ladder
(type_ladder (type_spec x y) (type_spec x' y))
| L_DistributeOverSpec2 : forall x y y',
(type_spec x (type_ladder y y')) (type_spec x (type_ladder y y'))
-->distribute-ladder -->distribute-ladder
(type_ladder (type_spec x y) (type_spec x y')) (type_ladder (type_spec x y) (type_spec x y'))
@ -56,13 +81,28 @@ Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
-->distribute-ladder -->distribute-ladder
(type_ladder (type_fun x y) (type_fun x y')) (type_ladder (type_fun x y) (type_fun x y'))
| L_DistributeOverMorph1 : forall x x' y,
(type_morph (type_ladder x x') y)
-->distribute-ladder
(type_ladder (type_morph x y) (type_morph x' y))
| L_DistributeOverMorph2 : forall x y y',
(type_morph x (type_ladder y y'))
-->distribute-ladder
(type_ladder (type_morph x y) (type_morph x y'))
where "S '-->distribute-ladder' T" := (type_distribute_ladder S T). where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
Reserved Notation "S '-->condense-ladder' T" (at level 40). Reserved Notation "S '-->condense-ladder' T" (at level 40).
Inductive type_condense_ladder : type_term -> type_term -> Prop := Inductive type_condense_ladder : type_term -> type_term -> Prop :=
| L_CondenseOverApp : forall x y y', | L_CondenseOverSpec1 : forall x x' y,
(type_ladder (type_spec x y) (type_spec x' y))
-->condense-ladder
(type_spec (type_ladder x x') y)
| L_CondenseOverSpec2 : forall x y y',
(type_ladder (type_spec x y) (type_spec x y')) (type_ladder (type_spec x y) (type_spec x y'))
-->condense-ladder -->condense-ladder
(type_spec x (type_ladder y y')) (type_spec x (type_ladder y y'))
@ -77,6 +117,16 @@ Inductive type_condense_ladder : type_term -> type_term -> Prop :=
-->condense-ladder -->condense-ladder
(type_fun x (type_ladder y y')) (type_fun x (type_ladder y y'))
| L_CondenseOverMorph1 : forall x x' y,
(type_ladder (type_morph x y) (type_morph x' y))
-->condense-ladder
(type_morph (type_ladder x x') y)
| L_CondenseOverMorph2 : forall x y y',
(type_ladder (type_morph x y) (type_morph x y'))
-->condense-ladder
(type_morph x (type_ladder y y'))
where "S '-->condense-ladder' T" := (type_condense_ladder S T). where "S '-->condense-ladder' T" := (type_condense_ladder S T).
@ -90,9 +140,12 @@ Lemma distribute_inverse :
Proof. Proof.
intros. intros.
destruct H. destruct H.
apply L_CondenseOverApp. apply L_CondenseOverSpec1.
apply L_CondenseOverSpec2.
apply L_CondenseOverFun1. apply L_CondenseOverFun1.
apply L_CondenseOverFun2. apply L_CondenseOverFun2.
apply L_CondenseOverMorph1.
apply L_CondenseOverMorph2.
Qed. Qed.
(** Inversion Lemma: (** Inversion Lemma:
@ -105,9 +158,12 @@ Lemma condense_inverse :
Proof. Proof.
intros. intros.
destruct H. destruct H.
apply L_DistributeOverApp. apply L_DistributeOverSpec1.
apply L_DistributeOverSpec2.
apply L_DistributeOverFun1. apply L_DistributeOverFun1.
apply L_DistributeOverFun2. apply L_DistributeOverFun2.
apply L_DistributeOverMorph1.
apply L_DistributeOverMorph2.
Qed. Qed.
@ -115,19 +171,23 @@ Qed.
Reserved Notation " S '===' T " (at level 40). Reserved Notation " S '===' T " (at level 40).
Inductive type_eq : type_term -> type_term -> Prop := Inductive type_eq : type_term -> type_term -> Prop :=
| L_Refl : forall x, | TEq_Refl : forall x,
x === x x === x
| L_Trans : forall x y z, | TEq_Trans : forall x y z,
x === y -> x === y ->
y === z -> y === z ->
x === z x === z
| L_Distribute : forall x y, | TEq_Rename : forall x y,
x -->α y ->
x === y
| TEq_Distribute : forall x y,
x -->distribute-ladder y -> x -->distribute-ladder y ->
x === y x === y
| L_Condense : forall x y, | TEq_Condense : forall x y,
x -->condense-ladder y -> x -->condense-ladder y ->
x === y x === y
@ -143,24 +203,23 @@ Proof.
intros. intros.
induction H. induction H.
1:{ apply TEq_Refl.
apply L_Refl.
}
2:{ apply TEq_Trans with (y:=y).
apply L_Condense.
apply distribute_inverse.
apply H.
}
2:{
apply L_Distribute.
apply condense_inverse.
apply H.
}
apply L_Trans with (y:=y).
apply IHtype_eq2. apply IHtype_eq2.
apply IHtype_eq1. apply IHtype_eq1.
apply type_alpha_symm in H.
apply TEq_Rename.
apply H.
apply TEq_Condense.
apply distribute_inverse.
apply H.
apply TEq_Distribute.
apply condense_inverse.
apply H.
Qed. Qed.
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *) (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
@ -237,25 +296,26 @@ Proof.
destruct t. destruct t.
exists type_unit. exists type_unit.
split. apply L_Refl. split. apply TEq_Refl.
apply LNF. apply LNF.
admit. admit.
exists (type_id s). exists (type_id s).
split. apply L_Refl. split. apply TEq_Refl.
apply LNF. apply LNF.
admit. admit.
admit. admit.
exists (type_num n). exists (type_num n).
split. apply L_Refl. split. apply TEq_Refl.
apply LNF. apply LNF.
admit. admit.
admit. admit.
exists (type_univ s t). exists (type_univ s t).
split. apply L_Refl. split.
apply TEq_Refl.
apply LNF. apply LNF.
Admitted. Admitted.
@ -302,8 +362,8 @@ Example example_type_eq :
(type_ladder (type_spec (type_id "Seq") (type_id "Char")) (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
(type_spec (type_id "Seq") (type_id "Byte"))). (type_spec (type_id "Seq") (type_id "Byte"))).
Proof. Proof.
apply L_Distribute. apply TEq_Distribute.
apply L_DistributeOverApp. apply L_DistributeOverSpec2.
Qed. Qed.

96
coq/subtype.v Normal file
View file

@ -0,0 +1,96 @@
(*
* This module defines the subtype relationship
*
* We distinguish between *representational* subtypes,
* where any high-level type is a subtype of its underlying
* representation type and *convertible* subtypes that
* are compatible at high level, but have a different representation
* that requires a conversion.
*)
From Coq Require Import Strings.String.
Require Import terms.
Require Import equiv.
Include Terms.
Include Equiv.
Module Subtype.
(** Subtyping *)
Reserved Notation "s ':<=' t" (at level 50).
Reserved Notation "s '~<=' t" (at level 50).
(* Representational Subtype *)
Inductive is_repr_subtype : type_term -> type_term -> Prop :=
| TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')
| TSubRepr_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
| TSubRepr_Ladder : forall x' x y, (x :<= y) -> ((type_ladder x' x) :<= y)
where "s ':<=' t" := (is_repr_subtype s t).
(* Convertible Subtype *)
Inductive is_conv_subtype : type_term -> type_term -> Prop :=
| TSubConv_Refl : forall t t', (t === t') -> (t ~<= t')
| TSubConv_Trans : forall x y z, (x ~<= y) -> (y ~<= z) -> (x ~<= z)
| TSubConv_Ladder : forall x' x y, (x ~<= y) -> ((type_ladder x' x) ~<= y)
| TSubConv_Morph : forall x y y', (type_ladder x y) ~<= (type_ladder x y')
where "s '~<=' t" := (is_conv_subtype s t).
(* Every Representational Subtype is a Convertible Subtype *)
Lemma syn_sub_is_sem_sub : forall x y, (x :<= y) -> (x ~<= y).
Proof.
intros.
induction H.
apply TSubConv_Refl.
apply H.
apply TSubConv_Trans with (x:=x) (y:=y) (z:=z).
apply IHis_repr_subtype1.
apply IHis_repr_subtype2.
apply TSubConv_Ladder.
apply IHis_repr_subtype.
Qed.
(* EXAMPLES *)
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Example sub0 :
[ < $"Seq"$ < $"Digit"$ $"10"$ > >
~ < $"Seq"$ $"Char"$ > ]
:<=
[ < $"Seq"$ $"Char"$ > ]
.
Proof.
apply TSubRepr_Ladder.
apply TSubRepr_Refl.
apply TEq_Refl.
Qed.
Example sub1 :
[ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ]
:<= [ < $"Seq"$ $"Char"$ > ]
.
Proof.
set [ < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > ].
set [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ].
set [ < $"Seq"$ $"Char"$ > ].
set (t0 === t).
set (t :<= t0).
set (t :<= t1).
apply TSubRepr_Trans with t.
apply TSubRepr_Refl.
apply TEq_Distribute.
apply L_DistributeOverSpec2.
apply TSubRepr_Ladder.
apply TSubRepr_Refl.
apply TEq_Refl.
Qed.
End Subtype.

View file

@ -32,40 +32,62 @@ Inductive expr_term : Type :=
| expr_descend : type_term -> expr_term -> expr_term | expr_descend : type_term -> expr_term -> expr_term
. .
Coercion type_var : string >-> type_term. (* values *)
Coercion expr_var : string >-> expr_term. Inductive is_value : expr_term -> Prop :=
| V_ValAbs : forall x τ e,
(is_value (expr_tm_abs x τ e))
(* | V_TypAbs : forall τ e,
Coercion type_var : string >-> type_term. (is_value (expr_ty_abs τ e))
Coercion expr_var : string >-> expr_term.
*) | V_Ascend : forall τ e,
(is_value e) ->
(is_value (expr_ascend τ e))
.
Declare Scope ladder_type_scope. Declare Scope ladder_type_scope.
Declare Scope ladder_expr_scope. Declare Scope ladder_expr_scope.
Declare Custom Entry ladder_type. Declare Custom Entry ladder_type.
Declare Custom Entry ladder_expr.
Notation "[ e ]" := e (e custom ladder_type at level 80) : ladder_type_scope. 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).
Notation "'<' σ τ '>'" := (type_spec σ τ)
(in custom ladder_type at level 80, left associativity) : ladder_type_scope.
Notation "'(' τ ')'" := τ
(in custom ladder_type at level 70) : ladder_type_scope.
Notation "σ '->' τ" := (type_fun σ τ)
(in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '->morph' τ" := (type_morph σ τ)
(in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
Notation "σ '~' τ" := (type_ladder σ τ)
(in custom ladder_type at level 70, right associativity) : ladder_type_scope.
Notation "'$' x '$'" := (type_id x%string)
(in custom ladder_type at level 0, x constr) : ladder_type_scope.
Notation "'%' x '%'" := (type_var x%string)
(in custom ladder_type at level 0, x constr) : ladder_type_scope.
(* TODO: allow any variable names in notation, not just α,β,γ *) Notation "[[ e ]]" := e
Notation "'∀α.' τ" := (type_univ "α" τ) (in custom ladder_type at level 80) : ladder_type_scope. (e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "'∀β.' τ" := (type_univ "β" τ) (in custom ladder_type at level 80) : ladder_type_scope. Notation "'%' x '%'" := (expr_var x%string)
Notation "'∀γ.' τ" := (type_univ "γ" τ) (in custom ladder_type at level 80) : ladder_type_scope. (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
Notation "'<' σ τ '>'" := (type_spec σ τ) (in custom ladder_type at level 80, left associativity) : ladder_type_scope. Notation "'λ' x τ '↦' e" := (expr_tm_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
Notation "'(' τ ')'" := τ (in custom ladder_type at level 70) : ladder_type_scope. Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
Notation "σ '->' τ" := (type_fun σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope. (in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
Notation "σ '->morph' τ" := (type_morph σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '~' τ" := (type_ladder σ τ) (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
Notation "'α'" := (type_var "α") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Notation "'β'" := (type_var "β") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Notation "'γ'" := (type_var "γ") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Open Scope ladder_type_scope. Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Definition t1 : type_term := [ α.β.(α~β~γ)->β->(α->α)->β ]. Check [ "α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) ].
Definition polymorphic_identity1 : expr_term := [[ Λ"T" λ"x"%"T"% %"x"% ]].
Definition polymorphic_identity2 : expr_term := [[ Λ"T" λ"y"%"T"% %"y"% ]].
Compute polymorphic_identity1.
Compute t1.
Close Scope ladder_type_scope. Close Scope ladder_type_scope.
Close Scope ladder_expr_scope.
End Terms. End Terms.

View file

@ -27,7 +27,7 @@ Reserved Notation "Gamma '|-' x '\compatible' X" (at level 101, x at next level
Inductive expr_type : context -> expr_term -> type_term -> Prop := Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Var : forall Γ x τ, | T_Var : forall Γ x τ,
(context_contains Γ x τ) -> (context_contains Γ x τ) ->
(Γ |- x \is τ) (Γ |- (expr_var x) \is τ)
| T_Let : forall Γ s (σ:type_term) t τ x, | T_Let : forall Γ s (σ:type_term) t τ x,
(Γ |- s \is σ) -> (Γ |- s \is σ) ->