text_formalization/tame/HRXEFDM.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Tame Hypermap                                                     *)
   5 (* Author: Alexey Solovyev                                                    *)
   6 (* Date: 2010-06-17                                                           *)
   7 (* Note: use Tame_lemmas.sum_tauVEF_upper_bound because the theorem below     *)
   8 (*       has unproved assumptions                                             *)
   9 (* ========================================================================== *)
  10
  11 (* Proof of HRXEFDM *)
  12
  13 flyspeck_needs "tame/TameGeneral.hl";;
  14
  15
  16 module Hrxefdm_tame = struct
  17
  18
  19 open Hypermap;;
  20 open Fan_defs;;
  21 open Tame_defs;;
  22 open Tame_general;;
  23 open Hypermap_and_fan;;
  24
  25
  26 let tauVEF_alt1 = prove(`!V E f. conforming (V,E) /\ f IN face_set_of_fan (V,E) ==>
  27                           tauVEF (V,E,f) = sol (vec 0) (dartset_leads_into (vec 0,V,E) f)  + (&2 - &(CARD f)) * sol0 - sol0 / pi * sum f (\x. azim_dart (V,E) x * (lmfun (h_dart x) - &1))`,
  28    REWRITE_TAC[face_set_of_fan; conforming; conforming_solid_angle] THEN
  29      REPEAT STRIP_TAC THEN
  30      FIRST_X_ASSUM (MP_TAC o SPEC `f:real^3#real^3->bool`) THEN
  31      ASM_REWRITE_TAC[] THEN
  32      DISCH_THEN (MP_TAC o let_RULE) THEN
  33      DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN
  34      DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN
  35      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
  36
  37      REWRITE_TAC[tauVEF] THEN
  38      REWRITE_TAC[REAL_ARITH `a * (&1 + b * (&1 - c)) = a - b * (a * (c - &1))`] THEN
  39      SUBGOAL_THEN `FINITE (f:real^3#real^3->bool)` ASSUME_TAC THENL
  40      [
  41        POP_ASSUM MP_TAC THEN
  42          REWRITE_TAC[face_set; set_of_orbits; GSYM face] THEN
  43          REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
  44          ASM_REWRITE_TAC[FACE_FINITE];
  45        ALL_TAC
  46      ] THEN
  47
  48      ASM_SIMP_TAC[SUM_SUB; SUM_LMUL; SUM_CONST] THEN
  49      REAL_ARITH_TAC);;
  50
  51
  52
  53 let tauVEF_alt2 = prove(`!V E f. conforming (V,E) /\ f IN face_set_of_fan (V,E)
  54                           ==> tauVEF (V,E,f) = sol  (vec 0) (dartset_leads_into (vec 0,V,E) f) * (&1 + sol0 / pi) - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`,
  55    REPEAT STRIP_TAC THEN
  56      ASM_SIMP_TAC[tauVEF_alt1] THEN
  57      REPEAT (POP_ASSUM MP_TAC) THEN
  58      REWRITE_TAC[conforming; conforming_solid_angle; face_set_of_fan] THEN
  59      REPEAT STRIP_TAC THEN
  60      FIRST_X_ASSUM (MP_TAC o SPEC `f:real^3#real^3->bool`) THEN
  61      ASM_REWRITE_TAC[] THEN
  62      DISCH_THEN (fun th -> REWRITE_TAC[let_RULE th]) THEN
  63
  64      SUBGOAL_THEN `FINITE (f:real^3#real^3->bool)` ASSUME_TAC THENL
  65      [
  66        POP_ASSUM MP_TAC THEN
  67          REWRITE_TAC[face_set; set_of_orbits; GSYM face] THEN
  68          REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
  69          ASM_REWRITE_TAC[FACE_FINITE];
  70        ALL_TAC
  71      ] THEN
  72
  73      REWRITE_TAC[REAL_ARITH `a * (b - &1) = a * b - a`] THEN
  74      ASM_SIMP_TAC[SUM_SUB; SUM_CONST] THEN
  75
  76      MP_TAC PI_POS THEN
  77      CONV_TAC REAL_FIELD);;
  78
  79
  80
  81
  82 let CHOICE_CONST_LEMMA = prove(`!f s. (!x y. x IN s /\ y IN s ==> f x = f y) ==> (!x. x IN s ==> f x = f (CHOICE s))`,
  83  MESON_TAC[CHOICE]);;
  84
  85
  86 let scriptL_lemma = prove(`!V E. FAN (vec 0,V,E)
  87                             ==> scriptL V = sum (node_set (hypermap_of_fan (V,E))) (\n. lmfun (h_dart (CHOICE n)))`,
  88    REPEAT STRIP_TAC THEN
  89      REWRITE_TAC[scriptL] THEN
  90      MP_TAC (SPEC_ALL NODE_SET_AS_IMAGE) THEN
  91      ASM_REWRITE_TAC[] THEN
  92      REPEAT STRIP_TAC THEN
  93      ASM_REWRITE_TAC[] THEN
  94
  95      SUBGOAL_THEN `(\v:real^3. lmfun (norm v / &2)) = (\n. lmfun (h_dart (CHOICE n))) o (f:real^3->(real^3#real^3->bool))` MP_TAC THENL
  96      [
  97        ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; h_dart];
  98        ALL_TAC
  99      ] THEN
 100
 101      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 102      MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
 103      REPEAT STRIP_TAC THEN
 104      FIRST_X_ASSUM (MP_TAC o SPECL [`x:real^3`; `y:real^3`]) THEN
 105      ASM_SIMP_TAC[]);;
 106
 107
 108
 109 let HRXEFDM_lemma1 = prove(`!V E. FAN (vec 0,V,E) ==>
 110                              sum (face_set_of_fan (V,E)) (\f. sum f (\x. azim_dart (V,E) x * lmfun (h_dart x)))
 111                              = &2 * pi * scriptL V`,
 112    REPEAT STRIP_TAC THEN
 113      SUBGOAL_THEN `!n. n IN node_set (hypermap_of_fan (V,E)) ==> sum n (azim_dart (V,E)) = &2 * pi` ASSUME_TAC THENL
 114      [
 115        GEN_TAC THEN
 116          REWRITE_TAC[node_set; set_of_orbits; GSYM node] THEN
 117          REWRITE_TAC[IN_ELIM_THM] THEN
 118          ASM_SIMP_TAC[dart; HYPERMAP_OF_FAN] THEN
 119          STRIP_TAC THEN
 120          MP_TAC (SPEC_ALL SUM_AZIM_DART) THEN
 121          ASM_SIMP_TAC[];
 122        ALL_TAC
 123      ] THEN
 124
 125      REWRITE_TAC[face_set_of_fan; DART_SUM_lemma] THEN
 126      REWRITE_TAC[GSYM (SPEC_ALL DART_SUM_lemma)] THEN
 127      ABBREV_TAC `g = (\n. sum n (\x. azim_dart (V,E) x * lmfun (h_dart x)))` THEN
 128      MP_TAC (ISPECL [`g:(real^3#real^3->bool)->real`; `node_set (hypermap_of_fan (V,E))`] SUM_RESTRICT) THEN
 129      REWRITE_TAC[FINITE_HYPERMAP_ORBITS] THEN
 130      DISCH_TAC THEN
 131
 132      SUBGOAL_THEN `!n. n IN node_set (hypermap_of_fan (V,E)) ==> g n = &2 * pi * lmfun (h_dart (CHOICE n))` MP_TAC THENL
 133      [
 134        REMOVE_ASSUM THEN GEN_TAC THEN
 135          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 136          DISCH_TAC THEN
 137          FIRST_ASSUM (fun th -> FIRST_X_ASSUM (ASSUME_TAC o (fun th2 -> MATCH_MP th2 th))) THEN
 138          MP_TAC (ISPECL [`(\x. azim_dart (V,E) x * lmfun (h_dart x))`; `n:real^3#real^3->bool`] SUM_RESTRICT) THEN
 139          SUBGOAL_THEN `FINITE (n:real^3#real^3->bool)` ASSUME_TAC THENL
 140          [
 141            REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 142              REWRITE_TAC[node_set; set_of_orbits; GSYM node] THEN
 143              REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 144              ASM_REWRITE_TAC[NODE_FINITE];
 145            ALL_TAC
 146          ] THEN
 147          ASM_REWRITE_TAC[] THEN
 148          DISCH_TAC THEN
 149
 150          ABBREV_TAC `c = lmfun (h_dart (CHOICE (n:real^3#real^3->bool)))` THEN
 151          SUBGOAL_THEN `!x. (if x IN n then azim_dart (V,E) x * lmfun (h_dart x) else &0) = (if x IN n then azim_dart (V,E) x * c else &0)` MP_TAC THENL
 152          [
 153            GEN_TAC THEN
 154              ASM_CASES_TAC `x:real^3#real^3 IN n` THEN ASM_REWRITE_TAC[] THEN
 155              SUBGOAL_THEN `h_dart (x:real^3#real^3) = h_dart (CHOICE (n:real^3#real^3->bool))` (fun th -> ASM_REWRITE_TAC[th]) THEN
 156              MP_TAC (ISPECL [`h_dart:real^3#real^3->real`; `n:real^3#real^3->bool`] CHOICE_CONST_LEMMA) THEN
 157              ANTS_TAC THENL
 158              [
 159                REPEAT STRIP_TAC THEN
 160                  REWRITE_TAC[h_dart] THEN
 161                  AP_THM_TAC THEN AP_TERM_TAC THEN
 162                  AP_TERM_TAC THEN
 163                  MP_TAC (SPEC_ALL FST_NODE_lemma) THEN
 164                  ASM_REWRITE_TAC[] THEN
 165                  DISCH_THEN MATCH_MP_TAC THEN
 166                  ASM_REWRITE_TAC[];
 167                ALL_TAC
 168              ] THEN
 169              DISCH_THEN MATCH_MP_TAC THEN
 170              ASM_REWRITE_TAC[];
 171            ALL_TAC
 172          ] THEN
 173          REMOVE_ASSUM THEN
 174          DISCH_TAC THEN
 175          FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
 176          ASM_REWRITE_TAC[] THEN
 177          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 178          MP_TAC (ISPECL [`(\x. azim_dart (V,E) x * c)`; `n:real^3#real^3->bool`] SUM_RESTRICT) THEN
 179          ASM_SIMP_TAC[SUM_RMUL; ETA_AX] THEN
 180          REWRITE_TAC[REAL_MUL_ASSOC];
 181        ALL_TAC
 182      ] THEN
 183
 184      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 185      DISCH_TAC THEN
 186      SUBGOAL_THEN `!x. (if x IN node_set (hypermap_of_fan (V,E)) then g x else &0) = (if x IN node_set (hypermap_of_fan (V,E)) then &2 * pi * lmfun (h_dart (CHOICE x)) else &0)` MP_TAC THENL
 187      [
 188        GEN_TAC THEN
 189          ASM_CASES_TAC `x IN node_set (hypermap_of_fan (V,E))` THEN ASM_REWRITE_TAC[] THEN
 190          ASM_SIMP_TAC[];
 191        ALL_TAC
 192      ] THEN
 193
 194      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 195      MP_TAC (ISPECL [`(\x:real^3#real^3->bool. &2 * pi * lmfun (h_dart (CHOICE x)))`; `node_set (hypermap_of_fan (V,E))`] SUM_RESTRICT) THEN
 196      REWRITE_TAC[FINITE_HYPERMAP_ORBITS] THEN
 197      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 198      REWRITE_TAC[SUM_LMUL] THEN
 199      ASM_SIMP_TAC[scriptL_lemma]);;
 200
 201
 202
 203
 204
 205 let solid_angle_sum_assumption = `!V E. sum (face_set_of_fan (V,E)) (\f. sol (vec 0) (dartset_leads_into (vec 0,V,E) f) ) = &4 * pi`;;
 206
 207
 208
 209 let HRXEFDM_concl = `!V.  contravening V  ==>
 210      (  sum (face_set_of_fan (V,ESTD V)) (\ f.  tauVEF (V,ESTD V,f) ) < &4 * pi - &20 * sol0 )`;;
 211
 212
 213 let HRXEFDM_concl2 = mk_imp (list_mk_conj [`!V. contravening V ==> conforming (V,ESTD V)`;
 214                                            solid_angle_sum_assumption], HRXEFDM_concl);;
 215
 216
 217
 218
 219 (* g (HRXEFDM_concl2);; *)
 220 let HRXEFDM = prove(HRXEFDM_concl2,
 221   REPEAT STRIP_TAC THEN
 222     REPEAT (FIRST_X_ASSUM (ASSUME_TAC o SPEC `V:real^3->bool`)) THEN
 223     POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 224     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 225     FIRST_X_ASSUM (ASSUME_TAC o SPEC `ESTD V`) THEN
 226
 227     SUBGOAL_THEN `FINITE (face_set_of_fan (V,ESTD V))` ASSUME_TAC THENL
 228     [
 229       REWRITE_TAC[face_set_of_fan; FINITE_HYPERMAP_ORBITS];
 230       ALL_TAC
 231     ] THEN
 232
 233     SUBGOAL_THEN `sum (face_set_of_fan (V,ESTD V)) (\f. tauVEF (V,ESTD V,f)) = &4 * pi * (&1 + sol0 / pi) - sol0 / pi * &2 * pi * scriptL V` ASSUME_TAC THENL
 234     [
 235       MP_TAC (ISPECL [`\f. tauVEF (V,ESTD V,f)`; `face_set_of_fan (V,ESTD V)`] SUM_RESTRICT) THEN
 236         ASM_REWRITE_TAC[] THEN
 237         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 238         ABBREV_TAC `g = (\f. sol (vec 0) (dartset_leads_into (vec 0,V,ESTD V) f)  * (&1 + sol0 / pi) - sol0 / pi * sum f (\x. azim_dart (V,ESTD V) x * lmfun (h_dart x)))` THEN
 239
 240         SUBGOAL_THEN `!x. (if x IN face_set_of_fan (V,ESTD V) then tauVEF (V,ESTD V,x) else &0) = (if x IN face_set_of_fan (V,ESTD V) then g x else &0)` (fun th -> REWRITE_TAC[th]) THENL
 241         [
 242           X_GEN_TAC `f:real^3#real^3->bool` THEN
 243             ASM_CASES_TAC `f IN face_set_of_fan (V,ESTD V)` THEN ASM_REWRITE_TAC[] THEN
 244             EXPAND_TAC "g" THEN
 245               MATCH_MP_TAC tauVEF_alt2 THEN
 246             ASM_REWRITE_TAC[];
 247           ALL_TAC
 248         ] THEN
 249
 250         MP_TAC (ISPECL [`(\x. g x):(real^3#real^3->bool)->real`; `face_set_of_fan (V,ESTD V)`] SUM_RESTRICT) THEN
 251         ASM_REWRITE_TAC[] THEN
 252         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 253         POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 254
 255         ASM_SIMP_TAC[SUM_SUB; SUM_RMUL; SUM_LMUL] THEN
 256         ASM_SIMP_TAC[HRXEFDM_lemma1] THEN
 257         REAL_ARITH_TAC;
 258       ALL_TAC
 259     ] THEN
 260
 261     POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 262     ASSUME_TAC PI_POS THEN
 263
 264     ASM_SIMP_TAC[REAL_FIELD `&0 < pi ==> &4 * pi * (&1 + sol0 / pi) = &4 * pi + &4 * sol0`] THEN
 265     ASM_SIMP_TAC[REAL_FIELD `&0 < pi ==> sol0 / pi * &2 * pi * a = &2 * a * sol0`] THEN
 266     REWRITE_TAC[REAL_ARITH `(&4 * pi + &4 * a) - (&2 * b * a) = (&4 * pi - &20 * a) + &2 * a * (&12 - b)`] THEN
 267     REWRITE_TAC[REAL_ARITH `a + b < a <=> b < &0`] THEN
 268     ONCE_REWRITE_TAC[REAL_ARITH `&0 = (&2 * sol0) * &0`] THEN
 269     REWRITE_TAC[REAL_MUL_ASSOC] THEN
 270     MATCH_MP_TAC REAL_LT_LMUL THEN
 271     CONJ_TAC THENL
 272     [
 273       MATCH_MP_TAC REAL_LT_MUL THEN
 274         REWRITE_TAC[REAL_ARITH `&0 < &2`; sol0_POS];
 275       ALL_TAC
 276     ] THEN
 277
 278     REWRITE_TAC[REAL_ARITH `a - b < &0 <=> b > a`] THEN
 279     FIRST_X_ASSUM (MP_TAC o check (fun th -> rator (concl th) = `contravening`)) THEN
 280     SIMP_TAC[contravening]);;
 281
 282
 283
 284 end;;