(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Calculate Numeric constants *) (* Author: Thomas C. Hales *) (* Date: 2010-07-27 *) (* ========================================================================== *) module Flyspeck_constants = struct open Sphere;; let conv_of (s,t) = (s,PURE_ONCE_REWRITE_CONV[t]);; let convl = [ conv_of ("sqrt2",sqrt2); conv_of ("sqrt3",sqrt3); conv_of ("sqrt8",sqrt8); conv_of ("sol0",sol0); conv_of("tau0",tau0); conv_of("mm1",mm1); conv_of("mm2",mm2); conv_of("pi_rt18",pi_rt18); conv_of("hplus",hplus); ];; let calc = snd o (Float.REAL_INEQUALITY_CALCULATOR convl) ;; let bounds = calc `#1.414213 < sqrt2 /\ sqrt2 < #1.414214 /\ #2.828427 < sqrt8 /\ sqrt8 < #2.828428 /\ #1.732 < sqrt3 /\ sqrt3 < #1.7321 /\ #3.14159 < pi /\ pi < #3.1416 /\ #0.551285 < sol0 /\ sol0 < #0.551286 /\ #1.54065 < tau0 /\ tau0 < #1.54066 /\ #0.740480 < pi_rt18 /\ pi_rt18 < #0.740481 /\ #1.012080 < mm1 /\ mm1 < #1.012081 /\ #0.02541 < mm2 /\ mm2 < #0.02542 /\ &0 < ((sqrt (&2) - &1) * &5 * (hplus - &1)) /\ &0 < sqrt(&2) - hplus /\ &0 < hplus - &1 `;; end;;