text_formalization/local/XIVPHKS.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (* Section: Appendix                                                          *)\r
   4 (* Chapter: Local Fan                                                         *)\r
   5 (* Author: John Harrison                                                      *)\r
   6 (* Date: 2013-06-11                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 module Xivphks = struct \r
  10 \r
  11   open Hales_tactic;;\r
  12 \r
  13 (* ------------------------------------------------------------------------- *)\r
  14 (* Lemma 7.141                                                               *)\r
  15 (* ------------------------------------------------------------------------- *)\r
  16 \r
  17 let FSQKWKK = prove\r
  18  (`!v0 v1 v2 v3.\r
  19         azim v0 v1 v2 v3 <= pi ==> azim v0 v2 v3 v1 <= pi`,\r
  20   GEOM_ORIGIN_TAC `v0:real^3` THEN\r
  21   REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT] THEN\r
  22   REWRITE_TAC[GSYM REAL_NOT_LT; Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN\r
  23   MESON_TAC[CROSS_TRIPLE]);;\r
  24 \r
  25 (* ------------------------------------------------------------------------- *)\r
  26 (* Lemma 7.143.                                                              *)\r
  27 (* ------------------------------------------------------------------------- *)\r
  28 \r
  29 let XIVPHKS = prove\r
  30  (`!W a d e n r w.\r
  31         1 <= n /\ n - 1 = r /\\r
  32         pairwise (\i j. ~collinear{vec 0,w i,w j}) (0..n) /\\r
  33         (\(i,j,k). dihV (vec 0) (w i) (w j) (w k)) = d /\\r
  34         (\(i,j,k). azim (vec 0) (w i) (w j) (w k)) = a /\\r
  35         (\i. wedge_ge (vec 0) (w i) (w(i + 1)) (w(i - 1))) = W /\\r
  36         &0 < &2 * e /\\r
  37         (!i. i IN 1..r ==> &2 * e < a(i,i + 1,i - 1)) /\\r
  38         (!i. i IN 1..r ==> a(i,i + 1,i - 1) <= pi) /\\r
  39         (!p q. {p,q,q+1} SUBSET 0..r /\ ~(p = q) /\ ~(p = q + 1)\r
  40                ==> d(p,q,q + 1) < e) /\\r
  41         (!p q. {p,p+1,q} SUBSET 0..r /\ q > p + 1\r
  42                ==> d(p,p + 1,q) < e) /\\r
  43         (!p q. {p+1,p,q} SUBSET 0..r /\ q < p\r
  44                ==> d(p + 1,p,q) < e)\r
  45         ==> (!k j. j + k <= r ==> w j IN W(j + k)) /\\r
  46             (!k j. 1 <= j /\ j + k <= r ==> w(j + k) IN W(j))`,\r
  47   REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `&0 < &2 * e <=> &0 < e`] THEN\r
  48   REWRITE_TAC[IN_NUMSEG; GT; pairwise; LE_0] THEN STRIP_TAC THEN\r
  49   REWRITE_TAC[AND_FORALL_THM; TAUT\r
  50    `(p ==> r) /\ (q /\ p ==> s) <=> p ==> r /\ (q ==> s)`] THEN\r
  51   INDUCT_TAC THENL\r
  52    [REWRITE_TAC[ADD_CLAUSES; SUB_0] THEN\r
  53     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN\r
  54     REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim; REAL_LE_REFL];\r
  55     ALL_TAC] THEN\r
  56   ASM_CASES_TAC `k = 0` THENL\r
  57    [ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1] THEN\r
  58     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN\r
  59     REWRITE_TAC[ADD_SUB; azim; REAL_LE_REFL; AZIM_REFL];\r
  60     ALL_TAC] THEN\r
  61   DISJ_CASES_TAC(ARITH_RULE `r <= 1 \/ 2 <= r`) THENL\r
  62    [ASM_ARITH_TAC; ALL_TAC] THEN\r
  63   SUBGOAL_THEN `&2 * e < &2 * pi` ASSUME_TAC THENL\r
  64    [MATCH_MP_TAC REAL_LT_TRANS THEN\r
  65     EXISTS_TAC `a(1,1 + 1,1 - 1):real` THEN CONJ_TAC THENL\r
  66      [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
  67       EXPAND_TAC "a" THEN REWRITE_TAC[azim]];\r
  68     ALL_TAC] THEN\r
  69   REWRITE_TAC[ADD1] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN\r
  70   MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC THENL\r
  71    [DISCH_TAC THEN UNDISCH_THEN\r
  72      `!j. j + k <= r\r
  73           ==> (w:num->real^3) j IN W (j + k) /\ (1 <= j ==> w (j + k) IN W j)`\r
  74      (MP_TAC o SPEC `j:num`) THEN\r
  75     ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_ARITH_TAC; STRIP_TAC] THEN\r
  76     SUBGOAL_THEN\r
  77      `a(j + k,j + k + 1,j) <= a(j + k,j + k + 1,j + k - 1)`\r
  78     ASSUME_TAC THENL\r
  79      [UNDISCH_TAC `(w:num->real^3) j IN W (j + k)` THEN\r
  80       MAP_EVERY EXPAND_TAC ["W"; "a"] THEN\r
  81       REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN\r
  82       DISCH_THEN(MP_TAC o CONJUNCT2) THEN MATCH_MP_TAC EQ_IMP THEN\r
  83       REPEAT(BINOP_TAC THEN REWRITE_TAC[]) THEN AP_TERM_TAC THEN ASM_ARITH_TAC;\r
  84       ALL_TAC] THEN\r
  85     SUBGOAL_THEN `a(j + k,j + k + 1,j + k - 1) <= pi` ASSUME_TAC THENL\r
  86      [ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> j + k - 1 = (j + k) - 1`] THEN\r
  87       REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
  88       ALL_TAC] THEN\r
  89     SUBGOAL_THEN `a(j,j + k,j + k + 1) <= pi` ASSUME_TAC THENL\r
  90      [SUBGOAL_THEN `a (j + k,j + k + 1,j) <= pi` MP_TAC THENL\r
  91        [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]] THEN\r
  92       MESON_TAC[FSQKWKK];\r
  93       ALL_TAC] THEN\r
  94     SUBGOAL_THEN `a(j,j + k,j + k + 1) < e` ASSUME_TAC THENL\r
  95      [SUBGOAL_THEN `a(j,j + k,j + k + 1):real = d(j,j + k,j + k + 1)`\r
  96       SUBST1_TAC THENL\r
  97        [UNDISCH_TAC `a (j,j + k,j + k + 1) <= pi` THEN\r
  98         MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN\r
  99         MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN\r
 100         CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 101         REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 102         REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC];\r
 103       ALL_TAC] THEN\r
 104     SUBGOAL_THEN `a(j,j + 1,j + k) <= a(j,j + 1,j - 1)` ASSUME_TAC THENL\r
 105      [UNDISCH_TAC `(w:num->real^3) (j + k) IN W j` THEN\r
 106       MAP_EVERY EXPAND_TAC ["W"; "a"] THEN\r
 107       SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM];\r
 108       ALL_TAC] THEN\r
 109     SUBGOAL_THEN `a(j,j + 1,j - 1) <= pi` ASSUME_TAC THENL\r
 110      [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN\r
 111     SUBGOAL_THEN `a(j,j + 1,j + k) <= pi` ASSUME_TAC THENL\r
 112      [ASM_REAL_ARITH_TAC; ALL_TAC] THEN\r
 113     SUBGOAL_THEN `a(j,j + 1,j + k) < e` ASSUME_TAC THENL\r
 114      [ASM_CASES_TAC `k = 1` THENL\r
 115        [EXPAND_TAC "a" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[AZIM_REFL];\r
 116         ALL_TAC] THEN\r
 117       SUBGOAL_THEN `a(j,j + 1,j + k):real = d(j,j + 1,j + k)`\r
 118       SUBST1_TAC THENL\r
 119        [UNDISCH_TAC `a (j,j + 1,j + k) <= pi` THEN\r
 120         MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN\r
 121         MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN\r
 122         CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 123         FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 124         REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN\r
 125         ASM_ARITH_TAC];\r
 126       ALL_TAC] THEN\r
 127     SUBGOAL_THEN `a(j,j + 1,j + k + 1):real <= a(j,j + 1,j - 1)`\r
 128     MP_TAC THENL\r
 129      [MATCH_MP_TAC REAL_LE_TRANS THEN\r
 130       EXISTS_TAC `a(j,j + 1,j + k) + a(j,j + k,j + k + 1)` THEN CONJ_TAC THENL\r
 131        [MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC\r
 132          [`a (j,j + k,j + k + 1):real < e`; `a (j,j + 1,j + k):real < e`] THEN\r
 133         EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN\r
 134         MATCH_MP_TAC Fan.sum3_azim_fan THEN\r
 135         CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN\r
 136         REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 137         ALL_TAC] THEN\r
 138       MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC THENL\r
 139        [ASM_REAL_ARITH_TAC; MATCH_MP_TAC REAL_LT_IMP_LE] THEN\r
 140       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 141       EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN\r
 142       EXPAND_TAC "a" THEN REWRITE_TAC[azim]];\r
 143     ALL_TAC] THEN\r
 144   DISCH_TAC THEN\r
 145   UNDISCH_THEN\r
 146    `!j. j + k <= r\r
 147         ==> (w:num->real^3) j IN W (j + k) /\ (1 <= j ==> w (j + k) IN W j)`\r
 148    (MP_TAC o SPEC `j + 1`) THEN\r
 149   ASM_REWRITE_TAC[ARITH_RULE `(j + 1) + k = j + k + 1`;\r
 150                   ARITH_RULE `1 <= j + 1`] THEN\r
 151   STRIP_TAC THEN\r
 152   SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` ASSUME_TAC THENL\r
 153    [UNDISCH_TAC `(w:num->real^3) (j + k + 1) IN W (j + 1)` THEN\r
 154     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN\r
 155     EXPAND_TAC "a" THEN SIMP_TAC[ARITH_RULE `(a + 1) + 1 = a + 2`; ADD_SUB];\r
 156     ALL_TAC] THEN\r
 157   SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) + a(j + 1,j + k + 1,j) =\r
 158                 a(j + 1,j + 2,j)`\r
 159   ASSUME_TAC THENL\r
 160    [CONV_TAC SYM_CONV THEN\r
 161     UNDISCH_TAC `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` THEN\r
 162     EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC THEN\r
 163     MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[] THEN\r
 164     REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 165     ALL_TAC] THEN\r
 166   SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= a(j + 1,j + 2,j)` ASSUME_TAC THENL\r
 167    [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH\r
 168      `a + b = c ==> &0 <= a ==> b <= c`)) THEN\r
 169     EXPAND_TAC "a" THEN REWRITE_TAC[azim];\r
 170     ALL_TAC] THEN\r
 171   SUBGOAL_THEN `a(j + 1,(j + 1) + 1,(j + 1) - 1) <= pi` MP_TAC THENL\r
 172    [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 173     REWRITE_TAC[ADD_SUB; ARITH_RULE `(n + 1) + 1 = n + 2`] THEN\r
 174     DISCH_TAC] THEN\r
 175   SUBGOAL_THEN `a(j + k + 1,j,j + 1) <= pi` ASSUME_TAC THENL\r
 176    [SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= pi` MP_TAC THENL\r
 177      [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]] THEN\r
 178     MESON_TAC[FSQKWKK];\r
 179     ALL_TAC] THEN\r
 180   SUBGOAL_THEN `a(j + k + 1,j,j + 1) < e` ASSUME_TAC THENL\r
 181    [SUBGOAL_THEN `a(j + k + 1,j,j + 1):real = d(j + k + 1,j,j + 1) `\r
 182     SUBST1_TAC THENL\r
 183      [UNDISCH_TAC `a(j + k + 1,j,j + 1) <= pi` THEN\r
 184       MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN\r
 185       MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN\r
 186       CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 187       REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 188       REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC];\r
 189     ALL_TAC] THEN\r
 190   SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)`\r
 191   ASSUME_TAC THENL\r
 192    [UNDISCH_TAC `(w:num->real^3)(j + 1) IN W (j + k + 1)` THEN\r
 193     MAP_EVERY EXPAND_TAC ["W"; "a"] THEN\r
 194     SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM;\r
 195              ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;\r
 196              ARITH_RULE `(j + k + 1) - 1 = j + k`];\r
 197     ALL_TAC] THEN\r
 198   SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) + a(j + k + 1,j + 1,j + k) =\r
 199                 a(j + k + 1,j + k + 2,j + k)`\r
 200   ASSUME_TAC THENL\r
 201    [CONV_TAC SYM_CONV THEN UNDISCH_TAC\r
 202      `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` THEN\r
 203     EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC THEN\r
 204     MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[] THEN\r
 205     REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 206     ALL_TAC] THEN\r
 207   SUBGOAL_THEN `a(j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1) <= pi`\r
 208   MP_TAC THENL\r
 209    [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 210     REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;\r
 211              ARITH_RULE `(j + k + 1) - 1 = j + k`] THEN\r
 212     DISCH_TAC] THEN\r
 213   SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= a(j + k + 1,j + k + 2,j + k)`\r
 214   ASSUME_TAC THENL\r
 215    [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH\r
 216      `a + b = c ==> &0 <= a ==> b <= c`)) THEN\r
 217     EXPAND_TAC "a" THEN REWRITE_TAC[azim];\r
 218     ALL_TAC] THEN\r
 219   SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= pi` ASSUME_TAC THENL\r
 220    [ASM_REAL_ARITH_TAC; ALL_TAC] THEN\r
 221   SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) < e` ASSUME_TAC THENL\r
 222    [ASM_CASES_TAC `k = 1` THENL\r
 223      [ASM_REWRITE_TAC[] THEN EXPAND_TAC "a" THEN REWRITE_TAC[AZIM_REFL] THEN\r
 224       ASM_REWRITE_TAC[];\r
 225       ALL_TAC] THEN\r
 226     SUBGOAL_THEN `a(j + k + 1,j + 1,j + k):real = d(j + k + 1,j + 1,j + k)`\r
 227     SUBST1_TAC THENL\r
 228      [UNDISCH_TAC `a(j + k + 1,j + 1,j + k) <= pi` THEN\r
 229       MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN\r
 230       MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN\r
 231       CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 232       ALL_TAC] THEN\r
 233     SUBGOAL_THEN `d((j + k) + 1,j + k,j + 1) < e` MP_TAC THENL\r
 234      [FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 235       REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC;\r
 236       EXPAND_TAC "d" THEN REWRITE_TAC[ADD_ASSOC; Counting_spheres.DIHV_SYM]];\r
 237     ALL_TAC] THEN\r
 238   SUBGOAL_THEN `a(j + k + 1,j + k + 2,j) <= a(j + k + 1,j + k + 2,j + k)`\r
 239   MP_TAC THENL\r
 240    [ALL_TAC;\r
 241     MAP_EVERY EXPAND_TAC ["W"; "a"] THEN\r
 242     SIMP_TAC[Localization.wedge_ge; azim; IN_ELIM_THM;\r
 243              ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;\r
 244              ARITH_RULE `(j + k + 1) - 1 = j + k`]] THEN\r
 245   MATCH_MP_TAC REAL_LE_TRANS THEN\r
 246   EXISTS_TAC `a(j + k + 1,j + k + 2,j) + a(j + k + 1,j,j + k)` THEN\r
 247   CONJ_TAC THENL\r
 248    [REWRITE_TAC[REAL_LE_ADDR] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim];\r
 249     ALL_TAC] THEN\r
 250   MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN\r
 251   EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN\r
 252   MATCH_MP_TAC Fan.sum5_azim_fan THEN CONJ_TAC THENL\r
 253    [ALL_TAC;\r
 254     REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC] THEN\r
 255   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC THENL\r
 256    [MATCH_MP_TAC REAL_LE_TRANS THEN\r
 257     EXISTS_TAC `a(j + k + 1,j,j + 1) + a(j + k + 1,j + 1,j + k)` THEN\r
 258     CONJ_TAC THENL\r
 259      [MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC\r
 260        [`a(j + k + 1,j,j + 1):real < e`;\r
 261         `a(j + k + 1,j + 1,j + k):real < e`] THEN\r
 262       EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN\r
 263       MATCH_MP_TAC Fan.sum3_azim_fan THEN\r
 264       CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN\r
 265       REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 266       ASM_REAL_ARITH_TAC];\r
 267     SUBGOAL_THEN\r
 268      `&2 * e < a (j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1)`\r
 269     MP_TAC THENL\r
 270      [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;\r
 271       EXPAND_TAC "a" THEN\r
 272       REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;\r
 273                   ARITH_RULE `(j + k + 1) - 1 = j + k`] THEN\r
 274       REAL_ARITH_TAC]]);;\r
 275 \r
 276 (* 1..r are the straight angles. Modified from Xivphks.XIVPHKS by shifting indices. *)\r
 277 \r
 278 let XIVPHKS_SHIFT = prove_by_refinement(\r
 279   `!W a d e r w.\r
 280             pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\\r
 281             pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\\r
 282             (\(i,j,k). dihV (vec 0) (w i) (w j) (w k)) = d /\\r
 283             (\(i,j,k). azim (vec 0) (w i) (w j) (w k)) = a /\\r
 284             (\i. wedge_ge (vec 0) (w i) (w (i + 1)) (w (i - 1))) = W /\\r
 285             &0 < &2 * e /\\r
 286             (!i. i IN 1..(r+1) ==> &2 * e < a (i,i + 1,i - 1)) /\\r
 287             (!i. i IN 1..(r+1) ==> a (i,i + 1,i - 1) <= pi) /\\r
 288             (!p q.\r
 289                  {p, q, q + 1} SUBSET 1..(r+1) /\ ~(p = q) /\ ~(p = q + 1)\r
 290                  ==> d (p,q,q + 1) < e) /\\r
 291             (!p q.\r
 292                  {p, p + 1, q} SUBSET 1..(r+1) /\ q > p + 1 ==> d (p,p + 1,q) < e) /\\r
 293             (!p q. {p + 1, p, q} SUBSET 1..(r+1) /\ q < p ==> d (p + 1,p,q) < e)\r
 294             ==> (!k j. 1 <= j /\ j + k <= r+1 ==> w j IN W (j + k)) /\ \r
 295                 (!k j. 1 <= j /\ j + k <= r+1 ==> w (j + k) IN W j)`,\r
 296   (* {{{ proof *)\r
 297   [\r
 298   REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `&0 < &2 * e <=> &0 < e`];\r
 299   REWRITE_TAC[IN_NUMSEG; GT; pairwise; LE_0] THEN STRIP_TAC;\r
 300   REWRITE_TAC[AND_FORALL_THM; TAUT `(p ==> r) /\ (q /\ p ==> s) <=> p ==> r /\ (q ==> s)`];\r
 301   INDUCT_TAC;\r
 302     REWRITE_TAC[ADD_CLAUSES; SUB_0];\r
 303     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];\r
 304     BY(REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim; REAL_LE_REFL]);\r
 305   ASM_CASES_TAC `k = 0`;\r
 306     ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1];\r
 307     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];\r
 308     BY(REWRITE_TAC[ADD_SUB; azim; REAL_LE_REFL; AZIM_REFL]);\r
 309   SUBGOAL_THEN `&2 * e < &2 * pi` ASSUME_TAC;\r
 310     MATCH_MP_TAC REAL_LT_TRANS;\r
 311     EXISTS_TAC `a(1,1 + 1,1 - 1):real` THEN CONJ_TAC;\r
 312       BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 313     BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);\r
 314   REWRITE_TAC[ADD1] THEN X_GEN_TAC `j:num`;\r
 315   MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC;\r
 316     DISCH_TAC;\r
 317     FIRST_X_ASSUM (C INTRO_TAC [`j`]);\r
 318     REPEAT WEAKER_STRIP_TAC;\r
 319     FIRST_X_ASSUM MP_TAC THEN ANTS_TAC;\r
 320       BY(ASM_ARITH_TAC);\r
 321     DISCH_TAC;\r
 322     FIRST_X_ASSUM_ST `==>` MP_TAC THEN ANTS_TAC;\r
 323       BY(ASM_ARITH_TAC);\r
 324     DISCH_TAC;\r
 325     SUBGOAL_THEN `a(j + k,j + k + 1,j) <= a(j + k,j + k + 1,j + k - 1)` ASSUME_TAC;\r
 326       FIRST_X_ASSUM MP_TAC THEN MAP_EVERY EXPAND_TAC ["W"; "a"];\r
 327       REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];\r
 328       DISCH_THEN(MP_TAC o CONJUNCT2) THEN MATCH_MP_TAC EQ_IMP;\r
 329       BY(REPEAT(BINOP_TAC THEN REWRITE_TAC[]) THEN AP_TERM_TAC THEN ASM_ARITH_TAC);\r
 330     SUBGOAL_THEN `a(j + k,j + k + 1,j + k - 1) <= pi` ASSUME_TAC;\r
 331       ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> j + k - 1 = (j + k) - 1`];\r
 332       BY(REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 333     SUBGOAL_THEN `a(j,j + k,j + k + 1) <= pi` ASSUME_TAC;\r
 334       SUBGOAL_THEN `a (j + k,j + k + 1,j) <= pi` MP_TAC THENL [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]];\r
 335       BY(MESON_TAC[FSQKWKK]);\r
 336     SUBGOAL_THEN `a(j,j + k,j + k + 1) < e` ASSUME_TAC;\r
 337       SUBGOAL_THEN `a(j,j + k,j + k + 1):real = d(j,j + k,j + k + 1)` SUBST1_TAC;\r
 338         UNDISCH_TAC `a (j,j + k,j + k + 1) <= pi`;\r
 339         MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;\r
 340         MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];\r
 341         BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 342       REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC;\r
 343       REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG];\r
 344       BY(ASM_ARITH_TAC);\r
 345     SUBGOAL_THEN `a(j,j + 1,j + k) <= a(j,j + 1,j - 1)` ASSUME_TAC;\r
 346       UNDISCH_TAC `(w:num->real^3) (j + k) IN W j`;\r
 347       MAP_EVERY EXPAND_TAC ["W"; "a"];\r
 348       BY(SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM]);\r
 349     SUBGOAL_THEN `a(j,j + 1,j - 1) <= pi` ASSUME_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC];\r
 350     SUBGOAL_THEN `a(j,j + 1,j + k) <= pi` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC];\r
 351     SUBGOAL_THEN `a(j,j + 1,j + k) < e` ASSUME_TAC;\r
 352       ASM_CASES_TAC `k=1`;\r
 353         BY(EXPAND_TAC "a" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[AZIM_REFL]);\r
 354       SUBGOAL_THEN `a(j,j + 1,j + k):real = d(j,j + 1,j + k)` SUBST1_TAC;\r
 355         UNDISCH_TAC `a (j,j + 1,j + k) <= pi`;\r
 356         MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;\r
 357         MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];\r
 358         BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 359       FIRST_X_ASSUM MATCH_MP_TAC;\r
 360       REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG];\r
 361       BY(ASM_ARITH_TAC);\r
 362     SUBGOAL_THEN `a(j,j + 1,j + k + 1):real <= a(j,j + 1,j - 1)` MP_TAC;\r
 363       MATCH_MP_TAC REAL_LE_TRANS;\r
 364       EXISTS_TAC `a(j,j + 1,j + k) + a(j,j + k,j + k + 1)` THEN CONJ_TAC;\r
 365         MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a (j,j + k,j + k + 1):real < e`; `a (j,j + 1,j + k):real < e`];\r
 366         EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;\r
 367         MATCH_MP_TAC Fan.sum3_azim_fan;\r
 368         CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC];\r
 369         BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 370       MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC;\r
 371         BY(ASM_REAL_ARITH_TAC);\r
 372       MATCH_MP_TAC REAL_LT_IMP_LE;\r
 373       BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 374     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];\r
 375     BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);\r
 376   DISCH_TAC;\r
 377   COMMENT "midpoint -- down to 1 goal";\r
 378   DISCH_TAC;\r
 379   FIRST_X_ASSUM (C INTRO_TAC [`j+1`]);\r
 380   ASM_REWRITE_TAC[arith `1 <= j+1`;arith `(j + 1) + k = j + k + 1`;];\r
 381   REPEAT WEAKER_STRIP_TAC;\r
 382   SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` ASSUME_TAC;\r
 383     UNDISCH_TAC `(w:num->real^3) (j + k + 1) IN W (j + 1)`;\r
 384     EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];\r
 385     BY(EXPAND_TAC "a" THEN SIMP_TAC[ARITH_RULE `(a + 1) + 1 = a + 2`; ADD_SUB]);\r
 386   SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) + a(j + 1,j + k + 1,j) =                a(j + 1,j + 2,j)` ASSUME_TAC;\r
 387     CONV_TAC SYM_CONV;\r
 388     UNDISCH_TAC `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)`;\r
 389     EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC;\r
 390     MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[];\r
 391     TYPIFY_GOAL_THEN `~collinear {vec 0, w (j + 1), w j}` (unlist REWRITE_TAC);\r
 392       FIRST_X_ASSUM_ST `collinear` kill;\r
 393       BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 394     BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN TRY ASM_ARITH_TAC);\r
 395   SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= a(j + 1,j + 2,j)` ASSUME_TAC;\r
 396     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`));\r
 397     BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);\r
 398   SUBGOAL_THEN `a(j + 1,(j + 1) + 1,(j + 1) - 1) <= pi` MP_TAC;\r
 399     BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 400   REWRITE_TAC[ADD_SUB; ARITH_RULE `(n + 1) + 1 = n + 2`];\r
 401   DISCH_TAC;\r
 402   SUBGOAL_THEN `a(j + k + 1,j,j + 1) <= pi` ASSUME_TAC;\r
 403     SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= pi` MP_TAC;\r
 404       BY(ASM_REAL_ARITH_TAC);\r
 405     EXPAND_TAC "a" THEN REWRITE_TAC[];\r
 406     BY(MESON_TAC[FSQKWKK]);\r
 407   SUBGOAL_THEN `a(j + k + 1,j,j + 1) < e` ASSUME_TAC;\r
 408     ASM_CASES_TAC `k = 0`;\r
 409       BY(EXPAND_TAC "a" THEN ASM_REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE;arith `j + 0 + 1 = j+1`]);\r
 410     SUBGOAL_THEN `a(j + k + 1,j,j + 1):real = d(j + k + 1,j,j + 1) ` SUBST1_TAC;\r
 411       UNDISCH_TAC `a(j + k + 1,j,j + 1) <= pi`;\r
 412       MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;\r
 413       MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];\r
 414       BY(CONJ_TAC THENL [FIRST_X_ASSUM_ST `collinear` kill;ALL_TAC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 415     REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC;\r
 416     BY(REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC);\r
 417   SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC;\r
 418     UNDISCH_TAC `(w:num->real^3)(j + 1) IN W (j + k + 1)`;\r
 419     MAP_EVERY EXPAND_TAC ["W"; "a"];\r
 420     BY(SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]);\r
 421   SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) + a(j + k + 1,j + 1,j + k) =                a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC;\r
 422     CONV_TAC SYM_CONV;\r
 423     UNDISCH_TAC `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)`;\r
 424     EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC;\r
 425     MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[];\r
 426     BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 427   COMMENT "ok";\r
 428   ASM_CASES_TAC `k = 0`;\r
 429     ASM_REWRITE_TAC[arith `j+0+1 = j+1`];\r
 430     EXPAND_TAC "W" THEN REWRITE_TAC[];\r
 431     ASM_SIMP_TAC[arith `1 <= j ==> (j+1)+1 = j+2 /\ (j+1)-1 = j`];\r
 432     BY(REWRITE_TAC[Local_lemmas1.FST_LST_IN_WEDGE_GE]);\r
 433   SUBGOAL_THEN `a(j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1) <= pi` MP_TAC;\r
 434     BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 435   REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`];\r
 436   DISCH_TAC;\r
 437   SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC;\r
 438     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`));\r
 439     BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);\r
 440   SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= pi` ASSUME_TAC;\r
 441     BY(ASM_REAL_ARITH_TAC);\r
 442   SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) < e` ASSUME_TAC;\r
 443     ASM_CASES_TAC `k = 1`;\r
 444       ASM_REWRITE_TAC[] THEN EXPAND_TAC "a" THEN REWRITE_TAC[AZIM_REFL];\r
 445       BY(ASM_REWRITE_TAC[]);\r
 446     SUBGOAL_THEN `a(j + k + 1,j + 1,j + k):real = d(j + k + 1,j + 1,j + k)` SUBST1_TAC;\r
 447       UNDISCH_TAC `a(j + k + 1,j + 1,j + k) <= pi`;\r
 448       MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;\r
 449       MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];\r
 450       BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 451     SUBGOAL_THEN `d((j + k) + 1,j + k,j + 1) < e` MP_TAC;\r
 452       FIRST_X_ASSUM MATCH_MP_TAC;\r
 453       BY(REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC);\r
 454     BY(EXPAND_TAC "d" THEN REWRITE_TAC[ADD_ASSOC; Counting_spheres.DIHV_SYM]);\r
 455   COMMENT "ok";\r
 456   ENOUGH_TO_SHOW_TAC `a(j + k + 1,j + k + 2,j) <= a(j + k + 1,j + k + 2,j + k)`;\r
 457     MAP_EVERY EXPAND_TAC ["W"; "a"];\r
 458     BY(SIMP_TAC[Localization.wedge_ge; azim; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]);\r
 459   MATCH_MP_TAC REAL_LE_TRANS;\r
 460   EXISTS_TAC `a(j + k + 1,j + k + 2,j) + a(j + k + 1,j,j + k)`;\r
 461   CONJ_TAC;\r
 462     BY(REWRITE_TAC[REAL_LE_ADDR] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]);\r
 463   MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV;\r
 464   EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;\r
 465   MATCH_MP_TAC Fan.sum5_azim_fan;\r
 466   CONJ2_TAC;\r
 467     BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 468   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC;\r
 469     MATCH_MP_TAC REAL_LE_TRANS;\r
 470     EXISTS_TAC `a(j + k + 1,j,j + 1) + a(j + k + 1,j + 1,j + k)`;\r
 471     CONJ_TAC;\r
 472       MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a(j + k + 1,j,j + 1):real < e`; `a(j + k + 1,j + 1,j + k):real < e`];\r
 473       EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;\r
 474       MATCH_MP_TAC Fan.sum3_azim_fan;\r
 475       CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC];\r
 476       BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 477     BY(ASM_REAL_ARITH_TAC);\r
 478   SUBGOAL_THEN `&2 * e < a (j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1)` MP_TAC;\r
 479     BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);\r
 480   EXPAND_TAC "a";\r
 481   REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`];\r
 482   BY(REAL_ARITH_TAC)\r
 483   ]);;\r
 484   (* }}} *)\r
 485 \r
 486 \r
 487 end;;\r