formal_lp/old/hypermap/nobranching_lp.hl

   1 needs "../formal_lp/hypermap/contravening_ineqs.hl";;
   2 needs "../formal_lp/hypermap/list_hypermap_computations.hl";;
   3 needs "../formal_lp/more_arith/prove_lp.hl";;
   4
   5 open Linear_function;;
   6 open Prove_lp;;
   7 open Arith_nat;;
   8 open Misc_vars;;
   9
  10 let REAL_ADD_ASSOC' = (SYM o SPEC_ALL) REAL_ADD_ASSOC;;
  11
  12 (* Performs the following conversions:
  13    (a + ... + c) + d = a + ... + c + d *)
  14 let rec plus_assoc_conv tm =
  15   if (is_binop add_op_real tm) then
  16     let lhs, rhs = dest_binop add_op_real tm in
  17       if (is_binop add_op_real lhs) then
  18         let x_tm, y_tm = dest_binop add_op_real lhs in
  19         let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; rhs, z_var_real] REAL_ADD_ASSOC' in
  20         let ltm, rtm = dest_comb(rand(concl th0)) in
  21           TRANS th0 (AP_TERM ltm (plus_assoc_conv rtm))
  22       else
  23         REFL tm
  24   else
  25     REFL tm;;
  26
  27 (*
  28 let tm = `(&1 + x + y + &2) + (z + t)`;;
  29 plus_assoc_conv tm;;
  30 (* 0.252 *)
  31 test 1000 (REWRITE_CONV[GSYM REAL_ADD_ASSOC]) tm;;
  32 (* 0.036 *)
  33 test 1000 plus_assoc_conv tm;;
  34 *)
  35
  36
  37
  38
  39 let prove_hypermap_lp hyp_str precision constraints target_var_bounds var_bounds =
  40   let list_hyp, list_thm, fun_table = compute_all hyp_str in
  41
  42   let table_set_rewrites =
  43     let hyp = Hashtbl.create 10 in
  44     let _ = map (fun set, name -> Hashtbl.add hyp set (Hashtbl.find list_thm name))
  45       [
  46         "list_of_darts", "darts";
  47         "list_of_darts3", "darts3";
  48         "list_of_darts4", "darts4";
  49         "list_of_dartsX", "dartsX";
  50         "list_of_nodes", "nodes";
  51         "list_of_edges", "edges";
  52         "list_of_faces", "faces";
  53         "list_of_faces3", "faces3";
  54         "list_of_faces4", "faces4";
  55         "list_of_faces5", "faces5";
  56         "list_of_faces6", "faces6";
  57       ] in
  58       hyp in
  59
  60   let l_var_list = `L:((num)list)list` in
  61
  62   (* Rewrites subterms in the inequality *)
  63   let rewrite_ineq ineq =
  64     let rec rewrite_lhs = fun tm ->
  65       let rewrite_one = fun tm ->
  66         if (is_binop mul_op_real tm) then
  67           let mul_tm, var_tm = dest_comb tm in
  68           let var_f, arg = dest_comb var_tm in
  69
  70           let rec convert_arg = fun arg ->
  71             if (is_comb arg) then
  72               let ltm, sub_arg' = dest_comb arg in
  73               let const_name = (fst o dest_const) (if (is_const ltm) then ltm else rator ltm) in
  74                 if (const_name = "CONS" or const_name = ",") then
  75                   REFL arg
  76                 else
  77                   try
  78                     let sub_arg_th = convert_arg sub_arg' in
  79                     let th0 = AP_TERM ltm sub_arg_th in
  80                     let rtm = rand(concl th0) in
  81                     let th1 =
  82                       if (const_name = "set_of_list") then
  83                         set_of_list_conv rtm
  84                       else if (const_name = "FST") then
  85                         fst_conv rtm
  86                       else if (const_name = "SND") then
  87                         snd_conv rtm
  88                       else
  89                         let table = Hashtbl.find fun_table const_name in
  90                           Hashtbl.find table (rand rtm) in
  91                       TRANS th0 th1
  92                   with e ->
  93                     failwith ("convert_arg: "^const_name)
  94             else
  95               REFL arg in
  96
  97           let arg_th = convert_arg arg in
  98             AP_TERM mul_tm (AP_TERM var_f arg_th)
  99
 100         else
 101           (* tm should be list_sum *)
 102           list_sum_conv BETA_CONV tm in
 103
 104         if (is_binop add_op_real tm) then
 105           let lhs, rhs = dest_binop add_op_real tm in
 106           let lhs_th = rewrite_one lhs in
 107           let rhs_th = rewrite_lhs rhs in
 108           let th1 = MK_COMB(AP_TERM add_op_real lhs_th, rhs_th) in
 109             if (is_binop add_op_real (rand(concl lhs_th))) then
 110               let th2 = plus_assoc_conv (rand(concl th1)) in
 111                 TRANS th1 th2
 112             else
 113               th1
 114         else
 115           rewrite_one tm in
 116
 117     let th0 = BETA_RULE ineq in
 118     let ltm, rtm = dest_comb(concl th0) in
 119     let op_tm, l_tm = dest_comb ltm in
 120     let lhs_th = rewrite_lhs l_tm in
 121       EQ_MP (AP_THM (AP_TERM op_tm lhs_th) rtm) th0 in
 122
 123   (* This function generates all inequalities from a given base inequality *)
 124   let get_ineqs = fun ineq indices ->
 125     let t0 = INST[list_hyp, l_var_list] ineq in
 126     let t1 = MY_PROVE_HYP (Hashtbl.find list_thm "good_list") t0 in
 127     let all_tm, set_tm = dest_comb (concl t1) in
 128     let set_th = Hashtbl.find table_set_rewrites ((fst o dest_const o rator) set_tm) in
 129     let t2 = EQ_MP (AP_TERM all_tm set_th) t1 in
 130     let ths = select_all t2 indices in
 131       map rewrite_ineq ths in
 132
 133
 134   let precision_constant = Int 10 **/ (Int precision) and
 135       target_bound = `&12` in
 136
 137   (* This function generates all inequalities with the given name and indices,
 138      multiplies these inequalities by given coefficients, and adds up the obtained
 139      inequalities *)
 140   let sum_step = fun (name, indices, c) ->
 141     try
 142       let ineq = find_ineq precision name in
 143       let ineqs = get_ineqs ineq indices in
 144       let s1 = map transform_le_ineq (zip ineqs c) in
 145         List.fold_left add_step' dummy s1
 146     with e ->
 147       failwith ("Problem: "^name) in
 148
 149   (* Find all sums *)
 150   let s1' = List.fold_left add_step' dummy (map sum_step constraints) in
 151   let s1 = mul_step s1' (mk_real_int precision_constant) in
 152   let s2 = List.fold_left add_step' dummy (map sum_step target_var_bounds) in
 153   let s3 = List.fold_left add_step' dummy (map sum_step var_bounds) in
 154   let s4 = add_step' (add_step' s1 s2) s3 in
 155
 156   (* Final transformations *)
 157   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) s4 in
 158   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 159   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 160   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 161   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real ((rand o concl) r8) target_bound)) in
 162     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 163
 164
 165