text_formalization/local/SGTRNAF.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 Sgtrnaf = struct
  16 open Polyhedron;;
  17 open Sphere;;
  18 open Topology;;
  19 open Fan_misc;;
  20 open Planarity;;
  21 open Conforming;;
  22 open Hypermap;;
  23 open Fan;;
  24 open Topology;;
  25 open Wrgcvdr_cizmrrh;;
  26 open Local_lemmas;;
  27 open Collect_geom;;
  28 open Dih2k_hypermap;;
  29 open Wjscpro;;
  30 open Tecoxbm;;
  31 open Hdplygy;;
  32 open Nkezbfc_local;;
  33 open Flyspeck_constants;;
  34 open Gbycpxs;;
  35 open Pcrttid;;
  36 open Local_lemmas1;;
  37 open Pack_defs;;
  38
  39 open Hales_tactic;;
  40
  41 open Appendix;;
  42
  43
  44
  45
  46
  47 open Hypermap;;
  48 open Fan;;
  49 open Wrgcvdr_cizmrrh;;
  50 open Local_lemmas;;
  51 open Flyspeck_constants;;
  52 open Pack_defs;;
  53
  54 open Hales_tactic;;
  55
  56 open Appendix;;
  57
  58
  59 open Zithlqn;;
  60
  61
  62 open Xwitccn;;
  63
  64 open Ayqjtmd;;
  65
  66 open Jkqewgv;;
  67
  68
  69 open Mtuwlun;;
  70
  71 open Uxckfpe;;
  72
  73
  74
  75 let UXCKFPE2=prove_by_refinement(
  76 ` !s vv. is_scs_v39 s /\ vv IN BBs_v39 s
  77 /\  taustar_v39 s vv < &0
  78  ==> ~(BBprime2_v39 s = {})`,
  79   (* {{{ proof *)
  80 [
  81 REPEAT GEN_TAC
  82 THEN  STRIP_TAC
  83 THEN MRESA_TAC UXCKFPE[`s:scs_v39`;`vv:num->real^3`]
  84 THEN POP_ASSUM MP_TAC
  85 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv1. vv1 IN A`;BBprime2_v39;IN;BBindex_min_v39;]
  86 THEN STRIP_TAC
  87 THEN SUBGOAL_THEN`?n. (?vv1. BBprime_v39 s vv1 /\
  88      BBindex_v39 s vv1=n)` ASSUME_TAC;
  89
  90 EXISTS_TAC`BBindex_v39 s vv1`
  91 THEN EXISTS_TAC`vv1:num->real^3`
  92 THEN ASM_REWRITE_TAC[];
  93
  94 POP_ASSUM MP_TAC
  95 THEN REWRITE_TAC[MINIMAL]
  96 THEN STRIP_TAC
  97 THEN EXISTS_TAC`vv1':num->real^3`
  98 THEN POP_ASSUM MP_TAC
  99 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC (SYM th))
 100 THEN ASM_REWRITE_TAC[Misc_defs_and_lemmas.min_num;ARITH_RULE`(A=B:num)<=> (B=A)`]
 101 THEN STRIP_TAC
 102 THEN MATCH_MP_TAC SELECT_UNIQUE
 103 THEN ASM_REWRITE_TAC[BETA_THM;IMAGE;IN_ELIM_THM;]
 104 THEN REWRITE_TAC[IN]
 105 THEN STRIP_TAC
 106 THEN EQ_TAC;
 107
 108 STRIP_TAC
 109 THEN POP_ASSUM MP_TAC
 110 THEN ASM_REWRITE_TAC[]
 111 THEN SUBGOAL_THEN`(?x. BBprime_v39 s x /\ BBindex_v39 s vv1' = BBindex_v39 s x)`ASSUME_TAC;
 112
 113 EXISTS_TAC`vv1':num->real^3`
 114 THEN ASM_REWRITE_TAC[];
 115
 116 STRIP_TAC
 117 THEN POP_ASSUM(fun th-> MRESA1_TAC th`BBindex_v39 s vv1'`)
 118 THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <= BBindex_v39 s vv1' ==>
 119 BBindex_v39 s x < BBindex_v39 s vv1' \/ BBindex_v39 s x = BBindex_v39 s vv1'`)
 120 THEN RESA_TAC
 121 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
 122 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN
 123 MRESA1_TAC th` BBindex_v39 s x`)
 124 THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;
 125
 126 EXISTS_TAC`x:num->real^3`
 127 THEN ASM_REWRITE_TAC[];
 128
 129 POP_ASSUM MP_TAC
 130 THEN ASM_REWRITE_TAC[];
 131
 132 STRIP_TAC
 133 THEN ASM_REWRITE_TAC[]
 134 THEN STRIP_TAC;
 135
 136
 137
 138 EXISTS_TAC`vv1':num->real^3`
 139 THEN ASM_REWRITE_TAC[];
 140
 141
 142 REPEAT STRIP_TAC
 143 THEN ASM_REWRITE_TAC[]
 144 THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <BBindex_v39 s vv1'   \/ BBindex_v39 s vv1' <= BBindex_v39 s x`)
 145 THEN RESA_TAC;
 146
 147
 148
 149 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 150 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN
 151 MRESA1_TAC th` BBindex_v39 s x`)
 152 THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;
 153
 154 EXISTS_TAC`x:num->real^3`
 155 THEN ASM_REWRITE_TAC[];
 156
 157
 158 POP_ASSUM MP_TAC
 159 THEN ASM_REWRITE_TAC[];
 160 ]);;
 161   (* }}} *)
 162
 163
 164
 165
 166 let SGTRNAF =prove(
 167 `!s vv. is_scs_v39 s/\ unadorned_v39 s /\ vv IN BBs_v39 s /\
 168   taustar_v39 s vv < &0
 169  ==> ~(MMs_v39 s = {})`,
 170 REPEAT GEN_TAC
 171 THEN STRIP_TAC
 172 THEN MP_TAC unadorned_MMs
 173 THEN RESA_TAC
 174 THEN MATCH_MP_TAC UXCKFPE2
 175 THEN EXISTS_TAC`vv:num->real^3`
 176 THEN ASM_REWRITE_TAC[]);;
 177
 178
 179
 180
 181  end;;
 182
 183
 184 (*
 185 let check_completeness_claimA_concl =
 186   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 187 *)
 188
 189
 190
 191