text_formalization/nonlinear/formal_tests/test2.hl

   1 (* TSKAJXY-TADIAMB *)
   2 let ineq_tm = `ineq
   3  [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
   4         #4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
   5  (unit6 x1 x2 x3 x4 x5 x6 *  #2.0 + rad2_x x1 x2 x3 x4 x5 x6 * -- &1 < &0)`;;
   6
   7 (* Too difficult:
   8 verify_flyspeck_ineq 3 ineq_tm;;
   9 *)
  10
  11 let ineq1_tm = `ineq
  12  [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
  13         #4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
  14  (&0 < delta_x x1 x2 x3 x4 x5 x6 * &4)`;;
  15
  16 let ineq2_tm = `ineq
  17  [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
  18         #4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
  19  ((unit6 x1 x2 x3 x4 x5 x6 * #2.0) * (delta_x x1 x2 x3 x4 x5 x6 * &4) < rho_x x1 x2 x3 x4 x5 x6)`;;
  20
  21 (* easy *)
  22 let delta_x4_pos = verify_flyspeck_ineq 3 ineq1_tm;;
  23 (* easy *)
  24 let ineq2_th = verify_flyspeck_ineq 3 ineq2_tm;;
  25
  26 let eq_th = REWRITE_CONV[ineq; IMP_IMP] ineq_tm;;
  27 let INEQ_RULE = UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[ineq; IMP_IMP];;
  28 let th0 = INEQ_RULE delta_x4_pos;;
  29 let th1 = INEQ_RULE ineq2_th;;
  30 let th2 = MATCH_MP REAL_LT_RDIV_EQ th0;;
  31 let th3 = REWRITE_RULE[GSYM th2; GSYM rad2_x] th1;;
  32 let th4 = ONCE_REWRITE_RULE[REAL_ARITH `a < b <=> a + b * -- &1 < &0`] th3;;
  33 let result = (REWRITE_RULE[GSYM eq_th] o DISCH_ALL) th4;;
  34
  35
  36
  37 (* 7067938795 *)
  38 add_example {id = "7067938795";
  39              difficulty = Medium;
  40              ineq_tm = `ineq [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #4.0;
  41                                #3.01 *  #3.01, x5, #3.24 *  #3.24;  #3.01 *  #3.01,x6, #3.24 *  #3.24]
  42     (dih_x' x1 x2 x3 x4 x5 x6 +
  43        unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 /  #2.0) +
  44        unit6 x1 x2 x3 x4 x5 x6 *  #0.46 <
  45      &0)`;;
  46
  47 (* base = 200: 690s (834s total) (386s (468s) Ubuntu 9/Ocaml 3.09.3)*)
  48 verify_flyspeck_ineq 4 ineq_tm;;
  49
  50
  51 (* 3318775219 *)
  52 let ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
  53                    &2, y3, #2.52; #2.52, y4, sqrt(&8);
  54                    &2, y5, #2.52; &2, y6, #2.52]
  55     ( ((dih_y' y1 y2 y3 y4 y5 y6) - #1.629 +
  56         (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
  57         (#0.763 * (y4 - #2.52)) -
  58         (#0.315 * (y1 - #2.0))) * (-- &1)  < &0)`;;
  59
  60 (* base = 200: 27946s (31514s total) (Ubuntu 9: 15226 (17091)) *)
  61 verify_flyspeck_ineq 5 ineq_tm;;
  62
  63 let ineq_tm2 = `ineq [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #6.3504,x4, #8.0;
  64   #4.0, x5, #6.3504;  #4.0,x6, #6.3504]
  65  (dih_x' x1 x2 x3 x4 x5 x6 * -- &1 +
  66   unit6 x1 x2 x3 x4 x5 x6 *  #1.629 +
  67   sqrt_x2 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  68   sqrt_x3 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  69   sqrt_x5 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  70   sqrt_x6 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  71   unit6 x1 x2 x3 x4 x5 x6 *  #0.414 *  #8.0 +
  72   sqrt_x4 x1 x2 x3 x4 x5 x6 *  #0.763 +
  73   unit6 x1 x2 x3 x4 x5 x6 *  #0.763 * -- #2.52 +
  74   sqrt_x1 x1 x2 x3 x4 x5 x6 *  #0.315 +
  75   unit6 x1 x2 x3 x4 x5 x6 *  #0.315 * -- #2.0 <
  76   &0)`;;
  77
  78 (* Ubuntu 9: 6hr (16279s (14296s) with Sys.time()) *)
  79 verify_flyspeck_ineq 5 ineq_tm2;;
  80
  81 (* 5490182221 *)
  82 let ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
  83                      &2, y3, #2.52; &2, y4, #2.52;
  84                      &2, y5, #2.52; &2, y6, #2.52]
  85   (dih_y' y1 y2 y3 y4 y5 y6 < #1.893)`;;
  86
  87 (* base = 200: 5570s (6480s total) *)
  88 verify_flyspeck_ineq 10 ineq_tm;;
  89
  90 (* base = 200 (Ubuntu 9): 3600s total (2716s (3128s) with Sys.time()) *)
  91 verify_flyspeck_ineq 4 ineq_tm;;
  92
  93 let ineq_tm2 = `ineq
  94  [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #6.3504;
  95   #4.0, x5, #6.3504;  #4.0,x6, #6.3504]
  96  (dih_x' x1 x2 x3 x4 x5 x6 + unit6 x1 x2 x3 x4 x5 x6 * -- #1.893 < &0)`;;
  97
  98 (* base = 200 (Ubuntu 9): 1593s (1450s) *)
  99 verify_flyspeck_ineq 4 ineq_tm2;;
 100
 101
 102
 103