formal_lp/old/formal_interval/test_taylor_arith.hl

   1 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
   2
   3 let reset_all () =
   4   Arith_cache.reset_stat();
   5   Arith_cache.reset_cache();
   6   Arith_float.reset_stat();
   7   Arith_float.reset_cache();;
   8
   9 (*************)
  10
  11 let pp = 4;;
  12
  13 let poly1 = expr_to_vector_fun `x1 * x2 * x3 + x2 * (x4 + x5) pow 3`;;
  14 let n = (get_dim o fst o dest_abs) poly1;;
  15 let xx = `[-- &3; -- &3; -- &3; -- &3; -- &3]` and
  16     zz = `[&2; &2; &2; &2; &2]`;;
  17
  18 let xx1 = convert_to_float_list n true xx and
  19     zz1 = convert_to_float_list n false zz;;
  20
  21 let eval_poly, tf, ti = mk_verification_functions pp poly1 false `&0`;;
  22 let dom_th = mk_m_center_domain n pp xx1 zz1;;
  23
  24 let th = eval_poly.taylor pp pp dom_th;;
  25
  26 (* 100: 0.524 *)
  27 reset_all();;
  28 test 100 (eval_poly.taylor pp pp) dom_th;;
  29 (* 100: 0.512 *)
  30 test 100 (eval_poly.taylor pp pp) dom_th;;
  31
  32 (************)
  33
  34 (* 100: 4.120 *)
  35 reset_all();;
  36 test 100 (eval_m_taylor_add n pp pp th) th;;
  37 (* 100: 4.184 *)
  38 test 100 (eval_m_taylor_add n pp pp th) th;;
  39
  40
  41 (*****************)
  42
  43 let p_lin = pp and p_second = pp and
  44     taylor1_th = th and taylor2_th = th;;
  45
  46 (****************)
  47
  48 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th;;
  49 let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th;;
  50 let f1_tm = (rand o concl) diff2_f1_th and
  51     f2_tm = (rand o concl) diff2_f2_th;;
  52 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th);;
  53 let ty = type_of y_tm;;
  54
  55 let x_var = mk_var ("x", ty) and
  56     y_var = mk_var ("y", ty) and
  57     w_var = mk_var ("w", ty) and
  58     f_var = mk_var ("f", type_of f1_tm) and
  59     g_var = mk_var ("g", type_of f2_tm) and
  60     domain_var = mk_var ("domain", type_of domain_tm);;
  61
  62 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
  63     _, bounds2_th, df2_th = m_lin_approx_components n lin2_th;;
  64
  65 let bounds_th = float_interval_add p_lin bounds1_th bounds2_th;;
  66 let bounds_tm = (rand o concl) bounds_th;;
  67
  68 let add_lemma0 = (INST[f1_tm, f_var; f2_tm, g_var; y_tm, x_var] o
  69                     INST_TYPE[n_type_array.(n), nty]) add_partial_lemma';;
  70
  71 let add th1 th2 =
  72   let add_th = float_interval_add p_lin th1 th2 in
  73   let int_tm = rand (concl add_th) and
  74       i_tm = (rand o rator o rator o lhand) (concl th1) in
  75   let th0 = INST[i_tm, i_var_num; int_tm, int_var] add_lemma0 in
  76     EQ_MP th0 add_th;;
  77
  78 let df_th = eval_all_n2 df1_th df2_th true add;;
  79 let d_bounds_list = (rand o rator o concl) df_th;;
  80
  81
  82 let dd1 = second_bounded_components n second1_th;;
  83 let dd2 = second_bounded_components n second2_th;;
  84
  85 let add_second_lemma0 = (INST[f1_tm, f_var; f2_tm, g_var] o
  86                            INST_TYPE[n_type_array.(n), nty]) add_second_lemma';;
  87
  88 let add_second_lemma1 = (INST[f1_tm, f_var; f2_tm, g_var] o
  89                            INST_TYPE[n_type_array.(n), nty]) add_second_lemma'';;
  90
  91
  92 let add_second2 th1 th2 =
  93   let i_tm = (rand o rator o concl) th1 in
  94   let th1, th2 = BETA_RULE th1, BETA_RULE th2 in
  95   let lemma = INST[i_tm, i_var_num] add_second_lemma0 in
  96   let add_second th1 th2 =
  97     let add_th = float_interval_add p_second th1 th2 in
  98     let int_tm = rand (concl add_th) and
  99         j_tm = (rand o rator o rator o rator o lhand) (concl th1) in
 100     let th0 = INST[j_tm, j_var_num; int_tm, int_var] lemma in
 101       EQ_MP th0 add_th in
 102   let add_th = eval_all_n2 th1 th2 true add_second in
 103   let list_tm = (rand o rator o concl) add_th in
 104   let lemma1 = INST[i_tm, i_var_num; list_tm, list_var_real_pair] add_second_lemma1 in
 105     EQ_MP lemma1 add_th;;
 106
 107
 108 let dd_th0 = eval_all_n2 dd1 dd2 false add_second2;;
 109 let dd_list = (rand o rator o concl) dd_th0;;
 110 let dd_th = GEN x_var (DISCH_ALL dd_th0);;
 111
 112 let th = (MY_PROVE_HYP dd_th o MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
 113             MY_PROVE_HYP bounds_th o MY_PROVE_HYP df_th o MY_PROVE_HYP domain_th o
 114             INST[f1_tm, f_var; f2_tm, g_var;
 115                  domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 116                  bounds_tm, bounds_var; d_bounds_list, d_bounds_list_var;
 117                  dd_list, dd_bounds_list_var] o
 118             INST_TYPE[n_type_array.(n), nty]) MK_M_TAYLOR_ADD';;
 119 let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var add_op_real;;
 120 m_taylor_interval_norm th eq_th;;
 121
 122
 123 (********************)
 124 reset_all();;
 125
 126 (* 0.028 *)
 127 test 100 (dest_m_taylor_thms n) taylor1_th;;
 128 (* 0.028 *)
 129 test 100 (dest_m_taylor_thms n) taylor2_th;;
 130
 131 (* 0.000 *)
 132 let f () =
 133   let a =(rand o concl) diff2_f1_th and
 134       b = (rand o concl) diff2_f2_th in
 135     a, b;;
 136 test 100 f ();;
 137
 138
 139 (* 0.000 *)
 140 test 100 dest_m_cell_domain (concl domain_th);;
 141 (* 0.000 *)
 142 test 100 type_of y_tm;;
 143
 144 (* 0.000 *)
 145 let f () =
 146   let x_var = mk_var ("x", ty) and
 147       y_var = mk_var ("y", ty) and
 148       w_var = mk_var ("w", ty) and
 149       f_var = mk_var ("f", type_of f1_tm) and
 150       g_var = mk_var ("g", type_of f2_tm) and
 151       domain_var = mk_var ("domain", type_of domain_tm) in
 152     x_var, y_var, w_var, f_var, g_var, domain_var;;
 153 test 100 f ();;
 154
 155 (* 0.052 *)
 156 let f () =
 157   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
 158       _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
 159     bounds1_th, df1_th, bounds2_th, df2_th;;
 160 test 100 f ();;
 161
 162 (* 0.012 *)
 163 test 100 (float_interval_add p_lin bounds1_th) bounds2_th;;
 164 (* 0.000 *)
 165 test 100 (rand o concl) bounds_th;;
 166
 167 (* 0.008 *)
 168 test 100 (INST[f1_tm, f_var; f2_tm, g_var; y_tm, x_var] o
 169    INST_TYPE[n_type_array.(n), nty]) add_partial_lemma';;
 170
 171 let add th1 th2 =
 172   let add_th = float_interval_add p_lin th1 th2 in
 173   let int_tm = rand (concl add_th) and
 174       i_tm = (rand o rator o rator o lhand) (concl th1) in
 175   let th0 = INST[i_tm, i_var_num; int_tm, int_var] add_lemma0 in
 176     EQ_MP th0 add_th;;
 177
 178 (* 0.688 *)
 179 test 100 (eval_all_n2 df1_th df2_th true) add;;
 180 (* 0.000 *)
 181 test 100 (rand o rator o concl) df_th;;
 182
 183 (* 0.044 *)
 184 test 100 (second_bounded_components n) second1_th;;
 185 (* 0.040 *)
 186 test 100 (second_bounded_components n) second2_th;;
 187
 188 (* 0.011 *)
 189 test 100 (INST[f1_tm, f_var; f2_tm, g_var] o
 190    INST_TYPE[n_type_array.(n), nty]) add_second_lemma';;
 191
 192 (* 0.020 *)
 193 test 100 (INST[f1_tm, f_var; f2_tm, g_var] o
 194    INST_TYPE[n_type_array.(n), nty]) add_second_lemma'';;
 195
 196
 197 let add_second2 th1 th2 =
 198   let i_tm = (rand o rator o concl) th1 in
 199   let th1, th2 = BETA_RULE th1, BETA_RULE th2 in
 200   let lemma = INST[i_tm, i_var_num] add_second_lemma0 in
 201   let add_second th1 th2 =
 202     let add_th = float_interval_add p_second th1 th2 in
 203     let int_tm = rand (concl add_th) and
 204         j_tm = (rand o rator o rator o rator o lhand) (concl th1) in
 205     let th0 = INST[j_tm, j_var_num; int_tm, int_var] lemma in
 206       EQ_MP th0 add_th in
 207   let add_th = eval_all_n2 th1 th2 true add_second in
 208   let list_tm = (rand o rator o concl) add_th in
 209   let lemma1 = INST[i_tm, i_var_num; list_tm, list_var_real_pair] add_second_lemma1 in
 210     EQ_MP lemma1 add_th;;
 211
 212
 213 (* 3.016 *)
 214 test 100 (eval_all_n2 dd1 dd2 false) add_second2;;
 215 (* 0.000 *)
 216 test 100 (rand o rator o concl) dd_th0;;
 217 (* 0.004 *)
 218 test 100 (GEN x_var o DISCH_ALL) dd_th0;;
 219
 220 (* 0.096 *)
 221 test 100 (MY_PROVE_HYP dd_th o MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
 222             MY_PROVE_HYP bounds_th o MY_PROVE_HYP df_th o MY_PROVE_HYP domain_th o
 223             INST[f1_tm, f_var; f2_tm, g_var;
 224                  domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 225                  bounds_tm, bounds_var; d_bounds_list, d_bounds_list_var;
 226                  dd_list, dd_bounds_list_var] o
 227             INST_TYPE[n_type_array.(n), nty]) MK_M_TAYLOR_ADD';;
 228 (* 0.000 *)
 229 test 100 (binary_beta_gen_eq f1_tm f2_tm x_var) add_op_real;;
 230 (* 0.004 *)
 231 test 100 (m_taylor_interval_norm th) eq_th;;
 232
 233
 234 (***********************)
 235
 236 test 100 (eval_all_n2 df1_th df2_th true) add;;
 237
 238 (* Constructs all_n n (map2 s list1 list2) *)
 239 let all_n1_th = df1_th and all_n2_th = df2_th and beta_flag = true and s = add;;
 240
 241 (***)
 242
 243 let ths1', suc_ths = all_n_components all_n1_th;;
 244 let ths2', _ = all_n_components all_n2_th;;
 245 let ths1, ths2 =
 246   if beta_flag then map BETA_RULE ths1', map BETA_RULE ths2' else ths1', ths2';;
 247
 248 let ths1, ths2, suc_ths = List.rev ths1, List.rev ths2, List.rev suc_ths;;
 249 let ths = map2 s ths1 ths2;;
 250 build_all_n ths suc_ths;;
 251
 252
 253 (***)
 254
 255 (* 0.040 *)
 256 test 100 all_n_components all_n1_th;;
 257 (* 0.052 *)
 258 test 100 all_n_components all_n2_th;;
 259 (* 0.244 *)
 260 test 100 (map BETA_RULE) ths1';;
 261 (* 0.240 *)
 262 test 100 (map BETA_RULE) ths2';;
 263
 264 hd ths1';;
 265 BETA_RULE (hd ths1');;
 266
 267 (* 0.000 *)
 268 let f () =
 269   let ths1, ths2, suc_ths = List.rev ths1, List.rev ths2, List.rev suc_ths in
 270     ths1, ths2, suc_ths;;
 271 test 100 f ();;
 272
 273 (* 0.052 *)
 274 test 100 (map2 s ths1) ths2;;
 275 (* 0.056 *)
 276 test 100 (build_all_n ths) suc_ths;;
 277
 278
 279 (*************)
 280
 281 let th0 = hd ths1';;
 282 BETA_RULE th0;;
 283
 284 (* 0.436 *)
 285 test 1000 BETA_RULE th0;;
 286
 287
 288 let MY_BETA_RULE th =
 289   let rec beta tm =
 290     let op, arg = dest_comb tm in
 291       if is_comb op then
 292         let op_th = AP_THM (beta op) arg in
 293         let beta_th = BETA_CONV (rand (concl op_th)) in
 294           TRANS op_th beta_th
 295       else
 296         BETA_CONV tm in
 297     EQ_MP (beta (concl th)) th;;
 298
 299
 300 let MY_BETA_RULE2 th0 =
 301   let c = concl th0 in
 302   let lhs, rhs = dest_comb c in
 303
 304   let th1 = BETA_CONV lhs in
 305   let th2 = AP_THM th1 rhs in
 306   let th3 = BETA_CONV (rand (concl th2)) in
 307     EQ_MP (TRANS th2 th3) th0;;
 308
 309 MY_BETA_RULE2 th0;;
 310 (* 0.036 *)
 311 test 1000 MY_BETA_RULE2 th0;;
 312
 313