-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexamples_flyspeck.hl
336 lines (252 loc) · 11.4 KB
/
examples_flyspeck.hl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
(* ========================================================================== *)
(* Formal verification of nonlinear inequalities in HOL Light *)
(* *)
(* Copyright (c) 2012 Alexey Solovyev *)
(* *)
(* This file is distributed under the terms of the MIT licence *)
(* ========================================================================== *)
(* -------------------------------------------------------------------------- *)
(* Some inequalities from the Flyspeck project *)
(* https://github.com/flyspeck/flyspeck *)
(* -------------------------------------------------------------------------- *)
(* Set up the loading path:
load_path := "path to the formal_ineqs directory" :: !load_path;;
*)
(* Change default arithmetic options before loading other libraries *)
(* (arithmetic options cannot be changed later) *)
needs "arith_options.hl";;
(* Set the base of natural number arithmetic to 200 *)
Arith_options.base := 200;;
(* Load all verification libraries *)
(* Note: the verification library loads Multivariate/realanalysis.ml,
so it is recommended to use a checkpointed version of HOL Light
with preloaded realanalysis.ml *)
needs "verifier/m_verifier_main.hl";;
(*
Set the level of info/debug printing:
0 - no info/debug printing
1 - report important steps (default)
2 - report everything
*)
needs "verifier_options.hl";;
Verifier_options.info_print_level := 1;;
(* Open the main verification module *)
open M_verifier_main;;
(************************)
(* Flyspeck definitions *)
(* ineq *)
let ineq = define
`(!c. ineq [] c <=> c)
/\ (!a x b xs c. ineq (CONS (a,x,b) xs) c <=> a <= x /\ x <= b ==> ineq xs c)`;;
(* A modified (only one case is considered, x > 0) definition of atn2 *)
(* Add ' to some definitions to avoid conflicts with original Flyspeck definitions *)
let atn2' = new_definition `atn2'(x,y) = atn(y / x)`;;
(* delta_x *)
let delta_x = new_definition (`delta_x x1 x2 x3 x4 x5 x6 =
x1*x4*(--x1 + x2 + x3 -x4 + x5 + x6) +
x2*x5*(x1 - x2 + x3 + x4 -x5 + x6) +
x3*x6*(x1 + x2 - x3 + x4 + x5 - x6)
-x2*x3*x4 - x1*x3*x5 - x1*x2*x6 -x4*x5*x6`);;
(* delta_y *)
let delta_y = new_definition `delta_y y1 y2 y3 y4 y5 y6 =
delta_x (y1*y1) (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6)`;;
(* delta_x4 *)
let delta_x4= new_definition(`delta_x4 x1 x2 x3 x4 x5 x6
= -- x2* x3 - x1* x4 + x2* x5
+ x3* x6 - x5* x6 + x1* (-- x1 + x2 + x3 - x4 + x5 + x6)`);;
(* ups_x *)
let ups_x = new_definition(`ups_x x1 x2 x6 =
--x1*x1 - x2*x2 - x6*x6
+ &2 *x1*x6 + &2 *x1*x2 + &2 *x2*x6`);;
(* rho_x *)
let rho_x = new_definition(`rho_x x1 x2 x3 x4 x5 x6 =
--x1*x1*x4*x4 - x2*x2*x5*x5 - x3*x3*x6*x6 +
(&2)*x1*x2*x4*x5 + (&2)*x1*x3*x4*x6 + (&2)*x2*x3*x5*x6`);;
(* rad2_x *)
let rad2_x = new_definition(`rad2_x x1 x2 x3 x4 x5 x6 =
(rho_x x1 x2 x3 x4 x5 x6)/((delta_x x1 x2 x3 x4 x5 x6)*(&4))`);;
(* dih_x', atn2 replaced with atan2 *)
let dih_x' = new_definition(`dih_x' x1 x2 x3 x4 x5 x6 =
let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
let d = delta_x x1 x2 x3 x4 x5 x6 in
pi/ (&2) + atn2'( (sqrt ((&4) * x1 * d)),-- d_x4)`);;
(* dih_y *)
let dih_y' = new_definition(`dih_y' y1 y2 y3 y4 y5 y6 =
let (x1,x2,x3,x4,x5,x6)= (y1*y1,y2*y2,y3*y3,y4*y4,y5*y5,y6*y6) in
dih_x' x1 x2 x3 x4 x5 x6`);;
(* arclength *)
let arclength' = new_definition(`arclength' a b c =
pi/(&2) + (atn2'( (sqrt (ups_x (a*a) (b*b) (c*c))),(c*c - a*a -b*b)))`);;
(* sol_x *)
let sol_x' = new_definition(`sol_x' x1 x2 x3 x4 x5 x6 =
(dih_x' x1 x2 x3 x4 x5 x6) +
(dih_x' x2 x3 x1 x5 x6 x4) + (dih_x' x3 x1 x2 x6 x4 x5) - pi`);;
(* sol_y *)
let sol_y' = new_definition(`sol_y' y1 y2 y3 y4 y5 y6 =
(dih_y' y1 y2 y3 y4 y5 y6) +
(dih_y' y2 y3 y1 y5 y6 y4) + (dih_y' y3 y1 y2 y6 y4 y5) - pi`);;
(* const1 *)
let const1' = new_definition `const1' = sol_y' (&2) (&2) (&2) (&2) (&2) (&2) / pi`;;
(* h0 *)
let h0 = new_definition `h0 = #1.26`;;
(* lfun *)
let lfun = new_definition `lfun h = (h0 - h)/(h0 - &1)`;;
(* lfun_y1 *)
let lfun_y1 = new_definition `lfun_y1 (y1:real) (y2:real) (y3:real)
(y4:real) (y5:real) (y6:real) = lfun y1`;;
(* num1 *)
let num1 = new_definition `num1 e1 e2 e3 a2 b2 c2 =
-- &4*((a2 pow 2) *e1 + &8*(b2 - c2)*(e2 - e3) -
a2*(&16*e1 + ( b2 - &8 )*e2 + (c2 - &8)*e3))`;;
(* unit6 *)
let unit6 = define `unit6 x1 x2 x3 x4 x5 x6 = &1`;;
(* arc_hhn *)
let arc_hhn' = new_definition `arc_hhn' =
arclength' (&2 * h0) (&2 * h0) (&2)`;;
(* arclength_y1 *)
let arclength_y1' = new_definition
`arclength_y1' a b
(y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
arclength' y1 a b`;;
(* arclength_x1 *)
let arclength_x1' = new_definition
`arclength_x1' a b x1 x2 x3 x4 x5 x6 =
arclength_y1' a b (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
(* arclength_x_123 *)
let arclength_x_123' = new_definition `arclength_x_123' (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
arclength' (sqrt x1) (sqrt x2) (sqrt x3)`;;
(* acs_sqrt_x1_d4 *)
let acs_sqrt_x1_d4 = new_definition `acs_sqrt_x1_d4 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
acs (sqrt(x1)/ &4)`;;
let sqrt_x1 = define `sqrt_x1 x1 x2 x3 x4 x5 x6 = sqrt x1`;;
let sqrt_x2 = define `sqrt_x2 x1 x2 x3 x4 x5 x6 = sqrt x2`;;
let sqrt_x3 = define `sqrt_x3 x1 x2 x3 x4 x5 x6 = sqrt x3`;;
let sqrt_x4 = define `sqrt_x4 x1 x2 x3 x4 x5 x6 = sqrt x4`;;
let sqrt_x5 = define `sqrt_x5 x1 x2 x3 x4 x5 x6 = sqrt x5`;;
let sqrt_x6 = define `sqrt_x6 x1 x2 x3 x4 x5 x6 = sqrt x6`;;
(* All definitions in one list *)
let flyspeck_defs = [atn2'; delta_x; delta_y; delta_x4;
ups_x; rho_x; dih_x'; dih_y'; arclength';
sol_x'; sol_y'; const1'; num1; unit6; h0; lfun; lfun_y1;
rad2_x; arc_hhn'; arclength_y1'; arclength_x1'; acs_sqrt_x1_d4;
arclength_x_123'; sqrt_x1; sqrt_x2; sqrt_x3; sqrt_x4; sqrt_x5; sqrt_x6];;
(* A simple function for verifying Flyspeck inequalities *)
let verify_flyspeck_ineq pp ineq_tm =
let conv = REWRITE_CONV ([ineq; IMP_IMP] @ flyspeck_defs) THENC DEPTH_CONV let_CONV in
let eq_th = conv ineq_tm in
let ineq_tm1 = (rand o concl) eq_th in
let th, time = verify_ineq default_params pp ineq_tm1 in
REWRITE_RULE[GSYM eq_th] th, time;;
(* Create a hashtable for saving inequalities *)
type difficulty = Easy | Medium | Hard;;
type flyspeck_example =
{
difficulty : difficulty;
id : string;
ineq_tm : term;
};;
let examples = Hashtbl.create 20;;
let add_example ex =
Hashtbl.add examples ex.id ex;;
(* 2485876245a *)
add_example {id = "2485876245a";
difficulty = Easy;
ineq_tm = `ineq
[ #4.0,x1, #6.3504; #4.0,x2, #6.3504; #4.0,x3, #6.3504; #4.0,x4, #6.3504;
#3.0 * #3.0, x5, #2.0 * #2.52 * #2.0 * #2.52; #4.0,x6, #6.3504]
(delta_x4 x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
(* 4559601669b *)
add_example {id = "4559601669b";
difficulty = Easy;
ineq_tm = `ineq
[ #4.0,x1, #6.3504; #4.0,x2, #4.0; #4.0,x3, #6.3504;
#3.01 * #3.01, x4, #3.01 * #3.01; #4.0, x5, #6.3504; #4.0,x6, #4.0]
(delta_x4 x1 x2 x3 x4 x5 x6 < &0)`};;
(* 5512912661 *)
add_example {id = "5512912661";
difficulty = Easy;
ineq_tm = `ineq [&1,x1,&1 + (pi * const1') / pi; &1,x2,&1 + (pi * const1') / pi;
&1, x3, &1 + (pi * const1') / pi; #2.38 * #2.38, x4, #3.01 * #3.01;
&2 * &2, x5, #2.52 * #2.52; #3.15 / #1.26 * #3.15 / #1.26,x6, #15.53]
(num1 x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
(* 6843920790 *)
add_example {id = "6843920790";
difficulty = Easy;
ineq_tm = `ineq [&1,x1,&1 + (pi * const1') / pi; &1,x2,&1 + (pi * const1') / pi;
&1, x3, &1 + (pi * const1') / pi; &2 / #1.26 * &2 / #1.26, x4, #3.01 * #3.01;
#2.38 * #2.38, x5, #15.53; #2.38 * #2.38,x6, #15.53]
(num1 x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
(* 6096597438a *)
add_example {id = "6096597438a";
difficulty = Easy;
ineq_tm = `ineq [ #1.0,x1, #1.0; &1,x2,&1; &1,x3,&1; &1,x4,&1; &1,x5,&1; &1,x6,&1]
(unit6 x1 x2 x3 x4 x5 x6 * #0.591 +
unit6 x1 x2 x3 x4 x5 x6 * #0.0331 * -- &64 +
unit6 x1 x2 x3 x4 x5 x6 * #0.506 * #1.26 * &1 / ( #1.26 + -- &1) +
unit6 x1 x2 x3 x4 x5 x6 * #0.506 * --(&1 / ( #1.26 + -- &1)) +
unit6 x1 x2 x3 x4 x5 x6 * #1.0 < &0)`};;
(* 4717061266 *)
add_example {id = "4717061266";
difficulty = Easy;
ineq_tm = `ineq
[ #4.0,x1, #2.0 * #1.26 * #2.0 * #1.26; #4.0, x2, #2.0 * #1.26 * #2.0 * #1.26;
#4.0, x3, #2.0 * #1.26 * #2.0 * #1.26; #4.0,x4, #2.0 * #1.26 * #2.0 * #1.26;
#4.0, x5, #2.0 * #1.26 * #2.0 * #1.26; #4.0,x6, #2.0 * #1.26 * #2.0 * #1.26]
(delta_x x1 x2 x3 x4 x5 x6 * -- &1 < &0)`};;
(* SDCCMGA b *)
add_example {id = "SDCCMGA b";
difficulty = Easy;
ineq_tm = `ineq [ #4.0,x1, #6.3504; &1 * &1,x2,&1 * &1; &1 * &1,x3,&1 * &1;
&1 * &1, x4, &1 * &1; &1 * &1, x5, &1 * &1; &1 * &1,x6,&1 * &1]
(arclength_x1' #2.0 ( #2.0 * #1.26) x1 x2 x3 x4 x5 x6 +
arclength_x1' #2.0 ( #2.0 * #1.26) x1 x2 x3 x4 x5 x6 +
arclength_x1' ( #2.0 * #1.26) #2.0 x1 x2 x3 x4 x5 x6 * -- &1 +
unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 / &3) +
unit6 x1 x2 x3 x4 x5 x6 * --arc_hhn' < &0)`};;
(* TSKAJXY-TADIAMB *)
add_example {id = "TSKAJXY-TADIAMB";
difficulty = Medium;
ineq_tm = `ineq
[ #2.0 * #1.3254 * #2.0 * #1.3254,x1, #8.0; #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
#4.0,x3, #8.0; #4.0, x4, #8.0; #4.0,x5, #8.0; #4.0,x6, #8.0]
((unit6 x1 x2 x3 x4 x5 x6 * #2.0) * (delta_x x1 x2 x3 x4 x5 x6 * &4) < rho_x x1 x2 x3 x4 x5 x6)`};;
(* 7067938795 *)
add_example {id = "7067938795";
difficulty = Medium;
ineq_tm = `ineq [ #4.0,x1, #6.3504; #4.0,x2, #6.3504; #4.0,x3, #6.3504; #4.0,x4, #4.0;
#3.01 * #3.01, x5, #3.24 * #3.24; #3.01 * #3.01,x6, #3.24 * #3.24]
(dih_x' x1 x2 x3 x4 x5 x6 +
unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 / #2.0) +
unit6 x1 x2 x3 x4 x5 x6 * #0.46 <
&0)`};;
(* 5490182221 *)
add_example { id = "5490182221";
difficulty = Medium;
ineq_tm = `ineq
[ #4.0,x1, #6.3504; #4.0,x2, #6.3504; #4.0,x3, #6.3504; #4.0,x4, #6.3504;
#4.0, x5, #6.3504; #4.0,x6, #6.3504]
(dih_x' x1 x2 x3 x4 x5 x6 + unit6 x1 x2 x3 x4 x5 x6 * -- #1.893 < &0)`};;
(* 3318775219 *)
add_example { id = "3318775219";
difficulty = Hard;
ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
&2, y3, #2.52; #2.52, y4, sqrt(&8);
&2, y5, #2.52; &2, y6, #2.52]
( ((dih_y' y1 y2 y3 y4 y5 y6) - #1.629 +
(#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
(#0.763 * (y4 - #2.52)) -
(#0.315 * (y1 - #2.0))) * (-- &1) < &0)`};;
(* Tests *)
let run_example id =
id, verify_flyspeck_ineq 4 (Hashtbl.find examples id).ineq_tm;;
let test_easy, test_medium, test_hard =
let run keys = map run_example keys in
let get_keys d0 =
let list = Hashtbl.fold (fun k v acc -> (k, v.difficulty) :: acc) examples [] in
(setify o fst o unzip) (filter (fun (_, d) -> d = d0) list) in
(fun () -> run (get_keys Easy)),
(fun () -> run (get_keys Medium)),
(fun () -> run (get_keys Hard));;
let easy = test_easy();;
(* let medium = test_medium();; *)
(* let hard = test_hard();; *)