formal_lp/hypermap/main/prove_flyspeck_lp.hl

   1 needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;
   2 needs "../formal_lp/hypermap/ineqs/lp_head_ineqs.hl";;
   3 needs "../formal_lp/hypermap/ineqs/lp_body_ineqs.hl";;
   4 needs "../formal_lp/hypermap/main/lp_certificate.hl";;
   5 needs "../formal_lp/hypermap/computations/list_hypermap_computations.hl";;
   6 needs "../formal_lp/hypermap/computations/informal_computations.hl";;
   7 needs "../formal_lp/more_arith/prove_lp.hl";;
   8
   9
  10 module Flyspeck_lp = struct
  11
  12 open List;;
  13 open Arith_misc;;
  14 open Linear_function;;
  15 open Prove_lp;;
  16 open Arith_nat;;
  17 open Misc_vars;;
  18 open List_hypermap_computations;;
  19 open List_conversions;;
  20 open Lp_approx_ineqs;;
  21 open Lp_ineqs;;
  22 open Lp_certificate;;
  23 open Lp_informal_computations;;
  24 open Lp_ineqs_proofs;;
  25 open Lp_main_estimate;;
  26
  27
  28 let init_ineqs() =
  29   let _ = Lp_head_ineqs.add_head_ineqs() in
  30   let _ = Lp_body_ineqs.add_body_ineqs() in
  31     Lp_ineqs.process_raw_ineqs();;
  32
  33
  34 (* Prepare theorems for the final inequality: &12 <= scriptL V *)
  35 let to_lin_f_ineq ineq_th =
  36   let lhs, rhs = dest_binop le_op_real (concl ineq_th) in
  37   let lhs_th = LIN_F_CONV lhs in
  38     EQ_MP (AP_THM (AP_TERM le_op_real lhs_th) rhs) ineq_th;;
  39
  40 let FINAL_INEQ = (MY_RULE_NUM o prove)(`lin_f [] <= -- &n <=> n = 0`,
  41                      REWRITE_TAC[LIN_F_EMPTY; REAL_NEG_GE0; REAL_OF_NUM_LE; LE]);;
  42
  43 let lnsum_ineqs =
  44   let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]) in
  45   let ineq_th = (add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum_ineq in
  46   let ineq_tm = concl ineq_th in
  47   let ths1 = create_approximations [9;12;15;18;21] ineq_tm in
  48   let ths2 = map generalize_hyp ths1 in
  49   let ths3 = map (itlist PROVE_HYP Lp_ineqs_def.list_var_pos) ths2 in
  50   let ths4 = map (C MP ineq_th) ths3 in
  51   let r = CONV_RULE(REWRITE_CONV[DECIMAL_INT; GSYM LIST_SUM_LMUL] THENC DEPTH_CONV Arith_nat.NUMERAL_TO_NUM_CONV) in
  52   let ths5 = map r ths4 in
  53     zip (3--7) ths5;;
  54
  55
  56
  57 (* Performs the following conversions:
  58    (a + ... + c) + d = a + ... + c + d *)
  59 let plus_assoc_conv =
  60   let REAL_ADD_ASSOC' = (SYM o SPEC_ALL) REAL_ADD_ASSOC in
  61   let rec plus_conv tm =
  62     if (is_binop add_op_real tm) then
  63       let lhs, rhs = dest_binop add_op_real tm in
  64         if (is_binop add_op_real lhs) then
  65           let x_tm, y_tm = dest_binop add_op_real lhs in
  66           let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; rhs, z_var_real] REAL_ADD_ASSOC' in
  67           let ltm, rtm = dest_comb(rand(concl th0)) in
  68             TRANS th0 (AP_TERM ltm (plus_conv rtm))
  69         else
  70           REFL tm
  71     else
  72       REFL tm
  73   in plus_conv;;
  74
  75
  76 (**********************)
  77
  78 let convert_ineq hyp_fun =
  79   let rec rewrite_lhs tm =
  80     let rewrite_one tm =
  81       if (is_binop mul_op_real tm) then
  82         let mul_tm, var_tm = dest_comb tm in
  83         let var_f, arg = dest_comb var_tm in
  84
  85         let rec convert_arg arg =
  86           if (is_comb arg) then
  87             let ltm, sub_arg' = dest_comb arg in
  88             let const_name = (fst o dest_const) (if (is_const ltm) then ltm else rator ltm) in
  89               (* Str.first_chars const_name 1 = "D" is a hack *)
  90               if (Str.first_chars const_name 1 = "D" or const_name = "_0"
  91                   or const_name = "," or const_name = "CONS" or const_name = "INSERT") then
  92                 REFL arg
  93               else
  94                 try
  95                   let sub_arg_th = convert_arg sub_arg' in
  96                   let th0 = AP_TERM ltm sub_arg_th in
  97                   let rtm = rand(concl th0) in
  98                   let th1 =
  99                     if (const_name = "set_of_list") then
 100                       set_of_list_conv rtm
 101                     else if (const_name = "FST") then
 102                       fst_conv rtm
 103                     else if (const_name = "SND") then
 104                       snd_conv rtm
 105                     else if (const_name = "HD") then
 106                       hd_conv rtm
 107                     else if (const_name = "e_list") then
 108                       e_list_conv_num rtm
 109                     else
 110                       hyp_fun const_name (rand rtm) in
 111                     TRANS th0 th1
 112                 with _ ->
 113                   failwith ("convert_arg: "^const_name)
 114           else
 115             REFL arg in
 116
 117         let arg_th = convert_arg arg in
 118           AP_TERM mul_tm (AP_TERM var_f arg_th)
 119
 120       else
 121         (* tm should be list_sum *)
 122         list_sum_conv BETA_CONV tm in
 123
 124       if (is_binop add_op_real tm) then
 125         let lhs, rhs = dest_binop add_op_real tm in
 126         let lhs_th = rewrite_one lhs in
 127         let rhs_th = rewrite_lhs rhs in
 128         let th1 = MK_COMB(AP_TERM add_op_real lhs_th, rhs_th) in
 129           if (is_binop add_op_real (rand(concl lhs_th))) then
 130             let th2 = plus_assoc_conv (rand(concl th1)) in
 131               TRANS th1 th2
 132           else
 133             th1
 134       else
 135         rewrite_one tm in
 136
 137     fun ineq_tm ->
 138       if not (is_binary "real_le" ineq_tm) then
 139         REFL ineq_tm
 140       else
 141         let ltm, rtm = dest_comb ineq_tm in
 142         let op_tm, l_tm = dest_comb ltm in
 143         let lhs_eq_th = rewrite_lhs l_tm in
 144           AP_THM (AP_TERM op_tm lhs_eq_th) rtm;;
 145
 146
 147 let convert_tm =
 148   let num_str = (fst o dest_const) Arith_hash.num_const in
 149   let rec convert hyp_fun tm =
 150     if (is_comb tm) then
 151       let ltm, rtm = dest_comb tm in
 152       let op_tm = if is_comb ltm then rator ltm else ltm in
 153         if is_const op_tm then
 154           let const_name = (fst o dest_const) op_tm in
 155             if const_name = "real_of_num" or const_name = "DECIMAL" then
 156               REFL tm
 157             else if const_name = "real_add" then
 158               let th1 = convert hyp_fun (rand ltm) and
 159                   th2 = convert hyp_fun rtm in
 160                 MK_COMB (AP_TERM op_tm th1, th2)
 161             else if const_name = "ye_list" then
 162               if is_pair rtm then
 163                 let ltm', b_tm = dest_comb rtm in
 164                 let pair_op, a_tm = dest_comb ltm' in
 165                 let a_th = convert hyp_fun a_tm and
 166                     b_th = convert hyp_fun b_tm in
 167                   AP_TERM ltm (MK_COMB (AP_TERM pair_op a_th, b_th))
 168               else
 169                 let rtm_th = convert hyp_fun rtm in
 170                   AP_TERM ltm rtm_th
 171             else
 172               let rtm_th = convert hyp_fun rtm in
 173               let th0 = AP_TERM ltm rtm_th in
 174               let arg = rand (concl th0) in
 175               let th1 =
 176                 if const_name = num_str then
 177                   INST[rand arg, n_var_num] Arith_hash.NUM_THM
 178                 else
 179                   match const_name with
 180                     | "set_of_list" -> set_of_list_conv arg
 181                     | "FST" -> fst_conv arg
 182                     | "SND" -> snd_conv arg
 183                     | "HD" -> hd_conv arg
 184                     | "e_list" -> e_list_conv_num arg
 185                     | "LENGTH" -> length_conv arg
 186                     | _ ->
 187                         (try hyp_fun const_name (rand arg)
 188                          with Failure _ -> REFL arg) in
 189                 TRANS th0 th1
 190         else
 191           REFL tm
 192     else
 193       REFL tm in
 194     convert;;
 195
 196
 197 let convert_condition hyp_fun tm =
 198   if is_comb tm then
 199     let ltm, rtm = dest_comb tm in
 200     let r_th = convert_tm hyp_fun rtm in
 201       if is_comb ltm then
 202         let op_tm, larg = dest_comb ltm in
 203         let l_th = convert_tm hyp_fun larg in
 204           MK_COMB (AP_TERM op_tm l_th, r_th)
 205       else
 206         AP_TERM ltm r_th
 207   else
 208     convert_tm hyp_fun tm;;
 209
 210
 211
 212 let rec simplify_ineq_tm hyp_fun tm =
 213   if is_imp tm then
 214     let ltm, q_tm = dest_comb tm in
 215     let imp_tm, p_tm = dest_comb ltm in
 216     let p_eq_th = convert_condition hyp_fun p_tm in
 217     let q_eq_th = simplify_ineq_tm hyp_fun q_tm in
 218       MK_COMB (AP_TERM imp_tm p_eq_th, q_eq_th)
 219   else
 220     convert_ineq hyp_fun tm;;
 221
 222
 223 let simplify_ineq hyp_fun ineq_th =
 224   let eq_th = simplify_ineq_tm hyp_fun (concl ineq_th) in
 225     EQ_MP eq_th ineq_th;;
 226
 227 let prove_conditions =
 228   let neq_elim_th = prove(`(s <=> F) <=> ~s`, REWRITE_TAC[]) in
 229   let rec prove_rec ineq_th =
 230     let concl_tm = concl ineq_th in
 231       if is_imp concl_tm then
 232         let p_tm = lhand concl_tm in
 233         let flag, p_th =
 234           (* (trivial) equality *)
 235           if is_eq p_tm then
 236             let ltm, rtm = dest_eq p_tm in
 237               if ltm = rtm then
 238                 true, REFL ltm
 239               else
 240                 false, TRUTH
 241                   (* n < m:num *)
 242           else if is_binary "<" p_tm then
 243             true, EQT_ELIM (raw_lt_hash_conv p_tm)
 244               (* ~(n = m) *)
 245           else if is_neg p_tm then
 246             let s_tm = rand p_tm in
 247             let th0 = raw_eq_hash_conv s_tm in
 248             let elim_th = INST[s_tm, s_var_bool] neq_elim_th in
 249               true, EQ_MP elim_th th0
 250           else
 251             false, TRUTH in
 252         let th1 =
 253           if flag then
 254             MP ineq_th p_th
 255           else
 256             UNDISCH ineq_th in
 257           prove_rec th1
 258       else
 259         ineq_th in
 260     prove_rec;;
 261
 262
 263 let get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices =
 264   let ineq0_th = (find_ineq std_flag precision name).ineq_th in
 265   let ineq1_th = INST[hyp_list_tm, l_cap_var] ineq0_th in
 266   let all_tm, set_tm = dest_comb (concl ineq1_th) in
 267   let set_eq_th = hyp_set ((fst o dest_const o rator) set_tm) in
 268   let ineq2_th = EQ_MP (AP_TERM all_tm set_eq_th) ineq1_th in
 269   let ineq0_ths = select_all ineq2_th indices in
 270   let ineq1_ths' = map MY_BETA_RULE ineq0_ths in
 271     (* A special treatment of the "main" inequality *)
 272   let ineq1_ths = if name = "main" then
 273     map (fun th -> EQ_MP (term_rewrite (concl th) (hyp_set "list_of_elements")) th) ineq1_ths'
 274   else ineq1_ths' in
 275   let ineq2_ths = map (simplify_ineq hyp_fun) ineq1_ths in
 276   let ineq3_ths = map prove_conditions ineq2_ths in
 277     ineq3_ths;;
 278
 279
 280 (****************************)
 281
 282 let int_zero_tm = mk_comb (amp_op_real, (rand o concl o NUMERAL_TO_NUM_CONV) `0`);;
 283 let int_neg_zero_tm = mk_comb (neg_op_real, int_zero_tm);;
 284 let var_table = Hashtbl.create 1000;;
 285
 286
 287 let prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun std_flag precision infeasible constraints target_variables variable_bounds =
 288   let precision_constant = Int 10 **/ (Int precision) in
 289
 290 (* This function generates all inequalities with the given name and indices,
 291    multiplies these inequalities by given coefficients, and finds the sum of
 292    the generated inequalities *)
 293   let sum_step = fun (name, indices, c) ->
 294     try
 295       let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in
 296       let s1 = map transform_le_ineq (zip ineqs c) in
 297         List.fold_left add_step' dummy s1
 298     with
 299       | Failure str -> failwith (sprintf "Problem: %s (%s)" name str)
 300       | _ ->  failwith ("Problem: "^name) in
 301
 302   let _ = Hashtbl.clear var_table in
 303   let add_to_var_table (name, indices, c) =
 304     let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in
 305     let m_ineqs = map2 (fun th m -> MY_PROVE_HYP th (var1_le_transform (concl th, m))) ineqs c in
 306     let _ = map (
 307       fun th ->
 308         let var = (rand o lhand o concl) th in
 309           if Hashtbl.mem var_table var then
 310             let ineq1 = Hashtbl.find var_table var in
 311           let ineq = add_le_ineqs th ineq1 in
 312           let c_tm = (lhand o lhand o concl) ineq in
 313             if c_tm = int_zero_tm or c_tm = int_neg_zero_tm then
 314               Hashtbl.remove var_table var
 315             else
 316               Hashtbl.replace var_table var ineq
 317           else
 318             Hashtbl.add var_table var th) m_ineqs in
 319       () in
 320
 321   let get_first_var ineq_th =
 322     try
 323       (rand o lhand o rand o lhand o concl) ineq_th
 324     with Failure _ -> a_var_real in
 325   let ineqs1 = map sum_step constraints in
 326   let ineqs2 = List.sort (fun ineq1 ineq2 ->
 327                             let var1 = get_first_var ineq1 and
 328                                 var2 = get_first_var ineq2 in
 329                               compare var1 var2) ineqs1 in
 330   let s1' = List.fold_right add_step' ineqs2 dummy in
 331   let s1 = mul_step s1' (mk_real_int precision_constant) in
 332   let r1 = if infeasible then s1 else
 333     let ineq_th0 = assoc precision lnsum_ineqs in
 334     let ineq_th1 = (INST[hyp_list_tm, l_cap_var]) ineq_th0 in
 335     let ineq_th2 = EQ_MP (term_rewrite (concl ineq_th1) (hyp_set "list_of_elements")) ineq_th1 in
 336     let ineq_th3 = simplify_ineq hyp_fun ineq_th2 in
 337     let ineq_th4 = to_lin_f_ineq ineq_th3 in
 338       add_step' ineq_th4 s1 in
 339   let _ = map add_to_var_table variable_bounds and
 340       _ = map add_to_var_table target_variables in
 341   let list1 = Hashtbl.fold (fun tm ineq list -> (tm, ineq) :: list) var_table [] in
 342   let list2 = List.sort (fun (tm1, _) (tm2, _) -> compare tm1 tm2) list1 in
 343   let var_list = map snd list2 in
 344   let result = List.fold_left add_cancel_step r1 var_list in
 345   let n_tm = (rand o rand o rand o concl) result in
 346   let r_eq_th = INST[n_tm, n_var_num] FINAL_INEQ in
 347   let not_zero_th = NUM_EQ0_HASH_CONV n_tm in
 348     EQ_MP not_zero_th (EQ_MP r_eq_th result);;
 349
 350 (*
 351 let prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun std_flag precision infeasible constraints target_variables variable_bounds =
 352   let precision_constant = Int 10 **/ (Int precision) in
 353   let sum_step = fun (name, indices, c) ->
 354     try
 355       let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in
 356       let s1 = map transform_le_ineq (zip ineqs c) in
 357         List.fold_left add_step' dummy s1
 358     with
 359       | Failure str -> failwith (sprintf "Problem: %s (%s)" name str)
 360       | _ -> failwith ("Problem: "^name) in
 361
 362   let s1' = List.fold_left add_step' dummy (map sum_step constraints) in
 363   let s1 = mul_step s1' (mk_real_int precision_constant) in
 364   let s2 = List.fold_left add_step' dummy (map sum_step target_variables) in
 365   let s3 = List.fold_left add_step' dummy (map sum_step variable_bounds) in
 366   let s4 = add_step' (add_step' s1 s2) s3 in
 367
 368   let result = if infeasible then s4 else
 369     let ineq_th0 = assoc precision lnsum_ineqs in
 370     let ineq_th1 = (INST[hyp_list_tm, l_cap_var]) ineq_th0 in
 371     let ineq_th2 = EQ_MP (term_rewrite (concl ineq_th1) (hyp_set "list_of_elements")) ineq_th1 in
 372     let ineq_th3 = simplify_ineq hyp_fun ineq_th2 in
 373     let ineq_th4 = to_lin_f_ineq ineq_th3 in
 374       add_step' ineq_th4 s4 in
 375
 376   let n_tm = (rand o rand o rand o concl) result in
 377   let r_eq_th = INST[n_tm, n_var_num] FINAL_INEQ in
 378   let not_zero_th = NUM_EQ0_HASH_CONV n_tm in
 379     EQ_MP not_zero_th (EQ_MP r_eq_th result);;
 380 *)
 381
 382
 383 (*************************)
 384
 385 (* Replaces the given term tm with a variable named var_name in the given theorem th *)
 386 (* A new assumption tm = var_name is added *)
 387 let ABBREV_RULE var_name tm th =
 388   let var_tm = mk_var (var_name, type_of tm) in
 389   let eq_th = ASSUME (mk_eq (tm, var_tm)) in
 390     (UNDISCH_ALL o PURE_REWRITE_RULE[eq_th] o DISCH_ALL) th;;
 391
 392 (* Transforms a theorem |- ?x. P x into (@x. P x) = x |- P x *)
 393 let SELECT_AND_ABBREV_RULE =
 394   let P = `P:A->bool` in
 395   let pth = prove
 396     (`(?) (P:A->bool) ==> P((@) P)`,
 397      SIMP_TAC[SELECT_AX; ETA_AX]) in
 398   fun th ->
 399     try
 400       let abs = rand (concl th) in
 401       let var, b_tm = dest_abs abs in
 402       let name, ty = dest_var var in
 403       let select_tm = mk_binder "@" (var, b_tm) in
 404       let th0 = CONV_RULE BETA_CONV (MP (PINST [ty,aty] [abs,P] pth) th) in
 405         ABBREV_RULE name select_tm th0
 406     with Failure _ -> failwith "SELECT_AND_ABBREV_RULE";;
 407
 408 (* Transforms a theorem tm = var_name, G |- P into G[tm/var_name] |- P[tm/var_name] *)
 409 let EXPAND_RULE var_name th =
 410   let hyp_tm = find (fun tm -> is_eq tm && is_var (rand tm) && name_of (rand tm) = var_name) (hyp th) in
 411   let l_tm, var_tm = dest_eq hyp_tm in
 412   let th1 = INST[l_tm, var_tm] th in
 413     PROVE_HYP (REFL l_tm) th1;;
 414
 415 (* Transforms a theorem tm = var_name, G |- P into tm = var_name, G |- P[tm/var_name] *)
 416 let EXPAND_CONCL_RULE var_name th =
 417   let hyp_tm = find (fun tm -> is_eq tm && is_var (rand tm) && name_of (rand tm) = var_name) (hyp th) in
 418   let eq_th = SYM (ASSUME hyp_tm) in
 419     PURE_REWRITE_RULE[eq_th] th;;
 420
 421 (*************************)
 422 (* Auxiliary definitions *)
 423 (*************************)
 424
 425 let report s =
 426   Format.print_string s; Format.print_newline(); Format.print_flush();;
 427
 428 let e_cap_var = `E:(real^3->bool)->bool` and
 429     l_cap_var = `L:((num)list)list` and
 430     estd_v = `ESTD V` and
 431     contravening_v = `contravening V` and
 432     d_var_pair = `d:num#num` and
 433     diag_vars = map (fun i -> mk_var ("diag" ^ string_of_int i, `:num#num`)) (0--6) and
 434     a_vars = map (fun i -> mk_var ("a" ^ string_of_int i, `:real`)) (0--6);;
 435
 436 let mk_raw_num = rand o Arith_nat.mk_small_numeral_array;;
 437 let mk_dart face i1 i2 = mk_pair (mk_raw_num (nth face i1), mk_raw_num (nth face i2));;
 438 let mk_all_darts face = map mk_pair (list_pairs (map mk_raw_num face));;
 439
 440 (* Given a list of pairs [x1,y1; ...; xn,yn] and an element x,  *)
 441 (* finds all y's such that (x,y) is in the list                 *)
 442 let rec assoc_all a list =
 443   match list with
 444     | [] -> []
 445     | (k,v) :: t -> if k = a then v :: assoc_all a t else assoc_all a t;;
 446
 447 (* Combines theorems |- A ==> C, |- B ==> C and yields |- A \/ B ==> C *)
 448 let combine_cases =
 449   let combine_th = TAUT `(A ==> C) /\ (B ==> C) ==> (A \/ B ==> C)` in
 450     fun case1_th case2_th ->
 451       MATCH_MP combine_th (CONJ case1_th case2_th);;
 452
 453 let dest_ye_list tm =
 454   let lhs, rhs = dest_comb tm in
 455   let c_tm = rator lhs in
 456     if (fst o dest_const) c_tm <> "ye_list" then
 457       failwith "dest_ye_list: not ye_list"
 458     else
 459       dest_pair rhs;;
 460
 461 (* Given |- ALL (\x. P x) (hypermap_set),                               *)
 462 (* returns |- P x1, ..., |- P xn for all elements x in hypermap_set     *)
 463 let get_all_ineqs hyp_set0 all_ineq_th =
 464   let all_tm, set_tm = dest_comb (concl all_ineq_th) in
 465   let set_eq_th = hyp_set0 ((fst o dest_const o rator) set_tm) in
 466   let ineq1_th = EQ_MP (AP_TERM all_tm set_eq_th) all_ineq_th in
 467     map MY_BETA_RULE (get_all ineq1_th);;
 468
 469 (* Generates a list inequality from a fan inequality.                        *)
 470 (* If simplify_all_flag is true then the conclusion of                       *)
 471 (* the generated inequality is simplified (yi's are transformed into ye).    *)
 472 let gen_list_ineq simplify_all_flag th =
 473   let th0 = add_lp_hyp true th in
 474   let tm1, proof_th = mk_lp_ineq th0 in
 475   let raw_data = {name = "tmp"; tm = tm1; proof = Some proof_th; std_only = false} in
 476     generate_ineq1 simplify_all_flag raw_data;;
 477
 478 (******************)
 479 (* Special lemmas *)
 480 (******************)
 481
 482 (* Quad split cases *)
 483 let split4_lemma = (INST[`ye_list (g:num#num->real^3#real^3) diag1`, `a:real`;
 484                          `ye_list (g:num#num->real^3#real^3) diag2`, `b:real`] o prove)
 485 (`(a <= b /\ a <= sqrt8)
 486    \/ (b <= a /\ b <= sqrt8)
 487    \/ (a <= b /\ sqrt8 <= a /\ a <= &3)
 488    \/ (b <= a /\ sqrt8 <= b /\ b <= &3)
 489    \/ (&3 <= a /\ &3 <= b)`,
 490  MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC);;
 491
 492 (* Pent split cases *)
 493 let split5_lemma =
 494   let inst = zip (map (fun d -> mk_comb (`ye_list (g:num#num->real^3#real^3)`, d)) diag_vars) a_vars in
 495     (INST inst o prove)(`(sqrt8 <= a1 /\ sqrt8 <= a2 /\ sqrt8 <= a3 /\ sqrt8 <= a4 /\ sqrt8 <= a5)
 496                           \/ (a1 <= sqrt8 /\ sqrt8 <= a3 /\ sqrt8 <= a4)
 497                           \/ (a2 <= sqrt8 /\ sqrt8 <= a4 /\ sqrt8 <= a5)
 498                           \/ (a3 <= sqrt8 /\ sqrt8 <= a5 /\ sqrt8 <= a1)
 499                           \/ (a4 <= sqrt8 /\ sqrt8 <= a1 /\ sqrt8 <= a2)
 500                           \/ (a5 <= sqrt8 /\ sqrt8 <= a2 /\ sqrt8 <= a3)
 501                           \/ (a1 <= sqrt8 /\ a3 <= sqrt8)
 502                           \/ (a2 <= sqrt8 /\ a4 <= sqrt8)
 503                           \/ (a3 <= sqrt8 /\ a5 <= sqrt8)
 504                           \/ (a4 <= sqrt8 /\ a1 <= sqrt8)
 505                           \/ (a5 <= sqrt8 /\ a2 <= sqrt8)`,
 506                         MAP_EVERY DISJ_CASES_TAC (map (fun tm -> SPECL[tm; `sqrt8`] REAL_LE_TOTAL) (take 5 (drop 1 a_vars))) THEN
 507                           ASM_REWRITE_TAC[]);;
 508
 509 (* Hex split cases *)
 510 let split6_lemma =
 511   let inst = zip (map (fun d -> mk_comb (`ye_list (g:num#num->real^3#real^3)`, d)) diag_vars) a_vars in
 512     (INST inst o prove)(`(sqrt8 <= a1 /\ sqrt8 <= a2 /\ sqrt8 <= a3 /\ sqrt8 <= a4 /\ sqrt8 <= a5 /\ sqrt8 <= a6)
 513                           \/ a1 <= sqrt8
 514                           \/ a2 <= sqrt8
 515                           \/ a3 <= sqrt8
 516                           \/ a4 <= sqrt8
 517                           \/ a5 <= sqrt8
 518                           \/ a6 <= sqrt8`, ARITH_TAC);;
 519
 520 (* Node and edge split lemmas *)
 521 let split218_lemma = SPECL [`#2.18`; `yn_list (h:num->real^3) i`] REAL_LE_TOTAL;;
 522 let split236_lemma = SPECL [`yn_list (h:num->real^3) i`; `#2.36`] REAL_LE_TOTAL;;
 523 let split225_lemma = SPECL [`#2.25`; `ye_list (g:num#num->real^3#real^3) d`] REAL_LE_TOTAL;;
 524
 525 (* lp_cond ==> good_list *)
 526 let lp_cond_imp_good_list = prove(`lp_cond (L, g, h:num->real^3) (V,E) ==> good_list L`, SIMP_TAC[lp_cond]);;
 527
 528 (* ESTD V = ESTD V *)
 529 let estd_refl = REFL estd_v;;
 530
 531 (* ye_list g d <= &3 for a standard fan *)
 532 let ye_hi_3 = generate_ineq (gen_raw_ineq_data "tmp" true ye_hi_std);;
 533
 534 (* ye_list g d <= #2.52 for a standard fan *)
 535 let ye_hi_2h0 = generate_ineq (gen_raw_ineq_data "tmp" true yy10_std);;
 536
 537 (* ye_list g (a,b) = ye_list g (b,a) *)
 538 let ye_sym0 = (add_lp_hyp false o prove)(`(!d. g d = h (FST d), h (SND d))
 539                                          ==> ye_list (g:num#num->real^3#real^3) (n,m) = ye_list g (m,n)`,
 540                                          DISCH_TAC THEN ASM_REWRITE_TAC Lp_ineqs_def.list_defs2 THEN
 541                                            REWRITE_TAC[Lp_ineqs_def.ye_fan; DIST_SYM]);;
 542
 543 (* #2.52 <= ye_list g d for diagonals *)
 544 let diag4_lo = gen_list_ineq true dart4_y4'_lo and
 545     diag5_lo = (gen_list_ineq true o CONV_RULE NUM_REDUCE_CONV o SPEC `5` o add_lp_hyp false) y4'_lo_2h0 and
 546     diag6_lo = (gen_list_ineq true o CONV_RULE NUM_REDUCE_CONV o SPEC `6` o add_lp_hyp false) y4'_lo_2h0;;
 547
 548 let diag5_lo_sym = PURE_ONCE_REWRITE_RULE[ye_sym0] diag5_lo and
 549     diag6_lo_sym = PURE_ONCE_REWRITE_RULE[ye_sym0] diag6_lo;;
 550
 551 (* lp_tau for different cases *)
 552 let tau_split4, tau_split5_one, tau_split5_two, tau_split6 =
 553   let r = SPEC `d:num#num` o REWRITE_RULE[GSYM ALL_MEM] o gen_list_ineq true in
 554     r lp_tau_split4, r lp_tau_split5_one_diag, r lp_tau_split5_two_diags, r lp_tau_split6;;
 555
 556
 557 (*****************************************)
 558
 559 (* Generates extra inequalities for a given inequality.  *)
 560 (* For instance, |- a <= sqrt8 yields |- a <= &3         *)
 561 let gen_extra_ineqs =
 562   let tm_3 = `&3` and
 563       tm_sqrt8 = `sqrt8` and
 564       tm_218 = `#2.18` and
 565       tm_236 = `#2.36` in
 566
 567   let r tm = prove(tm, MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC) in
 568   let l_ths_list = [
 569     tm_3, r `&3 <= a ==> sqrt8 <= a`;
 570     tm_236, r `#2.36 <= a ==> #2.18 <= a`;
 571   ] in
 572   let r_ths_list = [
 573     tm_sqrt8, r `a <= sqrt8 ==> a <= &3`;
 574     tm_218, r `a <= #2.18 ==> a <= #2.36`;
 575   ] in
 576   let a_var_real = `a:real` in
 577     fun ineq_th ->
 578       let lhs, rhs = dest_binary "real_le" (concl ineq_th) in
 579       let l_ths = map (fun th -> MP (INST[rhs, a_var_real] th) ineq_th) (assoc_all lhs l_ths_list) and
 580           r_ths = map (fun th -> MP (INST[lhs, a_var_real] th) ineq_th) (assoc_all rhs r_ths_list) in
 581         l_ths @ r_ths;;
 582
 583
 584 (* Generates ye-symmetric inequalities.                    *)
 585 (* Example: |- ye (a,b) <= c yields |- ye (b,a) <= c       *)
 586 (* Accepts inequalities in the form:                       *)
 587 (* |- ye d <= c, |- c <= ye d, and |- ye d1 <= ye d2       *)
 588 (* This function does not return the original inequality   *)
 589 let gen_ye_sym_ineqs ye_sym_th ineq_th =
 590   let sym_eqs tm =
 591     try
 592       let n_tm, m_tm = dest_ye_list tm in
 593         [REFL tm; INST[n_tm, n_var_num; m_tm, m_var_num] ye_sym_th]
 594     with Failure _ ->
 595       [REFL tm] in
 596   let ltm, rhs = dest_comb (concl ineq_th) in
 597   let op_tm, lhs = dest_comb ltm in
 598   let l_eqs = sym_eqs lhs and
 599       r_eqs = sym_eqs rhs in
 600     tl (allpairs (fun l_eq r_eq -> EQ_MP (MK_COMB (AP_TERM op_tm l_eq, r_eq)) ineq_th) l_eqs r_eqs);;
 601
 602
 603 (* Generates all extra inequalities (including ye-symmetric inequalities) *)
 604 let gen_all_extra_cases ye_sym_th case_tms =
 605   let case_ths = map ASSUME case_tms in
 606   let extra = List.flatten (map gen_extra_ineqs case_ths) in
 607   let sym = gen_ye_sym_ineqs ye_sym_th in
 608     extra @ List.flatten (map sym (case_ths @ extra));;
 609
 610 (* Computes lp_cond and lp_tau for a contravening packing *)
 611 let contravening_conditions hyp_list_tm hyp_set =
 612   let th0 = (MY_RULE_NUM o REWRITE_RULE[Seq.size]) Lp_ineqs_proofs.contravening_lp_cond_alt in
 613   let th1 = (UNDISCH_ALL o  ISPEC hyp_list_tm o REWRITE_RULE[GSYM IMP_IMP]) th0 in
 614   let good_list_nodes_th = EQT_ELIM (eval_good_list_nodes_condition hyp_set) in
 615   let lp_cond_th = (MY_PROVE_HYP (hyp_set "good_list") o MY_PROVE_HYP good_list_nodes_th) th1 in
 616   let lp_cond_th' = (SELECT_AND_ABBREV_RULE o SELECT_AND_ABBREV_RULE o ABBREV_RULE "L" hyp_list_tm) lp_cond_th in
 617   let lp_tau_th = (UNDISCH_ALL o SPEC_ALL) Lp_main_estimate.contravening_lp_tau in
 618     lp_cond_th', lp_tau_th;;
 619
 620
 621 (*******************************)
 622 (* Verification test functions *)
 623 (*******************************)
 624
 625 (* Returns all terminal cases and corresponding hypermap lists   *)
 626 (* for a given hypermap list and lp_certificate_case             *)
 627 let rec terminal_cases (hyp_list, case) =
 628   match case with
 629     | Lp_terminal terminal -> [(hyp_list, terminal)]
 630     | Lp_split (info, cs) ->
 631         (match info.split_type with
 632              (* Triangles, edges, nodes *)
 633            | "tri" | "edge" | "236" | "218" ->
 634                let case_args = zip [hyp_list; hyp_list] cs in
 635                  flatten (map terminal_cases case_args)
 636
 637            (* Special cases *)
 638            | "high" | "mid" | "add_big" ->
 639                let case_args = zip [hyp_list] cs in
 640                  flatten (map terminal_cases case_args)
 641
 642            (* Quad *)
 643            | "quad" ->
 644                let split_face = info.split_face in
 645                let dart13 = nth split_face 1, nth split_face 2 and
 646                    dart24 = nth split_face 0, nth split_face 1 in
 647                let split13 = split_list hyp_list dart13 and
 648                    split24 = split_list hyp_list dart24 in
 649                let case_args = zip [split13; split24; split13; split24; hyp_list] cs in
 650                  flatten (map terminal_cases case_args)
 651
 652            (* Pent *)
 653            | "pent" ->
 654                let split_face = info.split_face in
 655                let darts = rotateL 1 (list_pairs split_face) in
 656                let splits_one = map (split_list hyp_list) darts in
 657                let splits_two = map2 split_list splits_one (rotateL 2 darts) in
 658                let case_args = zip (hyp_list :: (splits_one @ splits_two)) cs in
 659                  flatten (map terminal_cases case_args)
 660
 661            (* Hex *)
 662            | "hex" ->
 663                let split_face = info.split_face in
 664                let darts = rotateL 1 (list_pairs split_face) in
 665                let splits = map (split_list hyp_list) darts in
 666                let case_args = zip (hyp_list :: splits) cs in
 667                  flatten (map terminal_cases case_args)
 668
 669            | s -> failwith ("cases: unknown split type: " ^ s));;
 670
 671 (* Returns all terminal cases and corresponding hypermap lists for lp_certificate *)
 672 let get_terminal_cases certificate =
 673   let hyp_list = (snd o convert_to_list) certificate.hypermap_string in
 674   let hyp_list0_tm = (to_num o create_hol_list) hyp_list in
 675   let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None in
 676   let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0 in
 677   let ye_ineqs_3, ye_ineqs_2h0, diag4_ineqs =
 678     let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o
 679       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
 680       r ye_hi_3, r ye_hi_2h0, r diag4_lo in
 681   let diag4_ths = map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th) diag4_ineqs in
 682   let base_ineqs = ye_ineqs_3 @ ye_ineqs_2h0 @ diag4_ths in
 683     base_ineqs, terminal_cases (hyp_list, certificate.root_case);;
 684
 685 (* Tests (verifies) a terminal case *)
 686 let test_terminal (hyp_list, terminal) =
 687   let hyp_list_tm = (to_num o create_hol_list) hyp_list in
 688   let hyp_set, hyp_fun = compute_all hyp_list_tm None in
 689   let r = (fun name, ind, v -> name, ind, map mk_real_int64 v) in
 690   let c = map r terminal.constraints and
 691       tv = map r terminal.target_variables and
 692       vb = map r terminal.variable_bounds in
 693     prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun false terminal.precision terminal.infeasible c tv vb;;
 694
 695
 696 (*******************************)
 697 (* Main verification functions *)
 698 (*******************************)
 699
 700 type lp_verification_arg = {
 701   (* Hypermap data *)
 702   hyp_data : ((string->thm) * (string->term->thm))list;
 703
 704   ye_sym_th : thm;
 705
 706   (* Theorems *)
 707   lp_cond_th : thm;
 708   lp_tau_th : thm;
 709
 710   (* Terms *)
 711   hyp_list_tm : term;
 712   e_tm : term;
 713 };;
 714
 715
 716 (* Computes a splitted hypermap list (L2), a new E term (E2), lp_cond (L2,g,h) (V,E2) *)
 717 let split_lp_conditions hyp_list_tm lp_cond_th d_tm =
 718   let split_eq_th = eval_split_list_hyp hyp_list_tm d_tm in
 719   let split_tm = (rand o concl) split_eq_th in
 720   let lp_cond2_th = (PURE_REWRITE_RULE[split_eq_th] o SPEC d_tm o MATCH_MP lp_cond_trans1) lp_cond_th in
 721   let e2_tm = (rand o rand o concl) lp_cond2_th in
 722     (split_tm, e2_tm), lp_cond2_th;;
 723
 724 (* Computes lp_tau (V,E2) *)
 725 let get_tau_split_th tau_trans_th (hyp_set, hyp_fun) arg d_tm =
 726   let set_name = (fst o dest_const o rator o rand o lhand o concl) tau_trans_th in
 727   let set_th = hyp_set set_name in
 728   let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair d_tm)) in
 729   let th0 = INST[arg.hyp_list_tm, l_cap_var; d_tm, d_var_pair; arg.e_tm, e_cap_var] tau_trans_th in
 730     (UNDISCH_ALL o MY_PROVE_HYP arg.lp_cond_th o MY_PROVE_HYP arg.lp_tau_th o simplify_ineq hyp_fun o MP th0) mem_th;;
 731
 732 (* Eliminates extra assumptions and discharges case assumptions *)
 733 let get_final_case_th ye_sym_th cases_tm case_th =
 734   let case_tms = striplist dest_conj cases_tm in
 735   let case_th2 = itlist MY_PROVE_HYP (gen_all_extra_cases ye_sym_th case_tms) case_th in
 736     PURE_REWRITE_RULE[IMP_IMP; GSYM CONJ_ASSOC] (itlist DISCH case_tms case_th2);;
 737
 738 (* Returns terms and inequalities for the triangle splitting case:            *)
 739 (* split_th = |- #6.25 <= a + b + c \/ a + b + c <= #6.25                     *)
 740 (* big_tm = `#6.25 <= a + b + c`, small_tm = `a + b + c <= #6.25              *)
 741 (* sym_big_ineqs = [|- #6.25 <= b + c + a; |- #6.25 <= c + a + b]             *)
 742 (* sym_small_ineqs = [|- b + c + a <= #6.25; |- c + a + b <= #6.25;           *)
 743 (*                    |- a <= #2.52; |- b <= #2.25; |- c <= #2.25;            *)
 744 (*                    |- e(a) <= #2.52; |- e(b) <= #2.52; |- e(c) <= #2.52]   *)
 745 (* Here, a = ye_list g (i1,i2), b = ye_list g (i2,i3), c = ye_list g (i3,i1)  *)
 746 (* for split_face = [i1; i2; i3]                                              *)
 747 let gen_triangle_ineqs =
 748   let ye_tm = `ye_list (g:num#num->real^3#real^3)` and
 749       c625 = `#6.25` in
 750   let sym_big = (SPEC c625 o ARITH_RULE) `!c. c <= x + y + z ==> c <= y + z + x /\ c <= z + x + y` and
 751       sym_small = (SPEC c625 o ARITH_RULE) `!c. x + y + z <= c ==> y + z + x <= c /\ z + x + y <= c` and
 752       split3_lemma = SPECL[c625; `x:real`] REAL_LE_TOTAL and
 753       small_extra = (SPEC `d:num#num` o REWRITE_RULE[GSYM ALL_MEM] o gen_list_ineq true) Lp_ineqs_proofs2.extra_ineqs_std3_small in
 754     fun  (hyp_set, hyp_fun) arg split_face ->
 755       let dart_tms = mk_all_darts split_face in
 756       let ye_tms = map (curry mk_comb ye_tm) dart_tms in
 757       let sum_tm = end_itlist (fun tm1 tm2 -> mk_comb (mk_comb (add_op_real, tm1), tm2)) ye_tms in
 758       let inst_list = zip ye_tms [x_var_real; y_var_real; z_var_real] in
 759       let big_tm = mk_comb (mk_comb (le_op_real, c625), sum_tm) and
 760           small_tm = mk_comb (mk_comb (le_op_real, sum_tm), c625) and
 761           split3_th = INST[sum_tm, x_var_real] split3_lemma in
 762       let sym_small_ineqs = (CONJUNCTS o MP (INST inst_list sym_small) o ASSUME) small_tm and
 763           sym_big_ineqs = (CONJUNCTS o MP (INST inst_list sym_big) o ASSUME) big_tm in
 764       let extra_small_ineqs =
 765         let set_th = hyp_set "list_of_darts3" in
 766         let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair (hd dart_tms))) in
 767         let th0 = INST[arg.hyp_list_tm, l_cap_var; hd dart_tms, d_var_pair; arg.e_tm, e_cap_var] small_extra in
 768         let extra0 = (CONJUNCTS o UNDISCH_ALL o MY_PROVE_HYP arg.lp_cond_th o simplify_ineq hyp_fun o MP th0) mem_th in
 769           map (CONV_RULE (convert_condition hyp_fun)) extra0 in
 770       let extra_sym = flatten (map (gen_ye_sym_ineqs arg.ye_sym_th) extra_small_ineqs) in
 771         split3_th, (big_tm, small_tm), (sym_big_ineqs, sym_small_ineqs @ extra_small_ineqs @ extra_sym);;
 772
 773
 774 (* Generate |- 6.25 <= a + b + c and symmetric inequalities when 2.25 <= a *)
 775 let gen_add_big_ineqs =
 776   let c625 = `#6.25` in
 777   let sym_big = (SPEC c625 o ARITH_RULE) `!c. c <= x + y + z ==> c <= y + z + x /\ c <= z + x + y` in
 778   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
 779     fun (hyp_set, hyp_fun) arg split_face ->
 780       let d_tm = mk_dart split_face 0 1 in
 781       let set_th = hyp_set "list_of_darts3" in
 782       let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair d_tm)) in
 783       let th0 = INST[arg.hyp_list_tm, l_cap_var; d_tm, d_var_pair; arg.e_tm, e_cap_var] big_extra in
 784       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
 785       let x_tm, yz_tms = dest_binary "real_add" (rand (concl big_th)) in
 786       let y_tm, z_tm = dest_binary "real_add" yz_tms in
 787       let inst_list = zip [x_tm; y_tm; z_tm] [x_var_real; y_var_real; z_var_real] in
 788         big_th :: CONJUNCTS (MP (INST inst_list sym_big) big_th);;
 789
 790
 791 (* Generates extra inequalities in the case when 2.18 <= yn(i) and 2.18 <= yn(j) for ~(i = j) *)
 792 let gen_mid_ineqs =
 793   let eq13 = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `13` in
 794   let lnsum13_mid_lemma = (REWRITE_RULE[GSYM IMP_IMP; eq13; Seq.size] o
 795                              SPEC_ALL o add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum13_mid in
 796     fun (hyp_set, hyp_fun) arg split_face ->
 797       let i_tm = mk_raw_num (nth split_face 0) in
 798       let j_tm = mk_raw_num (nth split_face 1) in
 799       let th0 = (MY_PROVE_HYP arg.lp_cond_th o
 800                    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
 801       let els_eq_th = hyp_set "list_of_elements" in
 802       let els_tm = rand (concl els_eq_th) in
 803       let indices =
 804         let list = dest_list els_tm in
 805         let i_ind = index i_tm list and
 806             j_ind = index j_tm list in
 807           subtract (0--(length list - 1)) [i_ind; j_ind] in
 808       let th1 = EQ_MP (term_rewrite (concl th0) els_eq_th) th0 in
 809       let th2 = (prove_conditions o simplify_ineq hyp_fun) th1 in
 810       let mem_i = EQT_ELIM (eval_mem_univ raw_eq_hash_conv i_tm els_tm) and
 811           mem_j = EQT_ELIM (eval_mem_univ raw_eq_hash_conv j_tm els_tm) in
 812       let ths = CONJUNCTS (MY_PROVE_HYP mem_i (MY_PROVE_HYP mem_j th2)) in
 813       let lo_th = nth ths 0 and
 814           hi_th1 = nth ths 1 and
 815           hi_th2 = nth ths 2 in
 816       let lo_ineqs1 = select_all lo_th indices in
 817       let lo_ineqs2 = map (prove_conditions o MY_BETA_RULE) lo_ineqs1 in
 818       let ineqs = hi_th1 :: hi_th2 :: lo_ineqs2 in
 819         ineqs @ flatten (map gen_extra_ineqs ineqs);;
 820
 821
 822 (* Generates extra inequalities in the case when 2.36 <= yn(i) *)
 823 let gen_high_ineqs =
 824   let eq13 = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `13` in
 825   let lnsum13_high_lemma = (REWRITE_RULE[GSYM IMP_IMP; eq13; Seq.size] o
 826                               SPEC_ALL o add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum13_high in
 827     fun (hyp_set, hyp_fun) arg split_face ->
 828       let i_tm = mk_raw_num (nth split_face 0) in
 829       let th0 = (MY_PROVE_HYP arg.lp_cond_th o
 830                    INST[arg.e_tm, e_cap_var; arg.hyp_list_tm, l_cap_var; i_tm, i_var_num]) lnsum13_high_lemma in
 831       let els_eq_th = hyp_set "list_of_elements" in
 832       let els_tm = rand (concl els_eq_th) in
 833       let indices =
 834         let list = dest_list els_tm in
 835         let i_ind = index i_tm list in
 836           subtract (0--(length list - 1)) [i_ind] in
 837       let th1 = EQ_MP (term_rewrite (concl th0) els_eq_th) th0 in
 838       let th2 = (prove_conditions o simplify_ineq hyp_fun) th1 in
 839       let mem_i = EQT_ELIM (eval_mem_univ raw_eq_hash_conv i_tm els_tm) in
 840       let lo_th = MY_PROVE_HYP mem_i th2 in
 841       let lo_ineqs1 = select_all lo_th indices in
 842       let ineqs = map (prove_conditions o MY_BETA_RULE) lo_ineqs1 in
 843         ineqs @ flatten (map gen_extra_ineqs ineqs);;
 844
 845
 846 let set_report, reset_progress, next_terminal, report_progress =
 847   let t = ref 0 in
 848   let flag = ref true in
 849     (fun b -> flag := b),
 850     (fun () -> t := 0),
 851   (fun () -> t := !t + 1),
 852   (fun () -> if !flag then (Format.print_string (sprintf "%d " !t); Format.print_flush()) else ());;
 853
 854
 855 let compute_hypermap arg =
 856   if arg.hyp_data = [] then
 857     let good_th = MATCH_MP lp_cond_imp_good_list arg.lp_cond_th in
 858     let hyp_data = compute_all arg.hyp_list_tm (Some good_th) in
 859       {arg with hyp_data = [hyp_data]}, hyp_data
 860   else
 861     arg, hd arg.hyp_data;;
 862
 863
 864 (* Verifies an lp_certificate_case *)
 865 let rec verify_lp_case base_ineqs std_flag (arg, case) =
 866   match case with
 867       (* Terminal case *)
 868     | Lp_terminal terminal ->
 869         let _ = next_terminal() in
 870         let hyp_set, hyp_fun = snd (compute_hypermap arg) in
 871         let r = (fun name, ind, v -> name, ind, map mk_real_int64 v) in
 872         let c = map r terminal.constraints and
 873             tv = map r terminal.target_variables and
 874             vb = map r terminal.variable_bounds in
 875         let th0 = prove_flyspeck_lp_step1 arg.hyp_list_tm hyp_set hyp_fun std_flag terminal.precision terminal.infeasible c tv vb in
 876         let _ = report_progress() in
 877         let th1 = (MY_PROVE_HYP arg.lp_tau_th o INST[arg.e_tm, e_cap_var]) th0 in
 878         let th2 = if std_flag then MY_PROVE_HYP estd_refl th1 else itlist MY_PROVE_HYP base_ineqs th1 in
 879           (MY_PROVE_HYP arg.lp_cond_th) th2
 880     | Lp_split (info, cs) ->
 881         (match info.split_type with
 882            | "tri" ->
 883                verify_split3 base_ineqs std_flag arg info cs
 884            | "quad" ->
 885                verify_split4 base_ineqs std_flag arg info cs
 886            | "pent" ->
 887                verify_split5 base_ineqs std_flag arg info cs
 888            | "hex" ->
 889                verify_split6 base_ineqs std_flag arg info cs
 890            | "edge" ->
 891                verify_edge base_ineqs std_flag arg info cs
 892            | "218" ->
 893                verify_218 base_ineqs std_flag arg info cs
 894            | "236" ->
 895                verify_236 base_ineqs std_flag arg info cs
 896            | "mid" ->
 897                verify_mid base_ineqs std_flag arg info cs
 898            | "high" ->
 899                verify_high base_ineqs std_flag arg info cs
 900            | "add_big" ->
 901                verify_add_big base_ineqs std_flag arg info cs
 902            | s -> failwith ("verify_lp_case: unknown case " ^ s))
 903
 904 (* Adds a new big triangle if one of its edges is >= #2.25 *)
 905 and verify_add_big base_ineqs std_flag arg info cs =
 906   let arg, hyp_data = compute_hypermap arg in
 907   let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
 908   let ineqs = gen_add_big_ineqs hyp_data arg info.split_face in
 909     itlist MY_PROVE_HYP ineqs case
 910
 911 (* Adds additional node inequalities *)
 912 and verify_mid base_ineqs std_flag arg info cs =
 913   let arg, hyp_data = compute_hypermap arg in
 914   let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
 915   let ineqs = gen_mid_ineqs hyp_data arg info.split_face in
 916     itlist MY_PROVE_HYP ineqs case
 917
 918 (* Adds additional node inequalities *)
 919 and verify_high base_ineqs std_flag arg info cs =
 920   let arg, hyp_data = compute_hypermap arg in
 921   let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
 922   let ineqs = gen_high_ineqs hyp_data arg info.split_face in
 923     itlist MY_PROVE_HYP ineqs case
 924
 925 (* Nodes: 2.18 <= yn(i) \/ yn(i) <= 2.18 *)
 926 and verify_218 base_ineqs std_flag arg info cs =
 927   let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
 928   let split_th = INST[mk_raw_num (hd info.split_face), i_var_num] split218_lemma in
 929   let split_cases = striplist dest_disj (concl split_th) in
 930   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 931   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 932     final_th
 933
 934 (* Nodes: yn(i) <= 2.36 \/ 2.36 <= yn(i) *)
 935 and verify_236 base_ineqs std_flag arg info cs =
 936   let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
 937   let split_th = INST[mk_raw_num (hd info.split_face), i_var_num] split236_lemma in
 938   let split_cases = striplist dest_disj (concl split_th) in
 939   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 940   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 941     final_th
 942
 943 (* Edges: 2.25 <= ye(d) \/ ye(d) <= 2.25 *)
 944 and verify_edge base_ineqs std_flag arg info cs =
 945   let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
 946   let split_th = INST[mk_dart info.split_face 0 1, d_var_pair] split225_lemma in
 947   let split_cases = striplist dest_disj (concl split_th) in
 948   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 949   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 950     final_th
 951
 952 (* Triangle *)
 953 and verify_split3 base_ineqs std_flag arg info cs =
 954   let arg, hyp_data = compute_hypermap arg in
 955     (* Prove all subcases *)
 956   let case1_th = verify_lp_case base_ineqs std_flag (arg, nth cs 0) and
 957       case2_th = verify_lp_case base_ineqs std_flag (arg, nth cs 1) in
 958     (* Combine subcases *)
 959   let split_th, (case1_tm, case2_tm), (case1_ineqs, case2_ineqs) = gen_triangle_ineqs hyp_data arg info.split_face in
 960   let th1 = DISCH case1_tm (itlist MY_PROVE_HYP case1_ineqs case1_th) and
 961       th2 = DISCH case2_tm (itlist MY_PROVE_HYP case2_ineqs case2_th) in
 962   let final_th = MP (combine_cases th1 th2) split_th in
 963     final_th
 964
 965 (* Quad *)
 966 and verify_split4 base_ineqs std_flag arg info cs =
 967   let d13_tm = mk_dart info.split_face 1 2 and
 968       d24_tm = mk_dart info.split_face 0 1 and
 969       diag1_tm = mk_dart info.split_face 0 2 and
 970       diag2_tm = mk_dart info.split_face 1 3 in
 971     (* compute lp_cond *)
 972   let (split13_tm, e13), lp_cond13 = split_lp_conditions arg.hyp_list_tm arg.lp_cond_th d13_tm and
 973       (split24_tm, e24), lp_cond24 = split_lp_conditions arg.hyp_list_tm arg.lp_cond_th d24_tm in
 974     (* compute lp_tau *)
 975   let arg, hyp_data = compute_hypermap arg in
 976   let tau13 = get_tau_split_th tau_split4 hyp_data arg d13_tm and
 977       tau24 = get_tau_split_th tau_split4 hyp_data arg d24_tm in
 978     (* Prove all subcases *)
 979   let arg13 = {arg with hyp_data = []; lp_cond_th = lp_cond13; lp_tau_th = tau13; hyp_list_tm = split13_tm; e_tm = e13} and
 980       arg24 = {arg with hyp_data = []; lp_cond_th = lp_cond24; lp_tau_th = tau24; hyp_list_tm = split24_tm; e_tm = e24} in
 981   let args = zip [arg13; arg24; arg13; arg24; arg] cs in
 982   let cases = map2 (verify_lp_case base_ineqs) [false; false; false; false; std_flag] args in
 983     (* Combine subcases *)
 984   let split_th = INST[diag1_tm, nth diag_vars 1; diag2_tm, nth diag_vars 2] split4_lemma in
 985   let split_cases = striplist dest_disj (concl split_th) in
 986   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
 987   let final_th = MP (end_itlist combine_cases final_cases) split_th in
 988     final_th
 989
 990 (* Pent *)
 991 and verify_split5 base_ineqs std_flag arg info cs =
 992   let dart_tms = rotateL 1 (mk_all_darts info.split_face) in
 993   let lp_conds_one = map (split_lp_conditions arg.hyp_list_tm arg.lp_cond_th) dart_tms in
 994   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
 995     (* compute lp_tau_th *)
 996   let arg, (hyp_set, hyp_fun) = compute_hypermap arg in
 997   let tau_ths_one = map (get_tau_split_th tau_split5_one (hyp_set, hyp_fun) arg) dart_tms in
 998   let tau_ths_two =
 999     let ths = map (get_tau_split_th tau_split5_two (hyp_set, hyp_fun) arg) dart_tms in
1000       map ((CONV_RULE o RAND_CONV o RAND_CONV o RAND_CONV o RAND_CONV) (convert_tm hyp_fun)) ths in
1001     (* Prove all subcases *)
1002   let args = arg :: map2 (fun ((split_tm, e_tm), lp_cond_th) tau_th ->
1003                             {arg with hyp_data = []; lp_cond_th = lp_cond_th; lp_tau_th = tau_th;
1004                                hyp_list_tm = split_tm; e_tm = e_tm})
1005     (lp_conds_one @ lp_conds_two) (tau_ths_one @ tau_ths_two) in
1006   let std_flags = std_flag :: replicate false 10 in
1007   let cases = map2 (verify_lp_case base_ineqs) std_flags (zip args cs) in
1008     (* Combine subcases *)
1009   let split_face_tms = map mk_raw_num info.split_face in
1010   let diag_tms = map mk_pair (zip split_face_tms (rotateL 2 split_face_tms)) in
1011   let split_th = INST (zip diag_tms (take 5 (drop 1 diag_vars))) split5_lemma in
1012   let split_cases = striplist dest_disj (concl split_th) in
1013   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
1014   let final_th = MP (end_itlist combine_cases final_cases) split_th in
1015     final_th
1016
1017 (* Hex *)
1018 and verify_split6 base_ineqs std_flag arg info cs =
1019   let _ = report "Warning: hex splitting case" in
1020   let dart_tms = rotateL 1 (mk_all_darts info.split_face) in
1021   let lp_conds = map (split_lp_conditions arg.hyp_list_tm arg.lp_cond_th) dart_tms in
1022     (* compute lp_tau_th *)
1023   let arg, hyp_data = compute_hypermap arg in
1024   let lp_tau_ths = map (get_tau_split_th tau_split6 hyp_data arg) dart_tms in
1025     (* Prove all subcases *)
1026   let args = arg :: map2 (fun ((split_tm, e_tm), lp_cond_th) tau_th ->
1027                             {arg with hyp_data = []; lp_cond_th = lp_cond_th; lp_tau_th = tau_th;
1028                                hyp_list_tm = split_tm; e_tm = e_tm}) lp_conds lp_tau_ths in
1029   let std_flags = std_flag :: replicate false 6 in
1030   let cases = map2 (verify_lp_case base_ineqs) std_flags (zip args cs) in
1031     (* Combine subcases *)
1032   let split_face_tms = map mk_raw_num info.split_face in
1033   let diag_tms = map mk_pair (zip split_face_tms (rotateL 2 split_face_tms)) in
1034   let split_th = INST (zip diag_tms (take 6 (drop 1 diag_vars))) split6_lemma in
1035   let split_cases = striplist dest_disj (concl split_th) in
1036   let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
1037   let final_th = MP (end_itlist combine_cases final_cases) split_th in
1038     final_th;;
1039
1040
1041 (* Verifies an lp_certificate *)
1042 let verify_lp_certificate certificate =
1043   let n = count_terminals certificate.root_case in
1044   let hyp_list = (snd o convert_to_list) certificate.hypermap_string in
1045   let hyp_list0_tm = (to_num o create_hol_list) hyp_list in
1046   let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None in
1047   let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0 in
1048   let ye_sym_th = (MY_PROVE_HYP lp_cond0 o INST[estd_v, e_cap_var]) ye_sym0 in
1049   let base_ineqs =
1050     if n == 1 then [] else
1051       let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o
1052         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
1053       let r2 = (map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th)) o r in
1054         (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
1055   let arg = {hyp_data = [hyp_set0, hyp_fun0]; ye_sym_th = ye_sym_th;
1056              lp_cond_th = EXPAND_CONCL_RULE "L" lp_cond0; lp_tau_th = lp_tau0;
1057              hyp_list_tm = hyp_list0_tm; e_tm = estd_v} in
1058
1059   let _ = reset_progress(); Format.print_string (sprintf "terminals = %d: " n); Format.print_flush() in
1060
1061   let final_th = verify_lp_case base_ineqs true (arg, certificate.root_case) in
1062   let _ = Format.print_newline() in
1063     (DISCH contravening_v o EXPAND_RULE "L" o EXPAND_RULE "g" o EXPAND_RULE "h") final_th;;
1064
1065
1066 end;;