text_formalization/tame/CDTETAT.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Contains proofs of CDTETAT and SZIPOAS                                     *)
   4 (* ========================================================================== *)
   5
   6
   7 flyspeck_needs "tame/TameGeneral.hl";;
   8 flyspeck_needs "tame/ssreflect/tame_lemmas-compiled.hl";;
   9
  10
  11
  12 module Cdtetat_tame = struct
  13
  14
  15 open Hypermap_and_fan;;
  16 open Fan_defs;;
  17 open Tame_defs;;
  18 open Tame_general;;
  19 open Tame_lemmas;;
  20
  21
  22
  23 (* This approximation of pi is sufficient for the next lemma *)
  24 let PI_APPROX_4 = prove(`#3.1415 <= pi /\ pi <= #3.1416`,
  25    MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;
  26
  27
  28
  29 (* This lemma is a part of the proof of CDTETAT *)
  30 let CDTETAT_lemma1 = prove(`!p t:num. &p * (#0.852) + &t * (#1.15) <= &2 * pi /\ &2 * pi < &p * #1.9 + &t * pi ==>
  31   (p, t) IN  { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4),
  32              (2,1), (2,2), (2,3), (3,1), (3,2), (3,3),
  33              (4,0), (4,1),(4,2), (5,0), (5,1),
  34              (6,0), (6,1), (7,0)  }`,
  35    REPEAT STRIP_TAC THEN
  36      SUBGOAL_THEN `p <= 7` ASSUME_TAC THENL
  37      [
  38        REMOVE_ASSUM THEN
  39          POP_ASSUM (MP_TAC o (fun th -> MATCH_MP (REAL_ARITH `&p * #0.852 + &t * #1.15 <= &2 * pi ==> &p <= (&2 * pi) / #0.852`) th)) THEN
  40          DISCH_TAC THEN
  41          SUBGOAL_THEN `p < 8` (fun th -> MP_TAC th THEN ARITH_TAC) THEN
  42          REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
  43          POP_ASSUM MP_TAC THEN MP_TAC PI_APPROX_4 THEN
  44          REAL_ARITH_TAC;
  45        ALL_TAC
  46      ] THEN
  47
  48      SUBGOAL_THEN `&t <= (&2 * #3.1416 - &p * #0.852) / #1.15` MP_TAC THENL
  49      [
  50        REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
  51          MP_TAC PI_APPROX_4 THEN
  52          REAL_ARITH_TAC;
  53        ALL_TAC
  54      ] THEN
  55
  56      SUBGOAL_THEN `&2 - (&p * #1.9) / pi < &t` MP_TAC THENL
  57      [
  58        MP_TAC (REAL_FIELD `&0 < pi ==> &2 - (&p * #1.9) / pi = (&2 * pi - &p * #1.9) / pi`) THEN
  59          SUBGOAL_TAC "A" `&0 < pi` [ MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC ] THEN
  60          ASM_REWRITE_TAC[] THEN
  61          DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
  62          ASM_SIMP_TAC[REAL_LT_LDIV_EQ] THEN
  63          REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
  64          REAL_ARITH_TAC;
  65        ALL_TAC
  66      ] THEN
  67      POP_ASSUM MP_TAC THEN
  68      REMOVE_ASSUM THEN REMOVE_ASSUM THEN
  69      DISCH_TAC THEN DISCH_TAC THEN
  70
  71      SUBGOAL_THEN `&2 - (&p * #1.9) / #3.1415 < &t` MP_TAC THENL
  72      [
  73        MATCH_MP_TAC REAL_LET_TRANS THEN
  74          EXISTS_TAC `&2 - (&p * #1.9) / pi` THEN
  75          ASM_REWRITE_TAC[REAL_ARITH `a - b <= a - c <=> c <= b`] THEN
  76          REWRITE_TAC[real_div] THEN
  77          MATCH_MP_TAC REAL_LE_LMUL THEN
  78          REWRITE_TAC[REAL_ARITH `&0 <= &p * #1.9`] THEN
  79          MATCH_MP_TAC REAL_LE_INV2 THEN
  80          MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC;
  81        ALL_TAC
  82      ] THEN
  83      REMOVE_ASSUM THEN
  84      DISCH_THEN (LABEL_TAC "A") THEN DISCH_THEN (LABEL_TAC "B") THEN
  85
  86      DISJ_CASES_TAC (ARITH_RULE `7 < p \/ p < 8`) THENL
  87      [
  88        ASM_MESON_TAC[NOT_LE];
  89        ALL_TAC
  90      ] THEN
  91      POP_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[gen_NUM_CASES 8] th)) THEN
  92
  93      POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  94      POP_ASSUM (fun th -> SUBST_ALL_TAC th) THEN
  95      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
  96      CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT STRIP_TAC THENL
  97      [
  98        SUBGOAL_THEN `2 < t /\ t < 6` ASSUME_TAC THENL
  99          [
 100            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 101              POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 102              REAL_ARITH_TAC;
 103            ALL_TAC
 104          ] THEN
 105         ASM SET_TAC[ARITH_RULE `2 < t /\ t < 6 ==> t = 3 \/ t = 4 \/ t = 5`];
 106
 107        SUBGOAL_THEN `1 < t /\ t < 5` ASSUME_TAC THENL
 108          [
 109            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 110              POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 111              REAL_ARITH_TAC;
 112            ALL_TAC
 113          ] THEN
 114         ASM SET_TAC[ARITH_RULE `1 < t /\ t < 5 ==> t = 2 \/ t = 3 \/ t = 4`];
 115
 116        SUBGOAL_THEN `0 < t /\ t < 4` ASSUME_TAC THENL
 117          [
 118            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 119              POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 120              REAL_ARITH_TAC;
 121            ALL_TAC
 122          ] THEN
 123         ASM SET_TAC[ARITH_RULE `0 < t /\ t < 4 ==> t = 1 \/ t = 2 \/ t = 3`];
 124
 125        SUBGOAL_THEN `0 < t /\ t < 4` ASSUME_TAC THENL
 126          [
 127            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 128              POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 129              REAL_ARITH_TAC;
 130            ALL_TAC
 131          ] THEN
 132         ASM SET_TAC[ARITH_RULE `0 < t /\ t < 4 ==> t = 1 \/ t = 2 \/ t = 3`];
 133
 134        SUBGOAL_THEN `t < 3` ASSUME_TAC THENL
 135          [
 136            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 137              POP_ASSUM MP_TAC THEN
 138              REAL_ARITH_TAC;
 139            ALL_TAC
 140          ] THEN
 141         ASM SET_TAC[ARITH_RULE `t < 3 ==> t = 0 \/ t = 1 \/ t = 2`];
 142
 143        SUBGOAL_THEN `t < 2` ASSUME_TAC THENL
 144          [
 145            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 146              POP_ASSUM MP_TAC THEN
 147              REAL_ARITH_TAC;
 148            ALL_TAC
 149          ] THEN
 150         ASM SET_TAC[ARITH_RULE `t < 2 ==> t = 0 \/ t = 1`];
 151
 152        SUBGOAL_THEN `t < 2` ASSUME_TAC THENL
 153          [
 154            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 155              POP_ASSUM MP_TAC THEN
 156              REAL_ARITH_TAC;
 157            ALL_TAC
 158          ] THEN
 159         ASM SET_TAC[ARITH_RULE `t < 2 ==> t = 0 \/ t = 1`];
 160
 161        SUBGOAL_THEN `t < 1` ASSUME_TAC THENL
 162          [
 163            REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 164              POP_ASSUM MP_TAC THEN
 165              REAL_ARITH_TAC;
 166            ALL_TAC
 167          ] THEN
 168         ASM SET_TAC[ARITH_RULE `t < 1 ==> t = 0`]
 169      ]);;
 170
 171
 172
 173 (* CDTETAT (with assumptions) *)
 174
 175 let CDTETAT = prove(`kcblrqc_ineq_def ==> !V x. contravening V /\ x IN dart_of_fan (V,ESTD V) ==>
 176                       (let (p,q,r) = type_of_node (hypermap_of_fan (V, ESTD V)) x in
 177                          ((p,q+r) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4),
 178                                        (2,1), (2,2), (2,3), (3,1), (3,2), (3,3),
 179                                        (4,0), (4,1),(4,2), (5,0), (5,1),
 180                                        (6,0), (6,1), (7,0)  }))`,
 181  REPEAT STRIP_TAC THEN
 182    MP_TAC (ISPEC `V:real^3->bool` CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 183    MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,ESTD V)`; `x:real^3#real^3`] NODE_TYPE_lemma) THEN
 184    ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN; Jgtdebu.JGTDEBU4] THEN
 185    DISCH_THEN (fun th -> ALL_TAC) THEN
 186    CONV_TAC let_CONV THEN
 187    ABBREV_TAC `H = hypermap_of_fan (V,ESTD V)` THEN
 188    ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN
 189    ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN
 190    ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN
 191    MATCH_MP_TAC CDTETAT_lemma1 THEN
 192
 193    MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] SUM_AZIM_DART_FULLY_SURROUNDED) THEN
 194    MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN
 195
 196    ASM_SIMP_TAC[CONTRAVENING_IMP_FULLY_SURROUNDED] THEN
 197    CONV_TAC (DEPTH_CONV let_CONV) THEN
 198    ASM_REWRITE_TAC[] THEN
 199    ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN
 200
 201    DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 202    DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN
 203    STRIP_TAC THEN
 204
 205    SUBGOAL_THEN `&(CARD (B:real^3#real^3->bool) + CARD (C:real^3#real^3->bool)) = &(CARD (D:real^3#real^3->bool))` MP_TAC THENL
 206    [
 207      REWRITE_TAC[REAL_OF_NUM_EQ] THEN
 208        MATCH_MP_TAC CARD_UNION_EQ THEN
 209        ASM_SIMP_TAC[GSYM DISJOINT];
 210      ALL_TAC
 211    ] THEN
 212
 213    FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_eq o concl)) THEN
 214    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 215
 216    SUBGOAL_THEN `!y:real^3#real^3. y IN node H x ==> y IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
 217    [
 218      REWRITE_TAC[GSYM SUBSET] THEN
 219        MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] NODE_SUBSET_DART_OF_FAN) THEN
 220        ASM_REWRITE_TAC[];
 221      ALL_TAC
 222    ] THEN
 223
 224    SUBGOAL_THEN `!y. y IN A ==> azim_dart (V,ESTD V) y < #1.9 /\ #0.852 < azim_dart (V,ESTD V) y` ASSUME_TAC THENL
 225    [
 226      EXPAND_TAC "A" THEN GEN_TAC THEN
 227        REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
 228        MP_TAC TRIANGULAR_FACE_AZIM_DART_BOUNDS THEN
 229        UNDISCH_TAC `kcblrqc_ineq_def` THEN SIMP_TAC[kcblrqc_ineq_def] THEN DISCH_THEN (fun th -> ALL_TAC) THEN
 230        DISCH_THEN (MP_TAC o SPECL [`V:real^3->bool`; `y:real^3#real^3`]) THEN
 231        ASM_SIMP_TAC[REAL_ARITH `a < #1.893 ==> a < #1.9`];
 232      ALL_TAC
 233    ] THEN
 234
 235    SUBGOAL_THEN `!y. y IN D ==> azim_dart (V,ESTD V) y < pi /\ #1.15 < azim_dart (V,ESTD V) y` ASSUME_TAC THENL
 236    [
 237      EXPAND_TAC "D" THEN GEN_TAC THEN
 238        REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
 239        MP_TAC (SPEC `V:real^3->bool` non_triangular_face_azim_dart_bound) THEN ASM_REWRITE_TAC[] THEN
 240        DISCH_THEN (MP_TAC o SPEC `y:real^3#real^3`) THEN
 241        ASM_SIMP_TAC[ARITH_RULE `3 < a <=> a >= 4`] THEN
 242        MP_TAC (SPECL [`V:real^3->bool`] CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
 243        ASM_REWRITE_TAC[fully_surrounded] THEN
 244        DISCH_THEN (MP_TAC o SPEC `y:real^3#real^3`) THEN
 245        ASM_SIMP_TAC[];
 246      ALL_TAC
 247    ] THEN
 248
 249    DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 250
 251    CONJ_TAC THENL
 252    [
 253      MATCH_MP_TAC REAL_LE_ADD2 THEN
 254        ONCE_REWRITE_TAC[GSYM REAL_LE_NEG] THEN
 255        GEN_REWRITE_TAC (PAT_CONV `(\f. --sum A f <= x /\ --sum D f <= y)`) [GSYM ETA_AX] THEN
 256        REWRITE_TAC[GSYM SUM_NEG] THEN
 257        REWRITE_TAC[REAL_NEG_RMUL] THEN
 258        CONJ_TAC THEN MATCH_MP_TAC SUM_BOUND THEN ASM_SIMP_TAC[REAL_LE_NEG; REAL_LT_IMP_LE];
 259
 260      SUBGOAL_THEN `x:real^3#real^3 IN A \/ x IN D` MP_TAC THENL
 261        [
 262          REWRITE_TAC[GSYM IN_UNION] THEN
 263            FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
 264            DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 265            REWRITE_TAC[Hypermap.node_refl];
 266          ALL_TAC
 267        ] THEN
 268
 269        STRIP_TAC THENL
 270        [
 271          MATCH_MP_TAC REAL_LTE_ADD2 THEN
 272            CONJ_TAC THENL
 273            [
 274              MATCH_MP_TAC SUM_BOUND_LT THEN
 275                ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 276                EXISTS_TAC `x:real^3#real^3` THEN
 277                ASM_SIMP_TAC[];
 278              MATCH_MP_TAC SUM_BOUND THEN
 279                ASM_SIMP_TAC[REAL_LT_IMP_LE]
 280            ];
 281          ALL_TAC
 282        ] THEN
 283
 284        MATCH_MP_TAC REAL_LET_ADD2 THEN
 285        CONJ_TAC THENL
 286        [
 287          MATCH_MP_TAC SUM_BOUND THEN
 288            ASM_SIMP_TAC[REAL_LT_IMP_LE];
 289          MATCH_MP_TAC SUM_BOUND_LT THEN
 290            ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 291            EXISTS_TAC `x:real^3#real^3` THEN
 292            POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[]
 293        ]
 294    ]);;
 295
 296
 297
 298
 299
 300 (* SZIPOAS *)
 301
 302 let SZIPOAS = prove(`kcblrqc_ineq_def ==>
 303                       !V. contravening V ==> tame_11b  (hypermap_of_fan (V, ESTD V))`,
 304    REPEAT STRIP_TAC THEN REWRITE_TAC[tame_11b] THEN
 305      MP_TAC (ISPEC `V:real^3->bool` CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 306      GEN_TAC THEN
 307      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
 308      DISCH_TAC THEN
 309
 310      MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE) THEN
 311      ASM_SIMP_TAC[CONTRAVENING_IMP_FULLY_SURROUNDED; Jgtdebu.JGTDEBU4] THEN
 312      FIRST_X_ASSUM (MP_TAC o SPECL [`V:real^3->bool`; `x:real^3#real^3`] o MATCH_MP CDTETAT) THEN
 313      ASM_REWRITE_TAC[type_of_node] THEN
 314      CONV_TAC (DEPTH_CONV let_CONV) THEN
 315      ABBREV_TAC `H = hypermap_of_fan (V,ESTD(V))` THEN
 316      ABBREV_TAC `p = CARD (set_of_triangles_meeting_node H (x:real^3#real^3))` THEN
 317      ABBREV_TAC `q = CARD (set_of_quadrilaterals_meeting_node H (x:real^3#real^3))` THEN
 318      ABBREV_TAC `r = CARD (set_of_exceptional_meeting_node H (x:real^3#real^3))` THEN
 319
 320      REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; PAIR_EQ] THEN
 321      ARITH_TAC);;
 322
 323
 324 end;;