94 lines
2.4 KiB
Coq
94 lines
2.4 KiB
Coq
(*
|
|
* 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.
|
|
|
|
(** 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.
|