formal_ineqs/examples_flyspeck.hl

   1 (* Some inequalities from the Flyspeck project *)
   2 (* http://code.google.com/p/flyspeck/ *)
   3
   4 (* Set up the loading path:
   5 load_path := "path to the formal_ineqs directory" :: !load_path;;
   6 *)
   7
   8 (* Change default arithmetic options before loading other libraries *)
   9 (* (arithmetic options cannot be changed later) *)
  10 needs "arith_options.hl";;
  11
  12 (* Set the base of natural number arithmetic to 200 *)
  13 Arith_options.base := 200;;
  14
  15 (* Load all verification libraries *)
  16 (* Note: the verification library loads Multivariate/realanalysis.ml,
  17    so it is recommended to use a checkpointed version of HOL Light
  18    with preloaded realanalysis.ml *)
  19 needs "verifier/m_verifier_main.hl";;
  20
  21 (*
  22   Set the level of info/debug printing:
  23   0 - no info/debug printing
  24   1 - report important steps (default)
  25   2 - report everything
  26 *)
  27 needs "verifier_options.hl";;
  28 Verifier_options.info_print_level := 1;;
  29
  30 (* Open the main verification module *)
  31 open M_verifier_main;;
  32
  33
  34
  35
  36 (************************)
  37 (* Flyspeck definitions *)
  38
  39
  40 (* ineq *)
  41 let ineq = define
  42  `(!c. ineq [] c <=> c)
  43     /\ (!a x b xs c. ineq (CONS (a,x,b) xs) c <=> a <= x /\ x <= b ==> ineq xs c)`;;
  44
  45 (* A modified (only one case is considered, x > 0) definition of atn2 *)
  46 (* Add ' to some definitions to avoid conflicts with original Flyspeck definitions *)
  47 let atn2' = new_definition `atn2'(x,y) = atn(y / x)`
  48
  49
  50 (* delta_x *)
  51 let delta_x = new_definition (`delta_x x1 x2 x3 x4 x5 x6 =
  52         x1*x4*(--x1 + x2 + x3 -x4 + x5 + x6) +
  53         x2*x5*(x1 - x2 + x3 + x4 -x5 + x6) +
  54         x3*x6*(x1 + x2 - x3 + x4 + x5 - x6)
  55         -x2*x3*x4 - x1*x3*x5 - x1*x2*x6 -x4*x5*x6`);;
  56
  57 (* delta_y *)
  58 let delta_y = new_definition `delta_y y1 y2 y3 y4 y5 y6 =
  59     delta_x (y1*y1) (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6)`;;
  60
  61 (* delta_x4 *)
  62 let delta_x4= new_definition(`delta_x4 x1 x2 x3 x4 x5 x6
  63         =  -- x2* x3 -  x1* x4 + x2* x5
  64         + x3* x6 -  x5* x6 + x1* (-- x1 +  x2 +  x3 -  x4 +  x5 +  x6)`);;
  65
  66 (* ups_x *)
  67 let ups_x = new_definition(`ups_x x1 x2 x6 =
  68     --x1*x1 - x2*x2 - x6*x6
  69     + &2 *x1*x6 + &2 *x1*x2 + &2 *x2*x6`);;
  70
  71 (* rho_x *)
  72 let rho_x = new_definition(`rho_x x1 x2 x3 x4 x5 x6 =
  73         --x1*x1*x4*x4 - x2*x2*x5*x5 - x3*x3*x6*x6 +
  74         (&2)*x1*x2*x4*x5 + (&2)*x1*x3*x4*x6 + (&2)*x2*x3*x5*x6`);;
  75
  76 (* rad2_x *)
  77 let rad2_x = new_definition(`rad2_x x1 x2 x3 x4 x5 x6 =
  78         (rho_x x1 x2 x3 x4 x5 x6)/((delta_x x1 x2 x3 x4 x5 x6)*(&4))`);;
  79
  80 (* dih_x', atn2 replaced with atan2 *)
  81 let dih_x' = new_definition(`dih_x' x1 x2 x3 x4 x5 x6 =
  82        let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
  83        let d = delta_x x1 x2 x3 x4 x5 x6 in
  84        pi/ (&2) +  atn2'( (sqrt ((&4) * x1 * d)),--  d_x4)`);;
  85
  86 (* dih_y *)
  87 let dih_y' = new_definition(`dih_y' y1 y2 y3 y4 y5 y6 =
  88        let (x1,x2,x3,x4,x5,x6)= (y1*y1,y2*y2,y3*y3,y4*y4,y5*y5,y6*y6) in
  89        dih_x' x1 x2 x3 x4 x5 x6`);;
  90
  91 (* arclength *)
  92 let arclength' = new_definition(`arclength' a b c =
  93         pi/(&2) + (atn2'( (sqrt (ups_x (a*a) (b*b) (c*c))),(c*c - a*a  -b*b)))`);;
  94
  95 (* sol_x *)
  96 let sol_x' = new_definition(`sol_x' x1 x2 x3 x4 x5 x6 =
  97         (dih_x' x1 x2 x3 x4 x5 x6) +
  98         (dih_x' x2 x3 x1 x5 x6 x4) +  (dih_x' x3 x1 x2 x6 x4 x5) -  pi`);;
  99
 100 (* sol_y *)
 101 let sol_y' = new_definition(`sol_y' y1 y2 y3 y4 y5 y6 =
 102         (dih_y' y1 y2 y3 y4 y5 y6) +
 103         (dih_y' y2 y3 y1 y5 y6 y4) +  (dih_y' y3 y1 y2 y6 y4 y5) -  pi`);;
 104
 105
 106 (* const1 *)
 107 let const1' = new_definition `const1' = sol_y' (&2) (&2) (&2) (&2) (&2) (&2) / pi`;;
 108
 109 (* h0 *)
 110 let h0 = new_definition `h0 = #1.26`;;
 111
 112 (* lfun *)
 113 let lfun = new_definition `lfun h =  (h0 - h)/(h0 - &1)`;;
 114
 115 (* lfun_y1 *)
 116 let lfun_y1 = new_definition `lfun_y1 (y1:real) (y2:real) (y3:real)
 117   (y4:real) (y5:real) (y6:real) =  lfun y1`;;
 118
 119
 120 (* num1 *)
 121 let num1 = new_definition `num1 e1 e2 e3 a2 b2 c2 =
 122    -- &4*((a2 pow 2) *e1 + &8*(b2 - c2)*(e2 - e3) -
 123   a2*(&16*e1 + ( b2 - &8 )*e2 + (c2 - &8)*e3))`;;
 124
 125 (* unit6 *)
 126 let unit6 = define `unit6 x1 x2 x3 x4 x5 x6 = &1`;;
 127
 128 (* arc_hhn *)
 129 let arc_hhn' = new_definition `arc_hhn' =
 130   arclength' (&2 * h0) (&2 * h0) (&2)`;;
 131
 132 (* arclength_y1 *)
 133 let arclength_y1' = new_definition
 134  `arclength_y1' a b
 135   (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
 136   arclength' y1 a b`;;
 137
 138 (* arclength_x1 *)
 139 let arclength_x1' = new_definition
 140  `arclength_x1' a b x1 x2 x3 x4 x5 x6 =
 141   arclength_y1' a b (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
 142
 143 (* arclength_x_123 *)
 144 let arclength_x_123' = new_definition `arclength_x_123'  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 145                 arclength' (sqrt x1) (sqrt x2) (sqrt x3)`;;
 146
 147 (* acs_sqrt_x1_d4 *)
 148 let acs_sqrt_x1_d4 = new_definition `acs_sqrt_x1_d4 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 149   acs (sqrt(x1)/ &4)`;;
 150
 151 let sqrt_x1 = define `sqrt_x1 x1 x2 x3 x4 x5 x6 = sqrt x1`;;
 152
 153 let sqrt_x2 = define `sqrt_x2 x1 x2 x3 x4 x5 x6 = sqrt x2`;;
 154
 155 let sqrt_x3 = define `sqrt_x3 x1 x2 x3 x4 x5 x6 = sqrt x3`;;
 156
 157 let sqrt_x4 = define `sqrt_x4 x1 x2 x3 x4 x5 x6 = sqrt x4`;;
 158
 159 let sqrt_x5 = define `sqrt_x5 x1 x2 x3 x4 x5 x6 = sqrt x5`;;
 160
 161 let sqrt_x6 = define `sqrt_x6 x1 x2 x3 x4 x5 x6 = sqrt x6`;;
 162
 163
 164 (* All definitions in one list *)
 165 let flyspeck_defs = [atn2'; delta_x; delta_y; delta_x4;
 166               ups_x; rho_x; dih_x'; dih_y'; arclength';
 167               sol_x'; sol_y'; const1'; num1; unit6; h0; lfun; lfun_y1;
 168               rad2_x; arc_hhn'; arclength_y1'; arclength_x1'; acs_sqrt_x1_d4;
 169               arclength_x_123'; sqrt_x1; sqrt_x2; sqrt_x3; sqrt_x4; sqrt_x5; sqrt_x6];;
 170
 171
 172
 173 (* A simple function for verifying Flyspeck inequalities *)
 174 let verify_flyspeck_ineq pp ineq_tm =
 175   let conv = REWRITE_CONV ([ineq; IMP_IMP] @ flyspeck_defs) THENC DEPTH_CONV let_CONV in
 176   let eq_th = conv ineq_tm in
 177   let ineq_tm1 = (rand o concl) eq_th in
 178   let th, time = verify_ineq default_params pp ineq_tm1 in
 179     REWRITE_RULE[GSYM eq_th] th, time;;
 180
 181
 182 (* Create a hashtable for saving inequalities *)
 183
 184 type difficulty = Easy | Medium | Hard;;
 185
 186 type flyspeck_example =
 187 {
 188   difficulty : difficulty;
 189   id : string;
 190   ineq_tm : term;
 191 };;
 192
 193 let examples = Hashtbl.create 20;;
 194 let add_example ex =
 195   Hashtbl.add examples ex.id ex;;
 196
 197 (* 2485876245a *)
 198 add_example {id = "2485876245a";
 199              difficulty = Easy;
 200              ineq_tm = `ineq
 201     [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #6.3504;
 202       #3.0 *  #3.0, x5, #2.0 *  #2.52 *  #2.0 *  #2.52;  #4.0,x6, #6.3504]
 203     (delta_x4 x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
 204
 205
 206 (* 4559601669b *)
 207 add_example {id = "4559601669b";
 208              difficulty = Easy;
 209              ineq_tm = `ineq
 210     [ #4.0,x1, #6.3504;  #4.0,x2, #4.0;  #4.0,x3, #6.3504;
 211       #3.01 *  #3.01, x4, #3.01 *  #3.01; #4.0, x5, #6.3504;  #4.0,x6, #4.0]
 212     (delta_x4 x1 x2 x3 x4 x5 x6 < &0)`};;
 213
 214
 215 (* 5512912661 *)
 216 add_example {id = "5512912661";
 217              difficulty = Easy;
 218              ineq_tm = `ineq [&1,x1,&1 + (pi * const1') / pi; &1,x2,&1 + (pi * const1') / pi;
 219                               &1, x3, &1 + (pi * const1') / pi;  #2.38 * #2.38, x4, #3.01 * #3.01;
 220                               &2 * &2, x5, #2.52 *  #2.52;  #3.15 /  #1.26 *  #3.15 /  #1.26,x6, #15.53]
 221     (num1 x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
 222
 223
 224 (* 6843920790 *)
 225 add_example {id = "6843920790";
 226              difficulty = Easy;
 227              ineq_tm = `ineq [&1,x1,&1 + (pi * const1') / pi; &1,x2,&1 + (pi * const1') / pi;
 228                               &1, x3, &1 + (pi * const1') / pi; &2 / #1.26 * &2 / #1.26, x4, #3.01 * #3.01;
 229                               #2.38 *  #2.38, x5, #15.53;  #2.38 *  #2.38,x6, #15.53]
 230     (num1 x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
 231
 232
 233 (* 6096597438a *)
 234 add_example {id = "6096597438a";
 235              difficulty = Easy;
 236              ineq_tm = `ineq [ #1.0,x1, #1.0; &1,x2,&1; &1,x3,&1; &1,x4,&1; &1,x5,&1; &1,x6,&1]
 237     (unit6 x1 x2 x3 x4 x5 x6 *  #0.591 +
 238        unit6 x1 x2 x3 x4 x5 x6 *  #0.0331 * -- &64 +
 239        unit6 x1 x2 x3 x4 x5 x6 *  #0.506 *  #1.26 * &1 / ( #1.26 + -- &1) +
 240        unit6 x1 x2 x3 x4 x5 x6 *  #0.506 * --(&1 / ( #1.26 + -- &1)) +
 241        unit6 x1 x2 x3 x4 x5 x6 *  #1.0 < &0)`};;
 242
 243
 244 (* 4717061266 *)
 245 add_example {id = "4717061266";
 246              difficulty = Easy;
 247              ineq_tm = `ineq
 248     [ #4.0,x1, #2.0 *  #1.26 *  #2.0 *  #1.26;  #4.0, x2, #2.0 *  #1.26 *  #2.0 *  #1.26;
 249       #4.0, x3, #2.0 *  #1.26 *  #2.0 *  #1.26;  #4.0,x4, #2.0 *  #1.26 *  #2.0 *  #1.26;
 250       #4.0, x5, #2.0 *  #1.26 *  #2.0 *  #1.26;  #4.0,x6, #2.0 *  #1.26 *  #2.0 *  #1.26]
 251     (delta_x x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
 252
 253
 254 (* SDCCMGA b *)
 255 add_example {id = "SDCCMGA b";
 256              difficulty = Easy;
 257              ineq_tm = `ineq [ #4.0,x1, #6.3504; &1 * &1,x2,&1 * &1; &1 * &1,x3,&1 * &1;
 258                                &1 * &1, x4, &1 * &1; &1 * &1, x5, &1 * &1; &1 * &1,x6,&1 * &1]
 259     (arclength_x1'  #2.0 ( #2.0 *  #1.26) x1 x2 x3 x4 x5 x6 +
 260        arclength_x1'  #2.0 ( #2.0 *  #1.26) x1 x2 x3 x4 x5 x6 +
 261        arclength_x1' ( #2.0 *  #1.26)  #2.0 x1 x2 x3 x4 x5 x6 * -- &1 +
 262        unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 / &3) +
 263        unit6 x1 x2 x3 x4 x5 x6 * --arc_hhn' < &0)`};;
 264
 265
 266 (* TSKAJXY-TADIAMB *)
 267 add_example {id = "TSKAJXY-TADIAMB";
 268              difficulty = Medium;
 269              ineq_tm = `ineq
 270     [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
 271       #4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
 272     ((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)`};;
 273
 274
 275 (* 7067938795 *)
 276 add_example {id = "7067938795";
 277              difficulty = Medium;
 278              ineq_tm = `ineq [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #4.0;
 279                                #3.01 *  #3.01, x5, #3.24 *  #3.24;  #3.01 *  #3.01,x6, #3.24 *  #3.24]
 280     (dih_x' x1 x2 x3 x4 x5 x6 +
 281        unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 /  #2.0) +
 282        unit6 x1 x2 x3 x4 x5 x6 *  #0.46 <
 283      &0)`};;
 284
 285 (* 5490182221 *)
 286 add_example { id = "5490182221";
 287               difficulty = Medium;
 288               ineq_tm = `ineq
 289     [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #6.3504;
 290       #4.0, x5, #6.3504;  #4.0,x6, #6.3504]
 291     (dih_x' x1 x2 x3 x4 x5 x6 + unit6 x1 x2 x3 x4 x5 x6 * -- #1.893 < &0)`};;
 292
 293
 294
 295 (* 3318775219 *)
 296 add_example { id = "3318775219";
 297               difficulty = Hard;
 298               ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
 299                                &2, y3, #2.52; #2.52, y4, sqrt(&8);
 300                                &2, y5, #2.52; &2, y6, #2.52]
 301     ( ((dih_y' y1 y2 y3 y4 y5 y6) - #1.629 +
 302          (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
 303          (#0.763 * (y4 - #2.52)) -
 304          (#0.315 * (y1 - #2.0))) * (-- &1)  < &0)`};;
 305
 306
 307 (* Tests *)
 308
 309 let run_example id =
 310   id, verify_flyspeck_ineq 4 (Hashtbl.find examples id).ineq_tm;;
 311
 312
 313
 314 let test_easy, test_medium, test_hard =
 315   let run keys = map run_example keys in
 316   let get_keys d0 =
 317     let list = Hashtbl.fold (fun k v acc -> (k, v.difficulty) :: acc) examples [] in
 318       (setify o fst o unzip) (filter (fun (_, d) -> d = d0) list) in
 319     (fun () -> run (get_keys Easy)),
 320   (fun () -> run (get_keys Medium)),
 321   (fun () -> run (get_keys Hard));;
 322
 323
 324 let easy = test_easy();;
 325 (* let medium = test_medium();; *)
 326 (* let hard = test_hard();; *)