text_formalization/tame/dont_repeat_yourself.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - TEXT FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                         *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-04-15                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 flyspeck_needs "../graph_generator/graph_control.hl";;
  11
  12 (* Let's check that repeated values are compatible *)
  13
  14 module Dont_repeat_yourself = struct
  15
  16 open Hales_tactic;;
  17
  18 (*
  19 glpk/minorlp/tame_table.mod repeats inequalities from ineq.hl, as does
  20 glpk/minorlp/OXLZLEZ.mod
  21
  22 These have been checked by hand, but it isn't automated.
  23
  24 TODO: automate comparison of graph_control with Bauer Nipkow values.
  25 *)
  26
  27 (* Table A, B, D *)
  28
  29
  30 let table_a = Tame_defs.a_tame;;
  31 let table_b = Tame_defs.b_tame;;
  32 let table_d = Tame_defs.d_tame;;
  33 let squander = Tame_defs.tgt;;
  34
  35 let table_a_bn = Tame_classification.bn_excessTCount;;
  36 let table_b_bn = Tame_classification.bn_squanderVertex;;
  37 let table_d_bn = Tame_classification.bn_squanderFace;;
  38 let squander_bn = Tame_classification.bn_squanderTarget;;
  39
  40 let table_a_gg = Graph_control.flyspeck_properties.Graph_control.table_weight_a;;
  41 let table_b_gg = Graph_control.flyspeck_properties.Graph_control.table_weight_b;;
  42 let table_d_gg = Graph_control.flyspeck_properties.Graph_control.table_weight_d;;
  43 let squander_gg = Graph_control.flyspeck_properties.Graph_control.squander_target;;
  44
  45 let table_multiplier = new_definition `table_multiplier = &10000`;;
  46
  47 let a_bn_eq = prove_by_refinement(
  48   `a_tame * table_multiplier = &bn_excessTCount`,
  49   (* {{{ proof *)
  50   [
  51   REWRITE_TAC[table_a;table_a_bn;table_multiplier];
  52   BY(ARITH_TAC)
  53   ]);;
  54   (* }}} *)
  55
  56 let COND_MUL = prove_by_refinement(
  57   `!a b c d. (if a then (b*d) else (c*d)) = (if a then b else c)*d`,
  58   (* {{{ proof *)
  59   [
  60     BY(MESON_TAC[])
  61   ]);;
  62   (* }}} *)
  63
  64 let b_bn_eq = prove_by_refinement(
  65   `!p q. b_tame p q * table_multiplier = &(bn_squanderVertex p q)`,
  66   (* {{{ proof *)
  67   [
  68   REPEAT GEN_TAC;
  69   REWRITE_TAC[table_b_bn];
  70   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))
  71   ]);;
  72   (* }}} *)
  73
  74 let d_bn_eq = prove_by_refinement(
  75   `!n. d_tame n * table_multiplier = &(bn_squanderFace n)`,
  76   (* {{{ proof *)
  77   [
  78   REPEAT GEN_TAC;
  79   REWRITE_TAC[table_d_bn];
  80   BY((REPEAT(COND_CASES_TAC) THEN ASM_REWRITE_TAC[table_d;squander;squander_bn;table_multiplier;PAIR_EQ;squander_bn]) THEN TRY(ARITH_TAC))
  81   ]);;
  82   (* }}} *)
  83
  84  end;;