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