% 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) E2) (E1 E2). 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'.
Click on a command or tactic to see a detailed view of its use.
%% POPLmark 2a: Progress and preservation for Fsub %% %% Most of this is derived from the Twelf solution by CMU %% Subtyping inversions Theorem sub_top : forall T, {sub top T} -> T = top. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] 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)}. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] 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)}. [Show Proof][Hide Proof] 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 E := {value E}. Define 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). [Show Proof][Hide Proof] 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). [Show Proof][Hide Proof] 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. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. apply invert_of_abs to H3. inst H5 with n1 = E2. assert {of E2 T1}. cut H8 with H9. 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 T1}. 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.