text_formalization/jordan/flyspeck_constants.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Calculate Numeric constants                                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-07-27                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 module Flyspeck_constants = struct
  11
  12   open Sphere;;
  13
  14   let conv_of (s,t) = (s,PURE_ONCE_REWRITE_CONV[t]);;
  15
  16   let convl = [
  17   conv_of ("sqrt2",sqrt2);
  18   conv_of ("sqrt3",sqrt3);
  19   conv_of ("sqrt8",sqrt8);
  20   conv_of ("sol0",sol0);
  21   conv_of("tau0",tau0);
  22   conv_of("mm1",mm1);
  23   conv_of("mm2",mm2);
  24   conv_of("pi_rt18",pi_rt18);
  25   conv_of("hplus",hplus);
  26   ];;
  27
  28   let calc = snd o  (Float.REAL_INEQUALITY_CALCULATOR convl)  ;;
  29
  30   let bounds = calc `#1.414213 < sqrt2 /\ sqrt2 < #1.414214 /\
  31    #2.828427 < sqrt8 /\ sqrt8 < #2.828428 /\
  32    #1.732  < sqrt3 /\ sqrt3 < #1.7321 /\
  33    #3.14159 < pi /\ pi < #3.1416 /\
  34    #0.551285 < sol0 /\ sol0 < #0.551286 /\
  35    #1.54065 < tau0 /\ tau0 < #1.54066 /\
  36    #0.740480 < pi_rt18 /\ pi_rt18 < #0.740481 /\
  37    #1.012080 < mm1 /\ mm1 < #1.012081 /\
  38    #0.02541 < mm2 /\ mm2 < #0.02542 /\
  39    &0 < ((sqrt (&2) - &1) * &5 * (hplus - &1)) /\
  40    &0 < sqrt(&2) - hplus /\
  41    &0 < hplus - &1 `;;
  42
  43
  44 end;;
  45
  46
  47