text_formalization/local/FEKTYIY.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 (*
  12 remaining conclusions from appendix to Local Fan chapter
  13 *)
  14
  15
  16 module Fektyiy = struct
  17
  18
  19 open Polyhedron;;
  20 open Sphere;;
  21 open Topology;;
  22 open Fan_misc;;
  23 open Planarity;;
  24 open Conforming;;
  25 open Hypermap;;
  26 open Fan;;
  27 open Topology;;
  28 open Wrgcvdr_cizmrrh;;
  29 open Local_lemmas;;
  30 open Collect_geom;;
  31 open Dih2k_hypermap;;
  32 open Wjscpro;;
  33 open Tecoxbm;;
  34 open Hdplygy;;
  35 open Nkezbfc_local;;
  36 open Flyspeck_constants;;
  37 open Gbycpxs;;
  38 open Pcrttid;;
  39 open Local_lemmas1;;
  40 open Pack_defs;;
  41
  42 open Hales_tactic;;
  43
  44 open Appendix;;
  45
  46
  47
  48
  49
  50 open Hypermap;;
  51 open Fan;;
  52 open Wrgcvdr_cizmrrh;;
  53 open Local_lemmas;;
  54 open Flyspeck_constants;;
  55 open Pack_defs;;
  56
  57 open Hales_tactic;;
  58
  59 open Appendix;;
  60
  61
  62 open Zithlqn;;
  63
  64
  65 open Xwitccn;;
  66
  67 open Ayqjtmd;;
  68
  69 open Jkqewgv;;
  70
  71
  72 open Mtuwlun;;
  73
  74
  75 open Uxckfpe;;
  76 open Sgtrnaf;;
  77
  78 open Yxionxl;;
  79
  80 open Qknvmlb;;
  81 open Odxlstcv2;;
  82
  83 open Yxionxl2;;
  84 open Eyypqdw;;
  85 open Ocbicby;;
  86 open Imjxphr;;
  87
  88 open Nuxcoea;;
  89
  90
  91 let FEKTYIY_concl = `!s v.
  92   is_scs_v39 s /\ v IN MMs_v39 s /\ 3 < scs_k_v39 s  ==>
  93   ~coplanar ({vec 0} UNION IMAGE v (:num))`;;
  94
  95 let FEKTYIY= prove_by_refinement((FEKTYIY_concl),
  96 [
  97 REWRITE_TAC[Trigonometry2.coplanar1;IN]
  98 THEN REPEAT STRIP_TAC
  99 THEN ABBREV_TAC`k=scs_k_v39 s`
 100 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 101 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 102 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 103 THEN ABBREV_TAC`v0= (v:num->real^3) 0`
 104 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
 105 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
 106 THEN MP_TAC Local_lemmas.CVLF_LF_F
 107 THEN RESA_TAC
 108 THEN MRESA_TAC WL_IN_V[`0`;`v`]
 109 THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k:num`]
 110 THEN SUBGOAL_THEN`{ITER n (rho_node1 FF) v0 | n <= k+1} = V`ASSUME_TAC;
 111
 112 MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v0:real^3`]
 113 THEN MATCH_MP_TAC(GEN_ALL(SET_RULE`A SUBSET B/\ B SUBSET C/\ A=C==> B=C`))
 114 THEN TYPIFY `{ITER n (rho_node1 FF) v0 | n < CARD V}` EXISTS_TAC
 115 THEN STRIP_TAC;
 116
 117 ASM_REWRITE_TAC[]
 118 THEN SYM_ASSUM_TAC
 119 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;]
 120 THEN REPEAT RESA_TAC
 121 THEN TYPIFY `n` EXISTS_TAC
 122 THEN DICH_TAC 1
 123 THEN ASM_REWRITE_TAC[]
 124 THEN ARITH_TAC;
 125
 126 ASM_REWRITE_TAC[]
 127 THEN REMOVE_ASSUM_TAC
 128 THEN EXPAND_TAC"V"
 129 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IMAGE;SET_RULE`(a:A) IN(:A)`]
 130 THEN REPEAT RESA_TAC
 131 THEN TYPIFY `n` EXISTS_TAC
 132 THEN ASM_REWRITE_TAC[]
 133 THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
 134 THEN RESA_TAC
 135 THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v0`;`v`;` 0`][ARITH_RULE`a+0=a`];
 136
 137 POP_ASSUM MP_TAC
 138 THEN MRESAL_TAC Nuxcoea.MMS_IMP_BBPRIME[`s:scs_v39`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
 139 THEN MP_TAC (SET_RULE`{vec 0:real^3} UNION V SUBSET x ==> vec 0 IN x /\V SUBSET x`)
 140 THEN RESA_TAC
 141 THEN STRIP_TAC
 142 THEN MRESA_TAC Lunar_deform.AZIM_PI_ITER_LOCAL_FAN[`E`;`V`;`V`;`x`;`k+1`;`FF`;`v0:real^3`]
 143 THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`v`]
 144 THEN POP_ASSUM MP_TAC
 145 THEN REWRITE_TAC[REAL_ARITH`~(a< b)<=> b<=a`;sol_local]
 146 THEN MATCH_MP_TAC (REAL_ARITH`&0< a/\ b= &0==> a<= &2 *a +b`)
 147 THEN REWRITE_TAC[PI_WORKS]
 148 THEN MATCH_MP_TAC SUM_EQ_0
 149 THEN GEN_TAC
 150 THEN STRIP_TAC
 151 THEN MRESA_TAC Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA[`V:real^3->bool`;`FF`;`E`;`x'`]
 152 THEN MRESA_TAC Local_lemmas.DETER_RHO_NODE[`V:real^3->bool`;`E`;`FF`;`FST x'`;`SND x'`]
 153 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V2[`E`;`FF`;`x'`;`V`]
 154 THEN MRESA_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND[`V`;`E`;`FF`;`FST x'`]
 155 THEN DICH_TAC (27-22)
 156 THEN EXPAND_TAC "FF"
 157 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM]
 158 THEN RESA_TAC
 159 THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ (k+1)-1=k/\ ~(k=0)/\ 1<k/\ SUC (x'' + k - 1) =1 * k + x''`)
 160 THEN RESA_TAC
 161 THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v0`;`v`;` 0`][ARITH_RULE`a+0=a`]
 162 THEN DICH_TAC (34-21)
 163 THEN MRESA_TAC DIVISION[`x''+k-1`;`k`]
 164 THEN RESA_TAC
 165 THEN THAYTHEL_TAC 0 [`(x''+k-1) MOD k`][ARITH_RULE`a+1= SUC a/\ a+2= SUC (SUC a)`]
 166 THEN POP_ASSUM MP_TAC
 167 THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`x''+k-1`;`k`]
 168 THEN MRESA_TAC MOD_REFL[`x'' `;`k`]
 169 THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`x''`]
 170 THEN MRESA_TAC
 171 CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC ((x'' + k - 1) MOD k)`;`v:num->real^3`;`SUC ((x'' + k - 1) MOD k) MOD k`]
 172 THEN MRESA_TAC
 173 CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`x'' MOD k`;`v:num->real^3`;`x''`]
 174 THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`x''`;`k`]
 175 THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`SUC((x''+k-1) MOD k)`;`k`]
 176 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 177 THEN MRESA_TAC MOD_REFL[`SUC x'' `;`k`]
 178 THEN MRESA_TAC MOD_REFL[`x''+k-1 `;`k`]
 179 THEN MRESA_TAC
 180 CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC (SUC ((x'' + k - 1) MOD k))`;`v:num->real^3`;`SUC(SUC ((x'' + k - 1) MOD k)) MOD k`]
 181 THEN MRESA_TAC
 182 CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC x'' MOD k`;`v:num->real^3`;`SUC x''`]
 183 THEN MRESA_TAC
 184 CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(x''+k-1) MOD k`;`v:num->real^3`;`x''+k-1`]
 185 THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x''`;`v`;` x''`][ARITH_RULE`a+0=a`]
 186 THEN MRESA_TAC WL_IN_V[`x''`;`v`]
 187 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
 188 THEN RESA_TAC
 189 THEN THAYTHE_TAC 0[`v x''`]
 190 THEN REWRITE_TAC[ARITH_RULE`a+k-1=k-1+a`]
 191 THEN SYM_ASSUM_TAC
 192 THEN STRIP_TAC
 193 THEN MP_TAC(REAL_ARITH`&0< pi==> ~(pi= &0)`)
 194 THEN ASM_REWRITE_TAC[PI_WORKS]
 195 THEN RESA_TAC
 196 THEN ASM_REWRITE_TAC[Rogers.AZIM_COMPL_EXT]
 197 THEN REAL_ARITH_TAC]);;
 198
 199
 200
 201
 202  end;;
 203
 204
 205 (*
 206 let check_completeness_claimA_concl =
 207   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 208 *)
 209
 210
 211
 212