needs "../formal_lp/hypermap/main/prove_flyspeck_lp.hl";;

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_ineqs_proofs;;
open Lp_main_estimate;;
open Flyspeck_lp;;


let split4_lemma = 
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);;

let split4_lemma' = INST[`ye_list (g:num#num->real^3#real^3) d1`, `a:real`;
			 `ye_list (g:num#num->real^3#real^3) d2`, `b:real`] split4_lemma;;

let d1_var = `d1:num#num` and
    d2_var = `d2:num#num`;;


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


let gen_extra_ineqs =
  let tm_3 = `&3` and
      tm_sqrt8 = `sqrt8` 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`;
  ] in
  let r_ths_list = [
    tm_sqrt8, r `a <= sqrt8 ==> a <= &3`;
  ] 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;;


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

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


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

let e_cap_var = `E:(real^3->bool)->bool`;;
let lp_cond_imp_good_list = 
prove(`lp_cond (L, g, h:num->real^3) (V,E) ==> good_list L`,
 SIMP_TAC[lp_cond]);;
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]);;

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

let tau_split4 = gen_list_ineq false lp_tau_split4;;
let diag4_lo = gen_list_ineq true dart4_y4'_lo;;



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


let contravening_conditions hyp_list_tm hyp_set =
  let th0 = (MY_RULE_NUM o REWRITE_RULE[Seq.size]) 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) contravening_lp_tau in
    lp_cond_th', lp_tau_th;;


let split_conditions hyp_list_tm d_tm lp_cond0_th =
  let split_eq_th = (ABBREV_RULE "L" hyp_list_tm) (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_cond0_th in
  let e2_tm = (rand o rand o concl) lp_cond2_th in
  let lp_cond2_th' = (ABBREV_RULE "L2" split_tm) lp_cond2_th in
(*
let good2_th = MATCH_MP lp_cond_imp_good_list lp_cond2_th;;
let hyp2_set, hyp2_fun = compute_all split_tm (Some good2_th);;
*)
  let hyp2_set, hyp2_fun = compute_all split_tm None in
    lp_cond2_th', split_eq_th, split_tm, e2_tm, (hyp2_set, hyp2_fun);;


(******************************)
(* Load data *)
loadt "../formal_lp/glpk/ex2/bb2_1_out.hl";;
let p1, c1, t1, v1 = precision, constraints, target_variables, variable_bounds;;

loadt "../formal_lp/glpk/ex2/bb2_2_out.hl";;
let p2, c2, t2, v2 = precision, constraints, target_variables, variable_bounds;;

loadt "../formal_lp/glpk/ex2/bb2_3_out.hl";;
let p3, c3, t3, v3 = precision, constraints, target_variables, variable_bounds;;

loadt "../formal_lp/glpk/ex2/bb2_4_out.hl";;
let p4, c4, t4, v4 = precision, constraints, target_variables, variable_bounds;;

loadt "../formal_lp/glpk/ex2/bb2_5_out.hl";;
let p5, c5, t5, v5 = precision, constraints, target_variables, variable_bounds;;


(******************************)
(* Compute preliminary data *)
let hyp_list0_tm = (to_num o create_hol_list_str) hypermap_string;;
let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None;;

let d13 = to_num `1,2` and
    d24 = to_num `0,1`;;

let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0;;
let ye_sym_th = (MY_PROVE_HYP lp_cond0 o INST[`ESTD V`, e_cap_var]) ye_sym0;;

let ye_hi_3 = generate_ineq (find_raw_ineq true "ye_hi");;
let ye_hi_2h0 = generate_ineq (find_raw_ineq true "yy10");;

let ye_ineqs_3, ye_ineqs_2h0, diag4_ineqs, tau_ths =
  let estd_refl = REFL `ESTD V` in
  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, r tau_split4;;


let diag4_ths = map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th) diag4_ineqs;;
let tau_ths2 = map (UNDISCH_ALL o simplify_ineq hyp_fun0) ((fst o chop_list 2) tau_ths);;
let tau_split13 = List.nth tau_ths2 1;;
let tau_split24 = List.nth tau_ths2 0;;

let base_ineqs = ye_ineqs_3 @ ye_ineqs_2h0 @ diag4_ths;;


(******************************)
(* case 1 *)
let lp_cond1, split1_eq, hyp_list1_tm, e1_tm, (hyp1_set, hyp1_fun) = split_conditions hyp_list0_tm d13 lp_cond0;;

let lp1_th0 = prove_flyspeck_lp_step1 hyp_list1_tm hyp1_set hyp1_fun false p1 c1 t1 v1;;
let lp1_th1 = (MY_PROVE_HYP tau_split13 o INST[e1_tm, e_cap_var]) lp1_th0;;
let lp1_th2 = itlist MY_PROVE_HYP base_ineqs lp1_th1;;

let case1_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond1 o INST[e1_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list1_tm) lp1_th2;;


(******************************)
(* case 2 *)
let lp_cond2, split2_eq, hyp_list2_tm, e2_tm, (hyp2_set, hyp2_fun) = split_conditions hyp_list0_tm d24 lp_cond0;;

let lp2_th0 = prove_flyspeck_lp_step1 hyp_list2_tm hyp2_set hyp2_fun false p2 c2 t2 v2;;
let lp2_th1 = (MY_PROVE_HYP tau_split24 o INST[e2_tm, e_cap_var]) lp2_th0;;
let lp2_th2 = itlist MY_PROVE_HYP base_ineqs lp2_th1;;

let case2_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond2 o INST[e2_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list2_tm) lp2_th2;;


(******************************)
(* case 3 *)
let lp_cond3, split3_eq, hyp_list3_tm, e3_tm, (hyp3_set, hyp3_fun) = split_conditions hyp_list0_tm d13 lp_cond0;;

let lp3_th0 = prove_flyspeck_lp_step1 hyp_list3_tm hyp3_set hyp3_fun false p3 c3 t3 v3;;
let lp3_th1 = (MY_PROVE_HYP tau_split13 o INST[e3_tm, e_cap_var]) lp3_th0;;
let lp3_th2 = itlist MY_PROVE_HYP base_ineqs lp3_th1;;

let case3_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond3 o INST[e2_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list3_tm) lp3_th2;;


(******************************)
(* case 4 *)
let lp_cond4, split4_eq, hyp_list4_tm, e4_tm, (hyp4_set, hyp4_fun) = split_conditions hyp_list0_tm d24 lp_cond0;;

let lp4_th0 = prove_flyspeck_lp_step1 hyp_list4_tm hyp4_set hyp4_fun false p4 c4 t4 v4;;
let lp4_th1 = (MY_PROVE_HYP tau_split24 o INST[e2_tm, e_cap_var]) lp4_th0;;
let lp4_th2 = itlist MY_PROVE_HYP base_ineqs lp4_th1;;

let case4_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond4 o INST[e4_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list4_tm) lp4_th2;;


(******************************)
(* case 5 *)
let lp5_th0 = prove_flyspeck_lp_step1 hyp_list0_tm hyp_set0 hyp_fun0 true p5 c5 t5 v5;;
let lp5_th1 = (MY_PROVE_HYP (REFL `ESTD V`) o INST [`ESTD V`, e_cap_var]) lp5_th0;;
let lp5_th2 = (MY_PROVE_HYP lp_tau0 o MY_PROVE_HYP lp_cond0 o ABBREV_RULE "L" hyp_list0_tm) lp5_th1;;

let case5_th = lp5_th2;;


(******************************)
(* combine all cases *)

let diag2 = to_num `1,3`;;
let diag1 = to_num `0,2`;;

let split_th = INST[diag1, d1_var; diag2, d2_var] split4_lemma';;
let split_cases = striplist dest_disj (concl split_th);;

let case1_tms = striplist dest_conj (List.nth split_cases 0);;
map concl (gen_all_extra_cases ye_sym_th case1_tms);;
let case1_th2 = itlist MY_PROVE_HYP (gen_all_extra_cases ye_sym_th case1_tms) case1_th;;
let case1_th_final = PURE_ONCE_REWRITE_RULE[IMP_IMP] (itlist DISCH case1_tms case1_th2);;

let get_final_case_th ye_sym_th n case_th cases =
  let case_tms = striplist dest_conj (List.nth cases n) 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);;

let case1_th_final = get_final_case_th ye_sym_th 0 case1_th split_cases;;
let case2_th_final = get_final_case_th ye_sym_th 1 case2_th split_cases;;
let case3_th_final = get_final_case_th ye_sym_th 2 case3_th split_cases;;
let case4_th_final = get_final_case_th ye_sym_th 3 case4_th split_cases;;
let case5_th_final = get_final_case_th ye_sym_th 4 case5_th split_cases;;

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 final' = itlist combine_cases [case1_th_final; case2_th_final; case3_th_final; case4_th_final] case5_th_final;;
let final = (DISCH `contravening V` o EXPAND_RULE "g" o EXPAND_RULE "h" o EXPAND_RULE "L") (MP final' split_th);;