1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Appendix, Main Estimate, check_completeness *)
4 (* Chapter: Local Fan *)
6 (* Author: Thomas Hales *)
8 (* ========================================================================== *)
10 module Bkossge = struct
14 let cos_bounds_0_pi = prove_by_refinement(
15 `!z. &0 < z /\ z < pi ==> -- &1 < cos z /\ cos z < &1`,
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];
25 TYPIFY `-- &1 < --cos z /\ --cos z < &1` ENOUGH_TO_SHOW_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`])
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 /\
41 &0 < ups_x (y1*y1) (y3*y3) (y5*y5)
42 ==> dih_y y1 y2 y3 y4 y5 y6 < pi / &2)
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`;];
51 REWRITE_TAC[arith `x <= y <=> ~(y < x)`];
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`];
62 GMATCH_SIMP_TAC Tskajxy.ATN2_Y_NEG;
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])
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))`,
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`]);
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])
90 (* shortest diag < 3.62 *)
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))`,
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`]);
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])
114 let INV_ARCLENGTH = prove_by_refinement(
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))`,
121 REPEAT WEAKER_STRIP_TAC;
122 INTRO_TAC cos_bounds_0_pi [`z`];
123 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_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);
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);
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)`;
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);
144 FIRST_X_ASSUM_ST `c * c = s` (SUBST1_TAC);
145 Calc_derivative.CALC_ID_TAC;
146 BY(ASM_TAC THEN REAL_ARITH_TAC);
150 GMATCH_SIMP_TAC SQRT_POS_LE;
151 BY(ASM_TAC THEN REAL_ARITH_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;
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)
168 let taum_dih_y = prove_by_refinement(
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)`,
176 REWRITE_TAC[Sphere.taum;Sphere.sol_y;Sphere.lnazim;Sphere.rho;Nonlinear_lemma.sol0_const1];
181 let real_continuous_dih_y_wrt4 = prove_by_refinement(
183 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
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`,
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];
196 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
197 BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
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;
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;
211 let real_continuous_dih_y_wrt5 = prove_by_refinement(
213 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
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`,
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];
226 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
227 BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
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;
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;
241 let real_continuous_dih_y_wrt6 = prove_by_refinement(
243 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
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`,
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];
256 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
257 BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
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;
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;
271 let real_continuous_taum = prove_by_refinement(
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`,
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]))))
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)`,
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)
304 let BKOSSGE = prove_by_refinement(
305 `scs_arrow_v39 {scs_3M1} {scs_3T1, scs_3T5}`,
308 REWRITE_TAC[Appendix.scs_arrow_v39;IN_SING;IN_INSERT;NOT_IN_EMPTY];
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;
319 MATCH_MP_TAC Ppbtydq.XWNHLMD_MM;
321 REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples];
323 BY(ASM_MESON_TAC[IN]);
325 BY(REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]);
328 REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39];
330 REWRITE_TAC[IN;Appendix.BBs_v39];
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];
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)`];
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)`]);
357 REPEAT WEAKER_STRIP_TAC;
358 TYPIFY `scs_3T1` EXISTS_TAC;
360 MATCH_MP_TAC Ppbtydq.XWNHLMD_MM;
362 REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples];
364 BY(ASM_MESON_TAC[IN]);
366 BY(REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_3M1;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]);
369 REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T1;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39];
371 REWRITE_TAC[IN;Appendix.BBs_v39];
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];
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)`];
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)