development/thales/session/scratch.hl

   1 #print_length 50;;
   2
   3 flyspeck_needs "../glpk/minorlp/tame_table.ml";;
   4 let process_exec = Preprocess.exec();;
   5 flyspeck_needs "nonlinear/prep.hl";;
   6
   7 flyspeck_needs "computational_build.hl";;
   8 Preprocess.prep_file;;
   9
  10
  11
  12
  13 Tame_table.execute();;
  14
  15 flyspeck_needs "usr/thales/hales_tactic.hl";;
  16 flyspeck_needs "general/debug.hl";;
  17 flyspeck_needs "volume/vol1.hl";;
  18 flyspeck_needs "hypermap/bauer_nipkow.hl";;
  19 needs "Multivariate/convex.ml";;
  20 rflyspeck_needs "local/polar_fan.hl";;
  21 rflyspeck_needs "local/lp_details.hl";;
  22 flyspeck_needs "local/polar.hl";;
  23 flyspeck_needs "local/localization.hl";;
  24 flyspeck_needs "local/local_lemmas1.hl";;
  25 flyspeck_needs "packing/YSSKQOY.hl";;
  26 flyspeck_needs "packing/counting_spheres.hl";;
  27 rflyspeck_needs "jordan/refinement.hl";;
  28 rflyspeck_needs "jordan/parse_ext_override_interface.hl";;
  29 rflyspeck_needs "jordan/real_ext.hl";;
  30 rflyspeck_needs "jordan/taylor_atn.hl";;
  31 rflyspeck_needs "jordan/parse_ext_override_interface.hl";;
  32 flyspeck_needs "general/print_types.hl";;
  33
  34 flyspeck_needs "local/RRCWNSJ.hl";;
  35 flyspeck_needs "local/JCYFMRP.hl";;
  36 flyspeck_needs "local/TFITSKC.hl";;
  37 flyspeck_needs "local/CQAOQLR.hl";;
  38 flyspeck_needs "local/JLXFDMJ.hl";;
  39 flyspeck_needs "leg/geomdetail.hl";;
  40 flyspeck_needs "local/local_lemmas1.hl";;
  41
  42
  43 flyspeck_needs "local/ARDBZYE.hl";;
  44 flyspeck_needs "local/AUEAHEH.hl";;
  45 flyspeck_needs "local/VASYYAU.hl";;
  46 flyspeck_needs "local/MIQMCSN.hl";;
  47 flyspeck_needs "local/JEJTVGB.hl";;
  48
  49 flyspeck_needs "local/yxionxl.hl";;
  50 flyspeck_needs "local/ODXLSTCv2.hl";;
  51 flyspeck_needs "local/ZLZTHIC.hl";;
  52 flyspeck_needs "local/lunar_deform.hl";;
  53 Lunar_deform.MHAEYJN;;
  54 flyspeck_needs "local/NUXCOEA.hl";;
  55 flyspeck_needs "packing/Oxl_def.hl";;
  56 flyspeck_needs "packing/Oxl_2012.hl";;
  57
  58
  59 let fn = flyspeck_needs;;
  60 fn "local/appendix_main_estimate.hl";;
  61 fn       "local/ODXLSTCv2.hl";;
  62 fn       "local/IMJXPHR.hl";;
  63 fn       "local/NUXCOEA.hl";;
  64 fn       "local/FEKTYIY.hl";;
  65 fn       "local/AURSIPD.hl";;
  66 fn       "local/PPBTYDQ.hl";;
  67 fn       "local/AXJRPNC.hl";;
  68 fn "local/YRTAFYH.hl";;
  69 fn       "local/WKEIDFT.hl";;
  70 fn        "local/hexagons.hl";;
  71        fn "local/OTMTOTJ.hl";;
  72        fn "local/HIJQAHA.hl";;
  73        fn "local/CNICGSF.hl";;
  74 fn "local/BKOSSGE.hl";;
  75 fn "local/IUNBUIG.hl";;
  76 flyspeck_needs "local/JOTSWIX.hl";;
  77
  78 flyspeck_needs "local/IUNBUIG.hl";;
  79
  80
  81 flyspeck_needs "local/";;
  82 Yxionxl2
  83 flyspeck_needs "general/flyspeck_lib.hl";;
  84 flyspeck_needs "local/Xivphks.hl";;
  85 flyspeck_needs   "local/EYYPQDW.hl";; (* 2013-07-08 *)
  86 flyspeck_needs   "local/IMJXPHR.hl";;
  87 Imjxphr.ZLZTHICv1_concl;;
  88 Appendix.ZLZTHIC_concl;;
  89 Imjxphr.IMJXPHR;;
  90 State_manager.neutralize_state();;
  91 rflyspeck_needs "nonlinear/lemma.hl";;
  92 rflyspeck_needs "nonlinear/functional_equation.hl";;
  93 Ineq.ineqs:= [];;
  94 rflyspeck_needs "nonlinear/ineq.hl";;
  95 rflyspeck_needs   "nonlinear/main_estimate_ineq.hl";;
  96 rflyspeck_needs  "nonlinear/parse_ineq.hl";;
  97 rflyspeck_needs "nonlinear/optimize.hl";;
  98 rflyspeck_needs "general/flyspeck_lib.hl";;
  99 rflyspeck_needs   "nonlinear/function_list.hl";;
 100 rflyspeck_needs "nonlinear/auto_lib.hl";;
 101 rflyspeck_needs "nonlinear/scripts.hl";;
 102 Scripts.execute_interval_all false;;
 103 Scripts.execute_cfsqp();;
 104 let cfsqp_out = it;;
 105 cfsqp_out;;
 106 Scripts.one_cfsqp  "QZECFIC wt0";;
 107 Scripts.cfsqp ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";"QZECFIC wt1";"QZECFIC wt2 A"];;
 108 Scripts.cfsqp ["IXPOTPA"; "GRKIBMP B V2"; "7796879304"; "8346775862"];;
 109 ;;
 110
 111 List.length !Ineq.ineqs;;
 112
 113 let idvs = Flyspeck_lib.nub (sort (<) (map (fun t -> t.idv) (!Ineq.ineqs)));;
 114 List.length idvs;;
 115
 116 flyspeck_needs "nonlinear/calc_derivative.hl";;
 117 flyspeck_needs "nonlinear/merge_ineq.hl";;
 118 rflyspeck_needs "nonlinear/scripts.hl";;
 119 (* Scripts.execute_interval_all true;; (* takes several hours *) *)
 120 Scripts.unfinished_cases();;
 121 let reruns = ["6843920790"; (* "9563139965D" ; *) "6944699408 a reduced"; "6944699408 a";
 122    "7043724150 a reduced v2"; "7043724150 a"; "8055810915"; "1965189142 34";
 123    "TSKAJXY-eulerA"];;
 124 map (Auto_lib.testsplit true) ["8055810915"];;
 125
 126
 127 Scripts.times;;
 128 Scripts.hour (Scripts.total Scripts.times);;
 129 Scripts.case_splits_execute;;
 130
 131 let redo (s,cs,t) =
 132   let rg = 0--(t-1) in
 133   let cs' = subtract rg cs in
 134     map (fun c -> (s,c,t)) cs';;
 135
 136 let redos = List.flatten (map redo incompletes);;
 137
 138
 139 (!Prep.prep_ineqs);;
 140
 141
 142 map (test_prep_case_split true) redos;;
 143
 144
 145 test_prep_case true 1 2 "GRKIBMP A V2";;
 146
 147 Auto_lib.testsplit true "GRKIBMP A V2";;
 148
 149 let some_cases = filter (fun (_,t) -> t > 300) Scripts.times;;
 150 let some_cases = filter (fun (_,t) -> t > 120) times;;
 151 total some_cases;;
 152 assoc "3862621143 revised" times;;
 153 assoc "7043724150 a" times;;
 154 assoc "9507202313" times;;
 155
 156 Scripts.hour (Scripts.total some_cases);;
 157 List.length some_cases;;
 158 783.0 /. 60.0;;
 159
 160 flyspeck_needs "general/flyspeck_lib.hl";;
 161 flyspeck_needs "../glpk/glpk_link.ml";;
 162 flyspeck_needs "../glpk/minorlp/OXLZLEZ.ml";;
 163      "local/UAGHHBM.hl";;
 164 flyspeck_needs "packing/oxl_def.hl";;
 165 flyspeck_needs "packing/oxl_2012.hl";;
 166 flyspeck_needs "packing/OXLZLEZ.hl";;
 167 Oxlzlez.PACKING_CHAPTER_MAIN_CONCLUSION;;
 168
 169 Mk_all_ineq.example2;;
 170 Mk_all_ineq.exec();;
 171 rflyspeck_needs "../projects_discrete_geom/bezdek_reid/bezdek_reid.hl";;
 172 let filter_edge_bak = Bezdek_reid.filter_edge;;
 173
 174 1;;
 175 Bezdek_reid.test_edge;;
 176 Bezdek_reid.test_triplet;;
 177 zip;;
 178 flyspeck_needs "../glpk/glpk_link.ml";;
 179 rflyspeck_needs "../projects_discrete_geom/fejestoth12/lipstick_ft.ml";;
 180 List.length Bezdek_reid.filter_triplet;;
 181 List.length (filter (fun (a,_,_) -> (a =[])) Bezdek_reid.coord_triplet);;
 182 let test = ref "";;
 183
 184 flyspeck_needs "nonlinear/check_completeness.hl";;
 185   let check_completeness_out = Check_completeness.execute();;
 186
 187 rflyspeck_needs   "nonlinear/types.hl";;
 188 rflyspeck_needs   "nonlinear/nonlin_def.hl";;
 189 rflyspeck_needs   "nonlinear/ineq.hl";;
 190 rflyspeck_needs   "nonlinear/mdtau.hl";;
 191 rflyspeck_needs   "nonlinear/main_estimate_ineq.hl";;
 192 rflyspeck_needs   "nonlinear/lemma.hl";;  (* needs trig1, trig2 *)
 193 rflyspeck_needs   "nonlinear/functional_equation.hl";;
 194 rflyspeck_needs   "nonlinear/parse_ineq.hl";;
 195 rflyspeck_needs   "nonlinear/optimize.hl";;
 196 rflyspeck_needs   "nonlinear/function_list.hl";;
 197 rflyspeck_needs   "nonlinear/auto_lib.hl";;
 198 rflyspeck_needs "nonlinear/scripts.hl";;
 199 flyspeck_needs "local/XBJRPHC.hl";;
 200
 201
 202 (* Formal LP verification *)
 203 needs "../formal_lp/hypermap/verify_all.hl";;
 204 let result = Verify_all.verify_all();;
 205 Verify_all.test_result result;;
 206 List.length result;;
 207 List.length (List.flatten (map fst result));;
 208 List.nth result 77;;
 209 (73386.0 /. 3600.0);;
 210
 211
 212 (*
 213
 214 Issues:
 215
 216 The zip file unpacked to glpk/binary/lp_certificates/.
 217 I had to move the files to glpk/binary/
 218
 219 The directory glpk/binary/ has hiddedn files .DS_Store and .svn
 220 Verify_all.verify_all() tried:
 221 Verifying /Users/thomashales/Desktop/googlecode/flyspeck/text_formalization/../formal_lp/glpk/binary/.DS_Store
 222 and threw an exception.
 223
 224 *)
 225
 226
 227   open Pent_hex;;
 228   open Optimize;;
 229 flyspeck_needs "../development/thales/session/local_defs.hl";;
 230 flyspeck_needs "../development/thales/session/interval_args.hl";;
 231 flyspeck_needs "../development/thales/session/2app.hl";;
 232
 233 (* Local materials *)
 234 Ineq.ineqs:= [];;
 235 rflyspeck_needs "nonlinear/ineq.hl";;
 236 rflyspeck_needs   "nonlinear/main_estimate_ineq.hl";;
 237 List.length !Ineq.ineqs;;
 238 flyspeck_needs "local/appendix_main_estimate.hl";;
 239
 240
 241    rflyspeck_needs "local/appendix_main_estimate.hl";;
 242    flyspeck_needs "local/terminal.hl";;
 243
 244 flyspeck_needs "local/lunar_deform.hl";;
 245
 246 flyspeck_needs "local/terminal.hl";;
 247 flyspeck_needs "local/pent_hex.hl";;
 248 flyspeck_needs "local/OCBICBY.hl";;
 249 flyspeck_needs "local/YXIONXL2.hl";;
 250 flyspeck_needs "local/XIVPHKS.hl";;
 251 flyspeck_needs "local/ZLZTHIC.hl";;
 252 flyspeck_needs "local/PQCSXWG.hl";;
 253 flyspeck_needs "local/CUXVZOZ.hl";;
 254   open Cuxvzoz;;
 255
 256 flyspeck_needs "../development/thales/session/work_in_progress.hl";;
 257
 258   open Work_in_progress;;
 259
 260
 261 let strip_id s =
 262   let ss = Str.split (Str.regexp "[],[]") s in
 263     (hd ss,map int_of_string (tl ss));;
 264
 265 strip_id "abc[0,1,2,3]";;
 266
 267 0.0659/. 0.042;;
 268
 269
 270 module Temp =  struct
 271   open Sphere;;
 272   open Ineq;;
 273 add
 274 {
 275   idv="2485876245b";
 276   doc="Used in some quad calculations to show that a node
 277    is not straight (both halves are acute)";
 278   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex];
 279   ineq = all_forall `ineq [
 280     (&2,y1,#2.52);
 281     (&2,y2,#2.52);
 282     (&2,y3,#2.52);
 283     (&2,y4,#2.52);
 284     (#3.01,y5, &2 * #2.52);
 285       (&2,y6,#3.01)
 286   ]
 287 ((delta4_y y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
 288 };;
 289 end;;
 290
 291 let ztg4s = map (fun t -> t.idv) (Ineq.getprefix "ZTGIJCF4");;
 292 cfsqp ztg4s;;
 293
 294 module Test = struct
 295   open Ineq;;
 296   open Sphere;;
 297 add
 298 {
 299   idv = "test QITNPEA 3848804089";
 300   ineq = all_forall `ineq
 301    [(&2 * hminus,y1, &2 * hplus);
 302     (&2,y2, &2 * hminus);
 303     (&2,y3, &2 * hminus);
 304     (#2 ,y4, &2 * hminus);
 305     (&2,y5, &2 * hminus);
 306     (&2,y6, &2 * hminus)
 307    ]
 308     ((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 )) `;
 309   doc =   "
 310      This is an inequality for quarters used to prove the cluster inequality.";
 311   tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
 312 };;
 313 add
 314 {
 315   idv = "MMGKNVE";
 316   ineq = all_forall `ineq
 317    [(&2 * hminus,y1, &2 * hplus);
 318     (&2,y2, &2 * hminus);
 319     (&2,y3, &2 * hminus);
 320     (&2,y4, &2 * hminus);
 321     (&2,y5, &2 * hminus);
 322     (&2,y6, &2 * hminus)
 323    ]
 324     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0539
 325       - #0.042*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
 326     (eta_y y1 y2 y6 pow 2 < #1.34 pow 2 ))`;
 327   doc =   "
 328      This is an inequality for quarters used to prove the cluster inequality.";
 329   tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ"];Clusterlp;Tex;Xconvert;Branching;Split[0]];
 330 };;
 331 add
 332 {
 333   idv = "test BIXPCGW 9455898160";
 334   ineq = all_forall `ineq
 335    [(&2 * hminus, y1, #2.6);
 336     (&2,y2, &2 * hminus);
 337     (&2,y3, &2 * hminus);
 338     (&2,y4, &2 * hminus);
 339     (&2,y5, &2 * hminus);
 340     (&2,y6, &2 * hminus)
 341    ]
 342    (
 343     gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) `;
 344   doc =   "
 345      If $X$ is a quarter, then $\\gamma(X,L)\\ge -0.00569$.";
 346   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 347 };;
 348 add
 349 {
 350   idv = "test ratio2";
 351   ineq = all_forall `ineq
 352    [(&2 * hminus, y4, &2 * hplus);
 353     (&2  ,y5, sqrt8);
 354     (&2 ,y6, sqrt8)
 355    ]
 356    ( truncate_gamma3f_x (#0.001) (h0cut y4) (h0cut y5) (h0cut y6) (&2) (&2) (&2) (y4*y4) (y5*y5) (y6*y6) /
 357        (&1* dih_y y4 y5 sqrt2 sqrt2 sqrt2 y6) > &0 \/
 358        eta_y y4 y5 y6 > sqrt2 - #0.001
 359      \/
 360      eta_y y4 y5 y6 < #1.34
 361    )`;
 362   doc =   "test";
 363   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 364 };;
 365 add
 366 {
 367   idv = "test gamma23";
 368   ineq = all_forall `ineq
 369    [(&2 * hminus, y1, &2 * hplus);
 370     (&2,y2, &2 * hminus);
 371     (&2,y3, &2 * hminus);
 372     (&2,y4, sqrt8);
 373     (&2,y5, &2 * hminus);
 374     (&2,y6, &2 * hminus)
 375    ]
 376    (
 377 y_of_x (truncate_gamma3f_x #0.0 (h0cut y1) (&1) (&1)) (&0) (&0) (&0) y1 y2 y6  +
 378 y_of_x (truncate_gamma3f_x #0.0 (h0cut y1) (&1) (&1)) (&0) (&0) (&0) y1 y3 y5  +
 379      (dih_y y1 y2 y3 y4 y5 y6 -
 380       (dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 381        dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2)) * #0.008  > &0 \/
 382      rad2_y y1 y2 y3 y4 y5 y6 < &2 \/
 383      eta_y y1 y2 y6 > #1.34 \/
 384      eta_y y1 y3 y5 > #1.34 \/
 385     dih_y y1 y2 y3 y4 y5 y6 < #1.946 \/
 386     dih_y y1 y2 y3 y4 y5 y6 > #2.089)`;
 387   doc =   "test";
 388   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 389 };;
 390 add
 391 {
 392   idv = "test gamma23bis";
 393   ineq = all_forall `ineq
 394    [(&2 * hminus, y1, &2 * hplus);
 395     (&2,y2, sqrt8);
 396     (&2,y3, &2 * hminus);
 397     (&2,y4, sqrt8);
 398     (&2,y5, &2 * hminus);
 399     (&2,y6, sqrt8)
 400    ]
 401    (
 402 y_of_x (truncate_gamma3f_x #0.0 (h0cut y1) (&1) (&1)) (&0) (&0) (&0) y1 y3 y5  +
 403      (dih_y y1 y2 y3 y4 y5 y6 -
 404        dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2) * #0.008  > a_spine5 +
 405      b_spine5 * dih_y y1 y2 y3 y4 y5 y6 \/
 406      rad2_y y1 y2 y3 y4 y5 y6 < &2 \/
 407      eta_y y1 y2 y6 < #1.34 \/
 408      eta_y y1 y2 y6 > sqrt2 \/
 409      eta_y y1 y3 y5 > #1.34 \/
 410     dih_y y1 y2 y3 y4 y5 y6 > #1.074)`;
 411   doc =   "test";
 412   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 413 };;
 414 end;;
 415
 416 add
 417 {
 418   idv = "test";
 419   ineq = all_forall `ineq
 420    [(&2 * hminus, y1, &2 * hplus);
 421     (&2,y2, sqrt8);
 422     (&2,y3, sqrt8);
 423     (&2,y4, sqrt8);
 424     (&2,y5, sqrt8);
 425     (&2,y6, sqrt8)
 426    ]
 427    (
 428     dih_y y1 y2 y3 y4 y5 y6  > &0 \/
 429      rad2_y y1 y2 y3 y4 y5 y6 < &2 \/
 430      eta_y y1 y2 y6 > sqrt2 \/
 431      eta_y y1 y3 y5 > sqrt2 )`;
 432   doc =   "test";
 433   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 434 };;
 435
 436
 437 type_of theorems;;
 438 follow;;
 439 textchar;;
 440 augment_search_results ["hi"];;
 441 really_expand "?-0";;
 442 help_grep "";;
 443 help_flag "";;
 444 help "apropos_short_order_script";;
 445 suggest();;
 446 String.sub "abcde" 1 (String.length "abcde" - 1);;
 447 expand_suggest "0";;
 448 hd it;;
 449 List.nth !loaded_files 69;; Reload 1--69
 450 mk_thm;;
 451 flyspeck_needs "general/lib.hl";;
 452 flyspeck_needs "nonlin/kelvin_lattice.hl";;
 453 flyspeck_needs "usr/thales/searching.hl";;
 454 open Searching;;
 455 rflyspeck_needs "usr/thales/init_search.hl";;
 456 reneeds "packing/counting_spheres.hl";;
 457 flyspeck_needs "packing/QZKSYKG.hl";;
 458 flyspeck_needs "packing/DDZUPHJ.hl";;
 459 flyspeck_needs "packing/AJRIPQN.hl";;
 460 flyspeck_needs "packing/QZYZMJC.hl";;
 461 flyspeck_needs "packing/marchal_cells_3.hl";;
 462 flyspeck_needs "packing/GRUTOTI.hl";;
 463 Grutoti.GRUTOTI;;
 464 flyspeck_needs "fan/CFYXFTY.hl";;
 465 flyspeck_needs "packing/counting_spheres.hl";;
 466 open Counting_spheres;;
 467 flyspeck_needs "nonlinear/cleanDeriv.hl";;
 468 flyspeck_needs "nonlinear/cleanDeriv_examples.hl";;
 469 flyspeck_needs "../development/thales/chaff/tmp/vectors_patch.ml";;
 470 flyspeck_needs "../development/thales/chaff/tmp/determinants_patch.ml";;
 471 flyspeck_needs "../development/thales/chaff/tmp/wlog_patch.hl";;
 472 flyspeck_needs "trigonometry/trig2.hl";;
 473 update_database();;
 474 augment_search_results;;
 475 !search_results;;
 476 Counting_spheres.ORDER_AZIM_SUM2PI;;
 477
 478 let u11111 = ((GOAL_TERM (fun w -> ALL_TAC)):tactic);;
 479 RDISK_R;;
 480
 481 GOAL_TERM (fun w -> (MP_TAC (ISPECL ( envl w [`p`;`v`;`u0`;`b`]) RCONE_PREP)));;
 482
 483 INST [(`u:bool`,`A:bool`)] (TAUT ` ((A ==> B) /\ A) ==> B`);;
 484
 485 let thh = Collect_geom.EQ_POW2_COND;;
 486 let ta1 = TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`;;
 487 let th2 = REWRITE_RULE[ta1] ( thh);;
 488 let tm1 = snd (strip_forall (concl th2));;
 489 let tm2 = snd (dest_imp tm1);;
 490 let tm3 = fst (dest_eq tm2);;
 491 let force_rewrite th;;
 492
 493
 494
 495 let goalx = `&0 <= sqrt x /\ &0 <= sqrt t ==> &0 <= sqrt u`;;
 496 GMATCH_SIMP_TAC SQRT_POS_LE;;
 497
 498 let (asl,w) = (top_realgoal());;
 499 let thm = SQRT_POS_LE;;
 500   let thm' = hd (mk_rewrites true thm []);;
 501   let t1 = fst (dest_eq(snd (dest_imp(concl(thm'))))) ;;
 502   let matcher u t =
 503     let m = term_match [] t1 t in
 504     let _ = subset (frees t) (frees u) or failwith "" in
 505       m ;;
 506   let wsub u = find_term (can (matcher u)) u ;;
 507   let w' = wsub w ;;
 508   let vv =
 509     let var1 = mk_var("v",type_of w') in
 510       variant (frees w) var1 ;;
 511   let athm = REWRITE_CONV[ ASSUME (mk_eq (w',vv))] w ;;
 512   let arhs = rhs (concl athm) ;;
 513   let bthm = (ISPECL [mk_abs(vv,arhs);w'] BETA_THM) ;;
 514   let betx = SYM(TRANS bthm (BETA_CONV (rhs (concl bthm)))) ;;
 515    ONCE_REWRITE_TAC[betx]
 516   MATCH_MP_TAC (lift_eq thm')
 517      BETA_TAC
 518  THEN BETA_TAC);;
 519 rt[]
 520
 521
 522 let lift_SQRT_POS_LE = GEN_ALL (MATCH_MP lift_imp (SPEC_ALL SQRT_POS_LE));;
 523
 524 add_rewrite_tag("mycase ",th);;
 525 let xxx n = add_rewrite_stag (List.nth search_result_dump_march7_8am n);;
 526 xxx 0;;
 527 assoc (List.nth search_result_dump_march7_8am 0) !theorems;;
 528
 529 !rewrite_tags;;
 530 let th = ASSUME (`!p q r. p ==> q ==> (cos r = s) /\ (u ==> sin y > &1)`);;
 531
 532 let gexp = `!t. (cos x + sqrt (t pow 2) > &0)`;;
 533 let hexp = `!x. (cos x + sqrt (t pow 2) > &0)`;;
 534
 535
 536 mk_rewrites;;
 537
 538
 539 let matcherx u t =
 540   let m = term_match [] t1 t in
 541   let _ = subset (frees t) (frees u) or failwith "" in
 542     m;;
 543 let mmat u = find_term (can (matcherx u)) u;;
 544 let mx = mmat hexp;;
 545 let mma1 = term_match [] `sqrt x` (mmat hexp);;
 546 let vv =
 547   let var1 = mk_var("v",type_of mx) in
 548     variant (frees hexp) var1;;
 549 let rrx = REWRITE_CONV[ ASSUME (mk_eq (mx,vv))] hexp;;
 550 let rhsx = rhs (concl rrx);;
 551 let bthx = (ISPECL [mk_abs(vv,rhsx);mx] BETA_THM);;
 552 let betx = SYM(TRANS bthx (BETA_CONV (rhs (concl bthx))));;
 553
 554 term_match [] `sqrt x` mmat;;
 555
 556 st_of  `sin x + cos (asn t)`;;
 557 mk_prover;;
 558 net_of_thm;;
 559 help "term_match";;
 560 help "find_term";;
 561 help "GEN_PART_MATCH";;
 562 help "PART_MATCH";;
 563 help "MATCH_MP";;
 564 `(&0 <= sqrt (t pow 2)) \/ b ==> ~(&0 <= sqrt u)`
 565 mmp lift_SQRT_POS_LE
 566 rt[]
 567 SPEC_ALL (ASSUME `!x. x = x`);;
 568 let lift_SQRT_POS_LE = GEN_ALL (MATCH_MP lift_imp (SPEC_ALL SQRT_POS_LE));;
 569 searcht 5 [`&0 <= sqrt x`];;
 570
 571 eval_command ~silent:true "let x111 = 1+1+4";;
 572 x111;;
 573 eval_command ~silent:false "mark 4";;
 574 mark 4;;
 575 snd it;;
 576 help_grep "match";;
 577 help "term_match";;
 578 help "PART_MATCH";;
 579 find_term;;
 580 help "find_term";;
 581 List.map hd (split_proof_record [] [] (!proof_record));;
 582 term_match;;
 583 help "term_match";;
 584 searchl;;
 585
 586 retrieve_search;;
 587 thm_counts;;
 588
 589
 590 eval_tactic_lines "st/r\nfxa mpt";;
 591 text_char;;
 592
 593
 594 process_to_string "date";;
 595 gax();;
 596
 597
 598 last (show_gax());;
 599 List.nth (show_gax()) 2;;
 600
 601 Clean_deriv.x1_eta2;;
 602 axioms();;
 603 type_of `( %% )`;;
 604 Qzyzmjc.QZYZMJC;;
 605 search [name "FMSWMVO"];;
 606 search [name "IVFICRK"];;
 607 search [name "volume_props"];;
 608 stm_depth "T";;
 609 (* PROJECT BUILD *)
 610 Hashtbl.hash;;
 611
 612   (*
 613   let (d,hd) = data (get_tm_depth w) in
 614     filter (fun ((d',hd'),_,_) -> (((abs (d-d')< 1+k)  && sorted_meet 0 hd hd' ))) thml;;
 615   *)
 616
 617 List.length (ballpark_theorems   (top_realgoal()));;
 618  (ballpark_theorems   (top_realgoal()));;
 619 abs_of_float;;
 620 int_abs;;
 621 last [0;1;2;3];;
 622 strip_imp `a`;;
 623 strip_imp `a ==> b==> c`;;
 624 help_grep "dest_";;
 625 type_of `==>`;;
 626 strip_comb;;
 627 help_grep "strip";;
 628 is_comb;;
 629 help "strip_exists";;
 630 strip_comb `a ==> b==> c`;;
 631 help_grep "comb";;
 632 help "strip_ncomb";;
 633 help_grep "strip";;
 634
 635
 636 let nearest_thm_to_goal thml (asl,w) =
 637   let tt tl = List.flatten (map (tm_depth o concl) tl) in
 638   let common = tt (map snd asl) in
 639   let thl = map (fun (s,t) -> ((tm_depth o snd o strip_forall o concl )t,s,t) ) thml in
 640   let r = map (fun (tl,s,t) -> (tl,s,t,msd 0.0 common (tm_depth w) tl)) thl in
 641     (sort (fun (_,_,_,a) (_,_,_,b) -> a < b) r);;
 642
 643 let thml_depth_of_goalmatch thml (asl,w) =
 644   let tt tl = List.flatten (map (tm_depth o concl) tl) in
 645   let w'::rest = List.rev strip_imp o  snd o strip_forall w in
 646   let common = tt ((map snd asl) @ rest) in
 647   let thl = map (fun (s,t) -> ((tm_depth o snd o strip_forall o concl )t,s,t) ) thml in
 648   let
 649 ;;
 650
 651
 652
 653 nearest_thm_to_goal (ballpark_theorems (top_realgoal())) (top_realgoal());;
 654 let guess = nearest_thm_to_goal (top_realgoal());;
 655 List.length !theorems;;
 656
 657 top_realgoal;;
 658 help_grep "goal";;
 659 (* *)
 660
 661 tt;;
 662 hd (!theorems);;
 663 tt;;
 664 strip_forall;;
 665 help_grep "strip";;
 666
 667 (* jan 3, 2012 chaff *)
 668
 669
 670
 671 (* USEFUL CONSTRUCTS *)
 672
 673 let report s =
 674   Format.print_string s; Format.print_newline();;
 675
 676 g `?(x:A) . f A`
 677
 678 (* generalize *)
 679
 680 let ( TYPE_VAR :string -> (term -> tactic) -> tactic) =
 681     fun s tm_tactic (asl,g) ->
 682       let (_,r) = dest_comb g in
 683       let (v,_) = dest_abs r in
 684       let (_,ty) = dest_var v in
 685         tm_tactic (mk_var(s,ty)) (asl,g);;
 686
 687 TYPE_VAR "x" EXISTS_TAC;
 688 ;;
 689 Format.print_flush();;
 690 FINITE_EMPTY;;
 691
 692 searcht 10 [`eulerA_hexall_x`];;
 693
 694 Sphere.num_combo1;;
 695
 696 (*
 697 process_to_string "cat qed_log.txt | sed  's/^.*ineq./\"/' | sed 's/., secs.*$/\";/'  "
 698
 699 cat qed_log.txt | sed  's/^.*ineq./"/' | sed 's/., secs.*$/";/' | sort -u | wc
 700
 701 (*
 702 let _ = Sys.command("cat "^flyspeck_dir^"/../interval_code/qed_log.txt");;
 703 *)
 704 *)
 705
 706
 707 let ee () =
 708   let b = (false or (let _ = Sys.command("date") in failwith "h")) in b;;
 709
 710
 711 suggest();;
 712
 713 EXISTSv_TAC "y";
 714
 715 dest_binder "?" (`?(x:A). f A`);;
 716
 717 (*
 718
 719 let searchl = sortlength_thml o search;;
 720 let take = Lib_ext.take;;
 721 let searcht r = take 0 5 (searchl r);;
 722 let searchtake i j r = take i j (searchl r);;
 723
 724 *)
 725 term_match;;
 726 INSTANTIATE;;
 727   open Searching;;
 728
 729 definitions();;
 730 State_manager.neutralize_state();;
 731 let vv = (eval("1+1")) + 3;;
 732 let vv = (eval("REFL `T`"));;
 733 concl vv;;
 734
 735 prefixes();;
 736 rev(infixes());;
 737 binders();;
 738 unparse_as_infix;;
 739 map (List.nth (infixes())) (95--131);;
 740 unparse_as_binder "!";;
 741 binders();;
 742
 743
 744 find_path ((=) `4`) `(sum (3..4) f)`;;  (* lrr *)
 745
 746 let kill_process n = Sys.command (Printf.sprintf "sudo kill -9 %d" n);;
 747
 748 help_grep "conj";;
 749 help "list_mk_conj";;
 750  end_itlist;;
 751
 752 FROZEN_REWRITE_TAC [REAL_ARITH `b + d = d - (--b)`];;
 753
 754 let goal_types = Print_types.print_goal_types;;
 755 Print_types.goal_types();;
 756 Print_types.print_term_types `#2`;;
 757 Print_types.print_thm_types (REFL `1`);;
 758
 759
 760
 761 (*
 762 (* parsing printing *)
 763 let pterm = Print_types.print_term_types;;
 764 let tterm = Print_types.print_thm_types;;
 765
 766 #install_printer print_qterm;;
 767
 768
 769 #install_printer Goal_printer.print_goal_hashed;;
 770 #install_printer Goal_printer.print_goalstack_hashed;;
 771
 772 #remove_printer Goal_printer.print_goal_hashed;;
 773 #remove_printer Goal_printer.print_goalstack_hashed;;
 774
 775 #print_length 1000;;
 776 *)
 777
 778 search[`f (x:A) (g (y:A) z) = f (g x y) z`];; (* min, max, + /\, \/ *, compose, monoidal ops,
 779    APPEND, a - (b + c) = a - b - c /\ a - (b - c) = a - b + c),
 780     p ==> q ==> r <=> p /\ q ==> r);; *)
 781
 782 find_term  ( can (term_match[ `r a (r y z) = r (r x y) z`])) (concl IMP_IMP);;
 783
 784 filter_pred;;
 785 can (term_match[]);;
 786 type_of;;
 787
 788 constant_of_regexp "at.*[gn]$";;
 789
 790 constant_of_regexp "FILTER";;
 791 searcht 15 [`cos`];;
 792 def_of_string "FILTER";;
 793
 794 def_of_string "fan";;
 795 conjuncts `!a b c. (u /\ v /\ (!c. w /\ r) /\ (!x y. r2 /\ r3))`;;
 796
 797
 798 help "dest_forall";;
 799 List.nth !theorems 0;;
 800
 801 help_grep ".*TAC$";;
 802
 803 INFINITE_DIFF_FINITE;;
 804 search[`INFINITE`;`DIFF`];;
 805
 806
 807 Format.set_max_boxes 100;;
 808 let tt = hol_of_smalllist (1--300);;
 809 string_of_my_term tt;;
 810
 811
 812
 813 let hel i = help (List.nth  tacsss i );;
 814
 815 hel 1;;
 816
 817 constant_of_regexp "sol";;
 818
 819 apropos;;
 820 suggest;;
 821
 822
 823 (* get all word counts in HOL LIGHT and FLYSPECK *)
 824
 825 let match_mp_strip =
 826   fun th ->
 827           let tm = concl th in
 828           let avs,bod = strip_forall tm in
 829           let ant,con = dest_imp bod in
 830           let th1 = SPECL avs (ASSUME tm) in
 831           let th2 = UNDISCH th1 in
 832           let evs = filter (fun v -> vfree_in v ant & not (vfree_in v con))
 833                            avs in
 834           let th3 = itlist SIMPLE_CHOOSE evs (DISCH tm th2) in
 835           let tm3 = hd(hyp th3) in
 836             MP (DISCH tm (GEN_ALL (DISCH tm3 (UNDISCH th3)))) th;;
 837
 838 let mp_short_list =
 839   let u = fst(chop_list 50 (trigger_counts "MATCH_MP_TAC")) in
 840   let sl = map fst !theorems in
 841   let f1 = filter (fun (t,_) -> mem t sl ) u in
 842   let f2 = map (fun (s,n) -> (s,n,assoc s !theorems)) f1 in
 843     filter (fun (_,_,t) -> can  match_mp_strip t) f2;;
 844
 845
 846 let relevant_match_mp r =
 847   filter (fun (_,_,t) -> can (MATCH_MP_TAC t) r) mp_short_list;;
 848
 849 let suggest_match_mp () = relevant_match_mp (top_realgoal());;
 850
 851 mp_short_list;;
 852
 853 tachy"rep";;
 854
 855 tcs;;
 856
 857 grep -r "\bREPEAT\b" . | grep -v svn | sed 's/^.*REPEAT *//' | sed 's/ .*$//g'
 858
 859
 860 let recent_search = ref [""];;
 861
 862 let refcount = ref [("",0)];;
 863
 864 trigger_counts "MATCH_MP_TAC";;
 865
 866 EQ_EXT;;
 867 FINITE_SUBSET;;
 868 search[regexp "EQ_SYM"];;
 869 tachy "amt";;
 870 tachy "asmcase";;
 871
 872 (* to get tacticals as well *)
 873 (* grep "TYPE.*tactic" -i *.doc -l | sed 's/.doc//g' *)
 874
 875 List.length tactic_list;;
 876 List.length(tachy "");;
 877 subtract tactic_list (tachy "");;
 878 tachy "bool";;
 879
 880 help "SUBST1_TAC";;
 881
 882 let typesss ss =
 883   let split =   Str.split (Str.regexp "\n") in
 884   let cmd s = process_to_string ("(cd "  ^s^  "; grep TYPE "^ss^".doc | sed 's/TYPE[^{]*//g' )") in
 885   List.flatten (map ( split o cmd ) (!helpdirs));;
 886
 887 typesss "ALL_TAC";;
 888 help "SUBST1_TAC";;
 889
 890 (*
 891 let MP_TAC_BAK = MP_TAC;;
 892 let MATCH_MP_TAC_BAK = MATCH_MP_TAC;;
 893 *)
 894
 895
 896 let mp_theorems = ref[];;
 897 let incr1 thm = (mp_theorems:= thm::!mp_theorems);;
 898
 899 let MP_TAC_COUNT t  =
 900   let _ = incr1 t in MP_TAC_BAK t;;
 901
 902 let MP_TAC = MP_TAC_COUNT ;;
 903
 904 let MATCH_MP_TAC_COUNT t  =
 905   let _ = incr1 t in MATCH_MP_TAC_BAK t;;
 906
 907 let MATCH_MP_TAC = MATCH_MP_TAC_COUNT ;;
 908 let MATCH_MP_TAC = MATCH_MP_TAC_BAK ;;
 909
 910
 911 reneeds "trigonometry/trig2.hl";;
 912
 913 let thm_hash = Hashtbl.create 1000;;
 914 map (fun (x,y) -> Hashtbl.add thm_hash y x) (!theorems);;
 915
 916 let find_name th =
 917   try (Hashtbl.find thm_hash th) with Not_found -> "ANONYMOUS";;
 918
 919 List.length (search[`x:A`]);;
 920
 921 List.length (search[`x > (y:real)`]);; (* 111 *)
 922
 923 List.length (search[`x > &0`]);; (* 67 *)
 924  (search[`x > y`; omit `x > &0`]);; (* complicated thing > simple thing. *)
 925 List.length (search[`x < y`]);; (* 1438 *)
 926
 927 List.length (search[`x >= &0`]);; (* 11 *)
 928 List.length (search[`x <= (y:real)`]);; (* 1830 *)
 929 List.length (search[`x >= y`; omit `x >= &0`]);; (* 85, complicated thing > simple thing. *)
 930
 931
 932 (* IN -- no rhyme or reason. *)
 933 List.length(search[`(IN)`])  (* 3455 *);;
 934 List.length(search[`SETSPEC`]);;  (* 1071 *);;
 935 List.length(search[`SETSPEC`;`(IN)`]);;  (* 568 *)
 936 dest_comb `{x | T} y`;;
 937 List.length (search[`y IN (GSPEC f)`]);; (* 23 *)
 938  (search[`y IN {u | f}`]);; (* 14 *)
 939 (search[`{u | f} y`]);; (* 3 *)
 940 (searcht 40 [`(IN)`;omit `SETSPEC`]);;
 941
 942 dest_comb `{x | x > 0}`;;
 943
 944 List.length (search[`x < y`]);; (* 1438 *)
 945
 946 (* search, what is the arc cosine called?  acs *)
 947
 948 search[rewrite `inv`;`( / )`];;
 949 searcht 5 [rewrite `inv`;`a*b`];;
 950 search [regexp "[dD]iff"];;
 951 is_rewrite "inv" ("",REAL_INV_MUL);;
 952 heads (snd(dest_thm(REAL_INV_MUL)));;
 953
 954 Toploop.execute_phrase;;
 955
 956
 957 types();;
 958
 959 constants();;
 960 heads(concl(hd(definitions())));;
 961
 962
 963
 964
 965 (* experiments *)
 966
 967 let _ =
 968   let dds = map fst def_assoc in
 969     sort (fun (_,a) (_,b) -> a > b) (map (fun t-> (t,stm_depth t)) dds);;
 970
 971
 972
 973
 974 let thm_depthnth n =
 975   let (s,th) = List.nth !theorems n in
 976   let d = thm_depth th in (s,d,th);;
 977
 978
 979 tm_depth `!a b.  (&2 <= a /\ a <= #2.52) /\ &2 <= b /\ b <= #2.52
 980          ==>( ((\x. -- (&4 + a pow 2 - x pow 2)/(a * sqrt(ups_x (a pow 2) (b pow 2) (&4)))) has_real_derivative
 981               (&32 * a * b /( (sqrt (ups_x (a pow 2) (b pow 2) (&4))) pow 3)))
 982              (atreal b within real_interval [&2,#2.52]))`;;
 983
 984 let depth_filter n = filter (fun (_,t)->
 985           let (_,c) = hd (thm_depth t) in (c <= n));;
 986
 987 searcht 10 [`has_real_derivative`;`real_div`];;
 988 (* now distance between constants *)
 989
 990 help_grep_flags "rat" "i";;
 991
 992 help "REAL_RAT_REDUCE_CONV";;
 993 stm_depth "pi";;
 994 stm_depth "cos";;
 995 stm_depth "sin";;
 996 assoc "pi" def_assoc;;
 997
 998 thm_depthnth 1000;;
 999
1000 stm_depth "?";;
1001 stm_depth "!";;
1002 stm_depth "hull";;
1003 stm_depth "uniformly_continuous_on";;
1004 stm_depth "real_add";;
1005 stm_depth "treal_add";;
1006 stm_depth "hreal_add";;
1007 stm_depth "nadd_eq";;
1008 stm_depth "dist";;
1009 stm_depth "-";;
1010 stm_depth "PRE";;
1011 stm_depth "_0";;
1012 assoc "_0" def_assoc;;
1013
1014 dest_const `(+)`;;
1015 s_depth "arclength";;
1016
1017 c_depth `acs`;;
1018 c_depth `(@)`;;
1019 assoc `T` def_assoc;;
1020
1021 rho_node;;
1022
1023 c_of [] `sin(cos (x + y))`;;
1024
1025 searcht 5 [`a/b + c/d`];;
1026
1027
1028 searcht 5 [`x pow n = &0`];;
1029
1030 help_grep "REAL_RAT";;
1031
1032 pre_rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;
1033
1034 strip_comb `&1 + &2`;;
1035 dest_comb;;
1036
1037
1038
1039
1040 REAL_INV_DIV;;
1041
1042 searcht 5 [`inv`;`a/b`];;
1043 searcht 5 [`a/b + c/d`];;
1044 let (rr,_)=hd[(`(+)`,ratform_add);
1045                        (`( * )`,ratform_mul);(`( - )`,ratform_sub);
1046                        (`( / )`,ratform_div)];;
1047 type_of rr;;
1048 rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;
1049 Calc_derivative.derivative_form `\q. sin(q pow 5)` `t:real` `{}:real->bool`;;
1050 pre_rationalize `inv (w)`;;
1051
1052 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]`;;
1053
1054 searcht 5[`x pow 1`];;
1055
1056 search [name "HAS_REAL";name "COS"];;
1057
1058 search [`(within)`;`(:real)`];;
1059
1060 open Calc_derivative;;
1061
1062   let th1 =
1063     let x = `x:real` in
1064     let s = `{t | t > &0}` in
1065     let tm = `\x. x pow 3 + x * x - x * -- x + x/(x + &1)`in
1066       differentiate tm x s;;
1067
1068   let th1 =
1069     let x = `x:real` in
1070     let s = `{t | t > &0}` in
1071     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
1072       differentiate tm x s;;
1073
1074   let th2 =
1075     let x = `x:real` in
1076     let s = `(:real)` in
1077     let tm = `\q.  cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in
1078       differentiate tm x s;;
1079
1080   let th3 =
1081     let x = `&5` in
1082     let s = `(:real)` in
1083     let tm = `\q.  cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in
1084       differentiate tm x s;;
1085
1086
1087 (* prove rational identity modulo accumulating assumptions *)
1088
1089   let   equ = `(&1 / u  - &1/v) pow 2  = inv u pow 2 - &2 * inv (u * v) + inv v pow 2`;;
1090   let eq0 = MATCH_MP (REAL_ARITH `u - v = &0 ==> (u=v)`);;
1091
1092 CONV_RULE rc (pre_rationalize `&1 / (x + y) - &1 / (x - y) - (-- &2 * y / (x pow 2 - y pow 2))`);;
1093   let lite_imp = MESON[] `ratform p a ;;
1094
1095 REAL_FIELD ` ((x - y - (x + y)) * (x pow 2 * &1 pow 2 - &1 pow 2 * y pow 2) -
1096       ((x + y) * (x - y)) * -- &2 * y * &1 pow 2 * &1 pow 2) = &0`;;
1097
1098 mk_neg;;
1099 mk_binop;;
1100
1101 searcht 5 [`(a1 pow n / b1 pow n)`];;
1102
1103 let ratform_tac =
1104     REWRITE_TAC [ratform] THEN
1105     REPEAT STRIP_TAC THENL
1106     [ASM_MESON_TAC[REAL_ENTIRE] ;
1107     REPEAT (FIRST_X_ASSUM (fun t -> MP_TAC t THEN ANTS_TAC THEN
1108                              ASM_REWRITE_TAC[])) THEN
1109     REPEAT STRIP_TAC THEN
1110     ASM_REWRITE_TAC[] THEN
1111     REPEAT (POP_ASSUM MP_TAC) THEN
1112     CONV_TAC REAL_FIELD];;
1113
1114
1115
1116 let ratform_pow = prove_by_refinement(
1117   `ratform p1 r1 a1 b1 ==> ratform p1 (r1 pow n) (a1 pow n) (b1 pow n)`,
1118   (* {{{ proof *)
1119   [
1120     REWRITE_TAC[ratform;GSYM REAL_POW_DIV];
1121   ratform_tac;
1122   ]);;
1123   (* }}} *)
1124
1125 rational_identity `&1 / (x + y) - &1 / (x - y) = -- &2 * y / (x pow 2 - y pow 2)`;;
1126
1127
1128 REAL_FIELD `&2 * x * y - &2 * y * x`;;
1129
1130
1131    let mk_derived tm =
1132      let (h1,[f1;f1';r1]) = strip_comb tm in
1133      let (h2,[b2;s1]) = strip_comb r1 in
1134      let (h3,b) = dest_comb b2 in
1135        (f1,SPECL [f1;f1';b;s1] triv) in
1136
1137    let hooked_deriv hook =
1138      let assumed_rules = map mk_derived hook in
1139      let d_hyp tm  =
1140        let r =        assoc tm assumed_rules in
1141        let _ = print_thm r in
1142          r in
1143
1144     let  triv = REWRITE_RULE[](REWRITE_CONV[derived_form]
1145      `!f f' x s. derived_form ((f has_real_derivative f') (atreal x within s)) f f' x s` ) in
1146
1147 differentiate_hook [`(f has_real_derivative (&17)) (atreal x within (:real))`] `\x. ((f:real->real) x) pow 2` `x:real` `(:real)`;;
1148
1149   differentiate_hook [`(f has_real_derivative f') (atreal x within (:real))`] `f:real->real` `x:real` `(:real)`;;
1150
1151 let  triv = REWRITE_RULE[](REWRITE_CONV[derived_form]
1152      `!f f' x s. derived_form ((f has_real_derivative f') (atreal x within s)) f f' x s` );;
1153
1154
1155 mk_derived `(f has_real_derivative (&17)) (atreal x within (:real))`;;
1156 assoc `f:real->real` [it];;
1157 differentiate_hook;;
1158
1159 `(f has_real_derivative f') (atreal x within (:univ))`;;
1160
1161   let d_hyp assumed_rules tm =
1162     snd(find (fun (r,s) -> aconv tm r) assumed_rules);;
1163
1164
1165 let triv2 = prove_by_refinement(
1166   `f f' x s. derived_form ((f has_real_derivative f') (atreal x)) f f' x (:real)`,
1167   (* {{{ proof *)
1168   [
1169   REWRITE_TAC[derived_form;WITHINREAL_UNIV];
1170   ]);;
1171   (* }}} *)
1172
1173
1174 (* acceptable forms
1175    `!x s. p ==> (f has_real_derivative f') (atreal x within s)`
1176    `!x s. p ==> (f has_real_derivative f') (atreal x)`
1177    `!x s. derived_form f f' x s`;;
1178 *)
1179
1180 let thm5 = prove_by_refinement(
1181   `!x s. derived_form (p x /\ (!x s.  (derived_form (p x) f (f' x) x s))) f (f' x) x s`,
1182   (* {{{ proof *)
1183   [
1184     REWRITE_TAC[derived_form];
1185     MESON_TAC[];
1186   ]);;
1187
1188
1189 let thm4 = prove_by_refinement(
1190   `!x s. derived_form (!x s.  (f has_real_derivative f' x) (atreal x within s)) f (f' x) x s`,
1191   (* {{{ proof *)
1192   [
1193     REWRITE_TAC[derived_form];
1194     MESON_TAC[];
1195   ]);;
1196   (* }}} *)
1197
1198 let thm3 = prove_by_refinement(
1199   `!x s. derived_form (!x.  (f has_real_derivative f' x) (atreal x)) f (f' x) x s`,
1200   (* {{{ proof *)
1201   [
1202    REWRITE_TAC[derived_form];
1203     MESON_TAC[HAS_REAL_DERIVATIVE_ATREAL_WITHIN];
1204   ]);;
1205   (* }}} *)
1206
1207 let thm2 = prove_by_refinement(
1208   `!x s. derived_form (p x /\ (!x. p x ==> (f has_real_derivative f' x) (atreal x) )) f (f' x) x s`,
1209   (* {{{ proof *)
1210   [
1211      REWRITE_TAC[derived_form];
1212     MESON_TAC[HAS_REAL_DERIVATIVE_ATREAL_WITHIN];
1213   ]);;
1214   (* }}} *)
1215
1216 let thm1 = prove_by_refinement(
1217   `! x s. derived_form (p x /\ (!x s. p x==> (f has_real_derivative f' x) (atreal x within s)))
1218     f (f' x) x s`,
1219   (* {{{ proof *)
1220   [
1221     REWRITE_TAC[derived_form];
1222     MESON_TAC[];
1223   ]);;
1224   (* }}} *)
1225
1226 let mk_derived  =
1227   let     form1 =    `!x s. p x==> (f has_real_derivative f' x) (atreal x within s)`in
1228   let     form2 =    `!x. p x ==> (f has_real_derivative f' x) (atreal x)` in
1229   let     form3 =    `!x.  (f has_real_derivative f' x) (atreal x)` in
1230   let     form4 =    `!x s.  (f has_real_derivative f' x) (atreal x within s)` in
1231   let     form5 =    `!x s.  derived_form p f f' x s` in
1232   let fls =  [
1233     (form1,thm1);(form2,thm2);(form3,thm3);(form4,thm4);(form5,thm5)] in
1234   let mm tm (r,s) =
1235     let ins = term_match [] r tm in
1236       INST ((fun (_,a,_) -> a) ins) s in
1237     fun tm ->
1238       tryfind (mm tm) fls;;
1239
1240
1241
1242
1243 df tm4;;
1244 search [`within`;`atreal`;`has_real_derivative`;name "HAS_REAL"];;
1245 let tm5 = `!x u. derived_form q g g' x u`;;
1246 let tm4 = `!x u. (x > &0) ==> (g has_real_derivative (x pow 2)) (atreal x within u)`;;
1247 if (can (term_match [] form5) tm) then tm else ( failwith "form5");;
1248 MATCH_MP th4 tm4;;
1249 MATCH_MP;;
1250 let ins =  (term_match [] form4) tm4 ;;
1251 INST ((fun (_,a,_) -> a) ins)  thm4;;
1252
1253 mk_derived tm5;;
1254
1255    let mk_derived tm =
1256      let (h1,[f1;f1';r1]) = strip_comb tm in
1257      let (h2,[b2;s1]) = strip_comb r1 in
1258      let (h3,b) = dest_comb b2 in
1259        (f1,SPECL [f1;f1';b;s1] triv) ;;
1260
1261
1262
1263
1264 MATCH_MP;;
1265
1266
1267
1268
1269 type_of `has_real_derivative`;;
1270 types_of `derived_form ((f has_real_deriv f') (atreal x within s))`;;
1271
1272
1273
1274 snd(top_realgoal());;
1275 let (h1,[f;f';r]) = strip_comb (snd(top_realgoal()));;
1276 let _ = (h1 = `(has_real_derivative)`) or
1277   failwith "form 'f has_real_derivative f' atreal b within s' expected." ;;
1278 let (h2,[atb;s1]) = strip_comb r;;
1279 let (h3,b) = dest_comb atb;;
1280 1;;
1281 1;;
1282
1283 BETA_CONV;;
1284
1285
1286
1287 search[`A INTER B = B INTER A`];;
1288
1289 search[`&0 <= x * x`];;
1290 REAL_ENTIRE;;
1291
1292 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`;;
1293
1294 Calc_derivative.differentiate `\t. &1/(cos (a * t pow 2))` `b+ &1` `(:real)`;;
1295
1296 time Calc_derivative.differentiate `\t. &1/(cos (a * t pow 2))` `b+ &1` `{x | x > &0}`;;
1297
1298
1299
1300
1301 searcht 5 [`(a,b) = (c,d)`];;
1302 ``,
1303     if (NULLSET X) then {} else
1304         (let (k,ul) = cell_params V X in set_of_list (truncate_simplex (k-1) ul))`;;
1305
1306 LET_TAC;;
1307
1308 g `!(x). (x = x) \/ (!(x:num). x = x) \/ (!(y:bool). y = y)`;;
1309
1310 Print_types.print_goal_var_overload();;
1311
1312 hash_of_term `p /\ q ==> r`;;
1313
1314 tachy "rt";;
1315
1316
1317 eval_goal `a /\ b /\ c /\ d ==> r /\ s`;;
1318 eval_tactic_abbrev "rt/a,[TRUTH]";;
1319
1320 st/r,
1321 rt/a,[];;
1322
1323 (!Toploop.parse_toplevel_phrase (Lexing.from_string ("let xx = `&1`;;")));;
1324
1325 eval_command "let xx = `(x:real) + 2`;;";;
1326
1327 eval_command "failwith \"hi\" ;;";;
1328 eval_command "assocrx";;
1329
1330 thm_depth FACET_OF_POLYHEDRON;;
1331 searcht 15 [`norm x = &1`];;
1332
1333
1334  let tachit s =
1335    let alpha_num = Str.regexp "[a-z_A-Z]+" in
1336     let _ = Str.string_match alpha_num s 0 or failwith "tachit" in
1337     let m = Str.matched_string s in
1338     let ns = (break_init m s) in
1339     let n = if (String.length n > 0)
1340       el n (tachy m)   ;;
1341 tachit "sgth";;
1342 tachy "sgth";;
1343
1344 Str.regexp;;
1345 String.escaped "/\\ ";;
1346
1347 Sys.command;;
1348 Sys.command "date";;
1349
1350
1351
1352 (*
1353 let lemma = prove_by_refinement(
1354   `!a b . (!t. a < t ==> b <= t) ==> (!t. a <= t ==> b <= t)`,
1355   (* {{{ proof *)
1356 [
1357 REPEAT STRIP_TAC ;
1358 DISJ_CASES_TAC (REAL_ARITH `a< t \/ a = t \/ t < a`);
1359 ASM_MESON_TAC [];
1360 HASH_UNDISCH_TAC 1429 ;
1361 DISCH_THEN DISJ_CASES_TAC;
1362 ASM_REWRITE_TAC [REAL_ARITH `b<=t <=> (t < b ==> F)`];
1363 DISCH_TAC ;
1364 HASH_RULE_TAC 6466 (SPEC `(a + b)/ (&2)`);
1365 ASM_REAL_ARITH_TAC ;
1366 ASM_REAL_ARITH_TAC
1367 ]
1368 );;
1369   (* }}} *)
1370 *)
1371 *)
1372 ]
1373 );;
1374   (* }}} *)
1375
1376
1377 List.length tactic_counts;;
1378   end_itlist (fun (_,t) (_,u) -> ("",t + u)) tactic_counts20;;
1379
1380 let INFINITE_EXISTS = prove_by_refinement (
1381 `!S. INFINITE S ==> (?(x:A). x IN S)`,
1382 [
1383 REWRITE_TAC[INFINITE];
1384 REPEAT STRIP_TAC;
1385 ASM_MESON_TAC[FINITE_EMPTY;Misc_defs_and_lemmas.EMPTY_EXISTS;];
1386 ]);;
1387 FINITE_EMPTY;;
1388 INFINITE;;
1389 FINITE_EMPTY;;
1390
1391 let INFINITE_EXISTS = prove_by_refinement (
1392 `!S. INFINITE S ==> (?(x:A). x IN S)`,
1393 [
1394 REWRITE_TAC[INFINITE;GSYM Misc_defs_and_lemmas.EMPTY_EXISTS];
1395 CONV_TAC (CONTRAPOS_CONV);
1396  THEN MESON_TAC[FINITE_EMPTY];
1397
1398 ]);;
1399
1400
1401 (* save. find strange constants *)
1402
1403 let symbolic_of cnames =
1404   let symbolchar = explode "=-~.,@#$%^&*|\\/?><" in
1405     filter (fun t -> not (intersect (explode t) symbolchar=[])) cnames;;
1406
1407 let symbolic_constants = symbolic_of (map fst (constants()));;
1408 let symbolic_infixes = symbolic_of (map fst (infixes()));;
1409
1410
1411 searcht 5 [name "CHAIN";`has_derivative`];;
1412 apropos();;
1413 help "apropos_derivative";;
1414 Calc_derivative.differentiate;;
1415 Calc_derivative.derived_form;;
1416 Calc_derivative.differentiate `cos` `x:real` `(:real)`;;
1417
1418 help;;
1419 help "help";;
1420
1421 type_of `vector`;;
1422
1423 type_of;;
1424 let types_of = Print_types.print_term_types;;
1425 let type_of_thm = Print_types.print_thm_types;;
1426 let type_of_goal = Print_types.print_goal_types;;
1427 help_grep "type";;
1428
1429 help "apropos_types";;
1430 types_of `($)`;;
1431 has_derivative;;
1432
1433 map (fun t -> (t,type_of t)) (frees ` (!(y:real^6). p y ==> (continuous) (lift o f'') (at y within s))`);;
1434
1435 let arclength2 = prove_by_refinement(
1436   `!h.  (&1 <= h /\ h <= h0) ==> arclength (&2) (&2 * h) (&2) = acs(h / &2)`,
1437   (* {{{ proof *)
1438   [
1439   REPEAT STRIP_TAC;
1440   MP_TAC (SPECL [`&2`;`&2 * h`;`&2`] Trigonometry1.ACS_ARCLENGTH);
1441   BRANCH_A [
1442     ANTS_TAC ;
1443     MP_TAC Sphere.h0;
1444     ASM_REAL_ARITH_TAC;
1445   ];
1446   DISCH_THEN SUBST1_TAC;
1447   AP_TERM_TAC;
1448   UNDISCH_TAC `&1 <= h`;
1449   BY (CONV_TAC REAL_FIELD);
1450   ]);;
1451   (* }}} *)
1452
1453 let usage_count x = List.length (search [x]);;
1454
1455 (* marking *)
1456 reset();;
1457 show_marked();;
1458
1459 let marked = ref [];;
1460 let show_marked() = map (fun t-> (t,assoc t !theorems)) (!marked);;
1461 let mark s =
1462   let th = assoc s (!theorems) in
1463   let _ = marked := s::!marked in
1464   th;;
1465 let resetm() = marked:=[];;
1466
1467
1468 term_match [] `s:C` `s:E->G`;;
1469 frees_of_goal();;
1470 `(r:B -> D) ((f:A->B) x) =  ((g:C->D) y)`;;
1471 map types_of (gtypl [`f x`;`y`;`f`;`z:D`]);;
1472 filter has_stv (setify (frees `f x`));;
1473 apropos();;
1474 help "apropos_types";;
1475
1476
1477 let EZ_SOS_TAC equ =
1478   let lh = lhs equ in
1479   (REWRITE_TAC[REAL_ARITH `(x > y <=> y < x) /\ (x >= y <=> y <= x)`] THEN
1480     ONCE_REWRITE_TAC[REAL_ARITH `(x < y <=> &0 < y - x) /\ (x <= y <=> (&0 <= y - x))`]) THEN
1481 let
1482     fun (asl,w) ->
1483       let eqthm = try    (REAL_FIELD eqn ) with _ -> failwith "sos_tac, REAL_FIELD failed" in
1484       let binop =
1485
1486 rhs;;
1487
1488 searcht 5 [`x > y <=> x < y`];;
1489
1490 let equ = `(&1 - t) * (&1 pow 2) + t * (&1 - t) * (&1 pow 2) = (&1 - t pow 2)`;;
1491 let lh = lhs equ;;
1492 let (plus,adden) = strip_comb  lh;;
1493 let _ = (plus = `(+)`) or failwith "sum expected";;
1494 help_grep "strip";;
1495 help "strip_comb";;
1496
1497 g `&1 + &1 = &2`;;
1498 r,[];;
1499
1500 Str.split (Str.regexp "`") "`how `1` is it`";;
1501 Str.split (Str.regexp "ab") "That is a better choice ab t";;
1502 Str.split (Str.regexp "(\*") "^(* Start comment (* ( *) $";;
1503
1504 help_grep "dest";;
1505 dest_pair `(a,b)`;;
1506
1507 map type_of [disjunct (`CARD`,`HAS_SIZE`)];;
1508 search [disjunct (`HAS_SIZE`,`CARD`)];;
1509 type_of `HAS_SIZE`;;
1510 search [disjunct (`&0 < inv x`,`&0 < sqrt u`)];;
1511 search [disjunct (`&0 < sqrt u`,`&0 < inv x`)];;
1512 search [`&0 < sqrt u`];;
1513
1514 search[disjunct (`INJ`,`(f x = f y) ==> (x = y)`);disjunct(`CARD`,`HAS_SIZE`)];;
1515
1516 INJ_CARD;;
1517
1518 mk_rewrites false (ASSUME `!s. s = t`) [];;
1519
1520 net_of_thm false (ASSUME `s = t`) empty_net;;
1521
1522 empty_net;;
1523
1524 p();;
1525 !invariant_under_linear;;
1526
1527
1528 let pollack_inconsistency =
1529   let thm1 = prove(  `?(n:num). (t < n)`,EXISTS_TAC`t + 1` THEN ARITH_TAC) in
1530   let t = mk_var("n < 0 /\\ 0",`:num`) in
1531     INST [(t,`t:num`)] thm1;;
1532
1533 (* *)
1534
1535     let curryl = [Calc_derivative.atn2curry] ;;
1536     let curry = REWRITE_CONV curryl;;
1537     let uncurry = REWRITE_CONV (map GSYM curryl) ;;
1538
1539 uncurry `\x. atn2 (x,x + &1)`;;
1540
1541 curry `f`;;
1542 (*
1543 Counting_spheres....
1544 *)
1545
1546 !invariant_under_translation;;
1547 searcht 10 [`dihV`;`arcV`];;
1548 searcht 10 [`r f x y = f y x`;omit `#x`];;
1549 VECTOR_ANGLE_ANGLE;;
1550 search[name "ARCV_ANGLE"];;
1551 search[`Arg`;`vector_angle`];;
1552 searcht 10 [`azim`;`Arg`];;
1553 (* from wlog_examples.ml *)
1554
1555 let TRUONG_1 = prove
1556  (`!u1:real^3 u2 p a b.
1557      ~(u1 = u2) /\
1558      plane p /\
1559      {u1,u2} SUBSET p /\
1560      dist(u1,u2) <= a + b /\
1561      abs(a - b) < dist(u1,u2) /\
1562      &0 <= a /\
1563      &0 <= b
1564      ==> (?d1 d2.
1565               {d1, d2} SUBSET p /\
1566               &1 / &2 % (d1 + d2) IN affine hull {u1, u2} /\
1567               dist(d1,u1) = a /\
1568               dist(d1,u2) = b /\
1569               dist(d2,u1) = a /\
1570               dist(d2,u2) = b)`,
1571   (*** First, rotate the plane p to the special case z$3 = &0 ***)
1572
1573   GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool`
1574
1575
1576 (* bug on loading misc.ml. (next is used as a variable, but later it becomes a constant  *)
1577 Debug.Term_of_preterm_error
1578  [("function head", `next`, `:(?2712096)loop->?2712096->?2712096`);
1579   ("function arg", `0`, `:num`)].
1580 Error in included file /Users/thomashales/Desktop/googlecode/hol_light/Multivariate/misc.ml
1581 - : unit = ()
1582
1583 File "/Users/thomashales/Desktop/googlecode/hol_light/calc_rat.ml", line 515, characters 4-160:
1584 Error: This expression has type
1585          (num -> term) * conv * conv * conv * (term -> thm) * (term -> thm) *
1586          (term -> thm) * (term -> thm) * 'a
1587        but an expression was expected of type
1588          (thm list * thm list * thm list -> positivstellensatz -> thm) ->
1589          thm list * thm list * thm list -> thm
1590
1591 (*
1592 let backup_proof_record = !proof_record;;
1593 List.length backup_proof_record;;
1594 *)
1595
1596 (*
1597 let rec clean_proof_record g skip tbs  =
1598    function
1599        [] -> (g, EVERY (List.rev tbs))
1600      | Gax u :: xs -> clean_proof_record [u] skip tbs xs
1601      | Bax::xs -> clean_proof_record g (skip+1) tbs
1602      | Tax (_,_,t)::xs -> if (skip<=0) then clean_proof_record g 0 (t::tbs) xs else
1603          clean_proof_record g (skip-1) tbs xs;;
1604
1605 let replay (g,t) =
1606
1607
1608 let replay_proof gax_no count =
1609   let p1 = List.nth (gax()) gax_no in
1610   let p2 = fst(chop_list count p1) in
1611   let _ = proof_record:= p2 @ !proof_record in
1612     replay();;
1613
1614 let rotate_proof n =
1615   let (a,b) = chop_list n (gax()) in
1616     List.flatten (b,a);;
1617 *)
1618
1619   let _ = reneeds "usr/thales/init_search.hl" in ();;
1620
1621
1622
1623 let REAL_LEMMA = prove_by_refinement(
1624   `!t s. (&0 < t ) ==> (?x. &0 < x /\ (&0 < s + t * x))`,
1625   (* {{{ proof *)
1626   [
1627   REPEAT WEAK_STRIP_TAC;
1628   ASM_CASES_TAC (`&0 < s + t `);
1629     EXISTS_TAC `&1`;
1630     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1631   EXISTS_TAC `&1 - s/t`;
1632   CONJ_TAC;
1633     MATCH_MP_TAC (arith `&0 < (-- a)/b ==> &0 < &1 - a/b`);
1634     MATCH_MP_TAC REAL_LT_DIV;
1635     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1636   SUBGOAL_THEN `s + t * (&1 - s/t) = t` SUBST1_TAC;
1637     Calc_derivative.CALC_ID_TAC;
1638     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1639   BY(ASM_REWRITE_TAC[])
1640   ]);;
1641   (* }}} *)
1642
1643 Topology.th1;;
1644
1645 let AZIM_ARG4 = prove_by_refinement(
1646   `!x v u w t1 t2 t3.  &0 < t3 /\ ~collinear {x , v , u} /\ ~collinear {x,v,w} ==>
1647     azim x v u w  = azim x v u (t1 % x + t2 % v + t3 % w)`,
1648   (* {{{ proof *)
1649   [
1650   st/r
1651   sgth `(?x. &0 < x /\ (&0 < (t1 + t2 + t3 * x)))` mptac
1652     rt[arith `t1 + t2 + t3*x = (t1 + t2) + t3*x`]
1653     mmp REAL_LEMMA
1654     art[]
1655     st
1656     sgth `(t3 % w = (t3 * x') % (&1/x' % (w:real^3)))` subst1
1657     rt[VECTOR_MUL_ASSOC]
1658     repeat (apthmtac ORELSE aptermtac)
1659     calc
1660     repeat (fxa mptac) then rat
1661       abbrev `s = t1 + t2 + t3 * x'`
1662       sgth `t1 % x + t2 % v + (t3 * x') % (&1/x' % w) =
1663   ]);;
1664   (* }}} *)
1665
1666 searcht 5 [`a % (b % c)`;`(a * b) % c`];;
1667
1668
1669
1670   EXTREME_POINT_OF_FACE;;
1671
1672 FACE_OF_EQ;;  (* relative interiors of faces are disjoint *)
1673
1674 QOEPBJD;;
1675  FACE_OF_POLYHEDRON_POLYHEDRON;;
1676
1677 NEHRQPR;;
1678   POLYHEDRON_COLLINEAR_FACES;;
1679
1680
1681
1682 Graph_control.run(Graph_control.bezdek_reid_properties);;
1683 flyspeck_needs "../glpk/fejesToth_contact/bezdek_reid_problem.ml";;
1684 List.length Bezdek_reid_problem.archive;;
1685 let brp = Bezdek_reid_problem.exec();;
1686 let zbrp = zip Bezdek_reid_problem.archive brp;;
1687 let feas = filter (fun (_,(a,_)) -> not(a = ["PROBLEM HAS NO PRIMAL FEASIBLE SOLUTION"]) && not (a = ["PROBLEM HAS NO FEASIBLE SOLUTION"])) zbrp;;
1688 List.length feas;;
1689 let mk_bb = Bezdek_reid_problem.mk_bb;;
1690 let feas_bb = map (fun (t,_) -> mk_bb t) feas;;
1691
1692 open Bezdek_reid_problem;;
1693 open Glpk_link;;
1694 let out_bb = map (fun bb -> solve_branch_f model dumpfile "optival" ampl_of_bb bb) feas_bb;;
1695 feas_bb;;
1696
1697 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 ";;
1698 solve_branch_f model dumpfile "optival" ampl_of_bb (mk_bb bb);;
1699
1700   let svar = mk_var (s,snd(dest_var t));;
1701
1702
1703
1704 let leaf_def = `leaf V u0 u1 = { u |  u IN V /\ ~collinear {u0,u1,u} /\
1705                                      radV {u0, u1, u2} < sqrt2 }`;;
1706
1707 let leaf_ordering_def = `leaf_ordering V u0 u1 v f n =
1708   leaf V u0 u1 HAS_SIZE n /\
1709   (! i j. i < n /\ j < n /\ (f i = f j) ==> (i = j)) /\
1710     (f n = f 0) /\
1711     (!i. i < n ==> (f i IN leaf V u0 u1)) /\
1712     u0 IN V /\ u1 IN V /\
1713     (!i j. i < j ==> azim u0 u1 v (f i) < azim u0 u1 v (f (i+1)))`;;
1714
1715 let mcell_group_def = `mcell_group V u0 u1 f i =
1716       {X |   X SUBSET wedge u0 u1 (f i) (f (i+1)) /\
1717            {u0,u1} IN edgeX V X /\
1718          X IN mcell_set V /\
1719          ~(NULLSET X) }`;;
1720
1721 let mcell_group_sum = `!V u0 u1 v f n i.
1722   packing V /\ saturated V /\
1723   leaf_ordering V u0 u1 v f n /\
1724   1 < n /\ i < n   ==>
1725   sum (mcell_group V u0 u1 f) (\X. dihX V X (u0,u1)) = azim u0 u1 (f i) (f (i+1))`;;
1726
1727 let mcell_group_4_type = `!V u0 u1 v f n X.
1728   packing V /\ saturated V /\
1729   leaf_ordering V u0 u1 v f n /\
1730   1 < n /\
1731   X IN mcell_set V /\
1732   ~(NULLSET X) /\
1733   {u0,u1} IN edgeX V X /\
1734   FST(cell_params V X) = 4 ==>
1735   (?i. i < n /\
1736      azim u0 u1 (f i) (f (i+1)) < pi /\
1737      radV {u0,u1,(f i),(f (i+1))} < sqrt2  /\
1738      X IN mcell_group V u0 u1 f i)`;;
1739
1740 let mcell_group_23_type = `!V u0 u1 v f n X.
1741   packing V /\ saturated V /\
1742   leaf_ordering V u0 u1 v f n /\
1743   1 < n /\
1744   X IN mcell_set V /\
1745   ~(NULLSET X) /\
1746   {u0,u1} IN edgeX V X /\
1747   FST(cell_params V X) IN {2,3} ==>
1748   (?i. i < n /\
1749      ~(azim u0 u1 (f i) (f (i+1)) < pi /\
1750      radV {u0,u1,(f i),(f (i+1))} < sqrt2)  /\
1751      X IN mcell_group V u0 u1 f i)`;;
1752
1753 (* consequence of previous 2 *)
1754 let mcell_group_type = `!V u0 u1 v f n X.
1755   packing V /\ saturated V /\
1756   leaf_ordering V u0 u1 v f n /\
1757   1 < n /\
1758   u0 IN V /\ u1 IN V
1759   X IN mcell_set V /\
1760   ~(NULLSET X) /\
1761   {u0,u1} IN edgeX V X ==>
1762   (?i. i < n /\ X IN mcell_group V u0 u1 f i)`;;
1763
1764 let mcell_group_4_singleton = `!V u0 u1 v f n i.
1765   packing V /\ saturated V /\
1766   leaf_ordering V u0 u1 v f n /\
1767   1 < n /\ i < n /\
1768   azim u0 u1 (f i) (f (i+1)) < pi /\
1769   radV {u0,u1,(f i),(f (i+1))} < sqrt2  ==>
1770   mcell_group V u0 u1 f i = {  mcell 4 V [u0;u1;(f i);(f (i+1))] }`;;
1771
1772 (* needed: ? *)
1773
1774 let mcell_sqrt2_barV = `!V u0 u1 w1 w2.
1775   packing V /\ saturated V /\
1776   {u0,u1,w1,w2} SUBSET V /\
1777   ~coplanar {u0,u1,w1,w2} /\
1778   radV {u0,u1,w1,w2} < sqrt2 ==>
1779   [u0;u1;w1;w2] IN barV V 3`;;
1780
1781 let mcell_group_3_a = `!V u0 u1 f v n i.
1782   packing V /\ saturated V /\
1783   leaf_ordering V u0 u1 v f n /\
1784   1 < n /\ i < n /\
1785   (azim u0 u1 (f i) (f (i+1)) >= pi \/
1786   radV {u0,u1,(f i),(f (i+1))} >= sqrt2)  ==>
1787   (?X w. X IN mcell_group V u0 u1 f i /\
1788      [u0;u1;(f i);w] IN barV V 3 /\
1789      X = mcell3 V [u0;u1;(f i);w])`;;
1790
1791 let mcell_group_3_b = `!V u0 u1 v f n i.
1792   packing V /\ saturated V /\
1793   leaf_ordering V u0 u1 v f n /\
1794   1 < n /\ i < n /\
1795   (azim u0 u1 (f i) (f (i+1)) >= pi \/
1796   radV {u0,u1,(f i),(f (i+1))} >= sqrt2)  ==>
1797   (?X w. X IN mcell_group V u0 u1 f i /\
1798      [u0;u1;(f i);w] IN barV V 3 /\
1799      X = mcell3 V [u0;u1;(f i);w])`;;
1800
1801 (*
1802 need if mcell3 V ul = mcell3 V vl , ul, vl IN barV, NONNULL, and both start with [u0;u1]
1803 the ul = vl.  In particular, the two mcells in 3_a and 3_b are distinct, and
1804 the w is uniquely determined by X.
1805 *)
1806
1807 let mcell_group_3_exhaust =
1808   `!V u0 u1 v f n i X.
1809     packing V /\ saturated V /\
1810     leaf_ordering V u0 u1 v f n /\
1811     1 < n /\ i < n /\
1812     X IN mcell_group V u0 u1 f i /\
1813     FST(cell_params V X) = 3 /\
1814   (?w u.
1815      u IN {(f i),(f (i+1))} /\
1816      X = mcell3 V [u0;u1;u;w] /\ [u0;u1;u;w] IN barV V 3)`;;
1817
1818 (* also need formula for 4-cell gamma, 3-cell gamma, 2-cell gamma (as a function of angle)
1819    in terms of the functions that appear in ineq.hl.
1820 *)
1821
1822
1823   module More = struct
1824     open Sphere;;
1825     open Ineq;;
1826 add
1827   {
1828     idv = "FWGKMBZ";
1829     ineq = all_forall `ineq
1830       [(&2 * hminus, y1, &2 * hplus );
1831        (&2 ,y2,sqrt8 );
1832        (&2,y3,sqrt8);
1833        (&2,y4,sqrt8);
1834        (&2,y5,sqrt8 );
1835        (&2,y6,sqrt8 )
1836       ]
1837       (y_of_x delta_x y1 y2 y3 y4 y5 y6 > &0)`;
1838     doc = "
1839      This is used with rad2_x calculations to bound the denominator.
1840  ";
1841     tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Tex;Cfsqp;Xconvert;Branching];
1842   };;
1843 add
1844   {
1845     idv = "FHBVYXZ a";
1846     ineq = all_forall `ineq
1847       [(&2 * hminus, y1, &2 * hplus );
1848        (&2 ,y2,&2 * hminus );
1849        (&2,y3,&2 * hminus);
1850        (&2,y4,&2 * hminus);
1851        (&2,y5,&2 * hminus );
1852        (&2,y6,&2 * hminus )
1853       ]
1854       ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
1855         > &0)\/
1856          (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
1857     doc = "
1858   OXLZLEZ.mod 'g_quqya' 'g_quqyb'
1859 %old idv: 1118115412, cc:2bl
1860 If $X$ is any quarter, and  $Y$ is a $3$-cell that flanks it, then
1861 \\[
1862 \\gamma(X,L) + \\gamma(Y,L) \\ge 0.
1863 \\]
1864 Nov2012, changed eta_y y1 y3 y5 to eta_y y1 y2 y6.
1865  ";
1866 (* + &0 * gamma3f y1 y3 y5 sqrt2 lmfun dropped *)
1867     tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
1868   };;
1869   end;;
1870
1871
1872
1873 Auto_lib.testsplit true "FHBVYXZ a";;
1874   map (fun t -> try (Auto_lib.testsplit bool t) with Failure _ -> [()]) cases;;
1875 open Functional_equation;;
1876 string_of_num (num_of `5`;;
1877 dest_numeral `55555555555555`;;
1878 i_mk2 `0`;;
1879
1880                module More = struct
1881                  open Sphere;;
1882                  open Ineq;;
1883 add
1884 {
1885   idv = "QZECFIC wt2 A"; (* was "test ratio" , y4 y5 swapped, nov 2012 *)
1886   ineq = all_forall `ineq
1887    [(sqrt2,y1,sqrt2);
1888     (sqrt2,y2,sqrt2);
1889     (sqrt2,y3,sqrt2);
1890     (&2 * hminus ,y4, sqrt8);
1891     (&2 * hminus, y5, sqrt8);
1892     (&2 ,y6, &2 * hminus)
1893    ]
1894    ( 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 \/
1895        eta_y y4 y5 y6 pow 2 > &2
1896    )`;
1897   doc =   "gamma3f averages at least 0.008 per azim.
1898     We don't have a wt3 case because eta[2hminus,2hminus,2hminus]>sqrt2.";
1899   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3;4]];
1900 };;
1901 add
1902 {
1903   idv = "PEMKWKU test1";
1904   ineq = all_forall `ineq
1905    [(&2 * hminus, y1, &2 * hplus);
1906     (&2 * hminus ,y2, sqrt8);
1907     (&2,y3, &2 * hminus);
1908     (&2 ,y4, sqrt8);
1909     (&2,y5, &2 * hminus);
1910     (&2,y6, &2 * hminus)
1911    ]
1912    (
1913   ((y_of_x (gamma23_keep135_x (h0cut y1))  y1 y2 y3 y4 y5 y6) / &2
1914    > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
1915       y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
1916     dih_y y1 y2 y3 y4 y5 y6 > #1.074 \/
1917      eta_y y1 y2 y6 pow 2 > &2 \/
1918      eta_y y1 y2 y6 pow 2 < #1.34 pow 2 \/
1919      eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
1920   doc =   "test";
1921   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1922 };;
1923 add
1924 {
1925   idv = "BIXPCGW b test";
1926   ineq = all_forall `ineq
1927    [(&2 * hminus,y1, &2 * hplus);
1928     (&2,y2, sqrt8);
1929     (&2,y3, sqrt8);
1930     (&2,y4, sqrt8);
1931     (&2,y5, sqrt8);
1932     (&2,y6, sqrt8)
1933    ]
1934    ( (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))`;
1935   doc =   "
1936    NONQXD
1937      If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
1938   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Penalty (500.0,500.0);Tex;Xconvert];
1939 };;
1940 add
1941 {
1942   idv = "BIXPCGW 6652007036 a2";
1943   ineq = all_forall `ineq
1944    [(&2 * hminus, y1, &2 * hplus);
1945     (&2,y2, sqrt8);
1946     (&2,y3, sqrt8);
1947     (&2,y4, sqrt8);
1948     (&2,y5, sqrt8);
1949     (&2,y6, sqrt8)
1950    ]
1951    ((dih_y y1 y2 y3 y4 y5 y6 < #2.8) )`;
1952   doc =   "
1953     OXLZLEZ.mod 'azim_c4' QX and QU
1954      If $X$ is a $4$-cell then  $\\dih(X) < 2.8$.";
1955   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
1956 };;
1957 add
1958 {
1959   idv = "BIXPCGW 7080972881 a2";
1960   ineq = all_forall `ineq
1961    [(&2 * hminus,y1, &2 * hplus);
1962     (&2 * hminus,y2, sqrt8);
1963     (&2,y3, sqrt8);
1964     (&2,y4, sqrt8);
1965     (&2,y5, sqrt8);
1966     (&2,y6, sqrt8)
1967    ]
1968     ((dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
1969   doc =   "
1970    OXLZLEZ.mod 'g_qxd' QXD
1971      If $X$ is a $4$-cell with a critical edge next to the spine, then  $\\dih(X) < 2.3$.";
1972   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
1973 };;
1974 add
1975 {
1976   idv = "BIXPCGW 1738910218 a2";
1977   ineq = all_forall `ineq
1978    [(&2 * hminus,y1, &2 * hplus);
1979     (&2,y2, sqrt8);
1980     (&2,y3, sqrt8);
1981     (&2,y4, &2 * hplus);
1982     (&2,y5, sqrt8);
1983     (&2,y6, sqrt8)
1984    ]
1985    ( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
1986   doc =   "
1987     OXLZLEZ.mod 'g_qxd'  QXD
1988      If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
1989   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
1990 };;
1991 add
1992 {
1993   idv = "BIXPCGW 7274157868 a";
1994   ineq = all_forall `ineq
1995    [(&2 * hminus,y1, &2 * hplus);
1996     (&2,y2, &2 * hminus);
1997     (&2,y3, &2 * hminus);
1998     (&2 * hplus,y4, sqrt8);
1999     (&2,y5, &2 * hminus);
2000     (&2,y6, &2 * hminus)
2001    ]
2002     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
2003     (dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
2004   doc =   "
2005      OXLZLEZ.mod 'g_qxd' QXD
2006      If $X$ is a $4$-cell with a single critical edge (the spine), and if $\\dih(X)\\ge 2.3$,
2007       then  $\\gamma(X,L) > 0.0057$.";
2008   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
2009 };;
2010 add
2011 {
2012   idv = "GCKBQEA";
2013   ineq = all_forall `ineq
2014    [(&2 * hminus, y1, &2 * hplus);
2015     (&2,y2, sqrt8);
2016     (&2,y3, sqrt8);
2017     (&2,y4, sqrt8);
2018     (&2,y5, sqrt8);
2019     (&2,y6, sqrt8)
2020    ]
2021    (
2022     dih_y y1 y2 y3 y4 y5 y6  > #0.606
2023  )`;
2024   doc =   "Min angle on a cell along a spine.
2025      Nov 2012";
2026   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
2027 };;
2028 add
2029 {
2030   idv = "JSPEVYT";
2031   ineq = all_forall `ineq
2032    [
2033      (&1,y1,&1);
2034      (&1,y2,&1);
2035      (&1,y3,&1);
2036     (&2 * hminus,y4, sqrt8);
2037     (&2 * hminus ,y5, sqrt8);
2038     (&2  ,y6, sqrt8)
2039    ]
2040    (eta_y y4 y5 y6 pow 2 > (#1.34) pow 2 )`;
2041   doc =   "eta small implies face small";
2042   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
2043 };;
2044 add
2045 {
2046   idv = "IXPOTPA";
2047   ineq = all_forall `ineq
2048    [(&2 * hminus, y1, &2 * hplus);
2049     (&2,y2, &2 * hminus);
2050     (&2,y3, &2 * hminus);
2051     (sqrt8,y4, &4 * hminus);
2052     (&2,y5, &2 * hminus);
2053     (&2,y6, &2 * hminus)
2054    ]
2055    (let tan2lower = #3.07 in ( // Tan[Pi-2.089]^2
2056     let tan2upper = #6.45 in ( // Tan[Pi-1.946]^2
2057      delta_y y1 y2 y3 y4 y5 y6 < &0 \/
2058        delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
2059        (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
2060        (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 > tan2upper * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
2061      eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
2062      eta_y y1 y3 y5 pow 2 > #1.34 pow 2 \/
2063   (y_of_x (gamma23_full8_x (h0cut y1)) y1 y2 y3 y4 y5 y6 > &3 * #0.0057))))`;
2064   doc =   "Dec 2, 2012.  This is the case of TXQTPVC, when y4 >= sqrt8.  We can't use monotonicty here,
2065     because of the explicit dih constraints.";
2066   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
2067 };;
2068 add{
2069   idv = "3287695934";
2070   doc="";
2071   tags = [Cfsqp;Tablelp;Xconvert;Tex];
2072   ineq = all_forall `ineq
2073     [
2074       (#4.37,y1,&4 * h0);
2075       (#2.0,y2,&2 * h0);
2076       (#2.0,y3,&2 * h0);
2077       (&2 * h0,y4,&4 * h0);
2078       (#2.0,y5,&2 * h0);
2079       (#2.0,y6,&2 * h0)]
2080    (delta_y y1 y2 y3 y4 y5 y6 < &0)`;
2081 };;
2082 add{
2083   idv = "4821120729";
2084   doc="";
2085   tags = [Cfsqp;Tablelp;Xconvert;Tex];
2086   ineq = all_forall `ineq
2087     [
2088       (&2,y1,&2 * h0);
2089       (#2.0,y2,&2 * h0);
2090       (#2.0,y3,&2 * h0);
2091       (#3.01,y4,#3.915);
2092       (#2.0,y5,&2 * h0);
2093       (#2.0,y6,&2 * h0)]
2094    (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)`;
2095 };;
2096 add{
2097   idv = "6762190381";
2098   doc="This reduces OWZLKVY to the case when delta_y < 200. Added 2013-4-18";
2099   tags = [Cfsqp;Tablelp;Xconvert;Tex];
2100   ineq = all_forall `ineq
2101     [
2102       (&2 ,y1,&2 * h0);
2103       (&2,y2,&2 * h0);
2104       (&2,y3,&2 * h0);
2105       (#3.01,y4,#3.915);
2106       (&2,y5,&2 * h0);
2107       (&2,y6,&2 * h0)]
2108    (
2109    delta_y y1 y2 y3 y4 y5 y6 < &200 \/ taum y1 y2 y3 y4 y5 y6 > &0 )`;
2110 };;
2111 add{
2112   idv = "8346775862";
2113   doc="In OWZLKVY the angle at y1 is obtuse. Added 2013-4-18.";
2114   tags = [Cfsqp;Tablelp;Xconvert;Tex];
2115   ineq = all_forall `ineq
2116     [
2117       (&2 ,y1,&2 * h0);
2118       (&2,y2,&2 * h0);
2119       (&2,y3,&2 * h0);
2120       (#3.01,y4,#3.915);
2121       (&2,y5,&2 * h0);
2122       (&2,y6,&2 * h0)]
2123    (
2124    delta_y y1 y2 y3 y4 y5 y6 > &200 \/ y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 ) `;
2125 };;
2126 add{
2127   idv = "8631418063";
2128   doc="In OWZLKVY the angle at y2,y3 is acute. Added 2013-4-18.";
2129   tags = [Cfsqp;Tablelp;Xconvert;Tex];
2130   ineq = all_forall `ineq
2131     [
2132       (&2,y1,&2 * h0);
2133       (&2,y2,&2 * h0);
2134       (&2,y3,&2 * h0);
2135       (&2,y4,&2 * h0);
2136       (#3.01,y5,#3.915);
2137       (&2,y6,&2 * h0)]
2138    (y_of_x delta_x4 y1 y2 y3 y4 y5 y6 > &0)`;
2139 };;
2140 add
2141 {
2142   idv="5026777310a";
2143   doc="pentagon case, clipped A-piece triangle.   ";
2144   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2145   ineq = all_forall `ineq [
2146     (&2,y1,#2.52);
2147     (#2.0,y2,#2.52);
2148     (&2,y3,#2.52);
2149     (sqrt8,y4,#3.01);
2150     (sqrt8,y5,#3.01);
2151       (&2,y6,#2.52)
2152   ]
2153 (
2154   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 4 1 - &2 * #0.11) \/
2155   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2156  )`;
2157 };;
2158                end;;
2159
2160
2161
2162                module More = struct
2163                  open Sphere;;
2164                  open Ineq;;
2165 add
2166 {
2167   idv="taum";
2168   doc="quad case top neg delta.
2169   Solve[Delta[x,2,2,x,2,3.01]==0,x] (*x < 3.166 *)
2170   Added 2013-05-05.";
2171   tags=[Cfsqp;Xconvert];
2172   ineq = all_forall `ineq [
2173       (&2,y1,#2.52);
2174       (&2,y2,#2.52);
2175       (#2.25,y3,#2.52);
2176       (#3.01,y4,#3.24);
2177       (&2,y5,&2);
2178       (&2,y6,&2)]
2179 (taum y1 y2 y3 y4 y5 y6    > &0)`;
2180 };;
2181 add
2182 {
2183   idv="test";
2184   doc="test ear";
2185   tags=[Cfsqp;Xconvert;Tex;];
2186   ineq = all_forall `ineq [
2187     (&2,y1,#2.52);
2188     (&2,y2,#2.52);
2189     (&2,y3,#2.52);
2190     (#3.01,y4,#3.24);
2191     (&2,y5,&2);
2192       (&2,y6,&2)
2193   ]
2194 (
2195   ( delta_y y1 y2 y3 y4 y5 y6 < &72 \/ taum y1 y2 y3 y4 y5 y6 > #0.038  )
2196  )`;
2197 };;
2198 add
2199 {
2200   idv="test2";
2201   doc="testA ";
2202   tags=[Cfsqp;Xconvert;Tex;];
2203   ineq = all_forall `ineq [
2204     (&2,y1,#2.52);
2205     (&2,y2,#2.52);
2206     (&2,y3,#2.52);
2207     (#3.01,y4,#3.24);
2208     (#3.01,y5,#3.24);
2209       (&2,y6,&2)
2210   ]
2211 (
2212   (  taum y1 y2 y3 y4 y5 y6 > &0  )
2213  )`;
2214 };;
2215 add
2216 {
2217   idv="test3";
2218   doc="";
2219   tags=[Cfsqp;Xconvert;Tex];
2220   ineq = all_forall `ineq [
2221       (#2.0,y1,#2.3);
2222       (#2.0,y2,&2 * h0);
2223       (#2.0,y3,&2 * h0);
2224       (#3.01,y4,#3.23607);
2225       (#2.0,y5,&2);
2226       (#2.0,y6,&2);
2227       (#2.0,y7,&2 * h0);
2228       (#2.0,y8,&2);
2229       (#3.01,y9,#3.23607)]
2230 ( delta_y y1 y2 y3 y4 y5 y6 > &30  \/
2231    enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.23607 )`;
2232 };;
2233 add
2234 {
2235   idv="test4";
2236   doc="
2237     ";
2238   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2239   ineq = all_forall `ineq [
2240     (&2,y1,#2.52);
2241     (&2,y2,#2.52);
2242     (&2,y3,#2.52);
2243     (#3.01,y4,#3.915);
2244     (&2,y5,&2);
2245       (&2,y6,&2)
2246   ]
2247 (
2248    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.027) \/
2249   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2250  )`;
2251 };;
2252                end;;
2253
2254
2255 1;;
2256 map Scripts.one_cfsqp ["test4"];;
2257 map (Auto_lib.testsplit true) ["7697147739 delta top issue";"4680581274 delta top issue";];;
2258
2259 map (Auto_lib.testsplit true) [
2260    "6762190381";
2261    "8346775862";
2262    "8631418063";
2263    "4821120729";];;
2264
2265
2266 let idq_of_string s = hd(Ineq.getexact s);;
2267 idq_of_string "GRKIBMP B";;
2268 Ineq.remove "GRKIBMP B";;
2269 idq_of_string "GRKIBMP test";;
2270 Auto_lib.testsplit true "BIXPCGW 1738910218 a2";;
2271 map (Auto_lib.testsplit true)  [
2272 "QITNPEA1 1 0 9063653052 A";
2273 "QITNPEA1 1 1 9063653052 A";
2274 "QITNPEA1 1 2 9063653052 A";
2275 "QITNPEA1 2 0 9063653052 A";
2276 "QITNPEA1 2 1 9063653052 A";
2277 "QITNPEA1 2 2 9063653052 A";
2278 ];;
2279
2280
2281 Scripts.one_cfsqp "GRKIBMP A V2";;
2282 let [(s1,tags1,testineq1);(s2,tags2,testineq2)] = Optimize.preprocess_split_idq (hd(Ineq.getexact  "GRKIBMP A V2"));;
2283 Auto_lib.execute_interval true tags1 s1 testineq1;;
2284
2285 Auto_lib.testsplit true "GRKIBMP A V2";;
2286
2287 Scripts.one_cfsqp "GLFVCVK4 2477216213 y4subcrit";;
2288
2289
2290 conflicts `x + 1`  `x + &2`;;
2291
2292 aty;;
2293 help_grep "cart";;
2294 help "CONJ_PAIR";;
2295 Debug.find_subterms;;
2296 help_grep "ty";;
2297 help "bty";;
2298 help_grep "mkty";;
2299 help_grep "mk_";;
2300 help "mk_type";;
2301 mk_type ("prod",[`:num`;`:bool`]);;
2302
2303 let follow_your_nose_string_list() =
2304   let aslw = top_realgoal() in
2305   let m = filter (fun (p,_,_) -> p aslw) !noses in
2306   let m2 = map (fun ((_,_,a),b) -> ("{"^string_of_int b ^":"^a^"}")) (zip m (0--((List.length m) -1))) in
2307     Flyspeck_lib.join_comma m2;;
2308
2309 let fynlist k =
2310   let aslw = top_realgoal() in
2311   let m = filter (fun (p,_,_) -> p aslw) !noses in
2312   let (_,t,_) = List.nth m k in
2313    t;;
2314
2315 String.sub "abcde" 0 4;;
2316
2317 let string_starts_with u s = (String.length u <= String.length s) && (u = String.sub s 0 (String.length u));;
2318 string_starts_with "ab" "c";;
2319
2320 help_grep "prior";;
2321 prioritize_real();;
2322 Print_types.print_goal_types();;
2323 bb 10;;
2324
2325
2326 (* Sudoku solver *)
2327 open String
2328
2329 let rec s p=
2330   try
2331     let rec(%)=(mod) and i=index p '0'and
2332         b j=
2333           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)
2334     in
2335       iter (fun c->p.[i]<-c;b 0||()=s p;()) "948721536";
2336       p.[i]<-'0'
2337   with
2338       _->print_string p;;
2339
2340 s(read_line());;
2341
2342 let longt = filter (fun (_,t) -> (30 < t)) times;;
2343 hour(total longt);;
2344 List.length longt;;
2345 map (fun (s,t) -> (s,float_of_int (t) /. 180.0)) longt;;
2346
2347 let t = `hello = there`;;
2348
2349
2350
2351   INST_TYPE;;
2352
2353   type_of  (inst [(`:b`,ty_b)]  b);;
2354 help_grep "inst";;
2355 inst;;
2356 env;;
2357
2358 let inxx = ref[];;
2359 let add_inequality idq = (inxx := idq::!inxx);;
2360 flyspeck_needs "nonlinear/prep.hl";;
2361 let inyy = map (fun t -> t.idv) (!inxx);;
2362 index "4717061266" inyy;;
2363 List.length inyy;;
2364 index "GRKIBMP B V2" inyy;;
2365
2366 Preprocess.exec();;
2367
2368 mk_rewrites true (ASSUME `!a b. a ==> (b /\ c)`) [];;
2369 SPEC_ALL (REFL `a:bool`);;
2370 30 + 230 + 46 + 9 + 224 + 996 + 5;;
2371 BETA_THM;;
2372 ISPECL;;
2373 Preprocess.preprocess1;;
2374 let funx s = (Optimize.preprocess_split_idq  (hd (Ineq.getexact  (s))));;
2375 funx "CJFZZDW";;
2376 Flyspeck_lib.output_filestring;;
2377
2378   let preprocess1 s =
2379     let prep = Optimize.preprocess_split_idq
2380                      (hd (Ineq.getexact  (s))) in
2381     let v =
2382     Flyspeck_lib.join_lines (map Preprocess.print_one prep) in
2383     let _ = report v in
2384       ((s,map (fun (s,_,_) -> s) prep),v);;
2385
2386 Preprocess.preprocess1 "GLFVCVK4a 8328676778";;
2387
2388 g `c ==> b`;;
2389 st/r;;
2390 top_goal();;
2391
2392 (* generating proves prep ==> ineq.hl *)
2393
2394 (* follow preprocess_split_idq, step by step *)
2395
2396   let strip_let_conv = REDEPTH_CONV let_CONV;;  (* strip_let_tm *)
2397
2398   let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV);;
2399
2400 Optimize.get_split_tags;;
2401
2402 let PREPROCESS (s,tags,case) =
2403   let is_xconvert = mem Xconvert tags in
2404   let is_branch = mem Branching tags in
2405   let strip_let_case = strip_let_conv case in
2406   let _ = report ("process and exec: "^s) in
2407   let tacl =
2408     [PRELIM_REWRITE_TAC;
2409      MP_TAC (REWRITE_RULE[] NONLIN);
2410      if (is_branch) then (BRANCH_TAC) else (ALL_TAC);
2411      if (is_xconvert) then e (X_OF_Y_TAC) else e(ALL_TAC);
2412      if (is_branch && not(is_xconvert)) then
2413        (SERIES3Q1H_5D_TAC) else (ALL_TAC);
2414      STYLIZE_TAC;
2415      WRAPUP_TAC] in
2416   let _ = g (strip_let_case) in
2417   let _ = e (EVERY tacl) in
2418   let testineq = snd(top_goal()) in
2419     (s,tags,testineq);;
2420
2421 Optimize.split_h0;;
2422 instantiation;;
2423
2424 g `c ==> b`;;
2425 st/r
2426 asmcase `a:bool` then (repeat (fxa mp))
2427 1;;
2428 refine(merge1_goal);;
2429  (top_asl_thm());;
2430
2431 UNDISCH;;
2432 top_thm();;
2433
2434 top_thm();;
2435 top_realgoal();;
2436 List.length (!current_goalstack);;
2437 List.nth (!current_goalstack) 0;;
2438 CONJ;;
2439
2440 let (merge1_goal:refinement) =
2441   fun (meta,sgs,just) ->
2442   if List.length sgs < 2 then (meta,sgs,just)
2443   else
2444     let s0::s1::s2 = sgs in
2445     let _ = fst(s0) = [] or failwith "merge1_goal asl nonempty" in
2446     let _ = fst(s1) = [] or failwith "merge1_goal asl nonempty" in
2447     let sgs' = ([],mk_conj (snd s0, snd s1)) ::s2 in
2448     let just' i ths =
2449       (just i ( (CONJUNCT1 (hd ths)) :: (CONJUNCT2 ( (hd ths))) :: tl ths)) in
2450       (meta,sgs',just');;
2451
2452 let top_asl_thm() =
2453   let (_,sgs,f)::_ = !current_goalstack in
2454   let t = snd(hd sgs) in
2455     DISCH t (f null_inst [ASSUME t]);;
2456
2457
2458 help_grep "conj";;
2459 mk_conj;;
2460 help "ACCEPT_TAC";;
2461 open Nonlinear_lemma;;
2462            gcy_low;;
2463 gcy_low_const;;
2464 gcy_low_hminus;;
2465 gcy_high;;
2466 gcy_high_hplus;;
2467
2468   let slxx = map (fun t -> t.idv) !Ineq.ineqs;;
2469 hd slxx;;
2470 List.length slxx;;
2471 List.nth sl 442xx;;
2472
2473 prove_ineq "4528012043";;
2474
2475 let s = "4528012043";;
2476   let DSPLIT_TAC i = DISCH_TAC THEN (Optimize.SPLIT_H0_TAC i);;
2477   let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV);;
2478   let is_xconvert tags = mem Xconvert tags;;
2479   let is_branch tags = mem Branching tags;;
2480   let NONL = `prepared_nonlinear:bool`;;
2481   let idq = hd(Ineq.getexact s);;
2482
2483   let (s',tags,ineq) = idq_fields idq;;
2484   let _ = (s = s') or failwith "prove_ineq: wrong ineq";;
2485     try (s,prove(mk_imp(NONL,ineq);;
2486
2487 g(mk_imp(NONL,ineq));;
2488
2489
2490 LET_ELIM_TAC
2491             (EVERY (map DSPLIT_TAC (get_split_tags idq)) );;
2492             EVERY
2493             [
2494 LET_ELIM_TAC;
2495              PRELIM_REWRITE_TAC;;
2496
2497              e(if (is_branch tags) then BRANCH_TAC else ALL_TAC);;
2498              e(if (is_xconvert tags) then X_OF_Y_TAC else ALL_TAC);;
2499              e(if (is_branch tags && not(is_xconvert tags)) then SERIES3Q1H_5D_TAC else ALL_TAC);;
2500              e(STYLIZE_TAC);;
2501              e(WRAPUP_TAC);;
2502              REWRITE_TAC (get_all_prep_nonlinear s)]))
2503     with Failure _ -> failwith s;;
2504 List.length !Ineq.ineqs;;
2505 List.length  !Prep.prep_ineqs;;
2506
2507
2508   module Test = struct
2509     open Hales_tactic;;
2510     open Counting_spheres;;
2511 let FCHANGED_RADIAL_ALT = prove_by_refinement(
2512   `!(p:real^3->bool) f r.
2513     bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f facet_of p ==>
2514     radial r (vec 0) ( fchanged f INTER normball (vec 0) r)`,
2515   (* {{{ proof *)
2516   [
2517   REWRITE_TAC[ Sphere.radial ];
2518   REPEAT WEAK_STRIP_TAC;
2519   REWRITE_TAC[ NORMBALL_BALL ];
2520   REWRITE_TAC[VECTOR_ADD_RID;VECTOR_SUB_RZERO;VECTOR_ADD_LID;VECTOR_SUB_LZERO];
2521   CONJ_TAC;
2522     BY(SET_TAC[]);
2523   REPEAT WEAK_STRIP_TAC;
2524   FIRST_X_ASSUM_ST `fchanged` MP_TAC;
2525   REWRITE_TAC[IN_INTER];
2526   REWRITE_TAC[ Polyhedron.fchanged ];
2527   REWRITE_TAC[ IN_ELIM_THM ];
2528   REPEAT WEAK_STRIP_TAC;
2529   CONJ_TAC;
2530     TYPIFY `v1` EXISTS_TAC;
2531     ASM_REWRITE_TAC[];
2532     TYPIFY `t * t'` EXISTS_TAC;
2533     REWRITE_TAC [ VECTOR_MUL_ASSOC ];
2534     REPEAT (FIRST_X_ASSUM_ST `a > b` MP_TAC);
2535     REWRITE_TAC [arith `a > b <=> b < a`];
2536     BY(MESON_TAC[ REAL_LT_MUL ]);
2537   INTRO_TAC Counting_spheres.RADIAL_NORMBALL [`(vec 0):real^3`;`r`];
2538   REWRITE_TAC[ NORMBALL_BALL ];
2539   REWRITE_TAC[ Sphere.radial ];
2540   REWRITE_TAC[VECTOR_ADD_RID;VECTOR_SUB_RZERO;VECTOR_ADD_LID;VECTOR_SUB_LZERO];
2541   FIRST_X_ASSUM MP_TAC;
2542   REWRITE_TAC[ IN_BALL ];
2543   REWRITE_TAC[ dist ];
2544   REWRITE_TAC[VECTOR_ADD_RID;VECTOR_SUB_RZERO;VECTOR_ADD_LID;VECTOR_SUB_LZERO];
2545   REWRITE_TAC[ NORM_NEG ];
2546   BY(ASM_MESON_TAC[SUBSET])
2547 ]
2548 );;
2549   (* }}} *)
2550   end;;
2551
2552 help_grep "stv";;
2553
2554 dest_imp `a ==> b`;;
2555 REWR_CONV;;
2556 help "IMP_REWR_CONV";;
2557 help "net_of_thm";;
2558 help "mk_rewrites";;
2559 mk_rewrites false ADD_CLAUSES [];;
2560 help "REWRITES_CONV";;
2561 AUGMENT_SIMPSET;;
2562 help "RULE_ASSUM_TAC";;
2563 help "mk_prover";;
2564 help "lookup";;
2565 EQT_ELIM;;
2566 help "EQT_ELIM";;
2567 help "EQ_MP";;
2568 help "TOP_SWEEP_SQCONV";;
2569 help "rand";;
2570   type_of `nsum`;;
2571 help "DISCH";;
2572 help "MP";;
2573 help "GEN_PART_MATCH";;
2574 help_grep "mk_";;
2575 list_mk_exists;;
2576 help_grep "IMP";;
2577 help "IMP_TRANS";;
2578 help_grep "EXIST";;
2579 help "SIMPLE_EXISTS";;
2580 help "CHOOSE";;
2581 help "EXISTS";;
2582 SPEC_ALL;;
2583 help_grep "GEN";;
2584 help "GEN_ALL";;
2585 help_grep "exist";;
2586 help "mk_exists";;
2587 help "IMP";;
2588 help_grep "IMP";;
2589 help "EQ_IMP_RULE";;
2590 help "DISCH";;
2591 help "DISCH_ALL";;
2592 mk_rewrites;;
2593
2594 (map Merge_ineq.get_pack_nonlinear_non_ox3q1h ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";"QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW";]);;
2595
2596 Flyspeck_constants.calc `atn (sqrt (#3.07)) < pi - #2.089`;;
2597
2598 Oxl_merge.CELL_CLUSTER_ESTIMATE_PROPS;;
2599
2600   let smt_timeouts=
2601 ["6988401556";
2602 "7394240696";
2603 "8248508703";
2604 "7863247282";
2605 "3862621143 back";
2606 "3862621143 side";
2607 "8519146937";
2608 "4667071578";
2609 "5026777310";
2610 "OMKYNLT 1 2";
2611 "3296257235";
2612 "3862621143 front";
2613 "7761782916";
2614 "6944699408 a reduced";
2615 "7726998381";
2616 "4840774900";
2617 "MKFKQWU";
2618 "5451229371";
2619 "7931207804";
2620 "4652969746 1";
2621 "5405130650";
2622 "6224332984";
2623 "4240815464 a reduced";
2624 "3862621143 revised";
2625 "4491491732";
2626 "9563139965 f";
2627 "8082208587";
2628 "2065952723 A1";
2629 "9563139965 d";
2630 "8673686234 b";
2631 "3603097872";
2632 "1642527039";
2633 "1395142356";
2634 "OMKYNLT 3336871894"];;
2635
2636   let t1 =  map (fun t -> (t,List.length((Ineq.getexact t)))) smt_timeouts;;
2637 filter (fun (_,s) -> (s = 0)) t1;;
2638
2639 map Scripts.one_cfsqp smt_timeouts;;
2640
2641   'ID[4322269127]'
2642    'ID[5556646409]';;
2643
2644 (* Analysis of constants for Clarke, Gao, et al. *)
2645 (* moved to function_list.hl *)
2646
2647
2648  let tm1 = `domain6 (\x1 x2 x3 x4 x5 x6.
2649    &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
2650        &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
2651               dih5_x  (rotate5 dih_x)`;;
2652  let thm1 = UNDISCH (MATCH_MP domain6_assum (ASSUME tm1));;
2653
2654
2655 !help_path;;
2656 help_path := ["/Users/thomashales/Desktop/googlecode/hol-light/Help"; "$/Help"];;
2657 help "SPEC_ALL";;
2658
2659
2660
2661
2662
2663   let cons2 = (map (const_types o test) (0--30));;
2664   let cons2 = (map (const_types o test) (0--100));;
2665
2666 const_types (test 740);;
2667
2668
2669
2670 Flyspeck_lib.nub cons;;
2671 List.length i1;;
2672
2673 let has_matan =
2674   let z1 = zip p1 cons in
2675   map fst (filter (fun (_,c) -> mem "matan" c) z1);;
2676 let hss = map (fun t -> t.idv) has_matan;;
2677
2678 let testcase = "5202826650 a";;
2679
2680 let testcase = "7796879304";;
2681 let testcases = subtract hss ["7796879304"];;
2682 map (Auto_lib.testsplit true) testcases;;
2683
2684   let i2 = map (fun t -> t.ineq) (!Ineq.ineqs);;
2685   let ct2 = setify (List.flatten (map cxx i2));;
2686
2687   let ct3 = setify (ct2 @ ct1);;
2688
2689
2690   let p1 = !Prep.prep_ineqs;;
2691   let i1 = map (fun t -> t.ineq) p1;;
2692   let i1 =[ (find (fun t -> (t.idv = "2200527225")) p1).ineq];;
2693   hd i1;;
2694   let h1 =  (ASSUME (snd(strip_forall (List.nth i1 0))));;
2695   let test =
2696     let u = REWRITE_RULE
2697     [Nonlin_def.unit6;Sphere.rad2_x;Sphere.y_of_x;Sphere.rho_x;Sphere.delta_x;
2698      Sphere.ineq;Nonlin_def.sqrt_x1;Nonlin_def.sqrt_x2;Nonlin_def.sqrt_x3;
2699      Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x5;Nonlin_def.sqrt_x6;
2700      Sphere.vol_x;Sphere.gchi1_x;Sphere.gchi;Sphere.gchi2_x;Sphere.gchi3_x;
2701      Sphere.gchi4_x;Sphere.gchi5_x;Sphere.gchi6_x;
2702      Sphere.dih_x;Sphere.dih2_x;Sphere.dih3_x;Sphere.dih4_x;Sphere.dih5_x;
2703      Sphere.dih6_x;Sphere.dih_y;Sphere.dih2_y;Sphere.dih3_y;
2704      Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y;
2705      LET_DEF;LET_END_DEF;
2706      Sphere.delta_x4;Sphere.dih_x;Nonlin_def.unit6;
2707      Sphere.delta_y_LC;Sphere.delta_y;Nonlin_def.proj_x2;Nonlin_def.proj_x3;
2708      Mdtau.mdtau_y_LC;Mdtau.mdtau_y;Mdtau.mdtau2uf_y_LC;Mdtau.mdtau2uf_y;Sphere.rho;Sphere.ups_x;
2709      Sphere.ly;Mdtau.dua;Sphere.sol_y;Sphere.interp;
2710      Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x;Sphere.rhazim;Sphere.const1;
2711      Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y;
2712     ] h1 in
2713        (concl u);;
2714 Print_types.print_term_types test;;
2715
2716   let hs1 r =  (ASSUME (snd(strip_forall (List.nth (is1 (List.nth cases r)) 0))));;
2717   let h2 = REWRITE_RULE
2718     [Nonlin_def.unit6;Sphere.rad2_x;Sphere.y_of_x;Sphere.rho_x;Sphere.delta_x;
2719      Sphere.ineq;Nonlin_def.sqrt_x1;Nonlin_def.sqrt_x2;Nonlin_def.sqrt_x3;
2720      Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x4;Nonlin_def.sqrt_x5;Nonlin_def.sqrt_x6;
2721      Sphere.vol_x;Sphere.gchi1_x;Sphere.gchi;Sphere.gchi2_x;Sphere.gchi3_x;
2722      Sphere.gchi4_x;Sphere.gchi5_x;Sphere.gchi6_x;
2723      Sphere.dih_x;Sphere.dih2_x;Sphere.dih3_x;Sphere.dih4_x;Sphere.dih5_x;
2724      Sphere.dih6_x;Sphere.dih_y;Sphere.dih2_y;Sphere.dih3_y;
2725      Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y;
2726      LET_DEF;LET_END_DEF;
2727      Sphere.delta_x4;Sphere.dih_x;Nonlin_def.unit6;
2728      Nonlin_def.gamma3f_x_div_sqrtdelta;
2729      Nonlin_def.sub6;Nonlin_def.constant6;Nonlin_def.mul6;
2730      Nonlin_def.scalar6;Nonlin_def.add6;Nonlin_def.mk_456;
2731      Sphere.rotate4;Sphere.rotate5;Sphere.rotate6;
2732      Nonlin_def.uni;Nonlin_def.two6;Nonlin_def.proj_x4;Nonlin_def.proj_x5;
2733      Nonlin_def.proj_x6;Nonlin_def.compose6;
2734      Sphere.sol_euler_x_div_sqrtdelta;Nonlin_def.proj_y4;Nonlin_def.proj_y5;
2735      Nonlin_def.proj_y6;
2736
2737     ] (hs1 10);;
2738
2739 List.nth p1 3;;
2740 list_mk_conj;;
2741
2742 Nonlin_def.unit6;;
2743 Sphere.dih_x;;
2744
2745
2746 Sphere.atn2;;
2747
2748   let cxx i = setify (map fst (Print_types.get_const_types i));;
2749
2750   let p1 = !Prep.prep_ineqs;;
2751   let i1 = map (fun t -> t.ineq) p1;;
2752   let ct1 = setify (List.flatten (map cxx i1));;
2753
2754   let i2 = map (fun t -> t.ineq) (!Ineq.ineqs);;
2755   let ct2 = setify (List.flatten (map cxx i2));;
2756
2757   let ct3 = setify (ct2 @ ct1);;
2758
2759
2760 Nonlin_def.safesqrt;;
2761
2762 List.nth p1 3;;
2763 list_mk_conj;;
2764
2765 Nonlin_def.unit6;;
2766 Sphere.dih_x;;
2767
2768
2769 Sphere.atn2;;
2770
2771
2772 ct1;;
2773 List.length ct1;;
2774
2775 flyspeck_needs "../glpk/sphere.ml";;
2776 flyspeck_needs "nonlinear/check_completeness.hl";;
2777   let check_completeness_out = Check_completeness.execute();;
2778
2779
2780 (* bcc lattice revisited *)
2781
2782
2783
2784
2785 (* BCC LATTICE PROJECT *)
2786
2787 flyspeck_needs  "../projects_discrete_geom/bcc_lattice.hl";;
2788   let ineq_list  = ["EIFIOKD-a";"EIFIOKD-b";"EIFIOKD-c";"EIFIOKD1";"EIFIOKD2";"EIFIOKD3";"EIFIOKD4"];;
2789 let testid =   "EIFIOKD-a";;
2790
2791 let uu = (hd(Ineq.getexact testid)).ineq;;
2792     let vv = REWRITE_RULE
2793     [LET_DEF;LET_END_DEF;
2794      Bcc_lattice.selling_surface_nn;
2795      Bcc_lattice.selling_surface_num;
2796      Bcc_lattice.selling_volume2;
2797      Bcc_lattice.bcc_value;
2798     ] (ASSUME uu);;
2799
2800 Ineq.add {
2801   idv=(testid^"-test");
2802   ineq = (concl vv);
2803   doc = "BCC";
2804   tags = [];
2805 };;
2806
2807 1;;
2808
2809     let testid2 = testid^"-test";;
2810 Optimize.testsplit false testid2;;
2811 map (Optimize.testsplit true) !testids;;
2812
2813 (* END BCC *)
2814
2815 Auto_lib.terms_with_real_arity_ge8;;
2816 report Auto_lib.fn_code;;
2817 Auto_lib.tmpfile;;
2818  Optimize.preprocess_split_idq (hd(Ineq.getexact "test B1-100"));;
2819 Auto_lib.mkfile_code (all_forall `ineq [
2820     (&2,y1,#2.52);
2821     (&2,y2,#2.52);
2822     (&2,y3,#2.52);
2823       (#3.01,y4,#3.915);
2824    (#3.01,y5,#3.915);
2825       (#3.01,y6,#3.915)
2826   ]
2827   (( taum y1 y2 y3 y4 y5 y6 +
2828           y_of_x (mudLs_234_x (sqrt(&15)) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0
2829     > #0.712) \/
2830     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
2831     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
2832      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
2833 )`)   "X" [];;
2834
2835 itlist;;
2836 flyspeck_needs;;
2837 install_functions();;
2838 rflyspeck_needs "nonlinear/scripts.hl";;
2839
2840     let run s =
2841       let _ = Ineq.add s in
2842         Scripts.one_cfsqp s.idv;;
2843
2844     rflyspeck_needs   "nonlinear/auto_lib.hl";;
2845
2846     let run2 s =
2847       let _ = Ineq.add s in
2848         Auto_lib.testsplit true s.idv;;
2849
2850     let run2f s =
2851       let _ = Ineq.add s in
2852         Auto_lib.testsplit false s.idv;;
2853
2854 for i1=0 to 4 do
2855 for i2=i1 to 4 do
2856 for i3=i2 to 4 do
2857       run2 (make_hex_ear i1 i2 i3) done done done;;
2858
2859
2860     let r k = report (string_of_int k);;
2861 r 1;;
2862
2863 (*
2864 let is_sphere= new_definition`is_sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;
2865
2866
2867 let NULLSET_RULES2 = prove_by_refinement
2868  (`(!P. ((plane P)\/ (is_sphere P) \/ (circular_cone P)) ==> NULLSET P) /\
2869    (!(s:real^3->bool) t. (NULLSET s /\ NULLSET t) ==> NULLSET (s UNION t))`,
2870   [
2871     SIMP_TAC[NEGLIGIBLE_UNION] ;
2872     X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC;
2873     MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE ;
2874     SIMP_TAC[COPLANAR; DIMINDEX_3; ARITH] THEN ASM_MESON_TAC[SUBSET_REFL];
2875     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [is_sphere]) ;
2876     STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ;
2877     ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE];
2878     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [circular_cone]) ;
2879     REWRITE_TAC[EXISTS_PAIRED_THM; c_cone] THEN STRIP_TAC ;
2880     ASM_REWRITE_TAC[] ;
2881     MP_TAC(ISPECL [`w + v:real^3`; `v:real^3`; `r:real`]     NEGLIGIBLE_RCONE_EQ) ;
2882     ASM_REWRITE_TAC[rcone_eq; rconesgn] ;
2883     REWRITE_TAC[dist; VECTOR_ARITH `(w + v) - v:real^N = w`] ;
2884     ASM_REWRITE_TAC[VECTOR_ARITH `w + v:real^N = v <=> w = vec 0`]
2885   ]);;
2886
2887 let NULLSET_IS_SPHERE = prove_by_refinement
2888  (`(!P. is_sphere P ==> NULLSET P)`,
2889   [
2890     X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC;
2891     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [is_sphere]) ;
2892     STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ;
2893     ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE];
2894   ]);;
2895 *)
2896 1;;
2897
2898 add
2899 {
2900   idv="1347067436";
2901   doc="old name: local max v4*, WNLKGOQ, 1671775772 (with #0.12->#0.1)  8146670324
2902     better local max test.
2903     This is the numerator of the 2nd derivative of the function taud.
2904     Case delta > 20.";
2905   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2906   ineq = all_forall `ineq [
2907     (&2,y1,#2.52);
2908     (&2,y2,#2.52);
2909     (&2,y3,#2.52);
2910     (#3.01,y4,#3.237);
2911     (&2,y5,&2);
2912     (&2,y6,&2)
2913   ]
2914     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  > &0 \/
2915     y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  < &0 \/
2916     y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
2917        y_of_x taud_x y1 y2 y3 y4 y5 y6 > #0.12 \/
2918   delta_y y1 y2 y3 y4 y5 y6 < &20)`;
2919 };;
2920
2921 run
2922 {
2923   idv="test 8723570049";
2924   doc="local fan/main estimate/terminal pent
2925     y1=2.52, delta>=20, falls into taum>=0.12 case";
2926   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2927   ineq = all_forall `ineq [
2928     (#2.52,y1,#2.52);
2929     (&2,y2,#2.52);
2930     (&2,y3,#2.52);
2931     (#3.01,y4,#3.237);
2932     (&2,y5,&2);
2933     (&2,y6,&2)
2934   ]
2935 (taud y1 y2 y3 y4 y5 y6 > #0.12 \/
2936 delta_y y1 y2 y3 y4 y5 y6 < &20
2937 )`;
2938 };;
2939
2940
2941
2942 Calc_derivative.differentiate `f:real->real` `x:real` `(:real)`;;
2943 Calc_derivative.differentiate `\x. (f (x pow 2)):real`  `x:real` `(:real)`;;
2944
2945
2946
2947 run
2948   {
2949 idv = "test 22065952723 A1";
2950 doc = "This is the case that $a_2 \\le 15.53$.
2951    $a_2$ upper bound changed on 2011-Jan-21.
2952    If larger than 15.53, it must be in a hexagon,  and two consecutive straight vertices.
2953    Warning: this is verified by custom code (using cfsqp heuristics)
2954    in the interval arithmetic calculations.
2955    Fixed statement 2013-06-01.
2956  ";
2957 (* was (num_combo1 e1 e2 e3 a2 b2 c2 > &0)  *)
2958 tags=[Flypaper["UPONLFY"];Tex];
2959 ineq = Sphere.all_forall `ineq
2960   [
2961   (&1 , e1, &1 + sol0/ pi);
2962   (&1 , e2, &1 + sol0/ pi);
2963   (&1 , e3, &1 + sol0/ pi);
2964   ((&2 / h0) pow 2, a2, #15.53);
2965   ((&2 / h0) pow 2, b2, &4 pow 2);
2966   ((&2 / h0) pow 2, c2, &4 pow 2)
2967   ]
2968    ((num1 e1 e2 e3 a2 b2 c2) pow 2 > &0 \/
2969     num2 e1 e2 e3 a2 b2 c2 < &0)`;
2970 };;
2971
2972
2973 time;;
2974 List.length Check_completeness.r_init;; (* 15 *)
2975 List.length Check_completeness.triquad_assumption;; (* 3 *)
2976
2977
2978 Check_completeness.terminal_cs;;
2979 List.length Check_completeness.terminal_cs;;
2980 List.nth Check_completeness.terminal_cs 21;;
2981
2982 run
2983 {
2984   idv="2900061606";
2985   doc="triangle 1,2-ac";
2986   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2987   ineq = Sphere.all_forall `ineq [
2988     (&2,y1,#2.52);
2989     (#2.0,y2,#2.52);
2990     (&2,y3,#2.52);
2991     (&2,y4,&2);
2992     (#2.52,y5,#2.52);
2993       (#3.01,y6,#3.01)
2994   ]
2995 (
2996    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + (tame_table_d 2 1 - #0.11)
2997  )`;
2998 };;
2999
3000 run
3001 {
3002   idv="testx";
3003   doc="";
3004   tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
3005   ineq = Sphere.all_forall `ineq [
3006     (&2,y1,#2.52);
3007     (#2.0,y2,#2.52);
3008     (&2,y3,#2.52);
3009     (#3.01,y4,#3.915);
3010     (&2,y5,&2);
3011       (&2,y6,&2)
3012   ]
3013 (
3014    ups_x (y2*y2) (y3*y3) (y4*y4) * ups_x (y4*y4) (y5*y5) (y6*y6) > &0
3015  )`;
3016 };;
3017
3018 (*
3019 June 4, 2013:
3020
3021 3 long: 4010906068
3022 2 long: 6833979866
3023 1 long (out to sqrt8): 5541487347
3024
3025 deprecated:
3026 OMKYNLT ....
3027 7645170609;;
3028 *)
3029
3030 Ineq.getexact "5541487347";;
3031 open Terminal;;
3032
3033
3034
3035
3036 new_build_silent();;
3037
3038
3039
3040
3041 let old_then = ( THEN );;
3042 let old_prove = prove;;
3043 let old_prove_by_refinement = prove_by_refinement;;
3044
3045 old_then;;
3046
3047 let tactic_counter = ref [3];;
3048
3049 let new_prove_by_refinement(g,thml) =
3050   let _ = tactic_counter := (List.length thml :: !tactic_counter) in
3051     old_prove_by_refinement (g,thml);;
3052
3053 let prove_by_refinement = new_prove_by_refinement;;
3054
3055 rflyspeck_needs "packing/counting_spheres.hl";;
3056 let _ =
3057   let prove_by_refinement = new_prove_by_refinement in
3058     flyspeck_needs "packing/counting_spheres.hl";;
3059
3060 !tactic_counter;;
3061
3062 let tlist = (Lib.sort (<) !tactic_counter);;
3063 List.length tlist;;
3064 List.nth (Lib.sort (<) tlist) (188 / 2);;
3065
3066 end_itlist (+) tlist;;
3067
3068 (end_itlist (+) ) (snd (chop_list (188 /2) tlist));;
3069
3070
3071 let all_forall = Sphere.all_forall;;
3072
3073
3074 run2
3075 {
3076   idv="8495326405";
3077   doc=" Main estimate/quad case.
3078    ";
3079   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
3080   ineq = all_forall `ineq [
3081     (&2,y1,&2);
3082     (&2,y2,&2);
3083     (#3.01,y3,&6);
3084     (&2,y4,&2);
3085     (&2 * h0,y5,&2 * h0);
3086       (#3.01,y6,&6)
3087   ]
3088   ( delta_y y1 y2 y3 y4 y5 y6 < &0)`;
3089 };;
3090
3091
3092 run
3093 {
3094   idv="test 8748498390";
3095   doc=" 0.513 estimate, A-piece triangle.
3096    One diagonal exactly 3.01. Added 2013-06-13";
3097   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
3098   ineq = all_forall `ineq [
3099     (&2,y1,#2.1);
3100     (&2,y2,#2.52);
3101     (&2,y3,#2.52);
3102     (&2,y4,#2.52);
3103     (#2.52,y5,#3.01);
3104       (#3.01,y6,#3.01)
3105   ]
3106   ( taum y1 y2 y3 y4 y5 y6  + #0.12 * (y1 - &2) > #0.403 )`;
3107 };;
3108
3109 run
3110 {
3111   idv="test 2445657182";
3112   doc=" 0.513 estimate. ear. Combine with 8748498390 along diagonal 3.01.
3113     Added 2013-06-13.";
3114   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
3115   ineq = all_forall `ineq [
3116     (&2,y1,#2.52);
3117     (&2,y2,#2.52);
3118     (&2,y3,#2.52);
3119     (&2,y4,#2.52);
3120     (&2,y5,#2.52);
3121       (#3.01,y6,#3.01)
3122   ]
3123   ( taum y1 y2 y3 y4 y5 y6   > #0.11 + #0.12 * (y1 - &2))`;
3124 };;
3125
3126 (*  + #0.5 * (#3.01 - y6) ;; *)
3127
3128 run
3129 {
3130   idv="test 2445657182";
3131   doc=" 0.513 estimate. ear. Combine with 8748498390 along diagonal 3.01.
3132     Added 2013-06-13.";
3133   tags=[Flypaper["FHOLLLW"];Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
3134   ineq = all_forall `ineq [
3135     (&1,y1,&1);
3136     (&2,y2,#2.52);
3137     (&2,y3,#2.52);
3138     (sqrt8,y4,#3.0);
3139     (&2,y5,#2.52);
3140       (&2,y6,#2.52)
3141   ]
3142   ( delta_y (&0) y2 y3 y4 y5 y6 > &0 )`;
3143 };;
3144
3145 add
3146 {
3147   idv="test";
3148   doc= "Used with 5691615370.
3149     Added 2013-06-19.";
3150   tags=[Cfsqp;Xconvert;Tex;Lp_aux "5691615370";Penalty(50.0,500.0)];
3151   ineq = all_forall `ineq [
3152     (&3,y1,&4 * h0);
3153     (&2,y2,#2.472);
3154     (&2,y3,#2.472);
3155     (&3,y4,&4 * h0);
3156     (&2,y5,#2.472);
3157       (&2,y6,#2.472)
3158   ]
3159   ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )`;
3160 };;
3161
3162 add
3163 {
3164   idv="test";
3165   doc= "";
3166   tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
3167   ineq = all_forall `ineq [
3168     (&3,y1,&4 * h0);
3169     (&2,y2,#2.472);
3170     (&2,y3,#2.472);
3171     (&3,y4,&4 * h0);
3172     (&2,y5,#2.472);
3173       (&2,y6,#2.472)
3174   ]
3175   (  delta_y y1 y2 y3 y4 y5 y6 < &200 )`;
3176 };;
3177
3178
3179
3180 let eta2_126 = new_definition `eta2_126 x1 (x2:real) (x3:real) (x4:real) (x5:real) x6 =
3181   (eta_y (sqrt x1) (sqrt x2) (sqrt x6)) pow 2`;;
3182
3183 Functional_equation.functional_overload();;
3184
3185 let nonf_ups_126 = prove_by_refinement(
3186   `!x1 x2 x3 x4 x5 x6. ups_126 x1 x2 x3 x4 x5 x6 = ups_x x1 x2 x6`,
3187   (* {{{ proof *)
3188   [
3189   REWRITE_TAC[Nonlin_def.ups_126];
3190   BY(Functional_equation.F_REWRITE_TAC)
3191   ]);;
3192   (* }}} *)
3193
3194
3195 searcht 5 [`BB1`];;
3196
3197 let t =  `V = IMAGE vv (:num)`;;
3198     let (a,b) = dest_eq t ;;
3199     let b' = env (top_realgoal())  b ;;
3200     let a' = tysubst [type_of b',type_of a] a ;;
3201     type_of a';;
3202     type_of b';;
3203     type_of b;;
3204     let t' = mk_eq (a',b') ;;
3205       ABBREV_TAC t' (asl,w);;
3206
3207 top_goal();;
3208 inst;;
3209
3210     type_of (inst [`:B`,`:A`] `x:A`);;
3211
3212 help "inst";;
3213 help "type_subst";;
3214 help "tysubst";;
3215 help "instantiate";;
3216
3217     let t =
3218     let (a,b) = dest_eq t ;;
3219     let b' = env (asl,w) b ;;
3220     let (a',_) = dest_var a ;;
3221     let t' =   mk_eq(mk_var(a',type_of b'),b');;
3222 type_of t';;
3223
3224 ABBREV_TAC t' (asl,w);;
3225
3226
3227
3228 run
3229 {
3230   idv="4887115291";
3231   doc="old name: angles pent*
3232     Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
3233   ";
3234   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3235   ineq = all_forall `ineq [
3236     (&2,y1,#2.52);
3237     (&2,y2,#2.52);
3238     (&2,y3,#2.52);
3239     (#3.01,y4,#3.01);
3240     (&2,y5,&2);
3241     (&2,y6,&2)
3242   ]
3243 (  #1.75 < dih_y y1 y2 y3 y4 y5 y6
3244 )`;
3245 };;
3246
3247 run
3248 {
3249   idv="6789182745";
3250   doc="old name: test A*
3251    Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
3252   ";
3253   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3254   ineq = Sphere.all_forall `ineq [
3255     (&2,y1,#2.52);
3256     (&2,y2,#2.52);
3257     (&2,y3,#2.52);
3258     (&2,y4,&2);
3259       (#3.01,y5,#3.237);
3260     (#3.01,y6,#3.237)
3261   ]
3262 (
3263      (dih_y y1 y2 y3 y4 y5 y6 < #1.109)
3264  )`;
3265 };;
3266
3267 run
3268 {
3269   idv="3405144397-numerical";
3270   doc="old name: test8*
3271    Local-fan/Main-estimate/terminal-pent/both-ears-under-20.
3272    ear dih inequality when delta < 20";
3273   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
3274   ineq = all_forall `ineq [
3275     (&2,y1,#2.52);
3276     (&2,y2,#2.52);
3277     (&2,y3,#2.52);
3278     (&2,y4,&2);
3279       (&2,y5,&2);
3280     (#3.01,y6,#3.237)
3281   ]
3282 (
3283   (delta_y y1 y2 y3 y4 y5 y6 > &20)  \/
3284      (dih_y y1 y2 y3 y4 y5 y6 < (#1.75 - #1.109) / &2) \/
3285   (delta_y y1 y2 y3 y4 y5 y6 < &0)
3286  )`;
3287 };;
3288
3289 run
3290 {
3291   idv="test 3405144397";
3292   doc="ear dih ineq when delta < 20.
3293    Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
3294     Adaptation of 9459075374.
3295     (EAR) A bound on the delta of an ear in a pent,
3296    The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.3205 = (1.75-1.109)/2)  has been 'linearized'.
3297    Tan[0.3205]^2 = (>=) 0.110186
3298    In more detail, this calc shows that delta > 20 or dih < 0.3205
3299    By 4887115291, we know that the combined angle at the crowded node of a pent is
3300    at least 1.75.  If both ears have delta < 20, then combined angle
3301    is at least 1.109 + 2 * 0.3205 = 1.75, so a cross diag <= 3.01.
3302    Hence wlog one of the two ears has delta >= 20.
3303    ";
3304   tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
3305   ineq = all_forall `ineq [
3306     (&2,y1,#2.52);
3307     (&2,y2,#2.52);
3308     (&2,y3,#2.52);
3309     (&2,y4,&2);
3310      (#3.01,y5,#3.237);
3311       (&2,y6,#2.52)
3312   ]
3313 (let tan2lower = #0.110186 in
3314    (delta_y y1 y2 y3 y4 y5 y6 > &20) \/
3315   (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
3316  )`;
3317 };;
3318
3319     let all_forall = Sphere.all_forall;;
3320
3321
3322 List.length remain;;
3323
3324         (filter Merge_ineq.is_ox3q1h (!Ineq.ineqs));;
3325
3326            Merge_ineq.packing_ineq_data;;
3327
3328 Ysskqoy.pack_ineq_def_a;;
3329
3330
3331 Script.unfinished_cases();;
3332 searcht 5 [def "deformation"];;
3333
3334 g Appendix.NUXCOEAv2_concl;;
3335
3336 let NUXCOEAv2=prove_by_refinement((Appendix.NUXCOEAv2_concl),
3337 MP_TAC Nuxcoea.NUXCOEA
3338  ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
3339 mt[]
3340 st/r
3341 fxa mmp
3342 typ `j` ex
3343 rule (orr[EQ_SYM_EQ])
3344 art[]
3345 THEN MESON_TAC[]);;
3346
3347 g Appendix.IMJXPHRv2_concl;;
3348
3349 let IMJXPHRv2=prove((Appendix.IMJXPHRv2_concl),
3350 MP_TAC Imjxphr.IMJXPHR
3351  ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
3352 mt[]
3353   THEN
3354  MESON_TAC[]);;
3355
3356 g Appendix.ODXLSTCv2_concl;;
3357
3358 let ODXLSTCv2=prove((Appendix.ODXLSTCv2_concl),
3359 MP_TAC Odxlstcv2.ODXLSTCv2
3360  ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
3361 st/r
3362 fxa (C intro [`s`;`k`;`w`;`l`])
3363 rt[]
3364 amt[]
3365
3366 art[]
3367
3368 rt[]
3369 mt[]
3370
3371
3372 THEN MESON_TAC[]);;
3373
3374 Appendix.NUXCOEAv2_concl;;
3375
3376 module Test = struct
3377
3378   open Imjxphr;;
3379   open Nuxcoea;;
3380
3381 let NUXCOEAv2=prove((Appendix.NUXCOEAv2_concl),
3382 MP_TAC NUXCOEA
3383 THEN ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
3384 THEN MESON_TAC[]);;
3385
3386
3387 let IMJXPHRv2=prove((Appendix.IMJXPHRv2_concl),
3388 MP_TAC IMJXPHR
3389 THEN ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC]
3390 THEN MESON_TAC[]);;
3391
3392
3393 let ODXLSTCv2=prove_by_refinement((Appendix.ODXLSTCv2_concl),
3394 [
3395   MP_TAC Odxlstcv2.ODXLSTCv2;
3396   ASM_REWRITE_TAC[Lunar_deform.MHAEYJN;Zlzthic.ZLZTHIC];
3397   REWRITE_TAC[];
3398   REPEAT WEAKER_STRIP_TAC;
3399   FIRST_X_ASSUM (C INTRO_TAC [`s`;`k`;`w`;`l`]);
3400   REWRITE_TAC[];
3401   BY(ASM_MESON_TAC[])
3402 ]);;
3403
3404
3405                                   end;;
3406
3407 searcht 5 [`arclength`;`atn`];;
3408
3409 let arclength222h0 = prove_by_refinement(
3410   `arclength (&2) (&2) (&2 * h0) < pi / &2`,
3411   (* {{{ proof *)
3412   [
3413   GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1;
3414   CONJ_TAC;
3415     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
3416     REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
3417     BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
3418   REWRITE_TAC[arith `x + y < x <=> y < &0`];
3419   ONCE_REWRITE_TAC[GSYM ATN_0];
3420   MATCH_MP_TAC ATN_MONO_LT;
3421   REWRITE_TAC[arith `(x / y < &0 <=> &0 < (-- x)/ y)`];
3422   GMATCH_SIMP_TAC REAL_LT_DIV;
3423   GMATCH_SIMP_TAC SQRT_POS_LT;
3424   REWRITE_TAC[Sphere.h0];
3425   BY(REAL_ARITH_TAC)
3426   ]);;
3427   (* }}} *)
3428
3429 let arclength_2h0_cstab = prove_by_refinement(
3430   `arclength (&2) (&2) (&2 *h0) + arclength (&2) (&2) cstab < pi`,
3431   (* {{{ proof *)
3432   [
3433   REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
3434   REWRITE_TAC[GSYM CONJ_ASSOC];
3435   CONJ_TAC;
3436     BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
3437   CONJ_TAC;
3438     BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
3439   REWRITE_TAC[arith `(pi/ &2 + b) + (pi / &2 + d) < pi <=> b + d < &0`];
3440   REWRITE_TAC[Sphere.h0;Sphere.cstab];
3441   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`);
3442   BY(REWRITE_TAC[])
3443   ]);;
3444   (* }}} *)
3445
3446 run
3447   {
3448     idv="test 6843920790";
3449     doc = "In a pentagon with one long edge, we can contract the long edge to 2.52,
3450    or even to 2, using 2 diags.
3451    The constant 2.38 < 3.01/h0.";
3452     tags=[];
3453   ineq = Sphere.all_forall `ineq
3454       [
3455         (&1 , e1, &1 + sol0/ pi);
3456         (&1 , e2, &1 + sol0/ pi);
3457         (&1 , e3, &1 + sol0/ pi);
3458         ((&2 / h0) pow 2, a2, #2.52 pow 2);
3459         (#2 pow 2, b2, #15.53);
3460         ((#3.01/ #1.26) pow 2, c2, #15.53)
3461       ]
3462       ((num1 e1 e2 e3 a2 b2 c2  > &0) ) `;
3463   };;
3464
3465 help_grep "strip";;
3466 let thm = Localization.deformation;;
3467
3468 let c = fst(dest_const (fst (strip_comb (fst (dest_eq (snd (strip_forall (concl thm))))))));;
3469
3470 (* TRIAL DEFINITION *)
3471
3472 let deflist = ref [];;
3473
3474 let adddef thm =
3475   let c = fst(dest_const (fst (strip_comb (fst (dest_eq (snd (strip_forall (concl thm)))))))) in
3476   let _ = deflist := (c,thm)::!deflist in
3477     c;;
3478
3479 let getd s =
3480   try assoc s (!deflist)
3481   with _ -> failwith ("definition "^s^" not found");;
3482
3483 List.length !proof_record;;
3484 hd !proof_record;;
3485
3486
3487 bb;;
3488 find;;
3489 index;;
3490
3491
3492 Searching.searcht 5 [`!f g x.
3493             f continuous at x /\ g continuous at x
3494             ==> (\x. lift (f x dot g x)) continuous at x`];;
3495 Searching.searcht 5 [`T`];;
3496
3497 module Xx = struct
3498   open Hales_tactic;;
3499 let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
3500   `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
3501             ==> (\x. (f x dot g x)) real_continuous atreal x`,
3502   (* {{{ proof *)
3503   [
3504   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
3505   REPEAT WEAKER_STRIP_TAC;
3506   TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
3507     BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
3508   INTRO_TAC CONTINUOUS_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`];
3509   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);
3510     BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
3511   BY(ASM_REWRITE_TAC[GSYM Xbjrphc.CONTINUOUS_CONTINUOUS_ATREAL])
3512   ]);;
3513   (* }}} *)
3514 end;;
3515
3516 let CONTINUOUS_LIFT_DOT2 = prove
3517  (`!net f:A->real^N g.
3518         f continuous net /\ g continuous net
3519         ==> (\x. lift(f x dot g x)) continuous net`,
3520   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
3521    [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
3522   BILINEAR_CONTINUOUS_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;
3523
3524 (*
3525 let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
3526   `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
3527             ==> (\x. (f x dot g x)) real_continuous atreal x`,
3528   (* {{{ proof *)
3529   [
3530   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
3531   REPEAT WEAKER_STRIP_TAC;
3532   TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
3533     BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
3534   INTRO_TAC CONTINUOUS_AT_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`];
3535   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);
3536     BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
3537   BY(ASM_REWRITE_TAC[GSYM (* Xbjrphc. *) CONTINUOUS_CONTINUOUS_ATREAL])
3538   ]);;
3539   (* }}} *)
3540 *)
3541
3542 module Test = struct
3543   open Hales_tactic;;
3544 let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
3545   `!(f:real->real^A) g x.  f continuous atreal x /\ g continuous atreal x
3546             ==> (\x. (f x dot g x)) real_continuous atreal x`,
3547   (* {{{ proof *)
3548   [
3549   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
3550   REPEAT WEAKER_STRIP_TAC;
3551   TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
3552     BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
3553   MATCH_MP_TAC CONTINUOUS_LIFT_DOT2;
3554   ASM_REWRITE_TAC[];
3555   ]);;
3556   (* }}} *)
3557 end;;
3558
3559
3560 proof_record := [];;
3561
3562 String.length "  REPEAT GEN_TAC;
3563   ASM_CASES_TAC `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`;
3564     BY(ASM_MESON_TAC[]);
3565   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
3566   ASM_CASES_TAC `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`;
3567     BY(ASM_MESON_TAC[]);
3568   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT STRIP_TAC;
3569   GEXISTL_TAC [`x1`;`x2`];
3570   BY(GEN_TAC THEN ASM_TAC THEN CONV_TAC REAL_RING)";;
3571
3572 String.length "g/r
3573 asmcs `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`
3574 amt[]
3575 fx mp then rt[] then str/r
3576 asmcs `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`
3577 amt[]
3578 fx mp then rt[NOT_FORALL_THM] then str/r
3579 exl [`x1`;`x2`]
3580 g then asm then cvc REAL_RING";;
3581
3582 233.0 /. 414.0;;
3583
3584
3585 (* BUGGY BEHAVIOR *)
3586 can (term_match [] `((f:A->B) ((v:num->A) 2))`) `((f:A->B) ((v:num->A) 7))`;;
3587
3588 can (term_match [] `(f:num->A) 2`) `(f:num->A) 7`;;
3589
3590 run
3591   {
3592     idv="test";
3593     doc = "";
3594     tags=[];
3595   ineq = Sphere.all_forall `ineq
3596       [
3597          (&2,y1,&2 * h0);
3598          (&2,y2,&2 * h0);
3599          (&2,y3,&2 * h0);
3600          (#3.42,y4,#3.42);
3601          (&2,y5,#3.01);
3602          (&2,y6,&2)]
3603
3604       ((dih_y y1 y2 y3 y4 y5 y6  > pi / &2) ) `;
3605   };;
3606
3607 run
3608   {
3609     idv="test";
3610     doc = "";
3611     tags=[];
3612   ineq = Sphere.all_forall `ineq
3613       [
3614          (&2,y1,&2 * h0);
3615          (&2,y2,&2 * h0);
3616          (&2,y3,&2 * h0);
3617          (#3.01,y4,#3.42);
3618          (&2,y5,#3.01);
3619          (#3.01,y6,#3.9)]
3620
3621       ((delta_y y1 y2 y3 y4 y5 y6  > &0)  \/
3622       arclength y1 y2 y6 > #2.8) `;
3623   };;
3624
3625 Sphere.h0;;
3626
3627 let s = "test";;
3628 Ineq.getexact "test";;
3629 let v1 = hd(Ineq.getexact s);;
3630 let v2 = List.length (fst (strip_forall (v1.ineq)));;
3631
3632 (* analysis of cases with more than 6 variables *)
3633
3634 let numvars s =
3635   let v1 = hd (Ineq.getexact s) in
3636     List.length (fst (strip_forall (v1.ineq)));;
3637
3638 let ineqnames = map (fun idq -> idq.idv) (!Ineq.ineqs);;
3639
3640 filter (fun s -> numvars s > 6) ineqnames;;
3641
3642 let manyvars = ["9507202313"; "4680581274 delta issue"; "4680581274 a"; "9563139965D";
3643    "3862621143 revised"; "4240815464 a"; "6944699408 a"; "7043724150 a"];;
3644
3645 map numvars manyvars;;
3646
3647
3648 1;;
3649
3650 map (fun t -> t.idv) (Ineq.getfield Onlycheckderiv1negative);;
3651
3652 map (fun t -> t.idv) (filter (fun t -> Optimize.has_cross_diag (t.ineq)) !Prep.prep_ineqs);;
3653  ["7043724150 a"; "6944699408 a"; "4240815464 a"; "3862621143 revised";
3654    "4680581274"; "4680581274 delta issue"; "7697147739";
3655    "7697147739 delta issue"; "9507202313"];;
3656 2;;
3657
3658 Ineq.getexact "4680581274 a";;
3659
3660 run2 {ineq =
3661      `!y1 y2 y3 y4 y5 y6 y7 y8 y9.
3662           ineq
3663           [ #2.0,y1,&2 * h0;  #2.0,y2,&2 * h0;  #2.0,y3,&2 * h0;  #3.01,
3664                                                                  y4,
3665                                                                   #3.166;
3666            #2.0,
3667           y5,
3668           &2;  #2.0,y6,&2;  #2.0,y7,&2 * h0;  #2.0,y8,&2;  #3.01,y9, #3.01]
3669           (tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 >  #0.513 \/
3670            delta_y y1 y2 y3 y4 y5 y6 < &10 \/
3671            delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
3672            enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 <  #3.01)`;
3673     idv = "test 4680581274 a";
3674     doc =
3675      "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.";
3676     tags =
3677      [Flypaper ["FHOLLLW"]; Main_estimate; Cfsqp; Quad_cluster 10000.0;
3678       Xconvert; Tex; Penalty (50., 5000.)]};;
3679
3680 module Am = Pervasives;;
3681
3682 let (x0,z0) =  ([0.0;0.0;0.0],[1.0;4.0;3.0]);;
3683 let avoid0 =  [];;
3684   let w0 = map (fun (xi,zi) -> zi -. xi) (zip x0 z0);;
3685   let avoid_filter = map (fun i -> (mem i avoid0)) (0--(List.length x0 - 1));;
3686   let w' = map (fun (t,b) -> if b then 0.0 else t) (zip w0 avoid_filter);;
3687   let wm = maxlist w' ;;
3688     index wm w';;
3689
3690 let arclength_lt_1553 = prove_by_refinement(
3691   `&2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2) (sqrt(#15.53))`,
3692   (* {{{ proof *)
3693   [
3694   REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
3695   GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
3696   REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
3697   REWRITE_TAC[arith `x + &2 - &2 = x`];
3698   REWRITE_TAC[Sphere.h0];
3699   TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C SUBGOAL_THEN ASSUME_TAC);
3700     GMATCH_SIMP_TAC REAL_LT_RSQRT;
3701     CONJ_TAC;
3702       BY(REAL_ARITH_TAC);
3703     MATCH_MP_TAC REAL_LT_LSQRT;
3704     BY(REAL_ARITH_TAC);
3705   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);
3706     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
3707   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))` );
3708   BY(REWRITE_TAC[])
3709   ]);;
3710   (* }}} *)
3711
3712
3713 run
3714   {
3715     idv="testA";
3716     doc = "";
3717     tags=[];
3718   ineq = Sphere.all_forall `ineq
3719       [
3720          (&2,y1,&2);
3721          (&2,y2,&2);
3722          (&2,y3,&2);
3723          (#3.01,y4,#3.01);
3724          (#3.01,y5,#3.01);
3725          (&2,y6,#2.52)]
3726       ((dih_y y1 y2 y3 y4 y5 y6  > pi / &2) ) `;
3727   };;
3728
3729
3730
3731 run2
3732   {
3733     idv="test 1348932091"; (* was "testB"; *)
3734     doc = "";
3735     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
3736   ineq = Sphere.all_forall `ineq
3737       [
3738          (&2,y1,&2);
3739          (&2,y2,#2.52);
3740          (&2,y3,#2.52);
3741          (#2.52,y4,#2.52);
3742          (#3.01,y5,#3.3);
3743          (&2,y6,#2.52)]
3744       ((dih_y y1 y2 y3 y4 y5 y6  < #1.4) ) `;
3745   };;
3746
3747
3748 run
3749   {
3750     idv= "test 5557288534"; (* was "testC"; *)
3751     doc = "";
3752     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
3753   ineq = Sphere.all_forall `ineq
3754       [
3755          (&2,y1,&2);
3756          (&2,y2,#2.52);
3757          (&2,y3,#2.52);
3758          (#3.01,y4,#3.01);
3759          (#3.01,y5,#3.3);
3760          (&2,y6,#2.52)]
3761       ((dih_y y1 y2 y3 y4 y5 y6  < #1.7) ) `;
3762   };;
3763
3764 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
3765 needs "../formal_lp/hypermap/computations/list_hypermap_computations.hl";;
3766
3767 needs "../formal_lp/hypermap/verify_all.hl";;
3768 Verify_all.init_ineqs();;
3769 let result = Verify_all.verify_file (flyspeck_dir ^"/../formal_lp/glpk/binary/easy_onepass_1.dat");;
3770 hd (fst result);;
3771
3772 (*
3773 val it : thm = lp_ineqs, lp_main_estimate,
3774   iso (hypermap_of_fan (V,ESTD V))
3775   (hypermap_of_list
3776   [['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]])
3777   |- contravening V ==> F
3778 *)
3779 type_of `hypermap_of_fan`;;
3780 type_of `hypermap_of_list`;;
3781 result;;
3782 hd(fst result);;
3783 type_of `['0;'1;'2]`;;
3784
3785 run2f (hd(Ineq.getexact "7550003505 0 1 3"));;
3786
3787 Print_types.get_const_types;;
3788
3789
3790
3791
3792 let tab =
3793 [`norm2hh (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3794      norm2hh_x x1 x2 x3 x4 x5 x6 `;
3795 `rad2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3796      rad2_x x1 x2 x3 x4 x5 x6 `;
3797 `delta4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3798      delta_x4 x1 x2 x3 x4 x5 x6 `;
3799 `delta4_y (sqrt x7) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x8) (sqrt x9) =
3800    delta_x4 x7 x2 x3 x4 x8 x9 `;
3801 `dih2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3802      dih2_x x1 x2 x3 x4 x5 x6 `;
3803 `dih3_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3804     dih3_x x1 x2 x3 x4 x5 x6 `;
3805 `dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3806      dih_x x1 x2 x3 x4 x5 x6 `;
3807 `dih4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3808     dih4_x x1 x2 x3 x4 x5 x6 `;
3809 `dih5_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3810    dih5_x x1 x2 x3 x4 x5 x6 `;
3811 `dih6_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3812    dih6_x x1 x2 x3 x4 x5 x6 `;
3813 `delta_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3814    delta_x x1 x2 x3 x4 x5 x6 `;
3815 `delta_y (sqrt x7) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x8) (sqrt x9) =
3816    delta_x x7 x2 x3 x4 x8 x9`;
3817 `vol_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
3818    vol_x x1 x2 x3 x4 x5 x6 `;
3819 `eta_y (sqrt x1) (sqrt x2) (sqrt x6) pow 2 = eta2_126 x1 x2 x3 x4 x5 x6 `;
3820 `eta_y (sqrt x1) (sqrt x3) (sqrt x5) pow 2 = eta2_135 x1 x2 x3 x4 x5 x6 `;
3821 `eta_y (sqrt x4) (sqrt x5) (sqrt x6) pow 2 = eta2_456 x1 x2 x3 x4 x5 x6 `;
3822 `vol3f (sqrt x1) (sqrt x2) (sqrt x6)  sqrt2 lfun = vol3f_x_lfun x1 x2 x3 x4 x5 x6 `;
3823 `vol_y sqrt2 sqrt2 sqrt2 (sqrt x1) (sqrt x2) (sqrt x6)  = vol3_x_sqrt x1 x2 x3 x4 x5 x6 `;
3824 `vol3f_sqrt2_lmplus (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)      (sqrt x6) =
3825    vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6`;
3826  ];;
3827
3828 let tab1 = List.nth tab 0;;
3829 fst (strip_comb (fst(dest_eq tab1)));;
3830
3831