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;;