HOL html


#print_length 50;;

flyspeck_needs "../glpk/minorlp/tame_table.ml";;
let process_exec = Preprocess.exec();;
flyspeck_needs "nonlinear/prep.hl";;

flyspeck_needs "computational_build.hl";;
Preprocess.prep_file;;




Tame_table.execute();;

flyspeck_needs "usr/thales/hales_tactic.hl";;
flyspeck_needs "general/debug.hl";;
flyspeck_needs "volume/vol1.hl";;
flyspeck_needs "hypermap/bauer_nipkow.hl";;
needs "Multivariate/convex.ml";;
rflyspeck_needs "local/polar_fan.hl";;
rflyspeck_needs "local/lp_details.hl";;
flyspeck_needs "local/polar.hl";;
flyspeck_needs "local/localization.hl";;
flyspeck_needs "local/local_lemmas1.hl";;
flyspeck_needs "packing/YSSKQOY.hl";;
flyspeck_needs "packing/counting_spheres.hl";;
rflyspeck_needs "jordan/refinement.hl";;
rflyspeck_needs "jordan/parse_ext_override_interface.hl";;
rflyspeck_needs "jordan/real_ext.hl";;
rflyspeck_needs "jordan/taylor_atn.hl";;
rflyspeck_needs "jordan/parse_ext_override_interface.hl";;
flyspeck_needs "general/print_types.hl";;

flyspeck_needs "local/RRCWNSJ.hl";;
flyspeck_needs "local/JCYFMRP.hl";;
flyspeck_needs "local/TFITSKC.hl";;
flyspeck_needs "local/CQAOQLR.hl";;
flyspeck_needs "local/JLXFDMJ.hl";;
flyspeck_needs "leg/geomdetail.hl";;
flyspeck_needs "local/local_lemmas1.hl";;


flyspeck_needs "local/ARDBZYE.hl";;
flyspeck_needs "local/AUEAHEH.hl";;
flyspeck_needs "local/VASYYAU.hl";;
flyspeck_needs "local/MIQMCSN.hl";;
flyspeck_needs "local/JEJTVGB.hl";;

flyspeck_needs "local/yxionxl.hl";;
flyspeck_needs "local/ODXLSTCv2.hl";;
flyspeck_needs "local/ZLZTHIC.hl";;
flyspeck_needs "local/lunar_deform.hl";;
Lunar_deform.MHAEYJN;;
flyspeck_needs "local/NUXCOEA.hl";;
flyspeck_needs "packing/Oxl_def.hl";;
flyspeck_needs "packing/Oxl_2012.hl";;


let fn = flyspeck_needs;;
fn "local/appendix_main_estimate.hl";;
fn       "local/ODXLSTCv2.hl";;
fn       "local/IMJXPHR.hl";;
fn       "local/NUXCOEA.hl";;
fn       "local/FEKTYIY.hl";;
fn       "local/AURSIPD.hl";;
fn       "local/PPBTYDQ.hl";;
fn       "local/AXJRPNC.hl";;
fn "local/YRTAFYH.hl";;
fn       "local/WKEIDFT.hl";;
fn        "local/hexagons.hl";;
       fn "local/OTMTOTJ.hl";;
       fn "local/HIJQAHA.hl";;
       fn "local/CNICGSF.hl";;
fn "local/BKOSSGE.hl";;
fn "local/IUNBUIG.hl";;
flyspeck_needs "local/JOTSWIX.hl";;

flyspeck_needs "local/IUNBUIG.hl";;


flyspeck_needs "local/";;
Yxionxl2
flyspeck_needs "general/flyspeck_lib.hl";;
flyspeck_needs "local/Xivphks.hl";;
flyspeck_needs   "local/EYYPQDW.hl";; (* 2013-07-08 *)
flyspeck_needs   "local/IMJXPHR.hl";; 
Imjxphr.ZLZTHICv1_concl;; 
Appendix.ZLZTHIC_concl;;
Imjxphr.IMJXPHR;;
State_manager.neutralize_state();;
rflyspeck_needs "nonlinear/lemma.hl";;
rflyspeck_needs "nonlinear/functional_equation.hl";;
Ineq.ineqs:= [];;
rflyspeck_needs "nonlinear/ineq.hl";;
rflyspeck_needs   "nonlinear/main_estimate_ineq.hl";;
rflyspeck_needs  "nonlinear/parse_ineq.hl";;
rflyspeck_needs "nonlinear/optimize.hl";;
rflyspeck_needs "general/flyspeck_lib.hl";;
rflyspeck_needs   "nonlinear/function_list.hl";;
rflyspeck_needs "nonlinear/auto_lib.hl";;
rflyspeck_needs "nonlinear/scripts.hl";;
Scripts.execute_interval_all false;;
Scripts.execute_cfsqp();;
let cfsqp_out = it;;
cfsqp_out;;
Scripts.one_cfsqp  "QZECFIC wt0";;
Scripts.cfsqp ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";"QZECFIC wt1";"QZECFIC wt2 A"];;
Scripts.cfsqp ["IXPOTPA"; "GRKIBMP B V2"; "7796879304"; "8346775862"];;
;;

List.length !Ineq.ineqs;;

let idvs = Flyspeck_lib.nub (sort (<) (map (fun t -> t.idv) (!Ineq.ineqs)));;
List.length idvs;;

flyspeck_needs "nonlinear/calc_derivative.hl";;
flyspeck_needs "nonlinear/merge_ineq.hl";;
rflyspeck_needs "nonlinear/scripts.hl";;
(* Scripts.execute_interval_all true;; (* takes several hours *) *)
Scripts.unfinished_cases();;
let reruns = ["6843920790"; (* "9563139965D" ; *) "6944699408 a reduced"; "6944699408 a";
   "7043724150 a reduced v2"; "7043724150 a"; "8055810915"; "1965189142 34";
   "TSKAJXY-eulerA"];;
map (Auto_lib.testsplit true) ["8055810915"];;


Scripts.times;;
Scripts.hour (Scripts.total Scripts.times);;
Scripts.case_splits_execute;;

let redo (s,cs,t) = 
  let rg = 0--(t-1) in
  let cs' = subtract rg cs in
    map (fun c -> (s,c,t)) cs';;

let redos = List.flatten (map redo incompletes);;


(!Prep.prep_ineqs);;


map (test_prep_case_split true) redos;;

  
test_prep_case true 1 2 "GRKIBMP A V2";;

Auto_lib.testsplit true "GRKIBMP A V2";;

let some_cases = filter (fun (_,t) -> t > 300) Scripts.times;;
let some_cases = filter (fun (_,t) -> t > 120) times;;
total some_cases;;
assoc "3862621143 revised" times;;
assoc "7043724150 a" times;;
assoc "9507202313" times;;

Scripts.hour (Scripts.total some_cases);;
List.length some_cases;;
783.0 /. 60.0;;

flyspeck_needs "general/flyspeck_lib.hl";;
flyspeck_needs "../glpk/glpk_link.ml";;
flyspeck_needs "../glpk/minorlp/OXLZLEZ.ml";;
     "local/UAGHHBM.hl";;
flyspeck_needs "packing/oxl_def.hl";;
flyspeck_needs "packing/oxl_2012.hl";;
flyspeck_needs "packing/OXLZLEZ.hl";;
Oxlzlez.PACKING_CHAPTER_MAIN_CONCLUSION;;

Mk_all_ineq.example2;;
Mk_all_ineq.exec();;
rflyspeck_needs "../projects_discrete_geom/bezdek_reid/bezdek_reid.hl";;
let filter_edge_bak = Bezdek_reid.filter_edge;;

1;;
Bezdek_reid.test_edge;;
Bezdek_reid.test_triplet;;
zip;;
flyspeck_needs "../glpk/glpk_link.ml";;
rflyspeck_needs "../projects_discrete_geom/fejestoth12/lipstick_ft.ml";;
List.length Bezdek_reid.filter_triplet;;
List.length (filter (fun (a,_,_) -> (a =[])) Bezdek_reid.coord_triplet);;
let test = ref "";;

flyspeck_needs "nonlinear/check_completeness.hl";;
  let check_completeness_out = Check_completeness.execute();;

rflyspeck_needs   "nonlinear/types.hl";;
rflyspeck_needs   "nonlinear/nonlin_def.hl";;
rflyspeck_needs   "nonlinear/ineq.hl";;
rflyspeck_needs   "nonlinear/mdtau.hl";;
rflyspeck_needs   "nonlinear/main_estimate_ineq.hl";;
rflyspeck_needs   "nonlinear/lemma.hl";;  (* needs trig1, trig2 *)
rflyspeck_needs   "nonlinear/functional_equation.hl";;
rflyspeck_needs   "nonlinear/parse_ineq.hl";;
rflyspeck_needs   "nonlinear/optimize.hl";;
rflyspeck_needs   "nonlinear/function_list.hl";;
rflyspeck_needs   "nonlinear/auto_lib.hl";;
rflyspeck_needs "nonlinear/scripts.hl";;
flyspeck_needs "local/XBJRPHC.hl";;


(* Formal LP verification *)
needs "../formal_lp/hypermap/verify_all.hl";;
let result = Verify_all.verify_all();;
Verify_all.test_result result;;
List.length result;;
List.length (List.flatten (map fst result));;
List.nth result 77;;
(73386.0 /. 3600.0);;


(*

Issues:

The zip file unpacked to glpk/binary/lp_certificates/.
I had to move the files to glpk/binary/

The directory glpk/binary/ has hiddedn files .DS_Store and .svn
Verify_all.verify_all() tried:
Verifying /Users/thomashales/Desktop/googlecode/flyspeck/text_formalization/../formal_lp/glpk/binary/.DS_Store
and threw an exception.

*)


  open Pent_hex;;
  open Optimize;;
flyspeck_needs "../development/thales/session/local_defs.hl";;
flyspeck_needs "../development/thales/session/interval_args.hl";;
flyspeck_needs "../development/thales/session/2app.hl";;

(* Local materials *)
Ineq.ineqs:= [];;
rflyspeck_needs "nonlinear/ineq.hl";;
rflyspeck_needs   "nonlinear/main_estimate_ineq.hl";;
List.length !Ineq.ineqs;;
flyspeck_needs "local/appendix_main_estimate.hl";;


   rflyspeck_needs "local/appendix_main_estimate.hl";; 
   flyspeck_needs "local/terminal.hl";;

flyspeck_needs "local/lunar_deform.hl";;

flyspeck_needs "local/terminal.hl";;
flyspeck_needs "local/pent_hex.hl";;
flyspeck_needs "local/OCBICBY.hl";;
flyspeck_needs "local/YXIONXL2.hl";;
flyspeck_needs "local/XIVPHKS.hl";;
flyspeck_needs "local/ZLZTHIC.hl";;
flyspeck_needs "local/PQCSXWG.hl";;
flyspeck_needs "local/CUXVZOZ.hl";;
  open Cuxvzoz;;

flyspeck_needs "../development/thales/session/work_in_progress.hl";;

  open Work_in_progress;;


let strip_id s =
  let ss = Str.split (Str.regexp "[],[]") s in
    (hd ss,map int_of_string (tl ss));;

strip_id "abc[0,1,2,3]";;

0.0659/. 0.042;;


module Temp =  struct
  open Sphere;;
  open Ineq;;
add
{
  idv="2485876245b";
  doc="Used in some quad calculations to show that a node
   is not straight (both halves are acute)";
  tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,#2.52);
    (#3.01,y5, &2 * #2.52);
      (&2,y6,#3.01)
  ]
((delta4_y y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
};;
end;;

let ztg4s = map (fun t -> t.idv) (Ineq.getprefix "ZTGIJCF4");;
cfsqp ztg4s;;

module Test = struct
  open Ineq;;
  open Sphere;;
add
{
  idv = "test QITNPEA 3848804089";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (#2 ,y4, &2 * hminus);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
    ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.164017 + #0.119482* dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/  (eta_y y1 y2 y6 pow 2 < #1.34 pow 2 )) `;
  doc =   "
     This is an inequality for quarters used to prove the cluster inequality.";
  tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "MMGKNVE";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (&2,y4, &2 * hminus);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
    ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0539 
      - #0.042*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
    (eta_y y1 y2 y6 pow 2 < #1.34 pow 2 ))`;
  doc =   "
     This is an inequality for quarters used to prove the cluster inequality.";
  tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ"];Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "test BIXPCGW 9455898160";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, #2.6);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (&2,y4, &2 * hminus);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
   (
    gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) `;
  doc =   "
     If $X$ is a quarter, then $\\gamma(X,L)\\ge -0.00569$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "test ratio2";
  ineq = all_forall `ineq
   [(&2 * hminus, y4, &2 * hplus);
    (&2  ,y5, sqrt8);
    (&2 ,y6, sqrt8)
   ]
   ( truncate_gamma3f_x (#0.001) (h0cut y4) (h0cut y5) (h0cut y6) (&2) (&2) (&2) (y4*y4) (y5*y5) (y6*y6) /
       (&1* dih_y y4 y5 sqrt2 sqrt2 sqrt2 y6) > &0 \/
       eta_y y4 y5 y6 > sqrt2 - #0.001 
     \/
     eta_y y4 y5 y6 < #1.34 
   )`;
  doc =   "test";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "test gamma23";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (&2,y4, sqrt8);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
   (
y_of_x (truncate_gamma3f_x #0.0 (h0cut y1) (&1) (&1)) (&0) (&0) (&0) y1 y2 y6  +
y_of_x (truncate_gamma3f_x #0.0 (h0cut y1) (&1) (&1)) (&0) (&0) (&0) y1 y3 y5  +
     (dih_y y1 y2 y3 y4 y5 y6 - 
      (dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
       dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2)) * #0.008  > &0 \/
     rad2_y y1 y2 y3 y4 y5 y6 < &2 \/
     eta_y y1 y2 y6 > #1.34 \/
     eta_y y1 y3 y5 > #1.34 \/
    dih_y y1 y2 y3 y4 y5 y6 < #1.946 \/
    dih_y y1 y2 y3 y4 y5 y6 > #2.089)`;
  doc =   "test";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "test gamma23bis";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, &2 * hminus);
    (&2,y4, sqrt8);
    (&2,y5, &2 * hminus);
    (&2,y6, sqrt8)
   ]
   (
y_of_x (truncate_gamma3f_x #0.0 (h0cut y1) (&1) (&1)) (&0) (&0) (&0) y1 y3 y5  +
     (dih_y y1 y2 y3 y4 y5 y6 - 
       dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2) * #0.008  > a_spine5 +
     b_spine5 * dih_y y1 y2 y3 y4 y5 y6 \/
     rad2_y y1 y2 y3 y4 y5 y6 < &2 \/
     eta_y y1 y2 y6 < #1.34 \/
     eta_y y1 y2 y6 > sqrt2 \/
     eta_y y1 y3 y5 > #1.34 \/
    dih_y y1 y2 y3 y4 y5 y6 > #1.074)`;
  doc =   "test";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
end;;

add
{
  idv = "test";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   (
    dih_y y1 y2 y3 y4 y5 y6  > &0 \/
     rad2_y y1 y2 y3 y4 y5 y6 < &2 \/
     eta_y y1 y2 y6 > sqrt2 \/
     eta_y y1 y3 y5 > sqrt2 )`;
  doc =   "test";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;


type_of theorems;;
follow;;
textchar;;
augment_search_results ["hi"];;
really_expand "?-0";;
help_grep "";;
help_flag "";;
help "apropos_short_order_script";;
suggest();;
String.sub "abcde" 1 (String.length "abcde" - 1);;
expand_suggest "0";;
hd it;;
List.nth !loaded_files 69;; Reload 1--69 
mk_thm;;
flyspeck_needs "general/lib.hl";;
flyspeck_needs "nonlin/kelvin_lattice.hl";;
flyspeck_needs "usr/thales/searching.hl";;
open Searching;;
rflyspeck_needs "usr/thales/init_search.hl";;
reneeds "packing/counting_spheres.hl";;
flyspeck_needs "packing/QZKSYKG.hl";;
flyspeck_needs "packing/DDZUPHJ.hl";;
flyspeck_needs "packing/AJRIPQN.hl";;
flyspeck_needs "packing/QZYZMJC.hl";;
flyspeck_needs "packing/marchal_cells_3.hl";;
flyspeck_needs "packing/GRUTOTI.hl";;
Grutoti.GRUTOTI;;
flyspeck_needs "fan/CFYXFTY.hl";;
flyspeck_needs "packing/counting_spheres.hl";;
open Counting_spheres;;
flyspeck_needs "nonlinear/cleanDeriv.hl";;
flyspeck_needs "nonlinear/cleanDeriv_examples.hl";;
flyspeck_needs "../development/thales/chaff/tmp/vectors_patch.ml";;
flyspeck_needs "../development/thales/chaff/tmp/determinants_patch.ml";;
flyspeck_needs "../development/thales/chaff/tmp/wlog_patch.hl";;
flyspeck_needs "trigonometry/trig2.hl";;
update_database();;
augment_search_results;;
!search_results;;
Counting_spheres.ORDER_AZIM_SUM2PI;;

let u11111 = ((GOAL_TERM (fun w -> ALL_TAC)):tactic);;
RDISK_R;;

GOAL_TERM (fun w -> (MP_TAC (ISPECL ( envl w [`p`;`v`;`u0`;`b`]) RCONE_PREP)));;

INST [(`u:bool`,`A:bool`)] (TAUT ` ((A ==> B) /\ A) ==> B`);;

let thh = Collect_geom.EQ_POW2_COND;;
let ta1 = TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`;;
let th2 = REWRITE_RULE[ta1] ( thh);;
let tm1 = snd (strip_forall (concl th2));;
let tm2 = snd (dest_imp tm1);;
let tm3 = fst (dest_eq tm2);;
let force_rewrite th;;



let goalx = `&0 <= sqrt x /\ &0 <= sqrt t ==> &0 <= sqrt u`;;
GMATCH_SIMP_TAC SQRT_POS_LE;;

let (asl,w) = (top_realgoal());;
let thm = SQRT_POS_LE;;
  let thm' = hd (mk_rewrites true thm []);;
  let t1 = fst (dest_eq(snd (dest_imp(concl(thm'))))) ;;
  let matcher u t = 
    let m = term_match [] t1 t in
    let _ = subset (frees t) (frees u) or failwith "" in
      m ;;
  let wsub u = find_term (can (matcher u)) u ;;
  let w' = wsub w ;;
  let vv = 
    let var1 = mk_var("v",type_of w') in
      variant (frees w) var1 ;;
  let athm = REWRITE_CONV[ ASSUME (mk_eq (w',vv))] w ;;
  let arhs = rhs (concl athm) ;;
  let bthm = (ISPECL [mk_abs(vv,arhs);w'] BETA_THM) ;;
  let betx = SYM(TRANS bthm (BETA_CONV (rhs (concl bthm)))) ;;
   ONCE_REWRITE_TAC[betx]
  MATCH_MP_TAC (lift_eq thm')
     BETA_TAC
 THEN BETA_TAC);;
rt[]


let lift_SQRT_POS_LE = GEN_ALL (MATCH_MP lift_imp (SPEC_ALL SQRT_POS_LE));;

add_rewrite_tag("mycase ",th);;
let xxx n = add_rewrite_stag (List.nth search_result_dump_march7_8am n);;
xxx 0;;
assoc (List.nth search_result_dump_march7_8am 0) !theorems;;

!rewrite_tags;;
let th = ASSUME (`!p q r. p ==> q ==> (cos r = s) /\ (u ==> sin y > &1)`);;

let gexp = `!t. (cos x + sqrt (t pow 2) > &0)`;;
let hexp = `!x. (cos x + sqrt (t pow 2) > &0)`;;


mk_rewrites;;


let matcherx u t = 
  let m = term_match [] t1 t in
  let _ = subset (frees t) (frees u) or failwith "" in
    m;;
let mmat u = find_term (can (matcherx u)) u;;
let mx = mmat hexp;;
let mma1 = term_match [] `sqrt x` (mmat hexp);;
let vv = 
  let var1 = mk_var("v",type_of mx) in
    variant (frees hexp) var1;;
let rrx = REWRITE_CONV[ ASSUME (mk_eq (mx,vv))] hexp;;
let rhsx = rhs (concl rrx);;
let bthx = (ISPECL [mk_abs(vv,rhsx);mx] BETA_THM);;
let betx = SYM(TRANS bthx (BETA_CONV (rhs (concl bthx))));;

term_match [] `sqrt x` mmat;;

st_of  `sin x + cos (asn t)`;;
mk_prover;;
net_of_thm;;
help "term_match";;
help "find_term";;
help "GEN_PART_MATCH";;
help "PART_MATCH";;
help "MATCH_MP";;
`(&0 <= sqrt (t pow 2)) \/ b ==> ~(&0 <= sqrt u)`
mmp lift_SQRT_POS_LE
rt[]
SPEC_ALL (ASSUME `!x. x = x`);;
let lift_SQRT_POS_LE = GEN_ALL (MATCH_MP lift_imp (SPEC_ALL SQRT_POS_LE));;
searcht 5 [`&0 <= sqrt x`];;

eval_command ~silent:true "let x111 = 1+1+4";;
x111;;
eval_command ~silent:false "mark 4";;
mark 4;;
snd it;;
help_grep "match";;
help "term_match";;  
help "PART_MATCH";;
find_term;;
help "find_term";;
List.map hd (split_proof_record [] [] (!proof_record));;
term_match;;
help "term_match";;
searchl;;

retrieve_search;;
thm_counts;;


eval_tactic_lines "st/r\nfxa mpt";;
text_char;;


process_to_string "date";;
gax();;


last (show_gax());;
List.nth (show_gax()) 2;;

Clean_deriv.x1_eta2;;
axioms();;
type_of `( %% )`;;
Qzyzmjc.QZYZMJC;;
search [name "FMSWMVO"];;
search [name "IVFICRK"];;
search [name "volume_props"];;
stm_depth "T";;
(* PROJECT BUILD *)
Hashtbl.hash;;

  (*
  let (d,hd) = data (get_tm_depth w) in
    filter (fun ((d',hd'),_,_) -> (((abs (d-d')< 1+k)  && sorted_meet 0 hd hd' ))) thml;; 
  *)

List.length (ballpark_theorems   (top_realgoal()));;
 (ballpark_theorems   (top_realgoal()));;
abs_of_float;;
int_abs;;
last [0;1;2;3];;
strip_imp `a`;;
strip_imp `a ==> b==> c`;;
help_grep "dest_";;
type_of `==>`;;
strip_comb;;
help_grep "strip";;
is_comb;;
help "strip_exists";;
strip_comb `a ==> b==> c`;;
help_grep "comb";;
help "strip_ncomb";;
help_grep "strip";;


let nearest_thm_to_goal thml (asl,w) = 
  let tt tl = List.flatten (map (tm_depth o concl) tl) in
  let common = tt (map snd asl) in
  let thl = map (fun (s,t) -> ((tm_depth o snd o strip_forall o concl )t,s,t) ) thml in
  let r = map (fun (tl,s,t) -> (tl,s,t,msd 0.0 common (tm_depth w) tl)) thl in
    (sort (fun (_,_,_,a) (_,_,_,b) -> a < b) r);;

let thml_depth_of_goalmatch thml (asl,w) = 
  let tt tl = List.flatten (map (tm_depth o concl) tl) in
  let w'::rest = List.rev strip_imp o  snd o strip_forall w in
  let common = tt ((map snd asl) @ rest) in
  let thl = map (fun (s,t) -> ((tm_depth o snd o strip_forall o concl )t,s,t) ) thml in
  let 
;;



nearest_thm_to_goal (ballpark_theorems (top_realgoal())) (top_realgoal());;
let guess = nearest_thm_to_goal (top_realgoal());;
List.length !theorems;;

top_realgoal;;
help_grep "goal";;
(* *)

tt;;
hd (!theorems);;
tt;;
strip_forall;;
help_grep "strip";;

(* jan 3, 2012 chaff *)



(* USEFUL CONSTRUCTS *)

let report s =
  Format.print_string s; Format.print_newline();;

g `?(x:A) . f A`

(* generalize *)

let ( TYPE_VAR :string -> (term -> tactic) -> tactic) = 
    fun s tm_tactic (asl,g) ->
      let (_,r) = dest_comb g in
      let (v,_) = dest_abs r in
      let (_,ty) = dest_var v in
	tm_tactic (mk_var(s,ty)) (asl,g);;

TYPE_VAR "x" EXISTS_TAC;
;;
Format.print_flush();;
FINITE_EMPTY;;

searcht 10 [`eulerA_hexall_x`];;

Sphere.num_combo1;;

(*
process_to_string "cat qed_log.txt | sed  's/^.*ineq./\"/' | sed 's/., secs.*$/\";/'  "

cat qed_log.txt | sed  's/^.*ineq./"/' | sed 's/., secs.*$/";/' | sort -u | wc  

(*
let _ = Sys.command("cat "^flyspeck_dir^"/../interval_code/qed_log.txt");;
*)
*)


let ee () = 
  let b = (false or (let _ = Sys.command("date") in failwith "h")) in b;;


suggest();;

EXISTSv_TAC "y";

dest_binder "?" (`?(x:A). f A`);;

(*

let searchl = sortlength_thml o search;;
let take = Lib_ext.take;;
let searcht r = take 0 5 (searchl r);;
let searchtake i j r = take i j (searchl r);;

*)
term_match;;
INSTANTIATE;;
  open Searching;;

definitions();;
State_manager.neutralize_state();;
let vv = (eval("1+1")) + 3;;
let vv = (eval("REFL `T`"));;
concl vv;;

prefixes();;
rev(infixes());;
binders();;
unparse_as_infix;;
map (List.nth (infixes())) (95--131);;
unparse_as_binder "!";;
binders();;


find_path ((=) `4`) `(sum (3..4) f)`;;  (* lrr *)

let kill_process n = Sys.command (Printf.sprintf "sudo kill -9 %d" n);;

help_grep "conj";;
help "list_mk_conj";;
 end_itlist;;

FROZEN_REWRITE_TAC [REAL_ARITH `b + d = d - (--b)`];;

let goal_types = Print_types.print_goal_types;;
Print_types.goal_types();;
Print_types.print_term_types `#2`;;
Print_types.print_thm_types (REFL `1`);;



(*
(* parsing printing *)
let pterm = Print_types.print_term_types;;
let tterm = Print_types.print_thm_types;;

#install_printer print_qterm;;


#install_printer Goal_printer.print_goal_hashed;;
#install_printer Goal_printer.print_goalstack_hashed;;

#remove_printer Goal_printer.print_goal_hashed;;
#remove_printer Goal_printer.print_goalstack_hashed;;

#print_length 1000;;
*)

search[`f (x:A) (g (y:A) z) = f (g x y) z`];; (* min, max, + /\, \/ *, compose, monoidal ops,
   APPEND, a - (b + c) = a - b - c /\ a - (b - c) = a - b + c),
    p ==> q ==> r <=> p /\ q ==> r);; *)

find_term  ( can (term_match[ `r a (r y z) = r (r x y) z`])) (concl IMP_IMP);;

filter_pred;;
can (term_match[]);;
type_of;;

constant_of_regexp "at.*[gn]$";;

constant_of_regexp "FILTER";;
searcht 15 [`cos`];;
def_of_string "FILTER";;

def_of_string "fan";;
conjuncts `!a b c. (u /\ v /\ (!c. w /\ r) /\ (!x y. r2 /\ r3))`;;


help "dest_forall";;
List.nth !theorems 0;;

help_grep ".*TAC$";;

INFINITE_DIFF_FINITE;;
search[`INFINITE`;`DIFF`];;


Format.set_max_boxes 100;;
let tt = hol_of_smalllist (1--300);;
string_of_my_term tt;;



let hel i = help (List.nth  tacsss i );;

hel 1;;

constant_of_regexp "sol";;

apropos;;
suggest;;


(* get all word counts in HOL LIGHT and FLYSPECK *)

let match_mp_strip =
  fun th ->
          let tm = concl th in
          let avs,bod = strip_forall tm in
          let ant,con = dest_imp bod in
          let th1 = SPECL avs (ASSUME tm) in
          let th2 = UNDISCH th1 in
          let evs = filter (fun v -> vfree_in v ant & not (vfree_in v con))
                           avs in
          let th3 = itlist SIMPLE_CHOOSE evs (DISCH tm th2) in
          let tm3 = hd(hyp th3) in
            MP (DISCH tm (GEN_ALL (DISCH tm3 (UNDISCH th3)))) th;;

let mp_short_list = 
  let u = fst(chop_list 50 (trigger_counts "MATCH_MP_TAC")) in
  let sl = map fst !theorems in
  let f1 = filter (fun (t,_) -> mem t sl ) u in
  let f2 = map (fun (s,n) -> (s,n,assoc s !theorems)) f1 in
    filter (fun (_,_,t) -> can  match_mp_strip t) f2;;


let relevant_match_mp r = 
  filter (fun (_,_,t) -> can (MATCH_MP_TAC t) r) mp_short_list;;

let suggest_match_mp () = relevant_match_mp (top_realgoal());;

mp_short_list;;

tachy"rep";;

tcs;;

grep -r "\bREPEAT\b" . | grep -v svn | sed 's/^.*REPEAT *//' | sed 's/ .*$//g'


let recent_search = ref [""];;

let refcount = ref [("",0)];;

trigger_counts "MATCH_MP_TAC";;

EQ_EXT;;
FINITE_SUBSET;;
search[regexp "EQ_SYM"];;
tachy "amt";;
tachy "asmcase";;

(* to get tacticals as well *)
(* grep "TYPE.*tactic" -i *.doc -l | sed 's/.doc//g' *)

List.length tactic_list;;
List.length(tachy "");;
subtract tactic_list (tachy "");;
tachy "bool";;

help "SUBST1_TAC";;

let typesss ss = 
  let split =   Str.split (Str.regexp "\n") in
  let cmd s = process_to_string ("(cd "  ^s^  "; grep TYPE "^ss^".doc | sed 's/TYPE[^{]*//g' )") in
  List.flatten (map ( split o cmd ) (!helpdirs));;

typesss "ALL_TAC";;
help "SUBST1_TAC";;

(*
let MP_TAC_BAK = MP_TAC;;
let MATCH_MP_TAC_BAK = MATCH_MP_TAC;;
*)


let mp_theorems = ref[];;
let incr1 thm = (mp_theorems:= thm::!mp_theorems);;

let MP_TAC_COUNT t  = 
  let _ = incr1 t in MP_TAC_BAK t;;

let MP_TAC = MP_TAC_COUNT ;;

let MATCH_MP_TAC_COUNT t  = 
  let _ = incr1 t in MATCH_MP_TAC_BAK t;;

let MATCH_MP_TAC = MATCH_MP_TAC_COUNT ;;
let MATCH_MP_TAC = MATCH_MP_TAC_BAK ;;


reneeds "trigonometry/trig2.hl";;

let thm_hash = Hashtbl.create 1000;;
map (fun (x,y) -> Hashtbl.add thm_hash y x) (!theorems);;

let find_name th = 
  try (Hashtbl.find thm_hash th) with Not_found -> "ANONYMOUS";;

List.length (search[`x:A`]);;

List.length (search[`x > (y:real)`]);; (* 111 *)

List.length (search[`x > &0`]);; (* 67 *)
 (search[`x > y`; omit `x > &0`]);; (* complicated thing > simple thing. *)
List.length (search[`x < y`]);; (* 1438 *)

List.length (search[`x >= &0`]);; (* 11 *)
List.length (search[`x <= (y:real)`]);; (* 1830 *)
List.length (search[`x >= y`; omit `x >= &0`]);; (* 85, complicated thing > simple thing. *)


(* IN -- no rhyme or reason. *)
List.length(search[`(IN)`])  (* 3455 *);;
List.length(search[`SETSPEC`]);;  (* 1071 *);;
List.length(search[`SETSPEC`;`(IN)`]);;  (* 568 *)
dest_comb `{x | T} y`;;
List.length (search[`y IN (GSPEC f)`]);; (* 23 *)
 (search[`y IN {u | f}`]);; (* 14 *)
(search[`{u | f} y`]);; (* 3 *)
(searcht 40 [`(IN)`;omit `SETSPEC`]);;  

dest_comb `{x | x > 0}`;;

List.length (search[`x < y`]);; (* 1438 *)

(* search, what is the arc cosine called?  acs *)

search[rewrite `inv`;`( / )`];;
searcht 5 [rewrite `inv`;`a*b`];;
search [regexp "[dD]iff"];;
is_rewrite "inv" ("",REAL_INV_MUL);;
heads (snd(dest_thm(REAL_INV_MUL)));;

Toploop.execute_phrase;;


types();;

constants();;
heads(concl(hd(definitions())));;




(* experiments *)

let _ = 
  let dds = map fst def_assoc in
    sort (fun (_,a) (_,b) -> a > b) (map (fun t-> (t,stm_depth t)) dds);;




let thm_depthnth n =
  let (s,th) = List.nth !theorems n in
  let d = thm_depth th in (s,d,th);;


tm_depth `!a b.  (&2 <= a /\ a <= #2.52) /\ &2 <= b /\ b <= #2.52
         ==>( ((\x. -- (&4 + a pow 2 - x pow 2)/(a * sqrt(ups_x (a pow 2) (b pow 2) (&4)))) has_real_derivative
              (&32 * a * b /( (sqrt (ups_x (a pow 2) (b pow 2) (&4))) pow 3)))
             (atreal b within real_interval [&2,#2.52]))`;;

let depth_filter n = filter (fun (_,t)-> 
	  let (_,c) = hd (thm_depth t) in (c <= n));;

searcht 10 [`has_real_derivative`;`real_div`];;
(* now distance between constants *)

help_grep_flags "rat" "i";;

help "REAL_RAT_REDUCE_CONV";;
stm_depth "pi";;
stm_depth "cos";;
stm_depth "sin";;
assoc "pi" def_assoc;;

thm_depthnth 1000;;

stm_depth "?";;
stm_depth "!";;
stm_depth "hull";;
stm_depth "uniformly_continuous_on";;
stm_depth "real_add";;
stm_depth "treal_add";;
stm_depth "hreal_add";;
stm_depth "nadd_eq";;
stm_depth "dist";;
stm_depth "-";;
stm_depth "PRE";;
stm_depth "_0";;
assoc "_0" def_assoc;;

dest_const `(+)`;;
s_depth "arclength";;

c_depth `acs`;;
c_depth `(@)`;;
assoc `T` def_assoc;;

rho_node;;

c_of [] `sin(cos (x + y))`;;

searcht 5 [`a/b + c/d`];;


searcht 5 [`x pow n = &0`];;

help_grep "REAL_RAT";;
    
pre_rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;

strip_comb `&1 + &2`;;
dest_comb;;




REAL_INV_DIV;;

searcht 5 [`inv`;`a/b`];;
searcht 5 [`a/b + c/d`];;
let (rr,_)=hd[(`(+)`,ratform_add);
		       (`( * )`,ratform_mul);(`( - )`,ratform_sub);
		       (`( / )`,ratform_div)];;
type_of rr;;
rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;
Calc_derivative.derivative_form `\q. sin(q pow 5)` `t:real` `{}:real->bool`;;
pre_rationalize `inv (w)`;;

Calc_derivative.derivative_form `(\x. --(&4 + a pow 2 - x pow 2) /       (a * sqrt (ups_x (a pow 2) (x pow 2) (&4))))` `b:real` `real_interval [&2,#2.52]`;;

searcht 5[`x pow 1`];;

search [name "HAS_REAL";name "COS"];;

search [`(within)`;`(:real)`];;

open Calc_derivative;;

  let th1 = 
    let x = `x:real` in
    let s = `{t | t > &0}` in
    let tm = `\x. x pow 3 + x * x - x * -- x + x/(x + &1)`in 
      differentiate tm x s;;

  let th1 = 
    let x = `x:real` in
    let s = `{t | t > &0}` in
    let tm = `(\q:real. (q  - sin(q pow 3) + q pow 7 + y)/(q pow 2  + q pow 4 *(&33 + &43 * q)) +  (q pow 3) *  ((q pow 2) / (-- (q pow 3))))` in
      differentiate tm x s;;

  let th2 = 
    let x = `x:real` in
    let s = `(:real)` in
    let tm = `\q.  cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in
      differentiate tm x s;;
  
  let th3 = 
    let x = `&5` in
    let s = `(:real)` in
    let tm = `\q.  cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in
      differentiate tm x s;;


(* prove rational identity modulo accumulating assumptions *)

  let   equ = `(&1 / u  - &1/v) pow 2  = inv u pow 2 - &2 * inv (u * v) + inv v pow 2`;;
  let eq0 = MATCH_MP (REAL_ARITH `u - v = &0 ==> (u=v)`);;

CONV_RULE rc (pre_rationalize `&1 / (x + y) - &1 / (x - y) - (-- &2 * y / (x pow 2 - y pow 2))`);;
  let lite_imp = MESON[] `ratform p a ;;

REAL_FIELD ` ((x - y - (x + y)) * (x pow 2 * &1 pow 2 - &1 pow 2 * y pow 2) -
      ((x + y) * (x - y)) * -- &2 * y * &1 pow 2 * &1 pow 2) = &0`;;
  
mk_neg;;
mk_binop;;

searcht 5 [`(a1 pow n / b1 pow n)`];;

let ratform_tac =   
    REWRITE_TAC [ratform] THEN
    REPEAT STRIP_TAC THENL
    [ASM_MESON_TAC[REAL_ENTIRE] ;
    REPEAT (FIRST_X_ASSUM (fun t -> MP_TAC t THEN ANTS_TAC THEN 
			     ASM_REWRITE_TAC[])) THEN 
    REPEAT STRIP_TAC THEN 
    ASM_REWRITE_TAC[] THEN 
    REPEAT (POP_ASSUM MP_TAC) THEN 
    CONV_TAC REAL_FIELD];;



let ratform_pow = prove_by_refinement(
  `ratform p1 r1 a1 b1 ==> ratform p1 (r1 pow n) (a1 pow n) (b1 pow n)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[ratform;GSYM REAL_POW_DIV];
  ratform_tac;
  ]);;  (* }}} *)

rational_identity `&1 / (x + y) - &1 / (x - y) = -- &2 * y / (x pow 2 - y pow 2)`;;


REAL_FIELD `&2 * x * y - &2 * y * x`;;


   let mk_derived tm =
     let (h1,[f1;f1';r1]) = strip_comb tm in
     let (h2,[b2;s1]) = strip_comb r1 in
     let (h3,b) = dest_comb b2 in
       (f1,SPECL [f1;f1';b;s1] triv) in

   let hooked_deriv hook =
     let assumed_rules = map mk_derived hook in
     let d_hyp tm  = 
       let r =        assoc tm assumed_rules in
       let _ = print_thm r in
	 r in

    let  triv = REWRITE_RULE[](REWRITE_CONV[derived_form] 
     `!f f' x s. derived_form ((f has_real_derivative f') (atreal x within s)) f f' x s` ) in 

differentiate_hook [`(f has_real_derivative (&17)) (atreal x within (:real))`] `\x. ((f:real->real) x) pow 2` `x:real` `(:real)`;;

  differentiate_hook [`(f has_real_derivative f') (atreal x within (:real))`] `f:real->real` `x:real` `(:real)`;;

let  triv = REWRITE_RULE[](REWRITE_CONV[derived_form] 
     `!f f' x s. derived_form ((f has_real_derivative f') (atreal x within s)) f f' x s` );;


mk_derived `(f has_real_derivative (&17)) (atreal x within (:real))`;;
assoc `f:real->real` [it];;
differentiate_hook;;

`(f has_real_derivative f') (atreal x within (:univ))`;;

  let d_hyp assumed_rules tm =
    snd(find (fun (r,s) -> aconv tm r) assumed_rules);;


let triv2 = prove_by_refinement(
  `f f' x s. derived_form ((f has_real_derivative f') (atreal x)) f f' x (:real)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[derived_form;WITHINREAL_UNIV];
  ]);;  (* }}} *)


(* acceptable forms
   `!x s. p ==> (f has_real_derivative f') (atreal x within s)`
   `!x s. p ==> (f has_real_derivative f') (atreal x)`
   `!x s. derived_form f f' x s`;;
*)

let thm5 = prove_by_refinement(
  `!x s. derived_form (p x /\ (!x s.  (derived_form (p x) f (f' x) x s))) f (f' x) x s`,
  (* {{{ proof *)
  [
    REWRITE_TAC[derived_form];
    MESON_TAC[];
  ]);;

let thm4 = prove_by_refinement(
  `!x s. derived_form (!x s.  (f has_real_derivative f' x) (atreal x within s)) f (f' x) x s`,
  (* {{{ proof *)
  [
    REWRITE_TAC[derived_form];
    MESON_TAC[];
  ]);;  (* }}} *)

let thm3 = prove_by_refinement(
  `!x s. derived_form (!x.  (f has_real_derivative f' x) (atreal x)) f (f' x) x s`,
  (* {{{ proof *)
  [
   REWRITE_TAC[derived_form];
    MESON_TAC[HAS_REAL_DERIVATIVE_ATREAL_WITHIN];
  ]);;  (* }}} *)

let thm2 = prove_by_refinement(
  `!x s. derived_form (p x /\ (!x. p x ==> (f has_real_derivative f' x) (atreal x) )) f (f' x) x s`,
  (* {{{ proof *)
  [
     REWRITE_TAC[derived_form];
    MESON_TAC[HAS_REAL_DERIVATIVE_ATREAL_WITHIN];
  ]);;  (* }}} *)

let thm1 = prove_by_refinement(
  `! x s. derived_form (p x /\ (!x s. p x==> (f has_real_derivative f' x) (atreal x within s)))
    f (f' x) x s`,
  (* {{{ proof *)
  [
    REWRITE_TAC[derived_form];
    MESON_TAC[];
  ]);;  (* }}} *)

let mk_derived  = 
  let     form1 =    `!x s. p x==> (f has_real_derivative f' x) (atreal x within s)`in
  let     form2 =    `!x. p x ==> (f has_real_derivative f' x) (atreal x)` in
  let     form3 =    `!x.  (f has_real_derivative f' x) (atreal x)` in
  let     form4 =    `!x s.  (f has_real_derivative f' x) (atreal x within s)` in
  let     form5 =    `!x s.  derived_form p f f' x s` in
  let fls =  [
    (form1,thm1);(form2,thm2);(form3,thm3);(form4,thm4);(form5,thm5)] in
  let mm tm (r,s) = 
    let ins = term_match [] r tm in
      INST ((fun (_,a,_) -> a) ins) s in
    fun tm -> 
      tryfind (mm tm) fls;;




df tm4;;
search [`within`;`atreal`;`has_real_derivative`;name "HAS_REAL"];;
let tm5 = `!x u. derived_form q g g' x u`;;
let tm4 = `!x u. (x > &0) ==> (g has_real_derivative (x pow 2)) (atreal x within u)`;;
if (can (term_match [] form5) tm) then tm else ( failwith "form5");;
MATCH_MP th4 tm4;;
MATCH_MP;;
let ins =  (term_match [] form4) tm4 ;;
INST ((fun (_,a,_) -> a) ins)  thm4;;

mk_derived tm5;;

   let mk_derived tm =
     let (h1,[f1;f1';r1]) = strip_comb tm in
     let (h2,[b2;s1]) = strip_comb r1 in
     let (h3,b) = dest_comb b2 in
       (f1,SPECL [f1;f1';b;s1] triv) ;;

 


MATCH_MP;;


  

type_of `has_real_derivative`;;
types_of `derived_form ((f has_real_deriv f') (atreal x within s))`;;



snd(top_realgoal());;
let (h1,[f;f';r]) = strip_comb (snd(top_realgoal()));;
let _ = (h1 = `(has_real_derivative)`) or 
  failwith "form 'f has_real_derivative f' atreal b within s' expected." ;;
let (h2,[atb;s1]) = strip_comb r;;
let (h3,b) = dest_comb atb;;
1;;
1;;

BETA_CONV;;



search[`A INTER B = B INTER A`];;

search[`&0 <= x * x`];;
REAL_ENTIRE;;

time REAL_RING `a' = &2 * a /\ b' = a*a - &4 * b /\ x2 * y1 = x1 /\ y2 * y1 pow 2 = &1 - b * x1 pow 4 /\ y1 pow 2 = &1 + a * x1 pow 2 + b * x1 pow 4 /\ ~(y1 = &0) ==> y2 pow 2 = &1 - a' * x2 pow 2 + b' * x2 pow 4`;;

Calc_derivative.differentiate `\t. &1/(cos (a * t pow 2))` `b+ &1` `(:real)`;;

time Calc_derivative.differentiate `\t. &1/(cos (a * t pow 2))` `b+ &1` `{x | x > &0}`;;




searcht 5 [`(a,b) = (c,d)`];;
``,
    if (NULLSET X) then {} else
        (let (k,ul) = cell_params V X in set_of_list (truncate_simplex (k-1) ul))`;;

LET_TAC;;

g `!(x). (x = x) \/ (!(x:num). x = x) \/ (!(y:bool). y = y)`;;

Print_types.print_goal_var_overload();;

hash_of_term `p /\ q ==> r`;;

tachy "rt";;


eval_goal `a /\ b /\ c /\ d ==> r /\ s`;;
eval_tactic_abbrev "rt/a,[TRUTH]";;

st/r,
rt/a,[];;

(!Toploop.parse_toplevel_phrase (Lexing.from_string ("let xx = `&1`;;")));;

eval_command "let xx = `(x:real) + 2`;;";;

eval_command "failwith \"hi\" ;;";;
eval_command "assocrx";;

thm_depth FACET_OF_POLYHEDRON;;
searcht 15 [`norm x = &1`];;


 let tachit s = 
   let alpha_num = Str.regexp "[a-z_A-Z]+" in
    let _ = Str.string_match alpha_num s 0 or failwith "tachit" in
    let m = Str.matched_string s in
    let ns = (break_init m s) in
    let n = if (String.length n > 0)
      el n (tachy m)   ;;
tachit "sgth";;
tachy "sgth";;

Str.regexp;;
String.escaped "/\\ ";;

Sys.command;;
Sys.command "date";;



(*
let lemma = prove_by_refinement(
  `!a b . (!t. a < t ==> b <= t) ==> (!t. a <= t ==> b <= t)`,
  (* {{{ proof *)
[
REPEAT STRIP_TAC ;
DISJ_CASES_TAC (REAL_ARITH `a< t \/ a = t \/ t < a`);
ASM_MESON_TAC [];
HASH_UNDISCH_TAC 1429 ;
DISCH_THEN DISJ_CASES_TAC;
ASM_REWRITE_TAC [REAL_ARITH `b<=t <=> (t < b ==> F)`];
DISCH_TAC ;
HASH_RULE_TAC 6466 (SPEC `(a + b)/ (&2)`);
ASM_REAL_ARITH_TAC ;
ASM_REAL_ARITH_TAC 
]
);;
  (* }}} *)
*)
*)
]
);;
  (* }}} *)


List.length tactic_counts;;
  end_itlist (fun (_,t) (_,u) -> ("",t + u)) tactic_counts20;;

let INFINITE_EXISTS = prove_by_refinement (
`!S. INFINITE S ==> (?(x:A). x IN S)`,
[
REWRITE_TAC[INFINITE];
REPEAT STRIP_TAC;
ASM_MESON_TAC[FINITE_EMPTY;Misc_defs_and_lemmas.EMPTY_EXISTS;];
]);;FINITE_EMPTY;;
INFINITE;;
FINITE_EMPTY;;

let INFINITE_EXISTS = prove_by_refinement (
`!S. INFINITE S ==> (?(x:A). x IN S)`,
[
REWRITE_TAC[INFINITE;GSYM Misc_defs_and_lemmas.EMPTY_EXISTS];
CONV_TAC (CONTRAPOS_CONV);
 THEN MESON_TAC[FINITE_EMPTY];

]);;

(* save. find strange constants *)

let symbolic_of cnames = 
  let symbolchar = explode "=-~.,@#$%^&*|\\/?><" in
    filter (fun t -> not (intersect (explode t) symbolchar=[])) cnames;;

let symbolic_constants = symbolic_of (map fst (constants()));;
let symbolic_infixes = symbolic_of (map fst (infixes()));;


searcht 5 [name "CHAIN";`has_derivative`];;
apropos();;
help "apropos_derivative";;
Calc_derivative.differentiate;;
Calc_derivative.derived_form;;
Calc_derivative.differentiate `cos` `x:real` `(:real)`;;

help;;
help "help";;

type_of `vector`;;

type_of;;
let types_of = Print_types.print_term_types;;
let type_of_thm = Print_types.print_thm_types;;
let type_of_goal = Print_types.print_goal_types;;
help_grep "type";;

help "apropos_types";;
types_of `($)`;;
has_derivative;;

map (fun t -> (t,type_of t)) (frees ` (!(y:real^6). p y ==> (continuous) (lift o f'') (at y within s))`);;

let arclength2 = prove_by_refinement(
  `!h.  (&1 <= h /\ h <= h0) ==> arclength (&2) (&2 * h) (&2) = acs(h / &2)`,
  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  MP_TAC (SPECL [`&2`;`&2 * h`;`&2`] Trigonometry1.ACS_ARCLENGTH);
  BRANCH_A [
    ANTS_TAC ;
    MP_TAC Sphere.h0;
    ASM_REAL_ARITH_TAC;
  ];
  DISCH_THEN SUBST1_TAC;
  AP_TERM_TAC;
  UNDISCH_TAC `&1 <= h`;
  BY (CONV_TAC REAL_FIELD);
  ]);;  (* }}} *)

let usage_count x = List.length (search [x]);;

(* marking *)
reset();;
show_marked();;

let marked = ref [];;
let show_marked() = map (fun t-> (t,assoc t !theorems)) (!marked);;
let mark s = 
  let th = assoc s (!theorems) in
  let _ = marked := s::!marked in
  th;;
let resetm() = marked:=[];;


term_match [] `s:C` `s:E->G`;;
frees_of_goal();;
`(r:B -> D) ((f:A->B) x) =  ((g:C->D) y)`;;
map types_of (gtypl [`f x`;`y`;`f`;`z:D`]);;
filter has_stv (setify (frees `f x`));;
apropos();;
help "apropos_types";;

 
let EZ_SOS_TAC equ =
  let lh = lhs equ in
  (REWRITE_TAC[REAL_ARITH `(x > y <=> y < x) /\ (x >= y <=> y <= x)`] THEN
    ONCE_REWRITE_TAC[REAL_ARITH `(x < y <=> &0 < y - x) /\ (x <= y <=> (&0 <= y - x))`]) THEN
let 
    fun (asl,w) -> 
      let eqthm = try    (REAL_FIELD eqn ) with _ -> failwith "sos_tac, REAL_FIELD failed" in
      let binop = 

rhs;;

searcht 5 [`x > y <=> x < y`];;

let equ = `(&1 - t) * (&1 pow 2) + t * (&1 - t) * (&1 pow 2) = (&1 - t pow 2)`;;
let lh = lhs equ;;
let (plus,adden) = strip_comb  lh;;
let _ = (plus = `(+)`) or failwith "sum expected";;
help_grep "strip";;
help "strip_comb";;

g `&1 + &1 = &2`;;
r,[];;

Str.split (Str.regexp "`") "`how `1` is it`";;
Str.split (Str.regexp "ab") "That is a better choice ab t";;
Str.split (Str.regexp "(\*") "^(* Start comment (* ( *) $";;

help_grep "dest";;
dest_pair `(a,b)`;;

map type_of [disjunct (`CARD`,`HAS_SIZE`)];;
search [disjunct (`HAS_SIZE`,`CARD`)];;
type_of `HAS_SIZE`;;
search [disjunct (`&0 < inv x`,`&0 < sqrt u`)];;
search [disjunct (`&0 < sqrt u`,`&0 < inv x`)];;
search [`&0 < sqrt u`];;

search[disjunct (`INJ`,`(f x = f y) ==> (x = y)`);disjunct(`CARD`,`HAS_SIZE`)];;

INJ_CARD;;

mk_rewrites false (ASSUME `!s. s = t`) [];;

net_of_thm false (ASSUME `s = t`) empty_net;;

empty_net;;

p();;
!invariant_under_linear;;


let pollack_inconsistency = 
  let thm1 = prove(  `?(n:num). (t < n)`,EXISTS_TAC`t + 1` THEN ARITH_TAC) in
  let t = mk_var("n < 0 /\\ 0",`:num`) in
    INST [(t,`t:num`)] thm1;;
(* *)

    let curryl = [Calc_derivative.atn2curry] ;;
    let curry = REWRITE_CONV curryl;;
    let uncurry = REWRITE_CONV (map GSYM curryl) ;;

uncurry `\x. atn2 (x,x + &1)`;;

curry `f`;;
(* 
Counting_spheres....
*)

!invariant_under_translation;;
searcht 10 [`dihV`;`arcV`];;
searcht 10 [`r f x y = f y x`;omit `#x`];;
VECTOR_ANGLE_ANGLE;;
search[name "ARCV_ANGLE"];;
search[`Arg`;`vector_angle`];;
searcht 10 [`azim`;`Arg`];;
(* from wlog_examples.ml *)

let TRUONG_1 = prove
 (`!u1:real^3 u2 p a b.
     ~(u1 = u2) /\
     plane p /\
     {u1,u2} SUBSET p /\
     dist(u1,u2) <= a + b /\
     abs(a - b) < dist(u1,u2) /\
     &0 <= a /\
     &0 <= b
     ==> (?d1 d2.
              {d1, d2} SUBSET p /\
              &1 / &2 % (d1 + d2) IN affine hull {u1, u2} /\
              dist(d1,u1) = a /\
              dist(d1,u2) = b /\
              dist(d2,u1) = a /\
              dist(d2,u2) = b)`,
  (*** First, rotate the plane p to the special case z$3 = &0 ***)

  GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` 


(* bug on loading misc.ml. (next is used as a variable, but later it becomes a constant  *)
Debug.Term_of_preterm_error
 [("function head", `next`, `:(?2712096)loop->?2712096->?2712096`);
  ("function arg", `0`, `:num`)].
Error in included file /Users/thomashales/Desktop/googlecode/hol_light/Multivariate/misc.ml
- : unit = ()

File "/Users/thomashales/Desktop/googlecode/hol_light/calc_rat.ml", line 515, characters 4-160:
Error: This expression has type
         (num -> term) * conv * conv * conv * (term -> thm) * (term -> thm) *
         (term -> thm) * (term -> thm) * 'a
       but an expression was expected of type
         (thm list * thm list * thm list -> positivstellensatz -> thm) ->
         thm list * thm list * thm list -> thm

(*
let backup_proof_record = !proof_record;;
List.length backup_proof_record;;
*)

(*
let rec clean_proof_record g skip tbs  = 
   function
       [] -> (g, EVERY (List.rev tbs))
     | Gax u :: xs -> clean_proof_record [u] skip tbs xs
     | Bax::xs -> clean_proof_record g (skip+1) tbs
     | Tax (_,_,t)::xs -> if (skip<=0) then clean_proof_record g 0 (t::tbs) xs else
	 clean_proof_record g (skip-1) tbs xs;;
      
let replay (g,t) = 
  

let replay_proof gax_no count = 
  let p1 = List.nth (gax()) gax_no in
  let p2 = fst(chop_list count p1) in
  let _ = proof_record:= p2 @ !proof_record in
    replay();;

let rotate_proof n =
  let (a,b) = chop_list n (gax()) in
    List.flatten (b,a);;
*)

  let _ = reneeds "usr/thales/init_search.hl" in ();;


let REAL_LEMMA = prove_by_refinement(
  `!t s. (&0 < t ) ==> (?x. &0 < x /\ (&0 < s + t * x))`,
  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  ASM_CASES_TAC (`&0 < s + t `);
    EXISTS_TAC `&1`;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  EXISTS_TAC `&1 - s/t`;
  CONJ_TAC;
    MATCH_MP_TAC (arith `&0 < (-- a)/b ==> &0 < &1 - a/b`);
    MATCH_MP_TAC REAL_LT_DIV;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  SUBGOAL_THEN `s + t * (&1 - s/t) = t` SUBST1_TAC;
    Calc_derivative.CALC_ID_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  BY(ASM_REWRITE_TAC[])
  ]);;  (* }}} *)

Topology.th1;;

let AZIM_ARG4 = prove_by_refinement(
  `!x v u w t1 t2 t3.  &0 < t3 /\ ~collinear {x , v , u} /\ ~collinear {x,v,w} ==>
    azim x v u w  = azim x v u (t1 % x + t2 % v + t3 % w)`,
  (* {{{ proof *)
  [
  st/r
  sgth `(?x. &0 < x /\ (&0 < (t1 + t2 + t3 * x)))` mptac
    rt[arith `t1 + t2 + t3*x = (t1 + t2) + t3*x`]
    mmp REAL_LEMMA
    art[]
    st
    sgth `(t3 % w = (t3 * x') % (&1/x' % (w:real^3)))` subst1
    rt[VECTOR_MUL_ASSOC]
    repeat (apthmtac ORELSE aptermtac)
    calc
    repeat (fxa mptac) then rat
      abbrev `s = t1 + t2 + t3 * x'`
      sgth `t1 % x + t2 % v + (t3 * x') % (&1/x' % w) = 
  ]);;  (* }}} *)

searcht 5 [`a % (b % c)`;`(a * b) % c`];;



  EXTREME_POINT_OF_FACE;;

FACE_OF_EQ;;  (* relative interiors of faces are disjoint *)

QOEPBJD;;
 FACE_OF_POLYHEDRON_POLYHEDRON;;

NEHRQPR;;
  POLYHEDRON_COLLINEAR_FACES;;



Graph_control.run(Graph_control.bezdek_reid_properties);;
flyspeck_needs "../glpk/fejesToth_contact/bezdek_reid_problem.ml";;
List.length Bezdek_reid_problem.archive;;
let brp = Bezdek_reid_problem.exec();;
let zbrp = zip Bezdek_reid_problem.archive brp;;
let feas = filter (fun (_,(a,_)) -> not(a = ["PROBLEM HAS NO PRIMAL FEASIBLE SOLUTION"]) && not (a = ["PROBLEM HAS NO FEASIBLE SOLUTION"])) zbrp;;
List.length feas;;
let mk_bb = Bezdek_reid_problem.mk_bb;;
let feas_bb = map (fun (t,_) -> mk_bb t) feas;;

open Bezdek_reid_problem;;
open Glpk_link;;
let out_bb = map (fun bb -> solve_branch_f model dumpfile "optival" ampl_of_bb bb) feas_bb;;
feas_bb;;

let bb = "154372608266 14 7 0 1 2 3 4 5 6 3 0 6 5 3 0 5 7 3 7 5 4 3 1 0 8 3 8 0 7 3 7 4 9 3 9 4 3 3 9 3 10 3 10 3 2 3 10 2 11 3 11 2 8 3 2 1 8 5 8 7 9 10 11 ";;
solve_branch_f model dumpfile "optival" ampl_of_bb (mk_bb bb);;

  let svar = mk_var (s,snd(dest_var t));;



let leaf_def = `leaf V u0 u1 = { u |  u IN V /\ ~collinear {u0,u1,u} /\
				     radV {u0, u1, u2} < sqrt2 }`;;

let leaf_ordering_def = `leaf_ordering V u0 u1 v f n = 
  leaf V u0 u1 HAS_SIZE n /\
  (! i j. i < n /\ j < n /\ (f i = f j) ==> (i = j)) /\
    (f n = f 0) /\
    (!i. i < n ==> (f i IN leaf V u0 u1)) /\
    u0 IN V /\ u1 IN V /\
    (!i j. i < j ==> azim u0 u1 v (f i) < azim u0 u1 v (f (i+1)))`;;
    
let mcell_group_def = `mcell_group V u0 u1 f i = 
      {X |   X SUBSET wedge u0 u1 (f i) (f (i+1)) /\
	   {u0,u1} IN edgeX V X /\
         X IN mcell_set V /\
	 ~(NULLSET X) }`;;

let mcell_group_sum = `!V u0 u1 v f n i.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\ i < n   ==>
  sum (mcell_group V u0 u1 f) (\X. dihX V X (u0,u1)) = azim u0 u1 (f i) (f (i+1))`;;

let mcell_group_4_type = `!V u0 u1 v f n X.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\
  X IN mcell_set V /\
  ~(NULLSET X) /\
  {u0,u1} IN edgeX V X /\
  FST(cell_params V X) = 4 ==>
  (?i. i < n /\
     azim u0 u1 (f i) (f (i+1)) < pi /\
     radV {u0,u1,(f i),(f (i+1))} < sqrt2  /\
     X IN mcell_group V u0 u1 f i)`;;

let mcell_group_23_type = `!V u0 u1 v f n X.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\
  X IN mcell_set V /\
  ~(NULLSET X) /\
  {u0,u1} IN edgeX V X /\
  FST(cell_params V X) IN {2,3} ==>
  (?i. i < n /\
     ~(azim u0 u1 (f i) (f (i+1)) < pi /\
     radV {u0,u1,(f i),(f (i+1))} < sqrt2)  /\
     X IN mcell_group V u0 u1 f i)`;;

(* consequence of previous 2 *)
let mcell_group_type = `!V u0 u1 v f n X.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\ 
  u0 IN V /\ u1 IN V  
  X IN mcell_set V /\
  ~(NULLSET X) /\
  {u0,u1} IN edgeX V X ==>
  (?i. i < n /\ X IN mcell_group V u0 u1 f i)`;;

let mcell_group_4_singleton = `!V u0 u1 v f n i.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\ i < n /\
  azim u0 u1 (f i) (f (i+1)) < pi /\
  radV {u0,u1,(f i),(f (i+1))} < sqrt2  ==>
  mcell_group V u0 u1 f i = {  mcell 4 V [u0;u1;(f i);(f (i+1))] }`;;

(* needed: ? *)

let mcell_sqrt2_barV = `!V u0 u1 w1 w2.
  packing V /\ saturated V /\
  {u0,u1,w1,w2} SUBSET V /\
  ~coplanar {u0,u1,w1,w2} /\
  radV {u0,u1,w1,w2} < sqrt2 ==>
  [u0;u1;w1;w2] IN barV V 3`;;

let mcell_group_3_a = `!V u0 u1 f v n i.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\ i < n /\
  (azim u0 u1 (f i) (f (i+1)) >= pi \/
  radV {u0,u1,(f i),(f (i+1))} >= sqrt2)  ==>
  (?X w. X IN mcell_group V u0 u1 f i /\
     [u0;u1;(f i);w] IN barV V 3 /\
     X = mcell3 V [u0;u1;(f i);w])`;;

let mcell_group_3_b = `!V u0 u1 v f n i.
  packing V /\ saturated V /\
  leaf_ordering V u0 u1 v f n /\
  1 < n /\ i < n /\
  (azim u0 u1 (f i) (f (i+1)) >= pi \/
  radV {u0,u1,(f i),(f (i+1))} >= sqrt2)  ==>
  (?X w. X IN mcell_group V u0 u1 f i /\
     [u0;u1;(f i);w] IN barV V 3 /\
     X = mcell3 V [u0;u1;(f i);w])`;;

(*
need if mcell3 V ul = mcell3 V vl , ul, vl IN barV, NONNULL, and both start with [u0;u1]
the ul = vl.  In particular, the two mcells in 3_a and 3_b are distinct, and
the w is uniquely determined by X.
*)

let mcell_group_3_exhaust = 
  `!V u0 u1 v f n i X.
    packing V /\ saturated V /\
    leaf_ordering V u0 u1 v f n /\
    1 < n /\ i < n /\
    X IN mcell_group V u0 u1 f i /\  
    FST(cell_params V X) = 3 /\
  (?w u.
     u IN {(f i),(f (i+1))} /\
     X = mcell3 V [u0;u1;u;w] /\ [u0;u1;u;w] IN barV V 3)`;;

(* also need formula for 4-cell gamma, 3-cell gamma, 2-cell gamma (as a function of angle)
   in terms of the functions that appear in ineq.hl.
*)


  module More = struct
    open Sphere;;
    open Ineq;;
add
  {
    idv = "FWGKMBZ";
    ineq = all_forall `ineq
      [(&2 * hminus, y1, &2 * hplus );
       (&2 ,y2,sqrt8 );
       (&2,y3,sqrt8);
       (&2,y4,sqrt8);
       (&2,y5,sqrt8 );
       (&2,y6,sqrt8 )
      ]
      (y_of_x delta_x y1 y2 y3 y4 y5 y6 > &0)`;
    doc = "
     This is used with rad2_x calculations to bound the denominator.
 ";
    tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Tex;Cfsqp;Xconvert;Branching];  
  };;
add
  {
    idv = "FHBVYXZ a";
    ineq = all_forall `ineq
      [(&2 * hminus, y1, &2 * hplus );
       (&2 ,y2,&2 * hminus );
       (&2,y3,&2 * hminus);
       (&2,y4,&2 * hminus);
       (&2,y5,&2 * hminus );
       (&2,y6,&2 * hminus )
      ]
      ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun  
	> &0)\/ 
	 (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
    doc = "
  OXLZLEZ.mod 'g_quqya' 'g_quqyb'
%old idv: 1118115412, cc:2bl
If $X$ is any quarter, and  $Y$ is a $3$-cell that flanks it, then
\\[ 
\\gamma(X,L) + \\gamma(Y,L) \\ge 0.
\\]  
Nov2012, changed eta_y y1 y3 y5 to eta_y y1 y2 y6.
 ";
(* + &0 * gamma3f y1 y3 y5 sqrt2 lmfun dropped *)
    tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];  
  };;
  end;;



Auto_lib.testsplit true "FHBVYXZ a";;
  map (fun t -> try (Auto_lib.testsplit bool t) with Failure _ -> [()]) cases;;
open Functional_equation;;
string_of_num (num_of `5`;;
dest_numeral `55555555555555`;;
i_mk2 `0`;;

	       module More = struct
		 open Sphere;;
		 open Ineq;;
add
{
  idv = "QZECFIC wt2 A"; (* was "test ratio" , y4 y5 swapped, nov 2012 *)
  ineq = all_forall `ineq
   [(sqrt2,y1,sqrt2);
    (sqrt2,y2,sqrt2);
    (sqrt2,y3,sqrt2);
    (&2 * hminus ,y4, sqrt8);
    (&2 * hminus, y5, sqrt8);
    (&2 ,y6, &2 * hminus)
   ]
   ( y_of_x (gamma3f_x_div_sqrtdelta (h0cut y4) (h0cut y5) (&1)) y1 y2 y3 y4 y5 y6 / &2 >  #0.008 * y_of_x dih4_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 \/
       eta_y y4 y5 y6 pow 2 > &2 
   )`;
  doc =   "gamma3f averages at least 0.008 per azim.
    We don't have a wt3 case because eta[2hminus,2hminus,2hminus]>sqrt2.";
  tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3;4]];
};;
add
{
  idv = "PEMKWKU test1"; 
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2 * hminus ,y2, sqrt8);
    (&2,y3, &2 * hminus);
    (&2 ,y4, sqrt8);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
   (
  ((y_of_x (gamma23_keep135_x (h0cut y1))  y1 y2 y3 y4 y5 y6) / &2  
   > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
      y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
    dih_y y1 y2 y3 y4 y5 y6 > #1.074 \/
     eta_y y1 y2 y6 pow 2 > &2 \/
     eta_y y1 y2 y6 pow 2 < #1.34 pow 2 \/
     eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
  doc =   "test";
  tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "BIXPCGW b test";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   ( (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 > &60) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
  doc =   "
   NONQXD
     If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Penalty (500.0,500.0);Tex;Xconvert];
};;
add
{
  idv = "BIXPCGW 6652007036 a2";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   ((dih_y y1 y2 y3 y4 y5 y6 < #2.8) )`;
  doc =   "
    OXLZLEZ.mod 'azim_c4' QX and QU
     If $X$ is a $4$-cell then  $\\dih(X) < 2.8$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
add
{
  idv = "BIXPCGW 7080972881 a2";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2 * hminus,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
    ((dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
  doc =   "
   OXLZLEZ.mod 'g_qxd' QXD
     If $X$ is a $4$-cell with a critical edge next to the spine, then  $\\dih(X) < 2.3$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
add
{
  idv = "BIXPCGW 1738910218 a2";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, &2 * hplus);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   ( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
  doc =   "
    OXLZLEZ.mod 'g_qxd'  QXD
     If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
add
{
  idv = "BIXPCGW 7274157868 a";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (&2 * hplus,y4, sqrt8);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
    ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
    (dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
  doc =   "
     OXLZLEZ.mod 'g_qxd' QXD
     If $X$ is a $4$-cell with a single critical edge (the spine), and if $\\dih(X)\\ge 2.3$,
      then  $\\gamma(X,L) > 0.0057$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
  idv = "GCKBQEA"; 
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   (
    dih_y y1 y2 y3 y4 y5 y6  > #0.606 
 )`;
  doc =   "Min angle on a cell along a spine.
     Nov 2012";
  tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
  idv = "JSPEVYT"; 
  ineq = all_forall `ineq
   [
     (&1,y1,&1);
     (&1,y2,&1);
     (&1,y3,&1);
    (&2 * hminus,y4, sqrt8);
    (&2 * hminus ,y5, sqrt8);
    (&2  ,y6, sqrt8)
   ]
   (eta_y y4 y5 y6 pow 2 > (#1.34) pow 2 )`;
  doc =   "eta small implies face small";
  tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
  idv = "IXPOTPA"; 
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (sqrt8,y4, &4 * hminus);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
   (let tan2lower = #3.07 in ( // Tan[Pi-2.089]^2
    let tan2upper = #6.45 in ( // Tan[Pi-1.946]^2
     delta_y y1 y2 y3 y4 y5 y6 < &0 \/
       delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
       (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
       (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 > tan2upper * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
     eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
     eta_y y1 y3 y5 pow 2 > #1.34 pow 2 \/
  (y_of_x (gamma23_full8_x (h0cut y1)) y1 y2 y3 y4 y5 y6 > &3 * #0.0057))))`;
  doc =   "Dec 2, 2012.  This is the case of TXQTPVC, when y4 >= sqrt8.  We can't use monotonicty here,
    because of the explicit dih constraints.";
  tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add{
  idv = "3287695934";
  doc="";
  tags = [Cfsqp;Tablelp;Xconvert;Tex];
  ineq = all_forall `ineq
    [ 
      (#4.37,y1,&4 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (&2 * h0,y4,&4 * h0);
      (#2.0,y5,&2 * h0);
      (#2.0,y6,&2 * h0)]
   (delta_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
add{
  idv = "4821120729";
  doc="";
  tags = [Cfsqp;Tablelp;Xconvert;Tex];
  ineq = all_forall `ineq
    [ 
      (&2,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.915);
      (#2.0,y5,&2 * h0);
      (#2.0,y6,&2 * h0)]
   (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)`;
};;
add{
  idv = "6762190381";
  doc="This reduces OWZLKVY to the case when delta_y < 200. Added 2013-4-18";
  tags = [Cfsqp;Tablelp;Xconvert;Tex];
  ineq = all_forall `ineq
    [ 
      (&2 ,y1,&2 * h0);
      (&2,y2,&2 * h0);
      (&2,y3,&2 * h0);
      (#3.01,y4,#3.915);
      (&2,y5,&2 * h0);
      (&2,y6,&2 * h0)]
   (
   delta_y y1 y2 y3 y4 y5 y6 < &200 \/ taum y1 y2 y3 y4 y5 y6 > &0 )`;
};;
add{
  idv = "8346775862";
  doc="In OWZLKVY the angle at y1 is obtuse. Added 2013-4-18.";
  tags = [Cfsqp;Tablelp;Xconvert;Tex];
  ineq = all_forall `ineq
    [ 
      (&2 ,y1,&2 * h0);
      (&2,y2,&2 * h0);
      (&2,y3,&2 * h0);
      (#3.01,y4,#3.915);
      (&2,y5,&2 * h0);
      (&2,y6,&2 * h0)]
   (
   delta_y y1 y2 y3 y4 y5 y6 > &200 \/ y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 ) `;
};;
add{
  idv = "8631418063";
  doc="In OWZLKVY the angle at y2,y3 is acute. Added 2013-4-18.";
  tags = [Cfsqp;Tablelp;Xconvert;Tex];
  ineq = all_forall `ineq
    [ 
      (&2,y1,&2 * h0);
      (&2,y2,&2 * h0);
      (&2,y3,&2 * h0);
      (&2,y4,&2 * h0);
      (#3.01,y5,#3.915);
      (&2,y6,&2 * h0)]
   (y_of_x delta_x4 y1 y2 y3 y4 y5 y6 > &0)`;
};;
add
{
  idv="5026777310a";
  doc="pentagon case, clipped A-piece triangle.   ";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (sqrt8,y4,#3.01);
    (sqrt8,y5,#3.01);
      (&2,y6,#2.52)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 4 1 - &2 * #0.11) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;
	       end;;



	       module More = struct
		 open Sphere;;
		 open Ineq;;
add
{
  idv="taum";
  doc="quad case top neg delta.
  Solve[Delta[x,2,2,x,2,3.01]==0,x] (*x < 3.166 *)
  Added 2013-05-05.";
  tags=[Cfsqp;Xconvert];
  ineq = all_forall `ineq [
      (&2,y1,#2.52);
      (&2,y2,#2.52);
      (#2.25,y3,#2.52);
      (#3.01,y4,#3.24);
      (&2,y5,&2);
      (&2,y6,&2)]
(taum y1 y2 y3 y4 y5 y6    > &0)`;
};;
add
{
  idv="test";
  doc="test ear";
  tags=[Cfsqp;Xconvert;Tex;];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.24);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( delta_y y1 y2 y3 y4 y5 y6 < &72 \/ taum y1 y2 y3 y4 y5 y6 > #0.038  )
 )`;
};;
add
{
  idv="test2";
  doc="testA ";
  tags=[Cfsqp;Xconvert;Tex;];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.24);
    (#3.01,y5,#3.24);
      (&2,y6,&2)
  ]
(
  (  taum y1 y2 y3 y4 y5 y6 > &0  )
 )`;
};;
add
{
  idv="test3";
  doc="";
  tags=[Cfsqp;Xconvert;Tex];
  ineq = all_forall `ineq [
      (#2.0,y1,#2.3);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.23607);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.23607)]
( delta_y y1 y2 y3 y4 y5 y6 > &30  \/
   enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.23607 )`;
};;
add
{
  idv="test4";
  doc="
    ";
  tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
   (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.027) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;
	       end;;


1;;
map Scripts.one_cfsqp ["test4"];;
map (Auto_lib.testsplit true) ["7697147739 delta top issue";"4680581274 delta top issue";];;

map (Auto_lib.testsplit true) [
   "6762190381";
   "8346775862";
   "8631418063";
   "4821120729";];;


let idq_of_string s = hd(Ineq.getexact s);;
idq_of_string "GRKIBMP B";;
Ineq.remove "GRKIBMP B";;
idq_of_string "GRKIBMP test";;
Auto_lib.testsplit true "BIXPCGW 1738910218 a2";;
map (Auto_lib.testsplit true)  [
"QITNPEA1 1 0 9063653052 A";
"QITNPEA1 1 1 9063653052 A";
"QITNPEA1 1 2 9063653052 A";
"QITNPEA1 2 0 9063653052 A";
"QITNPEA1 2 1 9063653052 A";
"QITNPEA1 2 2 9063653052 A";
];;


Scripts.one_cfsqp "GRKIBMP A V2";;
let [(s1,tags1,testineq1);(s2,tags2,testineq2)] = Optimize.preprocess_split_idq (hd(Ineq.getexact  "GRKIBMP A V2"));;
Auto_lib.execute_interval true tags1 s1 testineq1;;

Auto_lib.testsplit true "GRKIBMP A V2";;

Scripts.one_cfsqp "GLFVCVK4 2477216213 y4subcrit";;


conflicts `x + 1`  `x + &2`;;

aty;;
help_grep "cart";;
help "CONJ_PAIR";;
Debug.find_subterms;;
help_grep "ty";;
help "bty";;
help_grep "mkty";;
help_grep "mk_";;
help "mk_type";;
mk_type ("prod",[`:num`;`:bool`]);;

let follow_your_nose_string_list() = 
  let aslw = top_realgoal() in
  let m = filter (fun (p,_,_) -> p aslw) !noses in
  let m2 = map (fun ((_,_,a),b) -> ("{"^string_of_int b ^":"^a^"}")) (zip m (0--((List.length m) -1))) in
    Flyspeck_lib.join_comma m2;;

let fynlist k = 
  let aslw = top_realgoal() in
  let m = filter (fun (p,_,_) -> p aslw) !noses in
  let (_,t,_) = List.nth m k in
   t;;

String.sub "abcde" 0 4;;

let string_starts_with u s = (String.length u <= String.length s) && (u = String.sub s 0 (String.length u));;
string_starts_with "ab" "c";;

help_grep "prior";;
prioritize_real();;
Print_types.print_goal_types();;
bb 10;;


(* Sudoku solver *)
open String 

let rec s p=
  try 
    let rec(%)=(mod) and i=index p '0'and 
	b j=
          i<>j & (i/9=j/9||i%9=j%9||i/27=j/27&i%9/3=j%9/3) & p.[i]=p.[j] || j<80 & b(j+1)
    in
      iter (fun c->p.[i]<-c;b 0||()=s p;()) "948721536";
      p.[i]<-'0'
  with
      _->print_string p;;

s(read_line());;

let longt = filter (fun (_,t) -> (30 < t)) times;;
hour(total longt);;
List.length longt;;
map (fun (s,t) -> (s,float_of_int (t) /. 180.0)) longt;;

let t = `hello = there`;;



  INST_TYPE;;

  type_of  (inst [(`:b`,ty_b)]  b);;
help_grep "inst";;
inst;;
env;;

let inxx = ref[];;
let add_inequality idq = (inxx := idq::!inxx);;
flyspeck_needs "nonlinear/prep.hl";;
let inyy = map (fun t -> t.idv) (!inxx);;
index "4717061266" inyy;;  
List.length inyy;;
index "GRKIBMP B V2" inyy;;  

Preprocess.exec();;

mk_rewrites true (ASSUME `!a b. a ==> (b /\ c)`) [];;
SPEC_ALL (REFL `a:bool`);;
30 + 230 + 46 + 9 + 224 + 996 + 5;;
BETA_THM;;
ISPECL;;
Preprocess.preprocess1;;
let funx s = (Optimize.preprocess_split_idq  (hd (Ineq.getexact  (s))));;
funx "CJFZZDW";;
Flyspeck_lib.output_filestring;;

  let preprocess1 s = 
    let prep = Optimize.preprocess_split_idq 
		     (hd (Ineq.getexact  (s))) in
    let v = 
    Flyspeck_lib.join_lines (map Preprocess.print_one prep) in
    let _ = report v in
      ((s,map (fun (s,_,_) -> s) prep),v);;

Preprocess.preprocess1 "GLFVCVK4a 8328676778";;

g `c ==> b`;;
st/r;;
top_goal();;

(* generating proves prep ==> ineq.hl *)

(* follow preprocess_split_idq, step by step *)

  let strip_let_conv = REDEPTH_CONV let_CONV;;  (* strip_let_tm *)

  let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV);;

Optimize.get_split_tags;;

let PREPROCESS (s,tags,case) = 
  let is_xconvert = mem Xconvert tags in
  let is_branch = mem Branching tags in
  let strip_let_case = strip_let_conv case in
  let _ = report ("process and exec: "^s) in
  let tacl = 
    [PRELIM_REWRITE_TAC;
     MP_TAC (REWRITE_RULE[] NONLIN);
     if (is_branch) then (BRANCH_TAC) else (ALL_TAC);
     if (is_xconvert) then e (X_OF_Y_TAC) else e(ALL_TAC);
     if (is_branch && not(is_xconvert)) then
       (SERIES3Q1H_5D_TAC) else (ALL_TAC);
     STYLIZE_TAC;
     WRAPUP_TAC] in
  let _ = g (strip_let_case) in
  let _ = e (EVERY tacl) in
  let testineq = snd(top_goal()) in
    (s,tags,testineq);;

Optimize.split_h0;;
instantiation;;

g `c ==> b`;;
st/r
asmcase `a:bool` then (repeat (fxa mp))
1;;
refine(merge1_goal);;
 (top_asl_thm());;

UNDISCH;;
top_thm();;

top_thm();;
top_realgoal();;
List.length (!current_goalstack);;
List.nth (!current_goalstack) 0;;
CONJ;;

let (merge1_goal:refinement) = 
  fun (meta,sgs,just) ->
  if List.length sgs < 2 then (meta,sgs,just)
  else 
    let s0::s1::s2 = sgs in
    let _ = fst(s0) = [] or failwith "merge1_goal asl nonempty" in
    let _ = fst(s1) = [] or failwith "merge1_goal asl nonempty" in
    let sgs' = ([],mk_conj (snd s0, snd s1)) ::s2 in
    let just' i ths = 
      (just i ( (CONJUNCT1 (hd ths)) :: (CONJUNCT2 ( (hd ths))) :: tl ths)) in
      (meta,sgs',just');;

let top_asl_thm() =
  let (_,sgs,f)::_ = !current_goalstack in
  let t = snd(hd sgs) in
    DISCH t (f null_inst [ASSUME t]);;
  

help_grep "conj";;
mk_conj;;
help "ACCEPT_TAC";;
open Nonlinear_lemma;;
	   gcy_low;;
gcy_low_const;;
gcy_low_hminus;;
gcy_high;;
gcy_high_hplus;;

  let slxx = map (fun t -> t.idv) !Ineq.ineqs;;
hd slxx;;
List.length slxx;;
List.nth sl 442xx;;

prove_ineq "4528012043";;

let s = "4528012043";;
  let DSPLIT_TAC i = DISCH_TAC THEN (Optimize.SPLIT_H0_TAC i);;
  let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV);;
  let is_xconvert tags = mem Xconvert tags;;
  let is_branch tags = mem Branching tags;;
  let NONL = `prepared_nonlinear:bool`;;
  let idq = hd(Ineq.getexact s);;

  let (s',tags,ineq) = idq_fields idq;;
  let _ = (s = s') or failwith "prove_ineq: wrong ineq";;
    try (s,prove(mk_imp(NONL,ineq);;

g(mk_imp(NONL,ineq));;
	  

LET_ELIM_TAC 
	    (EVERY (map DSPLIT_TAC (get_split_tags idq)) );; 
	    EVERY
	    [
LET_ELIM_TAC;
	     PRELIM_REWRITE_TAC;;

	     e(if (is_branch tags) then BRANCH_TAC else ALL_TAC);;
	     e(if (is_xconvert tags) then X_OF_Y_TAC else ALL_TAC);;
	     e(if (is_branch tags && not(is_xconvert tags)) then SERIES3Q1H_5D_TAC else ALL_TAC);;
	     e(STYLIZE_TAC);;
	     e(WRAPUP_TAC);;
	     REWRITE_TAC (get_all_prep_nonlinear s)]))
    with Failure _ -> failwith s;;
List.length !Ineq.ineqs;;
List.length  !Prep.prep_ineqs;;


  module Test = struct
    open Hales_tactic;;
    open Counting_spheres;;
let FCHANGED_RADIAL_ALT = prove_by_refinement(
  `!(p:real^3->bool) f r.
    bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f facet_of p ==>
    radial r (vec 0) ( fchanged f INTER normball (vec 0) r)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[ Sphere.radial ];
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[ NORMBALL_BALL ];
  REWRITE_TAC[VECTOR_ADD_RID;VECTOR_SUB_RZERO;VECTOR_ADD_LID;VECTOR_SUB_LZERO];
  CONJ_TAC;
    BY(SET_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM_ST `fchanged` MP_TAC;
  REWRITE_TAC[IN_INTER];
  REWRITE_TAC[ Polyhedron.fchanged ];
  REWRITE_TAC[ IN_ELIM_THM ];
  REPEAT WEAK_STRIP_TAC;
  CONJ_TAC;
    TYPIFY `v1` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    TYPIFY `t * t'` EXISTS_TAC;
    REWRITE_TAC [ VECTOR_MUL_ASSOC ];
    REPEAT (FIRST_X_ASSUM_ST `a > b` MP_TAC);
    REWRITE_TAC [arith `a > b <=> b < a`];
    BY(MESON_TAC[ REAL_LT_MUL ]);
  INTRO_TAC Counting_spheres.RADIAL_NORMBALL [`(vec 0):real^3`;`r`];
  REWRITE_TAC[ NORMBALL_BALL ];
  REWRITE_TAC[ Sphere.radial ];
  REWRITE_TAC[VECTOR_ADD_RID;VECTOR_SUB_RZERO;VECTOR_ADD_LID;VECTOR_SUB_LZERO];
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[ IN_BALL ];
  REWRITE_TAC[ dist ];
  REWRITE_TAC[VECTOR_ADD_RID;VECTOR_SUB_RZERO;VECTOR_ADD_LID;VECTOR_SUB_LZERO];
  REWRITE_TAC[ NORM_NEG ];
  BY(ASM_MESON_TAC[SUBSET])
]
);;  (* }}} *)
  end;;

help_grep "stv";;

dest_imp `a ==> b`;;
REWR_CONV;;
help "IMP_REWR_CONV";;
help "net_of_thm";;
help "mk_rewrites";;
mk_rewrites false ADD_CLAUSES [];;
help "REWRITES_CONV";;
AUGMENT_SIMPSET;;
help "RULE_ASSUM_TAC";;
help "mk_prover";;
help "lookup";;
EQT_ELIM;;
help "EQT_ELIM";;
help "EQ_MP";;
help "TOP_SWEEP_SQCONV";;
help "rand";;
  type_of `nsum`;;
help "DISCH";;
help "MP";;
help "GEN_PART_MATCH";;
help_grep "mk_";;
list_mk_exists;;
help_grep "IMP";;
help "IMP_TRANS";;
help_grep "EXIST";;
help "SIMPLE_EXISTS";;
help "CHOOSE";;
help "EXISTS";;
SPEC_ALL;;
help_grep "GEN";;
help "GEN_ALL";;
help_grep "exist";;
help "mk_exists";;
help "IMP";;
help_grep "IMP";;
help "EQ_IMP_RULE";;
help "DISCH";;
help "DISCH_ALL";;
mk_rewrites;;

(map Merge_ineq.get_pack_nonlinear_non_ox3q1h ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";"QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW";]);;

Flyspeck_constants.calc `atn (sqrt (#3.07)) < pi - #2.089`;;

Oxl_merge.CELL_CLUSTER_ESTIMATE_PROPS;;

  let smt_timeouts=
["6988401556";
"7394240696";
"8248508703";
"7863247282";
"3862621143 back";
"3862621143 side";
"8519146937";
"4667071578";
"5026777310";
"OMKYNLT 1 2";
"3296257235";
"3862621143 front";
"7761782916";
"6944699408 a reduced";
"7726998381";
"4840774900";
"MKFKQWU";
"5451229371";
"7931207804";
"4652969746 1";
"5405130650";
"6224332984";
"4240815464 a reduced";
"3862621143 revised";
"4491491732";
"9563139965 f";
"8082208587";
"2065952723 A1";
"9563139965 d";
"8673686234 b";
"3603097872";
"1642527039";
"1395142356";
"OMKYNLT 3336871894"];;

  let t1 =  map (fun t -> (t,List.length((Ineq.getexact t)))) smt_timeouts;;
filter (fun (_,s) -> (s = 0)) t1;;

map Scripts.one_cfsqp smt_timeouts;;

  'ID[4322269127]'
   'ID[5556646409]';;

(* Analysis of constants for Clarke, Gao, et al. *)
(* moved to function_list.hl *)


 let tm1 = `domain6 (\x1 x2 x3 x4 x5 x6.
   &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
       &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
	      dih5_x  (rotate5 dih_x)`;;
 let thm1 = UNDISCH (MATCH_MP domain6_assum (ASSUME tm1));;


!help_path;;
help_path := ["/Users/thomashales/Desktop/googlecode/hol-light/Help"; "$/Help"];;
help "SPEC_ALL";;





  let cons2 = (map (const_types o test) (0--30));;
  let cons2 = (map (const_types o test) (0--100));;

const_types (test 740);;



Flyspeck_lib.nub cons;;
List.length i1;;

let has_matan = 
  let z1 = zip p1 cons in
  map fst (filter (fun (_,c) -> mem "matan" c) z1);;
let hss = map (fun t -> t.idv) has_matan;;

let testcase = "5202826650 a";;

let testcase = "7796879304";;
let testcases = subtract hss ["7796879304"];;
map (Auto_lib.testsplit true) testcases;;

  let i2 = map (fun t -> t.ineq) (!Ineq.ineqs);;
  let ct2 = setify (List.flatten (map cxx i2));;

  let ct3 = setify (ct2 @ ct1);;


  let p1 = !Prep.prep_ineqs;;
  let i1 = map (fun t -> t.ineq) p1;;
  let i1 =[ (find (fun t -> (t.idv = "2200527225")) p1).ineq];;
  hd i1;;
  let h1 =  (ASSUME (snd(strip_forall (List.nth i1 0))));;
  let test = 
    let u = REWRITE_RULE 
    [Nonlin_def.unit6;Sphere.rad2_x;Sphere.y_of_x;Sphere.rho_x;Sphere.delta_x;
     Sphere.ineq;Nonlin_def.sqrt_x1;Nonlin_def.sqrt_x2;Nonlin_def.sqrt_x3;
     Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x5;Nonlin_def.sqrt_x6;
     Sphere.vol_x;Sphere.gchi1_x;Sphere.gchi;Sphere.gchi2_x;Sphere.gchi3_x;
     Sphere.gchi4_x;Sphere.gchi5_x;Sphere.gchi6_x;
     Sphere.dih_x;Sphere.dih2_x;Sphere.dih3_x;Sphere.dih4_x;Sphere.dih5_x;
     Sphere.dih6_x;Sphere.dih_y;Sphere.dih2_y;Sphere.dih3_y;
     Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y;
     LET_DEF;LET_END_DEF;
     Sphere.delta_x4;Sphere.dih_x;Nonlin_def.unit6;
     Sphere.delta_y_LC;Sphere.delta_y;Nonlin_def.proj_x2;Nonlin_def.proj_x3;
     Mdtau.mdtau_y_LC;Mdtau.mdtau_y;Mdtau.mdtau2uf_y_LC;Mdtau.mdtau2uf_y;Sphere.rho;Sphere.ups_x;
     Sphere.ly;Mdtau.dua;Sphere.sol_y;Sphere.interp;
     Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x;Sphere.rhazim;Sphere.const1;
     Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y;
    ] h1 in
       (concl u);;
Print_types.print_term_types test;;

  let hs1 r =  (ASSUME (snd(strip_forall (List.nth (is1 (List.nth cases r)) 0))));;
  let h2 = REWRITE_RULE 
    [Nonlin_def.unit6;Sphere.rad2_x;Sphere.y_of_x;Sphere.rho_x;Sphere.delta_x;
     Sphere.ineq;Nonlin_def.sqrt_x1;Nonlin_def.sqrt_x2;Nonlin_def.sqrt_x3;
     Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x5;Nonlin_def.sqrt_x6;
     Sphere.vol_x;Sphere.gchi1_x;Sphere.gchi;Sphere.gchi2_x;Sphere.gchi3_x;
     Sphere.gchi4_x;Sphere.gchi5_x;Sphere.gchi6_x;
     Sphere.dih_x;Sphere.dih2_x;Sphere.dih3_x;Sphere.dih4_x;Sphere.dih5_x;
     Sphere.dih6_x;Sphere.dih_y;Sphere.dih2_y;Sphere.dih3_y;
     Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y;
     LET_DEF;LET_END_DEF;
     Sphere.delta_x4;Sphere.dih_x;Nonlin_def.unit6;
     Nonlin_def.gamma3f_x_div_sqrtdelta;
     Nonlin_def.sub6;Nonlin_def.constant6;Nonlin_def.mul6;
     Nonlin_def.scalar6;Nonlin_def.add6;Nonlin_def.mk_456;
     Sphere.rotate4;Sphere.rotate5;Sphere.rotate6;
     Nonlin_def.uni;Nonlin_def.two6;Nonlin_def.proj_x4;Nonlin_def.proj_x5;
     Nonlin_def.proj_x6;Nonlin_def.compose6;
     Sphere.sol_euler_x_div_sqrtdelta;Nonlin_def.proj_y4;Nonlin_def.proj_y5;
     Nonlin_def.proj_y6;
     
    ] (hs1 10);;

List.nth p1 3;;
list_mk_conj;;

Nonlin_def.unit6;;
Sphere.dih_x;;


Sphere.atn2;;

  let cxx i = setify (map fst (Print_types.get_const_types i));;

  let p1 = !Prep.prep_ineqs;;
  let i1 = map (fun t -> t.ineq) p1;;
  let ct1 = setify (List.flatten (map cxx i1));;

  let i2 = map (fun t -> t.ineq) (!Ineq.ineqs);;
  let ct2 = setify (List.flatten (map cxx i2));;

  let ct3 = setify (ct2 @ ct1);;


Nonlin_def.safesqrt;;

List.nth p1 3;;
list_mk_conj;;

Nonlin_def.unit6;;
Sphere.dih_x;;


Sphere.atn2;;


ct1;;
List.length ct1;;

flyspeck_needs "../glpk/sphere.ml";;
flyspeck_needs "nonlinear/check_completeness.hl";;
  let check_completeness_out = Check_completeness.execute();;


(* bcc lattice revisited *)




(* BCC LATTICE PROJECT *)

flyspeck_needs  "../projects_discrete_geom/bcc_lattice.hl";;
  let ineq_list  = ["EIFIOKD-a";"EIFIOKD-b";"EIFIOKD-c";"EIFIOKD1";"EIFIOKD2";"EIFIOKD3";"EIFIOKD4"];;
let testid =   "EIFIOKD-a";;

let uu = (hd(Ineq.getexact testid)).ineq;;
    let vv = REWRITE_RULE 
    [LET_DEF;LET_END_DEF;
     Bcc_lattice.selling_surface_nn;
     Bcc_lattice.selling_surface_num;
     Bcc_lattice.selling_volume2;
     Bcc_lattice.bcc_value;
    ] (ASSUME uu);;

Ineq.add {
  idv=(testid^"-test");
  ineq = (concl vv);
  doc = "BCC";
  tags = [];
};;

1;;

    let testid2 = testid^"-test";;
Optimize.testsplit false testid2;;
map (Optimize.testsplit true) !testids;;

(* END BCC *)

Auto_lib.terms_with_real_arity_ge8;;
report Auto_lib.fn_code;;
Auto_lib.tmpfile;;
 Optimize.preprocess_split_idq (hd(Ineq.getexact "test B1-100"));;
Auto_lib.mkfile_code (all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
      (#3.01,y4,#3.915);
   (#3.01,y5,#3.915);
      (#3.01,y6,#3.915)
  ]
  (( taum y1 y2 y3 y4 y5 y6 +
          y_of_x (mudLs_234_x (sqrt(&15)) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0 
    > #0.712) \/
    y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
    y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
     (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0) 
)`)   "X" [];;

itlist;;
flyspeck_needs;;
install_functions();;
rflyspeck_needs "nonlinear/scripts.hl";;

    let run s = 
      let _ = Ineq.add s in
	Scripts.one_cfsqp s.idv;;

    rflyspeck_needs   "nonlinear/auto_lib.hl";;

    let run2 s = 
      let _ = Ineq.add s in
	Auto_lib.testsplit true s.idv;;

    let run2f s = 
      let _ = Ineq.add s in
	Auto_lib.testsplit false s.idv;;

for i1=0 to 4 do
for i2=i1 to 4 do 
for i3=i2 to 4 do 
      run2 (make_hex_ear i1 i2 i3) done done done;;


    let r k = report (string_of_int k);;
r 1;;

(*
let is_sphere= new_definition`is_sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;


let NULLSET_RULES2 = prove_by_refinement
 (`(!P. ((plane P)\/ (is_sphere P) \/ (circular_cone P)) ==> NULLSET P) /\
   (!(s:real^3->bool) t. (NULLSET s /\ NULLSET t) ==> NULLSET (s UNION t))`,
  [
    SIMP_TAC[NEGLIGIBLE_UNION] ;
    X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC;
    MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE ;
    SIMP_TAC[COPLANAR; DIMINDEX_3; ARITH] THEN ASM_MESON_TAC[SUBSET_REFL];
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [is_sphere]) ;
    STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ;
    ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE];
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [circular_cone]) ;
    REWRITE_TAC[EXISTS_PAIRED_THM; c_cone] THEN STRIP_TAC ;
    ASM_REWRITE_TAC[] ;
    MP_TAC(ISPECL [`w + v:real^3`; `v:real^3`; `r:real`]     NEGLIGIBLE_RCONE_EQ) ;
    ASM_REWRITE_TAC[rcone_eq; rconesgn] ;
    REWRITE_TAC[dist; VECTOR_ARITH `(w + v) - v:real^N = w`] ;
    ASM_REWRITE_TAC[VECTOR_ARITH `w + v:real^N = v <=> w = vec 0`]
  ]);;

let NULLSET_IS_SPHERE = prove_by_refinement
 (`(!P. is_sphere P ==> NULLSET P)`,
  [
    X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC;
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [is_sphere]) ;
    STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ;
    ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE];
  ]);;
*)
1;;

add
{
  idv="1347067436";
  doc="old name: local max v4*, WNLKGOQ, 1671775772 (with #0.12->#0.1)  8146670324
    better local max test.
    This is the numerator of the 2nd derivative of the function taud.
    Case delta > 20.";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52); 
    (&2,y3,#2.52);
    (#3.01,y4,#3.237);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
    (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  > &0 \/
    y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  < &0 \/
    y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
       y_of_x taud_x y1 y2 y3 y4 y5 y6 > #0.12 \/
  delta_y y1 y2 y3 y4 y5 y6 < &20)`;
};;

run
{
  idv="test 8723570049";
  doc="local fan/main estimate/terminal pent
    y1=2.52, delta>=20, falls into taum>=0.12 case";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52); 
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.237);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
(taud y1 y2 y3 y4 y5 y6 > #0.12 \/
delta_y y1 y2 y3 y4 y5 y6 < &20
)`;
};;



Calc_derivative.differentiate `f:real->real` `x:real` `(:real)`;;
Calc_derivative.differentiate `\x. (f (x pow 2)):real`  `x:real` `(:real)`;;



run
  {
idv = "test 22065952723 A1";
doc = "This is the case that $a_2 \\le 15.53$.
   $a_2$ upper bound changed on 2011-Jan-21. 
   If larger than 15.53, it must be in a hexagon,  and two consecutive straight vertices.  
   Warning: this is verified by custom code (using cfsqp heuristics)
   in the interval arithmetic calculations.
   Fixed statement 2013-06-01.
 ";
(* was (num_combo1 e1 e2 e3 a2 b2 c2 > &0)  *)
tags=[Flypaper["UPONLFY"];Tex]; 
ineq = Sphere.all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, #15.53);
  ((&2 / h0) pow 2, b2, &4 pow 2);
  ((&2 / h0) pow 2, c2, &4 pow 2)
  ]
   ((num1 e1 e2 e3 a2 b2 c2) pow 2 > &0 \/
    num2 e1 e2 e3 a2 b2 c2 < &0)`;
};;


time;;
List.length Check_completeness.r_init;; (* 15 *)
List.length Check_completeness.triquad_assumption;; (* 3 *)


Check_completeness.terminal_cs;;
List.length Check_completeness.terminal_cs;;
List.nth Check_completeness.terminal_cs 21;;

run
{
  idv="2900061606";
  doc="triangle 1,2-ac";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = Sphere.all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#2.52,y5,#2.52);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + (tame_table_d 2 1 - #0.11)
 )`;
};;

run
{
  idv="testx";
  doc="";
  tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = Sphere.all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
   ups_x (y2*y2) (y3*y3) (y4*y4) * ups_x (y4*y4) (y5*y5) (y6*y6) > &0
 )`;
};;

(*
June 4, 2013:

3 long: 4010906068
2 long: 6833979866
1 long (out to sqrt8): 5541487347

deprecated:
OMKYNLT ....
7645170609;;
*)

Ineq.getexact "5541487347";;
open Terminal;;




new_build_silent();;




let old_then = ( THEN );;
let old_prove = prove;;
let old_prove_by_refinement = prove_by_refinement;;
old_then;;

let tactic_counter = ref [3];;

let new_prove_by_refinement(g,thml) = 
  let _ = tactic_counter := (List.length thml :: !tactic_counter) in
    old_prove_by_refinement (g,thml);;

let prove_by_refinement = new_prove_by_refinement;;

rflyspeck_needs "packing/counting_spheres.hl";;
let _ = 
  let prove_by_refinement = new_prove_by_refinement in
    flyspeck_needs "packing/counting_spheres.hl";;

!tactic_counter;;

let tlist = (Lib.sort (<) !tactic_counter);;
List.length tlist;;
List.nth (Lib.sort (<) tlist) (188 / 2);;

end_itlist (+) tlist;;

(end_itlist (+) ) (snd (chop_list (188 /2) tlist));;


let all_forall = Sphere.all_forall;;


run2
{
  idv="8495326405";
  doc=" Main estimate/quad case.
   ";
  tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,&2);
    (&2,y2,&2);
    (#3.01,y3,&6);
    (&2,y4,&2);
    (&2 * h0,y5,&2 * h0);
      (#3.01,y6,&6)
  ]
  ( delta_y y1 y2 y3 y4 y5 y6 < &0)`;
};;


run
{
  idv="test 8748498390";
  doc=" 0.513 estimate, A-piece triangle.
   One diagonal exactly 3.01. Added 2013-06-13";
  tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.1);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,#2.52);
    (#2.52,y5,#3.01);
      (#3.01,y6,#3.01)
  ]
  ( taum y1 y2 y3 y4 y5 y6  + #0.12 * (y1 - &2) > #0.403 )`;
};;

run
{
  idv="test 2445657182";
  doc=" 0.513 estimate. ear. Combine with 8748498390 along diagonal 3.01.
    Added 2013-06-13.";
  tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,#2.52);
    (&2,y5,#2.52);
      (#3.01,y6,#3.01)
  ]
  ( taum y1 y2 y3 y4 y5 y6   > #0.11 + #0.12 * (y1 - &2))`;
};;

(*  + #0.5 * (#3.01 - y6) ;; *)

run
{
  idv="test 2445657182";
  doc=" 0.513 estimate. ear. Combine with 8748498390 along diagonal 3.01.
    Added 2013-06-13.";
  tags=[Flypaper["FHOLLLW"];Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&1,y1,&1);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (sqrt8,y4,#3.0);
    (&2,y5,#2.52);
      (&2,y6,#2.52)
  ]
  ( delta_y (&0) y2 y3 y4 y5 y6 > &0 )`;
};;

add
{
  idv="test";
  doc= "Used with 5691615370.
    Added 2013-06-19.";
  tags=[Cfsqp;Xconvert;Tex;Lp_aux "5691615370";Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&3,y1,&4 * h0);
    (&2,y2,#2.472);
    (&2,y3,#2.472);
    (&3,y4,&4 * h0);
    (&2,y5,#2.472);
      (&2,y6,#2.472)
  ]
  ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )`;
};;

add
{
  idv="test";
  doc= "";
  tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&3,y1,&4 * h0);
    (&2,y2,#2.472);
    (&2,y3,#2.472);
    (&3,y4,&4 * h0);
    (&2,y5,#2.472);
      (&2,y6,#2.472)
  ]
  (  delta_y y1 y2 y3 y4 y5 y6 < &200 )`;
};;



let eta2_126 = new_definition `eta2_126 x1 (x2:real) (x3:real) (x4:real) (x5:real) x6 = 
  (eta_y (sqrt x1) (sqrt x2) (sqrt x6)) pow 2`;;
Functional_equation.functional_overload();;

let nonf_ups_126 = prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. ups_126 x1 x2 x3 x4 x5 x6 = ups_x x1 x2 x6`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.ups_126];
  BY(Functional_equation.F_REWRITE_TAC)
  ]);;  (* }}} *)


searcht 5 [`BB1`];;

let t =  `V = IMAGE vv (:num)`;;
    let (a,b) = dest_eq t ;;
    let b' = env (top_realgoal())  b ;;
    let a' = tysubst [type_of b',type_of a] a ;;
    type_of a';;
    type_of b';;
    type_of b;;
    let t' = mk_eq (a',b') ;;
      ABBREV_TAC t' (asl,w);;

top_goal();;
inst;;

    type_of (inst [`:B`,`:A`] `x:A`);;

help "inst";;
help "type_subst";;
help "tysubst";;
help "instantiate";;

    let t = 
    let (a,b) = dest_eq t ;;
    let b' = env (asl,w) b ;;
    let (a',_) = dest_var a ;;
    let t' =   mk_eq(mk_var(a',type_of b'),b');;
type_of t';;

ABBREV_TAC t' (asl,w);;



run
{
  idv="4887115291";
  doc="old name: angles pent*
    Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
  ";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.01);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
(  #1.75 < dih_y y1 y2 y3 y4 y5 y6 
)`;
};; 

run
{
  idv="6789182745";
  doc="old name: test A*
   Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
  ";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = Sphere.all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
      (#3.01,y5,#3.237);
    (#3.01,y6,#3.237)
  ]
(
     (dih_y y1 y2 y3 y4 y5 y6 < #1.109) 
 )`;
};;

run
{
  idv="3405144397-numerical";
  doc="old name: test8*
   Local-fan/Main-estimate/terminal-pent/both-ears-under-20.
   ear dih inequality when delta < 20";
  tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
      (&2,y5,&2);
    (#3.01,y6,#3.237)
  ]
(
  (delta_y y1 y2 y3 y4 y5 y6 > &20)  \/
     (dih_y y1 y2 y3 y4 y5 y6 < (#1.75 - #1.109) / &2) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;

run
{
  idv="test 3405144397";
  doc="ear dih ineq when delta < 20.
   Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
    Adaptation of 9459075374.
    (EAR) A bound on the delta of an ear in a pent,
   The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.3205 = (1.75-1.109)/2)  has been 'linearized'. 
   Tan[0.3205]^2 = (>=) 0.110186
   In more detail, this calc shows that delta > 20 or dih < 0.3205
   By 4887115291, we know that the combined angle at the crowded node of a pent is
   at least 1.75.  If both ears have delta < 20, then combined angle
   is at least 1.109 + 2 * 0.3205 = 1.75, so a cross diag <= 3.01.
   Hence wlog one of the two ears has delta >= 20.
   ";
  tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
     (#3.01,y5,#3.237);
      (&2,y6,#2.52)
  ]
(let tan2lower = #0.110186 in
   (delta_y y1 y2 y3 y4 y5 y6 > &20) \/
  (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
 )`;
};;

    let all_forall = Sphere.all_forall;;


List.length remain;;

	(filter Merge_ineq.is_ox3q1h (!Ineq.ineqs));;

	   Merge_ineq.packing_ineq_data;;

Ysskqoy.pack_ineq_def_a;;


Script.unfinished_cases();;
searcht 5 [def "deformation"];;

g Appendix.NUXCOEAv2_concl;;

let NUXCOEAv2=prove_by_refinement((Appendix.NUXCOEAv2_concl),
MP_TAC Nuxcoea.NUXCOEA
 ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
mt[]
st/r
fxa mmp
typ `j` ex
rule (orr[EQ_SYM_EQ])
art[]
THEN MESON_TAC[]);;
g Appendix.IMJXPHRv2_concl;;

let IMJXPHRv2=prove((Appendix.IMJXPHRv2_concl),
MP_TAC Imjxphr.IMJXPHR
 ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
mt[]
  THEN
 MESON_TAC[]);;
g Appendix.ODXLSTCv2_concl;;

let ODXLSTCv2=prove((Appendix.ODXLSTCv2_concl),
MP_TAC Odxlstcv2.ODXLSTCv2
 ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
st/r
fxa (C intro [`s`;`k`;`w`;`l`])
rt[]
amt[]

art[]

rt[]
mt[]


THEN MESON_TAC[]);;
Appendix.NUXCOEAv2_concl;;

module Test = struct

  open Imjxphr;;
  open Nuxcoea;;

let NUXCOEAv2=prove((Appendix.NUXCOEAv2_concl),
MP_TAC NUXCOEA
THEN ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
THEN MESON_TAC[]);;

let IMJXPHRv2=prove((Appendix.IMJXPHRv2_concl),
MP_TAC IMJXPHR
THEN ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
THEN MESON_TAC[]);;

let ODXLSTCv2=prove_by_refinement((Appendix.ODXLSTCv2_concl),
[
  MP_TAC Odxlstcv2.ODXLSTCv2;
  ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC];
  REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`s`;`k`;`w`;`l`]);
  REWRITE_TAC[];
  BY(ASM_MESON_TAC[])
]);;

				  end;;

searcht 5 [`arclength`;`atn`];;

let arclength222h0 = prove_by_refinement(
  `arclength (&2) (&2) (&2 * h0) < pi / &2`,
  (* {{{ proof *)
  [
  GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1;
  CONJ_TAC;
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
    BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `x + y < x <=> y < &0`];
  ONCE_REWRITE_TAC[GSYM ATN_0];
  MATCH_MP_TAC ATN_MONO_LT;
  REWRITE_TAC[arith `(x / y < &0 <=> &0 < (-- x)/ y)`];
  GMATCH_SIMP_TAC REAL_LT_DIV;
  GMATCH_SIMP_TAC SQRT_POS_LT;
  REWRITE_TAC[Sphere.h0];
  BY(REAL_ARITH_TAC)
  ]);;  (* }}} *)

let arclength_2h0_cstab = prove_by_refinement(
  `arclength (&2) (&2) (&2 *h0) + arclength (&2) (&2) cstab < pi`,
  (* {{{ proof *)
  [
  REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
  REWRITE_TAC[GSYM CONJ_ASSOC];
  CONJ_TAC;
    BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
  CONJ_TAC;
    BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `(pi/ &2 + b) + (pi / &2 + d) < pi <=> b + d < &0`];
  REWRITE_TAC[Sphere.h0;Sphere.cstab];
  MP_TAC (Flyspeck_constants.calc `atn (((&2 *  #1.26) * &2 *  #1.26 - &2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 + &2 *  #1.26) *   (&2 + &2 - &2 *  #1.26) *   (&2 + &2 *  #1.26 - &2) *   (&2 *  #1.26 + &2 - &2))) + atn (( #3.01 *  #3.01 - &2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 +  #3.01) *   (&2 + &2 -  #3.01) *   (&2 +  #3.01 - &2) *   ( #3.01 + &2 - &2))) < &0`);
  BY(REWRITE_TAC[])
  ]);;  (* }}} *)

run
  {
    idv="test 6843920790";
    doc = "In a pentagon with one long edge, we can contract the long edge to 2.52, 
   or even to 2, using 2 diags.
   The constant 2.38 < 3.01/h0.";
    tags=[];
  ineq = Sphere.all_forall `ineq
      [
	(&1 , e1, &1 + sol0/ pi);
	(&1 , e2, &1 + sol0/ pi);
	(&1 , e3, &1 + sol0/ pi);
	((&2 / h0) pow 2, a2, #2.52 pow 2);
	(#2 pow 2, b2, #15.53);
	((#3.01/ #1.26) pow 2, c2, #15.53)
      ]
      ((num1 e1 e2 e3 a2 b2 c2  > &0) ) `;
  };;

help_grep "strip";;
let thm = Localization.deformation;;

let c = fst(dest_const (fst (strip_comb (fst (dest_eq (snd (strip_forall (concl thm))))))));;

(* TRIAL DEFINITION *)

let deflist = ref [];;

let adddef thm = 
  let c = fst(dest_const (fst (strip_comb (fst (dest_eq (snd (strip_forall (concl thm)))))))) in
  let _ = deflist := (c,thm)::!deflist in
    c;;

let getd s = 
  try assoc s (!deflist)
  with _ -> failwith ("definition "^s^" not found");;

List.length !proof_record;;
hd !proof_record;;


bb;;
find;;
index;;


Searching.searcht 5 [`!f g x.
            f continuous at x /\ g continuous at x
            ==> (\x. lift (f x dot g x)) continuous at x`];;
Searching.searcht 5 [`T`];;

module Xx = struct
  open Hales_tactic;;
let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
  `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
            ==> (\x. (f x dot g x)) real_continuous atreal x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  INTRO_TAC CONTINUOUS_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`];
  TYPIFY `(\x. lift ((f o drop) x dot (g o drop) x)) = (\x. lift (f x dot g x)) o drop` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  BY(ASM_REWRITE_TAC[GSYM Xbjrphc.CONTINUOUS_CONTINUOUS_ATREAL])
  ]);;  (* }}} *)
end;;

let CONTINUOUS_LIFT_DOT2 = prove
 (`!net f:A->real^N g.                                                     
        f continuous net /\ g continuous net
        ==> (\x. lift(f x dot g x)) continuous net`,
  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
   [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
  BILINEAR_CONTINUOUS_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;
(*
let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
  `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
            ==> (\x. (f x dot g x)) real_continuous atreal x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  INTRO_TAC CONTINUOUS_AT_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`];
  TYPIFY `(\x. lift ((f o drop) x dot (g o drop) x)) = (\x. lift (f x dot g x)) o drop` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  BY(ASM_REWRITE_TAC[GSYM (* Xbjrphc. *) CONTINUOUS_CONTINUOUS_ATREAL])
  ]);;
  (* }}} *)
*)

module Test = struct
  open Hales_tactic;;
let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
  `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
            ==> (\x. (f x dot g x)) real_continuous atreal x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
  MATCH_MP_TAC CONTINUOUS_LIFT_DOT2;
  ASM_REWRITE_TAC[];
  ]);;  (* }}} *)
end;;


proof_record := [];;

String.length "  REPEAT GEN_TAC;
  ASM_CASES_TAC `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
  ASM_CASES_TAC `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT STRIP_TAC;
  GEXISTL_TAC [`x1`;`x2`];
  BY(GEN_TAC THEN ASM_TAC THEN CONV_TAC REAL_RING)";;

String.length "g/r
asmcs `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`
amt[]
fx mp then rt[] then str/r
asmcs `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1` 
amt[]
fx mp then rt[NOT_FORALL_THM] then str/r
exl [`x1`;`x2`]
g then asm then cvc REAL_RING";;

233.0 /. 414.0;;


(* BUGGY BEHAVIOR *)
can (term_match [] `((f:A->B) ((v:num->A) 2))`) `((f:A->B) ((v:num->A) 7))`;;

can (term_match [] `(f:num->A) 2`) `(f:num->A) 7`;;

run
  {
    idv="test";
    doc = "";
    tags=[];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2 * h0);
	 (&2,y2,&2 * h0);
	 (&2,y3,&2 * h0);
	 (#3.42,y4,#3.42);
	 (&2,y5,#3.01);
	 (&2,y6,&2)]
      
      ((dih_y y1 y2 y3 y4 y5 y6  > pi / &2) ) `;
  };;

run
  {
    idv="test";
    doc = "";
    tags=[];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2 * h0);
	 (&2,y2,&2 * h0);
	 (&2,y3,&2 * h0);
	 (#3.01,y4,#3.42);
	 (&2,y5,#3.01);
	 (#3.01,y6,#3.9)]
      
      ((delta_y y1 y2 y3 y4 y5 y6  > &0)  \/
      arclength y1 y2 y6 > #2.8) `;
  };;

Sphere.h0;;

let s = "test";;
Ineq.getexact "test";;
let v1 = hd(Ineq.getexact s);;
let v2 = List.length (fst (strip_forall (v1.ineq)));;

(* analysis of cases with more than 6 variables *)

let numvars s = 
  let v1 = hd (Ineq.getexact s) in
    List.length (fst (strip_forall (v1.ineq)));;

let ineqnames = map (fun idq -> idq.idv) (!Ineq.ineqs);;

filter (fun s -> numvars s > 6) ineqnames;;
    
let manyvars = ["9507202313"; "4680581274 delta issue"; "4680581274 a"; "9563139965D";
   "3862621143 revised"; "4240815464 a"; "6944699408 a"; "7043724150 a"];;

map numvars manyvars;;


1;;

map (fun t -> t.idv) (Ineq.getfield Onlycheckderiv1negative);;

map (fun t -> t.idv) (filter (fun t -> Optimize.has_cross_diag (t.ineq)) !Prep.prep_ineqs);;
 ["7043724150 a"; "6944699408 a"; "4240815464 a"; "3862621143 revised";
   "4680581274"; "4680581274 delta issue"; "7697147739";
   "7697147739 delta issue"; "9507202313"];;
2;;

Ineq.getexact "4680581274 a";;

run2 {ineq =
     `!y1 y2 y3 y4 y5 y6 y7 y8 y9.
          ineq
          [ #2.0,y1,&2 * h0;  #2.0,y2,&2 * h0;  #2.0,y3,&2 * h0;  #3.01,
                                                                 y4,
                                                                  #3.166; 
           #2.0,
          y5,
          &2;  #2.0,y6,&2;  #2.0,y7,&2 * h0;  #2.0,y8,&2;  #3.01,y9, #3.01]
          (tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 >  #0.513 \/
           delta_y y1 y2 y3 y4 y5 y6 < &10 \/
           delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
           enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 <  #3.01)`;
    idv = "test 4680581274 a";
    doc =
     "quad case both diags > 3.01, y9 long.\n   4559601669 gives the gratuitous delta4_y disjunct.\n   May 23, changed delta4 constant from -11.2 to 0.\n   2013-05-05, 0.696 -> 0.616.";
    tags =
     [Flypaper ["FHOLLLW"]; Main_estimate; Cfsqp; Quad_cluster 10000.0;
      Xconvert; Tex; Penalty (50., 5000.)]};;

module Am = Pervasives;;

let (x0,z0) =  ([0.0;0.0;0.0],[1.0;4.0;3.0]);;
let avoid0 =  [];;
  let w0 = map (fun (xi,zi) -> zi -. xi) (zip x0 z0);;
  let avoid_filter = map (fun i -> (mem i avoid0)) (0--(List.length x0 - 1));;
  let w' = map (fun (t,b) -> if b then 0.0 else t) (zip w0 avoid_filter);;
  let wm = maxlist w' ;;
    index wm w';;

let arclength_lt_1553 = prove_by_refinement(
  `&2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2) (sqrt(#15.53))`,
  (* {{{ proof *)
  [
  REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
  REWRITE_TAC[arith `x + &2 - &2 = x`];
  REWRITE_TAC[Sphere.h0];
  TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    CONJ_TAC;
      BY(REAL_ARITH_TAC);
    MATCH_MP_TAC REAL_LT_LSQRT;
    BY(REAL_ARITH_TAC);
  TYPIFY_GOAL_THEN `&0 < &2 + &2 *  #1.26 - &2 /\  &0 < &2 + &2 - &2 *  #1.26 /\ &0 < &2 + &2 + &2 *  #1.26 /\ &0 < &2 + sqrt  #15.53 - &2 /\ &0 < &2 + &2 - sqrt  #15.53 /\ &0 < &2 + &2 + sqrt  #15.53 /\ &0 < sqrt  #15.53 /\ &0 < &2 *  #1.26` (unlist REWRITE_TAC);
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  MP_TAC (Flyspeck_constants.calc `&2 * (pi / &2 +  atn  (((&2 *  #1.26) * &2 *  #1.26 - &2 * &2 - &2 * &2) /   sqrt   ((&2 + &2 + &2 *  #1.26) *    (&2 + &2 - &2 *  #1.26) *    (&2 + &2 *  #1.26 - &2) *    &2 *     #1.26))) < pi / &2 + atn ((sqrt  #15.53 * sqrt  #15.53 - &2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 + sqrt  #15.53) *   (&2 + &2 - sqrt  #15.53) *   (&2 + sqrt  #15.53 - &2) *   sqrt  #15.53))` );
  BY(REWRITE_TAC[])
  ]);;  (* }}} *)


run
  {
    idv="testA";
    doc = "";
    tags=[];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2);
	 (&2,y2,&2);
	 (&2,y3,&2);
	 (#3.01,y4,#3.01);
	 (#3.01,y5,#3.01);
	 (&2,y6,#2.52)]      
      ((dih_y y1 y2 y3 y4 y5 y6  > pi / &2) ) `;
  };;



run2
  {
    idv="test 1348932091"; (* was "testB"; *)
    doc = "";
    tags=[Main_estimate;Cfsqp;Tex;Xconvert];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2);
	 (&2,y2,#2.52);
	 (&2,y3,#2.52);
	 (#2.52,y4,#2.52);
	 (#3.01,y5,#3.3);
	 (&2,y6,#2.52)]      
      ((dih_y y1 y2 y3 y4 y5 y6  < #1.4) ) `;
  };;


run
  {
    idv= "test 5557288534"; (* was "testC"; *)
    doc = "";
    tags=[Main_estimate;Cfsqp;Tex;Xconvert];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2);
	 (&2,y2,#2.52);
	 (&2,y3,#2.52);
	 (#3.01,y4,#3.01);
	 (#3.01,y5,#3.3);
	 (&2,y6,#2.52)]      
      ((dih_y y1 y2 y3 y4 y5 y6  < #1.7) ) `;
  };;

needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
needs "../formal_lp/hypermap/computations/list_hypermap_computations.hl";;

needs "../formal_lp/hypermap/verify_all.hl";;
Verify_all.init_ineqs();;
let result = Verify_all.verify_file (flyspeck_dir ^"/../formal_lp/glpk/binary/easy_onepass_1.dat");;
hd (fst result);;

(*
val it : thm = lp_ineqs, lp_main_estimate,
  iso (hypermap_of_fan (V,ESTD V))
  (hypermap_of_list
  [['0; '1; '2; '3]; ['0; '3; '4; '5]; ['4; '3; '6; '7]; ['6; '3; '2]; ['1; '0; '8; '9]; ['8; '0; '5]; ['2; '1; '10]; ['10; '1; '9]; ['6; '2; '10]; ['5; '4; '11]; ['11; '4; '7]; ['7; '6; '12]; ['12; '6; '10]; ['8; '5; '11]; ['9; '8; '13]; ['13; '8; '11]; ['12; '10; '9]; ['12; '9; '13]; ['13; '11; '7]; ['7; '12; '13]])
  |- contravening V ==> F
*)
type_of `hypermap_of_fan`;;
type_of `hypermap_of_list`;;
result;;
hd(fst result);;
type_of `['0;'1;'2]`;;

run2f (hd(Ineq.getexact "7550003505 0 1 3"));;

Print_types.get_const_types;;




let tab = 
[`norm2hh (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
     norm2hh_x x1 x2 x3 x4 x5 x6 `;  
`rad2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
     rad2_x x1 x2 x3 x4 x5 x6 `;  
`delta4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
     delta_x4 x1 x2 x3 x4 x5 x6 `;  
`delta4_y (sqrt x7) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x8) (sqrt x9) = 
   delta_x4 x7 x2 x3 x4 x8 x9 `; 
`dih2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
     dih2_x x1 x2 x3 x4 x5 x6 `;  
`dih3_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
    dih3_x x1 x2 x3 x4 x5 x6 `;  
`dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
     dih_x x1 x2 x3 x4 x5 x6 `;  
`dih4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
    dih4_x x1 x2 x3 x4 x5 x6 `;  
`dih5_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
   dih5_x x1 x2 x3 x4 x5 x6 `;  
`dih6_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
   dih6_x x1 x2 x3 x4 x5 x6 `;  
`delta_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
   delta_x x1 x2 x3 x4 x5 x6 `; 
`delta_y (sqrt x7) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x8) (sqrt x9) =
   delta_x x7 x2 x3 x4 x8 x9`;
`vol_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
   vol_x x1 x2 x3 x4 x5 x6 `;  
`eta_y (sqrt x1) (sqrt x2) (sqrt x6) pow 2 = eta2_126 x1 x2 x3 x4 x5 x6 `;  
`eta_y (sqrt x1) (sqrt x3) (sqrt x5) pow 2 = eta2_135 x1 x2 x3 x4 x5 x6 `;  
`eta_y (sqrt x4) (sqrt x5) (sqrt x6) pow 2 = eta2_456 x1 x2 x3 x4 x5 x6 `;  
`vol3f (sqrt x1) (sqrt x2) (sqrt x6)  sqrt2 lfun = vol3f_x_lfun x1 x2 x3 x4 x5 x6 `;  
`vol_y sqrt2 sqrt2 sqrt2 (sqrt x1) (sqrt x2) (sqrt x6)  = vol3_x_sqrt x1 x2 x3 x4 x5 x6 `;  
`vol3f_sqrt2_lmplus (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)      (sqrt x6) =
   vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6`;
 ];;

let tab1 = List.nth tab 0;;
fst (strip_comb (fst(dest_eq tab1)));;