(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: nonlinear inequalities *) (* Author: Roland Zumkeller *) (* Date: 2010 *) (* ========================================================================== *) (* ssh -t wh opt/bin/dmtcp/dmtcp_restart flyspeck.dmtcp rsync -ahv ~/doc/flyspeck/ wh:ext/flyspeck/ --exclude .svn *) module Oracle = struct #load "unix.cma";; (* on Mac OS unix.cma needs to be pre-cooked into the toplevel with ocamlmktop *) let sergei_path = "sergei/bin/sergei";; let dest_decimal x = match strip_comb x with | (dec,[a;b]) -> div_num (dest_numeral a) (dest_numeral b) | (sqrt8,[]) when sqrt8 = `sqrt8` -> div_num (Int 3880899) (Int 1372105) | _ -> failwith ("dest_decimal: '" ^ string_of_term x ^ "'") ;; let string_of_num' x = string_of_float (float_of_num x);; (* rounding :( *) let rec sergei_of_ccl t = let soh = sergei_of_ccl in if is_var t then fst (dest_var t) else let (f,xs) = strip_comb t in let ifix i = let [a;b] = xs in "(" ^ soh a ^ " " ^ i ^ " " ^ soh b ^ ")" in let ifix_swapped i = let [b;a] = xs in "(" ^ soh a ^ " " ^ i ^ " " ^ soh b ^ ")" in (if not (is_const f) then failwith ("Oracle error: " ^ string_of_term f)); match fst (dest_const f) with | "real_gt" | "real_ge" | "real_sub" -> ifix "-" | "real_lt" | "real_le" -> ifix_swapped "-" | "real_add" -> ifix "+" | "real_mul" -> ifix "*" | "real_div" -> ifix "/" | "real_pow" -> ifix "^" | "\\/" -> ifix "\\/" | "atn" -> let [a] = xs in "Atan [" ^ soh a ^ "]" | "sqrt" -> let [a] = xs in "Sqrt [" ^ soh a ^ "]" | "real_neg" -> let [a] = xs in "(-" ^ soh a ^ ")" | "pi" -> let [] = xs in "Pi" | "real_of_num" -> let [a] = xs in string_of_num' (dest_numeral a) (* is this line redundant ? *) | "NUMERAL" -> let [a] = xs in string_of_num' (dest_numeral t) | "DECIMAL" -> string_of_num' (dest_decimal t) | "atn2" -> let [ab] = xs in let (a,b) = dest_pair ab in "(" ^ soh a ^ " ATN2 " ^ soh b ^ ")" | s -> failwith ("Encountered unknown constant '" ^ s ^ "'");; let sergei_of_goal (asms,ccl) = print_endline "Converting HOL term to sergei format..."; let vars = map (fun (_,axb) -> let (ax,xb) = dest_conj (concl axb) in let (a,x) = dest_binary "real_le" ax in let (x',b) = dest_binary "real_le" xb in if x <> x' then failwith ("Malformed assumption: " ^ string_of_term x' ^ " should be " ^ string_of_term x ^ ".") else string_of_num' (dest_decimal a) ^ " <= " ^ string_of_term x ^ " <= " ^ string_of_num' (dest_decimal b) ^ " ->\n") asms in List.fold_right (^) vars "" ^ " " ^ sergei_of_ccl ccl;; let SERGEI_TAC : tactic = fun (asms,ccl) -> print_endline ("Running sergei [" ^ sergei_path ^ "]:"); let (pin,pout) = Unix.open_process ("time " ^ sergei_path ^ " -nv -e0.00001") in Pervasives.output_string pout (sergei_of_goal (asms,ccl)); close_out pout; (try while true do print_endline ("sergei> " ^ input_line pin); flush stdout done with End_of_file -> ()); close_in pin; NO_TAC (asms,ccl);; let SERGEI_DUMP : tactic = fun gl -> print_endline (sergei_of_goal gl); NO_TAC gl;; let rec SINGLE_CONV c = c ORELSEC (fun t -> if is_comb t then ((RATOR_CONV (SINGLE_CONV c)) ORELSEC (RAND_CONV (SINGLE_CONV c))) t else failwith "SINGLE_CONV");; let SINGLE_REWR_TAC e = CONV_TAC (CHANGED_CONV (SINGLE_CONV (REWR_CONV e)));; let ineq' = define `(! c. ineq' [] c <=> c) /\ (!a x b xs c. ineq' (CONS (a,x,b) xs) c <=> a <= x /\ x <= b ==> ineq' xs c)`;; (* valid: (except for x=0, y<=0) useful: y >= 0 (1st & 2nd quadrant) *) let ATN2_ATN = prove (`atn2(x,y) = &2 * atn(y / (sqrt (x*x + y*y) + x))`, CHEAT_TAC);; let ATN2_90 = prove (`atn2(x,y) = atn2(--y,x) - pi/(&2)`, CHEAT_TAC);; let ATN2_30 = prove (`atn2(x,y) = atn2(sqrt (&3) * x - y, x + sqrt (&3) * y) - pi/(&6)`, CHEAT_TAC);; let ATN2_60 = prove (`atn2(x,y) = atn2(x - sqrt (&3) * y, sqrt (&3) * x + y) - pi/(&3)`, CHEAT_TAC);; let ATN2_45 = prove (`atn2(x,y) = atn2(x-y,x+y) - pi/(&4)`, CHEAT_TAC);; (* rotates atan by atan(t): valid if we don't cross the discontinuous line *) let ATN2_ROT_TAN = prove (`atn2 (x,y) = atn2 (x - y*t, y + x*t) - atn t`, CHEAT_TAC);; (* valid : x >= 0 (1st & 4th quadrant) useful: x >= 0 and y fixed (1st & 4th quadrant) *) let ATN2_ATN_XPOS = prove (`atn2(x,y) = atn(y/x)`, CHEAT_TAC);; (* rotate such that sign y becomes constant, then use ATN2_ATN. if we manage to make both sign x and sign y positive, then ATN2_ATN_POS is valid and useful (smaller formula) *) let delta = [ Sphere.taum; Sphere.sol_y; Sphere.const1; Sphere.lnazim; Sphere.delta_x; Sphere.delta_x4; Sphere.ly; Sphere.interp; Sphere.rhazim; Sphere.tauq; Pack_defs.lmfun (*COND*); Sphere.rho; Sphere.arclength; Sphere.ups_x; Sphere.dih_x; Sphere.dih_y; Enclosed.enclosed; Quadratic_root_plus.quadratic_root_plus; Abc_of_quadratic.abc_of_quadratic; Mur.muR; Cayleyr.cayleyR ];; let PREP = ((REPEAT GEN_TAC) THEN (REWRITE_TAC [prove (`ineq = ineq'`, CHEAT_TAC)]) THEN (REWRITE_TAC [ineq'])) THEN ((REWRITE_TAC delta) THEN (CONV_TAC (TOP_DEPTH_CONV let_CONV)) THEN (REPEAT DISCH_TAC));; end;;