coq: add subtype relations

coq/_CoqProject

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

coq/equiv.v

@@ -30,18 +30,43 @@
  * satisfies all properties required of an equivalence relation.
  *)
 Require Import terms.
+Require Import subst.
 From Coq Require Import Strings.String.
 
 Include Terms.
+Include Subst.
 
 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}$ *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
 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'))
     -->distribute-ladder
     (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
     (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).
 
 
 
 Reserved Notation "S '-->condense-ladder' T" (at level 40).
 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'))
     -->condense-ladder
     (type_spec x (type_ladder y y'))
@@ -77,6 +117,16 @@ Inductive type_condense_ladder : type_term -> type_term -> Prop :=
     -->condense-ladder
     (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).
 
 
@@ -90,9 +140,12 @@ Lemma distribute_inverse :
 Proof.
   intros.
   destruct H.
-  apply L_CondenseOverApp.
+  apply L_CondenseOverSpec1.
+  apply L_CondenseOverSpec2.
   apply L_CondenseOverFun1.
   apply L_CondenseOverFun2.
+  apply L_CondenseOverMorph1.
+  apply L_CondenseOverMorph2.
 Qed.
 
 (** Inversion Lemma:
@@ -105,9 +158,12 @@ Lemma condense_inverse :
 Proof.
   intros.
   destruct H.
-  apply L_DistributeOverApp.
+  apply L_DistributeOverSpec1.
+  apply L_DistributeOverSpec2.
   apply L_DistributeOverFun1.
   apply L_DistributeOverFun2.
+  apply L_DistributeOverMorph1.
+  apply L_DistributeOverMorph2.
 Qed.
 
 
@@ -115,19 +171,23 @@ Qed.
 
 Reserved Notation " S '===' T " (at level 40).
 Inductive type_eq : type_term -> type_term -> Prop :=
-  | L_Refl : forall x,
+  | TEq_Refl : forall x,
     x === x
 
-  | L_Trans : forall x y z,
+  | TEq_Trans : forall x y z,
     x === y ->
     y === 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 === y
 
-  | L_Condense : forall x y,
+  | TEq_Condense : forall x y,
     x -->condense-ladder y ->
     x === y
 
@@ -143,24 +203,23 @@ Proof.
   intros.
   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_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.
 
 (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
@@ -237,25 +296,26 @@ Proof.
   destruct t.
 
   exists type_unit.
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   
   exists (type_id s).
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   admit.
   
   exists (type_num n).
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   
   admit.
   
   exists (type_univ s t).
-  split. apply L_Refl.
+  split.
+  apply TEq_Refl.
   apply LNF.
   
 Admitted.
@@ -302,8 +362,8 @@ Example example_type_eq :
     (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
                (type_spec (type_id "Seq") (type_id "Byte"))).
 Proof.
-  apply L_Distribute.
+  apply TEq_Distribute.
-  apply L_DistributeOverApp.
+  apply L_DistributeOverSpec2.
 Qed.
 
 

coq/subtype.v

@@ -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.

coq/terms.v

@@ -32,40 +32,62 @@ Inductive expr_term : Type :=
   | 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_expr_scope.
 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_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_expr_scope.
-
 
 End Terms.

coq/typing.v

@@ -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 :=
   | T_Var : forall Γ x τ,
     (context_contains Γ x τ) ->
-    (Γ |- x \is τ)
+    (Γ |- (expr_var x) \is τ)
 
   | T_Let : forall Γ s (σ:type_term) t τ x,
     (Γ |- s \is σ) ->