legacy/oldnonlinear/nonlinear/experiments/oracle.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: nonlinear inequalities                                            *)
   5 (* Author:  Roland Zumkeller    *)
   6 (* Date: 2010                                                                 *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11 ssh -t wh opt/bin/dmtcp/dmtcp_restart flyspeck.dmtcp
  12 rsync -ahv ~/doc/flyspeck/ wh:ext/flyspeck/ --exclude .svn
  13 *)
  14
  15 module Oracle = struct
  16
  17 #load "unix.cma";; (* on Mac OS unix.cma needs to be pre-cooked into the toplevel with ocamlmktop *)
  18
  19 let sergei_path = "sergei/bin/sergei";;
  20
  21 let dest_decimal x = match strip_comb x with
  22   | (dec,[a;b]) ->                     div_num (dest_numeral a) (dest_numeral b)
  23   | (sqrt8,[]) when sqrt8 = `sqrt8` -> div_num (Int 3880899) (Int 1372105)
  24   | _ -> failwith ("dest_decimal: '" ^ string_of_term x ^ "'") ;;
  25
  26 let string_of_num' x = string_of_float (float_of_num x);; (* rounding :( *)
  27
  28 let rec sergei_of_ccl t =
  29   let soh = sergei_of_ccl in
  30   if is_var t then fst (dest_var t) else
  31   let (f,xs) = strip_comb t in
  32   let ifix i = let [a;b] = xs in "(" ^ soh a ^ " " ^ i ^ " " ^ soh b ^ ")" in
  33   let ifix_swapped i = let [b;a] = xs in "(" ^ soh a ^ " " ^ i ^ " " ^ soh b ^ ")" in
  34   (if not (is_const f) then failwith ("Oracle error: " ^ string_of_term f));
  35   match fst (dest_const f) with
  36   | "real_gt" | "real_ge" | "real_sub" -> ifix "-"
  37   | "real_lt" | "real_le" -> ifix_swapped "-"
  38   | "real_add" -> ifix "+"
  39   | "real_mul" -> ifix "*"
  40   | "real_div" -> ifix "/"
  41   | "real_pow" -> ifix "^"
  42   | "\\/" -> ifix "\\/"
  43   | "atn"      -> let [a] = xs in "Atan [" ^ soh a ^ "]"
  44   | "sqrt"     -> let [a] = xs in "Sqrt [" ^ soh a ^ "]"
  45   | "real_neg" -> let [a] = xs in "(-" ^ soh a ^ ")"
  46   | "pi"       -> let [] = xs in "Pi"
  47   | "real_of_num" -> let [a] = xs in string_of_num' (dest_numeral a) (* is this line redundant ? *)
  48   | "NUMERAL" -> let [a] = xs in string_of_num' (dest_numeral t)
  49   | "DECIMAL" ->  string_of_num' (dest_decimal t)
  50   | "atn2"      -> let [ab] = xs in let (a,b) = dest_pair ab in  "(" ^ soh a ^ " ATN2 " ^ soh b ^ ")"
  51   | s -> failwith ("Encountered unknown constant '" ^ s ^ "'");;
  52
  53 let sergei_of_goal (asms,ccl) =
  54   print_endline "Converting HOL term to sergei format...";
  55   let vars = map (fun (_,axb) ->
  56          let (ax,xb) = dest_conj (concl axb) in
  57          let (a,x) = dest_binary "real_le" ax in
  58          let (x',b) = dest_binary "real_le" xb in
  59            if x <> x' then
  60              failwith ("Malformed assumption: " ^ string_of_term x' ^
  61                        " should be " ^ string_of_term x ^ ".")
  62            else
  63              string_of_num' (dest_decimal a) ^ " <= " ^
  64              string_of_term x ^ " <= " ^
  65              string_of_num' (dest_decimal b) ^ " ->\n") asms
  66   in List.fold_right (^) vars "" ^ " " ^ sergei_of_ccl ccl;;
  67
  68 let SERGEI_TAC : tactic = fun (asms,ccl) ->
  69   print_endline ("Running sergei [" ^ sergei_path ^ "]:");
  70   let (pin,pout) = Unix.open_process ("time " ^ sergei_path ^ " -nv -e0.00001") in
  71     Pervasives.output_string pout (sergei_of_goal (asms,ccl));
  72     close_out pout;
  73     (try while true do
  74       print_endline ("sergei> " ^ input_line pin);
  75       flush stdout
  76     done with End_of_file -> ());
  77     close_in pin; NO_TAC (asms,ccl);;
  78
  79 let SERGEI_DUMP : tactic = fun gl ->
  80   print_endline (sergei_of_goal gl); NO_TAC gl;;
  81
  82 let rec SINGLE_CONV c = c
  83   ORELSEC (fun t -> if is_comb t then
  84              ((RATOR_CONV (SINGLE_CONV c)) ORELSEC (RAND_CONV (SINGLE_CONV c))) t
  85            else failwith "SINGLE_CONV");;
  86
  87 let SINGLE_REWR_TAC e = CONV_TAC (CHANGED_CONV (SINGLE_CONV (REWR_CONV e)));;
  88
  89 let ineq' = define
  90   `(!         c. ineq'                [] c <=> c)
  91 /\ (!a x b xs c. ineq' (CONS (a,x,b) xs) c <=> a <= x /\ x <= b ==> ineq' xs c)`;;
  92
  93 (*
  94   valid:  (except for x=0, y<=0)
  95   useful: y >= 0    (1st & 2nd quadrant)
  96 *)
  97 let ATN2_ATN = prove (`atn2(x,y) = &2 * atn(y / (sqrt (x*x + y*y) + x))`, CHEAT_TAC);;
  98
  99 let ATN2_90 = prove (`atn2(x,y) = atn2(--y,x) - pi/(&2)`, CHEAT_TAC);;
 100
 101 let ATN2_30 = prove (`atn2(x,y) = atn2(sqrt (&3) * x - y, x + sqrt (&3) * y) - pi/(&6)`, CHEAT_TAC);;
 102
 103 let ATN2_60 = prove (`atn2(x,y) = atn2(x - sqrt (&3) * y, sqrt (&3) * x + y) - pi/(&3)`, CHEAT_TAC);;
 104
 105 let ATN2_45 = prove (`atn2(x,y) = atn2(x-y,x+y) - pi/(&4)`, CHEAT_TAC);;
 106
 107 (* rotates atan by atan(t):
 108 valid if we don't cross the discontinuous line *)
 109 let ATN2_ROT_TAN = prove (`atn2 (x,y) = atn2 (x - y*t, y + x*t) - atn t`, CHEAT_TAC);;
 110
 111 (*
 112   valid : x >= 0    (1st & 4th quadrant)
 113   useful: x >= 0 and y fixed   (1st & 4th quadrant)
 114 *)
 115 let ATN2_ATN_XPOS = prove (`atn2(x,y) = atn(y/x)`, CHEAT_TAC);;
 116
 117 (* rotate such that sign y becomes constant, then use ATN2_ATN.  if we
 118    manage to make both sign x and sign y positive, then ATN2_ATN_POS is
 119    valid and useful (smaller formula) *)
 120
 121 let delta = [ Sphere.taum; Sphere.sol_y; Sphere.const1; Sphere.lnazim;
 122               Sphere.delta_x; Sphere.delta_x4; Sphere.ly; Sphere.interp; Sphere.rhazim; Sphere.tauq;
 123               Pack_defs.lmfun (*COND*); Sphere.rho; Sphere.arclength; Sphere.ups_x; Sphere.dih_x; Sphere.dih_y;
 124 Enclosed.enclosed;
 125 Quadratic_root_plus.quadratic_root_plus;
 126 Abc_of_quadratic.abc_of_quadratic;
 127 Mur.muR; Cayleyr.cayleyR ];;
 128
 129 let PREP =
 130   ((REPEAT GEN_TAC) THEN (REWRITE_TAC [prove (`ineq = ineq'`, CHEAT_TAC)]) THEN (REWRITE_TAC [ineq'])) THEN
 131   ((REWRITE_TAC delta) THEN (CONV_TAC (TOP_DEPTH_CONV let_CONV)) THEN (REPEAT DISCH_TAC));;
 132
 133
 134 end;;