text_formalization/local/PPBTYDQ.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Ppbtydq = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Fektyiy;;
  89
  90
  91
  92 let PPBTYDQ_concl = `!(u:real^3) v p. ~collinear {vec 0,v,p} /\ ~collinear {vec 0,u,p} /\
  93   arcV (vec 0) u p + arcV (vec 0) p v < pi ==> ~(vec 0 IN conv{u,v})`;;
  94
  95
  96
  97 let PPBTYDQ= prove_by_refinement((PPBTYDQ_concl),
  98 [REPEAT STRIP_TAC
  99 THEN POP_ASSUM MP_TAC
 100 THEN POP_ASSUM MP_TAC
 101 THEN ABBREV_TAC `e= u cross (p:real^3)`
 102 THEN SUBGOAL_THEN`orthogonal e (u:real^3)`ASSUME_TAC;
 103
 104 EXPAND_TAC "e"
 105 THEN REWRITE_TAC[orthogonal;DOT_CROSS_SELF];
 106
 107
 108 SUBGOAL_THEN`orthogonal e (p:real^3)`ASSUME_TAC;
 109
 110 EXPAND_TAC "e"
 111 THEN REWRITE_TAC[orthogonal;DOT_CROSS_SELF];
 112
 113
 114 REWRITE_TAC[Collect_geom.CONV_SET2;IN_ELIM_THM;VECTOR_ARITH`vec 0 = a % u + b % v<=> b % v = (--a) % u `]
 115 THEN REPEAT STRIP_TAC
 116 THEN POP_ASSUM MP_TAC
 117 THEN POP_ASSUM MP_TAC
 118 THEN MP_TAC(REAL_ARITH`&0<=b==> b= &0\/ &0< b`)
 119 THEN RESA_TAC;
 120
 121
 122 REWRITE_TAC[VECTOR_ARITH`&0 % v = --a % u<=> a % u= vec 0`;VECTOR_MUL_EQ_0;REAL_ARITH`a + &0= &1<=> a= &1`]
 123 THEN RESA_TAC
 124 THEN ASM_REWRITE_TAC[REAL_ARITH`~(&1= &0)`]
 125 THEN MRESA_TAC th3[`vec 0:real^3`;`u`;`p`];
 126
 127
 128 MP_TAC(REAL_ARITH`&0<=a==> a= &0\/ &0< a`)
 129 THEN RESA_TAC;
 130
 131
 132 REWRITE_TAC[VECTOR_ARITH`b % v = -- &0 % u<=> b % v= vec 0`;VECTOR_MUL_EQ_0;REAL_ARITH` &0+a= &1<=> a= &1`]
 133 THEN RESA_TAC
 134 THEN ASM_REWRITE_TAC[REAL_ARITH`~(&1= &0)`]
 135 THEN MRESA_TAC th3[`vec 0:real^3`;`v`;`p`];
 136
 137 REPEAT STRIP_TAC
 138 THEN MP_TAC(SET_RULE`b % v = --a % u
 139 ==> (inv b) %b % v = (inv b) % --a % u:real^3`)
 140 THEN REWRITE_TAC[VECTOR_ARITH`a%b%c=(a*b)%c`]
 141 THEN ASM_REWRITE_TAC[]
 142 THEN MP_TAC(ARITH_RULE`&0< b==> ~(b= &0)`)
 143 THEN RESA_TAC
 144 THEN ASM_SIMP_TAC[REAL_MUL_LINV;VECTOR_ARITH`&1 %v= v`]
 145 THEN SUBGOAL_THEN`(inv b * --a)< &0` ASSUME_TAC;
 146
 147 MATCH_MP_TAC(REAL_ARITH`&0<(inv b *a)==> (inv b * --a)< &0`)
 148 THEN MATCH_MP_TAC REAL_LT_MUL
 149 THEN ASM_REWRITE_TAC[]
 150 THEN MATCH_MP_TAC REAL_LT_INV
 151 THEN ASM_REWRITE_TAC[];
 152
 153 ABBREV_TAC `v'=(inv b * --a)`
 154 THEN STRIP_TAC
 155 THEN DICH_TAC (15-5)
 156 THEN ASM_REWRITE_TAC[]
 157 THEN MRESA_TAC th3[`vec 0:real^3`;`u`;`p`];
 158
 159
 160
 161
 162 MRESA_TAC Local_lemmas1.ARCV_PI_OPPOSITE[`v'`;`u`;`vec 0:real^3`]
 163 THEN POP_ASSUM MP_TAC
 164 THEN REDUCE_VECTOR_TAC
 165 THEN STRIP_TAC
 166 THEN SYM_ASSUM_TAC
 167 THEN REWRITE_TAC[REAL_ARITH`~(a<b)<=> b<=a`]
 168 THEN MATCH_MP_TAC Trigonometry.KEITDWB
 169 THEN MRESAL_TAC th3[`vec 0:real^3`;`v`;`p`][VECTOR_ARITH`&0 % a= vec 0`]]);;
 170
 171
 172 let OIQKKEP_concl = `!u v c.
 173   u IN ball_annulus /\ v IN ball_annulus /\ c < &4 /\ dist(u,v) <= c /\ &2<= dist(u,v)==>
 174   arcV (vec 0) u v <= arclength (&2) (&2) c`;;
 175
 176
 177 let OIQKKEP = prove_by_refinement(
 178  OIQKKEP_concl,
 179 [
 180 REWRITE_TAC[Ckqowsa_3_points.in_ball_annulus;dist]
 181 THEN REPEAT STRIP_TAC
 182 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`u`;`v`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
 183 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
 184 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
 185 THEN MRESAL_TAC NORM_TRIANGLE[`u:real^3`;`-- v:real^3`][VECTOR_ARITH`a+ --b=a-b:real^3`;NORM_NEG]
 186 THEN MRESAL_TAC NORM_TRIANGLE[`v:real^3`;`u- v:real^3`][VECTOR_ARITH`a+ b-a=b:real^3`;NORM_NEG]
 187 THEN MRESAL_TAC NORM_TRIANGLE[`u-v:real^3`;`-- u:real^3`][VECTOR_ARITH`a- b+ --a= --b:real^3`;NORM_NEG]
 188 THEN MRESAL_TAC Trigonometry1.ACS_ARCLENGTH[`norm (u)`;`norm v`;`norm(u-v)`]
 189 [NORM_POS_LE]
 190 THEN MP_TAC(REAL_ARITH`norm (u - v:real^3) <= c /\ c< &4 /\ &0<= norm (u - v)
 191 ==> &0 <= c /\ c <= &2 + &2 /\ &2 <= &2 + c /\ &2 <= c + &2 /\ c<= &4`)
 192 THEN ASM_REWRITE_TAC[NORM_POS_LE]
 193 THEN RESA_TAC
 194 THEN MRESAL_TAC Trigonometry1.ACS_ARCLENGTH[`&2`;`&2`;`c:real`]
 195 [NORM_POS_LE;REAL_ARITH`&0< &2`]
 196 THEN MATCH_MP_TAC ACS_MONO_LE
 197 THEN STRIP_TAC;
 198
 199
 200 REWRITE_TAC[REAL_ARITH`-- &1 <= (&2 * &2 + &2 * &2 - c * c) / (&2 * &2 * &2)
 201 <=> c*c<= &4* &4`]
 202 THEN MATCH_MP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE
 203 THEN MRESA_TAC REAL_ABS_REFL[`c`];
 204
 205 STRIP_TAC;
 206
 207 MRESAL_TAC Imjxphr.xrr_increasing_le[`&2`;`&2`;`norm(u-v)`;`c`][NORM_POS_LE;REAL_ARITH`&0< &2`]
 208 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`norm u`;`&2`;`norm(u-v)`]
 209 [NORM_POS_LE;REAL_ARITH`&2<= &2/\ &2 <= &2 * #1.26`;h0]
 210 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`norm v`;`norm u`;`norm(u-v)`]
 211 [NORM_POS_LE;REAL_ARITH`&2<= &2/\ &2 <= &2 * #1.26`;h0;]
 212 THEN POP_ASSUM MP_TAC
 213 THEN ONCE_REWRITE_TAC[Ocbicby.xrr_sym]
 214 THEN STRIP_TAC
 215 THEN MP_TAC(REAL_ARITH`xrr (&2) (&2) (norm (u - v)) <= xrr (&2) (&2) c
 216 /\ xrr (norm u) (&2) (norm (u - v)) <= xrr (&2) (&2) (norm (u - v))
 217 /\ xrr (norm u) (norm v) (norm (u - v)) <= xrr (norm u) (&2) (norm (u - v:real^3))
 218 ==> xrr (norm u) (norm v) (norm (u - v))<= xrr (&2) (&2) c`)
 219 THEN RESA_TAC
 220 THEN POP_ASSUM MP_TAC
 221 THEN REWRITE_TAC[xrr]
 222 THEN REAL_ARITH_TAC;
 223
 224 MRESAL_TAC Trigonometry1.TRI_SQUARES_BOUNDS[`norm u`;`norm v`;`norm(u-v)`]
 225 [NORM_POS_LE]]);;
 226
 227
 228
 229
 230
 231 let MXQTIED_concl = `!s s' v.
 232   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 233   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 234  scs_d_v39 s'= scs_d_v39 s /\
 235   v IN MMs_v39 s /\ v IN BBs_v39 s' /\
 236   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
 237 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
 238     v IN MMs_v39 s'`;;
 239
 240
 241 let MXQTIED_PRIME2_concl = `
 242   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 243   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 244  scs_d_v39 s'= scs_d_v39 s /\
 245   v IN MMs_v39 s /\ v IN BBs_v39 s' /\
 246   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
 247 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
 248     BBprime2_v39 s' v`;;
 249
 250
 251
 252 let MXQTIED_PRIME_concl = `
 253   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 254   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 255  scs_d_v39 s'= scs_d_v39 s /\
 256   v IN BBprime_v39 s /\ v IN BBs_v39 s' /\
 257   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
 258 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
 259     BBprime_v39 s' v`;;
 260
 261
 262
 263
 264
 265 let MXQTIED_TAU_concl = `
 266   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 267   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 268  scs_d_v39 s'= scs_d_v39 s /\
 269   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) ==>
 270     taustar_v39 s' v= taustar_v39 s v`;;
 271
 272
 273 let MXQTIED_TAU_DSV_concl = `
 274   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 275   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 276  scs_d_v39 s'= scs_d_v39 s /\
 277   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
 278 ==>
 279     dsv_v39 s' v= dsv_v39 s v`;;
 280
 281
 282 let MXQTIED_BB_concl = `!s s' v.
 283   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 284   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 285  scs_d_v39 s'= scs_d_v39 s /\
 286    v IN BBs_v39 s' /\
 287   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
 288 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
 289      BBs_v39 s v`;;
 290
 291
 292
 293
 294
 295
 296
 297 let MXQTIED_INDEX_concl = `
 298   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 299   scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 300  scs_d_v39 s'= scs_d_v39 s /\
 301    v IN BBs_v39 s' /\
 302   (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
 303 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
 304      BBindex_v39 s' v= BBindex_v39 s v`;;
 305
 306
 307
 308 let MXQTIED_INDEX=prove( MXQTIED_INDEX_concl,
 309 REWRITE_TAC[IN;BBindex_v39]
 310 THEN REPEAT RESA_TAC);;
 311
 312
 313
 314
 315
 316
 317 let  MXQTIED_BB=prove_by_refinement( MXQTIED_BB_concl,
 318 [REWRITE_TAC[IN;scs_basic]
 319 THEN REPEAT STRIP_TAC
 320 THEN DICH_TAC 2
 321 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;dsv_v39;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
 322 THEN REPEAT RESA_TAC;
 323
 324 THAYTHE_TAC 1[`i`;`j:num`]
 325 THEN THAYTHE_TAC (15-10)[`i`;`j`]
 326 THEN DICH_TAC 1
 327 THEN DICH_TAC 2
 328 THEN REAL_ARITH_TAC;
 329
 330 THAYTHE_TAC 1[`i`;`j:num`]
 331 THEN THAYTHE_TAC (15-10)[`i`;`j`]
 332 THEN DICH_TAC 0
 333 THEN DICH_TAC 1
 334 THEN REAL_ARITH_TAC;
 335
 336 THAYTHE_TAC 1[`i`;`j:num`]
 337 THEN THAYTHE_TAC (15-10)[`i`;`j`]
 338 THEN DICH_TAC 1
 339 THEN DICH_TAC 2
 340 THEN REAL_ARITH_TAC;
 341
 342 THAYTHE_TAC 1[`i`;`j:num`]
 343 THEN THAYTHE_TAC (15-10)[`i`;`j`]
 344 THEN DICH_TAC 0
 345 THEN DICH_TAC 1
 346 THEN REAL_ARITH_TAC]);;
 347
 348
 349
 350 let MXQTIED_TAU_DSV =prove(MXQTIED_TAU_DSV_concl,
 351 REWRITE_TAC[IN;scs_basic]
 352 THEN REPEAT STRIP_TAC
 353 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;dsv_v39;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
 354 THEN REPEAT STRIP_TAC);;
 355
 356
 357
 358 let MXQTIED_TAU =prove(MXQTIED_TAU_concl,
 359 REWRITE_TAC[IN;scs_basic]
 360 THEN REPEAT STRIP_TAC
 361 THEN MP_TAC MXQTIED_TAU_DSV
 362 THEN REWRITE_TAC[IN;scs_basic]
 363 THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;]
 364 THEN REPEAT STRIP_TAC);;
 365
 366
 367
 368
 369 let MXQTIED_PRIME=prove_by_refinement(
 370  MXQTIED_PRIME_concl,
 371 [
 372 REWRITE_TAC[IN;scs_basic]
 373 THEN REPEAT STRIP_TAC
 374 THEN MP_TAC MXQTIED_TAU_DSV
 375 THEN REWRITE_TAC[IN;scs_basic]
 376 THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
 377 THEN REPEAT STRIP_TAC;
 378
 379 MP_TAC MXQTIED_TAU
 380 THEN REWRITE_TAC[IN;scs_basic]
 381 THEN RESA_TAC
 382 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww`][IN;scs_basic]
 383 THEN DICH_TAC (16-9)
 384 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
 385 THEN REPEAT RESA_TAC
 386 THEN MATCH_DICH_TAC (18-17)
 387 THEN ASM_REWRITE_TAC[]
 388 THEN MATCH_MP_TAC MXQTIED_BB
 389 THEN ASM_REWRITE_TAC[IN;scs_basic]
 390 THEN EXISTS_TAC`s':scs_v39`
 391 THEN ASM_REWRITE_TAC[];
 392
 393 MP_TAC MXQTIED_TAU
 394 THEN REWRITE_TAC[IN;scs_basic]
 395 THEN RESA_TAC
 396 THEN DICH_TAC (14-9)
 397 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
 398 THEN REPEAT RESA_TAC]);;
 399
 400
 401
 402 let BBPRIME_IMP_BB=prove(`BBprime_v39 s' w ==> BBs_v39 s' w`,
 403 ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime_v39;]
 404 THEN RESA_TAC);;
 405
 406
 407
 408 let MXQTIED_PRIME2=prove_by_refinement( MXQTIED_PRIME2_concl,
 409 [
 410 REWRITE_TAC[IN;scs_basic]
 411 THEN REPEAT STRIP_TAC
 412 THEN MRESA_TAC(GEN_ALL Nuxcoea.MMS_IMP_BBPRIME)[`s`;`v`]
 413 THEN MP_TAC MXQTIED_PRIME
 414 THEN REWRITE_TAC[IN;scs_basic]
 415 THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;]
 416 THEN REPEAT STRIP_TAC
 417 THEN MP_TAC MXQTIED_INDEX
 418 THEN REWRITE_TAC[IN;scs_basic]
 419 THEN RESA_TAC
 420 THEN MP_TAC(SET_RULE`(?w. BBprime_v39 (s':scs_v39) w /\ BBindex_v39 s w< BBindex_v39 s v) \/ ~(?w.  BBprime_v39 s' w /\ BBindex_v39 s w< BBindex_v39 s v)`)
 421 THEN RESA_TAC;
 422
 423 MP_TAC BBPRIME_IMP_BB
 424 THEN RESA_TAC
 425 THEN MRESAL_TAC MXQTIED_BB[`s`;`s'`;`w`][scs_basic;IN]
 426 THEN DICH_TAC (19-9)
 427 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;]
 428 THEN RESA_TAC
 429 THEN DICH_TAC(24-19)
 430 THEN REWRITE_TAC[BBindex_min_v39]
 431 THEN SUBGOAL_THEN`BBprime_v39 s (w:num->real^3)`ASSUME_TAC;
 432
 433 ASM_TAC
 434 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime_v39;]
 435 THEN REPEAT RESA_TAC
 436 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`w`][scs_basic;IN]
 437 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww:num->real^3`][scs_basic;IN]
 438 THEN SYM_ASSUM_TAC
 439 THEN SYM_ASSUM_TAC
 440 THEN DICH_TAC (28-19)
 441 THEN STRIP_TAC;
 442
 443 THAYTHE_TAC 0[`v`]
 444 THEN THAYTHE_TAC (28-13)[`ww`]
 445 THEN POP_ASSUM MP_TAC
 446 THEN POP_ASSUM MP_TAC
 447 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`v`][scs_basic;IN]
 448 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww`][scs_basic;IN]
 449 THEN REAL_ARITH_TAC;
 450
 451 MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`w`][scs_basic;IN];
 452
 453 SUBGOAL_THEN`BBindex_v39 s w IN IMAGE (BBindex_v39 s) (BBprime_v39 s)`ASSUME_TAC;
 454
 455 REWRITE_TAC[IMAGE;IN_ELIM_THM]
 456 THEN REWRITE_TAC[IN]
 457 THEN EXISTS_TAC`w:num->real^3`
 458 THEN ASM_REWRITE_TAC[];
 459
 460 MRESA_TAC Nuxcoea.MIN_LEAST[`(IMAGE (BBindex_v39 s) (BBprime_v39 s))`;`BBindex_v39 s w`]
 461 THEN STRIP_TAC
 462 THEN DICH_TAC(28-16)
 463 THEN DICH_TAC 1
 464 THEN ASM_REWRITE_TAC[]
 465 THEN ARITH_TAC;
 466
 467
 468 POP_ASSUM MP_TAC
 469 THEN REWRITE_TAC[NOT_EXISTS_THM;BBindex_min_v39]
 470 THEN STRIP_TAC
 471 THEN SUBGOAL_THEN`BBindex_v39 s v IN IMAGE (BBindex_v39 s') (BBprime_v39 s')`ASSUME_TAC;
 472
 473 REWRITE_TAC[IN_ELIM_THM;IMAGE]
 474 THEN REWRITE_TAC[IN]
 475 THEN EXISTS_TAC`v:num->real^3`
 476 THEN ASM_REWRITE_TAC[];
 477
 478 MRESA_TAC Nuxcoea.MIN_LEAST[`(IMAGE (BBindex_v39 s') (BBprime_v39 s'))`;`BBindex_v39 s v`]
 479 THEN MP_TAC(ARITH_RULE`min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) <= BBindex_v39 s v
 480 ==> min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) < BBindex_v39 s v
 481 \/ min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) = BBindex_v39 s v`)
 482 THEN RESA_TAC;
 483
 484 DICH_TAC 2
 485 THEN REWRITE_TAC[GSYM BBindex_min_v39]
 486 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
 487 THEN REWRITE_TAC[IN]
 488 THEN RESA_TAC
 489 THEN THAYTHE_TAC(21-16)[`x`]
 490 THEN POP_ASSUM MP_TAC
 491 THEN DICH_TAC 2
 492 THEN ASM_REWRITE_TAC[GSYM BBindex_min_v39]
 493 THEN ASM_REWRITE_TAC[]
 494 THEN MRESA_TAC BBPRIME_IMP_BB[`s'`;`x`]
 495 THEN MRESAL_TAC MXQTIED_INDEX[`s'`;`s`;`x`][IN;scs_basic]
 496 THEN RESA_TAC]);;
 497
 498
 499
 500
 501
 502 let MXQTIED=prove(MXQTIED_concl,
 503 REWRITE_TAC[IN;scs_basic;]
 504 THEN REPEAT STRIP_TAC
 505 THEN MP_TAC MXQTIED_PRIME2
 506 THEN REWRITE_TAC[IN;scs_basic;]
 507 THEN RESA_TAC
 508 THEN MRESA_TAC Ayqjtmd.unadorned_MMs[`s'`]);;
 509
 510
 511
 512
 513
 514
 515
 516 let SCS_BASIC_DSV=prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 517   scs_k_v39 s = scs_k_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' ==>
 518 dsv_v39 s v <= dsv_v39  s' v`,
 519 REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF;IN;dsv_v39;scs_basic;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
 520 THEN RESA_TAC
 521 THEN ASM_REWRITE_TAC[SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0/\ a+ &0=a`]);;
 522
 523
 524
 525
 526
 527
 528
 529 let SCS_BASIC_TAUSTAR=prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 530   scs_k_v39 s = scs_k_v39 s'
 531 /\ scs_d_v39 s<= scs_d_v39 s'
 532 ==> taustar_v39 s' v <= taustar_v39  s v`,
 533 STRIP_TAC
 534 THEN MP_TAC SCS_BASIC_DSV
 535 THEN RESA_TAC
 536 THEN POP_ASSUM MP_TAC
 537 THEN REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF]
 538 THEN MP_TAC(SET_RULE`scs_k_v39 s' <= 3 \/ ~(scs_k_v39 s' <= 3)`)
 539 THEN RESA_TAC
 540 THEN REAL_ARITH_TAC);;
 541
 542
 543 let TAUSTAR_LE_0_XWNHLMD=prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 544   scs_k_v39 s = scs_k_v39 s' /\
 545   v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s<= scs_d_v39 s'
 546   ==> taustar_v39 s' v< &0`,
 547 REWRITE_TAC[IN;LET_DEF;LET_END_DEF;MMs_v39;BBprime2_v39;BBprime_v39]
 548 THEN STRIP_TAC
 549 THEN MP_TAC SCS_BASIC_TAUSTAR
 550 THEN RESA_TAC
 551 THEN POP_ASSUM MP_TAC
 552 THEN DICH_TAC(15-7)
 553 THEN REAL_ARITH_TAC);;
 554
 555
 556
 557
 558
 559
 560 let XWNHLMD_MM=prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 561   scs_k_v39 s = scs_k_v39 s' /\
 562   v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s<= scs_d_v39 s'
 563 ==> ~(MMs_v39 s' ={})`,
 564 STRIP_TAC
 565 THEN MP_TAC TAUSTAR_LE_0_XWNHLMD
 566 THEN RESA_TAC
 567 THEN MATCH_MP_TAC SGTRNAF
 568 THEN EXISTS_TAC`v:num->real^3`
 569 THEN ASM_REWRITE_TAC[]
 570 THEN ASM_TAC
 571 THEN REWRITE_TAC[scs_basic]
 572 THEN REPEAT RESA_TAC);;
 573
 574 let XWNHLMD_concl = `!s s' v.
 575   is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 576   scs_k_v39 s = scs_k_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' /\
 577   v IN MMs_v39 s /\ v IN BBs_v39 s' ==>
 578   scs_arrow_v39 {s} {s'}`;;
 579
 580
 581
 582
 583 let XWNHLMD=prove_by_refinement(XWNHLMD_concl,
 584 [REPEAT GEN_TAC
 585 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
 586 THEN ABBREV_TAC`k=scs_k_v39 s`
 587 THEN REPEAT RESA_TAC;
 588
 589 DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);
 590
 591 ASM_REWRITE_TAC[];
 592
 593 ASM_REWRITE_TAC[]
 594 THEN POP_ASSUM MP_TAC
 595 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 596 THEN REPEAT STRIP_TAC
 597 THEN POP_ASSUM MP_TAC
 598 THEN RESA_TAC
 599 THEN EXISTS_TAC`s':scs_v39`
 600 THEN ASM_REWRITE_TAC[]
 601 THEN MATCH_MP_TAC XWNHLMD_MM
 602 THEN ASM_REWRITE_TAC[IN]]);;
 603
 604  end;;
 605
 606
 607 (*
 608 let check_completeness_claimA_concl =
 609   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 610 *)
 611
 612
 613
 614