formal_lp/hypermap/ineqs/lp_body_ineqs.hl

   1 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
   2 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl";;
   3 needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
   4 needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;
   5 needs "../formal_lp/hypermap/ineqs/lp_body_ineqs_data.hl";;
   6
   7 module Lp_body_ineqs = struct
   8
   9 open Lp_ineqs_proofs;;
  10 open Lp_ineqs_proofs2;;
  11 open Lp_main_estimate;;
  12 open Sphere;;
  13 open Tame_general;;
  14 open Lp_ineqs;;
  15
  16 let special_list =
  17   let r = add_lp_hyp true in
  18     [
  19       "ineq71", (r ineq71, TRUTH);
  20       "ineq72", (r ineq72, TRUTH);
  21       "ineq73", (r ineq73, TRUTH);
  22       "ineq74", (r ineq74, TRUTH);
  23       "ineq77", (r ineq77, r ineq77_std);
  24       "ineq89", (r ineq89, r ineq89_std);
  25       "ineq90", (r ineq90, r ineq90_std);
  26       "ineq104", (r ineq104, r ineq104_std);
  27       "ineq105", (r ineq105, r ineq105_std);
  28       "ineq106", (r ineq106, r ineq106_std);
  29       "ineq118", (r ineq_tau4_diag3, r ineq_tau4_diag3_std);
  30       "ineq119", (r ineq119, r ineq119_std);
  31       "ineq120", (r ineq120, r ineq120_std);
  32       "ineq121", (r ineq121, r ineq121_std);
  33       "ineq122", (r ineq122, r ineq122_std);
  34     ];;
  35
  36 (**********************)
  37
  38 let DECIMAL_EQ = ARITH_RULE `#2.0 = &2 /\ #2.00 = &2 /\ #2 = &2 /\ #3.0 = &3`;;
  39
  40 let REAL_GT_IMP_GE = ARITH_RULE `a > b ==> a >= b:real`;;
  41
  42 let dih2_y_eq_dih3_y = prove(`dih2_y y1 y2 y3 y4 y5 y6 = dih3_y y1 y3 y2 y4 y6 y5`,
  43                              REWRITE_TAC[dih2_y; dih3_y]);;
  44
  45 let dih3_y_eq_dih2_y = prove(`dih3_y y1 y2 y3 y4 y5 y6 = dih2_y y1 y3 y2 y4 y6 y5`,
  46                              REWRITE_TAC[dih2_y; dih3_y]);;
  47
  48 let rhazim2_eq_rhazim3 = prove(`rhazim2 y1 y2 y3 y4 y5 y6 = rhazim3 y1 y3 y2 y4 y6 y5`,
  49                              REWRITE_TAC[rhazim2; rhazim3; node2_y; node3_y; rhazim; Nonlinear_lemma.dih_y_sym]);;
  50
  51
  52 let rhazim3_eq_rhazim2 = prove(`rhazim3 y1 y2 y3 y4 y5 y6 = rhazim2 y1 y3 y2 y4 y6 y5`,
  53                              REWRITE_TAC[rhazim2; rhazim3; node2_y; node3_y; rhazim; Nonlinear_lemma.dih_y_sym]);;
  54
  55
  56 let inst_list = [
  57   `y1_fan d`, `y1:real`;
  58   `y2_fan d`, `y2:real`;
  59   `y3_fan (V,E) d`, `y3:real`;
  60   `y4'_fan (V,E) d`, `y4:real`;
  61   `y5_fan (V,E) d`, `y5:real`;
  62   `y6_fan d`, `y6:real`;
  63   `y7_fan (V,E) d`, `y7:real`;
  64   `y8_fan (V,E) d`, `y8:real`;
  65   `y9_fan (V,E) d`, `y9:real`;
  66 ];;
  67
  68
  69 let inst_sym_list = [
  70   `y1_fan d`, `y1:real`;
  71   `y3_fan (V,E) d`, `y2:real`;
  72   `y2_fan d`, `y3:real`;
  73   `y4'_fan (V,E) d`, `y4:real`;
  74   `y6_fan d`, `y5:real`;
  75   `y5_fan (V,E) d`, `y6:real`;
  76 ];;
  77
  78
  79 let r = UNDISCH o SPEC_ALL o add_lp_hyp true;;
  80 let eq_ths = map r [
  81   GSYM azim_fan_eq_dih_y;
  82   GSYM rhazim_fan_eq_rhazim;
  83 ];;
  84
  85 let eq3_ths = map r [
  86   y4'_eq_y4;
  87   GSYM dart3_azim2_fan_eq_dih2_y;
  88   GSYM dart3_azim3_fan_eq_dih3_y;
  89   GSYM dart3_rhazim2_fan_eq_rhazim2;
  90   GSYM dart3_rhazim3_fan_eq_rhazim3;
  91   GSYM dart3_sol_fan_eq_sol;
  92   GSYM dart3_tau_fan_eq_taum;
  93 ] @ eq_ths;;
  94
  95 let eq4_ths = map r [
  96   GSYM dart4_tau_fan_eq_tauq;
  97 ] @ eq_ths;;
  98
  99
 100 let bounds_gen_ths = map r [
 101   y1_lo; y2_lo; y3_lo; y4_lo; y5_lo; y6_lo; y8_lo; y9_lo;
 102   y1_hi; y2_hi; y3_hi;
 103   y4'_lo; y7_lo; y7_hi;
 104 ];;
 105
 106 let bounds_std_ths = map r [
 107   y4_hi_std; y5_hi_std; y6_hi_std; y8_hi_std; y9_hi_std;
 108   y4_hi_std2; y5_hi_std2; y6_hi_std2;
 109 ];;
 110
 111 let mk_darts_k_subset_th k =
 112   let eq_th = add_lp_hyp false Hypermap_and_fan.COMPONENTS_HYPERMAP_OF_FAN in
 113     (UNDISCH_ALL o REWRITE_RULE[eq_th] o SPEC_ALL o ISPECL[`hypermap_of_fan (V,E)`; mk_small_numeral k])
 114       Lp_gen_theory.darts_k_subset;;
 115
 116 type lp_data = {
 117   d_in_tm : term;
 118   eq_ths : thm list;
 119   in_th : thm;
 120 };;
 121
 122 let mk_lp_data (tm, eq_ths, in_th) =
 123   {d_in_tm = tm; eq_ths = eq_ths; in_th = in_th};;
 124
 125 let lp_data = [
 126   "dart", mk_lp_data (`(d:real^3#real^3) IN dart_of_fan (V,E)`, eq_ths, TRUTH);
 127   "dart3", mk_lp_data (`(d:real^3#real^3) IN darts_k 3 (hypermap_of_fan (V,E))`, eq3_ths, mk_darts_k_subset_th 3);
 128   "dart4", mk_lp_data (`(d:real^3#real^3) IN darts_k 4 (hypermap_of_fan (V,E))`, eq4_ths, mk_darts_k_subset_th 4);
 129 ];;
 130
 131
 132
 133 let normalize_ineq =
 134   let normalize th =
 135     if is_binary "real_gt" (concl th) then
 136       MATCH_MP REAL_GT_IMP_GE th
 137     else if is_binary "real_lt" (concl th) then
 138       MATCH_MP REAL_LT_IMP_LE th
 139     else
 140       th in
 141     fun th ->
 142       if is_imp (concl th) then
 143         let p_tm, _ = dest_imp (concl th) in
 144         let th2 = normalize (UNDISCH th) in
 145           DISCH p_tm th2
 146       else
 147         normalize th;;
 148
 149 let finalize_th data th =
 150   let th1 = PROVE_HYP data.in_th th in
 151   let th2 = normalize_ineq th1 in
 152   let th3 = (PURE_REWRITE_RULE[GSYM IMP_IMP] o GEN `d:real^3#real^3` o DISCH data.d_in_tm) th2 in
 153     add_lp_ineqs_hyp th3;;
 154
 155
 156 (* set name, (set definitional theorem, corresponding lp set, generate std flag *)
 157 let ineq_sets = [
 158   "apex_std3_hll", (Ineq.apex_std3_hll, "dart3", true);
 159   "apex_flat_h", (Ineq.apex_flat_h, "dart3", false);
 160   "apex_flat_l", (Ineq.apex_flat_l, "dart3", false);
 161   "apex_flat_hll", (Ineq.apex_flat_hll, "dart3", false);
 162   "apex_flat", (Ineq.apex_flat, "dart3", false);
 163   "apex_std3_lhh", (Ineq.apex_std3_lhh, "dart3", true);
 164   "apex_sup_flat", (Ineq.apex_sup_flat, "dart3", false);
 165   "dart_mll_n", (Ineq.dart_mll_n, "dart3", true);
 166   "dart_mll_w", (Ineq.dart_mll_w, "dart3", true);
 167   "apex_std3_lll_wxx", (Ineq.apex_std3_lll_wxx, "dart3", true);
 168   "apex_std3_lll_xww", (Ineq.apex_std3_lll_xww, "dart3", true);
 169   "apex_std3_small_hll", (Ineq.apex_std3_small_hll, "dart3", true);
 170   "dart_std3_mini", (Ineq.dart_std3_mini, "dart3", true);
 171   "dart_std3_lw", (Ineq.dart_std3_lw, "dart3", true);
 172   "dart_std3", (Ineq.dart_std3, "dart3", true);
 173   "dart_Hll_w", (Ineq.dart_Hll_w, "dart3", true);
 174   "dart_Hll_n", (Ineq.dart_Hll_n, "dart3", true);
 175   "apexfA", (Ineq.apexfA, "dart3", false);
 176   "apexffA", (Ineq.apexffA, "dart3", false);
 177   "apex_A", (Ineq.apex_A, "dart3", false);
 178   "dart_std3_big_200_218", (Ineq.dart_std3_big_200_218, "dart3", true);
 179   "dart_std3_big", (REWRITE_RULE[GSYM Ineq.dart_std3_big] Ineq.dart_std3, "dart3", true);
 180   "dart_std3_small", (Ineq.dart_std3_small, "dart3", true);
 181   "dart4_diag3", (Ineq.dart4_diag3, "dart4", true);
 182   "dartY", (Ineq.dartY, "dart", false);
 183   "dartX", (Ineq.dartX, "dart", false);
 184 ];;
 185
 186
 187 let gen_body_ineq_ths sym_flag ineq_id set_name =
 188   let ineq_domain_th, lp_set, std_flag = assoc set_name ineq_sets in
 189   let data = assoc lp_set lp_data in
 190
 191   let ineq = (hd o Ineq.getexact) ineq_id in
 192   let th0 = (SPEC_ALL o ASSUME) (ineq.ineq) in
 193   let th1 =
 194     if sym_flag then
 195       let t1 = INST inst_sym_list th0 in
 196         ONCE_REWRITE_RULE[Nonlinear_lemma.dih_y_sym; dih2_y_eq_dih3_y; dih3_y_eq_dih2_y; rhazim2_eq_rhazim3; rhazim3_eq_rhazim2] t1
 197     else
 198       INST inst_list th0 in
 199
 200   let th2 = REWRITE_RULE data.eq_ths th1 in
 201   let th3 = REWRITE_RULE[ALL; INEQ_ALT; ineq_domain_th; DECIMAL_EQ] th2 in
 202
 203   let gen_th1 = REWRITE_RULE bounds_gen_ths th3 in
 204   let gen_th = finalize_th data gen_th1 in
 205   let std_th =
 206     if std_flag then
 207       let std_th1 = REWRITE_RULE bounds_std_ths gen_th1 in
 208         finalize_th data std_th1
 209     else
 210       TRUTH in
 211     gen_th, std_th;;
 212
 213
 214
 215
 216 (*********************)
 217
 218
 219 let add_body_ineqs () =
 220   let test (name, _, _) = true in
 221   let data = filter test Lp_body_ineqs_data.data in
 222   let sym_data = filter test Lp_body_ineqs_data.sym_data in
 223
 224   let report s =
 225     Format.print_string s; Format.print_newline(); Format.print_flush() in
 226   let counter = ref 0 and
 227       total = length data + length sym_data in
 228
 229   let add sym_flag (lp_name, ineq_id, set_name) =
 230     let _ = counter := !counter + 1 in
 231     let _ = report (sprintf "Adding %s (%d / %d)" lp_name !counter total) in
 232     let gen_th, std_th =
 233                 try assoc lp_name special_list
 234                         with Failure _ -> gen_body_ineq_ths sym_flag ineq_id set_name in
 235     let _ = add_lp_ineq_th (lp_name, false, gen_th) in
 236     let _ = if std_th <> TRUTH then add_lp_ineq_th (lp_name, true, std_th) else () in
 237       () in
 238
 239   let _ = map (add false) data in
 240   let _ = map (add true) sym_data in
 241     ();;
 242
 243 end;;
 244