needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_head_ineqs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_body_ineqs.hl";;
needs "../formal_lp/hypermap/main/lp_certificate.hl";;
needs "../formal_lp/hypermap/computations/list_hypermap_computations.hl";;
needs "../formal_lp/hypermap/computations/informal_computations.hl";;
needs "../formal_lp/more_arith/prove_lp.hl";;


module Flyspeck_lp = struct

open List;;
open Arith_misc;;
open Linear_function;;
open Prove_lp;;
open Arith_nat;;
open Misc_vars;;
open List_hypermap_computations;;
open List_conversions;;
open Lp_approx_ineqs;;
open Lp_ineqs;;
open Lp_certificate;;
open Lp_informal_computations;;
open Lp_ineqs_proofs;;
open Lp_main_estimate;;


let init_ineqs() =
  let _ = Lp_head_ineqs.add_head_ineqs() in
  let _ = Lp_body_ineqs.add_body_ineqs() in
    Lp_ineqs.process_raw_ineqs();;


(* Prepare theorems for the final inequality: &12 <= scriptL V *)
let to_lin_f_ineq ineq_th =
  let lhs, rhs = dest_binop le_op_real (concl ineq_th) in
  let lhs_th = LIN_F_CONV lhs in
    EQ_MP (AP_THM (AP_TERM le_op_real lhs_th) rhs) ineq_th;;

let FINAL_INEQ = (MY_RULE_NUM o prove)(`lin_f [] <= -- &n <=> n = 0`,
		     REWRITE_TAC[LIN_F_EMPTY; REAL_NEG_GE0; REAL_OF_NUM_LE; LE]);;

let lnsum_ineqs =
  
let DECIMAL_INT = 
prove(`!n. DECIMAL n 1 = &n`,
REWRITE_TAC[DECIMAL; REAL_DIV_1]) in let ineq_th = (add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum_ineq in let ineq_tm = concl ineq_th in let ths1 = create_approximations [9;12;15;18;21] ineq_tm in let ths2 = map generalize_hyp ths1 in let ths3 = map (itlist PROVE_HYP Lp_ineqs_def.list_var_pos) ths2 in let ths4 = map (C MP ineq_th) ths3 in let r = CONV_RULE(REWRITE_CONV[DECIMAL_INT; GSYM LIST_SUM_LMUL] THENC DEPTH_CONV Arith_nat.NUMERAL_TO_NUM_CONV) in let ths5 = map r ths4 in zip (3--7) ths5;;
(* Performs the following conversions: (a + ... + c) + d = a + ... + c + d *) let plus_assoc_conv = let REAL_ADD_ASSOC' = (SYM o SPEC_ALL) REAL_ADD_ASSOC in let rec plus_conv tm = if (is_binop add_op_real tm) then let lhs, rhs = dest_binop add_op_real tm in if (is_binop add_op_real lhs) then let x_tm, y_tm = dest_binop add_op_real lhs in let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; rhs, z_var_real] REAL_ADD_ASSOC' in let ltm, rtm = dest_comb(rand(concl th0)) in TRANS th0 (AP_TERM ltm (plus_conv rtm)) else REFL tm else REFL tm in plus_conv;; (**********************) let convert_ineq hyp_fun = let rec rewrite_lhs tm = let rewrite_one tm = if (is_binop mul_op_real tm) then let mul_tm, var_tm = dest_comb tm in let var_f, arg = dest_comb var_tm in let rec convert_arg arg = if (is_comb arg) then let ltm, sub_arg' = dest_comb arg in let const_name = (fst o dest_const) (if (is_const ltm) then ltm else rator ltm) in (* Str.first_chars const_name 1 = "D" is a hack *) if (Str.first_chars const_name 1 = "D" or const_name = "_0" or const_name = "," or const_name = "CONS" or const_name = "INSERT") then REFL arg else try let sub_arg_th = convert_arg sub_arg' in let th0 = AP_TERM ltm sub_arg_th in let rtm = rand(concl th0) in let th1 = if (const_name = "set_of_list") then set_of_list_conv rtm else if (const_name = "FST") then fst_conv rtm else if (const_name = "SND") then snd_conv rtm else if (const_name = "HD") then hd_conv rtm else if (const_name = "e_list") then e_list_conv_num rtm else hyp_fun const_name (rand rtm) in TRANS th0 th1 with _ -> failwith ("convert_arg: "^const_name) else REFL arg in let arg_th = convert_arg arg in AP_TERM mul_tm (AP_TERM var_f arg_th) else (* tm should be list_sum *) list_sum_conv BETA_CONV tm in if (is_binop add_op_real tm) then let lhs, rhs = dest_binop add_op_real tm in let lhs_th = rewrite_one lhs in let rhs_th = rewrite_lhs rhs in let th1 = MK_COMB(AP_TERM add_op_real lhs_th, rhs_th) in if (is_binop add_op_real (rand(concl lhs_th))) then let th2 = plus_assoc_conv (rand(concl th1)) in TRANS th1 th2 else th1 else rewrite_one tm in fun ineq_tm -> if not (is_binary "real_le" ineq_tm) then REFL ineq_tm else let ltm, rtm = dest_comb ineq_tm in let op_tm, l_tm = dest_comb ltm in let lhs_eq_th = rewrite_lhs l_tm in AP_THM (AP_TERM op_tm lhs_eq_th) rtm;; let convert_tm = let num_str = (fst o dest_const) Arith_hash.num_const in let rec convert hyp_fun tm = if (is_comb tm) then let ltm, rtm = dest_comb tm in let op_tm = if is_comb ltm then rator ltm else ltm in if is_const op_tm then let const_name = (fst o dest_const) op_tm in if const_name = "real_of_num" or const_name = "DECIMAL" then REFL tm else if const_name = "real_add" then let th1 = convert hyp_fun (rand ltm) and th2 = convert hyp_fun rtm in MK_COMB (AP_TERM op_tm th1, th2) else if const_name = "ye_list" then if is_pair rtm then let ltm', b_tm = dest_comb rtm in let pair_op, a_tm = dest_comb ltm' in let a_th = convert hyp_fun a_tm and b_th = convert hyp_fun b_tm in AP_TERM ltm (MK_COMB (AP_TERM pair_op a_th, b_th)) else let rtm_th = convert hyp_fun rtm in AP_TERM ltm rtm_th else let rtm_th = convert hyp_fun rtm in let th0 = AP_TERM ltm rtm_th in let arg = rand (concl th0) in let th1 = if const_name = num_str then INST[rand arg, n_var_num] Arith_hash.NUM_THM else match const_name with | "set_of_list" -> set_of_list_conv arg | "FST" -> fst_conv arg | "SND" -> snd_conv arg | "HD" -> hd_conv arg | "e_list" -> e_list_conv_num arg | "LENGTH" -> length_conv arg | _ -> (try hyp_fun const_name (rand arg) with Failure _ -> REFL arg) in TRANS th0 th1 else REFL tm else REFL tm in convert;; let convert_condition hyp_fun tm = if is_comb tm then let ltm, rtm = dest_comb tm in let r_th = convert_tm hyp_fun rtm in if is_comb ltm then let op_tm, larg = dest_comb ltm in let l_th = convert_tm hyp_fun larg in MK_COMB (AP_TERM op_tm l_th, r_th) else AP_TERM ltm r_th else convert_tm hyp_fun tm;; let rec simplify_ineq_tm hyp_fun tm = if is_imp tm then let ltm, q_tm = dest_comb tm in let imp_tm, p_tm = dest_comb ltm in let p_eq_th = convert_condition hyp_fun p_tm in let q_eq_th = simplify_ineq_tm hyp_fun q_tm in MK_COMB (AP_TERM imp_tm p_eq_th, q_eq_th) else convert_ineq hyp_fun tm;; let simplify_ineq hyp_fun ineq_th = let eq_th = simplify_ineq_tm hyp_fun (concl ineq_th) in EQ_MP eq_th ineq_th;; let prove_conditions =
let neq_elim_th = 
prove(`(s <=> F) <=> ~s`,
REWRITE_TAC[]) in let rec prove_rec ineq_th = let concl_tm = concl ineq_th in if is_imp concl_tm then let p_tm = lhand concl_tm in let flag, p_th = (* (trivial) equality *) if is_eq p_tm then let ltm, rtm = dest_eq p_tm in if ltm = rtm then true, REFL ltm else false, TRUTH (* n < m:num *) else if is_binary "<" p_tm then true, EQT_ELIM (raw_lt_hash_conv p_tm) (* ~(n = m) *) else if is_neg p_tm then let s_tm = rand p_tm in let th0 = raw_eq_hash_conv s_tm in let elim_th = INST[s_tm, s_var_bool] neq_elim_th in true, EQ_MP elim_th th0 else false, TRUTH in let th1 = if flag then MP ineq_th p_th else UNDISCH ineq_th in prove_rec th1 else ineq_th in prove_rec;;
let get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices = let ineq0_th = (find_ineq std_flag precision name).ineq_th in let ineq1_th = INST[hyp_list_tm, l_cap_var] ineq0_th in let all_tm, set_tm = dest_comb (concl ineq1_th) in let set_eq_th = hyp_set ((fst o dest_const o rator) set_tm) in let ineq2_th = EQ_MP (AP_TERM all_tm set_eq_th) ineq1_th in let ineq0_ths = select_all ineq2_th indices in let ineq1_ths' = map MY_BETA_RULE ineq0_ths in (* A special treatment of the "main" inequality *) let ineq1_ths = if name = "main" then map (fun th -> EQ_MP (term_rewrite (concl th) (hyp_set "list_of_elements")) th) ineq1_ths' else ineq1_ths' in let ineq2_ths = map (simplify_ineq hyp_fun) ineq1_ths in let ineq3_ths = map prove_conditions ineq2_ths in ineq3_ths;; (****************************) let int_zero_tm = mk_comb (amp_op_real, (rand o concl o NUMERAL_TO_NUM_CONV) `0`);; let int_neg_zero_tm = mk_comb (neg_op_real, int_zero_tm);; let var_table = Hashtbl.create 1000;; let prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun std_flag precision infeasible constraints target_variables variable_bounds = let precision_constant = Int 10 **/ (Int precision) in (* This function generates all inequalities with the given name and indices, multiplies these inequalities by given coefficients, and finds the sum of the generated inequalities *) let sum_step = fun (name, indices, c) -> try let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in let s1 = map transform_le_ineq (zip ineqs c) in List.fold_left add_step' dummy s1 with | Failure str -> failwith (sprintf "Problem: %s (%s)" name str) | _ -> failwith ("Problem: "^name) in let _ = Hashtbl.clear var_table in let add_to_var_table (name, indices, c) = let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in let m_ineqs = map2 (fun th m -> MY_PROVE_HYP th (var1_le_transform (concl th, m))) ineqs c in let _ = map ( fun th -> let var = (rand o lhand o concl) th in if Hashtbl.mem var_table var then let ineq1 = Hashtbl.find var_table var in let ineq = add_le_ineqs th ineq1 in let c_tm = (lhand o lhand o concl) ineq in if c_tm = int_zero_tm or c_tm = int_neg_zero_tm then Hashtbl.remove var_table var else Hashtbl.replace var_table var ineq else Hashtbl.add var_table var th) m_ineqs in () in let get_first_var ineq_th = try (rand o lhand o rand o lhand o concl) ineq_th with Failure _ -> a_var_real in let ineqs1 = map sum_step constraints in let ineqs2 = List.sort (fun ineq1 ineq2 -> let var1 = get_first_var ineq1 and var2 = get_first_var ineq2 in compare var1 var2) ineqs1 in let s1' = List.fold_right add_step' ineqs2 dummy in let s1 = mul_step s1' (mk_real_int precision_constant) in let r1 = if infeasible then s1 else let ineq_th0 = assoc precision lnsum_ineqs in let ineq_th1 = (INST[hyp_list_tm, l_cap_var]) ineq_th0 in let ineq_th2 = EQ_MP (term_rewrite (concl ineq_th1) (hyp_set "list_of_elements")) ineq_th1 in let ineq_th3 = simplify_ineq hyp_fun ineq_th2 in let ineq_th4 = to_lin_f_ineq ineq_th3 in add_step' ineq_th4 s1 in let _ = map add_to_var_table variable_bounds and _ = map add_to_var_table target_variables in let list1 = Hashtbl.fold (fun tm ineq list -> (tm, ineq) :: list) var_table [] in let list2 = List.sort (fun (tm1, _) (tm2, _) -> compare tm1 tm2) list1 in let var_list = map snd list2 in let result = List.fold_left add_cancel_step r1 var_list in let n_tm = (rand o rand o rand o concl) result in let r_eq_th = INST[n_tm, n_var_num] FINAL_INEQ in let not_zero_th = NUM_EQ0_HASH_CONV n_tm in EQ_MP not_zero_th (EQ_MP r_eq_th result);; (* let prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun std_flag precision infeasible constraints target_variables variable_bounds = let precision_constant = Int 10 **/ (Int precision) in let sum_step = fun (name, indices, c) -> try let ineqs = get_ineqs (hyp_list_tm, hyp_set, hyp_fun) std_flag precision name indices in let s1 = map transform_le_ineq (zip ineqs c) in List.fold_left add_step' dummy s1 with | Failure str -> failwith (sprintf "Problem: %s (%s)" name str) | _ -> failwith ("Problem: "^name) in let s1' = List.fold_left add_step' dummy (map sum_step constraints) in let s1 = mul_step s1' (mk_real_int precision_constant) in let s2 = List.fold_left add_step' dummy (map sum_step target_variables) in let s3 = List.fold_left add_step' dummy (map sum_step variable_bounds) in let s4 = add_step' (add_step' s1 s2) s3 in let result = if infeasible then s4 else let ineq_th0 = assoc precision lnsum_ineqs in let ineq_th1 = (INST[hyp_list_tm, l_cap_var]) ineq_th0 in let ineq_th2 = EQ_MP (term_rewrite (concl ineq_th1) (hyp_set "list_of_elements")) ineq_th1 in let ineq_th3 = simplify_ineq hyp_fun ineq_th2 in let ineq_th4 = to_lin_f_ineq ineq_th3 in add_step' ineq_th4 s4 in let n_tm = (rand o rand o rand o concl) result in let r_eq_th = INST[n_tm, n_var_num] FINAL_INEQ in let not_zero_th = NUM_EQ0_HASH_CONV n_tm in EQ_MP not_zero_th (EQ_MP r_eq_th result);; *) (*************************) (* Replaces the given term tm with a variable named var_name in the given theorem th *) (* A new assumption tm = var_name is added *) let ABBREV_RULE var_name tm th = let var_tm = mk_var (var_name, type_of tm) in let eq_th = ASSUME (mk_eq (tm, var_tm)) in (UNDISCH_ALL o PURE_REWRITE_RULE[eq_th] o DISCH_ALL) th;; (* Transforms a theorem |- ?x. P x into (@x. P x) = x |- P x *) let SELECT_AND_ABBREV_RULE = let P = `P:A->bool` in
let pth = 
prove (`(?) (P:A->bool) ==> P((@) P)`,
SIMP_TAC[SELECT_AX; ETA_AX]) in fun th -> try let abs = rand (concl th) in let var, b_tm = dest_abs abs in let name, ty = dest_var var in let select_tm = mk_binder "@" (var, b_tm) in let th0 = CONV_RULE BETA_CONV (MP (PINST [ty,aty] [abs,P] pth) th) in ABBREV_RULE name select_tm th0 with Failure _ -> failwith "SELECT_AND_ABBREV_RULE";
; (* Transforms a theorem tm = var_name, G |- P into G[tm/var_name] |- P[tm/var_name] *) let EXPAND_RULE var_name th = let hyp_tm = find (fun tm -> is_eq tm && is_var (rand tm) && name_of (rand tm) = var_name) (hyp th) in let l_tm, var_tm = dest_eq hyp_tm in let th1 = INST[l_tm, var_tm] th in PROVE_HYP (REFL l_tm) th1;; (* Transforms a theorem tm = var_name, G |- P into tm = var_name, G |- P[tm/var_name] *) let EXPAND_CONCL_RULE var_name th = let hyp_tm = find (fun tm -> is_eq tm && is_var (rand tm) && name_of (rand tm) = var_name) (hyp th) in let eq_th = SYM (ASSUME hyp_tm) in PURE_REWRITE_RULE[eq_th] th;; (*************************) (* Auxiliary definitions *) (*************************) let report s = Format.print_string s; Format.print_newline(); Format.print_flush();; let e_cap_var = `E:(real^3->bool)->bool` and l_cap_var = `L:((num)list)list` and estd_v = `ESTD V` and contravening_v = `contravening V` and d_var_pair = `d:num#num` and diag_vars = map (fun i -> mk_var ("diag" ^ string_of_int i, `:num#num`)) (0--6) and a_vars = map (fun i -> mk_var ("a" ^ string_of_int i, `:real`)) (0--6);; let mk_raw_num = rand o Arith_nat.mk_small_numeral_array;; let mk_dart face i1 i2 = mk_pair (mk_raw_num (nth face i1), mk_raw_num (nth face i2));; let mk_all_darts face = map mk_pair (list_pairs (map mk_raw_num face));; (* Given a list of pairs [x1,y1; ...; xn,yn] and an element x, *) (* finds all y's such that (x,y) is in the list *) let rec assoc_all a list = match list with | [] -> [] | (k,v) :: t -> if k = a then v :: assoc_all a t else assoc_all a t;; (* Combines theorems |- A ==> C, |- B ==> C and yields |- A \/ B ==> C *) let combine_cases = let combine_th = TAUT `(A ==> C) /\ (B ==> C) ==> (A \/ B ==> C)` in fun case1_th case2_th -> MATCH_MP combine_th (CONJ case1_th case2_th);; let dest_ye_list tm = let lhs, rhs = dest_comb tm in let c_tm = rator lhs in if (fst o dest_const) c_tm <> "ye_list" then failwith "dest_ye_list: not ye_list" else dest_pair rhs;; (* Given |- ALL (\x. P x) (hypermap_set), *) (* returns |- P x1, ..., |- P xn for all elements x in hypermap_set *) let get_all_ineqs hyp_set0 all_ineq_th = let all_tm, set_tm = dest_comb (concl all_ineq_th) in let set_eq_th = hyp_set0 ((fst o dest_const o rator) set_tm) in let ineq1_th = EQ_MP (AP_TERM all_tm set_eq_th) all_ineq_th in map MY_BETA_RULE (get_all ineq1_th);; (* Generates a list inequality from a fan inequality. *) (* If simplify_all_flag is true then the conclusion of *) (* the generated inequality is simplified (yi's are transformed into ye). *) let gen_list_ineq simplify_all_flag th = let th0 = add_lp_hyp true th in let tm1, proof_th = mk_lp_ineq th0 in let raw_data = {name = "tmp"; tm = tm1; proof = Some proof_th; std_only = false} in generate_ineq1 simplify_all_flag raw_data;; (******************) (* Special lemmas *) (******************) (* Quad split cases *) let split4_lemma = (INST[`ye_list (g:num#num->real^3#real^3) diag1`, `a:real`; `ye_list (g:num#num->real^3#real^3) diag2`, `b:real`] o prove) (`(a <= b /\ a <= sqrt8) \/ (b <= a /\ b <= sqrt8) \/ (a <= b /\ sqrt8 <= a /\ a <= &3) \/ (b <= a /\ sqrt8 <= b /\ b <= &3) \/ (&3 <= a /\ &3 <= b)`, MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC);; (* Pent split cases *) let split5_lemma = let inst = zip (map (fun d -> mk_comb (`ye_list (g:num#num->real^3#real^3)`, d)) diag_vars) a_vars in (INST inst o prove)(`(sqrt8 <= a1 /\ sqrt8 <= a2 /\ sqrt8 <= a3 /\ sqrt8 <= a4 /\ sqrt8 <= a5) \/ (a1 <= sqrt8 /\ sqrt8 <= a3 /\ sqrt8 <= a4) \/ (a2 <= sqrt8 /\ sqrt8 <= a4 /\ sqrt8 <= a5) \/ (a3 <= sqrt8 /\ sqrt8 <= a5 /\ sqrt8 <= a1) \/ (a4 <= sqrt8 /\ sqrt8 <= a1 /\ sqrt8 <= a2) \/ (a5 <= sqrt8 /\ sqrt8 <= a2 /\ sqrt8 <= a3) \/ (a1 <= sqrt8 /\ a3 <= sqrt8) \/ (a2 <= sqrt8 /\ a4 <= sqrt8) \/ (a3 <= sqrt8 /\ a5 <= sqrt8) \/ (a4 <= sqrt8 /\ a1 <= sqrt8) \/ (a5 <= sqrt8 /\ a2 <= sqrt8)`, MAP_EVERY DISJ_CASES_TAC (map (fun tm -> SPECL[tm; `sqrt8`] REAL_LE_TOTAL) (take 5 (drop 1 a_vars))) THEN ASM_REWRITE_TAC[]);; (* Hex split cases *) let split6_lemma = let inst = zip (map (fun d -> mk_comb (`ye_list (g:num#num->real^3#real^3)`, d)) diag_vars) a_vars in (INST inst o prove)(`(sqrt8 <= a1 /\ sqrt8 <= a2 /\ sqrt8 <= a3 /\ sqrt8 <= a4 /\ sqrt8 <= a5 /\ sqrt8 <= a6) \/ a1 <= sqrt8 \/ a2 <= sqrt8 \/ a3 <= sqrt8 \/ a4 <= sqrt8 \/ a5 <= sqrt8 \/ a6 <= sqrt8`, ARITH_TAC);; (* Node and edge split lemmas *) let split218_lemma = SPECL [`#2.18`; `yn_list (h:num->real^3) i`] REAL_LE_TOTAL;; let split236_lemma = SPECL [`yn_list (h:num->real^3) i`; `#2.36`] REAL_LE_TOTAL;; let split225_lemma = SPECL [`#2.25`; `ye_list (g:num#num->real^3#real^3) d`] REAL_LE_TOTAL;; (* lp_cond ==> good_list *)
let lp_cond_imp_good_list = 
prove(`lp_cond (L, g, h:num->real^3) (V,E) ==> good_list L`,
SIMP_TAC[lp_cond]);;
(* ESTD V = ESTD V *) let estd_refl = REFL estd_v;; (* ye_list g d <= &3 for a standard fan *) let ye_hi_3 = generate_ineq (gen_raw_ineq_data "tmp" true ye_hi_std);; (* ye_list g d <= #2.52 for a standard fan *) let ye_hi_2h0 = generate_ineq (gen_raw_ineq_data "tmp" true yy10_std);; (* ye_list g (a,b) = ye_list g (b,a) *) let ye_sym0 = (add_lp_hyp false o prove)(`(!d. g d = h (FST d), h (SND d)) ==> ye_list (g:num#num->real^3#real^3) (n,m) = ye_list g (m,n)`, DISCH_TAC THEN ASM_REWRITE_TAC Lp_ineqs_def.list_defs2 THEN REWRITE_TAC[Lp_ineqs_def.ye_fan; DIST_SYM]);; (* #2.52 <= ye_list g d for diagonals *) let diag4_lo = gen_list_ineq true dart4_y4'_lo and diag5_lo = (gen_list_ineq true o CONV_RULE NUM_REDUCE_CONV o SPEC `5` o add_lp_hyp false) y4'_lo_2h0 and diag6_lo = (gen_list_ineq true o CONV_RULE NUM_REDUCE_CONV o SPEC `6` o add_lp_hyp false) y4'_lo_2h0;; let diag5_lo_sym = PURE_ONCE_REWRITE_RULE[ye_sym0] diag5_lo and diag6_lo_sym = PURE_ONCE_REWRITE_RULE[ye_sym0] diag6_lo;; (* lp_tau for different cases *) let tau_split4, tau_split5_one, tau_split5_two, tau_split6 = let r = SPEC `d:num#num` o REWRITE_RULE[GSYM ALL_MEM] o gen_list_ineq true in r lp_tau_split4, r lp_tau_split5_one_diag, r lp_tau_split5_two_diags, r lp_tau_split6;; (*****************************************) (* Generates extra inequalities for a given inequality. *) (* For instance, |- a <= sqrt8 yields |- a <= &3 *) let gen_extra_ineqs = let tm_3 = `&3` and tm_sqrt8 = `sqrt8` and tm_218 = `#2.18` and tm_236 = `#2.36` in let r tm = prove(tm, MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC) in let l_ths_list = [ tm_3, r `&3 <= a ==> sqrt8 <= a`; tm_236, r `#2.36 <= a ==> #2.18 <= a`; ] in let r_ths_list = [ tm_sqrt8, r `a <= sqrt8 ==> a <= &3`; tm_218, r `a <= #2.18 ==> a <= #2.36`; ] in let a_var_real = `a:real` in fun ineq_th -> let lhs, rhs = dest_binary "real_le" (concl ineq_th) in let l_ths = map (fun th -> MP (INST[rhs, a_var_real] th) ineq_th) (assoc_all lhs l_ths_list) and r_ths = map (fun th -> MP (INST[lhs, a_var_real] th) ineq_th) (assoc_all rhs r_ths_list) in l_ths @ r_ths;; (* Generates ye-symmetric inequalities. *) (* Example: |- ye (a,b) <= c yields |- ye (b,a) <= c *) (* Accepts inequalities in the form: *) (* |- ye d <= c, |- c <= ye d, and |- ye d1 <= ye d2 *) (* This function does not return the original inequality *) let gen_ye_sym_ineqs ye_sym_th ineq_th = let sym_eqs tm = try let n_tm, m_tm = dest_ye_list tm in [REFL tm; INST[n_tm, n_var_num; m_tm, m_var_num] ye_sym_th] with Failure _ -> [REFL tm] in let ltm, rhs = dest_comb (concl ineq_th) in let op_tm, lhs = dest_comb ltm in let l_eqs = sym_eqs lhs and r_eqs = sym_eqs rhs in 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);; (* Generates all extra inequalities (including ye-symmetric inequalities) *) let gen_all_extra_cases ye_sym_th case_tms = let case_ths = map ASSUME case_tms in let extra = List.flatten (map gen_extra_ineqs case_ths) in let sym = gen_ye_sym_ineqs ye_sym_th in extra @ List.flatten (map sym (case_ths @ extra));; (* Computes lp_cond and lp_tau for a contravening packing *) let contravening_conditions hyp_list_tm hyp_set = let th0 = (MY_RULE_NUM o REWRITE_RULE[Seq.size]) Lp_ineqs_proofs.contravening_lp_cond_alt in let th1 = (UNDISCH_ALL o ISPEC hyp_list_tm o REWRITE_RULE[GSYM IMP_IMP]) th0 in let good_list_nodes_th = EQT_ELIM (eval_good_list_nodes_condition hyp_set) in let lp_cond_th = (MY_PROVE_HYP (hyp_set "good_list") o MY_PROVE_HYP good_list_nodes_th) th1 in let lp_cond_th' = (SELECT_AND_ABBREV_RULE o SELECT_AND_ABBREV_RULE o ABBREV_RULE "L" hyp_list_tm) lp_cond_th in let lp_tau_th = (UNDISCH_ALL o SPEC_ALL) Lp_main_estimate.contravening_lp_tau in lp_cond_th', lp_tau_th;; (*******************************) (* Verification test functions *) (*******************************) (* Returns all terminal cases and corresponding hypermap lists *) (* for a given hypermap list and lp_certificate_case *) let rec terminal_cases (hyp_list, case) = match case with | Lp_terminal terminal -> [(hyp_list, terminal)] | Lp_split (info, cs) -> (match info.split_type with (* Triangles, edges, nodes *) | "tri" | "edge" | "236" | "218" -> let case_args = zip [hyp_list; hyp_list] cs in flatten (map terminal_cases case_args) (* Special cases *) | "high" | "mid" | "add_big" -> let case_args = zip [hyp_list] cs in flatten (map terminal_cases case_args) (* Quad *) | "quad" -> let split_face = info.split_face in let dart13 = nth split_face 1, nth split_face 2 and dart24 = nth split_face 0, nth split_face 1 in let split13 = split_list hyp_list dart13 and split24 = split_list hyp_list dart24 in let case_args = zip [split13; split24; split13; split24; hyp_list] cs in flatten (map terminal_cases case_args) (* Pent *) | "pent" -> let split_face = info.split_face in let darts = rotateL 1 (list_pairs split_face) in let splits_one = map (split_list hyp_list) darts in let splits_two = map2 split_list splits_one (rotateL 2 darts) in let case_args = zip (hyp_list :: (splits_one @ splits_two)) cs in flatten (map terminal_cases case_args) (* Hex *) | "hex" -> let split_face = info.split_face in let darts = rotateL 1 (list_pairs split_face) in let splits = map (split_list hyp_list) darts in let case_args = zip (hyp_list :: splits) cs in flatten (map terminal_cases case_args) | s -> failwith ("cases: unknown split type: " ^ s));; (* Returns all terminal cases and corresponding hypermap lists for lp_certificate *) let get_terminal_cases certificate = let hyp_list = (snd o convert_to_list) certificate.hypermap_string in let hyp_list0_tm = (to_num o create_hol_list) hyp_list in let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None in let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0 in let ye_ineqs_3, ye_ineqs_2h0, diag4_ineqs = let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o 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 r ye_hi_3, r ye_hi_2h0, r diag4_lo in let diag4_ths = map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th) diag4_ineqs in let base_ineqs = ye_ineqs_3 @ ye_ineqs_2h0 @ diag4_ths in base_ineqs, terminal_cases (hyp_list, certificate.root_case);; (* Tests (verifies) a terminal case *) let test_terminal (hyp_list, terminal) = let hyp_list_tm = (to_num o create_hol_list) hyp_list in let hyp_set, hyp_fun = compute_all hyp_list_tm None in let r = (fun name, ind, v -> name, ind, map mk_real_int64 v) in let c = map r terminal.constraints and tv = map r terminal.target_variables and vb = map r terminal.variable_bounds in prove_flyspeck_lp_step1 hyp_list_tm hyp_set hyp_fun false terminal.precision terminal.infeasible c tv vb;; (*******************************) (* Main verification functions *) (*******************************) type lp_verification_arg = { (* Hypermap data *) hyp_data : ((string->thm) * (string->term->thm))list; ye_sym_th : thm; (* Theorems *) lp_cond_th : thm; lp_tau_th : thm; (* Terms *) hyp_list_tm : term; e_tm : term; };; (* Computes a splitted hypermap list (L2), a new E term (E2), lp_cond (L2,g,h) (V,E2) *) let split_lp_conditions hyp_list_tm lp_cond_th d_tm = let split_eq_th = eval_split_list_hyp hyp_list_tm d_tm in let split_tm = (rand o concl) split_eq_th in let lp_cond2_th = (PURE_REWRITE_RULE[split_eq_th] o SPEC d_tm o MATCH_MP lp_cond_trans1) lp_cond_th in let e2_tm = (rand o rand o concl) lp_cond2_th in (split_tm, e2_tm), lp_cond2_th;; (* Computes lp_tau (V,E2) *) let get_tau_split_th tau_trans_th (hyp_set, hyp_fun) arg d_tm = let set_name = (fst o dest_const o rator o rand o lhand o concl) tau_trans_th in let set_th = hyp_set set_name in let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair d_tm)) in 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 (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;; (* Eliminates extra assumptions and discharges case assumptions *) let get_final_case_th ye_sym_th cases_tm case_th = let case_tms = striplist dest_conj cases_tm in let case_th2 = itlist MY_PROVE_HYP (gen_all_extra_cases ye_sym_th case_tms) case_th in PURE_REWRITE_RULE[IMP_IMP; GSYM CONJ_ASSOC] (itlist DISCH case_tms case_th2);; (* Returns terms and inequalities for the triangle splitting case: *) (* split_th = |- #6.25 <= a + b + c \/ a + b + c <= #6.25 *) (* big_tm = `#6.25 <= a + b + c`, small_tm = `a + b + c <= #6.25 *) (* sym_big_ineqs = [|- #6.25 <= b + c + a; |- #6.25 <= c + a + b] *) (* sym_small_ineqs = [|- b + c + a <= #6.25; |- c + a + b <= #6.25; *) (* |- a <= #2.52; |- b <= #2.25; |- c <= #2.25; *) (* |- e(a) <= #2.52; |- e(b) <= #2.52; |- e(c) <= #2.52] *) (* Here, a = ye_list g (i1,i2), b = ye_list g (i2,i3), c = ye_list g (i3,i1) *) (* for split_face = [i1; i2; i3] *) let gen_triangle_ineqs = let ye_tm = `ye_list (g:num#num->real^3#real^3)` and c625 = `#6.25` in let sym_big = (SPEC c625 o ARITH_RULE) `!c. c <= x + y + z ==> c <= y + z + x /\ c <= z + x + y` and sym_small = (SPEC c625 o ARITH_RULE) `!c. x + y + z <= c ==> y + z + x <= c /\ z + x + y <= c` and split3_lemma = SPECL[c625; `x:real`] REAL_LE_TOTAL and 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 fun (hyp_set, hyp_fun) arg split_face -> let dart_tms = mk_all_darts split_face in let ye_tms = map (curry mk_comb ye_tm) dart_tms in let sum_tm = end_itlist (fun tm1 tm2 -> mk_comb (mk_comb (add_op_real, tm1), tm2)) ye_tms in let inst_list = zip ye_tms [x_var_real; y_var_real; z_var_real] in let big_tm = mk_comb (mk_comb (le_op_real, c625), sum_tm) and small_tm = mk_comb (mk_comb (le_op_real, sum_tm), c625) and split3_th = INST[sum_tm, x_var_real] split3_lemma in let sym_small_ineqs = (CONJUNCTS o MP (INST inst_list sym_small) o ASSUME) small_tm and sym_big_ineqs = (CONJUNCTS o MP (INST inst_list sym_big) o ASSUME) big_tm in let extra_small_ineqs = let set_th = hyp_set "list_of_darts3" in let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair (hd dart_tms))) in 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 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 map (CONV_RULE (convert_condition hyp_fun)) extra0 in let extra_sym = flatten (map (gen_ye_sym_ineqs arg.ye_sym_th) extra_small_ineqs) in split3_th, (big_tm, small_tm), (sym_big_ineqs, sym_small_ineqs @ extra_small_ineqs @ extra_sym);; (* Generate |- 6.25 <= a + b + c and symmetric inequalities when 2.25 <= a *) let gen_add_big_ineqs = let c625 = `#6.25` in let sym_big = (SPEC c625 o ARITH_RULE) `!c. c <= x + y + z ==> c <= y + z + x /\ c <= z + x + y` in 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 fun (hyp_set, hyp_fun) arg split_face -> let d_tm = mk_dart split_face 0 1 in let set_th = hyp_set "list_of_darts3" in let mem_th = EQT_ELIM (apply_op set_th (eval_mem_num_pair d_tm)) in let th0 = INST[arg.hyp_list_tm, l_cap_var; d_tm, d_var_pair; arg.e_tm, e_cap_var] big_extra in 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 let x_tm, yz_tms = dest_binary "real_add" (rand (concl big_th)) in let y_tm, z_tm = dest_binary "real_add" yz_tms in let inst_list = zip [x_tm; y_tm; z_tm] [x_var_real; y_var_real; z_var_real] in big_th :: CONJUNCTS (MP (INST inst_list sym_big) big_th);; (* Generates extra inequalities in the case when 2.18 <= yn(i) and 2.18 <= yn(j) for ~(i = j) *) let gen_mid_ineqs = let eq13 = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `13` in let lnsum13_mid_lemma = (REWRITE_RULE[GSYM IMP_IMP; eq13; Seq.size] o SPEC_ALL o add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum13_mid in fun (hyp_set, hyp_fun) arg split_face -> let i_tm = mk_raw_num (nth split_face 0) in let j_tm = mk_raw_num (nth split_face 1) in let th0 = (MY_PROVE_HYP arg.lp_cond_th o 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 let els_eq_th = hyp_set "list_of_elements" in let els_tm = rand (concl els_eq_th) in let indices = let list = dest_list els_tm in let i_ind = index i_tm list and j_ind = index j_tm list in subtract (0--(length list - 1)) [i_ind; j_ind] in let th1 = EQ_MP (term_rewrite (concl th0) els_eq_th) th0 in let th2 = (prove_conditions o simplify_ineq hyp_fun) th1 in let mem_i = EQT_ELIM (eval_mem_univ raw_eq_hash_conv i_tm els_tm) and mem_j = EQT_ELIM (eval_mem_univ raw_eq_hash_conv j_tm els_tm) in let ths = CONJUNCTS (MY_PROVE_HYP mem_i (MY_PROVE_HYP mem_j th2)) in let lo_th = nth ths 0 and hi_th1 = nth ths 1 and hi_th2 = nth ths 2 in let lo_ineqs1 = select_all lo_th indices in let lo_ineqs2 = map (prove_conditions o MY_BETA_RULE) lo_ineqs1 in let ineqs = hi_th1 :: hi_th2 :: lo_ineqs2 in ineqs @ flatten (map gen_extra_ineqs ineqs);; (* Generates extra inequalities in the case when 2.36 <= yn(i) *) let gen_high_ineqs = let eq13 = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `13` in let lnsum13_high_lemma = (REWRITE_RULE[GSYM IMP_IMP; eq13; Seq.size] o SPEC_ALL o add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum13_high in fun (hyp_set, hyp_fun) arg split_face -> let i_tm = mk_raw_num (nth split_face 0) in let th0 = (MY_PROVE_HYP arg.lp_cond_th o INST[arg.e_tm, e_cap_var; arg.hyp_list_tm, l_cap_var; i_tm, i_var_num]) lnsum13_high_lemma in let els_eq_th = hyp_set "list_of_elements" in let els_tm = rand (concl els_eq_th) in let indices = let list = dest_list els_tm in let i_ind = index i_tm list in subtract (0--(length list - 1)) [i_ind] in let th1 = EQ_MP (term_rewrite (concl th0) els_eq_th) th0 in let th2 = (prove_conditions o simplify_ineq hyp_fun) th1 in let mem_i = EQT_ELIM (eval_mem_univ raw_eq_hash_conv i_tm els_tm) in let lo_th = MY_PROVE_HYP mem_i th2 in let lo_ineqs1 = select_all lo_th indices in let ineqs = map (prove_conditions o MY_BETA_RULE) lo_ineqs1 in ineqs @ flatten (map gen_extra_ineqs ineqs);; let set_report, reset_progress, next_terminal, report_progress = let t = ref 0 in let flag = ref true in (fun b -> flag := b), (fun () -> t := 0), (fun () -> t := !t + 1), (fun () -> if !flag then (Format.print_string (sprintf "%d " !t); Format.print_flush()) else ());; let compute_hypermap arg = if arg.hyp_data = [] then let good_th = MATCH_MP lp_cond_imp_good_list arg.lp_cond_th in let hyp_data = compute_all arg.hyp_list_tm (Some good_th) in {arg with hyp_data = [hyp_data]}, hyp_data else arg, hd arg.hyp_data;; (* Verifies an lp_certificate_case *) let rec verify_lp_case base_ineqs std_flag (arg, case) = match case with (* Terminal case *) | Lp_terminal terminal -> let _ = next_terminal() in let hyp_set, hyp_fun = snd (compute_hypermap arg) in let r = (fun name, ind, v -> name, ind, map mk_real_int64 v) in let c = map r terminal.constraints and tv = map r terminal.target_variables and vb = map r terminal.variable_bounds in
let th0 = prove_flyspeck_lp_step1 arg.hyp_list_tm hyp_set hyp_fun std_flag terminal.precision terminal.infeasible c tv vb in
	let _ = report_progress() in
	let th1 = (MY_PROVE_HYP arg.lp_tau_th o INST[arg.e_tm, e_cap_var]) th0 in
	let th2 = if std_flag then MY_PROVE_HYP estd_refl th1 else itlist MY_PROVE_HYP base_ineqs th1 in
	  (MY_PROVE_HYP arg.lp_cond_th) th2
    | Lp_split (info, cs) ->
	(match info.split_type with
	   | "tri" ->
	       verify_split3 base_ineqs std_flag arg info cs
	   | "quad" ->
	       verify_split4 base_ineqs std_flag arg info cs
	   | "pent" ->
	       verify_split5 base_ineqs std_flag arg info cs
	   | "hex" ->
	       verify_split6 base_ineqs std_flag arg info cs
	   | "edge" ->
	       verify_edge base_ineqs std_flag arg info cs
	   | "218" ->
	       verify_218 base_ineqs std_flag arg info cs
	   | "236" ->
	       verify_236 base_ineqs std_flag arg info cs
	   | "mid" ->
	       verify_mid base_ineqs std_flag arg info cs
	   | "high" ->
	       verify_high base_ineqs std_flag arg info cs
	   | "add_big" ->
	       verify_add_big base_ineqs std_flag arg info cs
	   | s -> failwith ("verify_lp_case: unknown case " ^ s))

(* Adds a new big triangle if one of its edges is >= #2.25 *)
and verify_add_big base_ineqs std_flag arg info cs =
  let arg, hyp_data = compute_hypermap arg in
  let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
  let ineqs = gen_add_big_ineqs hyp_data arg info.split_face in
    itlist MY_PROVE_HYP ineqs case
    
(* Adds additional node inequalities *)
and verify_mid base_ineqs std_flag arg info cs =
  let arg, hyp_data = compute_hypermap arg in
  let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
  let ineqs = gen_mid_ineqs hyp_data arg info.split_face in
    itlist MY_PROVE_HYP ineqs case

(* Adds additional node inequalities *)
and verify_high base_ineqs std_flag arg info cs =
  let arg, hyp_data = compute_hypermap arg in
  let case = verify_lp_case base_ineqs std_flag (arg, hd cs) in
  let ineqs = gen_high_ineqs hyp_data arg info.split_face in
    itlist MY_PROVE_HYP ineqs case

(* Nodes: 2.18 <= yn(i) \/ yn(i) <= 2.18 *)
and verify_218 base_ineqs std_flag arg info cs =
  let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
  let split_th = INST[mk_raw_num (hd info.split_face), i_var_num] split218_lemma in
  let split_cases = striplist dest_disj (concl split_th) in
  let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
  let final_th = MP (end_itlist combine_cases final_cases) split_th in
    final_th

(* Nodes: yn(i) <= 2.36 \/ 2.36 <= yn(i) *)
and verify_236 base_ineqs std_flag arg info cs =
  let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
  let split_th = INST[mk_raw_num (hd info.split_face), i_var_num] split236_lemma in
  let split_cases = striplist dest_disj (concl split_th) in
  let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
  let final_th = MP (end_itlist combine_cases final_cases) split_th in
    final_th

(* Edges: 2.25 <= ye(d) \/ ye(d) <= 2.25 *)
and verify_edge base_ineqs std_flag arg info cs =
  let cases = map (curry (verify_lp_case base_ineqs std_flag) arg) cs in
  let split_th = INST[mk_dart info.split_face 0 1, d_var_pair] split225_lemma in
  let split_cases = striplist dest_disj (concl split_th) in
  let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
  let final_th = MP (end_itlist combine_cases final_cases) split_th in
    final_th

(* Triangle *)
and verify_split3 base_ineqs std_flag arg info cs =
  let arg, hyp_data = compute_hypermap arg in
    (* Prove all subcases *)
  let case1_th = verify_lp_case base_ineqs std_flag (arg, nth cs 0) and
      case2_th = verify_lp_case base_ineqs std_flag (arg, nth cs 1) in
    (* Combine subcases *)
  let split_th, (case1_tm, case2_tm), (case1_ineqs, case2_ineqs) = gen_triangle_ineqs hyp_data arg info.split_face in
  let th1 = DISCH case1_tm (itlist MY_PROVE_HYP case1_ineqs case1_th) and
      th2 = DISCH case2_tm (itlist MY_PROVE_HYP case2_ineqs case2_th) in
  let final_th = MP (combine_cases th1 th2) split_th in
    final_th

(* Quad *)
and verify_split4 base_ineqs std_flag arg info cs =
  let d13_tm = mk_dart info.split_face 1 2 and
      d24_tm = mk_dart info.split_face 0 1 and
      diag1_tm = mk_dart info.split_face 0 2 and
      diag2_tm = mk_dart info.split_face 1 3 in
    (* compute lp_cond *)
  let (split13_tm, e13), lp_cond13 = split_lp_conditions arg.hyp_list_tm arg.lp_cond_th d13_tm and
      (split24_tm, e24), lp_cond24 = split_lp_conditions arg.hyp_list_tm arg.lp_cond_th d24_tm in
    (* compute lp_tau *)
  let arg, hyp_data = compute_hypermap arg in
  let tau13 = get_tau_split_th tau_split4 hyp_data arg d13_tm and
      tau24 = get_tau_split_th tau_split4 hyp_data arg d24_tm in
    (* Prove all subcases *)
  let arg13 = {arg with hyp_data = []; lp_cond_th = lp_cond13; lp_tau_th = tau13; hyp_list_tm = split13_tm; e_tm = e13} and
      arg24 = {arg with hyp_data = []; lp_cond_th = lp_cond24; lp_tau_th = tau24; hyp_list_tm = split24_tm; e_tm = e24} in
  let args = zip [arg13; arg24; arg13; arg24; arg] cs in
  let cases = map2 (verify_lp_case base_ineqs) [false; false; false; false; std_flag] args in
    (* Combine subcases *)
  let split_th = INST[diag1_tm, nth diag_vars 1; diag2_tm, nth diag_vars 2] split4_lemma in
  let split_cases = striplist dest_disj (concl split_th) in
  let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
  let final_th = MP (end_itlist combine_cases final_cases) split_th in
    final_th

(* Pent *)
and verify_split5 base_ineqs std_flag arg info cs =
  let dart_tms = rotateL 1 (mk_all_darts info.split_face) in
  let lp_conds_one = map (split_lp_conditions arg.hyp_list_tm arg.lp_cond_th) dart_tms in
  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
    (* compute lp_tau_th *)
  let arg, (hyp_set, hyp_fun) = compute_hypermap arg in
  let tau_ths_one = map (get_tau_split_th tau_split5_one (hyp_set, hyp_fun) arg) dart_tms in
  let tau_ths_two =
    let ths = map (get_tau_split_th tau_split5_two (hyp_set, hyp_fun) arg) dart_tms in
      map ((CONV_RULE o RAND_CONV o RAND_CONV o RAND_CONV o RAND_CONV) (convert_tm hyp_fun)) ths in
    (* Prove all subcases *)
  let args = arg :: map2 (fun ((split_tm, e_tm), lp_cond_th) tau_th ->
			    {arg with hyp_data = []; lp_cond_th = lp_cond_th; lp_tau_th = tau_th; 
			       hyp_list_tm = split_tm; e_tm = e_tm})
    (lp_conds_one @ lp_conds_two) (tau_ths_one @ tau_ths_two) in
  let std_flags = std_flag :: replicate false 10 in
  let cases = map2 (verify_lp_case base_ineqs) std_flags (zip args cs) in
    (* Combine subcases *)
  let split_face_tms = map mk_raw_num info.split_face in
  let diag_tms = map mk_pair (zip split_face_tms (rotateL 2 split_face_tms)) in
  let split_th = INST (zip diag_tms (take 5 (drop 1 diag_vars))) split5_lemma in
  let split_cases = striplist dest_disj (concl split_th) in
  let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
  let final_th = MP (end_itlist combine_cases final_cases) split_th in
    final_th

(* Hex *)
and verify_split6 base_ineqs std_flag arg info cs =
  let _ = report "Warning: hex splitting case" in
  let dart_tms = rotateL 1 (mk_all_darts info.split_face) in
  let lp_conds = map (split_lp_conditions arg.hyp_list_tm arg.lp_cond_th) dart_tms in
    (* compute lp_tau_th *)
  let arg, hyp_data = compute_hypermap arg in
  let lp_tau_ths = map (get_tau_split_th tau_split6 hyp_data arg) dart_tms in
    (* Prove all subcases *)
  let args = arg :: map2 (fun ((split_tm, e_tm), lp_cond_th) tau_th ->
			    {arg with hyp_data = []; lp_cond_th = lp_cond_th; lp_tau_th = tau_th; 
			       hyp_list_tm = split_tm; e_tm = e_tm}) lp_conds lp_tau_ths in
  let std_flags = std_flag :: replicate false 6 in
  let cases = map2 (verify_lp_case base_ineqs) std_flags (zip args cs) in
    (* Combine subcases *)
  let split_face_tms = map mk_raw_num info.split_face in
  let diag_tms = map mk_pair (zip split_face_tms (rotateL 2 split_face_tms)) in
  let split_th = INST (zip diag_tms (take 6 (drop 1 diag_vars))) split6_lemma in
  let split_cases = striplist dest_disj (concl split_th) in
  let final_cases = map2 (get_final_case_th arg.ye_sym_th) split_cases cases in
  let final_th = MP (end_itlist combine_cases final_cases) split_th in
    final_th;;
(* Verifies an lp_certificate *) let verify_lp_certificate certificate = let n = count_terminals certificate.root_case in let hyp_list = (snd o convert_to_list) certificate.hypermap_string in let hyp_list0_tm = (to_num o create_hol_list) hyp_list in let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None in let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0 in let ye_sym_th = (MY_PROVE_HYP lp_cond0 o INST[estd_v, e_cap_var]) ye_sym0 in let base_ineqs = if n == 1 then [] else let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o 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 let r2 = (map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th)) o r in (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 let arg = {hyp_data = [hyp_set0, hyp_fun0]; ye_sym_th = ye_sym_th; lp_cond_th = EXPAND_CONCL_RULE "L" lp_cond0; lp_tau_th = lp_tau0; hyp_list_tm = hyp_list0_tm; e_tm = estd_v} in let _ = reset_progress(); Format.print_string (sprintf "terminals = %d: " n); Format.print_flush() in let final_th = verify_lp_case base_ineqs true (arg, certificate.root_case) in let _ = Format.print_newline() in (DISCH contravening_v o EXPAND_RULE "L" o EXPAND_RULE "g" o EXPAND_RULE "h") final_th;; end;;