1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Tame Hypermap *)
5 (* Author: Alexey Solovyev *)
7 (* Some nonlinear (polynomial) inequalities *)
8 (* ========================================================================== *)
10 flyspeck_needs "general/sphere.hl";;
11 flyspeck_needs "trigonometry/trigonometry.hl";;
12 flyspeck_needs "nonlinear/ineq.hl";;
15 module Tame_inequalities = struct
18 let let_RULE = fun th -> REWRITE_RULE[DEPTH_CONV let_CONV (concl th)] th;;
20 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
24 (* Alternative form for ineq *)
25 let INEQ_ALT = prove(`!A bounds. ineq bounds A <=> (ALL (\(a,x,b). a <= x /\ x <= b) bounds ==> A)`,
27 MATCH_MP_TAC list_INDUCT THEN REPEAT STRIP_TAC THENL
29 REWRITE_TAC[Sphere.ineq; ALL];
32 MP_TAC (ISPEC `a0:real#real#real` PAIR_SURJECTIVE) THEN
33 DISCH_THEN (X_CHOOSE_THEN `a:real` MP_TAC) THEN
34 DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
35 MP_TAC (ISPEC `y:real#real` PAIR_SURJECTIVE) THEN
36 DISCH_THEN (X_CHOOSE_THEN `x:real` MP_TAC) THEN
37 DISCH_THEN (X_CHOOSE_THEN `b:real` MP_TAC) THEN
38 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
39 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
40 ASM_SIMP_TAC[Sphere.ineq; ALL; IMP_IMP]);;
44 (**************************************************)
46 let lemma = prove(`!a b c x x0 x1. a < &0 /\ x0 <= x /\ x <= x1 ==> a*x*x + b*x + c >= a*x0*x0 + b*x0 + c \/ a*x*x + b*x + c >= a*x1*x1 + b*x1 + c`,
48 REWRITE_TAC[REAL_ARITH `a*x*x + b*x + c >= a*x0*x0 + b*x0 + c <=> &0 <= (x - x0) * (a * x0 + a * x + b)`] THEN
49 DISJ_CASES_TAC (REAL_ARITH `&0 <= a * x0 + a * x + b \/ a * x0 + a * x + b < &0`) THENL
52 MATCH_MP_TAC REAL_LE_MUL THEN
53 ASM_REWRITE_TAC[REAL_ARITH `&0 <= x - x0 <=> x0 <= x`];
55 REWRITE_TAC[REAL_ARITH `(x - x1) * (a * x1 + a * x + b) = (x1 - x) * --(a * x1 + a * x + b)`] THEN
56 MATCH_MP_TAC REAL_LE_MUL THEN
57 ASM_REWRITE_TAC[REAL_ARITH `&0 <= x1 - x <=> x <= x1`; REAL_ARITH `&0 <= --a <=> a <= &0`] THEN
58 MATCH_MP_TAC REAL_LE_TRANS THEN
59 EXISTS_TAC `a * x0 + a * x + b:real` THEN
60 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
61 REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`] THEN
62 REWRITE_TAC[REAL_ARITH `a * x1 <= a * x0 <=> &0 <= --a * (x1 - x0)`] THEN
63 MATCH_MP_TAC REAL_LE_MUL THEN
64 REPEAT (POP_ASSUM MP_TAC) THEN
69 let lemma' = prove(`!f a b c x x0 x1. f = (\x. a*x*x + b*x + c) /\ x0 <= x /\ x <= x1 /\ a < &0 ==> f x >= f x0 \/ f x >= f x1`,
71 ASM_REWRITE_TAC[] THEN
72 MATCH_MP_TAC lemma THEN
76 let lemma1 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x1 /\ x1 <= #6.3504 /\ #4.0 <= x4 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x #4.0 x2 x3 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x #6.3504 x2 x3 x4 x5 x6`,
78 SUBGOAL_THEN `!x1. delta_x x1 x2 x3 x4 x5 x6 = (\x. delta_x x x2 x3 x4 x5 x6) x1` (fun th -> ONCE_REWRITE_TAC[th]) THENL
84 MATCH_MP_TAC lemma' THEN
85 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
86 MAP_EVERY EXISTS_TAC [`--x4`; `x4*(x2+x3-x4+x5+x6)+x2*x5+x3*x6-x3*x5-x2*x6`; `x2*x5*(x3-x2+x4-x5+x6) + x3*x6*(x2-x3+x4+x5-x6)-x2*x3*x4-x4*x5*x6`] THEN
87 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
90 let lemma2 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x2 /\ x2 <= #6.3504 /\ #4.0 <= x5 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 #4.0 x3 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 #6.3504 x3 x4 x5 x6`,
92 SUBGOAL_THEN `!x2. delta_x x1 x2 x3 x4 x5 x6 = (\x. delta_x x1 x x3 x4 x5 x6) x2` (fun th -> ONCE_REWRITE_TAC[th]) THENL
98 MATCH_MP_TAC lemma' THEN
99 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
100 MAP_EVERY EXISTS_TAC [`--x5`; `x5*(x1+x3+x4-x5+x6)+x1*x4+x3*x6-x3*x4-x1*x6`; `x1*x4*(--x1+x3-x4+x5+x6) + x3*x6*(x1-x3+x4+x5-x6)-x1*x3*x5-x4*x5*x6`] THEN
101 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
104 let lemma3 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x3 /\ x3 <= #6.3504 /\ #4.0 <= x6 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #4.0 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #6.3504 x4 x5 x6`,
105 REPEAT STRIP_TAC THEN
106 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
107 MATCH_MP_TAC lemma' THEN
108 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
109 MAP_EVERY EXISTS_TAC [`--x6`; `x6*(x1+x2-x6+x4+x5)+x1*x4+x2*x5-x2*x4-x1*x5`; `x2*x5*(x1-x2+x4-x5+x6) + x1*x4*(--x1+x2-x4+x5+x6)-x1*x2*x6-x4*x5*x6`] THEN
110 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
113 let lemma4 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x4 /\ x4 <= #6.3504 /\ #4.0 <= x1 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 #4.0 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 #6.3504 x5 x6`,
114 REPEAT STRIP_TAC THEN
115 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN
116 MATCH_MP_TAC lemma' THEN
117 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
118 MAP_EVERY EXISTS_TAC [`--x1`; `x1*(--x1+x2+x3+x5+x6)+x2*x5+x3*x6-x2*x3-x5*x6`; `x2*x5*(x1-x2+x3-x5+x6) + x3*x6*(x1+x2-x3+x5-x6)-x1*x3*x5-x1*x2*x6`] THEN
119 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
122 let lemma5 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x5 /\ x5 <= #6.3504 /\ #4.0 <= x2 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 #4.0 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 #6.3504 x6`,
123 REPEAT STRIP_TAC THEN
124 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN
125 MATCH_MP_TAC lemma' THEN
126 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
127 MAP_EVERY EXISTS_TAC [`--x2`; `x2*(x1+x3-x2+x4+x6)+x1*x4+x3*x6-x1*x3-x4*x6`; `x1*x4*(--x1+x2+x3-x4+x6) + x3*x6*(x1+x2-x3+x4-x6)-x2*x3*x4-x1*x2*x6`] THEN
128 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
131 let lemma6 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x6 /\ x6 <= #6.3504 /\ #4.0 <= x3 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #4.0 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #6.3504`,
132 REPEAT STRIP_TAC THEN
133 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
134 MATCH_MP_TAC lemma' THEN
135 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
136 MAP_EVERY EXISTS_TAC [`--x3`; `x3*(x1+x2-x3+x4+x5)+x1*x4+x2*x5-x1*x2-x4*x5`; `x2*x5*(x1-x2+x3+x4-x5) + x1*x4*(--x1+x2+x3-x4+x5)-x2*x3*x4-x1*x3*x5`] THEN
137 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
144 let main_lemma = prove(`!(f:real->real) x x0 x1 m. (f x >= f x0 \/ f x >= f x1) /\ f x0 >= m /\ f x1 >= m ==> f x >= m`,
145 REWRITE_TAC[real_ge] THEN
146 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THENL
148 EXISTS_TAC `(f:real->real) x0` THEN
150 EXISTS_TAC `(f:real->real) x1` THEN
155 (* delta_x > 0 for x IN [4,4 h0^2] *)
157 let delta_x_pos = prove(`!x1 x2 x3 x4 x5 x6. ineq [#4.0,x1,#6.3504;
162 #4.0,x6,#6.3504] (delta_x x1 x2 x3 x4 x5 x6 >= #128.0)`,
163 REPEAT STRIP_TAC THEN
164 REWRITE_TAC[INEQ_ALT; ALL] THEN
165 REPEAT STRIP_TAC THEN
166 ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
169 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN
170 MATCH_MP_TAC main_lemma THEN
171 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
172 ASM_SIMP_TAC[lemma1] THEN
176 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN
177 MATCH_MP_TAC main_lemma THEN
178 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
179 ASM_SIMP_TAC[lemma2] THEN
183 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
184 MATCH_MP_TAC main_lemma THEN
185 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
186 ASM_SIMP_TAC[lemma3] THEN
190 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN
191 MATCH_MP_TAC main_lemma THEN
192 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
193 ASM_SIMP_TAC[lemma4] THEN
197 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN
198 MATCH_MP_TAC main_lemma THEN
199 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
200 ASM_SIMP_TAC[lemma5] THEN
204 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
205 MATCH_MP_TAC main_lemma THEN
206 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
207 ASM_SIMP_TAC[lemma6] THEN
211 REWRITE_TAC[Sphere.delta_x] THEN
212 CONV_TAC REAL_RAT_REDUCE_CONV);;
215 let lemma3 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x3 /\ x3 <= #6.3504 /\ #0.64 <= x6 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #4.0 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #6.3504 x4 x5 x6`,
216 REPEAT STRIP_TAC THEN
217 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
218 MATCH_MP_TAC lemma' THEN
219 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
220 MAP_EVERY EXISTS_TAC [`--x6`; `x6*(x1+x2-x6+x4+x5)+x1*x4+x2*x5-x2*x4-x1*x5`; `x2*x5*(x1-x2+x4-x5+x6) + x1*x4*(--x1+x2-x4+x5+x6)-x1*x2*x6-x4*x5*x6`] THEN
221 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
225 let lemma6 = prove(`!x1 x2 x3 x4 x5 x6. #0.64 <= x6 /\ x6 <= #6.3504 /\ #4.0 <= x3 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #0.64 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #6.3504`,
226 REPEAT STRIP_TAC THEN
227 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
228 MATCH_MP_TAC lemma' THEN
229 ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
230 MAP_EVERY EXISTS_TAC [`--x3`; `x3*(x1+x2-x3+x4+x5)+x1*x4+x2*x5-x1*x2-x4*x5`; `x2*x5*(x1-x2+x3+x4-x5) + x1*x4*(--x1+x2+x3-x4+x5)-x2*x3*x4-x1*x3*x5`] THEN
231 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
235 (* delta_x > 0 for a special configuration of three points *)
237 let delta_x_3_points = prove(`!x1 x2 x3 x6. ineq [#4.0,x1,#6.3504;
240 #0.64,x6,#6.3504] (delta_x x1 x2 x3 (#4.0) (#4.0) x6 >= #13.0)`,
241 REPEAT STRIP_TAC THEN
242 REWRITE_TAC[INEQ_ALT; ALL] THEN
243 REPEAT STRIP_TAC THEN
244 ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
247 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN
248 MATCH_MP_TAC main_lemma THEN
249 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
250 ASM_SIMP_TAC[lemma1] THEN
254 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN
255 MATCH_MP_TAC main_lemma THEN
256 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
257 ASM_SIMP_TAC[lemma2] THEN
261 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
262 MATCH_MP_TAC main_lemma THEN
263 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
264 ASM_SIMP_TAC[lemma3] THEN
268 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
269 MATCH_MP_TAC main_lemma THEN
270 MAP_EVERY EXISTS_TAC [`#0.64`; `#6.3504`] THEN
271 ASM_SIMP_TAC[lemma6] THEN
275 REWRITE_TAC[Sphere.delta_x] THEN
276 CONV_TAC REAL_RAT_REDUCE_CONV);;
280 (************************************************************)
283 (* eta_y pow 2 <= #2.2 *)
286 let lemma1 = prove(`!x1 x2 x3. #4.0 <= x1 /\ x1 <= #6.3504 ==>
287 #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x #4.0 x2 x3 - #4.0 * x2 * x3 \/
288 #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x #6.3504 x2 x3 - #6.3504 * x2 * x3`,
289 REPEAT STRIP_TAC THEN
290 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x x2 x3 - x * x2 * x3) x1`)] THEN
291 MATCH_MP_TAC lemma' THEN
292 ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN
293 MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x3 + &2 * x2) - x2 * x3`; `#2.2 * (&2 * x2 * x3 - x2*x2 - x3*x3)`] THEN
297 let lemma2 = prove(`!x1 x2 x3. #4.0 <= x2 /\ x2 <= #6.3504 ==>
298 #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 #4.0 x3 - x1 * #4.0 * x3 \/
299 #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 #6.3504 x3 - x1 * #6.3504 * x3`,
300 REPEAT STRIP_TAC THEN
301 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x x3 - x1 * x * x3) x2`)] THEN
302 MATCH_MP_TAC lemma' THEN
303 ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN
304 MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x1 + &2 * x3) - x1 * x3`; `#2.2 * (&2 * x1 * x3 - x1*x1 - x3*x3)`] THEN
308 let lemma3 = prove(`!x1 x2 x3. #4.0 <= x3 /\ x3 <= #6.3504 ==>
309 #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 x2 #4.0 - x1 * x2 * #4.0 \/
310 #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 x2 #6.3504 - x1 * x2 * #6.3504`,
311 REPEAT STRIP_TAC THEN
312 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x2 x - x1 * x2 * x) x3`)] THEN
313 MATCH_MP_TAC lemma' THEN
314 ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN
315 MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x1 + &2 * x2) - x2 * x1`; `#2.2 * (&2 * x2 * x1 - x2*x2 - x1*x1)`] THEN
320 let eta_x_ineq_lemma = prove(`!x1 x2 x3. ineq [#4.0,x1,#6.3504;
323 (#2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= &0)`,
324 REPEAT STRIP_TAC THEN
325 REWRITE_TAC[INEQ_ALT; ALL] THEN
326 REPEAT STRIP_TAC THEN
327 ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
330 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x x2 x3 - x * x2 * x3) x1`)] THEN
331 MATCH_MP_TAC main_lemma THEN
332 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
333 ASM_SIMP_TAC[lemma1] THEN
337 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x x3 - x1 * x * x3) x2`)] THEN
338 MATCH_MP_TAC main_lemma THEN
339 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
340 ASM_SIMP_TAC[lemma2] THEN
344 ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x2 x - x1 * x2 * x) x3`)] THEN
345 MATCH_MP_TAC main_lemma THEN
346 MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
347 ASM_SIMP_TAC[lemma3] THEN
351 REWRITE_TAC[Sphere.ups_x] THEN
352 CONV_TAC REAL_RAT_REDUCE_CONV);;
356 let ETA_Y_4_POINTS_INEQ = prove(`!y1 y2 y3. ineq[(&2, y1, &2 * h0); (&2, y2, &2 * h0); (&2, y3, &2 * h0)]
357 (eta_y y1 y2 y3 pow 2 <= #2.2)`,
358 REWRITE_TAC[INEQ_ALT; ALL; Sphere.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
359 REPEAT GEN_TAC THEN DISCH_TAC THEN
360 REWRITE_TAC[Sphere.eta_y; Sphere.eta_x] THEN
361 CONV_TAC (DEPTH_CONV let_CONV) THEN
362 MAP_EVERY ABBREV_TAC [`x1 = y1 * y1:real`; `x2 = y2 * y2:real`; `x3 = y3 * y3:real`] THEN
363 SUBGOAL_THEN `!y. &2 <= y /\ y <= #2.52 ==> #4.0 <= y * y /\ y * y <= #6.3504` ASSUME_TAC THENL
366 REWRITE_TAC[REAL_ARITH `#4.0 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
367 REWRITE_TAC[GSYM REAL_POW_2] THEN
368 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
372 MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`y1:real`; `y2:real`; `y3:real`] THEN
373 REMOVE_ASSUM THEN ASM_REWRITE_TAC[] THEN
374 REPEAT DISCH_TAC THEN
375 MP_TAC (SPEC_ALL eta_x_ineq_lemma) THEN
376 ASM_REWRITE_TAC[INEQ_ALT; ALL] THEN
379 SUBGOAL_THEN `&0 < x1 * x2 * x3` ASSUME_TAC THENL
381 ASSUME_TAC (REAL_ARITH `!x. #4.0 <= x ==> &0 < x`) THEN
382 MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[] THEN
383 MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[];
387 SUBGOAL_THEN `&0 < ups_x x1 x2 x3` ASSUME_TAC THENL
389 MATCH_MP_TAC (REAL_ARITH `#2.2 * u - x1 * x2 * x3 >= &0 /\ &0 < x1 * x2 * x3 ==> &0 < u`) THEN
394 SUBGOAL_THEN `&0 <= (x1 * x2 * x3) / ups_x x1 x2 x3` ASSUME_TAC THENL
396 MATCH_MP_TAC REAL_LE_DIV THEN
397 ASM_SIMP_TAC[REAL_LT_IMP_LE];
400 ASM_SIMP_TAC[SQRT_POW_2] THEN
401 ONCE_REWRITE_TAC[REAL_ARITH `#2.2 = #2.2 / &1`] THEN
402 ASSUME_TAC (REAL_ARITH `&0 < &1`) THEN
403 ASM_SIMP_TAC[RAT_LEMMA4] THEN
404 REPLICATE_TAC 4 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
414 (*************************************************************)
422 let DELTA_X4_MONO_LT_4 = prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 < x1
423 ==> delta_x4 x1 x2 x3 b x5 x6 <
424 delta_x4 x1 x2 x3 a x5 x6`,
425 REPEAT STRIP_TAC THEN
426 REWRITE_TAC[Sphere.delta_x4] THEN
427 REWRITE_TAC[REAL_ARITH `a - b + c + d - e + f < a - g + c + d - e + h <=> f - b < h - g`] THEN
428 REWRITE_TAC[REAL_ARITH `x1*(--x1+x2+x3-b+x5+x6)-x1*b = --(&2*x1*b) + x1*(--x1+x2+x3+x5+x6)`] THEN
429 REWRITE_TAC[REAL_ARITH `--a + b < --c + b <=> c < a`] THEN
430 MATCH_MP_TAC REAL_LT_LMUL THEN
431 REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
432 MATCH_MP_TAC REAL_LT_LMUL THEN
437 let DELTA_X4_MONO_LE_4 = prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 <= x1
438 ==> delta_x4 x1 x2 x3 b x5 x6 <=
439 delta_x4 x1 x2 x3 a x5 x6`,
440 REPEAT STRIP_TAC THEN
441 MP_TAC (REAL_ARITH `&0 <= x1 ==> x1 = &0 \/ &0 < x1`) THEN
442 ASM_REWRITE_TAC[] THEN
445 ASM_REWRITE_TAC[Sphere.delta_x4] THEN
447 MATCH_MP_TAC REAL_LT_IMP_LE THEN
448 ASM_SIMP_TAC[DELTA_X4_MONO_LT_4]
453 let REAL_LT_SQUARE_POS = prove(`!x y. &0 < x /\ x < y ==> x pow 2 < y pow 2`,
454 REPEAT STRIP_TAC THEN
455 REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
456 SUBGOAL_THEN `abs x = x` ASSUME_TAC THENL
458 ASM_SIMP_TAC[REAL_ABS_REFL; REAL_LT_IMP_LE];
461 SUBGOAL_THEN `abs y = y` ASSUME_TAC THENL
463 ASM_REWRITE_TAC[REAL_ABS_REFL] THEN
464 MATCH_MP_TAC REAL_LT_IMP_LE THEN
465 MATCH_MP_TAC REAL_LT_TRANS THEN
466 EXISTS_TAC `x:real` THEN
474 let ATN2_ACS_LEMMA = prove(`!a b. b * b < a ==>
475 pi / &2 + atn2(sqrt(a - b*b), --b) = acs(b/sqrt(a))`,
476 REPEAT STRIP_TAC THEN
477 SUBGOAL_THEN `&0 < a` ASSUME_TAC THENL
479 MATCH_MP_TAC REAL_LET_TRANS THEN
480 EXISTS_TAC `b*b:real` THEN
481 ASM_REWRITE_TAC[REAL_LE_SQUARE];
485 MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
487 SUBGOAL_THEN `sqrt a pow 2 = a` ASSUME_TAC THENL
489 ASM_REWRITE_TAC[SQRT_POW2];
493 SUBGOAL_THEN `atn2 (sqrt(a - b*b),--b) = --atn2(sqrt(a-b*b),b)` MP_TAC THENL
495 MATCH_MP_TAC Trigonometry1.ATN2_RNEG THEN
497 MATCH_MP_TAC SQRT_POS_LT THEN
498 ASM_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`];
502 DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ARITH `a + --b = a - b`]) THEN
503 SUBGOAL_THEN `atn2(sqrt(a - b*b), b) = atn2(sqrt(&1 - (b/sqrt a) pow 2),b/sqrt a)` MP_TAC THENL
505 MP_TAC (SPECL [`sqrt(&1 - (b/sqrt a) pow 2)`; `sqrt a`; `b/sqrt a`] (GEN_ALL Trigonometry2.POS_COMPATIBLE_WITH_ATN2)) THEN
506 SUBGOAL_THEN `&0 < sqrt a` ASSUME_TAC THENL
508 MATCH_MP_TAC SQRT_POS_LT THEN
512 ASM_REWRITE_TAC[] THEN
513 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
514 ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * b / a = b`] THEN
516 SUBGOAL_THEN `a - b*b = (sqrt a) pow 2 * (&1 - (b/sqrt a) pow 2)` MP_TAC THENL
518 ASM_REWRITE_TAC[REAL_POW_DIV] THEN
519 ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * (&1 - b/a) = a - b`] THEN
520 REWRITE_TAC[REAL_POW_2];
524 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
525 MP_TAC (SPECL [`sqrt a pow 2`; `&1 - (b/sqrt a) pow 2`] SQRT_MUL) THEN
528 ASM_REWRITE_TAC[REAL_POW_DIV] THEN
529 REWRITE_TAC[REAL_ARITH `&0 <= &1 - b <=> b <= &1`] THEN
530 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
531 ASM_SIMP_TAC[REAL_POW_2; REAL_ARITH `b < a ==> b <= a`];
535 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
540 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
541 MATCH_MP_TAC (GSYM Trigonometry2.acs_atn2) THEN
542 REWRITE_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 <=> abs x <= &1`] THEN
543 ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
544 REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
545 REWRITE_TAC[REAL_POW_DIV] THEN
546 ASM_REWRITE_TAC[REAL_POW_2; REAL_ARITH `&1 * &1 = &1`] THEN
547 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
548 ASM_SIMP_TAC[REAL_ARITH `b < a ==> b <= a`]);;
552 let DELTA_X_AND_DELTA_X4 = prove(`!x1 x2 x3 x4 x5 x6.
553 (let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
554 let d = delta_x x1 x2 x3 x4 x5 x6 in
555 let v1 = ups_x x1 x2 x6 in
556 let v2 = ups_x x1 x3 x5 in
557 &4 * x1 * d = v1 * v2 - d4 * d4)`,
559 REPEAT (CONV_TAC let_CONV) THEN
560 REWRITE_TAC[Sphere.delta_x4; Sphere.delta_x; Sphere.ups_x] THEN
564 let DELTA_EQ_DELTA_X = prove(`!x1 x2 x3 x4 x5 x6.
565 delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6`,
567 REWRITE_TAC[Sphere.delta_x; Collect_geom.delta] THEN
574 let DIH_X_MONO_LT_4 = prove(`!x1 x2 x3 a x5 x6 b. a < b /\
576 &0 < delta_x x1 x2 x3 a x5 x6 /\
577 &0 < delta_x x1 x2 x3 b x5 x6
578 ==> dih_x x1 x2 x3 a x5 x6 < dih_x x1 x2 x3 b x5 x6`,
579 REPEAT STRIP_TAC THEN
580 REWRITE_TAC[let_RULE Sphere.dih_x] THEN
581 ABBREV_TAC `da = delta_x x1 x2 x3 a x5 x6` THEN
582 ABBREV_TAC `db = delta_x x1 x2 x3 b x5 x6` THEN
583 SUBGOAL_THEN `&0 < &4 * x1 * da /\ &0 < &4 * x1 * db` MP_TAC THENL
586 MATCH_MP_TAC REAL_LT_MUL THEN
587 REWRITE_TAC[REAL_ARITH `&0 < &4`] THEN
588 MATCH_MP_TAC REAL_LT_MUL THEN
593 EXPAND_TAC "da" THEN EXPAND_TAC "db" THEN
594 REWRITE_TAC[let_RULE DELTA_X_AND_DELTA_X4] THEN
595 REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN
596 ABBREV_TAC `d4a = delta_x4 x1 x2 x3 a x5 x6` THEN
597 ABBREV_TAC `d4b = delta_x4 x1 x2 x3 b x5 x6` THEN
598 ABBREV_TAC `v1 = ups_x x1 x2 x6` THEN
599 ABBREV_TAC `v2 = ups_x x1 x3 x5` THEN
602 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP ATN2_ACS_LEMMA th)) THEN
603 POP_ASSUM MP_TAC THEN
604 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP ATN2_ACS_LEMMA th)) THEN
605 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
607 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
609 MATCH_MP_TAC ACS_MONO_LT THEN
610 SUBGOAL_THEN `!a b. b * b < a ==> -- &1 <= b / sqrt(a) /\ b / sqrt a <= &1` ASSUME_TAC THENL
612 REPEAT GEN_TAC THEN DISCH_TAC THEN
613 REWRITE_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 <=> abs x <= &1`] THEN
614 ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
615 REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
616 REWRITE_TAC[REAL_POW_DIV] THEN
618 SUBGOAL_THEN `&0 < a'` ASSUME_TAC THENL
620 MATCH_MP_TAC REAL_LET_TRANS THEN
621 EXISTS_TAC `b' * b':real` THEN
622 ASM_SIMP_TAC[REAL_LE_SQUARE; REAL_ARITH `b < a ==> b <= a`];
626 SUBGOAL_THEN `sqrt a' pow 2 = a'` (fun th -> REWRITE_TAC[th]) THENL
628 REWRITE_TAC[SQRT_POW2] THEN
629 ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`];
633 ASM_REWRITE_TAC[REAL_POW_2; REAL_ARITH `&1 * &1 = &1`] THEN
634 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
635 ASM_SIMP_TAC[REAL_ARITH `b < a ==> b <= a`];
639 POP_ASSUM (fun th -> ASM_SIMP_TAC[th]) THEN
640 REWRITE_TAC[real_div] THEN
641 MATCH_MP_TAC REAL_LT_RMUL THEN
642 REWRITE_TAC[REAL_LT_INV_EQ] THEN
645 MP_TAC (SPEC_ALL DELTA_X4_MONO_LT_4) THEN
647 MATCH_MP_TAC SQRT_POS_LT THEN
648 MATCH_MP_TAC REAL_LET_TRANS THEN
649 EXISTS_TAC `d4a * d4a:real` THEN
650 ASM_REWRITE_TAC[REAL_LE_SQUARE]
658 let DIH_Y_INEQ_concl = mk_imp ((hd (Ineq.getexact "2570626711")).ineq,
659 `ineq [(#2.0,y1,#2.52);
665 (dih_y y1 y2 y3 y4 y5 y6 > #1.15 \/ delta_y y1 y2 y3 y4 y5 y6 <= &0)`);;
668 g(DIH_Y_INEQ_concl);;
669 let DIH_Y_INEQ = prove(DIH_Y_INEQ_concl,
670 REWRITE_TAC[Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
671 REWRITE_TAC[INEQ_ALT; ALL] THEN
672 REPEAT STRIP_TAC THEN
673 DISJ_CASES_TAC (REAL_ARITH `delta_y y1 y2 y3 y4 y5 y6 <= &0 \/ delta_y y1 y2 y3 y4 y5 y6 > &0`) THENL
679 REWRITE_TAC[real_gt] THEN
680 MATCH_MP_TAC REAL_LTE_TRANS THEN
681 EXISTS_TAC `dih_y y1 y2 y3 #2.52 y5 y6` THEN
682 FIRST_X_ASSUM (MP_TAC o SPECL [`y1:real`; `y2:real`; `y3:real`; `#2.52`; `y5:real`; `y6:real`]) THEN
683 ASM_SIMP_TAC[REAL_LE_REFL; real_gt] THEN
684 DISCH_THEN (fun th -> ALL_TAC) THEN
685 POP_ASSUM MP_TAC THEN
687 REWRITE_TAC[let_RULE Sphere.dih_y; Sphere.delta_y] THEN
688 MAP_EVERY ABBREV_TAC [`x1 = y1 * y1`; `x2 = y2 * y2`; `x3 = y3 * y3`; `x4 = y4 * y4`; `x5 = y5 * y5`; `x6 = y6 * y6`] THEN
689 REWRITE_TAC[REAL_ARITH `a <= b <=> a < b \/ a = b`] THEN
690 ASM_CASES_TAC `dih_x x1 x2 x3 (#2.52 * #2.52) x5 x6 = dih_x x1 x2 x3 x4 x5 x6` THEN ASM_REWRITE_TAC[] THEN
691 REWRITE_TAC[real_gt] THEN
693 MATCH_MP_TAC DIH_X_MONO_LT_4 THEN
694 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
696 SUBGOAL_THEN `!y. #2.0 <= y /\ y <= #2.52 ==> #4.0 <= y * y /\ y * y <= #6.3504` ASSUME_TAC THENL
698 GEN_TAC THEN REWRITE_TAC[REAL_ARITH `#4.0 = #2.0 * #2.0`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
699 REWRITE_TAC[GSYM REAL_POW_2] THEN
700 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
705 SUBGOAL_THEN `#2.52 * #2.52 < x4` (fun th -> REWRITE_TAC[th]) THENL
708 REWRITE_TAC[GSYM REAL_POW_2] THEN
709 MATCH_MP_TAC REAL_LT_SQUARE_POS THEN
710 ASM_REWRITE_TAC[REAL_ARITH `&0 < #2.52`; REAL_ARITH `a < b <=> a <= b /\ ~(a = b)`] THEN
711 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
712 REWRITE_TAC[CONTRAPOS_THM] THEN
714 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]);
718 MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`y1:real`; `y2:real`; `y3:real`; `y5:real`; `y6:real`] THEN
719 REMOVE_ASSUM THEN REMOVE_ASSUM THEN
720 REPLICATE_TAC 6 (POP_ASSUM (fun th -> REWRITE_TAC[th])) THEN
721 ASM_REWRITE_TAC[] THEN
722 REPEAT REMOVE_ASSUM THEN REPEAT DISCH_TAC THEN
723 ASM_SIMP_TAC[REAL_ARITH `#4.0 <= x1 ==> &0 < x1`] THEN
724 MATCH_MP_TAC REAL_LTE_TRANS THEN
725 EXISTS_TAC `#128.0` THEN
726 REWRITE_TAC[REAL_ARITH `&0 < #128.0`; GSYM real_ge] THEN
728 MP_TAC delta_x_pos THEN
729 REWRITE_TAC[INEQ_ALT; ALL] THEN
730 DISCH_THEN MATCH_MP_TAC THEN
731 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;