text_formalization/nonlinear/function_list.hl

   1 (* ========================================================================= *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                             *)
   3 (*                                                                           *)
   4 (* Chapter: nonlinear inequalities                                           *)
   5 (* Author:  Thomas Hales      *)
   6 (* Date: 2013-05-16                                                          *)
   7 (* ========================================================================= *)
   8
   9 (*
  10
  11 Initialize the set of functions that are generated in interval calculations
  12
  13 *)
  14 module Function_list = struct
  15
  16 let    function_list  = ref
  17   [
  18     (* constants *)
  19     Float.pi_atn;
  20     Functional_equation.cos797;
  21    Sphere.h0;
  22    Sphere.hplus;
  23     Sphere.sqrt3;
  24     Sphere.sqrt8;
  25     Sphere.sol0;
  26     Sphere.tau0;
  27     Sphere.mm1;
  28     Sphere.mm2;
  29     Functional_equation.rh0;
  30     SYM Nonlinear_lemma.sol0_over_pi_EQ_const1;
  31     (* single variable *)
  32     Sphere.gchi;
  33     Sphere.matan;
  34     Sphere.lfun;
  35     Sphere.flat_term;
  36     Nonlinear_lemma.rho_alt;
  37 (* deprecated 2013-08-17
  38     Sphere.sqn;
  39 *)
  40     REWRITE_RULE[Sphere.flat_term] Sphere.flat_term_x;
  41   (* 3 vars *)
  42     Nonlinear_lemma.quad_root_plus_curry;
  43    Sphere.ups_x;
  44    Sphere.eta_x;
  45    Sphere.arclength;
  46    Sphere.arc_hhn;
  47     (* general 6 *)
  48    Functional_equation.scalar6;
  49    Functional_equation.promote1_to_6;
  50    Functional_equation.promote3_to_6;
  51    Nonlinear_lemma.unit6;
  52    Nonlinear_lemma.proj_x1;
  53    Nonlinear_lemma.proj_x2;
  54    Nonlinear_lemma.proj_x3;
  55    Nonlinear_lemma.proj_x4;
  56    Nonlinear_lemma.proj_x5;
  57    Nonlinear_lemma.proj_x6;
  58    Functional_equation.compose6;
  59    Functional_equation.functional_rotate2;
  60    Functional_equation.functional_rotate3;
  61    Functional_equation.functional_rotate4;
  62    Functional_equation.functional_rotate5;
  63    Functional_equation.functional_rotate6;
  64    Functional_equation.proj_y1;
  65    Functional_equation.functional_proj_y2;
  66    Functional_equation.functional_proj_y3;
  67    Functional_equation.functional_proj_y4;
  68    Functional_equation.functional_proj_y5;
  69    Functional_equation.functional_proj_y6;
  70    Sphere.delta_x;
  71    Sphere.delta_y;
  72    Sphere.delta_x4;
  73    Sphere.dih_x;
  74    Sphere.sol_x;
  75    Sphere.dih_y;
  76    Sphere.sol_y;
  77    Sphere.rho_x;
  78    Sphere.rad2_x;
  79    Functional_equation.uni;
  80    Functional_equation.constant6;
  81    Functional_equation.two6;
  82    Functional_equation.zero6;
  83    Functional_equation.four6;
  84    Functional_equation.dummy6;
  85    Functional_equation.add6;
  86    Functional_equation.sub6;
  87    Functional_equation.mul6;
  88    Functional_equation.div6;
  89    Functional_equation.mk_126;
  90    Functional_equation.mk_135;
  91    Functional_equation.mk_456;
  92    Functional_equation.rotate126;
  93  (* by hand:  Functional_equation.domain6; *)
  94 (* deprecated:
  95    Functional_equation.rotate234;
  96    Functional_equation.rotate345;
  97    *)
  98    Functional_equation.functional_norm2hh_x;
  99 Functional_equation.functional_eta2_126;
 100 Functional_equation.functional_x1_delta_x;
 101 Functional_equation.functional_delta4_squared_x;
 102 Functional_equation.functional_vol_x;
 103 Functional_equation.functional_dih2_x;
 104 Functional_equation.functional_dih3_x;
 105 Functional_equation.functional_dih4_x;
 106 Functional_equation.functional_dih5_x;
 107 Functional_equation.functional_dih6_x;
 108 Functional_equation.functional_lfun_y1;
 109 Functional_equation.functional_ldih_x;
 110 Functional_equation.functional_ldih2_x;
 111 Functional_equation.functional_ldih3_x;
 112 Functional_equation.functional_ldih6_x;
 113 Functional_equation.functional_eulerA_x;
 114 Functional_equation.functional_gchi1_x;
 115 Functional_equation.functional_gchi2_x;
 116 Functional_equation.functional_gchi3_x;
 117 Functional_equation.functional_gchi4_x;
 118 Functional_equation.functional_gchi5_x;
 119 Functional_equation.functional_gchi6_x;
 120 Sphere.bump;
 121 Nonlinear_lemma.halfbump_x;
 122 Functional_equation.functional_halfbump_x1;
 123 Functional_equation.functional_halfbump_x4;
 124 Functional_equation.functional_eta2_135;
 125 Functional_equation.functional_eta2_456;
 126 Functional_equation.functional_vol3_x_sqrt;
 127 Functional_equation.functional_vol3f_x_lfun;
 128 Functional_equation.functional_vol3f_x_sqrt2_lmplus;
 129 Functional_equation.functional_asn797k;
 130 Functional_equation.functional_asnFnhk;
 131 Functional_equation.functional_acs_sqrt_x1_d4;
 132 Functional_equation.functional_acs_sqrt_x2_d4;
 133 Functional_equation.functional_arclength_x_123;
 134 Functional_equation.functional_sol_euler_x_divsqrtdelta;
 135 Functional_equation.functional_sol246_euler_x_div_sqrtdelta;
 136 Functional_equation.functional_sol345_euler_x_div_sqrtdelta;
 137 Functional_equation.functional_sol156_euler_x_div_sqrtdelta;
 138 Functional_equation.functional_dih_x_div_sqrtdelta_posbranch;
 139 Functional_equation.functional_dih3_x_div_sqrtdelta_posbranch;
 140 Functional_equation.functional_dih4_x_div_sqrtdelta_posbranch;
 141
 142 Functional_equation.functional_rhazim_x;
 143 Functional_equation.functional_rhazim2_x;
 144 Functional_equation.functional_rhazim3_x;
 145 Functional_equation.functional_taum_x;
 146 Functional_equation.functional_ldih_x_div_sqrtdelta_posbranch;
 147 Functional_equation.functional_ldih2_x_div_sqrtdelta_posbranch;
 148 Functional_equation.functional_ldih3_x_div_sqrtdelta_posbranch;
 149 Functional_equation.functional_ldih5_x_div_sqrtdelta_posbranch;
 150 Functional_equation.functional_ldih6_x_div_sqrtdelta_posbranch;
 151 Functional_equation.functional_arclength_x1;
 152 Functional_equation.functional_arclength_x2;
 153 Functional_equation.functional_delta_126_x;
 154 Functional_equation.functional_delta_234_x;
 155 Functional_equation.functional_delta_135_x;
 156 Functional_equation.functional_rhazim_x_div_sqrt_delta_posbranch;
 157 Functional_equation.functional_rhazim2_x_div_sqrt_delta_posbranch;
 158 Functional_equation.functional_rhazim3_x_div_sqrt_delta_posbranch;
 159 Functional_equation.functional_tau_residual;
 160 Functional_equation.h0cut;
 161 (* Functional_equation.gamma2_x_div_azim;  deprecated =gamma2= *)
 162 Nonlin_def.gamma2_x_div_azim_v2;
 163   (* Functional_equation.gamma2_x1_div_a;  deprecated =gamma2= *)
 164 Nonlin_def.gamma2_x1_div_a_v2;
 165 Functional_equation.gamma3f_x_div_sqrtdelta_alt;
 166 Functional_equation.vol3f_456;
 167 Functional_equation.gamma3_x;
 168 Functional_equation.gamma23_full8_x;
 169 Functional_equation.gamma23_keep135_x;
 170 Sphere.num1;
 171 Functional_equation.functional_dnum1;
 172 (* added 2013-05-13 *)
 173 Functional_equation.functional_delta_x1;Nonlin_def.mu6_x;Functional_equation.taud_x_ALT;
 174 Nonlin_def.taud_D2_num_x;Nonlin_def.taud_D1_num_x;
 175 Functional_equation.functional_mud_135_x;Functional_equation.functional_mud_126_x;
 176 Functional_equation.functional_mud_234_x;Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x;
 177 Nonlin_def.mudLs_135_x;
 178 Nonlin_def.ups_126;
 179 Functional_equation.functional_edge2_126_x;Functional_equation.functional_edge2_135_x;
 180 Functional_equation.functional_edge2_234_x;
 181 Nonlin_def.flat_term2_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.flat_term2_234_x;
 182 Functional_equation.functional_ups_126;
 183    ];;
 184
 185
 186
 187 (*
 188
 189 (* Test code to determine which functions are actually used.
 190   The list of rewrites are more accurate than the function list above in what is
 191   acutally used.
 192  *)
 193
 194
 195 flyspeck_needs "nonlinear/prep.hl";;
 196 #print_length 100;;
 197 let suppress = Print_types.suppress;;
 198
 199 (* univariate functions *)
 200 map suppress ["matan";"acs";"asn";"sin";"pow2";"sqrt";];;
 201 (* constants *)
 202 map suppress ["cos797";"sqrt3";"pi";"hminus";"hplus";"h0";"const1";"mm1";"mm2";"sqrt8";"sol0"];;
 203 (* functional constants and operators *)
 204 map suppress ["two6";"dummy6"];;
 205 map suppress ["add6";"mul6";"compose6";"proj_x1";"proj_x2";"proj_x3";"proj_x4"];;
 206 map suppress ["proj_x5"; "proj_x6"; "proj_y1"; "scalar6"; "sub6"];;
 207 map suppress ["sqrt_x1";"sqrt_x2";"sqrt_x3";"sqrt_x4";"sqrt_x5";"sqrt_x6"];;
 208 map suppress ["unit6";"constant6";"uni"];;
 209 map suppress ["div6";"zero6";"promote1_to_6"];;
 210 (* Lib.h univariate *)
 211 map suppress ["flat_term_x";"gamma2_x1_div_a_v2";"lfun";"halfbump_x";"rho";];;
 212 (* Lib.h multivariate *)
 213 map suppress ["delta_x";"delta_x4";"sol_x";"rad2_x";"eta2_126";"ups_126";"dih_x"];;
 214
 215 let const_types i = setify (map fst (Print_types.get_const_types i));;
 216
 217 let h1 =
 218   let p1 = !Prep.prep_ineqs in
 219   let i1 = map (fun t -> t.ineq) p1 in
 220       fun k-> (ASSUME (snd(strip_forall (List.nth i1 k))));;
 221
 222 (* ignore domain6 constraints *)
 223
 224 let domain6_assum = prove_by_refinement(
 225   `!h g f. domain6 h f g ==> (F ==> (f = g))`,
 226   (* {{{ proof *)
 227   [
 228   MESON_TAC[]
 229   ]);;
 230   (* }}} *)
 231
 232   let strip_domain6 thm =
 233     try
 234       UNDISCH (MATCH_MP domain6_assum (SPEC_ALL thm))
 235     with Failure _ -> thm;;
 236
 237   let rewrite_to_cpp_library_functions = map strip_domain6 [
 238 Sphere.ineq;
 239     Sphere.gchi;
 240    Functional_equation.uni;
 241 Functional_equation.functional_vol_x;
 242 Functional_equation.functional_dih2_x;
 243 Functional_equation.functional_dih3_x;
 244 Functional_equation.functional_dih4_x;
 245 Functional_equation.functional_dih5_x;
 246 Functional_equation.functional_dih6_x;
 247 Functional_equation.functional_gchi1_x;
 248 Functional_equation.functional_gchi2_x;
 249 Functional_equation.functional_gchi3_x;
 250 Functional_equation.functional_gchi4_x;
 251 Functional_equation.functional_gchi5_x;
 252 Functional_equation.functional_gchi6_x;
 253 Functional_equation.functional_ldih2_x;
 254 Functional_equation.functional_ldih3_x;
 255 Functional_equation.functional_eulerA_x;
 256 Functional_equation.functional_sol156_euler_x_div_sqrtdelta;
 257 Functional_equation.functional_sol246_euler_x_div_sqrtdelta;
 258 Functional_equation.functional_sol345_euler_x_div_sqrtdelta;
 259    Functional_equation.add6;
 260    Functional_equation.sub6;
 261    Functional_equation.mul6;
 262    Functional_equation.div6;
 263    Functional_equation.mk_126;
 264    Functional_equation.mk_135;
 265    Functional_equation.mk_456;
 266    Nonlinear_lemma.proj_x1;
 267    Nonlinear_lemma.proj_x2;
 268    Nonlinear_lemma.proj_x3;
 269    Nonlinear_lemma.proj_x4;
 270    Nonlinear_lemma.proj_x5;
 271    Nonlinear_lemma.proj_x6;
 272    Functional_equation.compose6;
 273    Functional_equation.functional_rotate2;
 274    Functional_equation.functional_rotate3;
 275    Functional_equation.functional_rotate4;
 276    Functional_equation.functional_rotate5;
 277    Functional_equation.functional_rotate6;
 278    Functional_equation.proj_y1;
 279    Functional_equation.functional_proj_y2;
 280    Functional_equation.functional_proj_y3;
 281    Functional_equation.functional_proj_y4;
 282    Functional_equation.functional_proj_y5;
 283    Functional_equation.functional_proj_y6;
 284 Functional_equation.functional_delta_126_x;
 285 Functional_equation.functional_delta_234_x;
 286 Functional_equation.functional_delta_135_x;
 287 Nonlin_def.flat_term2_135_x;Nonlin_def.flat_term2_234_x;
 288 Functional_equation.functional_mud_135_x;Functional_equation.functional_mud_126_x;
 289 Functional_equation.functional_mud_234_x;
 290 Functional_equation.functional_ldih2_x_div_sqrtdelta_posbranch;
 291 Functional_equation.functional_ldih3_x_div_sqrtdelta_posbranch;
 292 Functional_equation.functional_ldih5_x_div_sqrtdelta_posbranch;
 293 Functional_equation.functional_ldih6_x_div_sqrtdelta_posbranch;
 294    Sphere.delta_x;
 295 Functional_equation.functional_ldih_x_div_sqrtdelta_posbranch;
 296 Functional_equation.functional_sol_euler_x_divsqrtdelta;
 297 Functional_equation.functional_dih_x_div_sqrtdelta_posbranch;
 298 Functional_equation.functional_rhazim_x;
 299 Functional_equation.functional_rhazim2_x;
 300 Functional_equation.functional_rhazim3_x;
 301     Functional_equation.rh0;
 302 Functional_equation.functional_delta4_squared_x;
 303 Functional_equation.functional_x1_delta_x;
 304 Functional_equation.functional_tau_residual;
 305 Nonlin_def.mu6_x;Functional_equation.taud_x_ALT;
 306 Nonlin_def.taud_D2_num_x;Nonlin_def.taud_D1_num_x;
 307 Functional_equation.functional_edge2_126_x;Functional_equation.functional_edge2_135_x;
 308 Functional_equation.functional_edge2_234_x;
 309 Nonlin_def.flat_term2_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.flat_term2_234_x;
 310 Functional_equation.functional_delta_x1;
 311     REWRITE_RULE[Sphere.flat_term] Sphere.flat_term_x;
 312 Functional_equation.functional_rhazim_x_div_sqrt_delta_posbranch;
 313 Functional_equation.functional_rhazim2_x_div_sqrt_delta_posbranch;
 314 Functional_equation.functional_rhazim3_x_div_sqrt_delta_posbranch;
 315 Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x;
 316 Nonlin_def.mudLs_135_x;
 317 Functional_equation.functional_taum_x;
 318 Functional_equation.functional_dnum1;
 319 Nonlinear_lemma.halfbump_x;
 320 Functional_equation.functional_halfbump_x1;
 321 Functional_equation.functional_halfbump_x4;
 322 Functional_equation.functional_asn797k;
 323 Functional_equation.functional_asnFnhk;
 324 Functional_equation.functional_acs_sqrt_x1_d4;
 325    Sphere.arc_hhn;
 326 Functional_equation.functional_arclength_x1;
 327 REWRITE_RULE[LET_DEF;LET_END_DEF] Functional_equation.functional_arclength_x_123;
 328 Functional_equation.vol3f_456;
 329 Functional_equation.functional_vol3_x_sqrt;
 330 Functional_equation.functional_vol3f_x_sqrt2_lmplus;
 331 Functional_equation.functional_vol3f_x_lfun;
 332 Functional_equation.functional_eta2_135;
 333 Functional_equation.functional_eta2_456;
 334 Functional_equation.gamma3_x;
 335 Functional_equation.gamma23_full8_x;
 336 Functional_equation.gamma23_keep135_x;
 337 Functional_equation.gamma3f_x_div_sqrtdelta_alt;
 338 Functional_equation.functional_dih4_x_div_sqrtdelta_posbranch;
 339 Functional_equation.functional_ldih6_x;
 340 Functional_equation.functional_ldih_x;
 341    Functional_equation.functional_norm2hh_x;
 342     ];;
 343
 344   let test k =
 345     let u = REWRITE_RULE rewrite_to_cpp_library_functions
 346      (h1 k) in
 347        (concl u);;
 348
 349 let cons = (map (const_types o test) (0--(List.length !Prep.prep_ineqs - 1)));;
 350 let nubcons = Flyspeck_lib.nub cons;;
 351 *)
 352
 353   let functions() = (!function_list);;
 354
 355   let function_remove thm =
 356     let _ = (function_list:= (filter (fun t -> not(t = thm)) !function_list)) in
 357       ();;
 358
 359   let function_add thm =
 360     let _ = function_remove thm in
 361     let _ = (function_list:= (!function_list) @ [thm]) in
 362       ();;
 363
 364 end;;