%% Type-preservation of Curry-style System F
%%
%% Contributed by Ahn Ki Yung <kyagrd@gmail.com>
Specification "fcurry".
Close ty, tm.
Theorem member_prune : forall (L:olist) 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.
