(* ========================================================================= *)
(* 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 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;;