text_formalization/nonlinear/scripts.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - CODE INFORMAL                                                   *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                         *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-04-15                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (* Interactive scripts for the running of interval arithmetic code from
  11     ineq.hl,
  12
  13    Execution done in computational_build.hl
  14 *)
  15
  16 (* START NONLINEAR INEQS *)
  17 (* reneeds "nonlinear/ineqdata3q1h.hl";;  *)
  18 (* reneeds "nonlinear/strongdodec_ineq.hl";; *)
  19
  20 flyspeck_needs "leg/enclosed_def.hl";;
  21 flyspeck_needs "general/sphere.hl";;
  22 (* flyspeck_needs "nonlinear/ineq.hl";; *)
  23 flyspeck_needs "nonlinear/main_estimate_ineq.hl";;
  24 (* flyspeck_needs "nonlinear/strongdodec_ineq.hl";; *)
  25
  26 flyspeck_needs "nonlinear/lemma.hl";;
  27 flyspeck_needs "nonlinear/functional_equation.hl";;
  28 flyspeck_needs  "nonlinear/parse_ineq.hl";;
  29 flyspeck_needs "nonlinear/optimize.hl";;
  30 flyspeck_needs "general/flyspeck_lib.hl";;
  31 flyspeck_needs "nonlinear/auto_lib.hl";;
  32 (* flyspeck_needs "../projects_discrete_geom/bcc_lattice.hl";; *)
  33
  34
  35 module Scripts = struct
  36
  37 let idq_of_string s = hd(Ineq.getexact s);;
  38
  39 let expand_string = map (fun t->t.idv) o Ineq.getprefix;;
  40
  41 let isquad s = Optimize.is_quad_cluster (idq_of_string s).tags;;
  42
  43 (*
  44 let finished_splits =
  45   let split_sp = Str.split(Str.regexp "\n") in
  46   let p = process_to_string("grep split "^flyspeck_dir
  47                               ^"/../interval_code/qed_log.txt   "
  48                              ^"| sed  's/^.*ineq./\"/' "
  49                              ^"| sed 's/., secs.*$/\";/'   "
  50                              ^"| sed 's/ split.*$//g' "
  51                              ^"| sed 's/\"//g' "
  52                              ^" | sed 's/;//g' ") in
  53     Parse_ineq.nub (split_sp p);;
  54
  55
  56 let hassplit =
  57   let a = filter (fun t -> List.length (get_split_tags t) > 0)  !Ineq.ineqs in
  58   let a' = filter (fun t -> mem t.id  unfinished_cases) a in
  59     map (fun t-> t.id) a';;
  60 List.length hassplit;;
  61
  62 *)
  63
  64 (* lists of inequality ids *)
  65
  66 let all_cases() =
  67   Parse_ineq.nub (map (fun t -> t.idv) (!Ineq.ineqs));;
  68
  69 let finished_cases() =
  70   let split_sp=  Str.split (Str.regexp "\n") in
  71   let p = process_to_string ("cat "^flyspeck_dir
  72                               ^"/../interval_code/qed_log_2012.txt "
  73                              (* ^"| grep 'Aug 1[67].*2013'  "   *)
  74                              ^"| sed 's!^//.*$!!'"
  75                              ^"| sed  's/^.*ineq(/\"/' "
  76                              ^"| sed 's/., secs.*$/\";/'   "
  77                              ^"| sed 's/ split(.*$//g' "
  78                              ^"| sed 's/\"//g' "
  79                              ^" | sed 's/;//g' ") in
  80     Parse_ineq.nub (split_sp p);;
  81
  82
  83 let unfinished_cases() = subtract (all_cases()) (finished_cases());;
  84
  85 let dodec_cases =
  86   let isdodec s = (mem Strongdodec (idq_of_string s).tags) in
  87     filter isdodec (all_cases());;
  88
  89
  90 (* *************************************************************************** *)
  91 (* C++ interval verification *)
  92 (* *************************************************************************** *)
  93
  94 let disregard =
  95    [
  96 "9563139965D"; (* derived lp, disregard it *)
  97   ] ;;
  98
  99 let special_concerns = [
 100 (* deprecated  "2065952723 A1";  *) (* requires special code, FAILS ON THACKMAC. *)
 101    ];;
 102
 103 let nocompile =
 104   [
 105 (* deprecated "2065952723 A1";
 106   "5556646409";"4322269127"; (* LC functions *)
 107   "5512912661"; "6843920790"; "4828966562"; (* num1 *) *)
 108 ] @ disregard;;
 109
 110 let testids = ref[];;
 111
 112 (*
 113 let view nth = idq_of_string (List.nth !testids nth);;
 114 idq_fields(view 0);;
 115 view 1;;
 116 *)
 117
 118 (* running one id *)
 119
 120 (*
 121 let testid =   "FXZXPNS";;
 122 Optimize.testsplit false testid;;
 123 map (Optimize.testsplit true) !testids;;
 124 *)
 125
 126 (* map (Auto_lib.testsplit true) (!testids);; *)
 127
 128 let execute_interval_cases cases bool =
 129 (*  let isquad s = Optimize.is_quad_cluster (idq_of_string s).tags in
 130   let nonquad  = filter (not o isquad) cases in  *)
 131   map (fun t -> try (Auto_lib.testsplit bool t) with Failure _ -> [()]) cases;;
 132
 133 let execute_interval_allbutdodec bool =
 134   execute_interval_cases (subtract (all_cases()) (union disregard dodec_cases)) bool;;
 135
 136 let execute_interval_all bool =
 137   execute_interval_cases (subtract (all_cases()) (disregard)) bool;;
 138
 139 (* execute_interval_allbutdodec true;; *)
 140 (* goal *)
 141
 142 (* open Optimize;; *)
 143
 144 let process_cases_testid testid =
 145   let idq =  idq_of_string testid in
 146   let (s,tags,ineq) = Optimize.idq_fields idq in
 147   let ls = Optimize.get_split_tags idq in
 148    if (ls=[]) then (s,tags,ineq) else
 149      let cases = Optimize.split_all_h0 [(ineq,ls)] in
 150        (s^" case-",tags,List.nth cases 1);;
 151
 152 let interactive_debug_stuff testid =
 153   let (id,tags,case) = process_cases_testid testid in
 154   let ife b t = e(if b then t else ALL_TAC) in
 155   let is_xconvert = mem Xconvert tags in
 156   let is_branch = mem Branching tags in
 157   let _ = g (mk_imp (`NONLIN`,case)) in
 158   let _ = e(Optimize.PRELIM_REWRITE_TAC) in
 159   let _ = ife (is_branch) Optimize.BRANCH_TAC in
 160   let _ = ife (is_xconvert) Optimize.X_OF_Y_TAC in
 161   let _ = ife (is_branch && not(is_xconvert))
 162     (Optimize.SERIES3Q1H_5D_TAC) in
 163   let _ = e (Optimize.STYLIZE_TAC) in
 164     e (Optimize.WRAPUP_TAC);;
 165
 166 (* *************************************************************************** *)
 167 (* TESTING CFSQP *)
 168 (* *************************************************************************** *)
 169
 170
 171 let one_cfsqp  =
 172   Parse_ineq.execute_cfsqp o idq_of_string;;
 173
 174 let cfsqp ts =
 175   let us = map (idq_of_string) ts in
 176   !(Parse_ineq.execute_cfsqp_list us);;
 177
 178 let execute_cfsqp() = cfsqp (all_cases());;
 179
 180 (* *************************************************************************** *)
 181 (* Timing *)
 182 (* *************************************************************************** *)
 183
 184 let rec finalize = function (* use time from most recent verification *)
 185   | [] -> []
 186   | (x,t)::vs -> if (exists (fun (x',_) -> (x'=x)) vs) then finalize vs
 187     else  (x,t)::(finalize vs);;
 188
 189 let total r =
 190   let rr = map snd r in
 191     end_itlist (+) rr;;
 192
 193 let hour r = float_of_int r /. (60.0 *. 60.0);;
 194
 195 let finished_times,finished_rejects =
 196   let split_sp = Str.split (Str.regexp "\n") in
 197   let split_semi = Str.split (Str.regexp ";") in
 198   let int_s [x;y] = try
 199     (x,int_of_string y)
 200   with Failure s -> failwith (s ^ " " ^ x ^ " " ^ y)
 201   in
 202   let p = process_to_string ("cat "^flyspeck_dir
 203                               ^"/../interval_code/qed_log_2012.txt   "
 204                              (* ^"| grep 'Aug 1[67].*2013'  " *)
 205                               ^"| sed 's!^//.*$!!'"
 206                              ^"| sed  's/^.*ineq(//' "
 207                              ^"| sed 's/., svn.*$//'   "
 208                               ^" | sed 's/., *msecs.*$//' "
 209                              ^"| sed 's/., *cell.*$//'   "
 210                               ^"| sed 's/., secs./;/' "
 211                              ) in
 212   let (accept,rejects) = partition (fun t -> List.length t =2)
 213                  (map split_semi (split_sp p)) in
 214      (map int_s accept,Parse_ineq.nub rejects);;
 215
 216 let finished_times_msecs,finished_rejects_msecs =
 217   let split_sp = Str.split (Str.regexp "\n") in
 218   let split_semi = Str.split (Str.regexp ";") in
 219   let int_s [x;y] = try
 220     (x,int_of_string y)
 221   with Failure s -> failwith (s ^ " " ^ x ^ " " ^ y)
 222   in
 223   let p = process_to_string ("grep msecs "^flyspeck_dir
 224                               ^"/../interval_code/qed_log_2012.txt   "
 225                               ^"| sed 's!^//.*$!!'"
 226                              ^"| sed  's/^.*ineq(//' "
 227                              ^"| sed 's/., *cell.*$/;/'   "
 228                               ^"| sed 's/., secs.[0-9]*//' "
 229                               ^"| sed 's/., *msecs./;/' "
 230                              ) in
 231   let (accept,rejects) = partition (fun t -> List.length t =2)
 232                  (map split_semi (split_sp p)) in
 233      (map int_s accept,Parse_ineq.nub rejects);;
 234
 235
 236 let times =
 237   let all = all_cases() in
 238   let ft = finalize finished_times in
 239   let split = Str.split(Str.regexp " +split") in
 240   let fti = filter (fun (x,_) -> mem (hd (split x)) all) ft in
 241     sort (fun (_,y) (_,y') -> (y>y')) fti;;
 242
 243 let fast_cases = filter (fun (_,t) -> t<=5) times;;
 244
 245 (*
 246 hour (total times);;
 247
 248
 249
 250 hour(total(filter (fun (t,_) ->
 251                      Str.string_match (Str.regexp "QITNPEA 4003") t 0) times));;
 252
 253 hour (total (filter (fun (t,_) ->
 254                        Str.string_match (Str.regexp "ZTGIJCF23") t 0) times));;
 255 *)
 256
 257 (* *************************************************************************** *)
 258 (* splits, test for missing cases, -- none found! may 27, 2011 *)
 259 (* *************************************************************************** *)
 260
 261 let case_splits ls =
 262   let split = Str.split(Str.regexp " +split") in
 263   let ss = map split ls in
 264   let ss2 = filter (fun t-> List.length t  = 2) ss in
 265   let pair bs = (List.nth bs 0,List.nth bs 1) in
 266   let nodigit = Str.split(Str.regexp "[^0-9]") in
 267   let digitize s =  map int_of_string (nodigit s) in
 268   let f  = function      | b::bs  ->    (b,pair (unions (map digitize bs)))
 269     | _ -> failwith "case_splits" in
 270     map f ss2;;
 271
 272 let rec unify_splits = function
 273   | [] -> []
 274   | (s,(_,t)):: _ as ys -> let (st,xs') = partition (fun (s',(_,t')) -> (s'=s & t'=t)) ys in
 275        (s,Parse_ineq.nub (map (fun (_,(r',_ )) -> r') st),t) ::unify_splits xs';;
 276
 277 let case_splits_execute =
 278       let vv = unify_splits (case_splits (map fst finished_times)) in
 279         filter (fun (_,ls,r) -> not ((0--(r-1)) = sort (<) ls)) vv;;
 280
 281
 282
 283 (* *************************************************************************** *)
 284 (* inventory of which inequalities actually get used in the proof *)
 285 (* *************************************************************************** *)
 286
 287     let flyspeck_used_ineqs =
 288       (* Merge_ineq.tsk_hyp *)
 289       ["TSKAJXY-GXSABWC DIV"; "TSKAJXY-IYOUOBF sharp v2";
 290              "TSKAJXY-IYOUOBF sym";
 291    "TSKAJXY-RIBCYXU sharp"; "TSKAJXY-RIBCYXU sym"; "TSKAJXY-TADIAMB";
 292    "TSKAJXY-WKGUESB sym"; "TSKAJXY-XLLIPLS"; "TSKAJXY-delta_x4";
 293    "TSKAJXY-eulerA"] @
 294
 295         Merge_ineq.ztg4_ineqs @
 296
 297         (* Merge_ineq.cell3_hyp *)
 298
 299         ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";
 300               "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW"] @
 301
 302         (* Merge_ineq.CRKIBMP *)
 303
 304         ["GRKIBMP A V2"; "GRKIBMP B V2"] @
 305
 306         (* Mege_ineq.g_quqya_goal *)
 307
 308          ["FHBVYXZ a";"FHBVYXZ b";"FWGKMBZ"] @
 309
 310         (* Merge_ineq.gamma10_gamma11_concl *)
 311
 312         ["GLFVCVK4 2477216213";"QITNPEA  5400790175 a";"QITNPEA  5400790175 b";"FWGKMBZ"] @
 313
 314         (* Merge_ineq.gamma23_full8_x_gamma *)
 315
 316         ["GRKIBMP A V2"] @
 317
 318         (* Merge_ineq.cell3_008 *)
 319         [             "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM"] @
 320
 321         (* Merge_ineq.gamma23_keep135_x_gamma *)
 322         ["GRKIBMP A V2"] @
 323
 324         Merge_ineq.QITNPEA1_9063653052_hypl @
 325
 326         Merge_ineq.g_qxd_hypl @
 327
 328         Merge_ineq.gamma_qx_hypl @
 329
 330         (* Merge_ineq.ox *)
 331 (*      (map (fun t -> t.idv) (Ineq.getprefix "OXLZLEZ 6346351218")) @ *)
 332
 333         (* Merge_ineq: *)
 334         (map (fun t -> t.idv) (filter Merge_ineq.is_ox3q1h (!Ineq.ineqs))) @
 335
 336         (* packing chapter, TSK and OXL *)
 337         (map (fun t -> t.idv) Merge_ineq.packing_ineq_data) @
 338
 339         (* TameGeneral *)
 340         ["5735387903"; "5490182221"] @
 341
 342         (* Pent_hex.get_ineq *)
 343
 344           (map (fun t -> t.idv) (Ineq.getprefix "7550003505")) @
 345
 346         (* Parse_ineq.lpstring () : *)
 347
 348           (map (fun t -> t.idv) (Ineq.getfield Lp)) @
 349           (map (fun t -> t.idv) (Ineq.getfield Lpsymmetry)) @
 350
 351         (* Lp_details *)
 352          ["5584033259";"6170936724";"5691615370"] @
 353         ["6170936724";"8673686234 a";"8673686234 b";"8673686234 c"] @
 354
 355         (* Yssqoy *)
 356         (let has_packid = (fun t -> not(intersect ["UKBRPFE";"WAZLDCD";"BIEFJHU"] (Ineq.flypaper_ids t) = [])) in
 357          let idl = (filter has_packid !Ineq.ineqs) in
 358                   (map (fun t -> t.idv) idl)) @
 359
 360
 361         (* Terminal, Pent_hex :
 362         grep get_main_nonlinear local/*.hl | sed 's/^.*get_main_nonlinear//g' | sed 's/").*$/";/g' *)
 363         [ "7439076204";
 364  "7439076204";
 365  "7439076204";
 366  "1834976363";
 367  "4828966562";
 368  "6843920790";
 369  "1117202051";
 370  "1117202051";
 371  "4559601669";
 372  "4559601669";
 373  "4559601669b";
 374  "4559601669b";
 375  "4821120729";
 376  "6459846571";
 377  "2485876245a";
 378  "7175074394";
 379  "6789182745";
 380  "4887115291";
 381  "2125338128";
 382  "2314572187";
 383  "7796879304";
 384  "1347067436";
 385  "6601228004";
 386  "3078028960";
 387  "3078028960";
 388  "3078028960";
 389  "5546286427";
 390  "3665919985";
 391  "3665919985";
 392  "7903347843";
 393  "7997589055";
 394  "2565248885";
 395  "2320951108";
 396  "5429238960";
 397  "1948775510";
 398  "3665919985";
 399  "5708641738";
 400  "1008824382";
 401  "1586903463";
 402  "8875146520";
 403  "6877738680";
 404  "9692636487";
 405  "2485876245b";
 406  "6762190381";
 407  "8346775862";
 408  "8631418063";
 409  "8631418063";
 410  "4821120729";
 411  "5202826650 a";
 412  "OMKYNLT 3336871894";
 413  "OMKYNLT 3336871894";
 414  "4010906068";
 415  "4010906068";
 416  "6833979866";
 417  "5541487347";
 418  "4528012043";
 419  "7459553847";
 420  "4143829594";
 421  "1080462150";
 422  "9816718044";
 423  "3106201101";
 424  "2200527225";
 425  "2900061606";
 426  "7097350062a";
 427  "OMKYNLT 1 2";
 428  "7645170609";
 429  "OMKYNLT 2 1";
 430  "7881254908";
 431  "5026777310a";
 432  "7720405539";
 433  "2739661360";
 434  "4922521904";
 435  "2468307358";
 436  "2739661360";
 437  "3603097872";
 438  "3603097872";
 439  "3603097872";
 440  "3603097872";
 441  "5405130650";
 442  "5766053833";
 443  "5691615370";
 444  "9563139965 d";
 445  "9563139965 d";
 446  "9563139965 f";
 447  "9563139965 f";
 448  "9563139965 e";
 449  "9563139965 e";
 450  "9563139965 e";
 451  "9563139965 e";
 452  "4680581274 delta top issue";
 453  "4559601669";
 454  "4680581274 delta issue";
 455  "4680581274 a";
 456  "7697147739 delta top issue";
 457  "4559601669";
 458  "7697147739 delta issue";
 459  "7697147739 a";
 460  "5405130650";
 461  "3603097872";
 462  "9096461391";
 463  "2445657182"];;
 464
 465     let all_ineqs = map (fun t -> t.idv) (!Ineq.ineqs);;
 466     let remain_to_be_used = Flyspeck_lib.nub (sort (<) (subtract all_ineqs flyspeck_used_ineqs));;
 467
 468
 469  end;;
 470
 471
 472 (* October, 2012 *)
 473
 474 (* generate file prep.hl of all preprocessed inequalities. *)
 475
 476 (* edit "#" -> " #" in printer.ml to defuse "--#0.02" bug *)
 477 (* needs "printer.ml";; *)
 478
 479 module Preprocess = struct
 480   open Scripts;;
 481
 482 (*  let add_inequality _ = ();; *)
 483
 484   let ineq = Sphere.ineq;;
 485   let print_tag t = match t with
 486   | Branching -> "Branching"
 487   | Sharp  -> "Sharp"
 488   | Disallow_derivatives  -> "Disallow_derivatives"
 489   | Onlycheckderiv1negative -> "Onlycheckderiv1negative"
 490   | Dim_red -> "Dim_red"
 491   | Dim_red_backsym -> "Dim_red_backsym"
 492   | Quad_cluster f -> "Quad_cluster "^(string_of_float f)
 493   | Set_rad2 -> "Set_rad2"
 494   | Delta126min f -> "Delta126min "^(string_of_float f)
 495   | Delta126max f -> "Delta126max "^(string_of_float f)
 496   | Widthcutoff f -> "Widthcutoff "^(string_of_float f)
 497   | Delta135min f -> "Delta135min "^(string_of_float f)
 498   | Delta135max f -> "Delta126max "^(string_of_float f)
 499   | _ -> ""
 500   ;;
 501
 502   let print_one (s,tgl,ii) =
 503     let p = Printf.sprintf in
 504     let tgs = filter (fun s -> not(s="")) (map print_tag tgl) in
 505     let jsemi  = Flyspeck_lib.unsplit ";" (fun x-> x) in
 506     let tl = jsemi tgs in
 507     let is = print_to_string pp_print_qterm (Sphere.all_forall ii) in
 508        Flyspeck_lib.join_lines [
 509       "add_inequality  { ";
 510       p "  idv= \"%s\";" s;
 511       "  doc=\"\";";
 512       p "  tags= [%s];" tl;
 513       p "  ineq= %s;" is;
 514       p "};;\n\n";
 515     ];;
 516
 517   let preprocess1 s =
 518     let prep =  (Optimize.preprocess_split_idq
 519                      (hd (Ineq.getexact  (s)))) in
 520     let v =
 521     Flyspeck_lib.join_lines (map print_one prep) in
 522     let _ = report v in
 523       ((s,map (fun (s,_,_) -> s) prep),v);;
 524
 525   (* return the association list of idv -> list of new idv *)
 526   let preprocess filename =
 527     let cc = subtract (all_cases()) (disregard) in
 528     let header = "(* Auto generated file of preprocessed  inequalities. See Scripts.exec *)\n\n" in
 529     let h1 = "(* "^flyspeck_version()^"\n   "^build_date() ^"*)\n\n" in
 530     let h2 = "(* need to defuse --# in printer.ml *)\n\n" in
 531     let h3 = "module Prep = struct\n\n"^
 532       "let prep_ineqs = ref ([]:ineq_datum list);;\n\n "^
 533       "let add_inequality i  = \n"^
 534       "let _ = prep_ineqs:= i :: !prep_ineqs in\n"^
 535       "  ();;\n\n" in
 536     let p = map preprocess1 cc in
 537     let v = Flyspeck_lib.join_lines (map snd p) in
 538     let e = "\n\nend;;" in
 539     let _ = Flyspeck_lib.output_filestring filename (header^h1^h2^h3^v^e) in
 540       map fst p;;
 541
 542   let prep_file = Filename.temp_file "prep" ".hl";;
 543
 544   let exec()=  preprocess prep_file;;
 545 (*  exec();; needs prep_file;; *)
 546
 547 end;;