formal_lp/hypermap/main/test_hard.hl

   1 needs "../formal_lp/hypermap/main/prove_flyspeck_lp.hl";;
   2
   3 open List;;
   4 open Arith_misc;;
   5 open Linear_function;;
   6 open Prove_lp;;
   7 open Arith_nat;;
   8 open Misc_vars;;
   9 open List_hypermap_computations;;
  10 open List_conversions;;
  11 open Lp_approx_ineqs;;
  12 open Lp_ineqs;;
  13 open Lp_certificate;;
  14 open Lp_informal_computations;;
  15 open Lp_ineqs_proofs;;
  16 open Lp_main_estimate;;
  17 open Flyspeck_lp;;
  18
  19
  20 let dir = "/mnt/Repository/formal_lp/glpk/binary";;
  21
  22 let get_files_with_prefix dir prefix =
  23   let files = Array.to_list (Sys.readdir dir) in
  24   let n = String.length prefix in
  25   let files1 = filter (fun f -> String.length f >= n) files in
  26   let files2 = filter (fun f -> String.sub f 0 n = prefix) files1 in
  27     map (fun f -> sprintf "%s/%s" dir f) files2;;
  28
  29
  30
  31 exception Debug_exception of (lp_verification_arg * split_case * lp_certificate_case list * thm list);;
  32
  33 (***************************)
  34
  35 (* Generate |- 6.25 <= a + b + c and symmetric inequalities when 2.25 <= a *)
  36 let gen_add_big_ineqs =
  37   let c625 = `#6.25` in
  38   let sym_big = (SPEC c625 o ARITH_RULE) `!c. c <= x + y + z ==> c <= y + z + x /\ c <= z + x + y` in
  39   let big_extra = (SPEC `d:num#num` o REWRITE_RULE[GSYM ALL_MEM] o gen_list_ineq true) Lp_ineqs_proofs2.extra_ineq_std3_big in
  40     fun (hyp_set, hyp_fun) arg split_face ->
  41       let d_tm = mk_dart split_face 0 1 in
  42       let set_th = hyp_set "list_of_darts3" in
  43       let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair d_tm)) in
  44       let th0 = INST[arg.hyp_list_tm, l_cap_var; d_tm, d_var_pair; arg.e_tm, e_cap_var] big_extra in
  45       let big_th = (CONV_RULE (convert_condition hyp_fun) o MY_PROVE_HYP arg.lp_cond_th o UNDISCH o MP th0) mem_th in
  46       let x_tm, yz_tms = dest_binary "real_add" (rand (concl big_th)) in
  47       let y_tm, z_tm = dest_binary "real_add" yz_tms in
  48       let inst_list = zip [x_tm; y_tm; z_tm] [x_var_real; y_var_real; z_var_real] in
  49         big_th :: CONJUNCTS (MP (INST inst_list sym_big) big_th);;
  50
  51
  52 (* Generates extra inequalities in the case when 2.18 <= yn(i) and 2.18 <= yn(j) for ~(i = j) *)
  53 let gen_mid_ineqs =
  54   let eq13 = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `13` in
  55   let lnsum13_mid_lemma = (REWRITE_RULE[GSYM IMP_IMP; eq13; Seq.size] o
  56                              SPEC_ALL o add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum13_mid in
  57     fun (hyp_set, hyp_fun) arg split_face ->
  58       let i_tm = mk_raw_num (nth split_face 0) in
  59       let j_tm = mk_raw_num (nth split_face 1) in
  60       let th0 = (MY_PROVE_HYP arg.lp_cond_th o
  61                    INST[arg.e_tm, e_cap_var; arg.hyp_list_tm, l_cap_var; i_tm, i_var_num; j_tm, j_var_num]) lnsum13_mid_lemma in
  62       let els_eq_th = hyp_set "list_of_elements" in
  63       let els_tm = rand (concl els_eq_th) in
  64       let indices =
  65         let list = dest_list els_tm in
  66         let i_ind = index i_tm list and
  67             j_ind = index j_tm list in
  68           subtract (0--(length list - 1)) [i_ind; j_ind] in
  69       let th1 = EQ_MP (term_rewrite (concl th0) els_eq_th) th0 in
  70       let th2 = (prove_conditions o simplify_ineq hyp_fun) th1 in
  71       let mem_i = EQT_ELIM (eval_mem_univ raw_eq_hash_conv i_tm els_tm) and
  72           mem_j = EQT_ELIM (eval_mem_univ raw_eq_hash_conv j_tm els_tm) in
  73       let ths = CONJUNCTS (MY_PROVE_HYP mem_i (MY_PROVE_HYP mem_j th2)) in
  74       let lo_th = nth ths 0 and
  75           hi_th1 = nth ths 1 and
  76           hi_th2 = nth ths 2 in
  77       let lo_ineqs1 = select_all lo_th indices in
  78       let lo_ineqs2 = map (prove_conditions o MY_BETA_RULE) lo_ineqs1 in
  79       let ineqs = hi_th1 :: hi_th2 :: lo_ineqs2 in
  80         ineqs @ flatten (map gen_extra_ineqs ineqs);;
  81
  82
  83 (* Generates extra inequalities in the case when 2.36 <= yn(i) *)
  84 let gen_high_ineqs =
  85   let eq13 = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `13` in
  86   let lnsum13_high_lemma = (REWRITE_RULE[GSYM IMP_IMP; eq13; Seq.size] o
  87                               SPEC_ALL o add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum13_high in
  88     fun (hyp_set, hyp_fun) arg split_face ->
  89       let i_tm = mk_raw_num (nth split_face 0) in
  90       let th0 = (MY_PROVE_HYP arg.lp_cond_th o
  91                    INST[arg.e_tm, e_cap_var; arg.hyp_list_tm, l_cap_var; i_tm, i_var_num]) lnsum13_high_lemma in
  92       let els_eq_th = hyp_set "list_of_elements" in
  93       let els_tm = rand (concl els_eq_th) in
  94       let indices =
  95         let list = dest_list els_tm in
  96         let i_ind = index i_tm list in
  97           subtract (0--(length list - 1)) [i_ind] in
  98       let th1 = EQ_MP (term_rewrite (concl th0) els_eq_th) th0 in
  99       let th2 = (prove_conditions o simplify_ineq hyp_fun) th1 in
 100       let mem_i = EQT_ELIM (eval_mem_univ raw_eq_hash_conv i_tm els_tm) in
 101       let lo_th = MY_PROVE_HYP mem_i th2 in
 102       let lo_ineqs1 = select_all lo_th indices in
 103       let ineqs = map (prove_conditions o MY_BETA_RULE) lo_ineqs1 in
 104         ineqs @ flatten (map gen_extra_ineqs ineqs);;
 105
 106
 107 let set_report, reset_progress, next_terminal, report_progress =
 108   let t = ref 0 in
 109   let flag = ref true in
 110     (fun b -> flag := b),
 111     (fun () -> t := 0),
 112   (fun () -> t := !t + 1),
 113   (fun () -> if !flag then (Format.print_string (sprintf "%d " !t); Format.print_flush()) else ());;
 114
 115
 116 let compute_hypermap arg =
 117   if arg.hyp_data = [] then
 118     let good_th = MATCH_MP lp_cond_imp_good_list arg.lp_cond_th in
 119     let hyp_data = compute_all arg.hyp_list_tm (Some good_th) in
 120       {arg with hyp_data = [hyp_data]}, hyp_data
 121   else
 122     arg, hd arg.hyp_data;;
 123
 124
 125 (* Verifies an lp_certificate_case *)
 126 let rec verify_lp_case base_ineqs std_flag (arg, case) =
 127   match case with
 128       (* Terminal case *)
 129     | Lp_terminal terminal ->
 130         let _ = next_terminal() in
 131         let hyp_set, hyp_fun = snd (compute_hypermap arg) in
 132         let r = (fun name, ind, v -> name, ind, map mk_real_int64 v) in
 133         let c = map r terminal.constraints and
 134             tv = map r terminal.target_variables and
 135             vb = map r terminal.variable_bounds in
 136         let th0 = prove_flyspeck_lp_step1 arg.hyp_list_tm hyp_set hyp_fun std_flag terminal.precision terminal.infeasible c tv vb in
 137         let _ = report_progress() in
 138         let th1 = (MY_PROVE_HYP arg.lp_tau_th o INST[arg.e_tm, e_cap_var]) th0 in
 139         let th2 = if std_flag then MY_PROVE_HYP estd_refl th1 else itlist MY_PROVE_HYP base_ineqs th1 in
 140           (MY_PROVE_HYP arg.lp_cond_th) th2
 141     | Lp_split (info, cs) ->
 142         (match info.split_type with
 143            | "tri" ->
 144                verify_split3 base_ineqs std_flag arg info cs
 145            | "quad" ->
 146                verify_split4 base_ineqs std_flag arg info cs
 147            | "pent" ->
 148                verify_split5 base_ineqs std_flag arg info cs
 149            | "hex" ->
 150                verify_split6 base_ineqs std_flag arg info cs
 151            | "edge" ->
 152                verify_edge base_ineqs std_flag arg info cs
 153            | "218" ->
 154                verify_218 base_ineqs std_flag arg info cs
 155            | "236" ->
 156                verify_236 base_ineqs std_flag arg info cs
 157            | "mid" ->
 158                verify_mid base_ineqs std_flag arg info cs
 159            | "high" ->
 160                verify_high base_ineqs std_flag arg info cs
 161            | "add_big" ->
 162                verify_add_big base_ineqs std_flag arg info cs
 163            | s -> failwith ("verify_lp_case: unknown case " ^ s))
 164
 165 (* Adds a new big triangle if one of its edges is >= #2.25 *)
 166 and verify_add_big base_ineqs std_flag arg info cs =
 167   let arg, hyp_data = compute_hypermap arg in
 168   let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
 169   let ineqs = gen_add_big_ineqs hyp_data arg info.split_face in
 170     itlist MY_PROVE_HYP ineqs case
 171
 172 (* Adds additional node inequalities *)
 173 and verify_mid base_ineqs std_flag arg info cs =
 174   let arg, hyp_data = compute_hypermap arg in
 175   let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
 176   let ineqs = gen_mid_ineqs hyp_data arg info.split_face in
 177     itlist MY_PROVE_HYP ineqs case
 178
 179 (* Adds additional node inequalities *)
 180 and verify_high base_ineqs std_flag arg info cs =
 181   let arg, hyp_data = compute_hypermap arg in
 182   let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
 183   let ineqs = gen_high_ineqs hyp_data arg info.split_face in
 184     itlist MY_PROVE_HYP ineqs case
 185
 186 (* Nodes: 2.18 <= yn(i) \/ yn(i) <= 2.18 *)
 187 and verify_218 base_ineqs std_flag arg info cs =
 188   let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
 189   let split_th = INST[mk_raw_num (hd info.split_face), i_var_num] split218_lemma in
 190   let split_cases = striplist dest_disj (concl split_th) in
 191   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 192   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 193     final_th
 194
 195 (* Nodes: yn(i) <= 2.36 \/ 2.36 <= yn(i) *)
 196 and verify_236 base_ineqs std_flag arg info cs =
 197   let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
 198   let split_th = INST[mk_raw_num (hd info.split_face), i_var_num] split236_lemma in
 199   let split_cases = striplist dest_disj (concl split_th) in
 200   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 201   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 202     final_th
 203
 204 (* Edges: 2.25 <= ye(d) \/ ye(d) <= 2.25 *)
 205 and verify_edge base_ineqs std_flag arg info cs =
 206   let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
 207   let split_th = INST[mk_dart info.split_face 0 1, d_var_pair] split225_lemma in
 208   let split_cases = striplist dest_disj (concl split_th) in
 209   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 210   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 211     final_th
 212
 213 (* Triangle *)
 214 and verify_split3 base_ineqs std_flag arg info cs =
 215   let arg, hyp_data = compute_hypermap arg in
 216     (* Prove all subcases *)
 217   let case1_th = verify_lp_case base_ineqs std_flag (arg, nth cs 0) and
 218       case2_th = verify_lp_case base_ineqs std_flag (arg, nth cs 1) in
 219     (* Combine subcases *)
 220   let split_th, (case1_tm, case2_tm), (case1_ineqs, case2_ineqs) = gen_triangle_ineqs hyp_data arg info.split_face in
 221   let th1 = DISCH case1_tm (itlist MY_PROVE_HYP case1_ineqs case1_th) and
 222       th2 = DISCH case2_tm (itlist MY_PROVE_HYP case2_ineqs case2_th) in
 223   let final_th = MP (combine_cases th1 th2) split_th in
 224     final_th
 225
 226 (* Quad *)
 227 and verify_split4 base_ineqs std_flag arg info cs =
 228   let d13_tm = mk_dart info.split_face 1 2 and
 229       d24_tm = mk_dart info.split_face 0 1 and
 230       diag1_tm = mk_dart info.split_face 0 2 and
 231       diag2_tm = mk_dart info.split_face 1 3 in
 232     (* compute lp_cond *)
 233   let (split13_tm, e13), lp_cond13 = split_lp_conditions arg.hyp_list_tm arg.lp_cond_th d13_tm and
 234       (split24_tm, e24), lp_cond24 = split_lp_conditions arg.hyp_list_tm arg.lp_cond_th d24_tm in
 235     (* compute lp_tau *)
 236   let arg, hyp_data = compute_hypermap arg in
 237   let tau13 = get_tau_split_th tau_split4 hyp_data arg d13_tm and
 238       tau24 = get_tau_split_th tau_split4 hyp_data arg d24_tm in
 239     (* Prove all subcases *)
 240   let arg13 = {arg with hyp_data = []; lp_cond_th = lp_cond13; lp_tau_th = tau13; hyp_list_tm = split13_tm; e_tm = e13} and
 241       arg24 = {arg with hyp_data = []; lp_cond_th = lp_cond24; lp_tau_th = tau24; hyp_list_tm = split24_tm; e_tm = e24} in
 242   let args = zip [arg13; arg24; arg13; arg24; arg] cs in
 243   let cases = map2 (verify_lp_case base_ineqs) [false; false; false; false; std_flag] args in
 244     (* Combine subcases *)
 245   let split_th = INST[diag1_tm, nth diag_vars 1; diag2_tm, nth diag_vars 2] split4_lemma in
 246   let split_cases = striplist dest_disj (concl split_th) in
 247   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 248   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 249     final_th
 250
 251 (* Pent *)
 252 and verify_split5 base_ineqs std_flag arg info cs =
 253   let dart_tms = rotateL 1 (mk_all_darts info.split_face) in
 254   let lp_conds_one = map (split_lp_conditions arg.hyp_list_tm arg.lp_cond_th) dart_tms in
 255   let lp_conds_two = map2 (fun ((list1, _), cond1) d_tm -> split_lp_conditions list1 cond1 d_tm) lp_conds_one (rotateL 2 dart_tms) in
 256     (* compute lp_tau_th *)
 257   let arg, (hyp_set, hyp_fun) = compute_hypermap arg in
 258   let tau_ths_one = map (get_tau_split_th tau_split5_one (hyp_set, hyp_fun) arg) dart_tms in
 259   let tau_ths_two =
 260     let ths = map (get_tau_split_th tau_split5_two (hyp_set, hyp_fun) arg) dart_tms in
 261       map ((CONV_RULE o RAND_CONV o RAND_CONV o RAND_CONV o RAND_CONV) (convert_tm hyp_fun)) ths in
 262     (* Prove all subcases *)
 263   let args = arg :: map2 (fun ((split_tm, e_tm), lp_cond_th) tau_th ->
 264                             {arg with hyp_data = []; lp_cond_th = lp_cond_th; lp_tau_th = tau_th;
 265                                hyp_list_tm = split_tm; e_tm = e_tm})
 266     (lp_conds_one @ lp_conds_two) (tau_ths_one @ tau_ths_two) in
 267   let std_flags = std_flag :: replicate false 10 in
 268   let cases = map2 (verify_lp_case base_ineqs) std_flags (zip args cs) in
 269     (* Combine subcases *)
 270   let split_face_tms = map mk_raw_num info.split_face in
 271   let diag_tms = map mk_pair (zip split_face_tms (rotateL 2 split_face_tms)) in
 272   let split_th = INST (zip diag_tms (take 5 (drop 1 diag_vars))) split5_lemma in
 273   let split_cases = striplist dest_disj (concl split_th) in
 274   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 275   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 276     final_th
 277
 278 (* Hex *)
 279 and verify_split6 base_ineqs std_flag arg info cs =
 280   let _ = report "Warning: hex splitting case" in
 281   let dart_tms = rotateL 1 (mk_all_darts info.split_face) in
 282   let lp_conds = map (split_lp_conditions arg.hyp_list_tm arg.lp_cond_th) dart_tms in
 283     (* compute lp_tau_th *)
 284   let arg, hyp_data = compute_hypermap arg in
 285   let lp_tau_ths = map (get_tau_split_th tau_split6 hyp_data arg) dart_tms in
 286     (* Prove all subcases *)
 287   let args = arg :: map2 (fun ((split_tm, e_tm), lp_cond_th) tau_th ->
 288                             {arg with hyp_data = []; lp_cond_th = lp_cond_th; lp_tau_th = tau_th;
 289                                hyp_list_tm = split_tm; e_tm = e_tm}) lp_conds lp_tau_ths in
 290   let std_flags = std_flag :: replicate false 6 in
 291   let cases = map2 (verify_lp_case base_ineqs) std_flags (zip args cs) in
 292     (* Combine subcases *)
 293   let split_face_tms = map mk_raw_num info.split_face in
 294   let diag_tms = map mk_pair (zip split_face_tms (rotateL 2 split_face_tms)) in
 295   let split_th = INST (zip diag_tms (take 6 (drop 1 diag_vars))) split6_lemma in
 296   let split_cases = striplist dest_disj (concl split_th) in
 297   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 298   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 299     final_th;;
 300
 301
 302 (* Verifies an lp_certificate *)
 303 let verify_lp_certificate certificate =
 304   let n = count_terminals certificate.root_case in
 305   let hyp_list = (snd o convert_to_list) certificate.hypermap_string in
 306   let hyp_list0_tm = (to_num o create_hol_list) hyp_list in
 307   let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None in
 308   let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0 in
 309   let ye_sym_th = (MY_PROVE_HYP lp_cond0 o INST[estd_v, e_cap_var]) ye_sym0 in
 310   let base_ineqs =
 311     if n == 1 then [] else
 312       let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o
 313         MY_PROVE_HYP lp_tau0 o MY_PROVE_HYP lp_cond0 o MY_PROVE_HYP estd_refl o INST[estd_v, e_cap_var] in
 314       let r2 = (map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th)) o r in
 315         (r ye_hi_3) @ (r ye_hi_2h0) @ (r2 diag4_lo) @ (r2 diag5_lo) @ (r2 diag5_lo_sym) @ (r2 diag6_lo) @ (r2 diag6_lo_sym) in
 316   let arg = {hyp_data = [hyp_set0, hyp_fun0]; ye_sym_th = ye_sym_th;
 317              lp_cond_th = EXPAND_CONCL_RULE "L" lp_cond0; lp_tau_th = lp_tau0;
 318              hyp_list_tm = hyp_list0_tm; e_tm = estd_v} in
 319
 320   let _ = reset_progress(); Format.print_string (sprintf "terminals = %d: " n); Format.print_flush() in
 321
 322   let final_th = verify_lp_case base_ineqs true (arg, certificate.root_case) in
 323     (DISCH contravening_v o EXPAND_RULE "L" o EXPAND_RULE "g" o EXPAND_RULE "h") final_th;;
 324
 325
 326 let get_debug certificate =
 327   let n = count_terminals certificate.root_case in
 328   let hyp_list = (snd o convert_to_list) certificate.hypermap_string in
 329   let hyp_list0_tm = (to_num o create_hol_list) hyp_list in
 330   let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None in
 331   let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0 in
 332   let ye_sym_th = (MY_PROVE_HYP lp_cond0 o INST[estd_v, e_cap_var]) ye_sym0 in
 333   let base_ineqs =
 334     if n == 1 then [] else
 335       let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o
 336         MY_PROVE_HYP lp_tau0 o MY_PROVE_HYP lp_cond0 o MY_PROVE_HYP estd_refl o INST[estd_v, e_cap_var] in
 337       let r2 = (map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th)) o r in
 338         (r ye_hi_3) @ (r ye_hi_2h0) @ (r2 diag4_lo) @ (r2 diag5_lo) @ (r2 diag5_lo_sym) @ (r2 diag6_lo) @ (r2 diag6_lo_sym) in
 339   let arg = {hyp_data = [hyp_set0, hyp_fun0]; ye_sym_th = ye_sym_th;
 340              lp_cond_th = EXPAND_CONCL_RULE "L" lp_cond0; lp_tau_th = lp_tau0;
 341              hyp_list_tm = hyp_list0_tm; e_tm = estd_v} in
 342     try
 343       let _ = reset_progress(); Format.print_string (sprintf "terminals = %d: " n); Format.print_flush() in
 344       let final_th = verify_lp_case base_ineqs true (arg, certificate.root_case) in
 345         arg, {split_type = "?"; split_face = []}, [], [(DISCH contravening_v o EXPAND_RULE "L" o EXPAND_RULE "g" o EXPAND_RULE "h") final_th]
 346     with Debug_exception (arg, info, cs, thm) ->
 347       arg, info, cs, thm;;
 348
 349
 350 (*************************)
 351
 352
 353 let cert = (C nth 5 o read_lp_certificates o hd o get_files_with_prefix dir) "not_onepass2_15";;
 354 certificate_info cert;;
 355 let n = count_terminals cert.root_case;;
 356 let _, _, cs_d = match (build_test_split cert.root_case) with Info (str, f, cs) -> str, f, cs;;
 357 nth cs_d 0;;
 358 nth cs_d 1;;
 359
 360
 361
 362 index;;
 363 let base_ineqs, ts = get_terminal_cases cert;;
 364 let t7 = find_all (fun _, t -> t.precision = 7) ts;;
 365 let ind = map (C index ts) t7;;
 366
 367
 368 let test_t k =
 369   let _ = Format.print_string (sprintf "%d " k); Format.print_flush() in
 370   let t = nth ts k in
 371   let th1 = itlist MY_PROVE_HYP base_ineqs (test_terminal t) in
 372     filter (is_binary "real_le") (hyp th1);;
 373
 374 test_t 299;;
 375
 376 let rr = map test_t ind;;
 377
 378 let t = nth ts 34;;
 379 test_terminal t;;
 380 test_t 0;;
 381
 382 let rr = map test_t (0--(n - 1));;
 383 setify (flatten rr);;
 384
 385 let test_one f arg =
 386   let start = Unix.gettimeofday() in
 387   let result = f arg in
 388   let finish = Unix.gettimeofday() in
 389     result, finish -. start;;
 390
 391 test_one verify_lp_certificate cert;;
 392
 393 (**************************)
 394
 395
 396
 397 let arg, info, cs, cases = get_debug cert;;
 398 info;;
 399 nth cases 0;;
 400 nth cases 1;;
 401
 402
 403 let hyp_set, hyp_fun =
 404   let good_th = MATCH_MP lp_cond_imp_good_list arg.lp_cond_th in
 405     compute_all arg.hyp_list_tm (Some good_th);;
 406
 407
 408
 409 itlist MY_PROVE_HYP big_ths (hd cases);;
 410 hd cases;;
 411
 412
 413 (****************************)
 414
 415 let mem_stat () =
 416   let stat = Gc.stat() in
 417   let word = float_of_int (Sys.word_size / 8) in
 418   let free = float_of_int stat.Gc.free_words *. word /. 1024.0 in
 419   let total = float_of_int stat.Gc.heap_words *. word /. 1024.0 in
 420   let allocated = total -. free in
 421   let str = sprintf "allocated = %f (free = %f; total_size = %f; %f)\n"
 422     allocated free total (free /. total) in
 423     print_string str;;
 424
 425 mem_stat();;
 426 Gc.compact();;
 427 let cert = (hd o read_lp_certificates o hd o get_files_with_prefix dir) "hard6";;
 428 certificate_info cert;;
 429
 430 let test_one f arg =
 431   let start = Unix.gettimeofday() in
 432   let result = f arg in
 433   let finish = Unix.gettimeofday() in
 434     result, finish -. start;;
 435
 436 let result, time = test_one verify_lp_certificate cert;;
 437
 438
 439 let get_all_names cert =
 440   let ts = map snd (snd (get_terminal_cases cert)) in
 441   let get_names t = map (fun name, _, _ -> name) t.constraints in
 442   let names = flatten (map get_names ts) in
 443     setify names;;
 444
 445
 446 let cert = (hd o read_lp_certificates o hd o get_files_with_prefix dir) "not_onepass1__2";;
 447 certificate_info cert;;
 448 verify_lp_certificate cert;;
 449
 450 mem "yapex_sup_flat" (get_all_names cert);;
 451
 452
 453 (******************************)
 454
 455
 456 let hyp_list, terminal = nth ts 4;;
 457 let hyp_list_tm = (to_num o create_hol_list) hyp_list;;
 458 let hyp_set, hyp_fun = compute_all hyp_list_tm None;;
 459
 460
 461 let r = (fun name, ind, v -> name, ind, map mk_real_int64 v);;
 462 let constraints = map r terminal.constraints and
 463     target_variables = map r terminal.target_variables and
 464     variable_bounds = map r terminal.variable_bounds;;
 465
 466 let std_flag = true and
 467     precision = terminal.precision and
 468     infeasible = terminal.infeasible;;
 469
 470 prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun std_flag precision infeasible constraints target_variables variable_bounds;;
 471
 472 let precision_constant = Int 10 **/ (Int precision);;
 473
 474 let sum_step = fun (name, indices, c) ->
 475   try
 476     let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in
 477     let s1 = map transform_le_ineq (zip ineqs c) in
 478       List.fold_left add_step' dummy s1
 479   with
 480     | Failure str -> failwith (sprintf "Problem: %s (%s)" name str)
 481     | _ ->  failwith ("Problem: "^name);;
 482
 483 let var_table = Hashtbl.create 1000;;
 484 let add_to_var_table (name, indices, c) =
 485   let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in
 486   let m_ineqs = map2 (fun th m -> MY_PROVE_HYP th (var1_le_transform (concl th, m))) ineqs c in
 487   let _ = map (
 488     fun th ->
 489       let var = (rand o lhand o concl) th in
 490         if Hashtbl.mem var_table var then
 491           let ineq1 = Hashtbl.find var_table var in
 492           let ineq = add_le_ineqs th ineq1 in
 493           let c_tm = (lhand o lhand o concl) ineq in
 494             if c_tm = int_zero_tm then
 495               Hashtbl.remove var_table var
 496             else
 497               Hashtbl.replace var_table var ineq
 498         else
 499           Hashtbl.add var_table var th) m_ineqs in
 500     ();;
 501
 502 let get_first_var ineq_th =
 503   try
 504     (rand o lhand o rand o lhand o concl) ineq_th
 505   with Failure _ -> a_var_real;;
 506 let ineqs1 = map sum_step constraints;;
 507 let ineqs2 = List.sort (fun ineq1 ineq2 ->
 508                           let var1 = get_first_var ineq1 and
 509                               var2 = get_first_var ineq2 in
 510                             compare var1 var2) ineqs1;;
 511 let s1' = List.fold_right add_step' ineqs2 dummy;;
 512 let s1 = mul_step s1' (mk_real_int precision_constant);;
 513 let r1 = if infeasible then s1 else
 514   let ineq_th0 = assoc precision lnsum_ineqs in
 515   let ineq_th1 = (INST[hyp_list_tm, l_cap_var]) ineq_th0 in
 516   let ineq_th2 = EQ_MP (term_rewrite (concl ineq_th1) (hyp_set "list_of_elements")) ineq_th1 in
 517   let ineq_th3 = simplify_ineq hyp_fun ineq_th2 in
 518   let ineq_th4 = to_lin_f_ineq ineq_th3 in
 519     add_step' ineq_th4 s1;;
 520 let _ = map add_to_var_table variable_bounds and
 521     _ = map add_to_var_table target_variables;;
 522 let list1 = Hashtbl.fold (fun tm ineq list -> (tm, ineq) :: list) var_table [];;
 523 let list2 = List.sort (fun (tm1, _) (tm2, _) -> compare tm1 tm2) list1;;
 524 let var_list = map snd list2;;
 525
 526 let l = take 294 var_list;;
 527 let l1 = take 293 var_list;;
 528 let l2 = take 1 (drop 293 var_list);;
 529
 530
 531
 532 List.fold_left add_cancel_step r1 l;;
 533
 534 let result = List.fold_left add_cancel_step r1 var_list;;
 535   let n_tm = (rand o rand o rand o concl) result in
 536   let r_eq_th = INST[n_tm, n_var_num] FINAL_INEQ in
 537   let not_zero_th = NUM_EQ0_HASH_CONV n_tm in
 538     EQ_MP not_zero_th (EQ_MP r_eq_th result);;
 539
 540
 541
 542
 543 (**************************)
 544
 545
 546 let precision_constant = Int 10 **/ (Int precision);;
 547 let sum_step (name, indices, c) =
 548   try
 549     let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in
 550     let s1 = map transform_le_ineq (zip ineqs c) in
 551       List.fold_left add_step' dummy s1
 552   with
 553     | Failure str -> failwith (sprintf "Problem: %s (%s)" name str)
 554     | _ ->  failwith ("Problem: "^name);;
 555
 556 let s1' = List.fold_left add_step' dummy (map sum_step constraints);;
 557 let s1 = mul_step s1' (mk_real_int precision_constant);;
 558 let s2 = List.fold_left add_step' dummy (map sum_step target_variables);;
 559 let s3 = List.fold_left add_step' dummy (map sum_step variable_bounds);;
 560 let s4 = add_step' s1 (add_step' s2 s3);;
 561
 562 let ineq_th0 = assoc precision lnsum_ineqs;;
 563 let ineq_th1 = (INST[hyp_list_tm, l_cap_var]) ineq_th0;;
 564 let ineq_th2 = EQ_MP (term_rewrite (concl ineq_th1) (hyp_set "list_of_elements")) ineq_th1;;
 565 let ineq_th3 = simplify_ineq hyp_fun ineq_th2;;
 566 let ineq_th4 = to_lin_f_ineq ineq_th3;;
 567
 568 let result = add_step' ineq_th4 s4;;
 569
 570 let n_tm = (rand o rand o rand o concl) result;;
 571 let r_eq_th = INST[n_tm, n_var_num] FINAL_INEQ;;
 572 let not_zero_th = NUM_EQ0_HASH_CONV n_tm;;
 573 EQ_MP not_zero_th (EQ_MP r_eq_th result);;
 574