sub S top.
sub X X :- bound X U.
sub X T :- bound X U, sub U 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\ (bound x T1 => sub (S2 x) (T2 x)).
Click on a command or tactic to see a detailed view of its use.
%% POPLmark 1a: Reflexivity and transitivity for Fsub % We use nominal constants to represent type variable names. This predicate % recognizes such nominal constants. Define nabla x, name x. % ctx defines the context in which subtyping judgements are made Define ctx nil. Define ctx (bound X U :: L) := name X /\ ctx L. % cty defines valid closed types (used for reflexivity) Define cty L top. Define cty L X := exists U, member (bound X U) L. Define cty L (arrow T1 T2) := cty L T1 /\ cty L T2. Define cty L (all T1 T2) := cty L T1 /\ nabla x, cty (bound x T1 :: L) (T2 x). % ty defines valid open types (used for transitivity) Define ty top. Define nabla x, ty x. Define ty (arrow T1 T2) := ty T1 /\ ty T2. Define ty (all T1 T2) := ty T1 /\ nabla x, ty (T2 x). Theorem sub_refl : forall L T, cty L T -> {L |- sub T T}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. search. apply IH to H2. apply IH to H3. search. apply IH to H2. apply IH to H3. search. Theorem ctx_sub_absurd : forall S T L, ctx L -> member (sub S T) L -> false. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. apply IH to H4 H5. Theorem ctx_name : forall L X U, ctx L -> member (bound X U) L -> name X. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. case H3. search. apply IH to H4 H5. search. Theorem bound_name : forall L X U, ctx L -> {L |- bound X U} -> name X. [Show Proof][Hide Proof] intros. case H2. apply ctx_name to H1 H3. search. Theorem sub_top : forall L T, ctx L -> {L |- sub top T} -> T = top. [Show Proof][Hide Proof] intros. case H2. apply ctx_sub_absurd to H1 H3. search. search. apply bound_name to H1 H3. case H5. Theorem dual_theorem : forall Q, ty Q -> (forall L S T, ctx L -> {L |- sub S Q} -> {L |- sub Q T} -> {L |- sub S T}) /\ (forall L P X TM TN, ctx (bound X Q :: L) -> {L |- sub P Q} -> {L, bound X Q |- sub TM TN} -> {L, bound X P |- sub TM TN}). [Show Proof][Hide Proof] % The proof is by induction on the type Q. % For transitivity there is a nested induction on {L |- sub S Q} % For narrowing there is a nested induction on {L, bound X Q |- sub TM TN} induction on 1. intros. split*. % split* lets us use the transitivity result for Q while proving narrowing % Proof of transitivity % Induction and case analysis on {L |- S <: Q} induction on 2. intros. case H3. apply ctx_sub_absurd to H2 H5. % SA-Top, Q = top apply sub_top to H2 H4. search. % SA-Refl-TVar, S = Q search. % SA-Trans-TVar apply IH1 to H2 H6 H4. search. % SA-Arrow, S = arrow S1 S2, Q = arrow T1 T2 % Case analysis on (arrow T1 T2) <: T case H4. apply ctx_sub_absurd to H2 H7. % SA-Top, T = top search. % SA-Refl-TVar, absurd since (arrow T1 T2) is not a type variable apply bound_name to H2 H7. case H8. % SA-Trans-TVar, absurd since (arrow T1 T2) is not a type variable apply bound_name to H2 H7. case H9. % SA-Arrow, T = arrow T3 T4 % Inductively use transitivity based on T1 and T2 case H1. apply IH to H9. apply IH to H10. apply H11 to H2 H7 H5. apply H13 to H2 H6 H8. search. % SA-All, S = all S1 (x\ S2 x), Q = all T1 (x\ T2 x) case H4. apply ctx_sub_absurd to H2 H7. % SA-Top, T = top search. % SA-Refl-TVar, absurd since (arrow T1 T2) is not a type variable apply bound_name to H2 H7. case H8. % SA-Trans-TVar, absurd since (arrow T1 T2) is not a type variable apply bound_name to H2 H7. case H9. % SA-All, T = all T3 (x\ T4 x) % Inductively use transitivity and narrowing based on T1 % Inductively use transitivity based on T2 case H1. apply IH to H9. apply IH to H10. apply H11 to H2 H7 H5. apply H12 to _ H7 H6 with X = n1. apply H13 to _ H16 H8. search. % Proof of narrowing % Induction and case analysis on {L, X:Q |- TM <: TN} induction on 3. intros. case H5 (keep). apply ctx_sub_absurd to H3 H6. % SA-Top, TN = top search. % SA-Refl-TVar, TM = TN, either TM = X or TM is bound in L case H6. case H7. search. search. % SA-Trans-TVar case H6. case H8. % TM = X % Use transitivity result established for Q apply IH1 to H3 H4 H7. case H3. apply H2 to _ H4 H9. search. % TM is bound in L % Use inner inductive hypothesis apply IH1 to H3 H4 H7. search. % SA-Arrow, TM = arrow S1 S2, TN = arrow T1 T2 % Use inner inductive hypothesis apply IH1 to H3 H4 H6. apply IH1 to H3 H4 H7. search. % SA-All, TM = all S1 (x\ S2 x), TN = all T1 (x\ T2 x) % Use inner inductive hypothesis apply IH1 to H3 H4 H6. assert ctx (bound X Q :: bound n1 T1 :: L). case H3. search. apply IH1 to H9 H4 H7. search. % We can extract the transitivity result from the generalized theorem Theorem transitivity : forall L Q S T, ctx L -> ty Q -> {L |- sub S Q} -> {L |- sub Q T} -> {L |- sub S T}. [Show Proof][Hide Proof] intros. apply dual_theorem to H2. apply H5 to H1 H3 H4. search.