formal_lp/more_arith/prove_lp.hl

   1 needs "../formal_lp/more_arith/lin_f.hl";;
   2 needs "../formal_lp/more_arith/arith_int.hl";;
   3
   4
   5 module Prove_lp = struct
   6
   7 open Linear_function;;
   8 open Arith_misc;;
   9 open Arith_nat;;
  10 open Arith_int;;
  11 open Misc_vars;;
  12
  13
  14
  15 (* Special versions of the above theorems (for using with INST) *)
  16
  17
  18 let NUM_ZERO = prove(mk_eq(mk_comb(amp_op_real, mk_comb(Arith_hash.num_const, zero_const)), `&0`),
  19                      REWRITE_TAC[Arith_hash.NUM_THM; NUMERAL]);;
  20
  21 let LIN_F_SUM_HD',
  22   LIN_F_SUM_HD_ZERO',
  23   LIN_F_SUM_EMPTY1', LIN_F_SUM_EMPTY2',
  24   LIN_F_SUM_MOVE1', LIN_F_SUM_MOVE2',
  25   LIN_F_ADD_SINGLE' =
  26      UNDISCH_ALL (SPEC_ALL LIN_F_SUM_HD),
  27      UNDISCH_ALL (SPEC_ALL (ONCE_REWRITE_RULE[GSYM NUM_ZERO] LIN_F_SUM_HD_ZERO)),
  28      SPEC_ALL LIN_F_SUM_EMPTY1, SPEC_ALL LIN_F_SUM_EMPTY2,
  29      SPEC_ALL LIN_F_SUM_MOVE1, SPEC_ALL LIN_F_SUM_MOVE2,
  30      SPEC_ALL LIN_F_ADD_SINGLE;;
  31
  32 let LIN_F_MUL_HD', LIN_F_MUL_EMPTY' =
  33   UNDISCH_ALL (SPEC_ALL LIN_F_MUL_HD), SPEC_ALL LIN_F_MUL_EMPTY;;
  34
  35 let LIN_F_ADD_SING_RCANCEL', LIN_F_ADD_SING_LCANCEL' =
  36   SPEC_ALL LIN_F_ADD_SING_RCANCEL, SPEC_ALL LIN_F_ADD_SING_LCANCEL;;
  37
  38
  39
  40 (***********************************************)
  41
  42
  43 (* Constants *)
  44
  45 let a1_var_real = `a1:real` and
  46     a2_var_real = `a2:real` and
  47     b1_var_real = `b1:real` and
  48     b2_var_real = `b2:real` and
  49     c1_var_real = `c1:real` and
  50     c2_var_real = `c2:real` and
  51     h_var = `h:real#real` and
  52     r_var = `r:(real#real)list` and
  53     x_var = `x:(real#real)list` and
  54     y_var = `y:(real#real)list` and
  55     t_var = `t:(real#real)list` and
  56     x_var_real = `x:real` and
  57     c1_var = `c1:real` and
  58     c2_var = `c2:real` and
  59     c_var = `c:real` and
  60     v_var = `v:real` and
  61     t1_var = `t1:(real#real)list` and
  62     t2_var = `t2:(real#real)list` and
  63     empty_const = `[]:(real)list`;;
  64
  65 let ge_op_real = `(>=):real->real->bool`;;
  66
  67 let cons_const = `CONS:(real#real)->(real#real)list->(real#real)list` and
  68     empty_const = `[]:(real)list`;;
  69
  70
  71 (* HACK: for some reason Big_int.big_int_of_int64 is not defined *)
  72 let num_of_int64 n =
  73   let big = Big_int.big_int_of_string (Int64.to_string n) in
  74     Num.num_of_big_int big;;
  75
  76 (* Term constructors *)
  77 let cons h t = mk_comb (mk_comb (cons_const, h), t);;
  78 let negate tm = mk_comb (neg_op_real, tm);;
  79 let mk_real_int n = mk_comb(amp_op_real, mk_numeral_array n);;
  80 let mk_real_int64 n = mk_comb(amp_op_real, mk_numeral_array (num_of_int64 n));;
  81 let mk_linear cs vars =
  82   let mk_term (c, var) = mk_binop mul_op_real c (mk_var (var, real_ty)) in
  83     list_mk_binop add_op_real (map mk_term (zip cs vars));;
  84
  85 let mk_le_ineq lhs rhs = mk_binop le_op_real lhs rhs;;
  86 let mk_eq_ineq lhs rhs = mk_eq (lhs, rhs);;
  87 let mk_ge_ineq lhs rhs = mk_binop ge_op_real lhs rhs;;
  88
  89
  90
  91 (************************************************)
  92
  93 (* Computes (lin_f x + lin_f y) with REAL_BITS_ADD_CONV *)
  94 let lin_f_add_conv tm =
  95   let rec lin_f_add_conv2 x y =
  96     if (is_comb y) then
  97       if (is_comb x) then
  98         let hx = rand (rator x) in
  99         let hy = rand (rator y) in
 100         let c1, v1 = dest_pair hx in
 101         let c2, v2 = dest_pair hy in
 102
 103           if v1 = v2 then
 104             let tx, ty = rand x, rand y in
 105             let c_thm = my_real_int_add_conv (mk_binop add_op_real c1 c2) in
 106             let c = rand (concl c_thm) in
 107               if (rand(rand c) = zero_const) then
 108                 let th0 = INST [v1, v_var; c1, c1_var; tx, t1_var; c2, c2_var; ty, t2_var]
 109                   LIN_F_SUM_HD_ZERO' in
 110                   TRANS (MY_PROVE_HYP c_thm th0) (lin_f_add_conv2 tx ty)
 111               else
 112                 let th0 = INST[v1, v_var; c1, c1_var; tx, t1_var; c2, c2_var; ty, t2_var; c, c_var]
 113                   LIN_F_SUM_HD' in
 114                 let ltm = rator (rand(concl th0)) in
 115                 let th1 = lin_f_add_conv2 tx ty in
 116                 let th2 = TRANS (MY_PROVE_HYP c_thm th0) (AP_TERM ltm th1) in
 117                 let th3 = INST[mk_pair (c, v1), h_var; rand(rand(concl th1)), t_var] LIN_F_ADD_SINGLE' in
 118                   TRANS th2 th3
 119           else
 120             if (v1 < v2) then
 121               let tx = rand x in
 122               let th0 = INST[hx, h_var; tx, t_var; y, x_var] LIN_F_SUM_MOVE1' in
 123               let ltm = rator (rand(concl th0)) in
 124               let th1 = lin_f_add_conv2 tx y in
 125               let th2 = TRANS th0 (AP_TERM ltm th1) in
 126               let th3 = INST[hx, h_var; rand(rand(concl th1)), t_var] LIN_F_ADD_SINGLE' in
 127                 TRANS th2 th3
 128             else
 129               let ty = rand y in
 130               let th0 = INST[hy, h_var; ty, t_var; x, x_var] LIN_F_SUM_MOVE2' in
 131               let ltm = rator (rand(concl th0)) in
 132               let th1 = lin_f_add_conv2 x ty in
 133               let th2 = TRANS th0 (AP_TERM ltm th1) in
 134               let th3 = INST[hy, h_var; rand(rand(concl th1)), t_var] LIN_F_ADD_SINGLE' in
 135                 TRANS th2 th3
 136       else
 137         (* x = [] *)
 138         INST[y, x_var] LIN_F_SUM_EMPTY1'
 139     else
 140       (* y = [] *)
 141       INST[x, x_var] LIN_F_SUM_EMPTY2' in
 142
 143   let larg, rarg = dest_comb tm in
 144   let larg = rand larg in
 145     lin_f_add_conv2 (rand larg) (rand rarg);;
 146
 147
 148
 149 (*********************)
 150 (* lin_f conversions *)
 151 (*********************)
 152
 153
 154 (* Transforms a sum in the form `a * x + b * y + c * z` into `lin_f [(c,z); (b,y); (a,x)]` *)
 155 let LIN_F_RAW_CONV = ONCE_REWRITE_CONV[TO_LIN_F0] THENC REWRITE_CONV[TO_LIN_F];;
 156
 157 let LIN_F_ADD_CONV = lin_f_add_conv;;
 158
 159 (* Transforms a sum into `lin_f` and sorts the terms *)
 160 let LIN_F_CONV = (REWRITE_CONV[TO_LIN_F1] THENC (DEPTH_CONV LIN_F_ADD_CONV));;
 161
 162
 163 (* Computes `v * lin_f y` *)
 164
 165 let rec LIN_F_MUL_CONV tm =
 166   let x, f = dest_binop mul_op_real tm in
 167   let list = rand f in
 168     if (is_comb list) then
 169       let cons_h, t = dest_comb list in
 170       let h = rand cons_h in
 171       let c, v = dest_pair h in
 172
 173       let product = my_real_int_mul_conv (mk_binop mul_op_real x c) in
 174       let c1 = rand(concl product) in
 175       let th = INST[x, x_var_real; c, c_var; v, v_var; t, t_var; c1, c1_var] LIN_F_MUL_HD' in
 176       let th1 = MY_PROVE_HYP product th in
 177       let lplus, tm = dest_comb(rand(concl th1)) in
 178       let th2 = LIN_F_MUL_CONV tm in
 179       let h = mk_pair (c1, v) in
 180       let t = rand(rand(concl th2)) in
 181       let th3 = TRANS th1 (AP_TERM lplus th2) in
 182       let th4 = INST[h, h_var; t, t_var] LIN_F_ADD_SINGLE' in
 183         TRANS th3 th4
 184     else
 185       INST[x, x_var_real] LIN_F_MUL_EMPTY';;
 186
 187
 188 (* Conversion without numerical multiplication *)
 189 let LIN_F_MUL_RAW_CONV = ONCE_REWRITE_CONV[LIN_F_MUL] THENC REWRITE_CONV[MAP];;
 190
 191
 192
 193 (************************************************)
 194
 195
 196 (* Creates an inequality in the correct form *)
 197 let REAL_POS' = SPEC_ALL REAL_POS;;
 198 let REAL_LE_LMUL' = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] (SPEC_ALL REAL_LE_LMUL));;
 199 let TO_LIN_F1' = SPEC_ALL TO_LIN_F1;;
 200
 201 let rec lin_f_conv tm =
 202   if is_binary "real_add" tm then
 203     let ltm, rtm = dest_binary "real_add" tm in
 204     let a_tm, x_tm = dest_binary "real_mul" ltm in
 205     let th1 = INST[a_tm, a_var_real; x_tm, x_var_real] TO_LIN_F1' in
 206     let th2 = lin_f_conv rtm in
 207     let eq_th = MK_COMB (AP_TERM add_op_real th1, th2) in
 208     let eq_th2 = lin_f_add_conv (rand (concl eq_th)) in
 209       TRANS eq_th eq_th2
 210   else
 211     let a_tm, x_tm = dest_binary "real_mul" tm in
 212       INST[a_tm, a_var_real; x_tm, x_var_real] TO_LIN_F1';;
 213
 214
 215 let transform_le_ineq (ineq, m) =
 216   let lhs, rhs = dest_binop le_op_real (concl ineq) in
 217   let lhs_f_th = lin_f_conv lhs in
 218   let original_th = EQ_MP (AP_THM (AP_TERM le_op_real lhs_f_th) rhs) ineq in
 219   let lhs = rand(concl lhs_f_th) in
 220   let pos_th = INST[rand m, n_var_num] REAL_POS' in
 221   let th0 = INST[m, x_var_real; lhs, y_var_real; rhs, z_var_real] REAL_LE_LMUL' in
 222   let th1 = MY_PROVE_HYP pos_th th0 in
 223   let th2 = MY_PROVE_HYP original_th th1 in
 224   let lhs, rhs = dest_binop le_op_real (concl th2) in
 225   let lhs_th = LIN_F_MUL_CONV lhs in
 226   let rhs_th = my_real_int_mul_conv rhs in
 227   let th3 = MK_COMB(AP_TERM le_op_real lhs_th, rhs_th) in
 228     EQ_MP th3 th2;;
 229
 230
 231 let transform_le_ineq_tm (ineq, m) =
 232   let lhs, rhs = dest_binop le_op_real ineq in
 233   let lhs_f_th = lin_f_conv lhs in
 234   let original_th = EQ_MP (AP_THM (AP_TERM le_op_real lhs_f_th) rhs) (ASSUME ineq) in
 235   let lhs = rand(concl lhs_f_th) in
 236   let pos_th = INST[rand m, n_var_num] REAL_POS' in
 237   let th0 = INST[m, x_var_real; lhs, y_var_real; rhs, z_var_real] REAL_LE_LMUL' in
 238   let th1 = MY_PROVE_HYP pos_th th0 in
 239   let th2 = MY_PROVE_HYP original_th th1 in
 240   let lhs, rhs = dest_binop le_op_real (concl th2) in
 241   let lhs_th = LIN_F_MUL_CONV lhs in
 242   let rhs_th = my_real_int_mul_conv rhs in
 243   let th3 = MK_COMB(AP_TERM le_op_real lhs_th, rhs_th) in
 244     EQ_MP th3 th2;;
 245
 246
 247
 248 (* Computes the sum of two inequalities *)
 249 let REAL_LE_ADD2' = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] (SPEC_ALL REAL_LE_ADD2));;
 250
 251 (* Computes the sum of two inequalities (with LIN_F_ADD_CONV and REAL_BITS_ADD_CONV) *)
 252 let add_step' ineq1 ineq2 =
 253   let lhs1, rhs1 = dest_binop le_op_real (concl ineq1) in
 254   let lhs2, rhs2 = dest_binop le_op_real (concl ineq2) in
 255   let th0 = INST [lhs1, w_var_real; rhs1, x_var_real; lhs2, y_var_real; rhs2, z_var_real]
 256     REAL_LE_ADD2' in
 257   let th1 = MY_PROVE_HYP ineq2 (MY_PROVE_HYP ineq1 th0) in
 258   let lhs, rhs = dest_binop le_op_real (concl th1) in
 259   let lhs_th = LIN_F_ADD_CONV lhs in
 260   let rhs_th = my_real_int_add_conv rhs in
 261     EQ_MP (MK_COMB(AP_TERM le_op_real lhs_th, rhs_th)) th1;;
 262
 263
 264 (* Computes the sum of lin_f[--c, x;...] and c * x *)
 265 let add_cancel_step ineq var_ineq =
 266   let lhs1, rhs1 = dest_binop le_op_real (concl var_ineq) in
 267   let lhs2, rhs2 = dest_binop le_op_real (concl ineq) in
 268   let th0 = INST[lhs1, w_var_real; rhs1, x_var_real; lhs2, y_var_real; rhs2, z_var_real]
 269     REAL_LE_ADD2' in
 270   let th1 = MY_PROVE_HYP ineq (MY_PROVE_HYP var_ineq th0) in
 271   let ctm, vtm = dest_binop mul_op_real lhs1 in
 272   let ttm = rand(rand lhs2) in
 273     if (rator ctm = neg_op_real) then
 274       let lhs_th = INST[rand ctm, c_var; vtm, v_var; ttm, t_var] LIN_F_ADD_SING_LCANCEL' in
 275       let rhs_th = my_real_int_add_conv (rand(concl th1)) in
 276         EQ_MP (MK_COMB(AP_TERM le_op_real lhs_th, rhs_th)) th1
 277     else
 278       let lhs_th = INST[ctm, c_var; vtm, v_var; ttm, t_var] LIN_F_ADD_SING_RCANCEL' in
 279       let rhs_th = my_real_int_add_conv (rand(concl th1)) in
 280         EQ_MP (MK_COMB(AP_TERM le_op_real lhs_th, rhs_th)) th1;;
 281
 282
 283
 284 let zero_const_real = `&0`;;
 285
 286 (* Multiplies a linear inequality by a rational positive constant *)
 287 let mul_rat_step ineq c =
 288   let pos_thm = REAL_ARITH (mk_le_ineq zero_const_real c) in
 289   let hyp = CONJ pos_thm ineq in
 290   let th0 = MATCH_MP REAL_LE_LMUL hyp in
 291   let lhs, rhs = dest_binop le_op_real (concl th0) in
 292   let lhs_th = (LIN_F_MUL_RAW_CONV THENC DEPTH_CONV REAL_RAT_MUL_CONV) lhs in
 293   let rhs_th = REAL_RAT_MUL_CONV rhs in
 294     EQ_MP (MK_COMB (AP_TERM le_op_real lhs_th, rhs_th)) th0;;
 295
 296
 297
 298 (* Multiplies a linear inequality in the form lin_f x <= y by
 299    a positive integer c *)
 300 let mul_step ineq c =
 301   let lhs, rhs = dest_binop le_op_real (concl ineq) in
 302   let pos_th = INST[rand c, n_var_num] REAL_POS' in
 303   let th0 = INST[c, x_var_real; lhs, y_var_real; rhs, z_var_real] REAL_LE_LMUL' in
 304   let th1 = MY_PROVE_HYP pos_th th0 in
 305   let th2 = MY_PROVE_HYP ineq th1 in
 306   let lhs, rhs = dest_binop le_op_real (concl th2) in
 307   let lhs_th = LIN_F_MUL_CONV lhs in
 308   let rhs_th = my_real_int_mul_conv rhs in
 309   let th3 = MK_COMB(AP_TERM le_op_real lhs_th, rhs_th) in
 310     EQ_MP th3 th2;;
 311
 312
 313
 314 (* Transformations for variables *)
 315
 316 let VAR_MUL_THM = prove(`!x c1 c2 a b v. &0 <= x /\ x * c1 = a /\ x * c2 = b /\ c1 * v <= c2
 317     ==> a * v <= b`,
 318    REPEAT STRIP_TAC THEN
 319      UNDISCH_TAC `x * c1 = a:real` THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 320      UNDISCH_TAC `x * c2 = b:real` THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 321      REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 322      MATCH_MP_TAC REAL_LE_LMUL THEN
 323      ASM_REWRITE_TAC[]);;
 324
 325
 326 let VAR_MUL_THM' = (UNDISCH_ALL o SPEC_ALL o (REWRITE_RULE[GSYM IMP_IMP])) VAR_MUL_THM;;
 327
 328 let VAR_ADD_THM = prove(`!x a1 b1 a2 b2 c1 c2. a1 * x <= b1 /\ a2 * x <= b2 /\
 329                           a1 + a2 = c1 /\ b1 + b2 = c2 ==> c1 * x <= c2`,
 330                         REPEAT STRIP_TAC THEN
 331                           EXPAND_TAC "c1" THEN EXPAND_TAC "c2" THEN
 332                           REWRITE_TAC[REAL_ADD_RDISTRIB] THEN
 333                           MATCH_MP_TAC REAL_LE_ADD2 THEN
 334                           ASM_REWRITE_TAC[]);;
 335
 336 let VAR_ADD_THM' = (UNDISCH_ALL o SPEC_ALL o (REWRITE_RULE[GSYM IMP_IMP])) VAR_ADD_THM;;
 337
 338
 339 (* Multiplies c1 * x <= c2 by m *)
 340 let var1_le_transform (var_ineq, m) =
 341   let lhs, c2tm = dest_binop le_op_real (var_ineq) in
 342   let pos_th = INST[rand m, n_var_num] REAL_POS' in
 343   let c1tm, xtm = dest_binop mul_op_real lhs in
 344   let c1_th = my_real_int_mul_conv (mk_binop mul_op_real m c1tm) in
 345   let c2_th = my_real_int_mul_conv (mk_binop mul_op_real m c2tm) in
 346   let th = INST[m, x_var_real; c1tm, c1_var; c2tm, c2_var; xtm, v_var;
 347               rand(concl c1_th), a_var_real; rand(concl c2_th), b_var_real]
 348     VAR_MUL_THM' in
 349     MY_PROVE_HYP pos_th (MY_PROVE_HYP (ASSUME var_ineq) (MY_PROVE_HYP c1_th (MY_PROVE_HYP c2_th th)));;
 350
 351
 352 (* Sums two inequalities *)
 353 let add_le_ineqs ineq1 ineq2 =
 354   let lhs1, b1tm = dest_binop le_op_real (concl ineq1) in
 355   let lhs2, b2tm = dest_binop le_op_real (concl ineq2) in
 356   let a1tm, xtm = dest_binop mul_op_real lhs1 in
 357   let a2tm = rand(rator lhs2) in
 358   let b_th = my_real_int_add_conv (mk_binop add_op_real b1tm b2tm) in
 359   let a_th = my_real_int_add_conv (mk_binop add_op_real a1tm a2tm) in
 360   let th0 = INST[a1tm, a1_var_real; a2tm, a2_var_real;
 361                  b1tm, b1_var_real; b2tm, b2_var_real;
 362                  rand(concl a_th), c1_var_real; rand(concl b_th), c2_var_real;
 363                  xtm, x_var_real] VAR_ADD_THM' in
 364     MY_PROVE_HYP ineq2 (MY_PROVE_HYP ineq1 (MY_PROVE_HYP b_th (MY_PROVE_HYP a_th th0)));;
 365
 366
 367
 368 (* Multiplies the corresponding inequalities and finds the sum of results *)
 369 let var2_le_transform (var_ineq1,m1) (var_ineq2,m2) =
 370   let ineq1 = var1_le_transform (var_ineq1, m1) and
 371       ineq2 = var1_le_transform (var_ineq2, m2) in
 372   let lhs1, b1tm = dest_binop le_op_real (concl ineq1) in
 373   let lhs2, b2tm = dest_binop le_op_real (concl ineq2) in
 374   let a1tm, xtm = dest_binop mul_op_real lhs1 in
 375   let a2tm = rand(rator lhs2) in
 376   let b_th = my_real_int_add_conv (mk_binop add_op_real b1tm b2tm) in
 377   let a_th = my_real_int_add_conv (mk_binop add_op_real a1tm a2tm) in
 378   let th0 = INST[a1tm, a1_var_real; a2tm, a2_var_real;
 379                  b1tm, b1_var_real; b2tm, b2_var_real;
 380                  rand(concl a_th), c1_var_real; rand(concl b_th), c2_var_real;
 381                  xtm, x_var_real] VAR_ADD_THM' in
 382     MY_PROVE_HYP ineq2 (MY_PROVE_HYP ineq1 (MY_PROVE_HYP b_th (MY_PROVE_HYP a_th th0)));;
 383
 384
 385
 386
 387
 388 (* The main function *)
 389 (* Example: prove_lp ineqs var_ineqs target_vars `&12` (Int 100000) *)
 390 (* ineq - inequalities obtained from constraints with multipliers *)
 391 (* var_ineqs - bounds for variables as inequalities in the correct form *)
 392 (* target_vars - bounds and multipliers for variables in the objective function *)
 393 (* bound - a bound for the objective function which is proved *)
 394 (* m - a precision constant *)
 395
 396
 397 let LIN_F_EMPTY_LE_0 = prove(`lin_f [] <= &0`, REWRITE_TAC[LIN_F_EMPTY; REAL_LE_REFL]);;
 398 let dummy = REWRITE_RULE[GSYM NUM_ZERO] LIN_F_EMPTY_LE_0;;
 399
 400
 401 let prove_lp_tm ineqs var_ineqs target_vars target_bound precision_constant =
 402   (* Compute the sum of all constraints *)
 403   let r1 = map transform_le_ineq_tm ineqs in
 404   let r2' = List.fold_left add_step' dummy r1 in
 405   let r2 = mul_step r2' (mk_real_int precision_constant) in
 406
 407   (* Use bounds of variables *)
 408   let r3 = List.fold_left add_cancel_step r2 var_ineqs in
 409   let r4 = List.fold_left add_step' dummy (map transform_le_ineq_tm target_vars) in
 410   let r5 = add_step' r3 r4 in
 411
 412   (* Convert the result into a usual form *)
 413   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) r5 in
 414   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 415   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 416   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 417   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real ((rand o concl) r8) target_bound)) in
 418     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 419
 420
 421 let prove_lp ineqs var_ineqs target_vars target_bound precision_constant =
 422   (* Compute the sum of all constraints *)
 423   let r1 = map transform_le_ineq ineqs in
 424   let r2' = List.fold_left add_step' dummy r1 in
 425   let r2 = mul_step r2' (mk_real_int precision_constant) in
 426
 427   (* Use bounds of variables *)
 428   let r3 = List.fold_left add_cancel_step r2 var_ineqs in
 429   let r4 = List.fold_left add_step' dummy (map transform_le_ineq target_vars) in
 430   let r5 = add_step' r3 r4 in
 431
 432   (* Convert the result into a usual form *)
 433   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) r5 in
 434   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 435   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 436   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 437   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real ((rand o concl) r8) target_bound)) in
 438     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 439
 440 end;;