coq: add subtype relations

This commit is contained in:
Michael Sippel 2024-08-21 15:02:43 +02:00
parent a65a33d9d6
commit 42ae93f2d7
Signed by: senvas
GPG key ID: 060F22F65102F95C
2 changed files with 97 additions and 0 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

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.