User:Rsimmons/Subtype
From The Twelf Project
| This is Literate Twelf Code: here Status: %% OK %% Output: here. |
Progress and preservation for a language with n-ary tuples that have both a notion of width and depth subtyping.
Contents |
Syntax
Natural numbers
nat : type. z : nat. s : nat -> nat.
Types
ty : type. tys : type. tys/nil : tys. tys/cons : ty -> tys -> tys. ty/tup : tys -> ty. ty/nat : ty. ty/int : ty.
Type equality
tyeq : ty -> ty -> type. tyeq/refl : tyeq T T. tyseq : tys -> tys -> type. tyseq/refl : tyseq Ts Ts. tyseq-cong : tyeq T S -> tyseq Ts Ss -> tyseq (tys/cons T Ts) (tys/cons S Ss) -> type. - : tyseq-cong tyeq/refl tyseq/refl tyseq/refl. %mode tyseq-cong +A +B -C. %worlds () (tyseq-cong _ _ _). %total {} (tyseq-cong _ _ _).
Terms
tm : type. tms : type. tms/nil : tms. tms/cons : tm -> tms -> tms. tm/tup : tms -> tm. tm/num : nat -> nat -> tm. tm/nadd : tm -> tm -> tm. tm/add : tm -> tm -> tm. tm/proj : tm -> nat -> tm.
Abbreviations
%abbrev @ = tys/nil. %abbrev , = tys/cons. %infix right 10 ,. %abbrev # = tms/nil. %abbrev ; = tms/cons. %infix right 10 ;.
Primitive operations
plus : nat -> nat -> nat -> type. plus/z : plus z N N. plus/s : plus N M P -> plus (s N) M (s P). projtm : tms -> nat -> tm -> type. projtm/z : projtm (E ; ES) z E. projtm/s : projtm ES N E -> projtm (E ; ES) (s N) E. projty : tys -> nat -> ty -> type. projty/z : projty (T , TS) z T. projty/s : projty TS N T -> projty (T , TS) (s N) T.
Dynamic semantics
Values
v : tm -> type. vs : tms -> type. vs/nil : vs tms/nil. vs/cons : v E -> vs ES -> vs (tms/cons E ES). v/num : v (tm/num N+ N-). v/tup : v (tm/tup ES).
Dynamics
step : tm -> tm -> type. steps : tms -> tms -> type. steps/s : step E E' -> steps (E ; ES) (E' ; ES). steps/v : v E -> steps ES ES' -> steps (E ; ES) (E ; ES'). step/nadd1 : step E1 E1' -> step (tm/nadd E1 E2) (tm/nadd E1' E2). step/nadd2 : v E1 -> step E2 E2' -> step (tm/nadd E1 E2) (tm/nadd E1 E2'). step/naddR : plus N1 N2 N3 -> step (tm/nadd (tm/num N1 z) (tm/num N2 z)) (tm/num N3 z). step/add1 : step E1 E1' -> step (tm/add E1 E2) (tm/add E1' E2). step/add2 : v E1 -> step E2 E2' -> step (tm/add E1 E2) (tm/add E1 E2'). step/addR : plus N1+ N2- N3+ -> plus N1- N2+ N3- -> step (tm/add (tm/num N1+ N1-) (tm/num N2+ N2-)) (tm/num N3+ N3-). step/tup : steps ES ES' -> step (tm/tup ES) (tm/tup ES'). step/proj1 : step E E' -> step (tm/proj E I) (tm/proj E' I'). step/projR : projtm ES I E -> vs ES -> step (tm/proj (tm/tup ES) I) E.
Static semantics
Subtyping
<| : ty -> ty -> type. %infix none 10 <|. <<| : tys -> tys -> type. %infix none 10 <<|. subs/nil : TS <<| @. subs/cons: S <| T -> SS <<| TS -> (S , SS) <<| (T , TS). sub/nat : ty/nat <| ty/nat. sub/int : ty/int <| ty/int. sub/num : ty/nat <| ty/int. sub/tup : TS <<| SS -> (ty/tup TS) <| (ty/tup SS).
Typing
of : tm -> ty -> type. ofs : tms -> tys -> type. %block gamma : some {T: ty} block {x: tm}{d: of x T}. ofs/nil : ofs # @. ofs/cons: of E T -> ofs ES TS -> ofs (E ; ES) (T , TS). of/tup : ofs ES TS -> of (tm/tup ES) (ty/tup TS). of/nat : of (tm/num N z) ty/nat. of/int : of (tm/num N+ N-) ty/int. of/nadd : of E1 ty/nat -> of E2 ty/nat -> of (tm/nadd E1 E2) ty/nat. of/add : of E1 ty/int -> of E2 ty/int -> of (tm/add E1 E2) ty/int. of/proj : projty TS N T -> of E (ty/tup TS) -> of (tm/proj E N) T. of/sub : S <| T -> of E S -> of E T.
Properties of subtyping
Reflexivity
sub-refl : {T} T <| T -> type. subs-refl : {Ts} Ts <<| Ts -> type. %mode sub-refl +T -TSub. %mode subs-refl +Ts -TsSub. - : sub-refl ty/nat sub/nat. - : sub-refl ty/int sub/int. - : sub-refl (ty/tup Ts) (sub/tup TTs) <- subs-refl Ts TTs. - : subs-refl tys/nil subs/nil. - : subs-refl (tys/cons T TS) (subs/cons D DS) <- sub-refl T D <- subs-refl TS DS. %worlds () (sub-refl _ _) (subs-refl _ _). %total (A B) (sub-refl A _) (subs-refl B _).
Transitivity
sub-trans : R <| S -> S <| T -> R <| T -> type. subs-trans : Rs <<| Ss -> Ss <<| Ts -> Rs <<| Ts -> type. %mode sub-trans +RS +ST -RT. %mode subs-trans +RSs +STs -RTs. - : sub-trans sub/nat S S. - : sub-trans S sub/int S. - : sub-trans (sub/tup RSs) (sub/tup STs) (sub/tup RTs) <- subs-trans RSs STs RTs. - : subs-trans _ subs/nil subs/nil. - : subs-trans (subs/cons RS RSs) (subs/cons ST STs) (subs/cons RT RTs) <- sub-trans RS ST RT <- subs-trans RSs STs RTs. %worlds () (subs-trans _ _ _) (sub-trans _ _ _). %total (A B) (subs-trans _ A _) (sub-trans _ B _).
Preservation
Inversion
The subtyping inversion theorem says that if (s1,...,sn) <: t, then t = (t1,...,tm) where m <= n.
inv-sub : ty/tup SS <| T -> tyeq T (ty/tup TS) -> SS <<| TS -> type. - : inv-sub (sub/tup A) tyeq/refl A. %mode inv-sub +A -B -C. %worlds () (inv-sub _ _ _). %total {} (inv-sub _ _ _).
The typing inversion lemma says that if G |- (e1,...,en) : t, then for each ei in [1,n], G |- ei : si, t = (t1,...,tm), m %lt;= n, and for each ti in [1,m], si %lt;: ti.
We need a simple lemma to handle a little equality and call transitivity.
inv-tup-lem : RS <<| SS -> tyeq S (ty/tup SS) -> S <| T -> tyeq T (ty/tup TS) -> RS <<| TS -> type. - : inv-tup-lem RS tyeq/refl (sub/tup ST) tyeq/refl RT <- subs-trans RS ST RT. %mode inv-tup-lem +A +B +C -D -E. %worlds () (inv-tup-lem _ _ _ _ _). %total {} (inv-tup-lem _ _ _ _ _). inv-tup : of (tm/tup ES) T -> ofs ES RS -> tyeq T (ty/tup TS) -> RS <<| TS -> type. - : inv-tup (of/tup (D: ofs ES SS)) D tyeq/refl DS <- subs-refl SS DS. - : inv-tup (of/sub (SUB : S <| T) (D: of (tm/tup ES) S)) Typs EqT Subs' <- inv-tup D (Typs: ofs ES RS) (EqS: tyeq S (ty/tup SS)) (Subs: RS <<| SS) <- inv-tup-lem Subs EqS SUB EqT Subs'. %mode inv-tup +A -B -C -D. %worlds (gamma) (inv-tup _ _ _ _). %total T (inv-tup T _ _ _).
