text_formalization/local/CQAOQLR.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 Cqaoqlr = 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 Aursipd;;
  89 open Cuxvzoz;;
  90 open Rrcwnsj;;
  91 open Tfitskc;;
  92
  93
  94
  95 let K_SUC_2_MOD_SUB=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 1) MOD k= (k- SUC((i+1) MOD k)) MOD k`,
  96 SIMP_TAC[GSYM ADD1;]
  97 THEN STRIP_TAC
  98 THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)`]);;
  99
 100 let K_SUC_2_MOD_SUB_ID=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 2) MOD k= (k- SUC((i) MOD k)) MOD k`,
 101 SIMP_TAC[GSYM ADD1;]
 102 THEN STRIP_TAC
 103 THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)`
 104 ]
 105 THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`SUC i`;`k`]
 106 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i) MOD k`;`k`]
 107 THEN SYM_ASSUM_TAC
 108 THEN SYM_ASSUM_TAC
 109 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i MOD k)`;`k`]
 110 THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (SUC i MOD k))=k - SUC i MOD k`]
 111 );;
 112
 113 let A_B_J_SCS_OPP=prove(`scs_a_v39 (scs_opp_v39 s) i j = scs_a_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))
 114 /\ scs_b_v39 (scs_opp_v39 s) i j = scs_b_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))
 115 /\ scs_J_v39 (scs_opp_v39 s) i j = scs_J_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))`,
 116 REWRITE_TAC[scs_opp_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;peropp2]);;
 117
 118 let SUC_OPP_ID=prove(`1<k ==> SUC (k - SUC i MOD k) MOD k= (k- i MOD k) MOD k`,
 119 STRIP_TAC
 120 THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`(i)`;`k`]
 121 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (i) MOD k`;`k`]
 122 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC ( i) MOD k)`;`k`]
 123 THEN SYM_ASSUM_TAC
 124 THEN SYM_ASSUM_TAC
 125 THEN SYM_ASSUM_TAC
 126 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (i MOD k)`;`k`]
 127 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (i MOD k))`;`k`]
 128 THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (i MOD k))=k - i MOD k`]);;
 129
 130
 131
 132
 133 let K_SUC_2_MOD_F_SUB_ID=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 3) MOD k= (k- SUC((i+k-1) MOD k)) MOD k`,
 134 SIMP_TAC[GSYM ADD1;]
 135 THEN STRIP_TAC
 136 THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)/\ i+3=SUC(i+2)`
 137 ]
 138 THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`(SUC i)`;`k`]
 139 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i) MOD k`;`k`]
 140 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (SUC i) MOD k)`;`k`]
 141 THEN SYM_ASSUM_TAC
 142 THEN SYM_ASSUM_TAC
 143 THEN SYM_ASSUM_TAC
 144 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i MOD k)`;`k`]
 145 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (SUC i MOD k))`;`k`]
 146 THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (SUC i MOD k))=k - SUC i MOD k/\ SUC (i + k - 1)= 1*k+i`;SUC_OPP_ID;MOD_MULT_ADD]);;
 147
 148 let ELEMENT1_SYM_0=prove(`{--a}= IMAGE (\x:real^N. --x) {a}`,
 149 REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;IN_SING;SET_RULE`a IN{b,c} <=> a=b\/ a=c`]
 150 THEN GEN_TAC
 151 THEN EQ_TAC
 152 THEN REPEAT RESA_TAC
 153 THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
 154 THEN SET_TAC[]);;
 155
 156 let SCS_GENERIC_SYM_0=prove(`BBs_v39 s v/\ is_scs_v39 s/\ scs_generic v
 157 ==> scs_generic (\i. --v (scs_k_v39 s - SUC (i MOD scs_k_v39 s)))`,
 158 REWRITE_TAC[scs_generic;BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
 159 THEN REPEAT RESA_TAC
 160 THEN ABBREV_TAC`k= scs_k_v39 s`
 161 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
 162 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
 163 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
 164 THEN RESA_TAC
 165 THEN ASM_SIMP_TAC[OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_E_EQ_NEG;]
 166 THEN ASM_TAC
 167 THEN REWRITE_TAC[generic]
 168 THEN REPEAT RESA_TAC
 169 THEN MRESAL_TAC IN_SYM_0[`u`;`IMAGE (\i. --(v:num->real^3) i) (:num)`][IMAGE_V_SYM_0;REFL_SYM_0]
 170 THEN MRESAL_TAC IMAGE_E_SYM_0[`{v',w}`;`v:num->real^3`][GSYM ELEMENT2_SYM_0]
 171 THEN THAYTHES_TAC (33-24)[`-- v':real^3`;`-- w:real^3`;`-- u:real^3`][ ELEMENT2_SYM_0;AFF_GE_VEC0_SYM_0;AFF_LT_VEC0_SYM_0;ELEMENT1_SYM_0;GSYM INTER_SYM_0]
 172 THEN POP_ASSUM MP_TAC
 173 THEN MRESAL_TAC SET_EQ_SYM_0[`IMAGE (\x:real^3. --x) (aff_ge {vec 0:real^3} {v', w} INTER aff_lt {vec 0} {u})`;`{}:real^3->bool`][REFL_SYM_0;IMAGE_CLAUSES]);;
 174
 175 let UNADORNED_OPP=prove(`is_scs_v39 s /\ unadorned_v39 s
 176 ==> unadorned_v39 (scs_opp_v39 s)`,
 177 REWRITE_TAC[LET_DEF;LET_END_DEF;unadorned_v39;scs_opp_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;peropp;EXTENSION;IN]
 178 THEN RESA_TAC
 179 THEN SET_TAC[]);;
 180
 181 let BASIC_OPP=prove(`is_scs_v39 s /\ scs_basic_v39 s
 182 ==> scs_basic_v39 (scs_opp_v39 s)`,
 183 SIMP_TAC[scs_basic;UNADORNED_OPP;A_B_J_SCS_OPP]);;
 184
 185
 186 let DIAG_OPP=prove_by_refinement(`3<k /\ scs_diag k i j ==> scs_diag k (k - SUC (i MOD k)) (k - SUC (j MOD k))`,
 187 [REWRITE_TAC[scs_diag]
 188 THEN REPEAT RESA_TAC;
 189
 190 DICH_TAC 3
 191 THEN REWRITE_TAC[]
 192 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
 193 THEN RESA_TAC
 194 THEN MRESA_TAC OPP_SUC_MOD[`i`;`k`]
 195 THEN MRESA_TAC OPP_SUC_MOD[`j`;`k`];
 196
 197 DICH_TAC 1
 198 THEN REWRITE_TAC[]
 199 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ SUC (k - SUC (i MOD k))= k- i MOD k/\ SUC (k - SUC (SUC (k - SUC i MOD k) MOD k))
 200 =(k - (SUC (k - SUC i MOD k) MOD k))`)
 201 THEN RESA_TAC
 202 THEN MRESA_TAC OPP_SUC_MOD[`j`;`k`]
 203 THEN POP_ASSUM MP_TAC
 204 THEN DICH_TAC 4
 205 THEN RESA_TAC
 206 THEN SYM_ASSUM_TAC
 207 THEN MRESA_TAC SUC_OPP_ID[`i`;`k`]
 208 THEN SYM_ASSUM_TAC
 209 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`k - SUC (SUC (k - SUC i MOD k) MOD k)`;`j`;`k`][MOD_REFL;]
 210 THEN STRIP_TAC
 211 THEN DICH_TAC 1
 212 THEN ASM_SIMP_TAC[MOD_REFL;GSYM SUC_MOD_EQ_MOD_SUC;OPP_SUC_MOD];
 213
 214 DICH_TAC 2
 215 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 216 THEN REWRITE_TAC[]
 217 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ SUC (k - SUC (j MOD k))= k- j MOD k/\ SUC (k - SUC (SUC (k - SUC j MOD k) MOD k))
 218 =(k - (SUC (k - SUC j MOD k) MOD k))`)
 219 THEN RESA_TAC
 220 THEN MRESA_TAC OPP_SUC_MOD[`i`;`k`]
 221 THEN POP_ASSUM MP_TAC
 222 THEN DICH_TAC 4
 223 THEN RESA_TAC
 224 THEN SYM_ASSUM_TAC
 225 THEN MRESA_TAC SUC_OPP_ID[`j`;`k`]
 226 THEN SYM_ASSUM_TAC
 227 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`k - SUC (SUC (k - SUC j MOD k) MOD k)`;`i`;`k`][MOD_REFL;]
 228 THEN STRIP_TAC
 229 THEN DICH_TAC 1
 230 THEN ASM_SIMP_TAC[MOD_REFL;GSYM SUC_MOD_EQ_MOD_SUC;OPP_SUC_MOD]]);;
 231
 232
 233 let CQAOQLR_concl =
 234 `main_nonlinear_terminal_v11
 235 ==> (!s (v:num->real^3) i.
 236   3< scs_k_v39 s/\
 237   is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
 238   (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) /\
 239  &2< scs_b_v39 s i (i+1) /\ &2< scs_b_v39 s (i+1) (i+2)/\
 240 scs_a_v39 s (i+2) (i+3)< scs_b_v39 s (i+2) (i+3) /\
 241 scs_a_v39 s (i+ scs_k_v39 s -1) i< scs_b_v39 s (i+scs_k_v39 s -1) i
 242 ==>
 243   scs_a_v39 s (i) (i+1) = &2 /\ scs_b_v39 s (i) (i+1) <= &2 * h0 /\
 244   scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0  ==>
 245   (dist(v i,v (i+1)) = &2 <=> dist(v(i+1),v(i+2)) = &2))`;;
 246
 247 let CQAOQLR = prove_by_refinement( CQAOQLR_concl,
 248 [
 249 REPEAT STRIP_TAC
 250 THEN EQ_TAC;
 251
 252 STRIP_TAC
 253 THEN MP_TAC TFITSKC
 254 THEN RESA_TAC
 255 THEN MATCH_DICH_TAC 0
 256 THEN EXISTS_TAC`s:scs_v39`
 257 THEN ASM_REWRITE_TAC[];
 258
 259 ASM_TAC
 260 THEN REWRITE_TAC[IN]
 261 THEN REPEAT STRIP_TAC
 262 THEN ABBREV_TAC`k=scs_k_v39 s`
 263 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
 264 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
 265 THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 266 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ ~(k<=3)/\ 1<k`)
 267 THEN RESA_TAC
 268 THEN MRESA_TAC MM_SCS_OPP[`s`;`v`;`k`]
 269 THEN MRESA_TAC(GEN_ALL OPP_IS_SCS)[`(scs_opp_v39 s)`;`s:scs_v39`]
 270 THEN MP_TAC TFITSKC
 271 THEN RESA_TAC
 272 THEN THAYTHES_TAC 0[`(scs_opp_v39 s)`;`(\i. -- peropp (v:num->real^3) k i)`;`k- SUC((i+2) MOD k)`][IN]
 273 THEN POP_ASSUM MP_TAC
 274 THEN ASM_SIMP_TAC[peropp;OPP_SUC_MOD;K_SUC_2_MOD_SUB;K_SUC_2_MOD_SUB_ID;DIST_SYM_0;K_SCS_OPP;A_B_J_SCS_OPP;K_SUC_2_MOD_F_SUB_ID]
 275 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 276 THEN MP_TAC SCS_GENERIC_SYM_0
 277 THEN RESA_TAC
 278 THEN MP_TAC BASIC_OPP
 279 THEN RESA_TAC
 280 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(i+1) MOD k`;`v:num->real^3`;`i+1`][MOD_REFL;]
 281 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;]
 282 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(i+2) MOD k`;`v:num->real^3`;`i+2`][MOD_REFL;]
 283 THEN ONCE_REWRITE_TAC[DIST_SYM]
 284 THEN ASM_REWRITE_TAC[]
 285 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(i+1) MOD k`;`i MOD k `;`s:scs_v39`;`i+1`;`i`][MOD_REFL]
 286 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i+1) MOD k`;`i MOD k `;`s:scs_v39`;`i+1`;`i`][MOD_REFL]
 287 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(i) MOD k`;`(i+k-1) MOD k `;`s:scs_v39`;`i`;`i+k-1`][MOD_REFL]
 288 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i) MOD k`;`(i+k-1) MOD k `;`s:scs_v39`;`i`;`i+k-1`][MOD_REFL]
 289 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i+2) MOD k`;`(i+1) MOD k `;`s:scs_v39`;`i+2`;`i+1`][MOD_REFL]
 290 THEN STRIP_TAC
 291 THEN ONCE_REWRITE_TAC[DIST_SYM]
 292 THEN MATCH_DICH_TAC 0
 293 THEN STRIP_TAC;
 294
 295 ASM_TAC
 296 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 297 THEN REPEAT RESA_TAC;
 298
 299 STRIP_TAC;
 300
 301 ASM_TAC
 302 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 303 THEN REPEAT RESA_TAC;
 304
 305 STRIP_TAC;
 306
 307 ASM_TAC
 308 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 309 THEN REPEAT RESA_TAC;
 310
 311 STRIP_TAC;
 312
 313 ASM_TAC
 314 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 315 THEN REPEAT RESA_TAC;
 316
 317 REPEAT GEN_TAC
 318 THEN STRIP_TAC
 319 THEN ONCE_REWRITE_TAC[DIST_SYM]
 320 THEN MATCH_DICH_TAC(36-6)
 321 THEN MATCH_MP_TAC DIAG_OPP
 322 THEN ASM_REWRITE_TAC[]]);;
 323
 324
 325  end;;
 326
 327
 328 (*
 329 let check_completeness_claimA_concl =
 330   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 331 *)
 332
 333
 334
 335