POPLmark 2a: Progress and preservation for Fsub

Executable Specification

[View poplmark-2a.sig] [View poplmark-2a.mod]
sig poplmark-2a.

kind     tm, ty     type.

type     top        ty.
type     arrow      ty -> ty -> ty.
type     all        ty -> (ty -> ty) -> ty.

type     abs        ty -> (tm -> tm) -> tm.
type     app        tm -> tm -> tm.
type     tabs       ty -> (ty -> tm) -> tm.
type     tapp       tm -> ty -> tm.

type     sub        ty -> ty -> o.
type     of         tm -> ty -> o.
type     value      tm -> o.
type     step       tm -> tm -> o.

module poplmark-2a.

% Subtyping (Declarative version)

sub S top.

sub T T.

sub S T :- sub S Q, sub Q T.

sub (arrow S1 S2) (arrow T1 T2) :- sub T1 S1, sub S2 T2.

sub (all S1 (x\ S2 x)) (all T1 (x\ T2 x)) :-
    sub T1 S1,
    pi x\ (sub x T1 => sub (S2 x) (T2 x)).


% Typing

of (abs T1 E) (arrow T1 T2) :-
    pi x\ of x T1 => of (E x) T2.

of (app E1 E2) T12 :-
    of E1 (arrow T11 T12), of E2 T11.

of (tabs T1 E) (all T1 T2) :-
    pi x\ sub x T1 => of (E x) (T2 x).

of (tapp E T2) (T12 T2) :-
    of E (all T11 T12), sub T2 T11.

of E T :- of E S, sub S T.


% Small step evaluation

value (abs T E).
value (tabs T E).

step (app (abs T E1) V2) (E1 V2) :- value V2.

step (tapp (tabs T1 E) T2) (E T2).

step (app E1 E2) (app E1' E2) :- step E1 E1'.

step (app V1 E2) (app V1 E2') :- value V1, step E2 E2'.

step (tapp E T) (tapp E' T) :- step E E'.

Reasoning

[View poplmark-2a.thm]

Click on a command or tactic to see a detailed view of its use.

%%
%% Most of this is derived from the Twelf solution by CMU

Specification "poplmark-2a".

%% Subtyping inversions

Theorem sub_top : forall T,
  {sub top T} -> T = top.

Theorem sub_arrow : forall S T1 T2,
  {sub S (arrow T1 T2)} -> exists S1 S2, S = arrow S1 S2.

Theorem sub_forall : forall S T1 T2,
  {sub S (all T1 T2)} -> exists S1 S2, S = all S1 S2.

Theorem invert_sub_arrow : forall S1 S2 T1 T2,
  {sub (arrow S1 S2) (arrow T1 T2)} -> {sub T1 S1} /\ {sub S2 T2}.

Theorem invert_sub_forall : forall S1 S2 T1 T2,
  {sub (all S1 S2) (all T1 T2)} ->
    {sub T1 S1} /\ nabla x, {sub x T1 |- sub (S2 x) (T2 x)}.

%% Typing inversions

Theorem absurd_ota : forall E T1 T2 T3,
  {of (tabs T1 E) (arrow T2 T3)} -> false.

Theorem absurd_oaf : forall E T1 T2 T3,
  {of (abs T1 E) (all T2 T3)} -> false.

Theorem invert_of_abs : forall S1 E T1 T2,
  {of (abs S1 E) (arrow T1 T2)} ->
    exists S2, nabla x,
      {of x S1 |- of (E x) S2} /\ {sub T1 S1} /\ {sub S2 T2}.

Theorem invert_of_tabs : forall S1 E T1 T2,
  {of (tabs S1 E) (all T1 T2)} ->
    exists S2, nabla x, {sub x S1 |- of (E x) (S2 x)} /\ {sub T1 S1} /\
                        {sub x T1 |- sub (S2 x) (T2 x)}.


%% Progress

Define progresses : tm -> prop by
  progresses E := {value E} ;
  progresses E := exists E', {step E E'}.

Theorem app_progresses : forall E1 E2 T,
  {of (app E1 E2) T} -> progresses E1 -> progresses E2 ->
    progresses (app E1 E2).

Theorem tapp_progresses : forall E T T',
  {of (tapp E T) T'} -> progresses E -> progresses (tapp E T).

Theorem progress : forall E T,
  {of E T} -> progresses E.


%% Preservation

Theorem preservation : forall E E' T,
  {of E T} -> {step E E'} -> {of E' T}.