text_formalization/nonlinear/optimize.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: nonlinear inequalities                                            *)
   5 (* Author:  Thomas Hales     *)
   6 (* Date: 2010-08-30                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11 Input is a nonlinear inequality.
  12 preprocess_split_idq generates cases and does general preprocessing.
  13 Output is executable interval arithmetic code in C++.
  14 *)
  15
  16 (*
  17 flyspeck_needs "general/sphere.hl";;
  18 flyspeck_needs "nonlinear/ineq.hl";;
  19 flyspeck_needs "nonlinear/lemma.hl";;
  20 *)
  21
  22 module Optimize = struct
  23
  24 open Lib;;
  25 open Nonlinear_lemma;;
  26
  27
  28 let length = List.length;;
  29
  30
  31 let svn_version = Flyspeck_lib.svn_version;;
  32
  33 let ineq = Sphere.ineq;;
  34 let all_forall = Sphere.all_forall;;
  35 let add = Ineq.add;;
  36
  37
  38 let nub = Flyspeck_lib.nub;;
  39
  40 let join_comma = Flyspeck_lib.join_comma;;
  41 let join_space = Flyspeck_lib.join_space;;
  42 let join_lines = Flyspeck_lib.join_lines;;
  43
  44 let string_of_num' = Flyspeck_lib.string_of_num';;
  45 let dest_decimal = Flyspeck_lib.dest_decimal;;
  46
  47 let strip_let_tm = Nonlinear_lemma.strip_let_tm;;
  48
  49 let output_filestring = Flyspeck_lib.output_filestring;;
  50
  51 let BY = Hales_tactic.BY;;
  52 let unlist = Hales_tactic.unlist;;
  53
  54 (* from glpk_link.ml *)
  55
  56 let load_and_close_channel_true = Flyspeck_lib.load_and_close_channel_true;;
  57
  58 let load_file = Flyspeck_lib.load_file;;
  59
  60 (* ========================================================================= *)
  61 (*    GENERAL PROCEDURES                                                  *)
  62 (* ========================================================================= *)
  63
  64 (* The marker NONLIN is used in mk_all_ineq.hl,
  65    where it is replaced with a constant equivalent to the conjunction of all the
  66    nonlinear ineqs.   *)
  67
  68 let NONLIN = new_definition `NONLIN = T`;;
  69
  70 let FROZEN_REWRITE_TAC ths =
  71    if (ths=[]) then REWRITE_TAC [] else
  72      let th = end_itlist CONJ ths in
  73       FREEZE_THEN (fun t -> REWRITE_TAC[t]) th;;
  74
  75 let quoted s = let q = "\"" in (q^s^q);;
  76
  77 let paren s = "("^ s ^")";;
  78
  79 let real_ty = `:real`;;
  80 let mk_x i = mk_var("x"^string_of_int i,real_ty);;
  81
  82 let x9list =  map mk_x (1--9);;
  83 let x6list = map mk_x (1--6);;
  84 let x_backlist = map mk_x [7;2;3;4;8;9];;
  85
  86 let xspec = SPECL x6list;;
  87
  88
  89 let dest_ineq ineq =
  90   let t = snd(strip_forall ineq) in
  91   let (vs,i) = dest_comb t in
  92   let (_,vs) = dest_comb vs in
  93   let vs = dest_list vs in
  94   let vs = map (fun t -> let (a,b) = dest_pair t in (a,dest_pair b)) vs in
  95   let vs = map (fun (a,(b,c)) -> (a, b, c)) vs in
  96     (t,vs,disjuncts i);;
  97
  98 (* renames variables as x1,x2,x3,.... *)
  99
 100 let (X_RENAME_TAC:tactic) =
 101    fun  gl  ->
 102      let (_,loc,_) = dest_ineq (goal_concl gl) in
 103      let loc' = map (fun (_,b,_) -> b) loc in
 104      let xvar = map mk_x (1 -- (length loc')) in
 105        EVERY (map SPEC_TAC (zip loc' xvar)) gl ;;
 106
 107
 108 (* ========================================================================= *)
 109 (*    SPLITTING INEQUALITIES AT h0                                           *)
 110 (* ========================================================================= *)
 111
 112 let get_split_tags idq =
 113   let ts = idq.tags in
 114   let rec gs = (function
 115     | [] -> []
 116     | (Split a::_) -> a
 117     | _ :: rs -> gs rs) in
 118     gs ts;;
 119
 120 let split_2h0 =
 121   let split_interval = prove(
 122     `! a b (y:real). (a <= y /\ y <= b) ==>
 123       ((a <= y /\ y <= m) \/ (m <= y /\ y <= b) )
 124       `,  REAL_ARITH_TAC) in
 125     INST [(`&2 * h0`,`m:real`)] split_interval;;
 126
 127 let split_2h0_strict =
 128   let split_interval = prove(
 129     `! a b (y:real). (a <= y /\ y <= b) ==>
 130       ((a <= y /\ y <= m) \/ (m < y /\ y <= b) )
 131       `,  REAL_ARITH_TAC) in
 132     INST [(`&2 * h0`,`m:real`)] split_interval;;
 133
 134
 135 (*  changed 2012-06-20
 136 let SPLIT_H0_TAC pos =
 137  (REPEAT GEN_TAC) THEN
 138  (REWRITE_TAC[ineq_expand6]) THEN
 139  (REPLICATE_TAC (pos) DISCH_TAC) THEN
 140  (DISCH_THEN (fun t -> MP_TAC (MATCH_MP split_2h0 t))) THEN
 141  DISCH_THEN DISJ_CASES_TAC    THEN
 142  (REPEAT (POP_ASSUM MP_TAC)) THEN
 143  (REWRITE_TAC[GSYM ineq_expand6]);;
 144 *)
 145
 146
 147 let h0cutA = prove_by_refinement(
 148   `!y. (y <= &2 * h0) ==> ((h0cut y) = &1)`,
 149   (* {{{ proof *)
 150   [
 151   MESON_TAC[Sphere.h0cut]
 152   ]);;
 153   (* }}} *)
 154
 155 let h0cutB = prove_by_refinement(
 156   `!y. (&2 * h0 < y) ==> ((h0cut y) = &0)`,
 157   (* {{{ proof *)
 158   [
 159   REWRITE_TAC[Sphere.h0cut];
 160   REPEAT STRIP_TAC;
 161   BY(COND_CASES_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
 162   ]);;
 163   (* }}} *)
 164
 165 let h0cutC = prove_by_refinement(
 166   `!y. (y <= &2 * hminus) ==> (h0cut y = &1)`,
 167   (* {{{ proof *)
 168   [
 169   REPEAT STRIP_TAC;
 170   MATCH_MP_TAC h0cutA;
 171   MP_TAC Nonlinear_lemma.hminus_lt_h0;
 172   POP_ASSUM MP_TAC;
 173   BY(REAL_ARITH_TAC)
 174   ]);;
 175   (* }}} *)
 176
 177
 178 let SPLIT_H0_TAC pos =
 179   let destrict = REAL_ARITH `a < y /\ y <= b ==> a <= y /\ y <= b` in
 180  (REPEAT GEN_TAC) THEN
 181  (REWRITE_TAC[ineq_expand6]) THEN
 182  (REPLICATE_TAC (pos) DISCH_TAC) THEN
 183  (DISCH_THEN (fun t -> MP_TAC (MATCH_MP split_2h0_strict t))) THEN
 184  DISCH_THEN DISJ_CASES_TAC    THEN
 185  ASM_SIMP_TAC[h0cutA;h0cutB;h0cutC] THENL
 186    [ALL_TAC;POP_ASSUM ( ASSUME_TAC o (MATCH_MP destrict))] THEN
 187  (REPEAT (POP_ASSUM MP_TAC)) THEN
 188  (REWRITE_TAC[GSYM ineq_expand6]);;
 189
 190
 191 (* WARNING: This disturbs the goal *)
 192
 193 let split_h0 (ineq,ss) =
 194   let current_goals() =
 195     map (fun (_,w) -> w)
 196       ((fun (_,b,_) -> b) (hd (!current_goalstack))) in
 197   let split_h0_term i inq =
 198     let _ = g inq in
 199     let _ = e(SPLIT_H0_TAC i) in
 200       map all_forall (current_goals()) in
 201   let _ = (length ss > 0)  or failwith "empty split" in
 202   let ineql = split_h0_term (hd ss) ineq in
 203    map (fun t-> (t, tl ss)) ineql;;
 204
 205 let rec split_all_h0 = function
 206   | [] -> []
 207   | (i,[])::rs -> i :: split_all_h0 rs
 208   | r::rs -> split_all_h0 (split_h0 r @ rs);;
 209
 210
 211
 212 (* ========================================================================== *)
 213 (*    PARSING INEQUALITIES                                                    *)
 214 (* ========================================================================== *)
 215
 216
 217
 218 let dest_nonlin t =
 219   let (_,r,il) = dest_ineq t in
 220   let p1 (a,_,_) = a in
 221   let p2 (_,b,_) = b in
 222   let p3 (_,_,c) = c in
 223   let dest x = try dest_binop `(real_lt)` x with Failure _ -> dest_binop `(real_le)` x in
 224   let (iis,zzs) = unzip( map (dest) il) in
 225   let zz = nub zzs in
 226   let _ = (zz = [`&0`]) or failwith "zero expected" in
 227   let _ = ((map p2 r = x6list) or (map p2 r = x9list)) or failwith "x1..x6 or x1..x9 expected" in
 228   (map p1 r, map p3 r,iis);;
 229
 230  (* these names don't change in cpp interval code *)
 231
 232 let idem_assoc = [];; (* make it the default *)
 233
 234 (* these names can change in cpp (hol_name,cpp_name).
 235     Don't generate function defs for these.
 236     "NOT_IMPLEMENTED" is a special tag to suppress the
 237     production of test routines. We would be better
 238     off using an option. *)
 239
 240 let native_fun = [
 241   ("unit6","Lib::unit");
 242   ("two6","Lib::two6");
 243   ("proj_x1","Lib::x1");
 244   ("proj_x2","Lib::x2");
 245   ("proj_x3","Lib::x3");
 246   ("proj_x4","Lib::x4");
 247   ("proj_x5","Lib::x5");
 248   ("proj_x6","Lib::x6");
 249   ("proj_y1","Lib::y1");
 250   ("sqrt_x1","Lib::y1");
 251   ("delta_x","Lib::delta_x");
 252   ("sol_x","Lib::sol_x");
 253   ("dih_x","Lib::dih_x");
 254   ("rad2_x","Lib::rad2_x");
 255   ("rho_x","NOT_IMPLEMENTED");
 256   ("delta_y","NOT_IMPLEMENTED");
 257   ("dih_y","NOT_IMPLEMENTED");
 258   ("sol_y","NOT_IMPLEMENTED");
 259   ("delta_x4","Lib::delta_x4");
 260   ("edge_flat2_x","Lib::edge_flat2_x");
 261   ("halfbump_x1","Lib::halfbump_x1");
 262   ("ups_126","Lib::ups_126");
 263   ("eta2_126","Lib::eta2_126");
 264   ("compose6","Function::compose");
 265   ("constant6","Lib::constant6");
 266   ("uni","Lib::uni");
 267   ("sqrt","univariate::i_sqrt");
 268   ("acs","univariate::i_acos");
 269   ("asn","univariate::i_asin");
 270   ("atn","univariate::i_atan");
 271   ("cos","univariate::i_cos");
 272   ("sin","univariate::i_sin");
 273   ("pow2","univariate::i_pow2");
 274   ("matan","univariate::i_matan");
 275   ("gchi","Lib::i_gchi");
 276   ("lfun","Lib::i_lfun");
 277   ("rho","Lib::i_rho");
 278   ("flat_term_x","Lib::i_flat_term_x");
 279   ("sqn","univariate::i_sqn");
 280   ("promote1_to_6","Lib::promote1_to_6");
 281   ("gamma2_x_div_azim_v2","Lib::i_gamma2_x_div_azim_v2");
 282   ("num1","Lib::num1");
 283 ];;
 284
 285
 286 (* and for these
 287 gradually eliminate this list.
 288 The default will be to have the same names.
 289 *)
 290
 291 let cpp_assoc =
 292   let pref = "" in
 293   let p (a,b) = (a, (pref^b)) in map p
 294   (idem_assoc @ [
 295   ("sqrt_x2","proj_y2");
 296   ("sqrt_x3","proj_y3");
 297   ("sqrt_x4","proj_y4");
 298   ("sqrt_x5","proj_y5");
 299   ("sqrt_x6","proj_y6");
 300   ("promote_pow2","x1square");
 301   ("promote_pow3","x1cube");
 302
 303  ]);;
 304
 305 let cpp_fn_name s =
 306   try Lib.assoc s native_fun
 307   with Failure _ ->
 308     try Lib.assoc s cpp_assoc
 309     with Failure _ -> s;;
 310
 311 let cpp0_assoc =
 312   [("sqrt8","sqrt8");("pi","pi");("const1","const1");
 313    ("hminus","hminus");("sqrt3","sqrt3");
 314    ("arc_hhn","arc_hhn");
 315    ("adodec","aStrongDodec");
 316    ("bdodec","bStrongDodec");
 317    ("ydodec","yStrongDodec");
 318    ];;
 319
 320 let cpp_of_constant s  =
 321   try (assoc s cpp0_assoc) with
 322       Failure _ -> failwith (s^" find: cpp_of_constant") ;;
 323
 324 let cpp_of_fun to_string xlist s xs =
 325   let (arg,xss) = chop_list (length xs - length xlist) xs in
 326   let _ = (xss = xlist) or failwith ("standard x list expected in "^s) in
 327   let hd =  (cpp_fn_name s) in
 328   let arg_s = map (paren o to_string) arg in
 329   let p = if (length arg > 0) then paren else I in
 330     (hd ^ " " ^ p(join_comma arg_s));;
 331
 332 (* 2013-08-14, changed for AWS compiler. was interval::interval( ... ) *)
 333 let i_mk s = "interval("^quoted s ^")";;
 334
 335 let i_mk2 t = (* treat small integers exactly *)
 336   let n = dest_numeral t in
 337   let s = if (Num.is_integer_num n) && (Num.sign_num n >= 0) && (n </ Int 100)
 338      then string_of_num n else string_of_num' n in
 339     i_mk s;;
 340
 341 let cpp_string_of_term =
 342   let rec soh t =
 343     if is_var t then fst (dest_var t) else
 344       let (f,xs) = strip_comb t in
 345       let _  = (is_const f) or
 346         failwith ("constant expected:" ^ string_of_term f) in
 347       let ifix i = let [a;b] = xs in paren(soh a ^ " " ^ i ^ " " ^ soh b) in
 348         match fst (dest_const f) with
 349           | "real_add" -> ifix "+"
 350           | "real_mul" -> ifix "*"
 351           | "real_div" -> ifix "/"
 352           | "\\/" -> ifix "\\/"
 353           | "real_neg" -> let [a] = xs in "(-" ^ soh a ^ ")"
 354           | "real_of_num" -> let [a] = xs in i_mk2( a)
 355           | "NUMERAL" -> let [a] = xs in string_of_num' (dest_numeral t)
 356           | "<" -> let [a;b] = xs in paren(soh a ^ " < " ^ soh b)
 357           | ">" -> let [a;b] = xs in paren(soh a ^ " > " ^ soh b)
 358           | "+" -> let [a;b] = xs in paren(soh a ^ " + " ^ soh b)
 359           | "*" -> let [a;b] = xs in paren(soh a ^ " * " ^ soh b)
 360           | "DECIMAL" ->  i_mk(string_of_num' (dest_decimal t))
 361           | s -> if (xs = [])
 362             then "("^cpp_of_constant s^")"
 363             else paren(cpp_of_fun soh x6list s xs) in
 364     fun t ->
 365       try (soh t)
 366       with Failure s -> failwith (s^" .......   "^string_of_term t);;
 367
 368 (* generation of cpp code *)
 369
 370 let cpp_template_taylor c (i,s) = Printf.sprintf
 371 "       Function F%s%d = %s;" c i s;;
 372
 373 let cpp_template_t c iis =
 374   join_lines
 375     (map (cpp_template_taylor c) (zip (1--(length iis)) iis));;
 376
 377 let cpp_template_F c i = Printf.sprintf "&F%s%d" c i;;
 378
 379 let cpp_template_Fc c len = join_comma
 380   (map (cpp_template_F c) (1-- len));;
 381
 382 let rec delta126min = function
 383     | [] -> -1.0
 384     | Delta126min t :: _ -> t
 385     | _ :: a -> delta126min a;;
 386
 387 let rec widthCut = function
 388   | [] -> (false,0.0)
 389   | Widthcutoff t::_ -> (true,t)
 390   | _:: a -> widthCut a;;
 391
 392 let rec delta126max = function
 393     | [] -> -1.0
 394     | Delta126max t :: _ -> t
 395     | _ :: a -> delta126max a;;
 396
 397 let rec delta135min = function
 398     | [] -> -1.0
 399     | Delta135min t :: _ -> t
 400     | _ :: a -> delta135min a;;
 401
 402 let rec delta135max = function
 403     | [] -> -1.0
 404     | Delta135max t :: _ -> t
 405     | _ :: a -> delta135max a;;
 406
 407 let cpp_template_gen = Printf.sprintf "
 408  const char svn[] = %s;
 409  const char ineq_id[] = %s;
 410
 411  int testRun() // autogenerated code
 412         {
 413         interval tx[6]={%s};
 414         interval tz[6]={%s};
 415         domain x = domain::lowerD(tx);
 416         domain z = domain::upperD(tz);
 417         domain x0=x;
 418         domain z0=z;
 419         %s
 420         const Function* I[%d] = {%s}; // len ...
 421         cellOption opt;
 422         opt.allowSharp = %d; // sharp
 423         opt.onlyCheckDeriv1Negative = %d; // checkderiv
 424         %s // other options.
 425         return  prove::recursiveVerifier(0,x,z,x0,z0,I,%d,opt); // len
 426         }";;
 427
 428 let mk_cpp_proc t s tags =
 429   let sharp = if  mem Sharp tags then 1 else 0 in
 430   let checkderiv = if  mem Onlycheckderiv1negative tags then 1 else 0 in
 431   let ifd b s = if b then s else "" in
 432   let setrad2 = ifd (mem Set_rad2 tags) "\topt.setRad2 = 1;\n" in
 433   let (b,f) = widthCut tags in
 434   let sWidth = ifd b (Printf.sprintf "\topt.widthCutoff = %8.16f;\n" f) in
 435   let d126min = delta126min tags in
 436   let s126min = ifd (d126min > -1.0)
 437     (Printf.sprintf  "\topt.delta126Min = %8.16f;\n" d126min) in
 438   let d126max = delta126max tags in
 439   let s126max = ifd (d126max > -1.0)
 440     (Printf.sprintf "\topt.delta126Max = %8.16f;\n" d126max) in
 441   let d135min = delta135min tags in
 442   let s135min = ifd (d135min > -1.0)
 443     (Printf.sprintf "\topt.delta135Min = %8.16f;\n" d135min) in
 444   let d135max = delta135max tags in
 445   let s135max = ifd (d135max > -1.0)
 446     (Printf.sprintf "\topt.delta135Max = %8.16f;\n" d135max) in
 447   let s206A = ifd (s="2065952723 A1" )
 448     (Printf.sprintf "\topt.strategy206A=1;\n") in
 449   let disallowderiv = ifd  (mem Disallow_derivatives tags)
 450     "\topt.allowDerivatives=0;\n" in
 451   let others = setrad2 ^ s126min ^ s126max ^ s135min ^ s135max ^
 452     sWidth ^ s206A ^ disallowderiv in
 453   let c = map cpp_string_of_term in
 454   let f (x,y,z) = (c x,c y,c z) in
 455   let (aas,bbs,iis) = f (dest_nonlin t) in
 456   let len = length iis in
 457   let sq = quoted s in
 458   let svn = (quoted(svn_version())) in
 459   let jaas = join_comma aas in
 460   let jbbs = join_comma bbs in
 461     cpp_template_gen svn sq jaas jbbs (cpp_template_t "" iis)
 462       len (cpp_template_Fc "" len) sharp  checkderiv others len;;
 463
 464 (* quad clusters *)
 465
 466 let has_subterm sub tm =
 467   can (find_term ((=) sub)) tm;;
 468
 469 let has_cross_diag = has_subterm `quad_cross_diag2_x`;;
 470
 471 let has_delta_top = has_subterm `delta_top_x`;;
 472
 473 let is_quad_cluster tags = (can (find (function Quad_cluster _ -> true | _ -> false)) tags);;
 474
 475 let quad_margin tags = (function Quad_cluster t -> t | _ -> 0.0)
 476   (find ((function Quad_cluster _ -> true | _ -> false))  tags);;
 477
 478 let check_quad_partition_term (r,s,t) tm =
 479   let tm2 = list_mk_binop `(+)` (r @ s @ t) in
 480   let t = mk_eq (tm ,tm2) in
 481       (REAL_ARITH) t;;
 482
 483 let partition_quad_term tm =
 484   let rec split tm =
 485     if (has_cross_diag tm) then ([],[],[tm]) else
 486     if (has_delta_top tm) then ([],[],[tm]) else
 487       if (subset (frees tm) x6list) then ([tm],[],[]) else
 488         if (subset (frees tm) x_backlist) then ([],[tm],[]) else
 489           let (a1,a2) = dest_binop `(+)` tm in
 490           let  (r1,s1,t1) = split a1 in
 491           let (r2,s2,t2) = split a2  in
 492             (r1 @ r2, s1 @ s2, t1 @ t2) in
 493   let (r,s,t) = split tm in
 494   let _ = check_quad_partition_term (r,s,t) tm in
 495   let v =  vsubst [`x1:real`,`x7:real`;  `x5:real`,`x8:real`; `x6:real`,`x9:real`] in
 496   let w = function | [] ->
 497    `unit6 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) * #0.0` | xl -> list_mk_binop `(+)` xl in
 498    (w r,w(map v s), t);;
 499
 500
 501 let cppq_template_gen = Printf.sprintf "
 502  char* svn = %s;
 503  char* ineq_id = %s;
 504
 505  int testRun()  // quad cluster case, autogenerated code
 506         {
 507         interval txA[6]={%s};
 508         interval tzA[6]={%s};
 509         domain xA = domain::lowerD(txA);
 510         domain zA = domain::upperD(tzA);
 511         interval txB[6]={%s};
 512         interval tzB[6]={%s};
 513         domain xB = domain::lowerD(txB);
 514         domain zB = domain::upperD(tzB);
 515         // Declare FA, FB...
 516         %s
 517         %s
 518         const Function* IA[%d] = {%s};
 519         const Function* IB[%d] = {%s};
 520         cellOption opt;
 521         %s // options.
 522         return prove::recursiveVerifierQ(0,xA,xB,zA,zB,IA,IB,%d,opt);
 523         }";;
 524
 525 let get_cross_diag_squared is9 =
 526   let id9' = filter (fun (_,_,c)-> length c >0 && has_cross_diag (hd c)) is9 in
 527   let is9'' = (fun (_,_,[c])::_ -> c ) id9' in
 528   let tm = term_match x9list `quad_cross_diag2_x x1 x2 x3 x4 x5 x6 x7 x8 x9 +
 529     unit6 x1 x2 x3 x4 x5 x6 * t` is9'' in
 530   let t =   (fun ([],[(x,_)],[]) -> x) tm in
 531     mk_binop `( * )` t t;;  (* t is negative, but it gets squared *)
 532
 533 let get_delta_top_squared is9 =
 534   let id9' = filter (fun (_,_,c)-> length c >0  && has_delta_top (hd c)) is9 in
 535   let is9'' = (fun (_,_,[c])::_ -> c ) id9' in
 536   let tm = term_match x9list `delta_top_x t x1 x2 x3 x4 x5 x6 x7 x8 x9` is9'' in
 537   let t =   (fun ([],[(x,_)],[]) -> x) tm in
 538     mk_binop `( * )` t t;;  (* gets squared *)
 539
 540 let cde_template =
 541   Printf.sprintf "opt.crossDiagMinEnclosed = interMath::inf(%s);\n";;
 542
 543 let cdt_template =
 544   Printf.sprintf "opt.crossDiagMinDelta = interMath::inf(%s);\n";;
 545
 546 let mk_cppq_proc t s tags =
 547   let svn = (quoted(svn_version())) in
 548   let ineq_id = quoted s in
 549   let cpp = cpp_string_of_term in
 550   let (x,z,is) = dest_nonlin t  in
 551   let is' = map partition_quad_term is in
 552   let (is9,is6) = partition (fun (_,_,c) -> length c > 0)   is' in
 553   let (is6A,is6B) = unzip (map (fun (a,b,_) -> (cpp a,cpp b)) is6) in
 554   let len = length  is6 in
 555   let xs = map cpp x in
 556   let zs = map cpp z in
 557   let nth = List.nth in
 558   let a_part u = [nth u 0;nth u 1;nth u 2;nth u 3; nth u 4;nth u 5] in
 559   let b_part u = [nth u 6;nth u 1;nth u 2;nth u 3;nth u 7; nth u 8] in
 560   let xA = join_comma(a_part xs) in
 561   let xB = join_comma(b_part xs) in
 562   let zA = join_comma(a_part zs) in
 563   let zB = join_comma(b_part zs) in
 564   let opt_cross =
 565     try
 566       (  cde_template (cpp ( get_cross_diag_squared is9) ))
 567     with _ -> "" in
 568   let opt_delta_top =
 569     try
 570       (  cdt_template (cpp ( get_delta_top_squared is9) ))
 571     with _ -> "" in
 572   let backsym =
 573     if (mem Dim_red_backsym tags)
 574     then "\topt.dimRedBackSym = 1;\n" else "" in
 575   let sWidth =
 576     let (b,f) = widthCut tags in
 577       if b then Printf.sprintf "\topt.widthCutoff = %8.16f;\n" f else ""  in
 578   let margin = Printf.sprintf "\topt.margin = %8.16f;\n\n" (quad_margin tags) in
 579   let options = opt_cross ^ opt_delta_top ^ backsym^margin^sWidth in
 580   cppq_template_gen svn ineq_id xA zA xB zB
 581     (cpp_template_t "A" is6A) (cpp_template_t "B" is6B)
 582     len (cpp_template_Fc "A" len) len (cpp_template_Fc "B" len) options len ;;
 583
 584 (*
 585 let t = snd(top_goal());;
 586 let s = "test";;
 587 let tags = [Quad_cluster 3.0];;
 588 *)
 589
 590 (*     next: put together header, proc, tail and run *)
 591
 592 let tmpfile = flyspeck_dir^"/../interval_code/test_auto.cc";;
 593
 594 let cpp_header() = join_lines (load_file  (flyspeck_dir^"/../interval_code/generic_head.txt"));;
 595
 596 let cpp_tail() = join_lines (load_file  (flyspeck_dir^"/../interval_code/generic_tail.txt"));;
 597
 598 let mkfile_cpp  t s tags  =
 599   output_filestring tmpfile
 600    (join_lines [cpp_header(); (mk_cpp_proc t s tags);cpp_tail()]);;
 601
 602 let mkfile_cppq  t s tags =
 603   output_filestring tmpfile
 604    (join_lines [cpp_header(); (mk_cppq_proc t s tags);cpp_tail()]);;
 605
 606 let compile_cpp =
 607   let err = Filename.temp_file "cpp_err" ".txt" in
 608     fun () ->
 609       let e = Sys.command("cd "^flyspeck_dir^"/../interval_code; make test_auto >& "^err) in
 610       let _ =   (e=0) or (let _ = Sys.command ("cat "^err) in failwith "compiler error") in
 611         ();;
 612
 613  let execute_interval ex tags s testineq =
 614   let interval_dir = flyspeck_dir^"/../interval_code" in
 615   let quad_cluster = is_quad_cluster tags  in
 616   let _ = if quad_cluster then
 617    mkfile_cppq testineq s tags
 618   else
 619       mkfile_cpp testineq s tags in
 620   let _ = compile_cpp() in
 621   let _ = (not ex) or (0=  Sys.command(interval_dir^"/test_auto")) or failwith "interval execution error" in
 622     ();;
 623
 624
 625 (* ========================================================================== *)
 626 (*    MEGA PREP    TACTICS                                                    *)
 627 (* ========================================================================== *)
 628
 629 (* *************************************************************************** *)
 630 (* PRELIM *)
 631 (* *************************************************************************** *)
 632
 633 let macro_expand = (
 634    [
 635      Sphere.x1_delta_y;Sphere.delta4_squared_y;
 636      vol4f_palt;Nonlinear_lemma.y_of_x_e;
 637      gamma4fgcy_alt;
 638      Sphere.vol3r;Sphere.vol2f;Sphere.gamma4f;
 639      Sphere.gamma3f;  GSYM Nonlinear_lemma.quadratic_root_plus_curry;
 640      REAL_MUL_LZERO;
 641      REAL_MUL_RZERO;FST;SND;
 642      Sphere.node2_y;Sphere.node3_y] @
 643      (!Ineq.dart_classes));;
 644
 645 let PRELIM_REWRITE_TAC = EVERY[
 646   (REWRITE_TAC[GSYM Sphere.rad2_y]) ;
 647   (REWRITE_TAC(macro_expand)) ;
 648 ];;
 649
 650 (* *************************************************************************** *)
 651 (* BRANCH *)
 652 (* *************************************************************************** *)
 653
 654 (* take care of branching *)
 655
 656 let BRANCH_TAC = EVERY[
 657   REWRITE_TAC[REAL_ARITH `x / &1 = x /\ &0 * x = &0 /\ &0 +x = x`];
 658   REWRITE_TAC[Sphere.gamma4f;vol4f_lmfun;Sphere.gamma3f;];
 659   REWRITE_TAC[ineq_expand6];
 660   DISCH_TAC;
 661   REPEAT GEN_TAC;
 662   REPEAT DISCH_TAC;
 663   ASSUM_LIST (let rec r = function | [] -> ALL_TAC | th::ths -> (MP_TAC (REPEAT_RULE (OR_RULE (MATCH_MP pathL_bound) (MATCH_MP pathR_bound)) th)) THEN r ths in r);
 664   REWRITE_TAC[];
 665   SIMP_TAC[c2001;
 666            gcy_low;gcy_low_const;gcy_low_hminus;gcy_high;gcy_high_hplus;
 667            h0_lt_gt;
 668            lmdih3_ldih3;lmdih5_ldih5;lmdih_ldih;lmdih5_0;lmdih3_0;lmdih0;
 669            (* Oct 28, 2010:*) vol3f_lm0;vol3f_lmln;
 670            (* nov23 *) lmfun0;lmfun_lfun;hm0;
 671          (* may 26, 2011. macro_expand was moved to prelim tac,
 672             so additional simps are needed. *)
 673          lmdih1_0';lmdih3_0';lmdih5_0';
 674          lmdih_ldih';lmdih3_ldih3';lmdih5_ldih5';
 675    ];
 676   SIMP_TAC[lmfun_lfun;lmfun0];
 677   REWRITE_TAC[REAL_ARITH `&0 * x = &0 /\ &0 + x = x`];
 678   REPEAT (DISCH_THEN (fun t-> ALL_TAC));
 679   REPEAT (POP_ASSUM MP_TAC);
 680   REWRITE_TAC[GSYM ineq_expand6];
 681   DISCH_TAC;
 682   EVERY (map SPEC_TAC [(`y6:real`,`y6:real`);(`y5:real`,`y5:real`);(`y4:real`,`y4:real`);(`y3:real`,`y3:real`);(`y2:real`,`y2:real`);(`y1:real`,`y1:real`)]);
 683   POP_ASSUM MP_TAC;
 684   REWRITE_TAC[Sphere.pathL;Sphere.pathR]; (*  moved May 24, 2011 *)
 685 ];;
 686
 687 (* *************************************************************************** *)
 688 (* *************************************************************************** *)
 689
 690 (*
 691   let SQRT_SQRT_TAC =
 692 EVERY[
 693   REPEAT DISCH_TAC;
 694   SUBGOAL_THEN `sqrt x1 * sqrt x1 = x1 /\ sqrt x2 * sqrt x2 = x2 /\ sqrt x3 * sqrt x3 = x3 /\ sqrt x4 * sqrt x4 = x4 /\ sqrt x5 * sqrt x5 = x5 /\ sqrt x6 * sqrt x6 = x6` (unlist REWRITE_TAC) THENL[ ASM_MESON_TAC[sq_pow2];ALL_TAC] THEN
 695   REPEAT (POP_ASSUM MP_TAC);
 696   DISCH_TAC;
 697 ];;
 698 *)
 699
 700   let SQRT_SQRT_TAC = EVERY[
 701   REPEAT DISCH_TAC;
 702   SUBGOAL_THEN `sqrt x1 * sqrt x1 = x1 /\ sqrt x2 * sqrt x2 = x2 /\ sqrt x3 * sqrt x3 = x3 /\
 703       sqrt x4 * sqrt x4 = x4 /\ sqrt x5 * sqrt x5 = x5 /\ sqrt x6 * sqrt x6 = x6`
 704       (unlist REWRITE_TAC)
 705   THENL [ REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP sq_pow2))) THEN
 706             REPEAT DISCH_TAC THEN BY(ASM_REWRITE_TAC[]);ALL_TAC] THEN
 707   REPEAT (POP_ASSUM MP_TAC);
 708   DISCH_TAC;];;
 709
 710
 711
 712 let X_SQRT_COMPOUND_ORDER =
 713 [`norm2hh (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 714      norm2hh_x x1 x2 x3 x4 x5 x6 `;
 715 `rad2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 716      rad2_x x1 x2 x3 x4 x5 x6 `;
 717 `delta4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 718      delta_x4 x1 x2 x3 x4 x5 x6 `;
 719 `delta4_y (sqrt x7) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x8) (sqrt x9) =
 720    delta_x4 x7 x2 x3 x4 x8 x9 `;
 721 `dih2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 722      dih2_x x1 x2 x3 x4 x5 x6 `;
 723 `dih3_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 724     dih3_x x1 x2 x3 x4 x5 x6 `;
 725 `dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 726      dih_x x1 x2 x3 x4 x5 x6 `;
 727 `dih4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 728     dih4_x x1 x2 x3 x4 x5 x6 `;
 729 `dih5_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 730    dih5_x x1 x2 x3 x4 x5 x6 `;
 731 `dih6_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 732    dih6_x x1 x2 x3 x4 x5 x6 `;
 733 `delta_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 734    delta_x x1 x2 x3 x4 x5 x6 `;
 735 `delta_y (sqrt x7) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x8) (sqrt x9) =
 736    delta_x x7 x2 x3 x4 x8 x9`;
 737 `vol_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 738    vol_x x1 x2 x3 x4 x5 x6 `;
 739 `eta_y (sqrt x1) (sqrt x2) (sqrt x6) pow 2 = eta2_126 x1 x2 x3 x4 x5 x6 `;
 740 `eta_y (sqrt x1) (sqrt x3) (sqrt x5) pow 2 = eta2_135 x1 x2 x3 x4 x5 x6 `;
 741 `eta_y (sqrt x4) (sqrt x5) (sqrt x6) pow 2 = eta2_456 x1 x2 x3 x4 x5 x6 `;
 742 `vol3f (sqrt x1) (sqrt x2) (sqrt x6)  sqrt2 lfun = vol3f_x_lfun x1 x2 x3 x4 x5 x6 `;
 743 `vol_y sqrt2 sqrt2 sqrt2 (sqrt x1) (sqrt x2) (sqrt x6)  = vol3_x_sqrt x1 x2 x3 x4 x5 x6 `;
 744 `vol3f_sqrt2_lmplus (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)      (sqrt x6) =
 745    vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6`;
 746  ];;
 747
 748
 749   let rec get_consts tm =
 750     match tm with
 751         Var(s,t) -> []
 752       | Const(s,t) -> [tm ]
 753       | Comb (t1,t2) -> get_consts t1 @ get_consts t2
 754       | Abs (t1,t2) -> get_consts t1 @ get_consts t2 ;;
 755
 756   let get_goal_const gl =
 757     let w = goal_concl gl in
 758       get_consts w;;
 759
 760 (*
 761   let X_SQRT_COMPOUND_ORDER_TAC:tactic =
 762     fun gl ->
 763       let (asl,a) = dest_goal gl in
 764       let fr = frees a in
 765         (* edited next line Nov 2012, svn 2931 *)
 766       let vos = filter (fun t -> subset (frees (fst (dest_eq t))) fr ) X_SQRT_COMPOUND_ORDER  in
 767     let X_SQRT_COMPOUND_ORDER_FIL = list_mk_conj vos in
 768   (SUBGOAL_THEN  X_SQRT_COMPOUND_ORDER_FIL  (fun t-> REWRITE_TAC[t;(GSYM Sphere.rhazim_x); (GSYM Sphere.rhazim2_x);xspec (GSYM Sphere.rhazim3_x)]) THENL[ (GEN_MESON_TAC 0 200 1[Sphere.norm2hh_x;rad2_x_y;delta_x4_delta4_y;dih_x_y;dih2_x_y;delta_x_y;dih3_x_y;tauq_x_y;GSYM Sphere.dih4_x;GSYM Sphere.dih5_x;GSYM Sphere.dih6_x;vol_x_y;Sphere.eta2_126; Sphere.eta2_135;Sphere.eta2_456;GSYM vol3f_x_lfun;GSYM vol3_x_sqrt;GSYM vol3f_x_sqrt2_lmplus]);ALL_TAC]) gl
 769 ;;
 770 *)
 771
 772   let X_SQRT_COMPOUND_ORDER_TAC:tactic =
 773     fun gl ->
 774       let (asl,a) = dest_goal gl in
 775       let fr = frees a in
 776       let c = get_goal_const gl in
 777       let vos = filter (fun t -> subset (frees (fst (dest_eq t))) fr ) X_SQRT_COMPOUND_ORDER  in
 778       let vos' = filter (fun t -> mem (fst (strip_comb (fst(dest_eq t)))) c) vos in
 779     let vconj = list_mk_conj vos' in
 780   (SUBGOAL_THEN  vconj  (fun t-> REWRITE_TAC[t;(GSYM Sphere.rhazim_x); (GSYM Sphere.rhazim2_x);xspec (GSYM Sphere.rhazim3_x)]) THENL[ (GEN_MESON_TAC 0 200 1[Sphere.norm2hh_x;rad2_x_y;delta_x4_delta4_y;dih_x_y;dih2_x_y;delta_x_y;dih3_x_y;tauq_x_y;GSYM Sphere.dih4_x;GSYM Sphere.dih5_x;GSYM Sphere.dih6_x;vol_x_y;Sphere.eta2_126; Sphere.eta2_135;Sphere.eta2_456;GSYM vol3f_x_lfun;GSYM vol3_x_sqrt;GSYM vol3f_x_sqrt2_lmplus]);ALL_TAC]) gl
 781 ;;
 782
 783
 784 let X_FROZEN_COMPOUND =(map SPEC_ALL [
 785  vol3r_126_x;REAL_ARITH `&2 = #2.0`;
 786  GSYM arclength_x_234;
 787  GSYM arclength_x_126;
 788  GSYM Functional_equation.nonf_gamma2_x1_div_a_v2;
 789  ] ) ;;
 790
 791
 792 let decimal = REWRITE_RULE [REAL_ARITH `&2 = #2.0`];;
 793
 794 let X_COMPOUND_DEF =  [REAL_ARITH `&2 = #2.0`;
 795  beta_bump_force_x;
 796  GSYM Sphere.gchi1_x;GSYM Sphere.gchi2_x;
 797  GSYM Sphere.gchi3_x;GSYM Sphere.gchi4_x;
 798  GSYM Sphere.gchi5_x;GSYM Sphere.gchi6_x;
 799  GSYM Sphere.arclength_x1;GSYM Sphere.arclength_x2;
 800  GSYM Enclosed.quad_cross_diag2_x;
 801  tauq_x_y;] @
 802   map decimal [
 803  GSYM Sphere.ldih_x;GSYM Sphere.ldih2_x;
 804  GSYM Sphere.ldih3_x;GSYM Sphere.ldih6_x;
 805   ];;
 806
 807 let X_OF_Y_TAC =
 808   (
 809   (DISCH_TAC) THEN
 810   TRY (MATCH_MP_TAC ineq_square2) THEN TRY (MATCH_MP_TAC ineq_square2_9) THEN
 811   (REWRITE_TAC basic_constants_nn) THEN
 812   REWRITE_TAC[GSYM CONJ_ASSOC] THEN
 813   (REPEAT (CONJ_TAC THENL[MP_TAC hminus_gt THEN MP_TAC sqrt3_nn THEN REWRITE_TAC[Sphere.h0;Sphere.hplus] THEN REAL_ARITH_TAC;ALL_TAC])) THEN
 814   (REPEAT GEN_TAC) THEN
 815   (REWRITE_TAC [sol_y_123;taum_123]) THEN
 816   (REWRITE_TAC[ineq]) THEN
 817   (SQRT_SQRT_TAC) THEN
 818     (REPEAT DISCH_TAC) THEN
 819     (* remove x variable compound *)
 820     X_SQRT_COMPOUND_ORDER_TAC THEN
 821     FROZEN_REWRITE_TAC X_FROZEN_COMPOUND THEN
 822     REWRITE_TAC X_COMPOUND_DEF THEN
 823     (* repackage *)
 824     (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN
 825     (REWRITE_TAC[GSYM ineq_expand9]) THEN
 826     (REWRITE_TAC[GSYM ineq_expand6]) THEN
 827     (REWRITE_TAC[REAL_ARITH `(&2 = #2.0) /\ (x pow 2 = x * x) /\ (#2.0 * #2.0 = #4.0) /\ (#2.18 * #2.18 = #4.7524 ) /\ (#2.52 * #2.52 = #6.3504)`;sqrt8_2;sqrt2_sqrt2;Sphere.h0;Sphere.hplus]) THEN
 828   ALL_TAC
 829   );;
 830
 831 let EXPAND_lfun =
 832   (SUBGOAL_THEN `lfun x1 = (#1.26 - proj_x1  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real))/(#0.26)` (fun t-> REWRITE_TAC[t])) THENL [
 833   REWRITE_TAC[Sphere.lfun;proj_x1;Sphere.h0;REAL_ARITH `#1.26 - &1 = #0.26`];ALL_TAC] ;;
 834
 835 let REMOVE_dummy = SUBGOAL_THEN `!(f:bool). (!(dummy:real). ineq [&1,dummy,&1] f) = (!(x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real). ineq[(&1,x1,&1);(&1,x2,&1);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)] f)` (fun t-> REWRITE_TAC[t]) THENL[  REWRITE_TAC[ineq] THEN  MESON_TAC[REAL_ARITH `~(&2 <= &1)`]; ALL_TAC];;
 836
 837 let EXPAND_1var = SUBGOAL_THEN `!(f:real->bool) a b. (!(y:real). ineq [a,y,b] (f y)) = (!(x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real). ineq[(a,x1,b);(&1,x2,&1);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)] (f x1))` (fun t-> REWRITE_TAC[t]) THENL [REWRITE_TAC[ineq] THEN  MESON_TAC[REAL_ARITH `(&1 <= &1)`];ALL_TAC] ;;
 838
 839
 840 let REAL_SIMPLIFY_EXPRESSION =  let
 841   arith = REAL_ARITH `!x y z. (&8 = #8) /\ (x - y = x + (-- #1.0) * y) /\
 842   (x * (y+z) = x * y + x * z) /\ (y+z) * x = y * x + z * x /\
 843   (x + y) + z = x + y + z /\ (-- x * -- y = x * y) /\ (x * -- y = -- x * y) /\
 844   (-- x * y = -- (x * y)) /\ (x * y) * z = x * y * z /\ -- #1.0 * x = -- x /\
 845   -- (x + y) = -- x + (--y) /\ -- (-- x) = x /\ (-- (-- x * y) = x * y) /\
 846    #0.0 = &0 /\ #0 = &0 /\ &0 * x = &0 /\ x * &0 = &0 /\ (&0 + x = x) /\
 847   -- &0 = &0 /\ (x + &0 = x) /\ (&0 + x = x) /\
 848   &1 * x = x /\ -- &1 * x = -- x /\ x * sqrt8 = sqrt8 * x    ` in
 849   (REWRITE_TAC[REAL_POW_MUL;real_div;REAL_MUL_LZERO; REAL_MUL_RZERO;arith]) ;;
 850
 851 let EXPAND_SQRT =
 852   (SUBGOAL_THEN `sqrt x1 = sqrt_x1 x1 x2 x3 x4 x5 x6 /\ sqrt x2 = sqrt_x2 x1 x2 x3 x4 x5 x6 /\ sqrt x3 = sqrt_x3 x1 x2 x3 x4 x5 x6 /\ sqrt x4 = sqrt_x4 x1 x2 x3 x4 x5 x6 /\ sqrt x5 = sqrt_x5 x1 x2 x3 x4 x5 x6 /\ sqrt x6  = sqrt_x6 x1 x2 x3 x4 x5 x6 /\ sqrt x8 = sqrt_x5 (x7:real) x2 x3 x4 x8 x9 /\ sqrt x9 = sqrt_x6 x7 x2 x3 x4 x8 x9 ` (fun t->REWRITE_TAC[t])  THENL [REWRITE_TAC[sqrt_x1;sqrt_x2; sqrt_x3;sqrt_x4;sqrt_x5;sqrt_x6];ALL_TAC]) ;;
 853
 854 (* for 1d inequality involving vol2f marchal *)
 855
 856 let EXPAND_vol2 =
 857 REWRITE_TAC[vol2f_marchal_pow_y;vol2r_y] THEN
 858   SUBGOAL_THEN `x1 pow 1 = promote pow1 x1 x2 x3 x4 x5 x6 /\
 859   x1 pow 2 = promote_pow2 x1 x2 x3 x4 x5 x6 /\
 860   x1 pow 3 = promote_pow3 (x1:real) (x2:real) (x3:real)
 861     (x4:real) (x5:real) (x6:real) /\
 862   x1 pow 4 = promote pow4 x1 x2 x3 x4 x5 x6`
 863   (fun t->REWRITE_TAC[t])
 864   THENL[ REWRITE_TAC[promote;pow1;pow2;pow3;pow4;promote_pow2;promote_pow3];
 865          REWRITE_TAC[LET_DEF;LET_END_DEF]] ;;
 866
 867 let DEF_expand =
 868  [Sphere.a_spine5;Sphere.b_spine5;Sphere.mm1;
 869   Sphere.flat_term;Sphere.beta_bump_lb;REAL_POW_2;
 870   Sphere.h0;
 871   Sphere.mm2;GSYM Sphere.sqrt2;GSYM Sphere.sqrt3;
 872   GSYM Sphere.sqrt8;sol0_const1;sqrt2_sqrt8;
 873   Sphere.mm1;Sphere.mm2;Sphere.tau0;Sphere.hplus;
 874   tame_table_d_values;Sphere.vol2f;
 875   Sphere.lfun; (* added Oct 17, 2010 *)
 876  ];;
 877
 878 (* *************************************************************************** *)
 879 (* SERIES3Q1H *)
 880 (* *************************************************************************** *)
 881
 882 let SERIES3Q1H_5D_TAC =
 883   let instjx = INST_TYPE [(`:real`,`:A`);(`:real`,`:B`);(`:real`,`:C`);
 884                           (`:real`,`:D`);(`:real`,`:E`);(`:real`,`:F`)] in
 885   let PROJX = map instjx [ proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6] in
 886   let projx = list_mk_conj (map (concl o GSYM) PROJX ) in
 887  (REPEAT STRIP_TAC   THEN MATCH_MP_TAC ineq6_of_ineq5) THEN
 888  (REWRITE_TAC[Sphere.pathL;Sphere.pathR;Sphere.hplus;Sphere.h0]) THEN
 889  (REWRITE_TAC[ineq_expand6]) THEN
 890  (REPEAT GEN_TAC THEN REPEAT DISCH_TAC) THEN
 891  (SUBGOAL_THEN projx (fun t -> PURE_ONCE_REWRITE_TAC[t])) THENL
 892  [(REWRITE_TAC PROJX);ALL_TAC] THEN
 893  (REPEAT (POP_ASSUM MP_TAC)) THEN
 894  (REWRITE_TAC[GSYM ineq_expand6]);;
 895
 896 (* *************************************************************************** *)
 897 (* STYLIZE and WRAPUP *)
 898 (* *************************************************************************** *)
 899
 900 let STYLIZE_TAC =
 901   let real_arith_lt =
 902     REAL_ARITH `(x < y <=> (x- y < &0)) /\ (x <= y <=> (x-y <= &0))` in
 903   let real_arith_gt =
 904     REAL_ARITH `(x > y <=> (y - x < &0) ) /\ (x >= y <=> (y-x <= &0))` in
 905   let real_arith_unit =
 906     REAL_ARITH `unit0 * (x + y ) = unit0 * x + unit0 * y /\
 907     unit0 * --x = --(unit0 * x) /\ (unit0 * x  = x  * unit0) /\
 908     (x * y) * z = x * y * z` in
 909   let subgoal_proj = `x2 * unit0 =
 910     proj_x2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) /\
 911       x3 * unit0 = proj_x3 (x1) (x2) (x3) (x4) (x5) (x6) /\
 912     x1 * unit0 = proj_x1 (x1) (x2) (x3) (x4) (x5) (x6) /\
 913     (x4 * unit0 = proj_x4 x1 x2 x3 x4 x5 x6) /\
 914     (x5 * unit0 = proj_x5 x1 x2 x3 x4 x5 x6) /\
 915     (x6 * unit0 = proj_x6 x1 x2 x3 x4 x5 x6)` in
 916   let subgoal_unit6 = `unit0 = unit6
 917     (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real)` in
 918   REMOVE_dummy  THEN
 919   EXPAND_1var THEN
 920   DISCH_TAC THEN REPEAT GEN_TAC THEN
 921   (* rename added Nov 27, 2010 *)
 922   X_RENAME_TAC THEN
 923   REPEAT GEN_TAC THEN
 924   EXPAND_vol2 THEN
 925   (* prev line added Sep 8 , 2010 *)
 926   REWRITE_TAC  DEF_expand THEN
 927   (* prev line moved down sep 8 *)
 928   EXPAND_lfun THEN
 929   REWRITE_TAC[ineq] THEN
 930   (REPEAT DISCH_TAC) THEN
 931   (ONCE_REWRITE_TAC[real_arith_lt]) THEN
 932   (REWRITE_TAC[real_arith_gt]) THEN
 933   EXPAND_SQRT THEN
 934   REAL_SIMPLIFY_EXPRESSION THEN
 935   SUBGOAL_THEN `!a. x1:real * a = a * x1` (fun t->REWRITE_TAC[t])
 936   THENL[REAL_ARITH_TAC;ALL_TAC] THEN (* added OCt 17, 2010 *)
 937   (SUBGOAL_THEN `!x. ((x < &0) <=> (unit0 * x < &0)) /\
 938      ((x <= &0) <=> (unit0 * x <= &0))` (fun t -> ONCE_REWRITE_TAC[t]))
 939   THENL [REWRITE_TAC[unit0;REAL_ARITH `&1 * x = x`];ALL_TAC] THEN
 940   (REWRITE_TAC[REAL_ARITH `f x1 x2 x3 x4 x5 x6 * (y:real) =
 941        y * f x1 x2 x3 x4 x5 x6 /\ ((x * y) * z = x * y * z)`]) THEN
 942   (REWRITE_TAC[real_arith_unit]) THEN
 943   (REWRITE_TAC[REAL_ARITH `unit0 * x = x * unit0`]) THEN
 944   (REWRITE_TAC[unit0f]) THEN
 945     (SUBGOAL_THEN subgoal_proj  (fun t-> REWRITE_TAC[t])
 946   THENL [REWRITE_TAC[proj_x3;proj_x4;proj_x5;proj_x6;proj_x2;
 947                     proj_x1;unit0;REAL_ARITH `x * &1 = x`];ALL_TAC]) THEN
 948   (SUBGOAL_THEN subgoal_unit6  (fun t-> REWRITE_TAC[t])
 949      THENL [REWRITE_TAC[unit0;unit6];ALL_TAC]) THEN
 950   (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN
 951   (REWRITE_TAC[GSYM ineq_expand9]) THEN
 952   (REWRITE_TAC[GSYM ineq_expand6]) THEN DISCH_TAC;;
 953
 954 let WRAPUP_TAC =
 955   (REWRITE_TAC[REAL_ARITH `(x * y * (z:real)) = (x * y) * z`]) THEN
 956   (REWRITE_TAC[REAL_ARITH `(y:real) * f x1 x2 x3 x4 x5 x6 =
 957        (f x1 x2 x3 x4 x5 x6) *  y `]) THEN
 958   (REWRITE_TAC[REAL_ARITH ` -- (x * y) = x * (-- y) `]) THEN
 959   (REWRITE_TAC[REAL_ARITH ` -- (f x1 x2 x3 x4 x5 x6) =
 960        f x1 x2 x3 x4 x5 x6 * -- &1`]) THEN
 961   (REWRITE_TAC[REAL_ARITH `(x * y) * (z:real) = x * y * z`]) THEN
 962   (REWRITE_TAC[REAL_ARITH `inv y = (&1/y)`]);;
 963
 964
 965
 966
 967 (* ========================================================================== *)
 968 (*    VERIFYING INEQUALITIES                                                  *)
 969 (* ========================================================================== *)
 970
 971 let idq_fields idq = (idq.idv,idq.tags, idq.ineq);;
 972
 973 (*
 974 let preprocess (s,tags,case) =
 975   let is_xconvert = mem Xconvert tags in
 976   let is_branch = mem Branching tags in
 977   let strip_let_case = strip_let_tm case in
 978   let _ = report ("process and exec: "^s) in
 979   let _ = g (strip_let_case) in
 980   let _ = e(PRELIM_REWRITE_TAC) in
 981   let NONLIN_INTRO = e(MP_TAC (REWRITE_RULE[] NONLIN)) in
 982   let _ = if (is_branch) then e(BRANCH_TAC) else e(ALL_TAC) in
 983   let _ = if (is_xconvert) then e (X_OF_Y_TAC) else e(ALL_TAC) in
 984   let _ =   if (is_branch && not(is_xconvert)) then
 985     e(SERIES3Q1H_5D_TAC) else e(ALL_TAC) in
 986   let _ = e (STYLIZE_TAC) in
 987   let _ = e (WRAPUP_TAC) in
 988   let testineq = snd(top_goal()) in
 989     (s,tags,testineq);;
 990 *)
 991
 992 (* rewritten Jan 28, 2013 *)
 993
 994 let preprocess (s,tags,case) =
 995   let is_xconvert = mem Xconvert tags in
 996   let is_branch = mem Branching tags in
 997   let _ = report ("process and exec: "^s) in
 998   let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV) in
 999   let tacl =
1000     [LET_ELIM_TAC;
1001      PRELIM_REWRITE_TAC;
1002      MP_TAC (REWRITE_RULE[] NONLIN);
1003      if (is_branch) then BRANCH_TAC else ALL_TAC;
1004      if (is_xconvert) then X_OF_Y_TAC else ALL_TAC;
1005      if (is_branch && not(is_xconvert)) then SERIES3Q1H_5D_TAC else ALL_TAC;
1006      STYLIZE_TAC;
1007      WRAPUP_TAC] in
1008   let _ = g (case) in
1009   let _ = e (EVERY tacl) in
1010   let testineq = snd(top_goal()) in
1011     (s,tags,testineq);;
1012
1013 let process_and_exec ex (s,tags,case) =
1014   let _ = report ("process and exec: "^s) in
1015   let (s,tags,testineq) = preprocess (s,tags,case) in
1016     execute_interval ex tags s testineq;;
1017
1018 (*
1019 let process_and_exec ex (s,tags,case) =
1020   let _ = report ("process and exec: "^s) in
1021   let is_xconvert = mem Xconvert tags in
1022   let is_branch = mem Branching tags in
1023   let strip_let_case = strip_let_tm case in
1024   let _ = report ("process and exec: "^s) in
1025   let _ = g (strip_let_case) in
1026   let _ = e(PRELIM_REWRITE_TAC) in
1027   let NONLIN_INTRO = e(MP_TAC (REWRITE_RULE[] NONLIN)) in
1028   let _ = if (is_branch) then e(BRANCH_TAC) else e(ALL_TAC) in
1029   let _ = if (is_xconvert) then e (X_OF_Y_TAC) else e(ALL_TAC) in
1030   let _ =   if (is_branch && not(is_xconvert)) then
1031     e(SERIES3Q1H_5D_TAC) else e(ALL_TAC) in
1032   let _ = e (STYLIZE_TAC) in
1033   let _ = e (WRAPUP_TAC) in
1034   let testineq = snd(top_goal()) in
1035     execute_interval ex tags s testineq;;
1036 *)
1037
1038
1039 (*
1040
1041 let get_firstexact s = idq_fields (hd(Ineq.getexact s));;
1042
1043 let process_and_exec_by_id ex s =
1044   let testcase = get_firstexact  s in
1045     process_and_exec ex s testcase;;
1046
1047 testsplit_idq
1048   ** strips let
1049   ** splits cases at h0 according to the split tags
1050   ** ships the cases off to process_and_exec.
1051 *)
1052
1053 (*
1054 let testsplit_idq ex idq =
1055   let (s,tags,ineq) = idq_fields idq in
1056   let ineq_strip_let = strip_let_tm ineq in
1057   let suffix i n = Printf.sprintf "%s split(%d/%d)" s i n in
1058   let ls = get_split_tags idq in
1059     if (ls = []) then process_and_exec ex (s,tags,ineq_strip_let) else
1060       let cases = split_all_h0  [(ineq_strip_let, ls)] in
1061       let n = length cases in
1062         for i=0 to (n - 1) do
1063           try (process_and_exec ex (suffix i n,tags,(List.nth cases i)))
1064           with Failure s -> failwith (s ^ " case fail: " ^(string_of_int i))
1065         done;;
1066 *)
1067
1068 let preprocess_split_idq idq =
1069   let (s,tags,ineq) = idq_fields idq in
1070   let ineq_strip_let = strip_let_tm ineq in
1071   let suffix i n = Printf.sprintf "%s split(%d/%d)" s i n in
1072   let ls = get_split_tags idq in
1073     if (ls = []) then [preprocess (s,tags,ineq_strip_let)] else
1074       let cases = split_all_h0  [(ineq_strip_let, ls)] in
1075       let n = length cases in
1076         map (fun i ->
1077             try preprocess (suffix i n,tags,List.nth cases i)
1078             with Failure s -> failwith (s^ " case fail: " ^ (string_of_int i)))
1079           (0--(n-1));;
1080
1081 let testsplit_idq ex idq =
1082   let splits = preprocess_split_idq idq in
1083     map (fun (s,tags,testineq) -> execute_interval ex tags s testineq) splits;;
1084
1085 let testsplit ex s = testsplit_idq ex (hd (Ineq.getexact s));;
1086
1087
1088 end;;