(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Nonlinear                                                  *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-05-30                                                           *)
(* ========================================================================== *)

(* 
File of types for nonlinear inequalities to be verified by interval arithmetic.
*)

type tag =
  (* Application and organization tags *)

 | Flypaper of string list
 | Clusterlp   | Marchal
 | Tablelp | Main_estimate
 | Fejestoth | Strongdodec | Further
 | Tex | Derived of string list   | Deprecated  

  (* Numerical testing tags *)

  | Cfsqp | Cfsqp_branch of int | Eps of float 
  | Penalty of float*float

  (* Linear programming tags *)
  |  Lp | Lp_aux of string | Lpsymmetry

  (* Interval arithmetic verification tags *)

  | Xconvert 
  | Split of int list 
  | Branching | Sharp  | Disallow_derivatives | Onlycheckderiv1negative 
  | Dim_red | Dim_red_backsym 
  | Quad_cluster of float
  | Set_rad2 | Delta126min of float | Delta126max of float | Widthcutoff of float
  | Delta135min of float | Delta135max of float 
  | Set298 (* deprecated *)
  ;;

type ineq_datum = 
  { 
    ineq : term;
    idv : string; (* name changed 2/16/2011 because of conflict with type_expr *)
    doc : string;
    tags : tag list;
  };;

type texmarker = Section | Ineqdoc | Comment;;

(* 
   Clusterlp means they enter the GLPK calcs for the cluster
   inequality.

   Marchal means they enter the non-negativity estimate for clusters
   of Marchal cells.

   Tablelp means they enter the LP calcs for the A and B tables in
   the definition of Tame h.

   Flypaper means an inequality cited directly in the flypaper
   text. The tags are the citation names in the book.  

   Further means that it is not part of the Flyspeck project, but
   part of one of the extension theorems: StrongDodec, Fejes
   Toth's contact conjecture, or Musin-Tarasov.

   Fejestoth means that it is part of the proof of the Fejes Toth's contact conjecture,
   but not part of the proof of the Kepler conjecture

   Strongdodec means that it is part of the proof of the strong dodec conjecture,
   but not part of the proof of the Kepler conjecture

   The TeX flag means that the doc field is Tex'able code (with
   software_guide.tex context).

   CFSQP TAGS:
   Cfsqp means that there is cfsqp nonlinear optimization code to
   test it by gradient descent.

   Cfsqp_branch uses this disjunct as the objective function, 
   the others as constraints.
   The default is disjunct 0.

   Eps is a small epsilon that is added to numerical testing to
   avoid answers neg. by machine eps.

   Penalty implements a penalty method in cfsqp.

   The floats (ub,wt) give the upper bound on the penalty term and its
   weight.

   LINEAR PROGRAMMING TAGS:
   Lp gives an instruction to generate a MathProg inequality for the
   GLPK program to eliminate tame hypermaps.

   Lp_aux are use to prove the Lp inequalities, but are not themselves Lp.

   Lpsymmetry gives an instruction to generate a second MathProg
   inequality by symmetry.  y2 <-> y3, y5 <-> y6.  The domain must
   already be symmetrical, otherwise an error results.

   INTERVAL ARITHMETIC TAGS:
   Derived means that it is not a primitive inequality, but rather a
   logical consequence of others.

   Main_estimate  inequalities for TameTableD and related AD HOC
   linear programming inequalities.  These appear in the Local Fan
   chapter of flypaper.

   Xconvert means to use the squared variables "x1...x6" rather than
   "y1..y6" when doing the nonlinear verification.

   Split is an instruction to the nonlinear ineq verification to split
   the indicated variables (at 2 h0).  This is needed on piecewise differentiable
   functions (namely, lmfun) to restrict to differentiable domains.

   Sharp means that equality is attained.

   Disallow_derivatives means that verification should not use first derivative
   sign to slide to an edge of the domain.

   Onlycheckderiv1negative means that it is not the function itself that should be
   verified, but only the first derivative of the first conjunct should be checked to 
   be negative.  This is useful in monotonicity results.

   Dim_red means that dimension reduction can be used on a quad cluster.

   Dim_red_backsym means that dimension reduction can be used on a
   quad cluster.  It is assumed that the function on the back simplex is taum.
   It takes the following form x8,x9 are both extremal, if both
   are as long as possible, then x7 is as short as possible.  Also x1
   is minimal or x5 is minimal (eliminating x6 minimal by a symmetry
   5-6,2-3,8-9 ).  The reductions also use ineq 4828966562 to assume
   that the diagonal y4 is at most 3.01 when both x5 and x6 are extremal.

   Quad_cluster is an ineq on a coupled pair of simplices. The float
   is the margin value for "breaksapart".

   Set_rad2 means the circumradius can be assumed to be exactly sqrt2.

   Delta126min is a lower bound on delta_x x1 x2 (&2) (&2) (&2) x6

   Delta126max is an upper bound on delta_x x1 x2 (&2) (&2) (&2) x6

   Delta135min is a lower bound on delta_x x1 (&2) x3 (&2) x5 (&2).

   Delta135max is an upper bound on delta_x x1 (&2) x3 (&2) x5 (&2).

(*   Set298 is a special tag for the inequality 2986512815. *)

*)