1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: nonlinear inequalities *)
5 (* Author: Thomas Hales *)
7 (* ========================================================================== *)
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++.
17 flyspeck_needs "general/sphere.hl";;
18 flyspeck_needs "nonlinear/ineq.hl";;
19 flyspeck_needs "nonlinear/lemma.hl";;
22 module Optimize = struct
25 open Nonlinear_lemma;;
28 let length = List.length;;
31 let svn_version = Flyspeck_lib.svn_version;;
33 let ineq = Sphere.ineq;;
34 let all_forall = Sphere.all_forall;;
38 let nub = Flyspeck_lib.nub;;
40 let join_comma = Flyspeck_lib.join_comma;;
41 let join_space = Flyspeck_lib.join_space;;
42 let join_lines = Flyspeck_lib.join_lines;;
44 let string_of_num' = Flyspeck_lib.string_of_num';;
45 let dest_decimal = Flyspeck_lib.dest_decimal;;
47 let strip_let_tm = Nonlinear_lemma.strip_let_tm;;
49 let output_filestring = Flyspeck_lib.output_filestring;;
51 let BY = Hales_tactic.BY;;
52 let unlist = Hales_tactic.unlist;;
54 (* from glpk_link.ml *)
56 let load_and_close_channel_true = Flyspeck_lib.load_and_close_channel_true;;
58 let load_file = Flyspeck_lib.load_file;;
60 (* ========================================================================= *)
61 (* GENERAL PROCEDURES *)
62 (* ========================================================================= *)
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
68 let NONLIN = new_definition `NONLIN = T`;;
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;;
75 let quoted s = let q = "\"" in (q^s^q);;
77 let paren s = "("^ s ^")";;
79 let real_ty = `:real`;;
80 let mk_x i = mk_var("x"^string_of_int i,real_ty);;
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];;
86 let xspec = SPECL x6list;;
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
98 (* renames variables as x1,x2,x3,.... *)
100 let (X_RENAME_TAC:tactic) =
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 ;;
108 (* ========================================================================= *)
109 (* SPLITTING INEQUALITIES AT h0 *)
110 (* ========================================================================= *)
112 let get_split_tags idq =
114 let rec gs = (function
117 | _ :: rs -> gs rs) in
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;;
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;;
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]);;
147 let h0cutA = prove_by_refinement(
148 `!y. (y <= &2 * h0) ==> ((h0cut y) = &1)`,
151 MESON_TAC[Sphere.h0cut]
155 let h0cutB = prove_by_refinement(
156 `!y. (&2 * h0 < y) ==> ((h0cut y) = &0)`,
159 REWRITE_TAC[Sphere.h0cut];
161 BY(COND_CASES_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
165 let h0cutC = prove_by_refinement(
166 `!y. (y <= &2 * hminus) ==> (h0cut y = &1)`,
171 MP_TAC Nonlinear_lemma.hminus_lt_h0;
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]);;
191 (* WARNING: This disturbs the goal *)
193 let split_h0 (ineq,ss) =
194 let current_goals() =
196 ((fun (_,b,_) -> b) (hd (!current_goalstack))) in
197 let split_h0_term i inq =
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;;
205 let rec split_all_h0 = function
207 | (i,[])::rs -> i :: split_all_h0 rs
208 | r::rs -> split_all_h0 (split_h0 r @ rs);;
212 (* ========================================================================== *)
213 (* PARSING INEQUALITIES *)
214 (* ========================================================================== *)
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
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);;
230 (* these names don't change in cpp interval code *)
232 let idem_assoc = [];; (* make it the default *)
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. *)
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");
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");
287 gradually eliminate this list.
288 The default will be to have the same names.
293 let p (a,b) = (a, (pref^b)) in map p
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");
306 try Lib.assoc s native_fun
308 try Lib.assoc s cpp_assoc
309 with Failure _ -> s;;
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");
320 let cpp_of_constant s =
321 try (assoc s cpp0_assoc) with
322 Failure _ -> failwith (s^" find: cpp_of_constant") ;;
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));;
332 (* 2013-08-14, changed for AWS compiler. was interval::interval( ... ) *)
333 let i_mk s = "interval("^quoted s ^")";;
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
341 let cpp_string_of_term =
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))
362 then "("^cpp_of_constant s^")"
363 else paren(cpp_of_fun soh x6list s xs) in
366 with Failure s -> failwith (s^" ....... "^string_of_term t);;
368 (* generation of cpp code *)
370 let cpp_template_taylor c (i,s) = Printf.sprintf
371 " Function F%s%d = %s;" c i s;;
373 let cpp_template_t c iis =
375 (map (cpp_template_taylor c) (zip (1--(length iis)) iis));;
377 let cpp_template_F c i = Printf.sprintf "&F%s%d" c i;;
379 let cpp_template_Fc c len = join_comma
380 (map (cpp_template_F c) (1-- len));;
382 let rec delta126min = function
384 | Delta126min t :: _ -> t
385 | _ :: a -> delta126min a;;
387 let rec widthCut = function
389 | Widthcutoff t::_ -> (true,t)
390 | _:: a -> widthCut a;;
392 let rec delta126max = function
394 | Delta126max t :: _ -> t
395 | _ :: a -> delta126max a;;
397 let rec delta135min = function
399 | Delta135min t :: _ -> t
400 | _ :: a -> delta135min a;;
402 let rec delta135max = function
404 | Delta135max t :: _ -> t
405 | _ :: a -> delta135max a;;
407 let cpp_template_gen = Printf.sprintf "
408 const char svn[] = %s;
409 const char ineq_id[] = %s;
411 int testRun() // autogenerated code
415 domain x = domain::lowerD(tx);
416 domain z = domain::upperD(tz);
420 const Function* I[%d] = {%s}; // len ...
422 opt.allowSharp = %d; // sharp
423 opt.onlyCheckDeriv1Negative = %d; // checkderiv
425 return prove::recursiveVerifier(0,x,z,x0,z0,I,%d,opt); // len
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
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;;
466 let has_subterm sub tm =
467 can (find_term ((=) sub)) tm;;
469 let has_cross_diag = has_subterm `quad_cross_diag2_x`;;
471 let has_delta_top = has_subterm `delta_top_x`;;
473 let is_quad_cluster tags = (can (find (function Quad_cluster _ -> true | _ -> false)) tags);;
475 let quad_margin tags = (function Quad_cluster t -> t | _ -> 0.0)
476 (find ((function Quad_cluster _ -> true | _ -> false)) tags);;
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
483 let partition_quad_term 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);;
501 let cppq_template_gen = Printf.sprintf "
505 int testRun() // quad cluster case, autogenerated code
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);
518 const Function* IA[%d] = {%s};
519 const Function* IB[%d] = {%s};
522 return prove::recursiveVerifierQ(0,xA,xB,zA,zB,IA,IB,%d,opt);
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 *)
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 *)
541 Printf.sprintf "opt.crossDiagMinEnclosed = interMath::inf(%s);\n";;
544 Printf.sprintf "opt.crossDiagMinDelta = interMath::inf(%s);\n";;
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
566 ( cde_template (cpp ( get_cross_diag_squared is9) ))
570 ( cdt_template (cpp ( get_delta_top_squared is9) ))
573 if (mem Dim_red_backsym tags)
574 then "\topt.dimRedBackSym = 1;\n" else "" in
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 ;;
585 let t = snd(top_goal());;
587 let tags = [Quad_cluster 3.0];;
590 (* next: put together header, proc, tail and run *)
592 let tmpfile = flyspeck_dir^"/../interval_code/test_auto.cc";;
594 let cpp_header() = join_lines (load_file (flyspeck_dir^"/../interval_code/generic_head.txt"));;
596 let cpp_tail() = join_lines (load_file (flyspeck_dir^"/../interval_code/generic_tail.txt"));;
598 let mkfile_cpp t s tags =
599 output_filestring tmpfile
600 (join_lines [cpp_header(); (mk_cpp_proc t s tags);cpp_tail()]);;
602 let mkfile_cppq t s tags =
603 output_filestring tmpfile
604 (join_lines [cpp_header(); (mk_cppq_proc t s tags);cpp_tail()]);;
607 let err = Filename.temp_file "cpp_err" ".txt" in
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
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
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
625 (* ========================================================================== *)
626 (* MEGA PREP TACTICS *)
627 (* ========================================================================== *)
629 (* *************************************************************************** *)
631 (* *************************************************************************** *)
635 Sphere.x1_delta_y;Sphere.delta4_squared_y;
636 vol4f_palt;Nonlinear_lemma.y_of_x_e;
638 Sphere.vol3r;Sphere.vol2f;Sphere.gamma4f;
639 Sphere.gamma3f; GSYM Nonlinear_lemma.quadratic_root_plus_curry;
641 REAL_MUL_RZERO;FST;SND;
642 Sphere.node2_y;Sphere.node3_y] @
643 (!Ineq.dart_classes));;
645 let PRELIM_REWRITE_TAC = EVERY[
646 (REWRITE_TAC[GSYM Sphere.rad2_y]) ;
647 (REWRITE_TAC(macro_expand)) ;
650 (* *************************************************************************** *)
652 (* *************************************************************************** *)
654 (* take care of branching *)
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];
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);
666 gcy_low;gcy_low_const;gcy_low_hminus;gcy_high;gcy_high_hplus;
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';
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];
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`)]);
684 REWRITE_TAC[Sphere.pathL;Sphere.pathR]; (* moved May 24, 2011 *)
687 (* *************************************************************************** *)
688 (* *************************************************************************** *)
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);
700 let SQRT_SQRT_TAC = EVERY[
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`
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);
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`;
749 let rec get_consts tm =
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 ;;
756 let get_goal_const gl =
757 let w = goal_concl gl in
761 let X_SQRT_COMPOUND_ORDER_TAC:tactic =
763 let (asl,a) = dest_goal gl 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
772 let X_SQRT_COMPOUND_ORDER_TAC:tactic =
774 let (asl,a) = dest_goal gl 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
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;
792 let decimal = REWRITE_RULE [REAL_ARITH `&2 = #2.0`];;
794 let X_COMPOUND_DEF = [REAL_ARITH `&2 = #2.0`;
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;
803 GSYM Sphere.ldih_x;GSYM Sphere.ldih2_x;
804 GSYM Sphere.ldih3_x;GSYM Sphere.ldih6_x;
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
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
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
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] ;;
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];;
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] ;;
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]) ;;
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]) ;;
854 (* for 1d inequality involving vol2f marchal *)
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]] ;;
868 [Sphere.a_spine5;Sphere.b_spine5;Sphere.mm1;
869 Sphere.flat_term;Sphere.beta_bump_lb;REAL_POW_2;
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 *)
878 (* *************************************************************************** *)
880 (* *************************************************************************** *)
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]);;
896 (* *************************************************************************** *)
897 (* STYLIZE and WRAPUP *)
898 (* *************************************************************************** *)
902 REAL_ARITH `(x < y <=> (x- y < &0)) /\ (x <= y <=> (x-y <= &0))` in
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
920 DISCH_TAC THEN REPEAT GEN_TAC THEN
921 (* rename added Nov 27, 2010 *)
925 (* prev line added Sep 8 , 2010 *)
926 REWRITE_TAC DEF_expand THEN
927 (* prev line moved down sep 8 *)
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
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;;
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)`]);;
967 (* ========================================================================== *)
968 (* VERIFYING INEQUALITIES *)
969 (* ========================================================================== *)
971 let idq_fields idq = (idq.idv,idq.tags, idq.ineq);;
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
992 (* rewritten Jan 28, 2013 *)
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
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;
1009 let _ = e (EVERY tacl) in
1010 let testineq = snd(top_goal()) in
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;;
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;;
1041 let get_firstexact s = idq_fields (hd(Ineq.getexact s));;
1043 let process_and_exec_by_id ex s =
1044 let testcase = get_firstexact s in
1045 process_and_exec ex s testcase;;
1049 ** splits cases at h0 according to the split tags
1050 ** ships the cases off to process_and_exec.
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))
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
1077 try preprocess (suffix i n,tags,List.nth cases i)
1078 with Failure s -> failwith (s^ " case fail: " ^ (string_of_int i)))
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;;
1085 let testsplit ex s = testsplit_idq ex (hd (Ineq.getexact s));;