text_formalization/local/LKGRQUI.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 Lkgrqui = struct
  16
  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 open Qknvmlb;;
  80
  81
  82 let SLICE_IS_UNADORNED=prove(`unadorned_v39 (scs_half_slice_v39 s p q d' mkj)`,
  83 ASM_REWRITE_TAC[MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;scs_half_slice_v39;is_scs_v39;scs_diag;scs_v39_explicit;unadorned_v39]
  84 );;
  85
  86
  87 let LKGRQUI= prove_by_refinement(
  88 `       is_scs_v39 s /\ scs_diag (scs_k_v39 s) p q /\
  89           is_scs_slice_v39 s s' s'' p q
  90          ==> scs_arrow_v39 {s} {s',s''}`,
  91 [REWRITE_TAC[scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;PAIR_EQ]
  92 THEN REPEAT STRIP_TAC;
  93
  94 POP_ASSUM MP_TAC
  95 THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/a=c`]
  96 THEN RESA_TAC;
  97
  98 MP_TAC SCS_HALF_SLICE_IS_A_SCS
  99 THEN RESA_TAC;
 100
 101 MP_TAC SCS_SLICE_SYM
 102 THEN RESA_TAC;
 103
 104 MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`]
 105 THEN ASM_TAC
 106 THEN REWRITE_TAC[scs_diag]
 107 THEN REPEAT RESA_TAC;
 108
 109 DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);
 110
 111 ASM_REWRITE_TAC[];
 112
 113 ASM_REWRITE_TAC[]
 114 THEN POP_ASSUM MP_TAC
 115 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 116 THEN REPEAT STRIP_TAC
 117 THEN POP_ASSUM MP_TAC
 118 THEN RESA_TAC
 119 THEN POP_ASSUM MP_TAC
 120 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?vv. A vv`;]
 121 THEN RESA_TAC
 122 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 123 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 124 THEN MP_TAC th
 125 THEN ASSUME_TAC th)
 126 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF]
 127 THEN ABBREV_TAC`mkj=scs_J_v39 s' 0 (scs_k_v39 s' - 1)`
 128 THEN ABBREV_TAC`d'=scs_d_v39 s'`
 129 THEN ABBREV_TAC`d''=scs_d_v39 s''`
 130 THEN REWRITE_TAC[scs_slice_v39;PAIR_EQ]
 131 THEN DISCH_TAC
 132 THEN ABBREV_TAC`vv'  = (\i. (vv:num->real^3) (i MOD (scs_k_v39 s')+ p MOD (scs_k_v39 s)))`
 133 THEN POP_ASSUM MP_TAC
 134 THEN RESA_TAC
 135 THEN MP_TAC QKNVMLB1
 136 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF]
 137 THEN STRIP_TAC
 138 THEN SUBGOAL_THEN`scs_bm_v39 s q p < &4 /\
 139       (scs_k_v39 s = 4 \/ scs_bm_v39 s q p <= cstab) /\
 140       scs_diag (scs_k_v39 s) q p` ASSUME_TAC;
 141
 142 ASM_TAC
 143 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;scs_diag;is_scs_v39]
 144 THEN REPEAT RESA_TAC;
 145
 146 MRESAL_TAC (GEN_ALL QKNVMLB1)[`vv:num->real^3`;`s:scs_v39`;`q:num`;`p:num`;`d'':real`;`mkj:bool`]
 147 [LET_DEF;LET_END_DEF]
 148 THEN ABBREV_TAC`vv''=(\i. (vv:num->real^3)
 149            (i MOD scs_k_v39 (scs_half_slice_v39 s q p d'' mkj) +
 150             q MOD scs_k_v39 s))`
 151 THEN MP_TAC QKNVMLB3
 152 THEN RESA_TAC
 153 THEN REPLICATE_TAC (14-3)(POP_ASSUM MP_TAC)
 154 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 155 THEN MP_TAC th
 156 THEN ASSUME_TAC th)
 157 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[MMs_v39;BBprime_v39;BBprime2_v39;LET_DEF;LET_END_DEF]
 158 THEN REWRITE_TAC[BBprime_v39;BBprime2_v39]
 159 THEN STRIP_TAC
 160 THEN MP_TAC(REAL_ARITH`taustar_v39 (scs_half_slice_v39 s p q d' mkj) vv' +
 161       taustar_v39 (scs_half_slice_v39 s q p d'' mkj) vv'' <=
 162       taustar_v39 s vv
 163 /\ taustar_v39 s vv< &0
 164 ==> taustar_v39 (scs_half_slice_v39 s p q d' mkj) vv' < &0 \/ taustar_v39 (scs_half_slice_v39 s q p d'' mkj) vv''< &0`)
 165 THEN RESA_TAC;
 166
 167
 168 EXISTS_TAC`s':scs_v39`
 169 THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
 170 THEN MATCH_MP_TAC SGTRNAF
 171 THEN EXISTS_TAC`vv':num->real^3`
 172 THEN ASM_REWRITE_TAC[IN]
 173 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 174 THEN RESA_TAC
 175 THEN REWRITE_TAC[SLICE_IS_UNADORNED];
 176
 177
 178 EXISTS_TAC`s'':scs_v39`
 179 THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
 180 THEN MATCH_MP_TAC SGTRNAF
 181 THEN EXISTS_TAC`vv'':num->real^3`
 182 THEN ASM_REWRITE_TAC[IN]
 183 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 184 THEN RESA_TAC
 185 THEN REWRITE_TAC[SLICE_IS_UNADORNED]
 186 THEN MP_TAC SCS_SLICE_SYM
 187 THEN RESA_TAC
 188 THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`];
 189
 190
 191
 192 EXISTS_TAC`s':scs_v39`
 193 THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
 194 THEN MATCH_MP_TAC SGTRNAF
 195 THEN EXISTS_TAC`vv':num->real^3`
 196 THEN ASM_REWRITE_TAC[IN]
 197 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 198 THEN RESA_TAC
 199 THEN REWRITE_TAC[SLICE_IS_UNADORNED];
 200
 201 EXISTS_TAC`s'':scs_v39`
 202 THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
 203 THEN MATCH_MP_TAC SGTRNAF
 204 THEN EXISTS_TAC`vv'':num->real^3`
 205 THEN ASM_REWRITE_TAC[IN]
 206 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 207 THEN RESA_TAC
 208 THEN REWRITE_TAC[SLICE_IS_UNADORNED]
 209 THEN MP_TAC SCS_SLICE_SYM
 210 THEN RESA_TAC
 211 THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`];
 212
 213 EXISTS_TAC`s':scs_v39`
 214 THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
 215 THEN MATCH_MP_TAC SGTRNAF
 216 THEN EXISTS_TAC`vv':num->real^3`
 217 THEN ASM_REWRITE_TAC[IN]
 218 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 219 THEN RESA_TAC
 220 THEN REWRITE_TAC[SLICE_IS_UNADORNED];
 221
 222 EXISTS_TAC`s'':scs_v39`
 223 THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
 224 THEN MATCH_MP_TAC SGTRNAF
 225 THEN EXISTS_TAC`vv'':num->real^3`
 226 THEN ASM_REWRITE_TAC[IN]
 227 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 228 THEN RESA_TAC
 229 THEN REWRITE_TAC[SLICE_IS_UNADORNED]
 230 THEN MP_TAC SCS_SLICE_SYM
 231 THEN RESA_TAC
 232 THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`]
 233 ;
 234
 235 EXISTS_TAC`s':scs_v39`
 236 THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
 237 THEN MATCH_MP_TAC SGTRNAF
 238 THEN EXISTS_TAC`vv':num->real^3`
 239 THEN ASM_REWRITE_TAC[IN]
 240 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 241 THEN RESA_TAC
 242 THEN REWRITE_TAC[SLICE_IS_UNADORNED];
 243
 244 EXISTS_TAC`s'':scs_v39`
 245 THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
 246 THEN MATCH_MP_TAC SGTRNAF
 247 THEN EXISTS_TAC`vv'':num->real^3`
 248 THEN ASM_REWRITE_TAC[IN]
 249 THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
 250 THEN RESA_TAC
 251 THEN REWRITE_TAC[SLICE_IS_UNADORNED]
 252 THEN MP_TAC SCS_SLICE_SYM
 253 THEN RESA_TAC
 254 THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`]
 255 ]);;
 256
 257
 258
 259  end;;
 260
 261
 262 (*
 263 let check_completeness_claimA_concl =
 264   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 265 *)
 266
 267
 268
 269