formal_ineqs/examples_poly.hl

   1 (* Multivariate polynomial inequalities *)
   2 (* Examples are taken from the paper:
   3    César Muñoz and Anthony Narkawicz,
   4    Formalization of a Representation of Bernstein Polynomials and Applications to Global Optimization,
   5    Journal of Automated Reasoning, DOI: 10.1007/s10817-012-9256-3
   6    http://shemesh.larc.nasa.gov/people/cam/Bernstein/ *)
   7
   8
   9 (* Set up the loading path:
  10 load_path := "path to the formal_ineqs directory" :: !load_path;;
  11 *)
  12
  13 (* Change default arithmetic options before loading other libraries *)
  14 (* (arithmetic options cannot be changed later) *)
  15 needs "arith_options.hl";;
  16
  17 (* Set the base of natural number arithmetic to 200 *)
  18 Arith_options.base := 200;;
  19
  20 (* Load all verification libraries *)
  21 (* Note: the verification library loads Multivariate/realanalysis.ml,
  22    so it is recommended to use a checkpointed version of HOL Light
  23    with preloaded realanalysis.ml *)
  24 needs "verifier/m_verifier_main.hl";;
  25
  26 (*
  27   Set the level of info/debug printing:
  28   0 - no info/debug printing
  29   1 - report important steps (default)
  30   2 - report everything
  31 *)
  32 needs "verifier_options.hl";;
  33 Verifier_options.info_print_level := 1;;
  34
  35 (* Open the main verification module *)
  36 open M_verifier_main;;
  37
  38
  39 (* Data *)
  40
  41 (* Polynomials *)
  42 let schwefel_poly = `(x1 - x2 pow 2) pow 2 + (x2 - &1) pow 2 +
  43   (x1 - x3 pow 2) pow 2 + (x3 - &1) pow 2` and
  44
  45     rd_poly = `-- x1 + &2 * x2 - x3 - #0.835634534 * x2 * (&1 + x2)` and
  46
  47     caprasse_poly = `-- x1 * x3 pow 3 + &4 * x2 * x3 pow 2 * x4 +
  48   &4 * x1 * x3 * x4 pow 2 + &2 * x2 * x4 pow 3 + &4 * x1 * x3 + &4 * x3 pow 2 -
  49   &10 * x2 * x4 - &10 * x4 pow 2 + &2` and
  50
  51     lv_poly = `x1 * x2 pow 2 + x1 * x3 pow 2 + x1 * x4 pow 2 - #1.1 * x1 + &1` and
  52
  53     butcher_poly = `x6 * x2 pow 2 + x5 * x3 pow 2 - x1 * x4 pow 2 + x4 pow 2 -
  54   &1 / &3 * x1 + &4 / &3 * x4` and
  55
  56     magnetism_poly = `x1 pow 2 + &2 * x2 pow 2 + &2 * x3 pow 2 + &2 * x4 pow 2 +
  57   &2 * x5 pow 2 + &2 * x6 pow 2 + &2 * x7 pow 2 - x1` and
  58
  59     heart_poly = `-- x1 * x6 pow 3 + &3 * x1 * x6 * x7 pow 2 - x3 * x7 pow 3 +
  60   &3 * x3 * x7 * x6 pow 2 - x2 * x5 pow 3 + &3 * x2 * x5 * x8 pow 2 - x4 * x8 pow 3 +
  61   &3 * x4 * x8 * x5 pow 2 - #0.9563453`;;
  62
  63 (* Minimal values *)
  64 let schwefel_min = `-- #0.00000000058806` and
  65     rd_min = `-- #36.7126907` and
  66     caprasse_min = `-- #3.1801` and
  67     lv_min = `-- #20.801` and
  68     butcher_min = `-- #1.44` and
  69     magnetism_min = `-- #0.25001` and
  70     heart_min = `-- #1.7435`;;
  71
  72 (* Domains *)
  73 let schwefel_dom = `[-- &10; -- &10; -- &10]`, `[&10; &10; &10]` and
  74     rd_dom = `[-- &5; -- &5; -- &5]`, `[&5; &5; &5]` and
  75     caprasse_dom = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]`, `[#0.5; #0.5; #0.5; #0.5]` and
  76     lv_dom = `[-- &2; -- &2; -- &2; -- &2]`, `[&2; &2; &2; &2]` and
  77     butcher_dom = `[-- &1; -- #0.1; -- #0.1; -- &1; -- #0.1; -- #0.1]`,
  78   `[&0; #0.9; #0.5; -- #0.1; -- #0.05; -- #0.03]` and
  79     magnetism_dom = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]`,
  80   `[&1; &1; &1; &1; &1; &1; &1]` and
  81     heart_dom = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]`,
  82   `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
  83
  84
  85 let mk_poly_ineq poly_tm min_tm dom =
  86   let n = length (frees poly_tm) in
  87   let xs = map (fun i -> "x"^string_of_int i) (1--n) in
  88   let ineq_tm = mk_binop `(<):real->real->bool` min_tm poly_tm in
  89   let ineq2_tm = M_verifier_main.mk_ineq ineq_tm xs dom in
  90     ineq2_tm;;
  91
  92 (* Create all inequalities *)
  93 let schwefel_ineq,
  94   rd_ineq,
  95   caprasse_ineq,
  96   lv_ineq,
  97   butcher_ineq,
  98   magnetism_ineq,
  99   heart_ineq =
 100   mk_poly_ineq schwefel_poly schwefel_min schwefel_dom,
 101   mk_poly_ineq rd_poly rd_min rd_dom,
 102   mk_poly_ineq caprasse_poly caprasse_min caprasse_dom,
 103   mk_poly_ineq lv_poly lv_min lv_dom,
 104   mk_poly_ineq butcher_poly butcher_min butcher_dom,
 105   mk_poly_ineq magnetism_poly magnetism_min magnetism_dom,
 106   mk_poly_ineq heart_poly heart_min heart_dom;;
 107
 108
 109 (* Tests *)
 110
 111 let test_schwefel () =
 112   verify_ineq default_params 5 schwefel_ineq;;
 113
 114 let test_rd () =
 115   verify_ineq default_params 5 rd_ineq;;
 116
 117 let test_caprasse () =
 118   verify_ineq default_params 5 caprasse_ineq;;
 119
 120 let test_lv () =
 121   verify_ineq default_params 5 lv_ineq;;
 122
 123 let test_butcher () =
 124   verify_ineq default_params 5 butcher_ineq;;
 125
 126 let test_magnetism () =
 127   verify_ineq default_params 5 magnetism_ineq;;
 128
 129 let test_heart () =
 130   verify_ineq {default_params with eps = 1e-10} 5 heart_ineq;;
 131
 132
 133 let run_tests () =
 134   [test_schwefel(); test_rd(); test_caprasse(); test_lv();
 135    test_butcher(); test_magnetism(); test_heart()];;
 136
 137 let results () =
 138   map fst (run_tests());;
 139
 140
 141 results();;