% % Transitivity of subtyping % % sub-trans' is the "real" transitivity result, plus a "pacifier" argument (see base.elf) % to handle the contravariant-arrow induction hypothesis. sub-trans' : % If {P : pacifier} {SubAB : sub A B CoeAB CoeTypingAB} {SubBC : sub B C CoeBC CoeTypingBC} % then sub A C CoeAC CoeTypingAC -> type. %mode sub-trans' +P +SubAB +SubBC -SubAC. %name sub-trans' _Trans'. %{ - : sub-trans' _ sub/refl Sub2 Sub2. - : sub-trans' _ Sub1 sub/refl Sub1. }% - : sub-trans' _ A (sub/top-right) (sub/top-right). - : sub-trans' P (sub/arr Dom1 Cod1) (sub/arr Dom2 Cod2) (sub/arr Dom Cod) <- pacify P Psmall % uses %trustme <- sub-trans' Psmall Dom2 Dom1 Dom % CLAIM: Dom2 and Dom1 are, together, as large as Dom1 and Dom2. <- sub-trans' P Cod1 Cod2 Cod. - : sub-trans' P (sub/sect-left-1 Sub1) Sub2 (sub/sect-left-1 Sub) <- sub-trans' P Sub1 Sub2 Sub. - : sub-trans' P (sub/sect-left-2 Sub1) Sub2 (sub/sect-left-2 Sub) <- sub-trans' P Sub1 Sub2 Sub. - : sub-trans' P Sub1 (sub/sect-right Sub21 Sub22) (sub/sect-right Sub21' Sub22') <- sub-trans' P Sub1 Sub21 Sub21' <- sub-trans' P Sub1 Sub22 Sub22'. - : sub-trans' P (sub/sect-right Sub11 Sub12) (sub/sect-left-1 Sub2) Sub <- sub-trans' P Sub11 Sub2 Sub. - : sub-trans' P (sub/sect-right Sub11 Sub12) (sub/sect-left-2 Sub2) Sub <- sub-trans' P Sub12 Sub2 Sub. - : sub-trans' P Sub1 (sub/union-right-1 Sub2) (sub/union-right-1 Sub) <- sub-trans' P Sub1 Sub2 Sub. - : sub-trans' P Sub1 (sub/union-right-2 Sub2) (sub/union-right-2 Sub) <- sub-trans' P Sub1 Sub2 Sub. - : sub-trans' P (sub/union-left Sub11 Sub12) Sub2 (sub/union-left Sub11' Sub12') <- sub-trans' P Sub11 Sub2 Sub11' <- sub-trans' P Sub12 Sub2 Sub12'. - : sub-trans' P (sub/union-right-1 Sub1) (sub/union-left Sub21 Sub22) Sub <- sub-trans' P Sub1 Sub21 Sub. - : sub-trans' P (sub/union-right-2 Sub1) (sub/union-left Sub21 Sub22) Sub <- sub-trans' P Sub1 Sub22 Sub. %worlds () (sub-trans' _ _ _ _). %total {P [Sub1 Sub2]} (sub-trans' P Sub1 Sub2 _). % Lexicographic ordering: % P dominates, then % [Sub1 Sub2] simultaneously sub-trans : % If {SubAB : sub A B CoeAB CoeTypingAB} {SubBC : sub B C CoeBC CoeTypingBC} % then sub A C CoeAC CoeTypingAC -> type. %mode sub-trans +SubAB +SubBC -SubAC. %name sub-trans _Trans. - : sub-trans Sub1 Sub2 Sub <- sub-trans' pacifier/i Sub1 Sub2 Sub. %worlds () (sub-trans _ _ _). %total {} (sub-trans Sub1 Sub2 _).