formal_lp/old/ineqs/nobranching_lp.hl

   1 needs "contravening_ineqs.hl";;
   2 needs "list_hypermap_computations.hl";;
   3 needs "arith/prove_lp.hl";;
   4
   5
   6 let plus_op_real = `(+):real->real->real` and
   7     mul_op_real = `( * ):real->real->real`;;
   8
   9
  10 let REAL_ADD_ASSOC' = (SYM o SPEC_ALL) REAL_ADD_ASSOC;;
  11 let x_var_real = `x:real` and
  12     y_var_real = `y:real` and
  13     z_var_real = `z:real`;;
  14
  15 (* Performs the following conversions:
  16    (a + ... + c) + d = a + ... + c + d *)
  17 let rec plus_assoc_conv tm =
  18   if (is_binop plus_op_real tm) then
  19     let lhs, rhs = dest_binop plus_op_real tm in
  20       if (is_binop plus_op_real lhs) then
  21         let x_tm, y_tm = dest_binop plus_op_real lhs in
  22         let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; rhs, z_var_real] REAL_ADD_ASSOC' in
  23         let ltm, rtm = dest_comb(rand(concl th0)) in
  24           TRANS th0 (AP_TERM ltm (plus_assoc_conv rtm))
  25       else
  26         REFL tm
  27   else
  28     REFL tm;;
  29
  30 (*
  31 let tm = `(&1 + x + y + &2) + (z + t)`;;
  32 plus_assoc_conv tm;;
  33 (* 0.252 *)
  34 test 1000 (REWRITE_CONV[GSYM REAL_ADD_ASSOC]) tm;;
  35 (* 0.036 *)
  36 test 1000 plus_assoc_conv tm;;
  37 *)
  38
  39
  40
  41
  42 let prove_hypermap_lp hyp_str precision constraints target_var_bounds var_bounds =
  43   let list_hyp, list_thm, fun_table = compute_all hyp_str in
  44
  45   let table_set_rewrites =
  46     let hyp = Hashtbl.create 10 in
  47     let _ = map (fun set, name -> Hashtbl.add hyp set (Hashtbl.find list_thm name))
  48       [
  49         "list_of_darts", "darts";
  50         "list_of_darts3", "darts3";
  51         "list_of_darts4", "darts4";
  52         "list_of_dartsX", "dartsX";
  53         "list_of_nodes", "nodes";
  54         "list_of_edges", "edges";
  55         "list_of_faces", "faces";
  56         "list_of_faces3", "faces3";
  57         "list_of_faces4", "faces4";
  58         "list_of_faces5", "faces5";
  59         "list_of_faces6", "faces6";
  60       ] in
  61       hyp in
  62
  63   let l_var_list = `L:((num)list)list` in
  64
  65   (* Rewrites subterms in the inequality *)
  66   let rewrite_ineq ineq =
  67     let rec rewrite_lhs = fun tm ->
  68       let rewrite_one = fun tm ->
  69         if (is_binop mul_op_real tm) then
  70           let mul_tm, var_tm = dest_comb tm in
  71           let var_f, arg = dest_comb var_tm in
  72
  73           let rec convert_arg = fun arg ->
  74             if (is_comb arg) then
  75               let ltm, sub_arg' = dest_comb arg in
  76               let const_name = (fst o dest_const) (if (is_const ltm) then ltm else rator ltm) in
  77                 if (const_name = "CONS" or const_name = ",") then
  78                   REFL arg
  79                 else
  80                   try
  81                     let sub_arg_th = convert_arg sub_arg' in
  82                     let th0 = AP_TERM ltm sub_arg_th in
  83                     let rtm = rand(concl th0) in
  84                     let th1 =
  85                       if (const_name = "set_of_list") then
  86                         set_of_list_conv rtm
  87                       else if (const_name = "FST") then
  88                         fst_conv rtm
  89                       else if (const_name = "SND") then
  90                         snd_conv rtm
  91                       else
  92                         let table = Hashtbl.find fun_table const_name in
  93                           Hashtbl.find table (rand rtm) in
  94                       TRANS th0 th1
  95                   with e ->
  96                     failwith ("convert_arg: "^const_name)
  97             else
  98               REFL arg in
  99
 100           let arg_th = convert_arg arg in
 101             AP_TERM mul_tm (AP_TERM var_f arg_th)
 102
 103         else
 104           (* tm should be list_sum *)
 105           list_sum_conv BETA_CONV tm in
 106
 107         if (is_binop plus_op_real tm) then
 108           let lhs, rhs = dest_binop plus_op_real tm in
 109           let lhs_th = rewrite_one lhs in
 110           let rhs_th = rewrite_lhs rhs in
 111           let th1 = MK_COMB(AP_TERM plus_op_real lhs_th, rhs_th) in
 112             if (is_binop plus_op_real (rand(concl lhs_th))) then
 113               let th2 = plus_assoc_conv (rand(concl th1)) in
 114                 TRANS th1 th2
 115             else
 116               th1
 117         else
 118           rewrite_one tm in
 119
 120     let th0 = BETA_RULE ineq in
 121     let ltm, rtm = dest_comb(concl th0) in
 122     let op_tm, l_tm = dest_comb ltm in
 123     let lhs_th = rewrite_lhs l_tm in
 124       EQ_MP (AP_THM (AP_TERM op_tm lhs_th) rtm) th0 in
 125
 126   (* This function generates all inequalities from a given base inequality *)
 127   let get_ineqs = fun ineq indices ->
 128     let t0 = INST[list_hyp, l_var_list] ineq in
 129     let t1 = MY_PROVE_HYP (Hashtbl.find list_thm "good_list") t0 in
 130     let all_tm, set_tm = dest_comb (concl t1) in
 131     let set_th = Hashtbl.find table_set_rewrites ((fst o dest_const o rator) set_tm) in
 132     let t2 = EQ_MP (AP_TERM all_tm set_th) t1 in
 133     let ths = select_all t2 indices in
 134       map rewrite_ineq ths in
 135
 136
 137   let precision_constant = Int 10 **/ (Int precision) and
 138       target_bound = `&12` in
 139
 140   (* This function generates all inequalities with the given name and indices,
 141      multiplies these inequalities by given coefficients, and adds up the obtained
 142      inequalities *)
 143   let sum_step = fun (name, indices, c) ->
 144     try
 145       let ineq = find_ineq precision name in
 146       let ineqs = get_ineqs ineq indices in
 147       let s1 = map transform_le_ineq (zip ineqs c) in
 148         List.fold_left add_step' dummy s1
 149     with e ->
 150       failwith ("Problem: "^name) in
 151
 152   (* Find all sums *)
 153   let s1' = List.fold_left add_step' dummy (map sum_step constraints) in
 154   let s1 = mul_step s1' (mk_real_int precision_constant) in
 155   let s2 = List.fold_left add_step' dummy (map sum_step target_var_bounds) in
 156   let s3 = List.fold_left add_step' dummy (map sum_step var_bounds) in
 157   let s4 = add_step' (add_step' s1 s2) s3 in
 158
 159   (* Final transformations *)
 160   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) s4 in
 161   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 162   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 163   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 164   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op ((rand o concl) r8) target_bound)) in
 165     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 166
 167
 168
 169
 170 (*******************************************)
 171
 172 (*
 173 needs "test_out.hl";;
 174 prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;
 175
 176 (* 3.060 *)
 177 test 1
 178 (prove_hypermap_lp hypermap_string precision constraints target_variables) variable_bounds;;
 179
 180
 181 let x = 1;;
 182 *)
 183
 184
 185 (*************************************)
 186
 187
 188 (*
 189 let prove_hypermap_lp hyp_str precision constraints target_var_bounds var_bounds =
 190   (* Compute all components of the hypermap *)
 191   let list_hyp, list_thm = compute_all hyp_str in
 192   let hyp_rewrites1 = map (Hashtbl.find list_thm)
 193     [
 194       "darts"; "darts3"; "darts4"; "dartsX";
 195       "nodes"; "edges";
 196       "faces"; "faces3"; "faces4"; "faces5"; "faces6"
 197     ] in
 198   let hyp_rewrites2 = map (Hashtbl.find list_thm)
 199     [
 200       "f_list_ext";
 201       "nodes_table";
 202       "faces_table";
 203     ] in
 204   let l_var_list = `L:((num)list)list` in
 205
 206   (* This function generates all inequalities from a given base inequality *)
 207   let get_ineqs = fun ineq indices ->
 208     let t0 = INST[list_hyp, l_var_list] ineq in
 209     let t1 = MY_PROVE_HYP (Hashtbl.find list_thm "good_list") t0 in
 210     let t2 = REWRITE_RULE hyp_rewrites1 t1 in
 211     let ths = select_all t2 indices in
 212     let ineqs = map (REWRITE_RULE ([list_sum; ITLIST; REAL_ADD_RID; set_of_list; GSYM REAL_ADD_ASSOC] @ hyp_rewrites2)) ths in
 213       ineqs in
 214
 215   let precision_constant = Int 10 **/ (Int precision) in
 216   let target_bound = `&12` in
 217
 218   (* This function generates all inequalities with the given name and indices,
 219      multiplies these inequalities by given coefficients, and adds up the obtained
 220      inequalities *)
 221   let sum_step = fun (name, indices, c) ->
 222     try
 223       let ineq = find_ineq precision name in
 224       let ineqs = get_ineqs ineq indices in
 225       let s1 = map transform_le_ineq (zip ineqs c) in
 226         List.fold_left add_step' dummy s1
 227     with e ->
 228       failwith ("Problem: "^name) in
 229
 230   (* Find all sums *)
 231   let s1' = List.fold_left add_step' dummy (map sum_step constraints) in
 232   let s1 = mul_step s1' (mk_real_int precision_constant) in
 233   let s2 = List.fold_left add_step' dummy (map sum_step target_var_bounds) in
 234   let s3 = List.fold_left add_step' dummy (map sum_step var_bounds) in
 235   let s4 = add_step' (add_step' s1 s2) s3 in
 236
 237   (* Final transformations *)
 238   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) s4 in
 239   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 240   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 241   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 242   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op ((rand o concl) r8) target_bound)) in
 243     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 244 *)
 245
 246
 247 (***********************************)
 248
 249 (*
 250 needs "test_out.hl";;
 251
 252 (* 18.821 *)
 253 test 1
 254 (prove_hypermap_lp hypermap_string precision constraints target_variables) variable_bounds;;
 255 *)
 256
 257 (*
 258 (* Compute all components of the hypermap *)
 259 let hyp_str = hypermap_string and
 260     target_var_bounds = target_variables and
 261     var_bounds = variable_bounds;;
 262
 263 (* 0.736 *)
 264 test 1 (compute_all) hyp_str;;
 265
 266
 267 (**************************)
 268
 269 (*
 270
 271 (* 2.340 *)
 272 test 10 (get_ineqs ineq) indices;;
 273
 274 (* 2.136 *)
 275 test 10 (get_ineqs2 ineq) indices;;
 276
 277 *)
 278
 279 *)