text_formalization/local/AYQJTMD.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 remaining conclusions from appendix to Local Fan chapter
  11 *)
  12
  13
  14 module Ayqjtmd = struct
  15
  16
  17 open Polyhedron;;
  18 open Sphere;;
  19 open Topology;;
  20 open Fan_misc;;
  21 open Planarity;;
  22 open Conforming;;
  23 open Hypermap;;
  24 open Fan;;
  25 open Topology;;
  26 open Wrgcvdr_cizmrrh;;
  27 open Local_lemmas;;
  28 open Collect_geom;;
  29 open Dih2k_hypermap;;
  30 open Wjscpro;;
  31 open Tecoxbm;;
  32 open Hdplygy;;
  33 open Nkezbfc_local;;
  34 open Flyspeck_constants;;
  35 open Gbycpxs;;
  36 open Pcrttid;;
  37 open Local_lemmas;;
  38 open Pack_defs;;
  39
  40 open Hales_tactic;;
  41
  42 open Appendix;;
  43
  44
  45
  46
  47
  48 open Hypermap;;
  49 open Fan;;
  50 open Wrgcvdr_cizmrrh;;
  51 open Local_lemmas;;
  52 open Flyspeck_constants;;
  53 open Pack_defs;;
  54
  55 open Hales_tactic;;
  56
  57 open Appendix;;
  58
  59
  60 open Zithlqn;;
  61
  62
  63
  64
  65
  66
  67 open Xwitccn;;
  68
  69
  70
  71
  72 let XWITCCN2=prove_by_refinement(
  73 ` !s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s
  74 /\  taustar_v39 s vv < &0
  75  ==> ~(BBprime2_v39 s = {})`,
  76   (* {{{ proof *)
  77 [
  78 REPEAT GEN_TAC
  79 THEN  STRIP_TAC
  80 THEN MRESA_TAC XWITCCN[`s:scs_v39`;`vv:num->real^3`]
  81 THEN POP_ASSUM MP_TAC
  82 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv1. vv1 IN A`;BBprime2_v39;IN;BBindex_min_v39;]
  83 THEN STRIP_TAC
  84 THEN SUBGOAL_THEN`?n. (?vv1. BBprime_v39 s vv1 /\
  85      BBindex_v39 s vv1=n)` ASSUME_TAC;
  86
  87 EXISTS_TAC`BBindex_v39 s vv1`
  88 THEN EXISTS_TAC`vv1:num->real^3`
  89 THEN ASM_REWRITE_TAC[];
  90
  91 POP_ASSUM MP_TAC
  92 THEN REWRITE_TAC[MINIMAL]
  93 THEN STRIP_TAC
  94 THEN EXISTS_TAC`vv1':num->real^3`
  95 THEN POP_ASSUM MP_TAC
  96 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC (SYM th))
  97 THEN ASM_REWRITE_TAC[Misc_defs_and_lemmas.min_num;ARITH_RULE`(A=B:num)<=> (B=A)`]
  98 THEN STRIP_TAC
  99 THEN MATCH_MP_TAC SELECT_UNIQUE
 100 THEN ASM_REWRITE_TAC[BETA_THM;IMAGE;IN_ELIM_THM;]
 101 THEN REWRITE_TAC[IN]
 102 THEN STRIP_TAC
 103 THEN EQ_TAC;
 104
 105 STRIP_TAC
 106 THEN POP_ASSUM MP_TAC
 107 THEN ASM_REWRITE_TAC[]
 108 THEN SUBGOAL_THEN`(?x. BBprime_v39 s x /\ BBindex_v39 s vv1' = BBindex_v39 s x)`ASSUME_TAC;
 109
 110 EXISTS_TAC`vv1':num->real^3`
 111 THEN ASM_REWRITE_TAC[];
 112
 113 STRIP_TAC
 114 THEN POP_ASSUM(fun th-> MRESA1_TAC th`BBindex_v39 s vv1'`)
 115 THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <= BBindex_v39 s vv1' ==>
 116 BBindex_v39 s x < BBindex_v39 s vv1' \/ BBindex_v39 s x = BBindex_v39 s vv1'`)
 117 THEN RESA_TAC
 118 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
 119 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN
 120 MRESA1_TAC th` BBindex_v39 s x`)
 121 THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;
 122
 123 EXISTS_TAC`x:num->real^3`
 124 THEN ASM_REWRITE_TAC[];
 125
 126 POP_ASSUM MP_TAC
 127 THEN ASM_REWRITE_TAC[];
 128
 129 STRIP_TAC
 130 THEN ASM_REWRITE_TAC[]
 131 THEN STRIP_TAC;
 132
 133
 134
 135 EXISTS_TAC`vv1':num->real^3`
 136 THEN ASM_REWRITE_TAC[];
 137
 138
 139 REPEAT STRIP_TAC
 140 THEN ASM_REWRITE_TAC[]
 141 THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <BBindex_v39 s vv1'   \/ BBindex_v39 s vv1' <= BBindex_v39 s x`)
 142 THEN RESA_TAC;
 143
 144
 145
 146 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 147 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN
 148 MRESA1_TAC th` BBindex_v39 s x`)
 149 THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;
 150
 151 EXISTS_TAC`x:num->real^3`
 152 THEN ASM_REWRITE_TAC[];
 153
 154
 155 POP_ASSUM MP_TAC
 156 THEN ASM_REWRITE_TAC[];
 157 ]);;
 158   (* }}} *)
 159
 160
 161 let unadorned_MMs=prove_by_refinement(
 162 `  unadorned_v39 s ==> (MMs_v39 s = BBprime2_v39 s)`
 163 ,
 164   (* {{{ proof *)
 165 [
 166 REWRITE_TAC[FUN_EQ_THM]
 167 THEN REWRITE_TAC[unadorned_v39;MMs_v39;]
 168 THEN REPEAT STRIP_TAC
 169 THEN EQ_TAC
 170 THEN RESA_TAC;
 171
 172 STRIP_TAC;
 173
 174 SET_TAC[];
 175
 176 STRIP_TAC;
 177
 178 SET_TAC[];
 179
 180 STRIP_TAC;
 181
 182 SET_TAC[];
 183
 184
 185 POP_ASSUM MP_TAC
 186 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;]
 187 THEN RESA_TAC;
 188 ]);;
 189   (* }}} *)
 190
 191
 192
 193
 194 let S_INIT_IS_UNADORNED=prove(
 195 `MEM s s_init_list_v39
 196 ==> unadorned_v39 s`,
 197 REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;set_of_list;LET_DEF;LET_END_DEF
 198 ;SET_RULE`A IN {A1,A2,A3,A4,A5,A6,A7,A8} <=> A= A1 \/ A= A2 \/  A= A3 \/ A= A4 \/ A= A5 \/ A= A6 \/ A= A7 \/ A= A8`]
 199 THEN REPEAT GEN_TAC
 200 THEN RESA_TAC
 201 THEN REWRITE_TAC[unadorned_v39]
 202 THEN ASM_REWRITE_TAC[scs_lo_v39_explicit;scs_str_v39_explicit;scs_am_v39_explicit;scs_bm_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`~(4<=3)/\ 3-1=2`;mk_unadorned_v39;CS_ADJ;scs_J_v39_explicit;change_type_v2;d_tame ;change_type_v3;scs_hi_v39_explicit;]);;
 203
 204
 205
 206 let AYQJTMD =prove(
 207 `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
 208   taustar_v39 s vv < &0
 209  ==> ~(MMs_v39 s = {})`,
 210 REPEAT GEN_TAC
 211 THEN STRIP_TAC
 212 THEN MP_TAC S_INIT_IS_UNADORNED
 213 THEN RESA_TAC
 214 THEN MP_TAC unadorned_MMs
 215 THEN RESA_TAC
 216 THEN MATCH_MP_TAC XWITCCN2
 217 THEN EXISTS_TAC`vv:num->real^3`
 218 THEN ASM_REWRITE_TAC[]);;
 219
 220
 221
 222 let EAPGLE =prove(  `(!s. MEM s s_init_list_v39 ==> MMs_v39 s = {}) ==> JEJTVGB_assume_v39`,
 223 REPEAT STRIP_TAC
 224 THEN MATCH_MP_TAC ZITHLQN
 225 THEN REPEAT STRIP_TAC
 226 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv< &0\/ &0 <= taustar_v39 s vv`)
 227 THEN RESA_TAC
 228 THEN MRESA_TAC AYQJTMD[`s:scs_v39`;`vv:num->real^3`]
 229 THEN ASM_TAC
 230 THEN STRIP_TAC
 231 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 232 THEN MRESA1_TAC th`s:scs_v39`));;
 233
 234
 235
 236  end;;
 237