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.

Reasoning

[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.

% Proof:
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
% 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.

% Proof:
induction on 1. intros. case H1.
  case H2.
  case H2.
    search.
    apply member_prune to H4. apply IH to H3 H4. search.
% 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.

% Proof:
induction on 1. intros. case H1.
  case H2.
  case H2.
    case H3.
      search.
      apply member_prune to H5.
    case H3.
      apply member_prune to H5.
      apply IH to H4 H5 H6. search.
% 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}.

% Proof:
induction on 2. intros. case H2.
  % Subgoal 1
  case H3.
    inst H5 with n1 = N. cut H6 with H4. search. % 1.1
    case H6. apply of_name to _ H9. case H8.     % 1.2
    apply of_name to _ H7. case H6.              % 1.3
  % Subgoal 2
  case H3.
    case H6.                        % 2.1
      inst H5 with n1 = U2. apply IH to _ H8 H7 H4. search. % 2.1.1
      apply of_name to _ H9. case H8.                       % 2.1.2
    apply of_name to _ H7. case H6. % 2.2
  % Subgoal 3
  assert {L |- ins* (all T1) (arr U T)}. apply IH to _ H5 H6 H4. search.
  % Subgoal 4
  apply of_name to _ H6. case H5. case H7.
% 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}.

% Proof:
induction on 2. intros. case H2.
  % Subgoal 1
  inst H4 with n1 = N. cut H5 with H3. search.
  % Subgoal 2 (abs_ins*_arr lemma used)
  case H4.
    % Subgoal 2.1
    assert {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))}.
    apply abs_ins_arr to _ H5 H6 H3. search.
    % Subgoal 2.2
    assert {L |- ins* (all (z1\z1)) (arr U T)}.
    apply abs_ins_arr to _ H5 H6 H3. search.
  % Subgoal 3
  apply of_name to _ H5. case H6. case H4.
% 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}.

% Proof:
induction on 2. intros. case H2.
  case H3.
  % Subgoal 1
    apply IH to _ H4 H6. search.      % 1.1
    apply IH to _ H5 H6. search.      % 1.2
    apply abs_arr to _ H4 H5. search. % 1.3 (abs_arr lemma used)
  % Subgoal 2
  case H3. apply IH to _ H4 H5. search.
  % Subgoal 3
  apply IH to _ H4 H3. search.
  % Subgoal 4
  apply IH to _ H4 H3. search.
  % Subgoal 5
  apply of_name to _ H5. case H4. case H3. case H6. case H6. case H6. case H6.
% Q.E.D.