legacy/oldnonlinear/nonlinear/temp_ineq.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - CODE FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Linear Programming Inequalities                                          *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-08-01                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (* Generate new linear inequalities that are needed for linear
  11    programs.  This file is part of the scaffolding of the project.  It
  12    was used extensively to generate new inequalities that have been used
  13    in the linear programming part of the proof.  These inequalities have
  14    all been added to ineq.hl.
  15
  16    This file has served its purpose and is no longer needed.
  17
  18    Mathematica and Cfsqp both need to be installed before this code can
  19    be executed.  The mathematica runs are generated with the script found
  20    in the file whose pathname is given by the string math_initf.
  21
  22   There is also tight coordinate between this file and the linear programming
  23    directory glpk/tame_archive/
  24
  25    WARNING: For the functions that write external files and reread them into a
  26    reference, it seems that it is necessary to open this module for it to
  27    function properly.
  28 *)
  29
  30
  31 (*
  32
  33   There are several steps required to create an inequality and rerun
  34   linear programs.  This file automates these steps.
  35
  36   0/- Analyze output to find a triangle that is bad with
  37   sorted_azim_weighted_diff darts_of_std_tri amx;;
  38   1/- Mathematica.  holineq[Dihedral,{2,2,2,2,2,2},{2.52,2.25,2.52,2.52,2.52,2.52}].
  39   2/- save, strip "\ " at the end of lines.
  40   3/- run Parse_ineq.execute_cfsqp new_ineq to check if it seems to be true.
  41   If not, edit until it is correct.
  42   4/- change the domain info to something that is recognized by glpk model.
  43   5/- add new_ineq to put in archive.
  44   6/- Parse_ineq.lp_string()  to generate model body.mod.
  45   7/- Save body.mod in directory: glpk/tame_archive.
  46   8/- Lpproc.make_model() to make the new model.
  47   9/- Rerun the linear programs.
  48
  49 *)
  50
  51 (* Interaction with inequality generation. Mathematica is needed for
  52     the next bit.  *)
  53
  54
  55
  56
  57 flyspeck_needs "nonlinear/ineq.hl";;
  58
  59 module Temp_ineq = struct
  60
  61
  62   let all_forall = Sphere.all_forall;;
  63
  64 let junkval =  {
  65  idv = "junk";
  66  doc="junk";
  67  tags=[];
  68  ineq =
  69  all_forall `ineq [(&1,y,&2)] (y > &0)`;
  70  };;
  71
  72 (* ========================================================================== *)
  73 (* Mathematica section. *)
  74 (* ========================================================================== *)
  75
  76 let mathfile = "/Applications/Mathematica\ 5.2.app/Contents/MacOS/MathKernel";;
  77
  78 let math_initf= "/Users/thomashales/Desktop/googlecode/flyspeck/mathematica/auto_mkineq.m";;
  79
  80 let mathtemp = "/tmp/mathtemp4.hl";; (* hardwired into mathematica code *)
  81
  82 let command_string fn lb ub =
  83 (mathfile^" -run \"<< "^math_initf^ ";\n runQuit["^fn^","^lb^","^ub^"];\"");;
  84
  85 let command_string_p fn p lb ub =
  86 (mathfile^" -run \"<< "^math_initf^ ";\n runQuitp["^fn^","^p^","^lb^","^ub^"];\"");;
  87
  88 (* ========================================================================== *)
  89 (* cfsqp and ineq creation section.  The mathematica code produces a
  90    guess of an inequality (that is often inaccurate).  It is run to cfsqp
  91    to correct the guess, then packaged into an ineq.  *)
  92 (* ========================================================================== *)
  93
  94
  95  let cfsqp_margin idq =
  96   let cfsqp_dir = flyspeck_dir^"/../cfsqp" in
  97   let _ =  Parse_ineq.mk_cc (cfsqp_dir ^ "/tmp/t.cc") idq in
  98   let _ = Parse_ineq.compile() in
  99   let _ = (0=  Sys.command(cfsqp_dir^"/tmp/t.o > /tmp/cfsqp_out.txt")) or failwith "execution error" in
 100   let s2 =  process_to_string("grep 'constrained min:' /tmp/cfsqp_out.txt | sed 's/^constrained min://g' | tr -d '\n'") in  float_of_string s2;;
 101
 102 let padded_decimal_of_cfsqp idq = (* add padding to make nonlinear verifications easier *)
 103    let r =  cfsqp_margin idq in
 104      let a = if r < 0.001 then 0.001 -. r else 0.0 in
 105      let b = int_of_float (Pervasives.ceil (10000.0 *. a)) in
 106      mk_binop `DECIMAL` (mk_numeral (Int b)) (mk_numeral (Int 10000));;
 107
 108 let add_decimal ineq a =
 109   let (quant,raw) = strip_forall ineq in
 110   let (dom,gt) = dest_binop `ineq` raw in
 111   let (lhs,rhs) = dest_binop `real_gt` gt in
 112   let lhs' = mk_binop `real_add` lhs a in
 113   let gt' = mk_binop `real_gt` lhs' rhs in
 114   let raw' = mk_binop `ineq` dom gt' in
 115   let ineq' = list_mk_forall (quant,raw') in
 116    ineq';;
 117
 118 let sqrt8_sqrt2 = prove_by_refinement(
 119   `sqrt (&8) = &2 * sqrt2`,
 120   (* {{{ proof *)
 121   [
 122   SIMP_TAC[Sphere.sqrt2;SQRT_MUL;
 123      REAL_ARITH `&8 = &4 * &2 /\ &0 <= &2 /\ &0 <= &4`;];
 124   REWRITE_TAC[REAL_ARITH `&4 = &2 pow 2 /\ abs(&2) = &2`;POW_2_SQRT_ABS];
 125   ]);;
 126   (* }}} *)
 127
 128 let constant_fix = [sqrt8_sqrt2;Sphere.h0;Sphere.sqrt2;Sphere.sqrt8;
 129   REAL_ARITH `#2 = &2 /\ #2.0 = &2 /\ &2 * #1.26 = #2.52 /\ #2.00 = &2 `];;
 130
 131 (*
 132 problem: dart_std3 and dart_std3_big have the same "domain".
 133 *)
 134
 135 let reduced_dart_classes() = search_thml (term_match [])  [omit `dart_std3_big`] (map (fun t-> ("",t)) (!Ineq.dart_classes));;
 136
 137 let dart_class_rew() = map (REWRITE_RULE constant_fix)  (map (GSYM o snd ) (reduced_dart_classes()));;
 138
 139 let convert_domain ineq = snd (dest_eq (concl
 140   (REWRITE_CONV ( constant_fix @ (dart_class_rew()) ) ineq)));;
 141
 142 let adjust =
 143   let zero = `&0` in
 144   fun s idq ->
 145     let a = padded_decimal_of_cfsqp idq in
 146       if (a = zero) then idq else
 147      {
 148      idv = idq.idv;
 149      doc = idq.doc ^ s^ "\n  The inequality has been fitted to cfsqp margins.";
 150      tags = idq.tags;
 151      ineq = convert_domain(add_decimal idq.ineq a);
 152      };;
 153
 154 (* By loading the file mathtemp, the value of the reference tempval is
 155     changed to the output of the mathematica run *)
 156
 157   let tempval = ref junkval;;
 158
 159 let generate_ineq_datum =
 160   fun  fname slb sub ->
 161   let example = command_string fname slb sub in
 162   let _ = Sys.command(example) in
 163   let _ = loadt mathtemp in
 164     adjust
 165   ("\n Generated by generate_ineq_datum with input "^
 166    fname ^" "^slb^" "^sub^".") (!tempval);;
 167
 168 let generate_ineq_datum_p =
 169   fun fname sp slb sub ->
 170   let example = command_string_p fname sp slb sub in
 171   let _ = Sys.command(example) in
 172   let _ = loadt mathtemp in
 173     adjust  ("\n Generated by generate_ineq_datum_p with input "^
 174    fname ^" "^sp^" "^slb^" "^sub^".") (!tempval);;
 175
 176 (* ========================================================================== *)
 177 (* Ocaml function section. *)
 178 (* ========================================================================== *)
 179
 180
 181 (*
 182
 183 This is a quick hack that converts an Hol-light inequality (>) into a function
 184 that gives the difference between the right and left hand sides of an
 185 ineq  LHS > RHS for given values y1..y6.
 186
 187 It generates the code as a string, writes it to an external file, then
 188 reads it back into the reference tempfn.
 189
 190 It assumes that the inequality has this particular form (six free variables
 191 named y1..y6.
 192 *)
 193
 194 let ocaml_funstring_of_ineq iqd =
 195   let t = snd(strip_forall (Parse_ineq.prep_term (iqd.ineq))) in
 196   let (_,tm) = dest_comb t in
 197 let (lhs,rhs) = dest_binop `real_gt` tm in
 198 let olhs = Parse_ineq.ocaml_string_of_term lhs in
 199 let orhs = Parse_ineq.ocaml_string_of_term rhs in
 200   "(fun y1 y2 y3 y4 y5 y6 -> " ^ olhs ^ " -. " ^ orhs ^ ");;";;
 201
 202 let tempfn = ref (fun (y1:float) (y2:float) (y3:float) (y4:float) (y5:float) (y6:float) -> 0.0);;
 203
 204 let ocaml_eval =
 205   let tempfile = Filename.temp_file "ocaml_eval_" ".ml" in
 206   fun iqd ->
 207   let _ = Parse_ineq.output_filestring tempfile
 208     ("tempfn := " ^ ocaml_funstring_of_ineq iqd) in
 209   let _ = loadt tempfile in
 210     !tempfn;;
 211
 212 end;;