formal_ineqs/list/list_float.hl

   1 (* =========================================================== *)\r
   2 (* Special list conversions                                    *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 needs "arith/more_float.hl";;\r
   8 needs "list/list_conversions.hl";;\r
   9 needs "misc/vars.hl";;\r
  10 \r
  11 \r
  12 module type List_float_sig = sig\r
  13   val list_sum : thm\r
  14   val list_sum2 : thm\r
  15   val error_mul_f2 : thm\r
  16   val error_mul_f1 : thm\r
  17   val list_sum_conv : (term -> thm) -> term -> thm\r
  18   val list_sum2_le_conv : int -> (int -> term -> term -> thm) -> term -> thm\r
  19   val error_mul_f2_le_conv : int -> term -> term -> thm\r
  20   val error_mul_f2_le_conv2 : int -> term -> term -> thm\r
  21   val error_mul_f1_le_conv : term -> int -> term -> term -> thm\r
  22 end;;\r
  23 \r
  24 \r
  25 module List_float : List_float_sig = struct\r
  26 \r
  27 open Arith_misc;;\r
  28 open Arith_nat;;\r
  29 open Arith_float;;\r
  30 open More_float;;\r
  31 open Float_theory;;\r
  32 open List_conversions;;\r
  33 open Misc_vars;;\r
  34 \r
  35 let MY_RULE_FLOAT = UNDISCH_ALL o NUMERALS_TO_NUM o \r
  36   PURE_REWRITE_RULE[FLOAT_OF_NUM; min_exp_def; GSYM IMP_IMP] o SPEC_ALL;;\r
  37 \r
  38 \r
  39 (****************************)\r
  40 (* new definitions *)\r
  41 \r
  42 let list_sum = new_definition `list_sum list f = ITLIST (\t1 t2. f t1 + t2) list (&0)`;;\r
  43 let list_sum2 = new_definition `list_sum2 f l1 l2 = ITLIST2 (\a b c. f a b + c) l1 l2 (&0)`;;\r
  44 \r
  45 let error_mul_f2 = new_definition `error_mul_f2 a int = a * iabs int`;;  \r
  46 let error_mul_f1 = new_definition `error_mul_f1 w x list = x * list_sum2 error_mul_f2 w list`;;\r
  47 \r
  48 (*************************************)\r
  49 (* list_sum conversions *)\r
  50 \r
  51 let LIST_SUM_A_EMPTY = prove(`list_sum [] (f:A->real) = &0`, REWRITE_TAC[list_sum; ITLIST]) and\r
  52     LIST_SUM_A_H = prove(`list_sum [h:A] f = f h`, REWRITE_TAC[list_sum; ITLIST; REAL_ADD_RID]) and\r
  53     LIST_SUM_A_CONS = prove(`list_sum (CONS (h:A) t) f = f h + list_sum t f`, REWRITE_TAC[list_sum; ITLIST]);;\r
  54 \r
  55 \r
  56 let list_sum_conv f_conv tm =\r
  57   let ltm, f_tm = dest_comb tm in\r
  58   let list_tm = rand ltm in\r
  59   let list_ty = type_of list_tm in\r
  60   let f_ty = type_of f_tm in\r
  61   let ty = (hd o snd o dest_type) list_ty in\r
  62   let f_var = mk_var("f", f_ty) and\r
  63       h_var = mk_var("h", ty) and\r
  64       t_var = mk_var("t", list_ty) in\r
  65   let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in\r
  66   let list_sum_h = inst_t LIST_SUM_A_H and\r
  67       list_sum_cons = inst_t LIST_SUM_A_CONS in\r
  68 \r
  69   let rec list_sum_conv_raw = fun h_tm t_tm ->\r
  70     if (is_comb t_tm) then\r
  71       let h_tm', t_tm' = dest_comb t_tm in\r
  72       let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in\r
  73       let ltm, rtm = dest_comb(rand(concl th0)) in\r
  74       let plus_op, fh_tm = dest_comb ltm in\r
  75       let f_th = f_conv fh_tm in\r
  76       let th1 = list_sum_conv_raw (rand h_tm') t_tm' in\r
  77       let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in\r
  78         TRANS th0 th2\r
  79     else\r
  80       let th0 = INST[h_tm, h_var] list_sum_h in\r
  81       let f_th = f_conv (rand(concl th0)) in\r
  82         TRANS th0 f_th in\r
  83 \r
  84     if (is_comb list_tm) then\r
  85       let h_tm, t_tm = dest_comb list_tm in\r
  86         list_sum_conv_raw (rand h_tm) t_tm\r
  87     else\r
  88       inst_t LIST_SUM_A_EMPTY;;\r
  89 \r
  90 \r
  91   \r
  92 (*************************************)\r
  93 (* list_sum2 evaluation *)\r
  94 \r
  95 let LIST_SUM2_0_LE' = (MY_RULE_FLOAT o prove)(`list_sum2 (f:A->B->real) [] [] <= &0`, \r
  96                                               REWRITE_TAC[list_sum2; ITLIST2; REAL_LE_REFL]);;\r
  97 let LIST_SUM2_1_LE' = (MY_RULE_FLOAT o prove)(`f h1 h2 <= x ==> list_sum2 (f:A->B->real) [h1] [h2] <= x`, \r
  98                                         REWRITE_TAC[list_sum2; ITLIST2; REAL_ADD_RID]);;\r
  99 let LIST_SUM2_LE' = (MY_RULE_FLOAT o prove)(`f h1 h2 <= x /\ list_sum2 f t1 t2 <= y /\ x + y <= z ==>\r
 100                                         list_sum2 (f:A->B->real) (CONS h1 t1) (CONS h2 t2) <= z`,\r
 101                                       REWRITE_TAC[list_sum2; ITLIST2] THEN STRIP_TAC THEN\r
 102                                         MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x + y:real` THEN\r
 103                                         ASM_SIMP_TAC[REAL_LE_ADD2]);;\r
 104 \r
 105 \r
 106 let list_sum2_le_conv pp f_le_conv tm =\r
 107   let ltm, list2_tm = dest_comb tm in\r
 108   let ltm2, list1_tm = dest_comb ltm in\r
 109   let f_tm = rand ltm2 in\r
 110   let list1_ty = type_of list1_tm and\r
 111       list2_ty = type_of list2_tm and\r
 112       f_ty = type_of f_tm in\r
 113   let ty1 = (hd o snd o dest_type) list1_ty and\r
 114       ty2 = (hd o snd o dest_type) list2_ty in\r
 115   let f_var = mk_var ("f", f_ty) and\r
 116       h1_var, t1_var = mk_var ("h1", ty1), mk_var ("t1", list1_ty) and\r
 117       h2_var, t2_var = mk_var ("h2", ty2), mk_var ("t2", list2_ty) in\r
 118   let inst_t = INST[f_tm, f_var] o INST_TYPE[ty1, aty; ty2, bty] in\r
 119   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
 120 \r
 121   let rec rec_conv = fun list1_tm list2_tm ->\r
 122     if (is_comb list1_tm) then\r
 123       let h1_tm, t1_tm = dest_cons list1_tm and\r
 124           h2_tm, t2_tm = dest_cons list2_tm in\r
 125       let f_le_th = f_le_conv pp h1_tm h2_tm in\r
 126       let x_tm = (rand o concl) f_le_th in\r
 127       let inst0 = INST[h1_tm, h1_var; h2_tm, h2_var; x_tm, x_var_real] in\r
 128         if is_comb t1_tm then\r
 129           let sum2_t_th = rec_conv t1_tm t2_tm in\r
 130           let y_tm = (rand o concl) sum2_t_th in\r
 131           let xy_th = float_add_hi pp x_tm y_tm in\r
 132           let z_tm = (rand o concl) xy_th in\r
 133             (MY_PROVE_HYP xy_th o MY_PROVE_HYP sum2_t_th o MY_PROVE_HYP f_le_th o\r
 134                INST[y_tm, y_var_real; z_tm, z_var_real; t1_tm, t1_var; t2_tm, t2_var] o \r
 135                inst0) list2_le\r
 136         else\r
 137           if is_comb t2_tm then failwith ("sum2_le_conv: t1 = []; t2 = "^string_of_term t2_tm) else\r
 138             (MY_PROVE_HYP f_le_th o inst0) list2_1\r
 139     else\r
 140       if is_comb list2_tm  then failwith ("sum2_le_conv: list1 = []; list2 = "^string_of_term list2_tm) else\r
 141         list2_0 in\r
 142 \r
 143     rec_conv list1_tm list2_tm;;\r
 144             \r
 145 \r
 146 \r
 147 (**************************)\r
 148 (* \a b c. a * iabs b + c *)\r
 149 \r
 150 let ERROR_MUL_F2' = (SYM o MY_RULE_FLOAT) error_mul_f2;;\r
 151 \r
 152 \r
 153 (* |- x = a, |- P x y -> P a y *)\r
 154 let rewrite_lhs eq_th th =\r
 155   let ltm, rhs = dest_comb (concl th) in\r
 156   let th0 = AP_THM (AP_TERM (rator ltm) eq_th) rhs in\r
 157     EQ_MP th0 th;;\r
 158 \r
 159 let error_mul_f2_le_conv pp tm1 tm2 =\r
 160   let eq_th = INST[tm1, a_var_real; tm2, int_var] ERROR_MUL_F2' in\r
 161   let iabs_th = float_iabs tm2 in\r
 162   let iabs_tm = (rand o concl) iabs_th in\r
 163   let mul_th = float_mul_hi pp tm1 iabs_tm in\r
 164   let th0 = AP_TERM (mk_comb (mul_op_real, tm1)) iabs_th in\r
 165   let th1 = AP_THM (AP_TERM le_op_real th0) (rand (concl mul_th)) in\r
 166   let le_th = EQ_MP (SYM th1) mul_th in\r
 167     rewrite_lhs eq_th le_th;;\r
 168 \r
 169 let ERROR_MUL_F2_LEMMA' = (MY_RULE_FLOAT o prove)(`iabs int = x /\ a * x <= y ==> error_mul_f2 a int <= y`,\r
 170                                           REWRITE_TAC[error_mul_f2] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;\r
 171 \r
 172 let error_mul_f2_le_conv2 pp tm1 tm2 =\r
 173   let iabs_th = float_iabs tm2 in\r
 174   let x_tm = (rand o concl) iabs_th in\r
 175   let mul_th = float_mul_hi pp tm1 x_tm in\r
 176   let y_tm = (rand o concl) mul_th in\r
 177     (MY_PROVE_HYP iabs_th o MY_PROVE_HYP mul_th o\r
 178        INST[tm2, int_var; tm1, a_var_real; x_tm, x_var_real; y_tm, y_var_real]) ERROR_MUL_F2_LEMMA';;\r
 179 \r
 180 \r
 181 \r
 182 (**************************)\r
 183 (* \a b c. a * iabs b + c *)\r
 184 \r
 185 let ERROR_MUL_F1_LEMMA' = (MY_RULE_FLOAT o prove)(`x * list_sum2 error_mul_f2 w list <= z ==>\r
 186                                            error_mul_f1 w x list <= z`, REWRITE_TAC[error_mul_f1]);;\r
 187 \r
 188 let list_sum2_error2_const = `list_sum2 error_mul_f2` and\r
 189     w_var_list = `w:(real)list` and\r
 190     list_var = `list:(real#real)list`;;\r
 191 \r
 192 let error_mul_f1_le_conv w_tm pp x_tm list_tm =\r
 193   (* TODO: if x = 0 then do not need to compute the sum *)\r
 194   let sum2_tm = mk_binop list_sum2_error2_const w_tm list_tm in\r
 195   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 sum2_tm in\r
 196   let ineq_th = mul_ineq_pos_const_hi pp x_tm sum2_le_th in\r
 197   let z_tm = (rand o concl) ineq_th in\r
 198     (MY_PROVE_HYP ineq_th o\r
 199        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
 200 \r
 201 \r
 202 end;;\r