Type-preservation of Curry-style System F

Executable Specification

[View fcurry.sig] [View fcurry.mod]
sig fcurry. %%% fcurry.sig

kind tm, ty     type.

type arr        ty -> ty -> ty.
type all        (ty -> ty) -> ty.

type app        tm -> tm -> tm.
type abs        (tm -> tm) -> tm.

type ins        ty -> ty -> o.
type ins*       ty -> ty -> o.

type of         tm -> ty -> o.

type step       tm -> tm -> o.
type steps      tm -> tm -> o.

module fcurry. %%% fcurry.mod

of (app M N) T :- of M (arr U T), of N U.
of (abs R) (arr T U) :- pi x\ (of x T => of (R x) U).
of N (all T) :- pi a\ of N (T a).
of N (T U) :- of N (all T).

ins (all T) (T U).

ins* T T.
ins* T S :- ins T U, ins* U S.

step (app M N) (app M' N) :- step M M'.
step (app M N) (app M N') :- step N N'.
step (abs R) (abs R') :- pi x\ step (R x) (R' x).
step (app (abs R) N) (R N).

steps M M.
steps M N :- step M M', steps M' N.


[View fcurry.thm]

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

%% Contributed by Ahn Ki Yung 

Specification "fcurry".

Close ty, tm.

Theorem member_prune : forall L E, nabla (x : tm),
  member (E x) L -> exists F, E = x\ F.
% Q.E.D.


Define ctx : olist -> prop by
  ctx nil ;
  nabla x, ctx (of x T :: L) := ctx L.

Define name : tm -> prop by
  nabla x, name x.

Theorem of_name :
  forall L E,
  ctx L -> member E L ->
  exists X T, E = of X T /\ name X.
% Q.E.D.

Theorem ctx_uniq : forall L E T1 T2,
  ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.
% Q.E.D.


Theorem abs_ins_arr : forall L R N U T S,
  ctx L -> {L |- of (abs R) S} -> {L |- ins* S (arr U T)} ->
  {L |- of N U} -> {L |- of (R N) T}.
% Q.E.D.

Theorem abs_arr : forall L R N U T,
  ctx L -> {L |- of (abs R) (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}.
% Q.E.D.

Theorem step_preserves_of : forall L M N T,
  ctx L -> {L |- of M T} -> {step M N} -> {L |- of N T}.
% Q.E.D.