formal_ineqs/verifier/m_verifier_build.hl

   1 (* =========================================================== *)
   2 (* Auxiliary formal verification functions                     *)
   3 (* Author: Alexey Solovyev                                     *)
   4 (* Date: 2012-10-27                                            *)
   5 (* =========================================================== *)
   6
   7 needs "arith/eval_interval.hl";;
   8 needs "arith/more_float.hl";;
   9 needs "taylor/m_taylor.hl";;
  10 needs "verifier/interval_m/taylor.ml";;
  11 needs "informal/informal_m_verifier.hl";;
  12 needs "verifier_options.hl";;
  13 needs "misc/vars.hl";;
  14
  15 module M_verifier_build = struct
  16
  17 open More_float;;
  18 open Eval_interval;;
  19 open M_taylor;;
  20
  21 open Interval_types;;
  22 open Interval;;
  23 open Line_interval;;
  24 open Taylor;;
  25
  26 open Misc_vars;;
  27 open Verifier_options;;
  28
  29 type verification_funs =
  30 {
  31   (* p_lin -> p_second -> domain_th -> taylor_th *)
  32   taylor : int -> int -> thm -> thm;
  33   (* pp -> lo -> hi -> interval_th *)
  34   f : int -> term -> term -> thm;
  35   (* i -> pp -> lo -> hi -> interval_th *)
  36   df : int -> int -> term -> term -> thm;
  37   (* i -> j -> pp -> lo -> hi -> interval_th *)
  38   ddf : int -> int -> int -> term -> term -> thm;
  39   (* lo -> hi -> diff2_th *)
  40   diff2_f : term -> term -> thm;
  41 };;
  42
  43 (****************************)
  44 (* Interval polynomial functions for the native OCaml arithmetic *)
  45
  46 type int_poly_fun =
  47   | F_int_var of int
  48   | F_int_const of interval
  49   | F_int_pow of int * int_poly_fun
  50   | F_int_neg of int_poly_fun
  51   | F_int_add of int_poly_fun * int_poly_fun
  52   | F_int_sub of int_poly_fun * int_poly_fun
  53   | F_int_mul of int_poly_fun * int_poly_fun;;
  54
  55
  56 let ipow = Arith_misc.gen_pow imul Interval.one;;
  57
  58
  59 let eval_int_poly_fun i_fun =
  60   fun x ->
  61     let rec eval_rec f =
  62       match f with
  63         | F_int_var i -> List.nth x (i - 1)
  64         | F_int_const int -> int
  65         | F_int_neg f1 -> ineg (eval_rec f1)
  66         | F_int_pow (n,f1) -> ipow n (eval_rec f1)
  67         | F_int_add (f1,f2) -> iadd (eval_rec f1) (eval_rec f2)
  68         | F_int_sub (f1,f2) -> isub (eval_rec f1) (eval_rec f2)
  69         | F_int_mul (f1,f2) -> imul (eval_rec f1) (eval_rec f2) in
  70       eval_rec i_fun;;
  71
  72 (****************************)
  73 (* Automatic conversion of formal interval polynomials into functions (polynomials) *)
  74 (* TODO: take Int_ref into account *)
  75
  76 let rec build_poly_fun i_fun =
  77   match i_fun with
  78     | Int_var tm ->
  79         (try F_int_var (dest_small_numeral (rand tm))
  80          with Failure _ ->
  81            let name = (fst o dest_var) tm in
  82              F_int_var (int_of_string (String.sub name 1 (String.length name - 1))))
  83     | Int_const th ->
  84         let f1, f2 = (dest_pair o rand o concl) th in
  85         let int = mk_interval (float_of_float_tm f1, float_of_float_tm f2) in
  86           F_int_const int
  87     | Int_pow (n, f) -> F_int_pow (n, build_poly_fun f)
  88     | Int_unary (op, f) ->
  89         let f' = build_poly_fun f in
  90           if op = neg_op_real then F_int_neg f' else failwith ("Unsupported operator: "^string_of_term op)
  91     | Int_binary (op, f1, f2) ->
  92         let f1', f2' = build_poly_fun f1, build_poly_fun f2 in
  93           if op = add_op_real then F_int_add (f1',f2')
  94           else if op = sub_op_real then F_int_sub (f1',f2')
  95           else if op = mul_op_real then F_int_mul (f1',f2')
  96           else failwith ("Unsupported operator: "^string_of_term op)
  97     | _ -> failwith "Unsupported function";;
  98
  99
 100 let build_polyL pp lin_th =
 101   let funs = map (fst o dest_interval_arith) ((striplist dest_conj o rand o concl) lin_th) in
 102   let i_funs = map (eval_constants pp o build_interval_fun) funs in
 103   let fs = map build_poly_fun i_funs @ (replicate (F_int_const zero) (8 - length funs + 1)) in
 104   let eval_fs = map eval_int_poly_fun fs in
 105   let f, df = hd eval_fs, tl eval_fs in
 106     (fun i x z ->
 107       let vars = map2 (curry mk_interval) x z in
 108         if i = 0 then f vars else (List.nth df (i - 1)) vars),
 109     (fun x ->
 110       let vars = map (fun x -> mk_interval (x,x)) x in
 111         mk_line (f vars, map (fun df -> df vars) df));;
 112
 113 let build_polyL0 pp poly_tm =
 114   let lin_th = gen_lin_approx_poly_thm0 poly_tm in
 115     build_polyL pp lin_th;;
 116
 117 let build_polyDD pp second_th =
 118   let poly_tm = (lhand o rator o lhand o concl) second_th in
 119   let n = (get_dim o fst o dest_abs) poly_tm in
 120   let ns = 1--n in
 121   let funs = (striplist dest_conj o rand o snd o dest_forall o rand o concl) second_th in
 122   let i_funs = map (eval_constants pp o build_interval_fun o fst o dest_interval_arith) funs in
 123   let fs0 = map build_poly_fun i_funs in
 124   let pad1 = replicate zero (8 - n) and
 125       pad2 = replicate zero 8 in
 126   let pad3 = replicate pad2 (8 - n) in
 127   let get_el dd i j =
 128     let i', j' = if j <= i then i, j else j, i in
 129     let index = (i' - 1) * i' / 2 + (j' - 1) in
 130       List.nth dd index in
 131   let eval_fs = map eval_int_poly_fun fs0 in
 132     fun x z ->
 133       let ints = map2 (curry mk_interval) x z in
 134       let vals = map (fun f -> f ints) eval_fs in
 135         map (fun i -> map (fun j -> get_el vals i j) ns @ pad1) ns @ pad3;;
 136
 137
 138 let build_polyDD0 pp poly_tm =
 139   let second_th = gen_second_bounded_poly_thm0 poly_tm in
 140     build_polyDD pp second_th;;
 141
 142
 143 (******)
 144
 145 let build_poly_taylor pp lin_th second_th =
 146   let f_df, lin = build_polyL pp lin_th and
 147       dd = build_polyDD pp second_th in
 148     Prim_a (make_primitiveA (f_df, lin, dd));;
 149
 150 let build_poly_taylor0 pp poly_tm =
 151   build_poly_taylor pp (gen_lin_approx_poly_thm0 poly_tm) (gen_second_bounded_poly_thm0 poly_tm);;
 152
 153
 154 (**********************************)
 155 (* mk_verification_functions *)
 156
 157 let mk_verification_functions_poly pp0 poly_tm =
 158   let x_tm, body_tm = dest_abs poly_tm in
 159   let new_f = poly_tm in
 160   let n = get_dim x_tm in
 161
 162   let _ = !info_print_level = 0 or (report0 (sprintf "Computing partial derivatives (%d)..." n); true) in
 163   let partials = map (fun i ->
 164                         let _ = !info_print_level = 0 or (report0 (sprintf " %d" i); true) in
 165                           gen_partial_poly i new_f) (1--n) in
 166   let get_partial i eq_th =
 167     let partial_i = gen_partial_poly i (rand (concl eq_th)) in
 168     let pi = (rator o lhand o concl) partial_i in
 169       REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in
 170   let partials2 = map (fun j ->
 171                          let th = List.nth partials (j - 1) in
 172                            map (fun i ->
 173                                   let _ = !info_print_level = 0 or (report0 (sprintf " %d,%d" j i); true) in
 174                                     get_partial i th) (1--j)) (1--n) in
 175
 176   let _ = !info_print_level = 0 or (report0 " done\n"; true) in
 177
 178   let diff_th = gen_diff_poly new_f in
 179   let lin_th = gen_lin_approx_poly_thm new_f diff_th partials in
 180   let diff2_th = gen_diff2c_domain_poly new_f in
 181   let second_th = gen_second_bounded_poly_thm new_f partials2 in
 182
 183   let replace_numeral i th =
 184     let num_eq = (REWRITE_RULE[Arith_hash.NUM_THM] o Arith_nat.NUMERAL_TO_NUM_CONV)
 185       (mk_small_numeral i) in
 186       GEN_REWRITE_RULE (LAND_CONV o RATOR_CONV o DEPTH_CONV) [num_eq] th in
 187
 188   let eval0 = mk_eval_function pp0 new_f in
 189   let eval1 = map (fun i ->
 190                      let d_th = List.nth partials (i - 1) in
 191                      let eq_th = replace_numeral i d_th in
 192                        mk_eval_function_eq pp0 eq_th) (1--n) in
 193
 194   let eval2 = map (fun i ->
 195                      map (fun j ->
 196                             let d2_th = List.nth (List.nth partials2 (i - 1)) (j - 1) in
 197                             let eq_th' = replace_numeral i d2_th in
 198                             let eq_th = replace_numeral j eq_th' in
 199                               mk_eval_function_eq pp0 eq_th) (1--i)) (1--n) in
 200
 201   let diff2_f = eval_diff2_poly diff2_th in
 202   let eval_f = eval_m_taylor pp0 diff2_th lin_th second_th in
 203   let taylor_f = build_poly_taylor pp0 lin_th second_th in
 204     {taylor = eval_f;
 205      f = eval0;
 206      df = (fun i -> List.nth eval1 (i - 1));
 207      ddf = (fun i j -> List.nth (List.nth eval2 (j - 1)) (i - 1));
 208      diff2_f = diff2_f;
 209     }, taylor_f, Informal_verifier.mk_verification_functions_poly pp0 new_f partials partials2;;
 210
 211
 212
 213
 214 end;;