(* ========================================================================== *)
(* FLYSPECK - TEXT FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Nonlinear                                                         *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-04-15                                                           *)
(* ========================================================================== *)


flyspeck_needs "../graph_generator/graph_control.hl";;

(* Let's check that repeated values are compatible *)

module Dont_repeat_yourself = struct

open Hales_tactic;;

(*
glpk/minorlp/tame_table.mod repeats inequalities from ineq.hl, as does
glpk/minorlp/OXLZLEZ.mod

These have been checked by hand, but it isn't automated.

TODO: automate comparison of graph_control with Bauer Nipkow values.
*)

(* Table A, B, D *)


let table_a = Tame_defs.a_tame;;
let table_b = Tame_defs.b_tame;;
let table_d = Tame_defs.d_tame;;
let squander = Tame_defs.tgt;;

let table_a_bn = Tame_classification.bn_excessTCount;;
let table_b_bn = Tame_classification.bn_squanderVertex;;
let table_d_bn = Tame_classification.bn_squanderFace;;
let squander_bn = Tame_classification.bn_squanderTarget;;

let table_a_gg = Graph_control.flyspeck_properties.Graph_control.table_weight_a;;
let table_b_gg = Graph_control.flyspeck_properties.Graph_control.table_weight_b;;
let table_d_gg = Graph_control.flyspeck_properties.Graph_control.table_weight_d;;
let squander_gg = Graph_control.flyspeck_properties.Graph_control.squander_target;;

let table_multiplier = new_definition `table_multiplier = &10000`;;
let a_bn_eq = 
prove_by_refinement(
  `a_tame * table_multiplier = &bn_excessTCount`,

  (* {{{ proof *)
  [
  REWRITE_TAC[table_a;table_a_bn;table_multiplier];
  BY(ARITH_TAC)
  ]);;
  (* }}} *)

let COND_MUL = 
prove_by_refinement(
  `!a b c d. (if a then (b*d) else (c*d)) = (if a then b else c)*d`,

  (* {{{ proof *)
  [
    BY(MESON_TAC[])
  ]);;
  (* }}} *)

let b_bn_eq = 
prove_by_refinement(
  `!p q. b_tame p q * table_multiplier = &(bn_squanderVertex p q)`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[table_b_bn];
  BY(REPEAT(COND_CASES_TAC) THEN ASM_REWRITE_TAC[squander;table_b;table_b_bn;table_multiplier;PAIR_EQ;squander_bn;GSYM COND_MUL] THEN TRY (ARITH_TAC))
  ]);;
  (* }}} *)

let d_bn_eq = 
prove_by_refinement(
  `!n. d_tame n * table_multiplier = &(bn_squanderFace n)`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[table_d_bn];
  BY((REPEAT(COND_CASES_TAC) THEN ASM_REWRITE_TAC[table_d;squander;squander_bn;table_multiplier;PAIR_EQ;squander_bn]) THEN TRY(ARITH_TAC))
  ]);;
  (* }}} *)

 end;;