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";;
10 module Flyspeck_lp = struct
14 open Linear_function;;
18 open List_hypermap_computations;;
19 open List_conversions;;
20 open Lp_approx_ineqs;;
23 open Lp_informal_computations;;
24 open Lp_ineqs_proofs;;
25 open Lp_main_estimate;;
29 let _ = Lp_head_ineqs.add_head_ineqs() in
30 let _ = Lp_body_ineqs.add_body_ineqs() in
31 Lp_ineqs.process_raw_ineqs();;
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;;
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]);;
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
57 (* Performs the following conversions:
58 (a + ... + c) + d = a + ... + c + d *)
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))
76 (**********************)
78 let convert_ineq hyp_fun =
79 let rec rewrite_lhs 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
85 let rec convert_arg arg =
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
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
99 if (const_name = "set_of_list") then
101 else if (const_name = "FST") then
103 else if (const_name = "SND") then
105 else if (const_name = "HD") then
107 else if (const_name = "e_list") then
110 hyp_fun const_name (rand rtm) in
113 failwith ("convert_arg: "^const_name)
117 let arg_th = convert_arg arg in
118 AP_TERM mul_tm (AP_TERM var_f arg_th)
121 (* tm should be list_sum *)
122 list_sum_conv BETA_CONV tm in
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
138 if not (is_binary "real_le" ineq_tm) then
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;;
148 let num_str = (fst o dest_const) Arith_hash.num_const in
149 let rec convert hyp_fun tm =
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
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
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))
169 let rtm_th = convert hyp_fun rtm in
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
176 if const_name = num_str then
177 INST[rand arg, n_var_num] Arith_hash.NUM_THM
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
187 (try hyp_fun const_name (rand arg)
188 with Failure _ -> REFL arg) in
197 let convert_condition hyp_fun tm =
199 let ltm, rtm = dest_comb tm in
200 let r_th = convert_tm hyp_fun rtm in
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)
208 convert_tm hyp_fun tm;;
212 let rec simplify_ineq_tm hyp_fun tm =
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)
220 convert_ineq hyp_fun tm;;
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;;
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
234 (* (trivial) equality *)
236 let ltm, rtm = dest_eq p_tm in
242 else if is_binary "<" p_tm then
243 true, EQT_ELIM (raw_lt_hash_conv p_tm)
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
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'
275 let ineq2_ths = map (simplify_ineq hyp_fun) ineq1_ths in
276 let ineq3_ths = map prove_conditions ineq2_ths in
280 (****************************)
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;;
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
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) ->
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
299 | Failure str -> failwith (sprintf "Problem: %s (%s)" name str)
300 | _ -> failwith ("Problem: "^name) in
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
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
316 Hashtbl.replace var_table var ineq
318 Hashtbl.add var_table var th) m_ineqs in
321 let get_first_var ineq_th =
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);;
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) ->
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
359 | Failure str -> failwith (sprintf "Problem: %s (%s)" name str)
360 | _ -> failwith ("Problem: "^name) in
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
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
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);;
383 (*************************)
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;;
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
396 (`(?) (P:A->bool) ==> P((@) P)`,
397 SIMP_TAC[SELECT_AX; ETA_AX]) in
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";;
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;;
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;;
421 (*************************)
422 (* Auxiliary definitions *)
423 (*************************)
426 Format.print_string s; Format.print_newline(); Format.print_flush();;
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);;
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));;
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 =
445 | (k,v) :: t -> if k = a then v :: assoc_all a t else assoc_all a t;;
447 (* Combines theorems |- A ==> C, |- B ==> C and yields |- A \/ B ==> C *)
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);;
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"
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);;
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;;
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);;
492 (* Pent split cases *)
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
509 (* Hex split cases *)
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)
518 \/ a6 <= sqrt8`, ARITH_TAC);;
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;;
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]);;
528 (* ESTD V = ESTD V *)
529 let estd_refl = REFL estd_v;;
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);;
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);;
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]);;
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;;
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;;
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;;
557 (*****************************************)
559 (* Generates extra inequalities for a given inequality. *)
560 (* For instance, |- a <= sqrt8 yields |- a <= &3 *)
561 let gen_extra_ineqs =
563 tm_sqrt8 = `sqrt8` and
567 let r tm = prove(tm, MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC) in
569 tm_3, r `&3 <= a ==> sqrt8 <= a`;
570 tm_236, r `#2.36 <= a ==> #2.18 <= a`;
573 tm_sqrt8, r `a <= sqrt8 ==> a <= &3`;
574 tm_218, r `a <= #2.18 ==> a <= #2.36`;
576 let a_var_real = `a:real` in
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
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 =
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]
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);;
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));;
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;;
621 (*******************************)
622 (* Verification test functions *)
623 (*******************************)
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) =
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)
638 | "high" | "mid" | "add_big" ->
639 let case_args = zip [hyp_list] cs in
640 flatten (map terminal_cases case_args)
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)
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)
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)
669 | s -> failwith ("cases: unknown split type: " ^ s));;
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);;
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;;
696 (*******************************)
697 (* Main verification functions *)
698 (*******************************)
700 type lp_verification_arg = {
702 hyp_data : ((string->thm) * (string->term->thm))list;
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;;
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;;
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);;
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
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);;
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);;
791 (* Generates extra inequalities in the case when 2.18 <= yn(i) and 2.18 <= yn(j) for ~(i = j) *)
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
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);;
822 (* Generates extra inequalities in the case when 2.36 <= yn(i) *)
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
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);;
846 let set_report, reset_progress, next_terminal, report_progress =
848 let flag = ref true in
849 (fun b -> flag := b),
851 (fun () -> t := !t + 1),
852 (fun () -> if !flag then (Format.print_string (sprintf "%d " !t); Format.print_flush()) else ());;
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
861 arg, hd arg.hyp_data;;
864 (* Verifies an lp_certificate_case *)
865 let rec verify_lp_case base_ineqs std_flag (arg, 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
883 verify_split3 base_ineqs std_flag arg info cs
885 verify_split4 base_ineqs std_flag arg info cs
887 verify_split5 base_ineqs std_flag arg info cs
889 verify_split6 base_ineqs std_flag arg info cs
891 verify_edge base_ineqs std_flag arg info cs
893 verify_218 base_ineqs std_flag arg info cs
895 verify_236 base_ineqs std_flag arg info cs
897 verify_mid base_ineqs std_flag arg info cs
899 verify_high base_ineqs std_flag arg info cs
901 verify_add_big base_ineqs std_flag arg info cs
902 | s -> failwith ("verify_lp_case: unknown case " ^ s))
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
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
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
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
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
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
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
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
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
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
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
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
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
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
1059 let _ = reset_progress(); Format.print_string (sprintf "terminals = %d: " n); Format.print_flush() in
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;;