formal_lp/hypermap/main/test6.hl

   1 needs "../formal_lp/hypermap/main/prove_flyspeck_lp.hl";;
   2
   3
   4 open Flyspeck_lp;;
   5 open Lp_ineqs;;
   6 open Lp_certificate;;
   7 open List_hypermap_computations;;
   8 open List;;
   9 open Lp_informal_computations;;
  10 open Prove_lp;;
  11 open Arith_misc;;
  12 open List_conversions;;
  13 open Lp_main_estimate;;
  14 open Lp_ineqs_proofs;;
  15 open Misc_vars;;
  16
  17 init_ineqs();;
  18
  19
  20 (**************************)
  21
  22 let cert3_file = "/mnt/Repository/formal_lp/glpk/binary/c3.dat";;
  23 let c3 = hd (read_lp_certificates cert3_file);;
  24
  25 let cert4_file = "/mnt/Repository/formal_lp/glpk/binary/c4.dat";;
  26 let c4 = hd (read_lp_certificates cert4_file);;
  27
  28 let cert5_file = "/mnt/Repository/formal_lp/glpk/binary/c5.dat";;
  29 let c5 = hd (read_lp_certificates cert5_file);;
  30
  31 let binary_dir = "/mnt/Repository/formal_lp/glpk/binary";;
  32 let files = map (fun i -> sprintf "%s/c5_%d.dat" binary_dir i) (0--4);;
  33 let cs = map (hd o read_lp_certificates) files;;
  34
  35 let cert = nth cs 4;;
  36 case_info cert.root_case;;
  37 convert_to_list cert.hypermap_string;;
  38 verify_lp_certificate cert;;
  39
  40
  41 let cert = c3;;
  42 let hyp_list = (to_num o create_hol_list o snd o convert_to_list) cert.hypermap_string;;
  43 let base_ineqs, cs = get_terminal_cases cert;;
  44 length cs;;
  45
  46
  47 let th1 = test_terminal (nth cs 4);;
  48 let th2 = INST[`E2:(real^3->bool)->bool`, e_cap_var] th1;;
  49 let th3 = itlist MY_PROVE_HYP base_ineqs th2;;
  50 let th4 = ABBREV_RULE "L" hyp_list th3;;
  51
  52 (****************)
  53
  54 verify_lp_certificate c3;;
  55 verify_lp_certificate c4;;
  56 verify_lp_certificate c5;;
  57
  58 (* 100: 10.671 *)
  59 test 1 (verify_lp_case base_ineqs true) (arg, c4.root_case);;
  60
  61 (* 100: 85.464 *)
  62 test 1 verify_lp_certificate c3;;
  63 (* 100: 10.851 *)
  64 test 1 verify_lp_certificate c4;;
  65 (* 100: 24.318 *)
  66 test 1 verify_lp_certificate c5;;
  67 (* 100: 31.674 *)
  68 test 1 verify_lp_certificate c6;;