1 (* Several simple examples *)
3 (* Set up the loading path:
4 load_path := "path to the formal_ineqs directory" :: !load_path;;
7 (* Change default arithmetic options before loading other libraries *)
8 (* (arithmetic options cannot be changed later) *)
9 needs "arith_options.hl";;
11 (* Set the base of natural number arithmetic to 200 *)
12 Arith_options.base := 200;;
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";;
21 Set the level of info/debug printing:
22 0 - no info/debug printing
23 1 - report important steps (default)
26 needs "verifier_options.hl";;
27 Verifier_options.info_print_level := 1;;
29 (* Open the main verification module *)
30 open M_verifier_main;;
33 (* Several simple tests *)
35 (* default_params: default verification parameters *)
36 (* 5: precision parameter for floating point arithmetic *)
38 verify_ineq default_params 5 `sqrt(pi) < #1.773`;;
41 verify_ineq default_params 11 `#1.230959417 < acs(&1 / &3)`;;
44 verify_ineq default_params 11 `#1.230959418 > acs(&1 / &3)`;;
46 (* An approximation of atn *)
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];;
53 (* A polynomial approximation of atn *)
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. *)
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];;
65 (* Returns a list of theorems with verification information *)
67 [test1(); test2(); test3()] @ test4() @ test5();;
69 (* Returns a list of theorems *)
71 map fst (run_tests ());;