(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: nonlinear inequalities *) (* Author: Thomas Hales *) (* Date: 2013-05-16 *) (* ========================================================================= *) (* Initialize the set of functions that are generated in interval calculations *) module Function_list = struct let function_list = ref [ (* constants *) Float.pi_atn; Functional_equation.cos797; Sphere.h0; Sphere.hplus; Sphere.sqrt3; Sphere.sqrt8; Sphere.sol0; Sphere.tau0; Sphere.mm1; Sphere.mm2; Functional_equation.rh0; SYM Nonlinear_lemma.sol0_over_pi_EQ_const1; (* single variable *) Sphere.gchi; Sphere.matan; Sphere.lfun; Sphere.flat_term; Nonlinear_lemma.rho_alt; (* deprecated 2013-08-17 Sphere.sqn; *) REWRITE_RULE[Sphere.flat_term] Sphere.flat_term_x; (* 3 vars *) Nonlinear_lemma.quad_root_plus_curry; Sphere.ups_x; Sphere.eta_x; Sphere.arclength; Sphere.arc_hhn; (* general 6 *) Functional_equation.scalar6; Functional_equation.promote1_to_6; Functional_equation.promote3_to_6; Nonlinear_lemma.unit6; Nonlinear_lemma.proj_x1; Nonlinear_lemma.proj_x2; Nonlinear_lemma.proj_x3; Nonlinear_lemma.proj_x4; Nonlinear_lemma.proj_x5; Nonlinear_lemma.proj_x6; Functional_equation.compose6; Functional_equation.functional_rotate2; Functional_equation.functional_rotate3; Functional_equation.functional_rotate4; Functional_equation.functional_rotate5; Functional_equation.functional_rotate6; Functional_equation.proj_y1; Functional_equation.functional_proj_y2; Functional_equation.functional_proj_y3; Functional_equation.functional_proj_y4; Functional_equation.functional_proj_y5; Functional_equation.functional_proj_y6; Sphere.delta_x; Sphere.delta_y; Sphere.delta_x4; Sphere.dih_x; Sphere.sol_x; Sphere.dih_y; Sphere.sol_y; Sphere.rho_x; Sphere.rad2_x; Functional_equation.uni; Functional_equation.constant6; Functional_equation.two6; Functional_equation.zero6; Functional_equation.four6; Functional_equation.dummy6; Functional_equation.add6; Functional_equation.sub6; Functional_equation.mul6; Functional_equation.div6; Functional_equation.mk_126; Functional_equation.mk_135; Functional_equation.mk_456; Functional_equation.rotate126; (* by hand: Functional_equation.domain6; *) (* deprecated: Functional_equation.rotate234; Functional_equation.rotate345; *) Functional_equation.functional_norm2hh_x; Functional_equation.functional_eta2_126; Functional_equation.functional_x1_delta_x; Functional_equation.functional_delta4_squared_x; Functional_equation.functional_vol_x; Functional_equation.functional_dih2_x; Functional_equation.functional_dih3_x; Functional_equation.functional_dih4_x; Functional_equation.functional_dih5_x; Functional_equation.functional_dih6_x; Functional_equation.functional_lfun_y1; Functional_equation.functional_ldih_x; Functional_equation.functional_ldih2_x; Functional_equation.functional_ldih3_x; Functional_equation.functional_ldih6_x; Functional_equation.functional_eulerA_x; Functional_equation.functional_gchi1_x; Functional_equation.functional_gchi2_x; Functional_equation.functional_gchi3_x; Functional_equation.functional_gchi4_x; Functional_equation.functional_gchi5_x; Functional_equation.functional_gchi6_x; Sphere.bump; Nonlinear_lemma.halfbump_x; Functional_equation.functional_halfbump_x1; Functional_equation.functional_halfbump_x4; Functional_equation.functional_eta2_135; Functional_equation.functional_eta2_456; Functional_equation.functional_vol3_x_sqrt; Functional_equation.functional_vol3f_x_lfun; Functional_equation.functional_vol3f_x_sqrt2_lmplus; Functional_equation.functional_asn797k; Functional_equation.functional_asnFnhk; Functional_equation.functional_acs_sqrt_x1_d4; Functional_equation.functional_acs_sqrt_x2_d4; Functional_equation.functional_arclength_x_123; Functional_equation.functional_sol_euler_x_divsqrtdelta; Functional_equation.functional_sol246_euler_x_div_sqrtdelta; Functional_equation.functional_sol345_euler_x_div_sqrtdelta; Functional_equation.functional_sol156_euler_x_div_sqrtdelta; Functional_equation.functional_dih_x_div_sqrtdelta_posbranch; Functional_equation.functional_dih3_x_div_sqrtdelta_posbranch; Functional_equation.functional_dih4_x_div_sqrtdelta_posbranch; Functional_equation.functional_rhazim_x; Functional_equation.functional_rhazim2_x; Functional_equation.functional_rhazim3_x; Functional_equation.functional_taum_x; Functional_equation.functional_ldih_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih2_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih3_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih5_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih6_x_div_sqrtdelta_posbranch; Functional_equation.functional_arclength_x1; Functional_equation.functional_arclength_x2; Functional_equation.functional_delta_126_x; Functional_equation.functional_delta_234_x; Functional_equation.functional_delta_135_x; Functional_equation.functional_rhazim_x_div_sqrt_delta_posbranch; Functional_equation.functional_rhazim2_x_div_sqrt_delta_posbranch; Functional_equation.functional_rhazim3_x_div_sqrt_delta_posbranch; Functional_equation.functional_tau_residual; Functional_equation.h0cut; (* Functional_equation.gamma2_x_div_azim; deprecated =gamma2= *) Nonlin_def.gamma2_x_div_azim_v2; (* Functional_equation.gamma2_x1_div_a; deprecated =gamma2= *) Nonlin_def.gamma2_x1_div_a_v2; Functional_equation.gamma3f_x_div_sqrtdelta_alt; Functional_equation.vol3f_456; Functional_equation.gamma3_x; Functional_equation.gamma23_full8_x; Functional_equation.gamma23_keep135_x; Sphere.num1; Functional_equation.functional_dnum1; (* added 2013-05-13 *) Functional_equation.functional_delta_x1;Nonlin_def.mu6_x;Functional_equation.taud_x_ALT; Nonlin_def.taud_D2_num_x;Nonlin_def.taud_D1_num_x; Functional_equation.functional_mud_135_x;Functional_equation.functional_mud_126_x; Functional_equation.functional_mud_234_x;Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x; Nonlin_def.mudLs_135_x; Nonlin_def.ups_126; Functional_equation.functional_edge2_126_x;Functional_equation.functional_edge2_135_x; Functional_equation.functional_edge2_234_x; Nonlin_def.flat_term2_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.flat_term2_234_x; Functional_equation.functional_ups_126; ];; (* (* Test code to determine which functions are actually used. The list of rewrites are more accurate than the function list above in what is acutally used. *) flyspeck_needs "nonlinear/prep.hl";; #print_length 100;; let suppress = Print_types.suppress;; (* univariate functions *) map suppress ["matan";"acs";"asn";"sin";"pow2";"sqrt";];; (* constants *) map suppress ["cos797";"sqrt3";"pi";"hminus";"hplus";"h0";"const1";"mm1";"mm2";"sqrt8";"sol0"];; (* functional constants and operators *) map suppress ["two6";"dummy6"];; map suppress ["add6";"mul6";"compose6";"proj_x1";"proj_x2";"proj_x3";"proj_x4"];; map suppress ["proj_x5"; "proj_x6"; "proj_y1"; "scalar6"; "sub6"];; map suppress ["sqrt_x1";"sqrt_x2";"sqrt_x3";"sqrt_x4";"sqrt_x5";"sqrt_x6"];; map suppress ["unit6";"constant6";"uni"];; map suppress ["div6";"zero6";"promote1_to_6"];; (* Lib.h univariate *) map suppress ["flat_term_x";"gamma2_x1_div_a_v2";"lfun";"halfbump_x";"rho";];; (* Lib.h multivariate *) map suppress ["delta_x";"delta_x4";"sol_x";"rad2_x";"eta2_126";"ups_126";"dih_x"];; let const_types i = setify (map fst (Print_types.get_const_types i));; let h1 = let p1 = !Prep.prep_ineqs in let i1 = map (fun t -> t.ineq) p1 in fun k-> (ASSUME (snd(strip_forall (List.nth i1 k))));; (* ignore domain6 constraints *) let domain6_assum = prove_by_refinement( `!h g f. domain6 h f g ==> (F ==> (f = g))`, (* {{{ proof *) [ MESON_TAC[] ]);; (* }}} *) let strip_domain6 thm = try UNDISCH (MATCH_MP domain6_assum (SPEC_ALL thm)) with Failure _ -> thm;; let rewrite_to_cpp_library_functions = map strip_domain6 [ Sphere.ineq; Sphere.gchi; Functional_equation.uni; Functional_equation.functional_vol_x; Functional_equation.functional_dih2_x; Functional_equation.functional_dih3_x; Functional_equation.functional_dih4_x; Functional_equation.functional_dih5_x; Functional_equation.functional_dih6_x; Functional_equation.functional_gchi1_x; Functional_equation.functional_gchi2_x; Functional_equation.functional_gchi3_x; Functional_equation.functional_gchi4_x; Functional_equation.functional_gchi5_x; Functional_equation.functional_gchi6_x; Functional_equation.functional_ldih2_x; Functional_equation.functional_ldih3_x; Functional_equation.functional_eulerA_x; Functional_equation.functional_sol156_euler_x_div_sqrtdelta; Functional_equation.functional_sol246_euler_x_div_sqrtdelta; Functional_equation.functional_sol345_euler_x_div_sqrtdelta; Functional_equation.add6; Functional_equation.sub6; Functional_equation.mul6; Functional_equation.div6; Functional_equation.mk_126; Functional_equation.mk_135; Functional_equation.mk_456; Nonlinear_lemma.proj_x1; Nonlinear_lemma.proj_x2; Nonlinear_lemma.proj_x3; Nonlinear_lemma.proj_x4; Nonlinear_lemma.proj_x5; Nonlinear_lemma.proj_x6; Functional_equation.compose6; Functional_equation.functional_rotate2; Functional_equation.functional_rotate3; Functional_equation.functional_rotate4; Functional_equation.functional_rotate5; Functional_equation.functional_rotate6; Functional_equation.proj_y1; Functional_equation.functional_proj_y2; Functional_equation.functional_proj_y3; Functional_equation.functional_proj_y4; Functional_equation.functional_proj_y5; Functional_equation.functional_proj_y6; Functional_equation.functional_delta_126_x; Functional_equation.functional_delta_234_x; Functional_equation.functional_delta_135_x; Nonlin_def.flat_term2_135_x;Nonlin_def.flat_term2_234_x; Functional_equation.functional_mud_135_x;Functional_equation.functional_mud_126_x; Functional_equation.functional_mud_234_x; Functional_equation.functional_ldih2_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih3_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih5_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih6_x_div_sqrtdelta_posbranch; Sphere.delta_x; Functional_equation.functional_ldih_x_div_sqrtdelta_posbranch; Functional_equation.functional_sol_euler_x_divsqrtdelta; Functional_equation.functional_dih_x_div_sqrtdelta_posbranch; Functional_equation.functional_rhazim_x; Functional_equation.functional_rhazim2_x; Functional_equation.functional_rhazim3_x; Functional_equation.rh0; Functional_equation.functional_delta4_squared_x; Functional_equation.functional_x1_delta_x; Functional_equation.functional_tau_residual; Nonlin_def.mu6_x;Functional_equation.taud_x_ALT; Nonlin_def.taud_D2_num_x;Nonlin_def.taud_D1_num_x; Functional_equation.functional_edge2_126_x;Functional_equation.functional_edge2_135_x; Functional_equation.functional_edge2_234_x; Nonlin_def.flat_term2_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.flat_term2_234_x; Functional_equation.functional_delta_x1; REWRITE_RULE[Sphere.flat_term] Sphere.flat_term_x; Functional_equation.functional_rhazim_x_div_sqrt_delta_posbranch; Functional_equation.functional_rhazim2_x_div_sqrt_delta_posbranch; Functional_equation.functional_rhazim3_x_div_sqrt_delta_posbranch; Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x; Nonlin_def.mudLs_135_x; Functional_equation.functional_taum_x; Functional_equation.functional_dnum1; Nonlinear_lemma.halfbump_x; Functional_equation.functional_halfbump_x1; Functional_equation.functional_halfbump_x4; Functional_equation.functional_asn797k; Functional_equation.functional_asnFnhk; Functional_equation.functional_acs_sqrt_x1_d4; Sphere.arc_hhn; Functional_equation.functional_arclength_x1; REWRITE_RULE[LET_DEF;LET_END_DEF] Functional_equation.functional_arclength_x_123; Functional_equation.vol3f_456; Functional_equation.functional_vol3_x_sqrt; Functional_equation.functional_vol3f_x_sqrt2_lmplus; Functional_equation.functional_vol3f_x_lfun; Functional_equation.functional_eta2_135; Functional_equation.functional_eta2_456; Functional_equation.gamma3_x; Functional_equation.gamma23_full8_x; Functional_equation.gamma23_keep135_x; Functional_equation.gamma3f_x_div_sqrtdelta_alt; Functional_equation.functional_dih4_x_div_sqrtdelta_posbranch; Functional_equation.functional_ldih6_x; Functional_equation.functional_ldih_x; Functional_equation.functional_norm2hh_x; ];; let test k = let u = REWRITE_RULE rewrite_to_cpp_library_functions (h1 k) in (concl u);; let cons = (map (const_types o test) (0--(List.length !Prep.prep_ineqs - 1)));; let nubcons = Flyspeck_lib.nub cons;; *) let functions() = (!function_list);; let function_remove thm = let _ = (function_list:= (filter (fun t -> not(t = thm)) !function_list)) in ();; let function_add thm = let _ = function_remove thm in let _ = (function_list:= (!function_list) @ [thm]) in ();; end;;