1 (* ========================================================================== *)
2 (* FLYSPECK - TEXT FORMALIZATION *)
4 (* Chapter: Nonlinear *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 flyspeck_needs "../graph_generator/graph_control.hl";;
12 (* Let's check that repeated values are compatible *)
14 module Dont_repeat_yourself = struct
19 glpk/minorlp/tame_table.mod repeats inequalities from ineq.hl, as does
20 glpk/minorlp/OXLZLEZ.mod
22 These have been checked by hand, but it isn't automated.
24 TODO: automate comparison of graph_control with Bauer Nipkow values.
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;;
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;;
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;;
45 let table_multiplier = new_definition `table_multiplier = &10000`;;
47 let a_bn_eq = prove_by_refinement(
48 `a_tame * table_multiplier = &bn_excessTCount`,
51 REWRITE_TAC[table_a;table_a_bn;table_multiplier];
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`,
64 let b_bn_eq = prove_by_refinement(
65 `!p q. b_tame p q * table_multiplier = &(bn_squanderVertex p q)`,
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))
74 let d_bn_eq = prove_by_refinement(
75 `!n. d_tame n * table_multiplier = &(bn_squanderFace n)`,
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))