formal_ineqs/examples.hl

   1 (* Several simple examples *)
   2
   3 (* Set up the loading path:
   4 load_path := "path to the formal_ineqs directory" :: !load_path;;
   5 *)
   6
   7 (* Change default arithmetic options before loading other libraries *)
   8 (* (arithmetic options cannot be changed later) *)
   9 needs "arith_options.hl";;
  10
  11 (* Set the base of natural number arithmetic to 200 *)
  12 Arith_options.base := 200;;
  13
  14 (* Load all verification libraries *)
  15 (* Note: the verification library loads Multivariate/realanalysis.ml,
  16    so it is recommended to use a checkpointed version of HOL Light
  17    with preloaded realanalysis.ml *)
  18 needs "verifier/m_verifier_main.hl";;
  19
  20 (*
  21   Set the level of info/debug printing:
  22   0 - no info/debug printing
  23   1 - report important steps (default)
  24   2 - report everything
  25 *)
  26 needs "verifier_options.hl";;
  27 Verifier_options.info_print_level := 1;;
  28
  29 (* Open the main verification module *)
  30 open M_verifier_main;;
  31
  32
  33 (* Several simple tests *)
  34
  35 (* default_params: default verification parameters *)
  36 (* 5: precision parameter for floating point arithmetic *)
  37 let test1 () =
  38   verify_ineq default_params 5 `sqrt(pi) < #1.773`;;
  39
  40 let test2 () =
  41   verify_ineq default_params 11 `#1.230959417 < acs(&1 / &3)`;;
  42
  43 let test3 () =
  44   verify_ineq default_params 11 `#1.230959418 > acs(&1 / &3)`;;
  45
  46 (* An approximation of atn *)
  47 let test4 () =
  48   let ineq1 = `&0 <= x /\ x <= &1 ==> atn x - x / (&1 + #0.28 * x * x) < #0.005` in
  49   let ineq2 = `&0 <= x /\ x <= &1 ==> -- #0.005 < atn x - x / (&1 + #0.28 * x * x)` in
  50     [verify_ineq default_params 5 ineq1;
  51      verify_ineq default_params 6 ineq2];;
  52
  53 (* A polynomial approximation of atn *)
  54 (* Taken from: *)
  55 (* Marc Daumas, David Lester, and César Muñoz,
  56    Verified real number calculations: A library for interval arithmetic,
  57    IEEE Transactions on Computers, Volume 58, Number 2, 2009. *)
  58 let test5 () =
  59   let ineq1 = `-- &1 / &30 <= x /\ x <= &1 / &30 ==> x * (&1 - (x * x) * (&11184811 / &33554432 - (x * x) * (&13421773 / &67108864))) - atn x < #0.1 pow 7` in
  60   let ineq2 = `-- &1 / &30 <= x /\ x <= &1 / &30 ==> -- (#0.1 pow 7) < x * (&1 - (x * x) * (&11184811 / &33554432 - (x * x) * (&13421773 / &67108864))) - atn x` in
  61     [verify_ineq default_params 5 ineq1;
  62      verify_ineq default_params 5 ineq2];;
  63
  64
  65 (* Returns a list of theorems with verification information *)
  66 let run_tests () =
  67   [test1(); test2(); test3()] @ test4() @ test5();;
  68
  69 (* Returns a list of theorems *)
  70 let results () =
  71   map fst (run_tests ());;
  72
  73
  74 results();;