(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Appendix, Main Estimate, check_completeness                       *)
(* Chapter: Local Fan                                                         *)
(* Lemma: BKOSSGE                                                             *)
(* Author: Thomas Hales                                                       *)
(* Date: 2013-08-07                                                           *)
(* ========================================================================== *)

module Bkossge = struct 

  open Hales_tactic;;

let cos_bounds_0_pi = 
prove_by_refinement( `!z. &0 < z /\ z < pi ==> -- &1 < cos z /\ cos z < &1`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `(&0 < z /\ z < pi / &2) \/ z = pi / &2 \/ (&0 < pi - z /\ pi - z < pi / &2)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC); BY(ASM_MESON_TAC[Counting_spheres.cos_bounds_0_Pi2;arith `&0 < x ==> -- &1 < x`]); ASM_REWRITE_TAC[COS_PI2]; BY(REAL_ARITH_TAC); TYPIFY `-- &1 < --cos z /\ --cos z < &1` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); ONCE_REWRITE_TAC[GSYM COS_NEG]; REWRITE_TAC[GSYM COS_PERIODIC_PI;arith `--z + pi = pi - z`]; BY(ASM_MESON_TAC[Counting_spheres.cos_bounds_0_Pi2;arith `&0 < x ==> -- &1 < x`]) ]);;
(* }}} *)
let ear_acute = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6. &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ &2 <= y4 /\ y4 <= &2 * h0 /\ &2 <= y6 /\ y6 <= &2 * h0 /\ &3 <= y5 /\ &0 < ups_x (y1*y1) (y3*y3) (y5*y5) ==> dih_y y1 y2 y3 y4 y5 y6 < pi / &2) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.h0;arith `&2 * #1.26 = #2.52`;Trigonometry.IHIQXLM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (Terminal.get_main_nonlinear "2485876245a") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]; ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `#3.0 = &3`;]; ANTS_TAC; REWRITE_TAC[arith `x <= y <=> ~(y < x)`]; DISCH_TAC; FIRST_X_ASSUM_ST `&16` MP_TAC THEN REWRITE_TAC[arith `a * b * c = (a * b) * c`]; REWRITE_TAC[arith `~(&0 < x * y) <=> &0 <= x * (-- y)`]; REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL_EQ); REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ); BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Nonlinear_lemma.dih_x_alt;Sphere.dih_y;LET_THM;GSYM Sphere.delta_y]; REWRITE_TAC[GSYM Sphere.delta4_y;GSYM Sphere.y_of_x]; REWRITE_TAC[arith `pi2 + a < pi2 <=> a < &0`]; DISCH_TAC; GMATCH_SIMP_TAC Tskajxy.ATN2_Y_NEG; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[arith `p - a = p + -- a`;GSYM ATN_NEG;arith `-- p + a < &0 <=> a < p`;ATN_BOUNDS]) ]);;
(* }}} *)
let quad_nonexist_849 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> ~(?(v1:real^3) v2 v3 v4. dist(v1,v2) = &2 /\ dist(v2,v3) = &2 /\ dist(v3,v4) = &2 /\ dist(v1,v4)= &2 * h0 /\ cstab <= dist(v1,v3) /\ cstab <= dist(v2,v4))`,
(* {{{ proof *) [ REWRITE_TAC[NOT_EXISTS_THM;Sphere.cstab]; REPEAT WEAKER_STRIP_TAC; 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)`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `x <= x`]; DISCH_THEN MP_TAC THEN ANTS_TAC; ASM_REWRITE_TAC[arith `x <= x`]; TYPIFY `!w1 w3 w2. dist(w1,w2) = &2 /\ dist(w2,w3) = &2 ==> dist((w1:real^3),w3) <= &6` ENOUGH_TO_SHOW_TAC; BY(DISCH_TAC THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[DIST_SYM]); REPEAT GEN_TAC THEN (INTRO_TAC DIST_TRIANGLE[`w1`;`w2`;`w3`]); BY(REAL_ARITH_TAC); REWRITE_TAC[arith `~(x < &0) <=> &0 <= x`]; BY(INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`v3`;`v4`;`v2`;`v1`] THEN REWRITE_TAC[DIST_SYM]) ]);;
(* }}} *) (* shortest diag < 3.62 *)
let quad_diag_362 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!(v1:real^3) v2 v3 v4. dist(v1,v2) = &2 /\ dist(v2,v3) = cstab /\ dist(v3,v4) = &2 /\ dist(v1,v4)= cstab ==> (dist(v1,v3) <= #3.62 \/ dist(v2,v4) <= #3.62))`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.cstab;arith `x <= y <=> ~(y < x)`;GSYM DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; 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)`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `x <= x`]; DISCH_THEN MP_TAC THEN ANTS_TAC; ASM_REWRITE_TAC[arith `x <= x`]; ASM_SIMP_TAC[arith `x < y ==> x <= y`]; TYPIFY `!w1 w3 w2. dist(w1,w2) = &2 /\ dist(w2,w3) = #3.01 ==> dist((w1:real^3),w3) <= &6` ENOUGH_TO_SHOW_TAC; 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]); REPEAT GEN_TAC THEN (INTRO_TAC DIST_TRIANGLE[`w1`;`w2`;`w3`]); BY(REAL_ARITH_TAC); REWRITE_TAC[arith `~(x < &0) <=> &0 <= x`]; BY(INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`v3`;`v4`;`v2`;`v1`] THEN REWRITE_TAC[DIST_SYM]) ]);;
(* }}} *)
let INV_ARCLENGTH = 
prove_by_refinement( `!y1 y3 z. &0 < z /\ z < pi /\ &0 < y1 /\ &0 < y3 ==> &0 < y1 pow 2 + y3 pow 2 - &2 * y1 *y3 * cos z /\ z = arclength y1 y3 (sqrt (y1 pow 2 + y3 pow 2 - &2 * y1 *y3 * cos z))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC cos_bounds_0_pi [`z`]; ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC; SUBCONJ_TAC; REWRITE_TAC[arith `y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z = (y1 - y3) pow 2 + &2 * y1 *y3 * (&1 - cos z)`]; MATCH_MP_TAC (arith `&0 <= a /\ &0 < b ==> &0 < a + b`); REWRITE_TAC[ REAL_LE_POW_2]; REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ); BY(ASM_TAC THEN REAL_ARITH_TAC); DISCH_TAC; TYPED_ABBREV_TAC `c = sqrt (y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z)`; GMATCH_SIMP_TAC Trigonometry1.ACS_ARCLENGTH; TYPIFY `c*c = y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "c";
GMATCH_SIMP_TAC Merge_ineq.sqrtpow2; BY(ASM_TAC THEN REAL_ARITH_TAC); TYPED_ABBREV_TAC `r = (y1 * y1 + y3 * y3 - c * c) / (&2 * y1 * y3)`; CONJ2_TAC; TYPIFY `r = cos z` ENOUGH_TO_SHOW_TAC; DISCH_THEN SUBST1_TAC; GMATCH_SIMP_TAC ACS_COS; BY(ASM_TAC THEN REAL_ARITH_TAC); EXPAND_TAC "r"; FIRST_X_ASSUM_ST `c * c = s` (SUBST1_TAC); Calc_derivative.CALC_ID_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; SUBCONJ_TAC; EXPAND_TAC "c"; GMATCH_SIMP_TAC SQRT_POS_LE; BY(ASM_TAC THEN REAL_ARITH_TAC); DISCH_TAC; TYPIFY `c pow 2 <= (y1 + y3) pow 2 /\ (abs(y1 - y3)) pow 2 <= c pow 2` ENOUGH_TO_SHOW_TAC; GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND); GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND); BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[REAL_POW2_ABS]; ASM_REWRITE_TAC[arith `c pow 2 = c * c`]; TYPIFY `-- &2 * y1 * y3 * cos z <= &2 * y1 * y3 /\ -- &2 * y1 * y3 <= -- &2 * y1 * y3 * cos z` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); 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)`]; GMATCH_SIMP_TAC REAL_LE_MUL; REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let taum_dih_y = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. taum y1 y2 y3 y4 y5 y6 = rho y1 * dih_y y1 y2 y3 y4 y5 y6 + rho y2 * dih_y y2 y3 y1 y5 y6 y4 + rho y3 * dih_y y3 y1 y2 y6 y4 y5 - (pi + sol0)`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.taum;Sphere.sol_y;Sphere.lnazim;Sphere.rho;Nonlinear_lemma.sol0_const1]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let real_continuous_dih_y_wrt4 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 < delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\ &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5) ==> (\q. dih_y y1 y2 y3 q y5 y6) real_continuous atreal y4`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x4 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`]; REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM]; REWRITE_TAC[WITHINREAL_UNIV]; ANTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]); DISCH_TAC; 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); BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]); MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE; CONJ_TAC; MATCH_MP_TAC REAL_CONTINUOUS_POW; BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]); REWRITE_TAC[arith `y4 pow 2 = y4 * y4`]; MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let real_continuous_dih_y_wrt5 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 < delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\ &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5) ==> (\q. dih_y y1 y2 y3 y4 q y6) real_continuous atreal y5`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x5 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`]; REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM]; REWRITE_TAC[WITHINREAL_UNIV]; ANTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]); DISCH_TAC; 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); BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]); MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE; CONJ_TAC; MATCH_MP_TAC REAL_CONTINUOUS_POW; BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]); REWRITE_TAC[arith `y5 pow 2 = y5 * y5`]; MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let real_continuous_dih_y_wrt6 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 < delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\ &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5) ==> (\q. dih_y y1 y2 y3 y4 y5 q) real_continuous atreal y6`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x6 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`]; REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM]; REWRITE_TAC[WITHINREAL_UNIV]; ANTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]); DISCH_TAC; 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); BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]); MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE; CONJ_TAC; MATCH_MP_TAC REAL_CONTINUOUS_POW; BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]); REWRITE_TAC[arith `y6 pow 2 = y6 * y6`]; MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let real_continuous_taum = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 < delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < y2 /\ &0 < y3 /\ &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\ &0 < ups_x (y2 * y2) (y3 * y3) (y4 * y4) /\ &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5) ==> (\q. taum y1 y2 y3 q y5 y6) real_continuous atreal y4`,
(* {{{ proof *) [ REWRITE_TAC[taum_dih_y]; REPEAT WEAKER_STRIP_TAC; 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); BY(MESON_TAC[Merge_ineq.delta_y_sym]); 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); BY(REWRITE_TAC[Merge_ineq.ups_x_sym]); 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])))) ]);;
(* }}} *)
let UPS_X_STD_POS = 
prove_by_refinement( `!y1 y2 y3. &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 ==> &0 < ups_x (y1 * y1) (y2 * y2) (y3 * y3)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; BY(MATCH_MP_TAC Ysskqoy.TRI_UPS_X_STRICT_POS THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let BKOSSGE = 
prove_by_refinement( `scs_arrow_v39 {scs_3M1} {scs_3T1, scs_3T5}`,
(* {{{ proof *) [ REWRITE_TAC[Appendix.scs_arrow_v39;IN_SING;IN_INSERT;NOT_IN_EMPTY]; CONJ_TAC; BY(MESON_TAC[Ocbicby.is_scs_examples]); REWRITE_TAC[TAUT `(a \/ b) <=> (~a ==> b)`;NOT_FORALL_THM]; REWRITE_TAC[TAUT `~(a ==> b) <=> (a /\ ~b)`]; REWRITE_TAC[IN;NOT_FORALL_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `?v. MMs_v39 s v /\ dist(v 0,v 1) <= sqrt8` ASM_CASES_TAC; FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `scs_3T5` EXISTS_TAC; REWRITE_TAC[]; MATCH_MP_TAC Ppbtydq.XWNHLMD_MM; ASM_REWRITE_TAC[]; REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples]; nCONJ_TAC 1; BY(ASM_MESON_TAC[IN]); CONJ_TAC; BY(REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]); ASM_REWRITE_TAC[]; CONJ2_TAC; REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39]; BY(REAL_ARITH_TAC); REWRITE_TAC[IN;Appendix.BBs_v39]; REPEAT LET_TAC; REWRITE_TAC[Appendix.scs_3T5;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit]; TYPIFY `BBs_v39 scs_3M1 v` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC Nuxcoea.MMS_IMP_BBS; BY(ASM_MESON_TAC[IN]); REWRITE_TAC[IN;Appendix.BBs_v39]; ASM_REWRITE_TAC[]; REWRITE_TAC[LET_THM]; REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit]; REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC Terminal.periodic2_mod_reduce; TYPIFY `3` EXISTS_TAC; REWRITE_TAC[arith `~(3 =0)`]; CONJ_TAC; FIRST_X_ASSUM_ST `periodic` MP_TAC; REWRITE_TAC[Appendix.periodic2;Oxl_def.periodic]; DISCH_THEN (unlist REWRITE_TAC); BY(MESON_TAC[Terminal.periodic2_funlist;Appendix.periodic2]); REWRITE_TAC[arith `i < 3 <=> i = 0 \/ i = 1 \/ i = 2 `]; REWRITE_TAC[TAUT ` ((a \/ b) /\ c) <=> ((a /\ c) \/ (b /\ c))`;TAUT `(a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))`]; 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); COMMENT "second half";
TYPIFY `?v. MMs_v39 s v /\ sqrt8 <= dist(v 0,v 1)` (C SUBGOAL_THEN MP_TAC); FIRST_X_ASSUM_ST `{}` MP_TAC THEN REWRITE_TAC[EXTENSION;NOT_IN_EMPTY]; BY(REWRITE_TAC[IN] THEN ASM_MESON_TAC[arith `~(x <= y) ==> (y <= x)`]); POP_ASSUM kill; REPEAT WEAKER_STRIP_TAC; TYPIFY `scs_3T1` EXISTS_TAC; REWRITE_TAC[]; MATCH_MP_TAC Ppbtydq.XWNHLMD_MM; ASM_REWRITE_TAC[]; REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples]; nCONJ_TAC 1; BY(ASM_MESON_TAC[IN]); CONJ_TAC; BY(REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_3M1;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]); ASM_REWRITE_TAC[]; CONJ2_TAC; REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T1;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39]; BY(REAL_ARITH_TAC); REWRITE_TAC[IN;Appendix.BBs_v39]; REPEAT LET_TAC; REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit]; TYPIFY `BBs_v39 scs_3M1 v` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC Nuxcoea.MMS_IMP_BBS; BY(ASM_MESON_TAC[IN]); REWRITE_TAC[IN;Appendix.BBs_v39]; ASM_REWRITE_TAC[]; REWRITE_TAC[LET_THM]; REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit]; REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC Terminal.periodic2_mod_reduce; TYPIFY `3` EXISTS_TAC; REWRITE_TAC[arith `~(3 =0)`]; CONJ_TAC; FIRST_X_ASSUM_ST `periodic` MP_TAC; REWRITE_TAC[Appendix.periodic2;Oxl_def.periodic]; DISCH_THEN (unlist REWRITE_TAC); BY(MESON_TAC[Terminal.periodic2_funlist;Appendix.periodic2]); REWRITE_TAC[arith `i < 3 <=> i = 0 \/ i = 1 \/ i = 2 `]; REWRITE_TAC[TAUT ` ((a \/ b) /\ c) <=> ((a /\ c) \/ (b /\ c))`;TAUT `(a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))`]; 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) ]);; (* }}} *) end;;