text_formalization/tame/CRTTXAT.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Tame Hypermap                                                     *)\r
   5 (* Author: Alexey Solovyev                                                    *)\r
   6 (* Date: 2010-06-17                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 (******************************)\r
  10 (* Proof of CRTTXAT (tame_9a) *)\r
  11 (******************************)\r
  12 \r
  13 \r
  14 flyspeck_needs "tame/TameGeneral.hl";;\r
  15 flyspeck_needs "tame/ArcProperties.hl";;\r
  16 \r
  17 \r
  18 module Crttxat_tame = struct\r
  19 \r
  20 \r
  21 open Fan_defs;;\r
  22 open Tame_defs;;\r
  23 open Tame_general;;\r
  24 open Hypermap_and_fan;;\r
  25 open Arc_properties;;\r
  26 \r
  27 \r
  28 \r
  29 (* An auxiliary result about sums over a face *)\r
  30 let ORBIT_MAP_PAIR_SUM_lemma = prove(`!P s f g (x:A#A). FINITE s /\ f permutes s /\\r
  31                                                 (!y. y IN orbit_map f x ==> f y = (SND y, g y))\r
  32                                                 ==> sum (orbit_map f x) (\x. P (FST x)) = sum (orbit_map f x) (\x. P (SND x))`,\r
  33    REPEAT STRIP_TAC THEN\r
  34      ABBREV_TAC `k = CARD (orbit_map f (x:A#A))` THEN\r
  35      MP_TAC (ISPECL [`(\x:A#A. (P:A->real) (FST x))`; `s:A#A->bool`; `f:A#A->A#A`; `x:A#A`; `k:num`; `1`] SUM_ORBIT) THEN\r
  36      ASM_REWRITE_TAC[] THEN\r
  37      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
  38      MP_TAC (ISPECL [`(\x:A#A. (P:A->real) (SND x))`; `s:A#A->bool`; `f:A#A->A#A`; `x:A#A`; `k:num`; `0`] SUM_ORBIT) THEN\r
  39      ASM_REWRITE_TAC[] THEN\r
  40      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
  41      REWRITE_TAC[ARITH_RULE `1 + k - 1 = (k - 1) + 1`] THEN\r
  42      GEN_REWRITE_TAC (DEPTH_CONV o (PAT_CONV `\x. sum (x..m) f`)) [ARITH_RULE `1 = 0 + 1`] THEN\r
  43      REWRITE_TAC[SUM_OFFSET; ARITH_RULE `0 + a = a`] THEN\r
  44      MATCH_MP_TAC SUM_EQ THEN\r
  45      X_GEN_TAC `i:num` THEN BETA_TAC THEN\r
  46      REWRITE_TAC[ARITH_RULE `i + 1 = 1 + i`] THEN\r
  47      REWRITE_TAC[Hypermap.addition_exponents; Hypermap.POWER_1; o_THM] THEN\r
  48      ABBREV_TAC `y:A#A = (f POWER i) x` THEN\r
  49      SUBGOAL_THEN `y:A#A IN orbit_map f x` ASSUME_TAC THENL\r
  50      [\r
  51        EXPAND_TAC "y" THEN\r
  52          REWRITE_TAC[Hypermap.lemma_in_orbit];\r
  53        ALL_TAC\r
  54      ] THEN\r
  55      FIRST_X_ASSUM (MP_TAC o SPEC `y:A#A`) THEN\r
  56      ASM_SIMP_TAC[]);;\r
  57 \r
  58 \r
  59 \r
  60 \r
  61 let FACE_SUM_lemma = prove(`!V E x P. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)\r
  62                              ==> sum (face (hypermap_of_fan (V,E)) x) (\x. P (FST x)) = \r
  63                                  sum (face (hypermap_of_fan (V,E)) x) (\x. P (SND x))`,\r
  64    REPEAT STRIP_TAC THEN\r
  65      REWRITE_TAC[Hypermap.face] THEN\r
  66      MATCH_MP_TAC ORBIT_MAP_PAIR_SUM_lemma THEN\r
  67      EXISTS_TAC `dart (hypermap_of_fan (V,E))` THEN\r
  68      EXISTS_TAC `(\x. SND (face_map (hypermap_of_fan (V,E)) x))` THEN\r
  69      REWRITE_TAC[Hypermap.hypermap_lemma; GSYM Hypermap.face] THEN\r
  70      ASM_SIMP_TAC[Hypermap.face_map; HYPERMAP_OF_FAN] THEN\r
  71      REPEAT STRIP_TAC THEN\r
  72      SUBGOAL_THEN `y IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL\r
  73      [\r
  74        MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
  75          EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN\r
  76          ASM_REWRITE_TAC[] THEN\r
  77          MATCH_MP_TAC FACE_SUBSET_DART1_OF_FAN THEN\r
  78          ASM_REWRITE_TAC[];\r
  79        ALL_TAC\r
  80      ] THEN\r
  81      ASM_REWRITE_TAC[f_fan_pair_ext] THEN\r
  82      MP_TAC (ISPEC `y:real^3#real^3` PAIR_SURJECTIVE) THEN\r
  83      STRIP_TAC THEN\r
  84      ASM_REWRITE_TAC[f_fan_pair]);;\r
  85    \r
  86 \r
  87 \r
  88 \r
  89 \r
  90 let CRTTXAT_lemma1 = prove(`!V f. simple_hypermap (hypermap_of_fan (V,ESTD V)) ==>\r
  91                              contravening V /\ f IN face_set (hypermap_of_fan (V,ESTD V)) ==>\r
  92                              sum f (\x. lmfun (h_dart x)) >= &12 + &(CARD f) - &(CARD V)`,\r
  93    REPEAT GEN_TAC THEN DISCH_TAC THEN\r
  94      DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "A") MP_TAC) THEN\r
  95      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
  96      USE_THEN "A" MP_TAC THEN\r
  97      REWRITE_TAC[contravening] THEN\r
  98      REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN\r
  99      DISCH_THEN (CONJUNCTS_THEN2 MP_TAC (fun th -> ALL_TAC)) THEN\r
 100      REPEAT STRIP_TAC THEN\r
 101      SUBGOAL_THEN `sum f (\x:real^3#real^3. lmfun (h_dart x)) = sum {FST x | x IN f} (\v. lmfun ((norm v) / &2))` ASSUME_TAC THENL\r
 102      [\r
 103        REWRITE_TAC[IMAGE_LEMMA; h_dart] THEN\r
 104          SUBGOAL_THEN `(\x:real^3#real^3. lmfun (norm (FST x) / &2)) = (\v. lmfun (norm v / &2)) o FST` ASSUME_TAC THENL\r
 105          [\r
 106            REWRITE_TAC[FUN_EQ_THM; o_THM];\r
 107            ALL_TAC\r
 108          ] THEN\r
 109          ASM_REWRITE_TAC[] THEN\r
 110          MATCH_MP_TAC EQ_SYM THEN\r
 111          MATCH_MP_TAC SUM_IMAGE THEN\r
 112          REPEAT STRIP_TAC THEN\r
 113          MP_TAC (SPEC_ALL (SPECL [`V:real^3->bool`; `ESTD V`] HYPERMAP_OF_FAN_FACE_NODE_INJ)) THEN\r
 114          ASM_REWRITE_TAC[];\r
 115        ALL_TAC\r
 116      ] THEN\r
 117      POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN\r
 118      ABBREV_TAC `A = {FST (x:real^3#real^3) | x IN f}` THEN\r
 119 \r
 120      SUBGOAL_THEN `A:real^3->bool SUBSET V` ASSUME_TAC THENL\r
 121      [\r
 122        EXPAND_TAC "A" THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN\r
 123          X_GEN_TAC `v:real^3` THEN DISCH_THEN (CHOOSE_THEN MP_TAC) THEN\r
 124          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN\r
 125          REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face; IN_ELIM_THM] THEN\r
 126          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN\r
 127          SUBGOAL_THEN `x:real^3#real^3 IN dart (hypermap_of_fan (V,ESTD V))` MP_TAC THENL\r
 128          [\r
 129            MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 130              EXISTS_TAC `f:real^3#real^3->bool` THEN\r
 131              ASM_SIMP_TAC[Hypermap.lemma_face_subset];\r
 132            ALL_TAC\r
 133          ] THEN\r
 134 \r
 135          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 136          MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN\r
 137          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 138          MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x'':real^3`; `y:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 139          ASM_SIMP_TAC[];\r
 140        ALL_TAC\r
 141      ] THEN\r
 142 \r
 143      SUBGOAL_THEN `A:real^3->bool = V DIFF (V DIFF A)` MP_TAC THENL\r
 144      [\r
 145        MATCH_MP_TAC DIFF_LEMMA THEN ASM_REWRITE_TAC[];\r
 146        ALL_TAC\r
 147      ] THEN\r
 148 \r
 149      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN\r
 150      SUBGOAL_THEN `FINITE (V:real^3->bool)` ASSUME_TAC THENL\r
 151      [\r
 152        UNDISCH_TAC `FAN (vec 0, V, ESTD V)` THEN\r
 153          SIMP_TAC[Fan_defs.FAN; Fan_defs.fan1];\r
 154        ALL_TAC\r
 155      ] THEN\r
 156 \r
 157      SUBGOAL_THEN `sum (V DIFF (V DIFF A)) (\v:real^3. lmfun (norm v / &2)) = scriptL V - sum (V DIFF A) (\v. lmfun (norm v / &2))` MP_TAC THENL\r
 158      [\r
 159        REWRITE_TAC[scriptL] THEN\r
 160          MATCH_MP_TAC SUM_DIFF THEN\r
 161          ASM_REWRITE_TAC[SUBSET_DIFF];\r
 162        ALL_TAC\r
 163      ] THEN\r
 164 \r
 165      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 166      MATCH_MP_TAC (REAL_ARITH `a >= c /\ b <= --d ==> a - b >= c + d`) THEN\r
 167      FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `&12`)) THEN\r
 168      SIMP_TAC[real_ge; real_gt; REAL_LT_IMP_LE] THEN DISCH_TAC THEN\r
 169      MATCH_MP_TAC REAL_LE_TRANS THEN\r
 170      EXISTS_TAC `&(CARD (V:real^3->bool DIFF A)) * &1` THEN\r
 171      CONJ_TAC THENL\r
 172      [\r
 173        MATCH_MP_TAC SUM_BOUND THEN\r
 174          CONJ_TAC THENL\r
 175          [\r
 176            MATCH_MP_TAC FINITE_DIFF THEN\r
 177              ASM_REWRITE_TAC[];\r
 178            ALL_TAC\r
 179          ] THEN\r
 180 \r
 181          X_GEN_TAC `v:real^3` THEN REWRITE_TAC[IN_DIFF] THEN\r
 182          STRIP_TAC THEN\r
 183          MP_TAC (SPEC_ALL CONTRAVENING_LMFUN_BOUND) THEN\r
 184          ASM_REWRITE_TAC[];\r
 185        ALL_TAC\r
 186      ] THEN\r
 187 \r
 188      SUBGOAL_THEN `CARD (V:real^3->bool DIFF A) = CARD V - CARD A /\ CARD A <= CARD V` MP_TAC THENL\r
 189      [\r
 190        CONJ_TAC THENL\r
 191          [\r
 192            MATCH_MP_TAC CARD_DIFF THEN\r
 193              ASM_REWRITE_TAC[];\r
 194            MATCH_MP_TAC CARD_SUBSET THEN\r
 195              ASM_REWRITE_TAC[]\r
 196          ];\r
 197        ALL_TAC\r
 198      ] THEN\r
 199   \r
 200      STRIP_TAC THEN\r
 201      MP_TAC (SPECL [`CARD (A:real^3->bool)`; `CARD (V:real^3->bool)`] REAL_OF_NUM_SUB) THEN\r
 202      ASM_REWRITE_TAC[] THEN\r
 203      DISCH_THEN (fun th -> REWRITE_TAC[SYM th; REAL_MUL_RID; REAL_NEG_SUB]) THEN\r
 204      SUBGOAL_THEN `CARD (A:real^3->bool) = CARD (f:real^3#real^3->bool)` MP_TAC THENL\r
 205      [\r
 206        EXPAND_TAC "A" THEN\r
 207          REWRITE_TAC[IMAGE_LEMMA] THEN\r
 208          MATCH_MP_TAC CARD_IMAGE_INJ THEN\r
 209          CONJ_TAC THENL\r
 210          [\r
 211            REPEAT GEN_TAC THEN\r
 212              MP_TAC (SPEC_ALL (SPECL [`V:real^3->bool`; `ESTD V`] HYPERMAP_OF_FAN_FACE_NODE_INJ)) THEN\r
 213              ASM_SIMP_TAC[];\r
 214            ALL_TAC\r
 215          ] THEN\r
 216 \r
 217          FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN\r
 218          REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
 219          REWRITE_TAC[IN_ELIM_THM] THEN\r
 220          STRIP_TAC THEN ASM_REWRITE_TAC[Hypermap.FACE_FINITE];\r
 221        ALL_TAC\r
 222      ] THEN\r
 223 \r
 224      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 225      REWRITE_TAC[REAL_LE_REFL]);;\r
 226 \r
 227 \r
 228 \r
 229 \r
 230 \r
 231 \r
 232 \r
 233 (* Another expression for the perimeter of f *)\r
 234 let CRTTXAT_lemma2 = prove(`!V f. FAN (vec 0,V,ESTD V) /\ f IN face_set (hypermap_of_fan (V,ESTD V))\r
 235                              ==> sum f (\(v,w). arcV (vec 0) v w) = sum f (\(v,w). arclength (norm v) (norm w) (dist (v,w)))`,\r
 236    REPEAT STRIP_TAC THEN\r
 237      MATCH_MP_TAC SUM_EQ THEN\r
 238      GEN_TAC THEN\r
 239      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN\r
 240      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN\r
 241      DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN\r
 242      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 243      REWRITE_TAC[GSYM DIST_0] THEN\r
 244      MATCH_MP_TAC Trigonometry1.arcVarc THEN\r
 245 \r
 246      SUBGOAL_THEN `(v,w) IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL\r
 247      [\r
 248        MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 249          EXISTS_TAC `f:real^3#real^3->bool` THEN\r
 250          POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN\r
 251          FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN\r
 252          REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face; IN_ELIM_THM] THEN\r
 253          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 254          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
 255          MATCH_MP_TAC FACE_SUBSET_DART_OF_FAN THEN\r
 256          ASM_REWRITE_TAC[];\r
 257        ALL_TAC\r
 258      ] THEN\r
 259 \r
 260      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 261      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 262      FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `(vec 0:real^3,V,ESTD V)`)) THEN\r
 263      REWRITE_TAC[Fan_defs.FAN; Fan_defs.fan2] THEN\r
 264      POP_ASSUM MP_TAC THEN\r
 265      SET_TAC[]);;\r
 266 \r
 267 \r
 268 \r
 269 (* A variation of the first lemma *)\r
 270 let CRTTXAT_lemma1' = prove(`!V f. simple_hypermap (hypermap_of_fan (V,ESTD V)) ==>\r
 271                              contravening V /\ f IN face_set (hypermap_of_fan (V,ESTD V)) ==>\r
 272                              sum f (\x. lmfun (norm (SND x) / &2)) >= &12 + &(CARD f) - &(CARD V)`,\r
 273    REPEAT STRIP_TAC THEN\r
 274      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 275      SUBGOAL_THEN `sum f (\x:real^3#real^3. lmfun (norm (SND x) / &2)) = sum f (\x. lmfun (h_dart x))` (fun th -> REWRITE_TAC[th]) THENL\r
 276      [\r
 277        FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN\r
 278          REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
 279          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 280          REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN\r
 281          ASM_REWRITE_TAC[h_dart] THEN\r
 282          MATCH_MP_TAC (GSYM FACE_SUM_lemma) THEN\r
 283          ASM_REWRITE_TAC[] THEN\r
 284          MATCH_MP_TAC CONTRAVENING_IMP_IN_DART1_OF_FAN THEN\r
 285          ASM_REWRITE_TAC[];\r
 286        ALL_TAC\r
 287      ] THEN\r
 288      MP_TAC (SPEC_ALL CRTTXAT_lemma1) THEN\r
 289      ASM_SIMP_TAC[]);;\r
 290      \r
 291 \r
 292 \r
 293 \r
 294 \r
 295 (* LEMMA: aux *)\r
 296 let SUM_RMUL_BOUND = prove(`!(s:A->bool) f g c. FINITE s /\ \r
 297                                 (!x. x IN s ==> c <= g x /\ &0 <= f x)\r
 298                               ==> sum s (\x. f x) * c <= sum s (\x. f x * g x)`,\r
 299    REPEAT STRIP_TAC THEN\r
 300      REWRITE_TAC[GSYM SUM_RMUL] THEN\r
 301      MATCH_MP_TAC SUM_LE THEN\r
 302      ASM_REWRITE_TAC[] THEN GEN_TAC THEN\r
 303      DISCH_TAC THEN\r
 304      MATCH_MP_TAC REAL_LE_LMUL THEN\r
 305      ASM_SIMP_TAC[]);;\r
 306      \r
 307 \r
 308 \r
 309 \r
 310 (* Main theorem *)\r
 311 let CRTTXAT_concl = `!V. contravening V /\ (perimeterbound (V, ESTD V))==> \r
 312        tame_9a  (hypermap_of_fan (V, ESTD V))`;;\r
 313 \r
 314 \r
 315 \r
 316 let CRTTXAT_assum = mk_imp (list_mk_conj [`!V. contravening V ==> simple_hypermap (hypermap_of_fan (V,ESTD V))`], CRTTXAT_concl);;\r
 317 \r
 318 \r
 319 (* g(CRTTXAT_assum);; *)\r
 320 let CRTTXAT = prove(CRTTXAT_assum,\r
 321    REPEAT STRIP_TAC THEN\r
 322      FIRST_X_ASSUM (MP_TAC o SPEC `V:real^3->bool`) THEN\r
 323      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN\r
 324      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN\r
 325 \r
 326      REWRITE_TAC[tame_9a] THEN\r
 327      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 328      REPEAT STRIP_TAC THENL\r
 329      [\r
 330        MP_TAC (SPEC_ALL CONTRAVENING_IMP_CARD_FACE_GE_3) THEN\r
 331          ASM_REWRITE_TAC[] THEN\r
 332          DISCH_THEN (MP_TAC o SPEC `x:real^3#real^3`) THEN\r
 333          ASM_SIMP_TAC[];\r
 334        ALL_TAC\r
 335      ] THEN\r
 336 \r
 337      ABBREV_TAC `f = face (hypermap_of_fan (V,ESTD V)) x` THEN\r
 338      ABBREV_TAC `k = CARD (f:real^3#real^3->bool)` THEN\r
 339      \r
 340      FIRST_X_ASSUM (MP_TAC o check (fun th -> rator (concl th) = `perimeterbound`)) THEN\r
 341      REWRITE_TAC[perimeterbound] THEN\r
 342      DISCH_THEN (MP_TAC o SPEC `f:(real^3#real^3->bool)`) THEN\r
 343 \r
 344      SUBGOAL_THEN `f IN face_set_of_fan (V,ESTD V) /\ FINITE f` MP_TAC THENL\r
 345      [\r
 346        EXPAND_TAC "f" THEN REWRITE_TAC[Hypermap.FACE_FINITE] THEN\r
 347          REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
 348          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 349          REWRITE_TAC[IN_ELIM_THM] THEN\r
 350          EXISTS_TAC `x:real^3#real^3` THEN\r
 351          ASM_REWRITE_TAC[];\r
 352        ALL_TAC\r
 353      ] THEN\r
 354 \r
 355      SIMP_TAC[face_set_of_fan] THEN DISCH_TAC THEN\r
 356      MP_TAC (SPEC_ALL CRTTXAT_lemma2) THEN\r
 357      ASM_REWRITE_TAC[] THEN\r
 358      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 359      DISCH_TAC THEN\r
 360 \r
 361      SUBGOAL_THEN `!v w. (v:real^3,w:real^3) IN f ==> &2 <= norm v /\ norm v <= #2.52 /\ &2 <= norm w /\ norm w <= #2.52 /\ &2 <= dist (v,w) /\ dist (v,w) <= #2.52` ASSUME_TAC THENL\r
 362      [\r
 363        REPEAT GEN_TAC THEN DISCH_TAC THEN\r
 364          SUBGOAL_THEN `v,w IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL\r
 365          [\r
 366            MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 367              EXISTS_TAC `f:real^3#real^3->bool` THEN\r
 368              ASM_REWRITE_TAC[] THEN\r
 369              EXPAND_TAC "f" THEN\r
 370              MATCH_MP_TAC FACE_SUBSET_DART_OF_FAN THEN\r
 371              ASM_REWRITE_TAC[];    \r
 372            ALL_TAC\r
 373          ] THEN\r
 374          SUBGOAL_THEN `v:real^3 IN V /\ w IN V` ASSUME_TAC THENL\r
 375          [\r
 376            MATCH_MP_TAC PAIR_IN_DART_OF_FAN THEN\r
 377              EXISTS_TAC `ESTD V` THEN\r
 378              ASM_REWRITE_TAC[];\r
 379            ALL_TAC\r
 380          ] THEN\r
 381 \r
 382          MP_TAC (SPEC_ALL CONTRAVENING_DIST) THEN\r
 383          MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN\r
 384          MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_DART_DIST) THEN\r
 385          ASM_REWRITE_TAC[DIST_0; REAL_ARITH `&2 = #2.0`] THEN\r
 386          SIMP_TAC[];\r
 387        ALL_TAC\r
 388      ] THEN\r
 389 \r
 390      SUBGOAL_THEN `sum f (\x:real^3#real^3. arclength (#2.52) (norm (SND x)) (&2) + lmfun (h_dart x) * (arclength (&2) (norm (SND x)) (&2) - arclength (#2.52) (norm (SND x)) (&2))) <= &2 * pi` MP_TAC THENL\r
 391      [\r
 392        MATCH_MP_TAC REAL_LE_TRANS THEN\r
 393          EXISTS_TAC `sum f (\(v:real^3,w:real^3). arclength (norm v) (norm w) (&2))` THEN\r
 394          CONJ_TAC THENL\r
 395          [\r
 396            MATCH_MP_TAC SUM_LE THEN\r
 397              ASM_REWRITE_TAC[] THEN\r
 398              GEN_TAC THEN\r
 399              MP_TAC (ISPEC `x':real^3#real^3` PAIR_SURJECTIVE) THEN\r
 400              DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN\r
 401              DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN\r
 402              ASM_REWRITE_TAC[GSYM real_ge] THEN DISCH_TAC THEN\r
 403              REWRITE_TAC[h_dart] THEN\r
 404              MATCH_MP_TAC arc_lemma3 THEN\r
 405              FIRST_X_ASSUM (MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN\r
 406              ASM_SIMP_TAC[];\r
 407            ALL_TAC\r
 408          ] THEN\r
 409 \r
 410          MATCH_MP_TAC REAL_LE_TRANS THEN\r
 411          EXISTS_TAC `sum f (\(v:real^3,w:real^3). arclength (norm v) (norm w) (dist (v,w)))` THEN\r
 412          ASM_REWRITE_TAC[] THEN\r
 413          MATCH_MP_TAC SUM_LE THEN\r
 414          ASM_REWRITE_TAC[] THEN GEN_TAC THEN\r
 415          MP_TAC (ISPEC `x':real^3#real^3` PAIR_SURJECTIVE) THEN\r
 416          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 417          MATCH_MP_TAC arc_lemma1 THEN\r
 418          FIRST_X_ASSUM (MP_TAC o SPECL [`x'':real^3`; `y:real^3`]) THEN\r
 419          ASM_SIMP_TAC[];\r
 420        ALL_TAC\r
 421      ] THEN\r
 422 \r
 423      ASM_SIMP_TAC[SUM_ADD] THEN\r
 424      ABBREV_TAC `s1 = sum f (\x:real^3#real^3. arclength #2.52 #2.52 (&2) + lmfun (norm (SND x) / &2) * (arclength #2.52 (&2) (&2) - arclength #2.52 #2.52 (&2)))` THEN\r
 425      ABBREV_TAC `s2 = sum f (\x:real^3#real^3. arclength #2.52 (norm (SND x)) (&2))` THEN\r
 426      ABBREV_TAC `s3 = sum f (\x:real^3#real^3. lmfun (h_dart x) * (arclength (&2) (norm (SND x)) (&2) - arclength #2.52 (norm (SND x)) (&2)))` THEN\r
 427      DISCH_TAC THEN\r
 428 \r
 429      SUBGOAL_THEN `s1:real <= s2` ASSUME_TAC THENL\r
 430      [\r
 431        EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN\r
 432          MATCH_MP_TAC SUM_LE THEN\r
 433          ASM_REWRITE_TAC[] THEN GEN_TAC THEN\r
 434          MP_TAC (ISPEC `x':real^3#real^3` PAIR_SURJECTIVE) THEN\r
 435          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 436          REWRITE_TAC[GSYM real_ge] THEN\r
 437          MP_TAC (SPECL [`norm (y:real^3)`; `#2.52`] arc_lemma3) THEN\r
 438          REWRITE_TAC[arc_sym] THEN\r
 439          DISCH_THEN MATCH_MP_TAC THEN\r
 440          FIRST_X_ASSUM (MP_TAC o SPECL [`x'':real^3`; `y:real^3`]) THEN\r
 441          ASM_SIMP_TAC[] THEN\r
 442          REAL_ARITH_TAC;\r
 443        ALL_TAC\r
 444      ] THEN\r
 445 \r
 446      SUBGOAL_THEN `(&12 + &k - &(CARD (V:real^3->bool))) * #0.073 <= s3` ASSUME_TAC THENL\r
 447      [\r
 448        MATCH_MP_TAC REAL_LE_TRANS THEN\r
 449          EXISTS_TAC `sum f (\x:real^3#real^3. lmfun (h_dart x)) * #0.073` THEN\r
 450          CONJ_TAC THENL\r
 451          [\r
 452            MATCH_MP_TAC REAL_LE_RMUL THEN\r
 453              MP_TAC (SPEC_ALL CRTTXAT_lemma1) THEN\r
 454              ASM_SIMP_TAC[REAL_ARITH `&0 <= #0.073`; real_ge];\r
 455            ALL_TAC\r
 456          ] THEN\r
 457 \r
 458          EXPAND_TAC "s3" THEN\r
 459          MATCH_MP_TAC SUM_RMUL_BOUND THEN\r
 460          ASM_REWRITE_TAC[] THEN\r
 461          GEN_TAC THEN MP_TAC (ISPEC `x':real^3#real^3` PAIR_SURJECTIVE) THEN\r
 462          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 463          CONJ_TAC THENL\r
 464          [\r
 465            REWRITE_TAC[GSYM real_ge] THEN\r
 466              MATCH_MP_TAC arc_lemma4 THEN\r
 467              FIRST_X_ASSUM (MP_TAC o SPECL [`x'':real^3`; `y:real^3`]) THEN\r
 468              ASM_SIMP_TAC[];\r
 469            ALL_TAC\r
 470          ] THEN\r
 471 \r
 472          REWRITE_TAC[h_dart; Pack_defs.lmfun; Pack_defs.h0] THEN\r
 473          REAL_ARITH_TAC;\r
 474        ALL_TAC\r
 475      ] THEN\r
 476 \r
 477      SUBGOAL_THEN `(&k) * (arclength #2.52 #2.52 (&2)) + (&12 + &k - &(CARD (V:real^3->bool))) * #0.073 <= s1` ASSUME_TAC THENL\r
 478      [\r
 479        REPLICATE_TAC 5 REMOVE_ASSUM THEN\r
 480          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
 481          ASM_SIMP_TAC[SUM_ADD] THEN\r
 482          ASM_SIMP_TAC[SUM_CONST] THEN\r
 483          REWRITE_TAC[REAL_ARITH `a + b <= a + c <=> b <= c`] THEN\r
 484          REWRITE_TAC[SUM_RMUL] THEN\r
 485          MATCH_MP_TAC REAL_LE_TRANS THEN\r
 486          EXISTS_TAC `sum f (\x:real^3#real^3. lmfun (norm (SND x) / &2)) * #0.073` THEN\r
 487          CONJ_TAC THENL\r
 488          [\r
 489            MATCH_MP_TAC REAL_LE_RMUL THEN\r
 490              REWRITE_TAC[REAL_ARITH `&0 <= #0.073`; GSYM real_ge] THEN\r
 491              MP_TAC (SPEC_ALL CRTTXAT_lemma1') THEN\r
 492              ASM_SIMP_TAC[];\r
 493            ALL_TAC\r
 494          ] THEN\r
 495          MATCH_MP_TAC REAL_LE_LMUL THEN\r
 496          CONJ_TAC THENL\r
 497          [\r
 498            MATCH_MP_TAC SUM_POS_LE THEN\r
 499              ASM_REWRITE_TAC[Pack_defs.lmfun; Pack_defs.h0] THEN\r
 500              REAL_ARITH_TAC;\r
 501            ALL_TAC\r
 502          ] THEN\r
 503 \r
 504          REWRITE_TAC[GSYM real_ge] THEN\r
 505          MP_TAC (SPEC `#2.52` arc_lemma4) THEN\r
 506          REWRITE_TAC[arc_sym] THEN\r
 507          REAL_ARITH_TAC;\r
 508        ALL_TAC\r
 509      ] THEN\r
 510 \r
 511      SUBGOAL_THEN `&k * arclength #2.52 #2.52 (&2) + (&2) * (&12 + &k - &(CARD (V:real^3->bool))) * #0.073 <= &2 * pi` MP_TAC THENL\r
 512      [\r
 513        MATCH_MP_TAC REAL_LE_TRANS THEN\r
 514          EXISTS_TAC `(s1:real) + s3` THEN\r
 515          CONJ_TAC THENL\r
 516          [\r
 517            REWRITE_TAC[REAL_ARITH `c + &2 * a * b = (c + a * b) + a * b`] THEN\r
 518              MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 519              ASM_REWRITE_TAC[];\r
 520            ALL_TAC\r
 521          ] THEN\r
 522          MATCH_MP_TAC REAL_LE_TRANS THEN\r
 523          EXISTS_TAC `(s2:real) + s3` THEN\r
 524          ASM_REWRITE_TAC[] THEN\r
 525          MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 526          ASM_REWRITE_TAC[REAL_LE_REFL];\r
 527        ALL_TAC\r
 528      ] THEN\r
 529 \r
 530      DISCH_TAC THEN\r
 531      SUBGOAL_THEN `&k * (arclength #2.52 #2.52 (&2) + #0.146) <= &2 * pi + (&(CARD (V:real^3->bool)) - &12) * #0.146` ASSUME_TAC THENL\r
 532      [\r
 533        POP_ASSUM MP_TAC THEN\r
 534          REAL_ARITH_TAC;\r
 535        ALL_TAC\r
 536      ] THEN\r
 537 \r
 538      SUBGOAL_THEN `&k * (#0.816 + #0.146) <= &2 * #3.1416 + &3 * #0.146` ASSUME_TAC THENL\r
 539      [\r
 540        MATCH_MP_TAC REAL_LE_TRANS THEN\r
 541          EXISTS_TAC `&k * (arclength #2.52 #2.52 (&2) + #0.146)` THEN\r
 542          CONJ_TAC THENL\r
 543          [\r
 544            MATCH_MP_TAC REAL_LE_LMUL THEN\r
 545              REWRITE_TAC[REAL_ARITH `&0 <= &k`; REAL_ARITH `a + b <= c + b <=> a <= c`] THEN\r
 546              ASM_REWRITE_TAC[GSYM real_ge; arc_lemma5];\r
 547            ALL_TAC\r
 548          ] THEN\r
 549          MATCH_MP_TAC REAL_LE_TRANS THEN\r
 550          EXISTS_TAC `&2 * pi + (&(CARD (V:real^3->bool)) - &12) * #0.146` THEN\r
 551          CONJ_TAC THEN ASM_REWRITE_TAC[] THEN\r
 552          MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 553          CONJ_TAC THENL\r
 554          [\r
 555            MP_TAC PI_APPROX_32 THEN\r
 556              REAL_ARITH_TAC;\r
 557            ALL_TAC\r
 558          ] THEN\r
 559          MATCH_MP_TAC REAL_LE_RMUL THEN\r
 560          REWRITE_TAC[REAL_ARITH `&0 <= #0.146`; REAL_ARITH `a - &12 <= &3 <=> a <= &15`] THEN\r
 561          REWRITE_TAC[REAL_OF_NUM_LE] THEN\r
 562          FIRST_X_ASSUM (MP_TAC o check (fun th -> rator (concl th) = `contravening`)) THEN\r
 563          REWRITE_TAC[contravening] THEN\r
 564          SIMP_TAC[ARITH_RULE `a = 13 \/ a = 14 \/ a = 15 ==> a <= 15`];\r
 565        ALL_TAC\r
 566      ] THEN\r
 567 \r
 568      SUBGOAL_THEN `&k <= #6.99` MP_TAC THENL\r
 569      [\r
 570        POP_ASSUM MP_TAC THEN\r
 571          REAL_ARITH_TAC;\r
 572        ALL_TAC\r
 573      ] THEN\r
 574 \r
 575      DISJ_CASES_TAC (ARITH_RULE `k <= 6 \/ 7 <= k`) THEN ASM_REWRITE_TAC[] THEN\r
 576      POP_ASSUM MP_TAC THEN\r
 577      REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN\r
 578      REAL_ARITH_TAC);;\r
 579      \r
 580      \r
 581      \r
 582 \r
 583 \r
 584 end;;\r