%% POPLmark 2a: Progress and preservation for Fsub %% %% 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. induction on 1. intros. case H1. search. search. apply IH to H2. apply IH to H3. search. Theorem sub_arrow : forall S T1 T2, {sub S (arrow T1 T2)} -> exists S1 S2, S = arrow S1 S2. induction on 1. intros. case H1. search. apply IH to H3. apply IH to H2. search. search. Theorem sub_forall : forall S T1 T2, {sub S (all T1 T2)} -> exists S1 S2, S = all S1 S2. induction on 1. intros. case H1. search. apply IH to H3. apply IH to H2. search. search. Theorem invert_sub_arrow : forall S1 S2 T1 T2, {sub (arrow S1 S2) (arrow T1 T2)} -> {sub T1 S1} /\ {sub S2 T2}. induction on 1. intros. case H1. search. apply sub_arrow to H3. apply IH to H2. apply IH to H3. search. search. 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)}. induction on 1. intros. case H1. search. apply sub_forall to H3. apply IH to H2. apply IH to H3. assert {sub n1 T1 |- sub n1 S3}. cut H5 with H8. search. search. %% Typing inversions Theorem absurd_ota : forall E T1 T2 T3, {of (tabs T1 E) (arrow T2 T3)} -> false. induction on 1. intros. case H1. apply sub_arrow to H3. apply IH to H2. Theorem absurd_oaf : forall E T1 T2 T3, {of (abs T1 E) (all T2 T3)} -> false. induction on 1. intros. case H1. apply sub_forall to H3. apply IH to H2. 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}. induction on 1. intros. case H1. search. apply sub_arrow to H3. apply invert_sub_arrow to H3. apply IH to H2. search. 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)}. induction on 1. intros. case H1. search. apply sub_forall to H3. apply invert_sub_forall to H3. apply IH to H2. assert {sub n1 T1 |- sub n1 S2}. cut H8 with H9. search. %% 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). induction on 1. intros. case H1. case H2. case H3. case H6. search. apply absurd_ota to H4. search. search. apply IH to H4 H2 H3. search. Theorem tapp_progresses : forall E T T', {of (tapp E T) T'} -> progresses E -> progresses (tapp E T). induction on 1. intros. case H1. case H2. case H5. apply absurd_oaf to H3. search. search. apply IH to H3 H2. search. Theorem progress : forall E T, {of E T} -> progresses E. induction on 1. intros. case H1 (keep). search. apply IH to H2. apply IH to H3. apply app_progresses to H1 H4 H5. search. search. apply IH to H2. apply tapp_progresses to H1 H4. search. apply IH to H2. search. %% Preservation Theorem preservation : forall E E' T, {of E T} -> {step E E'} -> {of E' T}. induction on 1. intros. case H1. case H2. case H2. apply invert_of_abs to H3. inst H6 with n1 = E2. assert {of E2 T1}. cut H9 with H10. search. apply IH to H3 H5. search. apply IH to H4 H6. search. case H2. case H2. apply invert_of_tabs to H3. assert {sub T2 T3}. inst H5 with n1 = T2. cut H9 with H8. inst H7 with n1 = T2. cut H11 with H4. search. apply IH to H3 H5. search. apply IH to H3 H2. search.