1(* standard prelude *) 2open HolKernel boolLib Parse 3 4 5(* extra theorem-proving oomph from libraries *) 6open bossLib metisLib ncLib BasicProvers boolSimps 7 8 9 10(* ancestor theories *) 11open fsubtypesTheory pred_setTheory 12 13val _ = new_theory "kernel_subtyping" 14 15 16 17(* set up syntax for subtyping judgements *) 18val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 19 fixity = Infix(NONASSOC, 425), 20 paren_style = OnlyIfNecessary, 21 pp_elements = [HardSpace 1, TOK "|-", BreakSpace(1, 0), 22 BeginFinalBlock(PP.INCONSISTENT, 2), 23 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)], 24 term_name = "fsubtyping"} 25 26(* define subtyping rules *) 27val (fsubtyping_rules, fsubtyping_ind, fsubtyping_cases) = Hol_reln` 28 (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==> 29 Gamma |- ty <: ty) /\ 30 (!Gamma ty1 ty2 ty3. Gamma |- ty1 <: ty2 /\ 31 Gamma |- ty2 <: ty3 ==> 32 Gamma |- ty1 <: ty3) /\ 33 (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==> 34 Gamma |- ty <: Top) /\ 35 (!Gamma x ty. wfctxt Gamma /\ MEM (x, ty) Gamma ==> 36 Gamma |- TyVar x <: ty) /\ 37 (!Gamma s1 t1 s2 t2. 38 Gamma |- t1 <: s1 /\ Gamma |- s2 <: t2 ==> 39 Gamma |- Fun s1 s2 <: Fun t1 t2) /\ 40 (!Gamma x u1 s2 t2. 41 ((x,u1) :: Gamma) |- s2 <: t2 ==> 42 Gamma |- ForallTy x u1 s2 <: ForallTy x u1 t2) 43`; 44 45(* prove that sub-typing relation "respects" permutation *) 46val fsubtyping_swap = store_thm( 47 "fsubtyping_swap", 48 ``!Gamma ty1 ty2. 49 Gamma |- ty1 <: ty2 ==> 50 ctxtswap x y Gamma |- fswap x y ty1 <: fswap x y ty2``, 51 HO_MATCH_MP_TAC fsubtyping_ind THEN 52 REPEAT CONJ_TAC THENL [ 53 (* refl *) SRW_TAC [][SUBSET_DEF, fsubtyping_rules], 54 (* trans *) METIS_TAC [fsubtyping_rules], 55 (* top *) SRW_TAC [][fsubtyping_rules, SUBSET_DEF], 56 (* tvar *) SRW_TAC [][fsubtyping_rules], 57 (* fun *) SRW_TAC [][fsubtyping_rules], 58 (* forall *)SRW_TAC [][fsubtyping_rules, SUBSET_DEF] 59 ]); 60 61val fsubtyping_wfctxt = store_thm( 62 "fsubtyping_wfctxt", 63 ``!G ty1 ty2. G |- ty1 <: ty2 ==> wfctxt G``, 64 HO_MATCH_MP_TAC fsubtyping_ind THEN SRW_TAC [][]); 65 66val strong_fsubtyping_ind = 67 IndDefRules.derive_strong_induction (CONJUNCTS fsubtyping_rules, 68 fsubtyping_ind) 69 70val fsubtyping_fv_constraint = store_thm( 71 "fsubtyping_fv_constraint", 72 ``!G ty1 ty2. G |- ty1 <: ty2 ==> 73 ftyFV ty1 SUBSET cdom G /\ 74 ftyFV ty2 SUBSET cdom G``, 75 HO_MATCH_MP_TAC strong_fsubtyping_ind THEN 76 SRW_TAC [][SUBSET_DEF] THEN 77 TRY (IMP_RES_TAC fsubtyping_wfctxt) THEN 78 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [wfctxt_MEM, SUBSET_DEF]); 79 80(* define algorithmic sub-typing, with a depth of derivation parameter *) 81val (algn_subtyping_rules, algn_subtyping_ind, algn_subtyping_cases) = 82 Hol_reln` 83 (!Gamma s. wfctxt Gamma /\ ftyFV s SUBSET cdom Gamma ==> 84 algn_subtyping 0 Gamma s Top) /\ 85 (!Gamma x. wfctxt Gamma /\ x IN cdom Gamma ==> 86 algn_subtyping 0 Gamma (TyVar x) (TyVar x)) /\ 87 (!Gamma x u t n. MEM (x, u) Gamma /\ algn_subtyping n Gamma u t ==> 88 algn_subtyping (n + 1) Gamma (TyVar x) t) /\ 89 (!Gamma t1 s1 t2 s2 n m. 90 algn_subtyping n Gamma t1 s1 /\ 91 algn_subtyping m Gamma s2 t2 ==> 92 algn_subtyping (MAX n m + 1) Gamma (Fun s1 s2) (Fun t1 t2)) /\ 93 (!Gamma x u1 s2 t2 n. 94 algn_subtyping n ((x,u1)::Gamma) s2 t2 ==> 95 algn_subtyping (n + 1) Gamma (ForallTy x u1 s2) 96 (ForallTy x u1 t2)) 97`; 98 99(* algorithmic sub-typing also respects permutation *) 100val algn_subtyping_fswap = store_thm( 101 "algn_subtyping_fswap", 102 ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==> 103 !x y. algn_subtyping n (ctxtswap x y G) 104 (fswap x y ty1) 105 (fswap x y ty2)``, 106 HO_MATCH_MP_TAC algn_subtyping_ind THEN REPEAT CONJ_TAC THEN 107 SRW_TAC [][algn_subtyping_rules] THEN 108 METIS_TAC [algn_subtyping_rules, MEM_ctxtswap, fswap_inv, 109 swapTheory.swapstr_inverse]); 110 111(* this equivalence applies more often than the one above; it removes 112 any permutations that might have appeared on the first argument *) 113val algn_subtyping_fswap1_eq = store_thm( 114 "algn_subtyping_fswap1_eq", 115 ``algn_subtyping n G (fswap x y ty1) ty2 = 116 algn_subtyping n (ctxtswap x y G) ty1 (fswap x y ty2)``, 117 METIS_TAC [algn_subtyping_fswap, fswap_inv, ctxtswap_inv]); 118 119val algn_subtyping_wfctxt = store_thm( 120 "algn_subtyping_wfctxt", 121 ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==> wfctxt G``, 122 HO_MATCH_MP_TAC algn_subtyping_ind THEN SRW_TAC [][]); 123 124 125(* set up syntax for algorithmic sub-typing relation without the depth 126 parameter *) 127val _ = remove_rules_for_term "dSUB" 128 129val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 130 fixity = Infix(NONASSOC, 425), 131 paren_style = OnlyIfNecessary, 132 pp_elements = [HardSpace 1, TOK "|->", BreakSpace(1, 0), 133 BeginFinalBlock(PP.INCONSISTENT, 2), 134 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)], 135 term_name = "alg_subtyping"} 136 137val alg_subtyping_def = Define` 138 Gamma |-> s <: t = ?n. algn_subtyping n Gamma s t 139`; 140 141val alg_subtyping_fswap1_eq = store_thm( 142 "alg_subtyping_fswap1_eq", 143 ``Gamma |-> fswap x y ty1 <: ty2 = 144 ctxtswap x y Gamma |-> ty1 <: fswap x y ty2``, 145 METIS_TAC [alg_subtyping_def, algn_subtyping_fswap1_eq]); 146 147fun derive_rule th0 = let 148 val (vs, base) = strip_forall (concl th0) 149 val th = UNDISCH_ALL (SPEC_ALL th0) 150 val (f, args) = strip_comb (concl th) 151 val n = mk_var("n", numSyntax.num) 152 val pattern = mk_exists(n, list_mk_comb(f, n::tl args)) 153 val witness = hd args 154 val ex_thm = EXISTS (pattern, witness) th 155 val discharged = 156 GENL vs (DISCH_ALL (REWRITE_RULE [GSYM alg_subtyping_def] ex_thm)) 157 val exs_in = SIMP_RULE bool_ss [LEFT_FORALL_IMP_THM, 158 LEFT_EXISTS_AND_THM, 159 RIGHT_EXISTS_AND_THM] discharged 160in 161 REWRITE_RULE [GSYM alg_subtyping_def] exs_in 162end 163 164val alg_subtyping_rules = save_thm( 165 "alg_subtyping_rules", 166 LIST_CONJ (map derive_rule (CONJUNCTS algn_subtyping_rules))); 167 168(* derive the rule induction principle for algorithmic sub-typing *) 169val alg_subtyping_ind = 170 (Q.GEN `P` o 171 SIMP_RULE (srw_ss()) [GSYM alg_subtyping_def] o 172 CONV_RULE (RAND_CONV 173 (SWAP_VARS_CONV THENC 174 BINDER_CONV (SWAP_VARS_CONV THENC 175 BINDER_CONV (SWAP_VARS_CONV THENC 176 BINDER_CONV FORALL_IMP_CONV)))) o 177 SIMP_RULE (srw_ss()) [] o 178 Q.SPEC `\n G ty1 ty2. P G ty1 ty2`) algn_subtyping_ind 179 180(* likewise for the "cases" or inversion theorem *) 181val alg_subtyping_cases = 182 (REWRITE_CONV [alg_subtyping_def] THENC 183 ONCE_REWRITE_CONV [algn_subtyping_cases] THENC 184 SIMP_CONV (srw_ss()) [EXISTS_OR_THM] THENC 185 SIMP_CONV (srw_ss()) 186 (map (INST_TYPE [alpha |-> numSyntax.num]) 187 [LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM]) THENC 188 REWRITE_CONV [GSYM alg_subtyping_def]) 189 ``Gamma |-> ty1 <: ty2`` 190 191val alg_subtyping_refl (* lemma 28.3.1 *) = store_thm( 192 "alg_subtyping_refl", 193 ``!ty G. wfctxt G /\ ftyFV ty SUBSET cdom G ==> G |-> ty <: ty``, 194 HO_MATCH_MP_TAC fsubty_ind THEN 195 SRW_TAC [][alg_subtyping_rules] THEN 196 Q_TAC (NEW_TAC "z") `cdom G UNION ftyFV ty UNION ftyFV ty'` THEN 197 `ForallTy v ty ty' = ForallTy z ty (fswap z v ty')` 198 by SRW_TAC [][ForallTy_ALPHA] THEN 199 SRW_TAC [][] THEN 200 MATCH_MP_TAC (last (CONJUNCTS alg_subtyping_rules)) THEN 201 SRW_TAC [][alg_subtyping_fswap1_eq] THEN 202 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 203 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 204 METIS_TAC [swapTheory.swapstr_def]); 205val _ = export_rewrites ["alg_subtyping_refl"] 206 207val alg_subtyping_top_left = store_thm( 208 "alg_subtyping_top_left", 209 ``!Gamma t. wfctxt Gamma ==> (Gamma |-> Top <: t = (t = Top))``, 210 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM, alg_subtyping_rules] THEN 211 ONCE_REWRITE_TAC [alg_subtyping_cases] THEN 212 SRW_TAC [][]); 213val _ = export_rewrites ["alg_subtyping_top_left"] 214 215val alg_subtyping_tyvar_right0 = prove( 216 ``!Gamma ty1 ty2. Gamma |-> ty1 <: ty2 ==> 217 !x. (ty2 = TyVar x) ==> 218 ?y. ty1 = TyVar y``, 219 HO_MATCH_MP_TAC alg_subtyping_ind THEN SRW_TAC [][]); 220val alg_subtyping_tyvar_right = save_thm( 221 "alg_subtyping_tyvar_right", 222 SIMP_RULE (bool_ss ++ DNF_ss) [] alg_subtyping_tyvar_right0) 223 224val strong_algn_subtyping_ind = 225 IndDefRules.derive_strong_induction (CONJUNCTS algn_subtyping_rules, 226 algn_subtyping_ind) 227 228val algn_subtyping_ftyFVs_in_ctxt = store_thm( 229 "algn_subtyping_ftyFVs_in_ctxt", 230 ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==> 231 ftyFV ty1 SUBSET cdom G /\ ftyFV ty2 SUBSET cdom G``, 232 HO_MATCH_MP_TAC strong_algn_subtyping_ind THEN 233 SRW_TAC [][SUBSET_DEF] THEN 234 TRY (IMP_RES_TAC algn_subtyping_wfctxt) THEN 235 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [cdom_MEM]) 236 237val algn_subtyping_swap = store_thm( 238 "algn_subtyping_swap", 239 ``!n G ty1 ty2. 240 algn_subtyping n G ty1 ty2 ==> 241 !x y. algn_subtyping n (ctxtswap x y G) (fswap x y ty1) (fswap x y ty2)``, 242 HO_MATCH_MP_TAC algn_subtyping_ind THEN 243 SRW_TAC [][algn_subtyping_rules] THEN 244 MATCH_MP_TAC (List.nth(CONJUNCTS algn_subtyping_rules, 2)) THEN 245 Q.EXISTS_TAC `fswap x' y ty1` THEN SRW_TAC [][]); 246val algn_subtyping_swap1_eqn = store_thm( 247 "algn_subtyping_swap1_eqn", 248 ``algn_subtyping n G (fswap x y ty1) ty2 = 249 algn_subtyping n (ctxtswap x y G) ty1 (fswap x y ty2)``, 250 METIS_TAC [algn_subtyping_swap, ctxtswap_inv, fswap_inv]); 251 252 253(* important to have this sort of inversion theorem, where you get the 254 same bound variable in the "other" position of the relation. By 255 analogy, in the lambda calculus with beta reduction, you have to prove 256 that if 257 LAM v bod --> t 258 then 259 ?bod'. (t = LAM v bod') /\ bod --> bod' 260 In the lambda calculus, it's always possible to get this v (which 261 has to do with the fact that beta reduction doesn't produce extra 262 free variables). In F<:, your x has to satisfy certain constraints. 263*) 264val algn_subtyping_ForallTy_eqn = store_thm( 265 "algn_subtyping_ForallTy_eqn", 266 ``~(x IN ftyFV bnd) /\ ~(x IN cdom G) ==> 267 (algn_subtyping p G (ForallTy x bnd ty) t = 268 wfctxt G /\ 269 ((t = Top) /\ (p = 0) /\ ftyFV (ForallTy x bnd ty) SUBSET cdom G \/ 270 (?ty' p0. (t = ForallTy x bnd ty') /\ (p = p0 + 1) /\ 271 algn_subtyping p0 ((x,bnd)::G) ty ty')))``, 272 SIMP_TAC (srw_ss() ++ DNF_ss ++ SatisfySimps.SATISFY_ss) 273 [EQ_IMP_THM, algn_subtyping_rules, algn_subtyping_wfctxt] THEN 274 STRIP_TAC THEN 275 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [algn_subtyping_cases])) THEN 276 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [ForallTy_11] THEN 277 Q.EXISTS_TAC `fswap x x' t2` THEN 278 `wfctxt ((x',u1)::G)` by METIS_TAC [algn_subtyping_wfctxt] THEN 279 FULL_SIMP_TAC (srw_ss()) [algn_subtyping_swap1_eqn] THEN 280 `ftyFV t2 SUBSET cdom ((x',u1)::G)` 281 by METIS_TAC [algn_subtyping_ftyFVs_in_ctxt] THEN 282 Cases_on `x = x'` THEN1 SRW_TAC [][] THEN 283 `~(x' IN ftyFV u1) /\ ~(x IN ftyFV t2)` 284 by METIS_TAC [SUBSET_DEF, cdom_def, pairTheory.FST, IN_INSERT] THEN 285 SRW_TAC [][ctxtswap_fresh, fswap_fresh, wfctxt_ctxtFV_cdom]); 286 287val algn_subtyping_trans = prove( 288 ``!n m p Gamma s q t. 289 (n = m + p) /\ 290 algn_subtyping m Gamma s q /\ 291 algn_subtyping p Gamma q t ==> 292 ?r. algn_subtyping r Gamma s t``, 293 HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN 294 REPEAT STRIP_TAC THEN 295 Q.PAT_ASSUM `algn_subtyping m Gamma s q` 296 (MP_TAC o ONCE_REWRITE_RULE [algn_subtyping_cases]) THEN 297 SRW_TAC [][] THENL [ 298 METIS_TAC [alg_subtyping_def, alg_subtyping_top_left, 299 algn_subtyping_rules], 300 METIS_TAC [], 301 FULL_SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 302 `?r. algn_subtyping r Gamma u t` 303 by METIS_TAC [DECIDE ``n + p < n + 1 + p``] THEN 304 METIS_TAC [algn_subtyping_rules], 305 Q.PAT_ASSUM `algn_subtyping p Gamma (Fun t1 t2) t` 306 (MP_TAC o ONCE_REWRITE_RULE [algn_subtyping_cases]) THEN 307 SRW_TAC [][] THEN1 METIS_TAC [algn_subtyping_rules, 308 algn_subtyping_ftyFVs_in_ctxt] THEN 309 FULL_SIMP_TAC (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] THEN 310 `?r. algn_subtyping r Gamma t1' s1` 311 by (FIRST_X_ASSUM MATCH_MP_TAC THEN 312 MAP_EVERY Q.EXISTS_TAC [`n'`, `n`, `t1`] THEN 313 ASM_SIMP_TAC arith_ss [arithmeticTheory.MAX_DEF]) THEN 314 `?r'. algn_subtyping r' Gamma s2 t2'` 315 by (FIRST_X_ASSUM MATCH_MP_TAC THEN 316 MAP_EVERY Q.EXISTS_TAC [`m'`, `m`, `t2`] THEN 317 ASM_SIMP_TAC arith_ss [arithmeticTheory.MAX_DEF]) THEN 318 METIS_TAC [algn_subtyping_rules], 319 `wfctxt ((x,u1)::Gamma)` by METIS_TAC [algn_subtyping_wfctxt] THEN 320 FULL_SIMP_TAC (srw_ss()) [] THEN 321 `~(x IN ftyFV u1)` by METIS_TAC [SUBSET_DEF] THEN 322 Q.PAT_ASSUM `algn_subtyping p Gamma (ForallTy x u1 t2) t` MP_TAC THEN 323 ASM_SIMP_TAC (srw_ss()) [algn_subtyping_ForallTy_eqn] THEN 324 SRW_TAC [][] THENL [ 325 (* case where it's less than Top *) 326 IMP_RES_TAC algn_subtyping_ftyFVs_in_ctxt THEN 327 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [], 328 ALL_TAC 329 ] THEN 330 SRW_TAC [][ForallTy_11] THEN 331 METIS_TAC [DECIDE ``n + p0 < n + 1 + (p0 + 1)``] 332 ]); 333 334val alg_subtyping_trans (* lemma 28.3.2 *) = store_thm( 335 "alg_subtyping_trans", 336 ``!Gamma s q. Gamma |-> s <: q /\ Gamma |-> q <: t ==> 337 Gamma |-> s <: t``, 338 METIS_TAC [alg_subtyping_def, algn_subtyping_trans]); 339 340val alg_soundcomplete (* theorem 28.3.3 *) = store_thm( 341 "alg_soundcomplete", 342 ``G |- ty1 <: ty2 = G |-> ty1 <: ty2``, 343 EQ_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`ty2`, `ty1`, `G`] THENL [ 344 HO_MATCH_MP_TAC fsubtyping_ind THEN SRW_TAC [][alg_subtyping_rules] THENL [ 345 METIS_TAC [alg_subtyping_trans], 346 `Gamma |-> ty <: ty` 347 by METIS_TAC [alg_subtyping_refl, wfctxt_MEM, SUBSET_DEF] THEN 348 METIS_TAC [alg_subtyping_rules] 349 ], 350 HO_MATCH_MP_TAC alg_subtyping_ind THEN SRW_TAC [][fsubtyping_rules] THEN 351 METIS_TAC [fsubtyping_rules, wfctxt_MEM, SUBSET_DEF, 352 fsubtyping_wfctxt] 353 ]); 354 355val _ = export_theory (); 356