formal_lp/old/list/list_float.hl

   1 needs "../formal_lp/formal_interval/more_float.hl";;\r
   2 needs "../formal_lp/list/list_conversions.hl";;\r
   3 \r
   4 let MY_RULE_FLOAT = UNDISCH_ALL o NUMERALS_TO_NUM o \r
   5   PURE_REWRITE_RULE[FLOAT_OF_NUM; min_exp_def; GSYM IMP_IMP] o SPEC_ALL;;\r
   6 \r
   7 \r
   8 (*************************************)\r
   9 (* list_sum2 evaluation *)\r
  10 \r
  11 let list_sum2 = new_definition `list_sum2 f l1 l2 = ITLIST2 (\a b c. f a b + c) l1 l2 (&0)`;;\r
  12 \r
  13 let LIST_SUM2_0_LE' = (MY_RULE_FLOAT o prove)(`list_sum2 (f:A->B->real) [] [] <= &0`, \r
  14                                               REWRITE_TAC[list_sum2; ITLIST2; REAL_LE_REFL]);;\r
  15 let LIST_SUM2_1_LE' = (MY_RULE o prove)(`f h1 h2 <= x ==> list_sum2 (f:A->B->real) [h1] [h2] <= x`, \r
  16                                         REWRITE_TAC[list_sum2; ITLIST2; REAL_ADD_RID]);;\r
  17 let LIST_SUM2_LE' = (MY_RULE o prove)(`f h1 h2 <= x /\ list_sum2 f t1 t2 <= y /\ x + y <= z ==>\r
  18                                         list_sum2 (f:A->B->real) (CONS h1 t1) (CONS h2 t2) <= z`,\r
  19                                       REWRITE_TAC[list_sum2; ITLIST2] THEN STRIP_TAC THEN\r
  20                                         MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x + y:real` THEN\r
  21                                         ASM_SIMP_TAC[REAL_LE_ADD2]);;\r
  22 \r
  23 \r
  24 let list_sum2_le_conv pp f_le_conv tm =\r
  25   let ltm, list2_tm = dest_comb tm in\r
  26   let ltm2, list1_tm = dest_comb ltm in\r
  27   let f_tm = rand ltm2 in\r
  28   let list1_ty = type_of list1_tm and\r
  29       list2_ty = type_of list2_tm and\r
  30       f_ty = type_of f_tm in\r
  31   let ty1 = (hd o snd o dest_type) list1_ty and\r
  32       ty2 = (hd o snd o dest_type) list2_ty in\r
  33   let f_var = mk_var ("f", f_ty) and\r
  34       h1_var, t1_var = mk_var ("h1", ty1), mk_var ("t1", list1_ty) and\r
  35       h2_var, t2_var = mk_var ("h2", ty2), mk_var ("t2", list2_ty) in\r
  36   let inst_t = INST[f_tm, f_var] o INST_TYPE[ty1, aty; ty2, bty] in\r
  37   let list2_0, list2_1, list2_le = inst_t LIST_SUM2_0_LE', inst_t LIST_SUM2_1_LE', inst_t LIST_SUM2_LE' in\r
  38 \r
  39   let rec rec_conv = fun list1_tm list2_tm ->\r
  40     if (is_comb list1_tm) then\r
  41       let h1_tm, t1_tm = dest_cons list1_tm and\r
  42           h2_tm, t2_tm = dest_cons list2_tm in\r
  43       let f_le_th = f_le_conv pp h1_tm h2_tm in\r
  44       let x_tm = (rand o concl) f_le_th in\r
  45       let inst0 = INST[h1_tm, h1_var; h2_tm, h2_var; x_tm, x_var_real] in\r
  46         if is_comb t1_tm then\r
  47           let sum2_t_th = rec_conv t1_tm t2_tm in\r
  48           let y_tm = (rand o concl) sum2_t_th in\r
  49           let xy_th = float_add_hi pp x_tm y_tm in\r
  50           let z_tm = (rand o concl) xy_th in\r
  51             (MY_PROVE_HYP xy_th o MY_PROVE_HYP sum2_t_th o MY_PROVE_HYP f_le_th o\r
  52                INST[y_tm, y_var_real; z_tm, z_var_real; t1_tm, t1_var; t2_tm, t2_var] o \r
  53                inst0) list2_le\r
  54         else\r
  55           if is_comb t2_tm then failwith ("sum2_le_conv: t1 = []; t2 = "^string_of_term t2_tm) else\r
  56             (MY_PROVE_HYP f_le_th o inst0) list2_1\r
  57     else\r
  58       if is_comb list2_tm  then failwith ("sum2_le_conv: list1 = []; list2 = "^string_of_term list2_tm) else\r
  59         list2_0 in\r
  60 \r
  61     rec_conv list1_tm list2_tm;;\r
  62             \r
  63 \r
  64 (*\r
  65 let pp = 5;;\r
  66 let pi_approx = (fst o dest_pair o rand o concl) pi_approx_array.(pp) and\r
  67     pi2_approx = (fst o dest_pair o rand o concl) pi2_approx_array.(pp);;\r
  68 \r
  69 let l1 = mk_list (replicate pi_approx 5, real_ty) and\r
  70     l2 = mk_list (replicate pi2_approx 5, real_ty);;\r
  71 \r
  72 let tm = mk_binop `list_sum2 ( * )` l1 l2;;\r
  73 (*let test_conv pp tm =\r
  74   let tm1, tm2 = dest_binop mul_op_real tm in float_mul_hi pp tm1 tm2;; *)\r
  75 list_sum2_le_conv pp float_mul_hi tm;;\r
  76 (* 10: 4.504 *)\r
  77 test 1000 (list_sum2_le_conv pp float_mul_hi) tm;;\r
  78 *)\r
  79 \r
  80 \r
  81 (**************************)\r
  82 (* \a b c. a * iabs b + c *)\r
  83 \r
  84 let error_mul_f2 = new_definition `error_mul_f2 a int = a * iabs int`;;\r
  85 let ERROR_MUL_F2' = (SYM o MY_RULE) error_mul_f2;;\r
  86 \r
  87 \r
  88 (* |- x = a, |- P x y -> P a y *)\r
  89 let rewrite_lhs eq_th th =\r
  90   let ltm, rhs = dest_comb (concl th) in\r
  91   let th0 = AP_THM (AP_TERM (rator ltm) eq_th) rhs in\r
  92     EQ_MP th0 th;;\r
  93 \r
  94 let a_var_real = `a:real`;;\r
  95 let le_op_real = `(<=):real->real->bool`;;\r
  96 \r
  97 let error_mul_f2_le_conv pp tm1 tm2 =\r
  98   let eq_th = INST[tm1, a_var_real; tm2, int_var] ERROR_MUL_F2' in\r
  99   let iabs_th = float_iabs tm2 in\r
 100   let iabs_tm = (rand o concl) iabs_th in\r
 101   let mul_th = float_mul_hi pp tm1 iabs_tm in\r
 102   let th0 = AP_TERM (mk_comb (mul_op_real, tm1)) iabs_th in\r
 103   let th1 = AP_THM (AP_TERM le_op_real th0) (rand (concl mul_th)) in\r
 104   let le_th = EQ_MP (SYM th1) mul_th in\r
 105     rewrite_lhs eq_th le_th;;\r
 106 \r
 107 let ERROR_MUL_F2_LEMMA' = (MY_RULE o prove)(`iabs int = x /\ a * x <= y ==> error_mul_f2 a int <= y`,\r
 108                                           REWRITE_TAC[error_mul_f2] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;\r
 109 \r
 110 let error_mul_f2_le_conv2 pp tm1 tm2 =\r
 111   let iabs_th = float_iabs tm2 in\r
 112   let x_tm = (rand o concl) iabs_th in\r
 113   let mul_th = float_mul_hi pp tm1 x_tm in\r
 114   let y_tm = (rand o concl) mul_th in\r
 115     (MY_PROVE_HYP iabs_th o MY_PROVE_HYP mul_th o\r
 116        INST[tm2, int_var; tm1, a_var_real; x_tm, x_var_real; y_tm, y_var_real]) ERROR_MUL_F2_LEMMA';;\r
 117 \r
 118 \r
 119 (*\r
 120 let pp = 5;;\r
 121 let tm1 = pi_approx and tm2 = (rand o concl) pi2_approx_array.(pp);;\r
 122 error_mul_f2_le_conv pp tm1 tm2;;\r
 123 error_mul_f2_le_conv2 pp tm1 tm2;;\r
 124 (* 10: 0.772  *)\r
 125 test 1000 (error_mul_f2_le_conv pp tm1) tm2;;\r
 126 (* 10: 0.768 *)\r
 127 test 1000 (error_mul_f2_le_conv2 pp tm1) tm2;;\r
 128 \r
 129 let n = 6;;\r
 130 let l1 = mk_list (replicate pi_approx n, real_ty) and\r
 131     l2 = mk_list (replicate (mk_pair (pi2_approx, pi2_approx)) n, `:real#real`);;\r
 132 \r
 133 let tm = mk_comb (mk_comb (`list_sum2 error_mul_f2`, l1), l2);;\r
 134 \r
 135 list_sum2_le_conv pp error_mul_f2_le_conv2 tm;;\r
 136 (* 10: 5.920 *)\r
 137 test 1000 (list_sum2_le_conv pp error_mul_f2_le_conv2) tm;;\r
 138 *)\r
 139 \r
 140 \r
 141 (**************************)\r
 142 (* \a b c. a * iabs b + c *)\r
 143 \r
 144 let error_mul_f1 = new_definition `error_mul_f1 w x list = x * list_sum2 error_mul_f2 w list`;;\r
 145 \r
 146 let ERROR_MUL_F1_LEMMA' = (MY_RULE o prove)(`x * list_sum2 error_mul_f2 w list <= z ==>\r
 147                                               error_mul_f1 w x list <= z`, REWRITE_TAC[error_mul_f1]);;\r
 148 \r
 149 let list_sum2_error2_const = `list_sum2 error_mul_f2` and\r
 150     w_var_list = `w:(real)list` and\r
 151     list_var = `list:(real#real)list`;;\r
 152 \r
 153 let error_mul_f1_le_conv w_tm pp x_tm list_tm =\r
 154   (* TODO: if x = 0 then do not need to compute the sum *)\r
 155   let sum2_tm = mk_binop list_sum2_error2_const w_tm list_tm in\r
 156   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 sum2_tm in\r
 157   let ineq_th = mul_ineq_pos_const_hi pp x_tm sum2_le_th in\r
 158   let z_tm = (rand o concl) ineq_th in\r
 159     (MY_PROVE_HYP ineq_th o\r
 160        INST[x_tm, x_var_real; z_tm, z_var_real; w_tm, w_var_list; list_tm, list_var]) ERROR_MUL_F1_LEMMA';;\r
 161 \r
 162 (*\r
 163 let pp = 5;;\r
 164 let w_tm = mk_list (replicate pi5 6, real_ty) and\r
 165     x_tm = pi5;;\r
 166 let list_tm = mk_list (replicate (mk_pair (two_float, two_float)) 6, `:real#real`);;\r
 167 \r
 168 error_mul_f1_le_conv w_tm pp x_tm list_tm;;\r
 169 \r
 170 (* 10: 3.672  *)\r
 171 test 1000 (error_mul_f1_le_conv w_tm pp x_tm) list_tm;;\r
 172 *)\r
 173 \r
 174 (***********************)\r
 175 \r
 176 (*\r
 177 let n = 6;;\r
 178 let pp = 5;;\r
 179 \r
 180 let xx = mk_vector_list (replicate two_float n) and\r
 181     zz = mk_vector_list (replicate pi5 n);;\r
 182 \r
 183 let eval_poly = eval_second_bounded_poly pp delta_x_poly;;\r
 184 let th = eval_poly xx zz;;\r
 185 let domain6_th = mk_m_center_domain n pp (rand xx) (rand zz);;\r
 186 let w_tm = (rand o rand o concl) domain6_th;;\r
 187 let dd_tm = (rand o concl) th;;\r
 188 \r
 189 let op = mk_icomb (`list_sum2`, mk_comb (`error_mul_f1`, w_tm));;\r
 190 let tm = mk_binop op w_tm dd_tm;;\r
 191 \r
 192 list_sum2_le_conv pp (error_mul_f1_le_conv w_tm) tm;;\r
 193 (* 10: 4.236 *)\r
 194 test 100 (list_sum2_le_conv pp (error_mul_f1_le_conv w_tm)) tm;;\r
 195 *)\r