text_formalization/local/BKOSSGE.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Appendix, Main Estimate, check_completeness                       *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Lemma: BKOSSGE                                                             *)
   6 (* Author: Thomas Hales                                                       *)
   7 (* Date: 2013-08-07                                                           *)
   8 (* ========================================================================== *)
   9
  10 module Bkossge = struct
  11
  12   open Hales_tactic;;
  13
  14 let cos_bounds_0_pi = prove_by_refinement(
  15   `!z. &0 < z /\ z < pi ==> -- &1 < cos z /\ cos z < &1`,
  16   (* {{{ proof *)
  17   [
  18   REPEAT WEAKER_STRIP_TAC;
  19   TYPIFY `(&0 < z /\ z < pi / &2) \/ z = pi / &2 \/ (&0 < pi - z /\ pi - z < pi / &2)` (C SUBGOAL_THEN ASSUME_TAC);
  20     BY(ASM_TAC THEN REAL_ARITH_TAC);
  21   REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC);
  22       BY(ASM_MESON_TAC[Counting_spheres.cos_bounds_0_Pi2;arith `&0 < x ==> -- &1 < x`]);
  23     ASM_REWRITE_TAC[COS_PI2];
  24     BY(REAL_ARITH_TAC);
  25   TYPIFY `-- &1 < --cos z /\ --cos z < &1` ENOUGH_TO_SHOW_TAC;
  26     BY(REAL_ARITH_TAC);
  27   ONCE_REWRITE_TAC[GSYM COS_NEG];
  28   REWRITE_TAC[GSYM COS_PERIODIC_PI;arith `--z + pi = pi - z`];
  29   BY(ASM_MESON_TAC[Counting_spheres.cos_bounds_0_Pi2;arith `&0 < x ==> -- &1 < x`])
  30   ]);;
  31   (* }}} *)
  32
  33 let ear_acute = prove_by_refinement(
  34   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6.
  35     &2 <= y1 /\ y1 <= &2 * h0 /\
  36     &2 <= y2 /\ y2 <= &2 * h0 /\
  37     &2 <= y3 /\ y3 <= &2 * h0 /\
  38     &2 <= y4 /\ y4 <= &2 * h0 /\
  39     &2 <= y6 /\ y6 <= &2 * h0 /\
  40     &3 <= y5 /\
  41     &0 < ups_x (y1*y1) (y3*y3) (y5*y5)
  42     ==> dih_y y1 y2 y3 y4 y5 y6 < pi / &2)
  43 `,
  44   (* {{{ proof *)
  45   [
  46   REWRITE_TAC[Sphere.h0;arith `&2 * #1.26  = #2.52`;Trigonometry.IHIQXLM];
  47   REPEAT WEAKER_STRIP_TAC;
  48   INTRO_TAC (Terminal.get_main_nonlinear "2485876245a") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
  49   ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `#3.0 = &3`;];
  50   ANTS_TAC;
  51     REWRITE_TAC[arith `x <= y <=> ~(y < x)`];
  52     DISCH_TAC;
  53     FIRST_X_ASSUM_ST `&16` MP_TAC THEN REWRITE_TAC[arith `a * b * c = (a * b) * c`];
  54     REWRITE_TAC[arith `~(&0 < x * y) <=> &0 <= x * (-- y)`];
  55     REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL_EQ);
  56     REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
  57     BY(ASM_TAC THEN REAL_ARITH_TAC);
  58   REWRITE_TAC[Nonlinear_lemma.dih_x_alt;Sphere.dih_y;LET_THM;GSYM Sphere.delta_y];
  59   REWRITE_TAC[GSYM Sphere.delta4_y;GSYM Sphere.y_of_x];
  60   REWRITE_TAC[arith `pi2 + a < pi2 <=> a < &0`];
  61   DISCH_TAC;
  62   GMATCH_SIMP_TAC Tskajxy.ATN2_Y_NEG;
  63   CONJ_TAC;
  64     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  65   BY(REWRITE_TAC[arith `p - a = p + -- a`;GSYM ATN_NEG;arith `-- p + a < &0 <=> a < p`;ATN_BOUNDS])
  66   ]);;
  67   (* }}} *)
  68
  69 let quad_nonexist_849 = prove_by_refinement(
  70   `main_nonlinear_terminal_v11 ==> ~(?(v1:real^3) v2 v3 v4.
  71       dist(v1,v2) = &2 /\ dist(v2,v3) = &2 /\ dist(v3,v4) = &2 /\ dist(v1,v4)= &2 * h0 /\
  72       cstab <= dist(v1,v3) /\ cstab <= dist(v2,v4))`,
  73   (* {{{ proof *)
  74   [
  75   REWRITE_TAC[NOT_EXISTS_THM;Sphere.cstab];
  76   REPEAT WEAKER_STRIP_TAC;
  77   INTRO_TAC (Terminal.get_main_nonlinear "8495326405") [`dist(v3,v4)`;`dist(v2,v3)`;`dist(v1,v3)`;`dist(v1,v2)`;`dist(v1,v4)`;`dist(v2,v4)`];
  78   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `x <= x`];
  79   DISCH_THEN MP_TAC THEN ANTS_TAC;
  80     ASM_REWRITE_TAC[arith `x <= x`];
  81     TYPIFY `!w1 w3 w2. dist(w1,w2) = &2 /\ dist(w2,w3) = &2 ==> dist((w1:real^3),w3) <= &6` ENOUGH_TO_SHOW_TAC;
  82       BY(DISCH_TAC THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[DIST_SYM]);
  83     REPEAT GEN_TAC THEN (INTRO_TAC DIST_TRIANGLE[`w1`;`w2`;`w3`]);
  84     BY(REAL_ARITH_TAC);
  85   REWRITE_TAC[arith `~(x < &0) <=> &0 <= x`];
  86   BY(INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`v3`;`v4`;`v2`;`v1`] THEN REWRITE_TAC[DIST_SYM])
  87   ]);;
  88   (* }}} *)
  89
  90 (* shortest diag < 3.62 *)
  91
  92 let quad_diag_362 = prove_by_refinement(
  93   `main_nonlinear_terminal_v11 ==> (!(v1:real^3) v2 v3 v4.
  94       dist(v1,v2) = &2 /\ dist(v2,v3) = cstab /\ dist(v3,v4) = &2 /\ dist(v1,v4)= cstab ==>
  95       (dist(v1,v3) <= #3.62 \/ dist(v2,v4) <= #3.62))`,
  96   (* {{{ proof *)
  97   [
  98   REWRITE_TAC[Sphere.cstab;arith `x <= y <=> ~(y < x)`;GSYM DE_MORGAN_THM];
  99   REPEAT WEAKER_STRIP_TAC;
 100   INTRO_TAC (Terminal.get_main_nonlinear "2171548893") [`dist(v3,v4)`;`dist(v2,v3)`;`dist(v1,v3)`;`dist(v1,v2)`;`dist(v1,v4)`;`dist(v2,v4)`];
 101   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `x <= x`];
 102   DISCH_THEN MP_TAC THEN ANTS_TAC;
 103     ASM_REWRITE_TAC[arith `x <= x`];
 104     ASM_SIMP_TAC[arith `x < y ==> x <= y`];
 105     TYPIFY `!w1 w3 w2. dist(w1,w2) = &2 /\ dist(w2,w3) = #3.01 ==> dist((w1:real^3),w3) <= &6` ENOUGH_TO_SHOW_TAC;
 106       BY(DISCH_TAC THEN CONJ_TAC THENL [ALL_TAC;ONCE_REWRITE_TAC[DIST_SYM]] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[DIST_SYM]);
 107     REPEAT GEN_TAC THEN (INTRO_TAC DIST_TRIANGLE[`w1`;`w2`;`w3`]);
 108     BY(REAL_ARITH_TAC);
 109   REWRITE_TAC[arith `~(x < &0) <=> &0 <= x`];
 110   BY(INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`v3`;`v4`;`v2`;`v1`] THEN REWRITE_TAC[DIST_SYM])
 111   ]);;
 112   (* }}} *)
 113
 114 let INV_ARCLENGTH = prove_by_refinement(
 115   `!y1 y3 z.
 116    &0 < z /\ z < pi /\ &0 < y1 /\ &0 < y3 ==>
 117     &0 < y1 pow 2 + y3 pow 2 - &2 * y1  *y3 * cos z /\
 118     z = arclength y1 y3 (sqrt (y1 pow 2 + y3 pow 2 - &2 * y1 *y3 * cos z))`,
 119   (* {{{ proof *)
 120   [
 121   REPEAT WEAKER_STRIP_TAC;
 122   INTRO_TAC cos_bounds_0_pi [`z`];
 123   ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
 124   SUBCONJ_TAC;
 125     REWRITE_TAC[arith `y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z = (y1 - y3) pow 2 + &2 * y1 *y3 * (&1 - cos z)`];
 126     MATCH_MP_TAC (arith `&0 <= a /\ &0 < b ==> &0 < a + b`);
 127     REWRITE_TAC[ REAL_LE_POW_2];
 128     REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
 129     BY(ASM_TAC THEN REAL_ARITH_TAC);
 130   DISCH_TAC;
 131   TYPED_ABBREV_TAC `c = sqrt (y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z)`;
 132   GMATCH_SIMP_TAC Trigonometry1.ACS_ARCLENGTH;
 133   TYPIFY `c*c = y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z` (C SUBGOAL_THEN ASSUME_TAC);
 134     EXPAND_TAC "c";
 135     GMATCH_SIMP_TAC Merge_ineq.sqrtpow2;
 136     BY(ASM_TAC THEN REAL_ARITH_TAC);
 137   TYPED_ABBREV_TAC `r = (y1 * y1 + y3 * y3 - c * c) / (&2 * y1 * y3)`;
 138   CONJ2_TAC;
 139     TYPIFY `r = cos z` ENOUGH_TO_SHOW_TAC;
 140       DISCH_THEN SUBST1_TAC;
 141       GMATCH_SIMP_TAC ACS_COS;
 142       BY(ASM_TAC THEN REAL_ARITH_TAC);
 143     EXPAND_TAC "r";
 144     FIRST_X_ASSUM_ST `c * c = s` (SUBST1_TAC);
 145     Calc_derivative.CALC_ID_TAC;
 146     BY(ASM_TAC THEN REAL_ARITH_TAC);
 147   ASM_REWRITE_TAC[];
 148   SUBCONJ_TAC;
 149     EXPAND_TAC "c";
 150     GMATCH_SIMP_TAC SQRT_POS_LE;
 151     BY(ASM_TAC THEN REAL_ARITH_TAC);
 152   DISCH_TAC;
 153   TYPIFY `c pow 2 <= (y1 + y3) pow 2 /\ (abs(y1 - y3)) pow 2 <= c pow 2` ENOUGH_TO_SHOW_TAC;
 154     GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
 155     GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
 156     BY(ASM_TAC THEN REAL_ARITH_TAC);
 157   REWRITE_TAC[REAL_POW2_ABS];
 158   ASM_REWRITE_TAC[arith `c pow 2  = c * c`];
 159   TYPIFY `-- &2 * y1 * y3 * cos z <= &2 * y1 * y3 /\ -- &2 * y1 * y3 <= -- &2 * y1 * y3 * cos z` ENOUGH_TO_SHOW_TAC;
 160     BY(REAL_ARITH_TAC);
 161   REWRITE_TAC[arith ` -- &2 * y1 * y3 * cos z <= &2 * y1 *y3 <=> &0 <= &2 * y1 * y3 * (&1 + cos z)`;arith `-- &2 * y1 * y3 <= -- &2 * y1 * y3 * cos z <=> &0 <= &2 * y1 * y3 * (&1 - cos z)`];
 162   GMATCH_SIMP_TAC REAL_LE_MUL;
 163   REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
 164   BY(ASM_TAC THEN REAL_ARITH_TAC)
 165   ]);;
 166   (* }}} *)
 167
 168 let taum_dih_y = prove_by_refinement(
 169   `!y1 y2 y3 y4 y5 y6.
 170     taum y1 y2 y3 y4 y5 y6 =
 171     rho y1 * dih_y y1 y2 y3 y4 y5 y6 +
 172       rho y2 * dih_y y2 y3 y1 y5 y6 y4 +
 173       rho y3 * dih_y y3 y1 y2 y6 y4 y5 - (pi + sol0)`,
 174   (* {{{ proof *)
 175   [
 176   REWRITE_TAC[Sphere.taum;Sphere.sol_y;Sphere.lnazim;Sphere.rho;Nonlinear_lemma.sol0_const1];
 177   BY(REAL_ARITH_TAC)
 178   ]);;
 179   (* }}} *)
 180
 181 let real_continuous_dih_y_wrt4 = prove_by_refinement(
 182  `!y1 y2 y3 y4 y5 y6.
 183      &0 < delta_y y1 y2 y3 y4 y5 y6 /\
 184      &0 < y1 /\
 185      &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
 186      &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5)
 187      ==> (\q. dih_y y1 y2 y3 q y5 y6) real_continuous atreal y4`,
 188   (* {{{ proof *)
 189   [
 190   REPEAT WEAKER_STRIP_TAC;
 191   INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x4 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
 192   REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM];
 193   REWRITE_TAC[WITHINREAL_UNIV];
 194   ANTS_TAC;
 195     ASM_REWRITE_TAC[];
 196     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 197     BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
 198   DISCH_TAC;
 199   TYPIFY `(\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (q * q) (y5 * y5) (y6 * y6)) = (\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (q) (y5 * y5) (y6 * y6)) o (\t. t pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
 200     BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]);
 201   MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE;
 202   CONJ_TAC;
 203     MATCH_MP_TAC REAL_CONTINUOUS_POW;
 204     BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);
 205   REWRITE_TAC[arith `y4 pow 2 = y4 * y4`];
 206   MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
 207   BY(ASM_MESON_TAC[])
 208   ]);;
 209   (* }}} *)
 210
 211 let real_continuous_dih_y_wrt5 = prove_by_refinement(
 212  `!y1 y2 y3 y4 y5 y6.
 213      &0 < delta_y y1 y2 y3 y4 y5 y6 /\
 214      &0 < y1 /\
 215      &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
 216      &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5)
 217      ==> (\q. dih_y y1 y2 y3 y4 q y6) real_continuous atreal y5`,
 218   (* {{{ proof *)
 219   [
 220   REPEAT WEAKER_STRIP_TAC;
 221   INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x5 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
 222   REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM];
 223   REWRITE_TAC[WITHINREAL_UNIV];
 224   ANTS_TAC;
 225     ASM_REWRITE_TAC[];
 226     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 227     BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
 228   DISCH_TAC;
 229   TYPIFY `(\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (q * q) (y6 * y6)) = (\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4*y4) (q) (y6 * y6)) o (\t. t pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
 230     BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]);
 231   MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE;
 232   CONJ_TAC;
 233     MATCH_MP_TAC REAL_CONTINUOUS_POW;
 234     BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);
 235   REWRITE_TAC[arith `y5 pow 2 = y5 * y5`];
 236   MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
 237   BY(ASM_MESON_TAC[])
 238   ]);;
 239   (* }}} *)
 240
 241 let real_continuous_dih_y_wrt6 = prove_by_refinement(
 242  `!y1 y2 y3 y4 y5 y6.
 243      &0 < delta_y y1 y2 y3 y4 y5 y6 /\
 244      &0 < y1 /\
 245      &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
 246      &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5)
 247      ==> (\q. dih_y y1 y2 y3 y4 y5 q) real_continuous atreal y6`,
 248   (* {{{ proof *)
 249   [
 250   REPEAT WEAKER_STRIP_TAC;
 251   INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x6 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
 252   REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM];
 253   REWRITE_TAC[WITHINREAL_UNIV];
 254   ANTS_TAC;
 255     ASM_REWRITE_TAC[];
 256     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 257     BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
 258   DISCH_TAC;
 259   TYPIFY `(\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (q*q)) = (\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4*y4) (y5 * y5) (q)) o (\t. t pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
 260     BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]);
 261   MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE;
 262   CONJ_TAC;
 263     MATCH_MP_TAC REAL_CONTINUOUS_POW;
 264     BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);
 265   REWRITE_TAC[arith `y6 pow 2 = y6 * y6`];
 266   MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
 267   BY(ASM_MESON_TAC[])
 268   ]);;
 269   (* }}} *)
 270
 271 let real_continuous_taum = prove_by_refinement(
 272   `!y1 y2 y3 y4 y5 y6.
 273          &0 < delta_y y1 y2 y3 y4 y5 y6 /\
 274          &0 < y1 /\ &0 < y2 /\ &0 < y3 /\
 275          &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
 276          &0 < ups_x (y2 * y2) (y3 * y3) (y4 * y4) /\
 277          &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5) ==>
 278      (\q. taum y1 y2 y3 q y5 y6) real_continuous atreal y4`,
 279   (* {{{ proof *)
 280   [
 281   REWRITE_TAC[taum_dih_y];
 282   REPEAT WEAKER_STRIP_TAC;
 283   TYPIFY `delta_y y3 y1 y2 y6 y4 y5 = delta_y y1 y2 y3 y4 y5 y6 /\ delta_y y2 y3 y1 y5 y6 y4 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
 284     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
 285   TYPIFY `ups_x (y3 * y3) (y1 * y1) (y5 * y5) = ups_x (y1 * y1) (y3 * y3) (y5 * y5) /\ ups_x (y3 * y3) (y2 * y2) (y4 * y4) = ups_x (y2 * y2) (y3 * y3) (y4 * y4) /\ ups_x (y2 * y2) (y1 * y1) (y6 * y6) = ups_x (y1 * y1) (y2 * y2) (y6 * y6)` (C SUBGOAL_THEN ASSUME_TAC);
 286     BY(REWRITE_TAC[Merge_ineq.ups_x_sym]);
 287   BY((REPEAT (REPEAT CONJ_TAC THEN (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_POW ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB ORELSE MATCH_MP_TAC real_continuous_dih_y_wrt6 ORELSE MATCH_MP_TAC real_continuous_dih_y_wrt5 ORELSE MATCH_MP_TAC real_continuous_dih_y_wrt4 THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST]))))
 288   ]);;
 289   (* }}} *)
 290
 291 let UPS_X_STD_POS = prove_by_refinement(
 292   `!y1 y2 y3.   &2 <= y1 /\ y1 <= &2 * h0 /\
 293         &2 <= y2 /\ y2 <= &2 * h0 /\
 294         &2 <= y3 /\ y3 <= &2 * h0 ==> &0 < ups_x (y1 * y1) (y2 * y2) (y3 * y3)`,
 295   (* {{{ proof *)
 296   [
 297   REPEAT WEAKER_STRIP_TAC;
 298   BY(MATCH_MP_TAC Ysskqoy.TRI_UPS_X_STRICT_POS THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
 299   ]);;
 300   (* }}} *)
 301
 302
 303
 304 let BKOSSGE = prove_by_refinement(
 305   `scs_arrow_v39 {scs_3M1} {scs_3T1, scs_3T5}`,
 306   (* {{{ proof *)
 307   [
 308   REWRITE_TAC[Appendix.scs_arrow_v39;IN_SING;IN_INSERT;NOT_IN_EMPTY];
 309   CONJ_TAC;
 310     BY(MESON_TAC[Ocbicby.is_scs_examples]);
 311   REWRITE_TAC[TAUT `(a \/ b) <=> (~a ==> b)`;NOT_FORALL_THM];
 312   REWRITE_TAC[TAUT `~(a ==> b) <=> (a /\ ~b)`];
 313   REWRITE_TAC[IN;NOT_FORALL_THM];
 314   REPEAT WEAKER_STRIP_TAC;
 315   TYPIFY `?v. MMs_v39 s v /\ dist(v 0,v 1) <= sqrt8` ASM_CASES_TAC;
 316     FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
 317     TYPIFY `scs_3T5` EXISTS_TAC;
 318     REWRITE_TAC[];
 319     MATCH_MP_TAC Ppbtydq.XWNHLMD_MM;
 320     ASM_REWRITE_TAC[];
 321     REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples];
 322     nCONJ_TAC 1;
 323       BY(ASM_MESON_TAC[IN]);
 324     CONJ_TAC;
 325       BY(REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]);
 326     ASM_REWRITE_TAC[];
 327     CONJ2_TAC;
 328       REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39];
 329       BY(REAL_ARITH_TAC);
 330     REWRITE_TAC[IN;Appendix.BBs_v39];
 331     REPEAT LET_TAC;
 332     REWRITE_TAC[Appendix.scs_3T5;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
 333     TYPIFY `BBs_v39 scs_3M1 v` (C SUBGOAL_THEN MP_TAC);
 334       MATCH_MP_TAC Nuxcoea.MMS_IMP_BBS;
 335       BY(ASM_MESON_TAC[IN]);
 336     REWRITE_TAC[IN;Appendix.BBs_v39];
 337     ASM_REWRITE_TAC[];
 338     REWRITE_TAC[LET_THM];
 339     REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
 340     REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
 341     MATCH_MP_TAC Terminal.periodic2_mod_reduce;
 342     TYPIFY `3` EXISTS_TAC;
 343     REWRITE_TAC[arith `~(3 =0)`];
 344     CONJ_TAC;
 345       FIRST_X_ASSUM_ST `periodic` MP_TAC;
 346       REWRITE_TAC[Appendix.periodic2;Oxl_def.periodic];
 347       DISCH_THEN (unlist REWRITE_TAC);
 348       BY(MESON_TAC[Terminal.periodic2_funlist;Appendix.periodic2]);
 349     REWRITE_TAC[arith `i < 3 <=> i = 0 \/ i = 1 \/ i = 2 `];
 350     REWRITE_TAC[TAUT ` ((a \/ b) /\ c) <=> ((a /\ c) \/ (b /\ c))`;TAUT `(a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))`];
 351     BY(REPEAT STRIP_TAC THEN (FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`])) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN REWRITE_TAC[Appendix.psort;LET_THM;Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN FIRST_X_ASSUM_ST `sqrt8` MP_TAC THEN REWRITE_TAC[DIST_SYM;PAIR_EQ] THEN NUM_REDUCE_TAC THEN TRY REAL_ARITH_TAC);
 352   COMMENT "second half";
 353   TYPIFY `?v. MMs_v39 s v /\ sqrt8 <= dist(v 0,v 1)` (C SUBGOAL_THEN MP_TAC);
 354     FIRST_X_ASSUM_ST `{}` MP_TAC THEN REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
 355     BY(REWRITE_TAC[IN] THEN ASM_MESON_TAC[arith `~(x <= y) ==> (y <= x)`]);
 356   POP_ASSUM kill;
 357   REPEAT WEAKER_STRIP_TAC;
 358   TYPIFY `scs_3T1` EXISTS_TAC;
 359   REWRITE_TAC[];
 360   MATCH_MP_TAC Ppbtydq.XWNHLMD_MM;
 361   ASM_REWRITE_TAC[];
 362   REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples];
 363   nCONJ_TAC 1;
 364     BY(ASM_MESON_TAC[IN]);
 365   CONJ_TAC;
 366     BY(REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_3M1;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]);
 367   ASM_REWRITE_TAC[];
 368   CONJ2_TAC;
 369     REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T1;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39];
 370     BY(REAL_ARITH_TAC);
 371   REWRITE_TAC[IN;Appendix.BBs_v39];
 372   REPEAT LET_TAC;
 373   REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
 374   TYPIFY `BBs_v39 scs_3M1 v` (C SUBGOAL_THEN MP_TAC);
 375     MATCH_MP_TAC Nuxcoea.MMS_IMP_BBS;
 376     BY(ASM_MESON_TAC[IN]);
 377   REWRITE_TAC[IN;Appendix.BBs_v39];
 378   ASM_REWRITE_TAC[];
 379   REWRITE_TAC[LET_THM];
 380   REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
 381   REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
 382   MATCH_MP_TAC Terminal.periodic2_mod_reduce;
 383   TYPIFY `3` EXISTS_TAC;
 384   REWRITE_TAC[arith `~(3 =0)`];
 385   CONJ_TAC;
 386     FIRST_X_ASSUM_ST `periodic` MP_TAC;
 387     REWRITE_TAC[Appendix.periodic2;Oxl_def.periodic];
 388     DISCH_THEN (unlist REWRITE_TAC);
 389     BY(MESON_TAC[Terminal.periodic2_funlist;Appendix.periodic2]);
 390   REWRITE_TAC[arith `i < 3 <=> i = 0 \/ i = 1 \/ i = 2 `];
 391   REWRITE_TAC[TAUT ` ((a \/ b) /\ c) <=> ((a /\ c) \/ (b /\ c))`;TAUT `(a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))`];
 392   BY(REPEAT STRIP_TAC THEN (FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`])) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN REWRITE_TAC[Appendix.psort;LET_THM;Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN FIRST_X_ASSUM_ST `sqrt8` MP_TAC THEN REWRITE_TAC[DIST_SYM;PAIR_EQ] THEN NUM_REDUCE_TAC THEN TRY REAL_ARITH_TAC)
 393   ]);;
 394   (* }}} *)
 395
 396 end;;