Update from HH
[Flyspeck/.git] / legacy / oldlocal / nguyenquangtruong270983 / JBDNJJB.hl
1                                                                                                                                                                                                                                                                
2 (*
3 JBDNJJB
4
5 This is code that Nguyen Quang Truong sent me purporting to be a proof of JBDNJJB.
6 However, it seems to be buggy. --Thales
7
8 Here is the proof of this lemma.  It should be loaded after loading
9 sphere.hl and trg2.ml.
10 *)
11
12 parse_as_infix("re_eqvl",(12,"right"));;
13
14 let re_eqvl = new_definition ` a re_eqvl (b:real)
15  <=> (? t. &0 < t /\ a = t * b )`;;
16
17
18
19
20 let VEC_DIV_MOV = prove(
21 ` ~( a = &0 ) ==> (( b / a ) % x = y <=>
22 b % x = a % y ) `,
23 SIMP_TAC[MESON[VECTOR_MUL_LCANCEL]` ~( a = &0 ) ==>
24 (( b / a ) % x = y <=> a % ( b / a) % x = a % y ) `;
25 VECTOR_MUL_ASSOC; REAL_DIV_LMUL]);;
26
27
28 g `sin ( azim ( vec 0 ) u v w ) re_eqvl (u cross v ) dot w `;;
29 e (ASM_CASES_TAC `(u:real^3) = vec 0 ` THENL [
30
31 ASM_SIMP_TAC[AZIM_DEGENERATE; CROSS_0; DOT_LZERO;
32 SIN_0; re_eqvl] THEN EXISTS_TAC `&1` THEN REAL_ARITH_TAC;
33
34
35 ASM_CASES_TAC` collinear {vec 0, u, (v:real^3)}`]
36
37 THENL [
38
39
40 FIRST_X_ASSUM MP_TAC THEN ASM_SIMP_TAC[GSYM CROSS_EQ_0] THEN
41 REWRITE_TAC[CROSS_EQ_0] THEN
42 ASM_SIMP_TAC[AZIM_DEGENERATE; CROSS_0; DOT_LZERO;
43 SIN_0; re_eqvl] THEN
44 DISCH_TAC THEN
45 EXISTS_TAC `&1 ` THEN
46 REAL_ARITH_TAC;
47
48 ASM_CASES_TAC` collinear {vec 0, u, (w:real^3)}`] THENL [
49
50 FIRST_X_ASSUM MP_TAC THEN ASM_SIMP_TAC[GSYM CROSS_EQ_0] THEN
51 REWRITE_TAC[CROSS_EQ_0] THEN
52 ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE] THEN
53 ONCE_REWRITE_TAC[SET_RULE[]` {a,b} = {b,a}`] THEN
54 ASM_SIMP_TAC[AZIM_DEGENERATE;GSYM CROSS_EQ_0] THEN
55 ASM_SIMP_TAC[CROSS_EQ_0] THEN
56 ASM_SIMP_TAC[AZIM_DEGENERATE; CROSS_0; DOT_LZERO;
57 SIN_0; re_eqvl; SET_RULE[]` {a,b} = {b,a}`] THEN
58 DISCH_TAC THEN
59 EXISTS_TAC `&1 ` THEN
60 REAL_ARITH_TAC;
61 ABBREV_TAC ` e3 = &1 / norm (u:real^3) % u ` THEN
62 ABBREV_TAC `v' = v - (e3 dot v) % (e3:real^3) ` THEN
63 ABBREV_TAC `(e1:real^3) = &1 / norm (v') % v' ` THEN
64 ABBREV_TAC ` e2 = e3 cross e1 ` THEN
65 SUBGOAL_THEN `orthonormal e1 e2 e3 ` ASSUME_TAC]
66
67
68
69
70
71
72
73
74
75
76
77
78 THENL [
79 REWRITE_TAC[orthonormal] THEN
80 EXPAND_TAC "e2" THEN
81 REWRITE_TAC[DOT_CROSS_SELF; DOT_CROSS] THEN
82 SUBGOAL_THEN `~((v':real^3) = vec 0)` ASSUME_TAC THENL [
83
84
85 EXPAND_TAC "v'" THEN
86 EXPAND_TAC "e3" THEN
87 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
88 ASSUME_TAC2 (ISPECL [`u:real^3 `;` v:real^3 `]
89  NOT_EQ_VEC0_IMP_EQU_AFF_COLL) THEN
90 UNDISCH_TAC `~ collinear {vec 0, u, (v:real^3)}` THEN
91 FIRST_X_ASSUM MP_TAC THEN
92 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
93 SIMP_TAC[] THEN
94 DISCH_TAC THEN
95 REWRITE_TAC[AFF2_VEC0; IN_ELIM_THM; VECTOR_ARITH` vec 0 =
96 x - y <=> x = y `] THEN
97 MESON_TAC[];
98
99
100 SUBGOAL_THEN `e3 dot (e3:real^3) = &1 /\ e1 dot (e1:real^3)
101 = &1 ` ASSUME_TAC] THENL [
102
103 EXPAND_TAC "e3" THEN
104 EXPAND_TAC "e1" THEN
105 REWRITE_TAC[DOT_LMUL; DOT_RMUL; GSYM NORM_POW_2] THEN
106 UNDISCH_TAC `~((u:real^3) = vec 0 ) ` THEN
107 UNDISCH_TAC `~((v':real^3) = vec 0) ` THEN
108 REWRITE_TAC[GSYM NORM_EQ_0] THEN
109 PHA THEN CONV_TAC REAL_FIELD;
110
111
112
113 SUBGOAL_THEN `e1 dot (e3: real^3) = &0 ` ASSUME_TAC] THENL [
114
115
116 EXPAND_TAC "e1" THEN
117 EXPAND_TAC "v'" THEN
118 REWRITE_TAC[DOT_LSUB; DOT_LMUL; REAL_MUL_RID] THEN
119 ASM_SIMP_TAC[REAL_MUL_RID; DOT_SYM; REAL_SUB_REFL;
120 REAL_MUL_RZERO];
121
122
123
124 ASM_SIMP_TAC[DOT_SYM] THEN
125 ONCE_REWRITE_TAC[DOT_SYM] THEN
126 ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE] THEN
127 EXPAND_TAC "e2" THEN
128 REWRITE_TAC[DOT_CROSS] THEN
129 ASM_SIMP_TAC[DOT_SYM] THEN
130 REAL_ARITH_TAC];
131
132 MP_TAC (let ddd = (let dd = SPEC_ALL (SPECL [`v: real^3 `;` vec 0 : real^3
133 `;`u:real^3 `;
134 `w:real^3 `] SPHERICAL_COORDINATES) in SPEC `dist(vec 0, w:real^3 )`
135 (GEN `r:real` dd)) in
136 SPEC ` azim ( vec 0 ) u v w ` (GEN `theta: real`
137 (SPEC `arcV ( vec 0) w (u:real^3) ` (GEN `phi: real` ddd)))) THEN
138 ANTS_TAC]);;
139
140
141
142
143
144 e (ASM_REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
145 EXPAND_TAC "e3" THEN
146 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
147 UNDISCH_TAC `~((u:real^3) = vec 0 ) ` THEN
148 SIMP_TAC[GSYM NORM_EQ_0; REAL_FIELD` ~( x = &0) ==>
149 x * &1 / x = &1 `; VECTOR_MUL_LID] THEN
150 SUBGOAL_THEN `DISJOINT {vec 0, u} {v:real^3 }` ASSUME_TAC
151
152
153 THENL [
154
155
156
157 REWRITE_TAC[DISJOINT; SET_RULE[]` {a,b} INTER {c} = {}
158 <=> ~( c = a ) /\ ~( c = b ) `] THEN
159 (let drt = STRIP_TAC THEN
160 UNDISCH_TAC `~ collinear { vec 0, u, (v:real^3)} ` THEN
161 ASM_SIMP_TAC[INSERT_AC; COLLINEAR_2] in CONJ_TAC THENL [drt;
162 drt]);
163
164
165 FIRST_X_ASSUM MP_TAC THEN
166 NHANH AFF_GT_2_1 THEN
167 PHA THEN SIMP_TAC[] THEN
168 STRIP_TAC THEN
169 REWRITE_TAC[IN_ELIM_THM] THEN
170 EXPAND_TAC "e1" THEN
171 EXPAND_TAC "v'" THEN
172 SIMP_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID;
173 VECTOR_SUB_LDISTRIB] THEN
174 SUBGOAL_THEN `~( v - (e3 dot v) % (e3:real^3)
175 = vec 0) ` ASSUME_TAC] THENL [
176
177
178
179 EXPAND_TAC "e3" THEN
180 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
181 UNDISCH_TAC `~ collinear {vec 0, u, (v:real^3)}` THEN
182 FIRST_X_ASSUM MP_TAC THEN
183 REWRITE_TAC[NORM_EQ_0] THEN
184 PAT_ONCE_REWRITE_TAC `\x. x ==> _ ` [EQ_SYM_EQ] THEN
185 NHANH (GSYM (ISPECL [`u:real^3 `;` v:real^3 `]
186 NOT_EQ_VEC0_IMP_EQU_AFF_COLL)) THEN
187 SIMP_TAC[] THEN DISCH_TAC THEN
188 REWRITE_TAC[AFF2_VEC0; IN_ELIM_THM; VECTOR_SUB_EQ] THEN
189 MESON_TAC[];
190
191
192 ABBREV_TAC `r3 = e3 dot (v:real^3 ) ` THEN
193 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
194 ABBREV_TAC `e33 = r3 % (e3: real^3) ` THEN
195 EXPAND_TAC "e3" THEN
196 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
197 EXISTS_TAC ` &1 - &1 / norm ((v:real^3 ) -
198 e33) + (&1 / norm ((v:real^3) - e33) * r3) * &1 / norm (u:real^3) ` THEN
199 EXISTS_TAC `-- (&1 / norm ((v:real^3) - e33) * r3) * &1 / norm (u:real^3)`
200 THEN
201 EXISTS_TAC `&1 / norm ((v:real^3) - e33)` THEN
202 CONJ_TAC THENL [
203
204
205 MATCH_MP_TAC REAL_LT_DIV THEN
206 UNDISCH_TAC `~((v:real^3) - e33 = vec 0) ` THEN
207 REWRITE_TAC[GSYM NORM_POS_LT] THEN
208 SIMP_TAC[] THEN REAL_ARITH_TAC;
209 CONJ_TAC THENL [REAL_ARITH_TAC;
210 CONV_TAC VECTOR_ARITH]]]);;
211
212
213 e (SUBGOAL_THEN `~( v - (e3 dot v) % (e3:real^3)
214 = vec 0) ` ASSUME_TAC);;
215
216
217 e (EXPAND_TAC "e3" THEN
218 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
219 UNDISCH_TAC `~ collinear {vec 0, u, (v:real^3)}` THEN
220 UNDISCH_TAC ` ~( (u:real^3) = vec 0) ` THEN
221 REWRITE_TAC[NORM_EQ_0] THEN
222 PAT_ONCE_REWRITE_TAC `\x. x ==> _ ` [EQ_SYM_EQ] THEN
223 NHANH (GSYM (ISPECL [`u:real^3 `;` v:real^3 `]
224 NOT_EQ_VEC0_IMP_EQU_AFF_COLL)) THEN
225 SIMP_TAC[] THEN DISCH_TAC THEN
226 REWRITE_TAC[AFF2_VEC0; IN_ELIM_THM; VECTOR_SUB_EQ] THEN
227 MESON_TAC[]);;
228
229
230
231 e (SUBST_ALL_TAC (SYM (ISPEC `u:real^3 ` NORM_EQ_0)));;
232 e (ASSUME_TAC2 (ISPECL [`&1 `;` u: real^3 `; ` norm (u:real^3)`
233 ; `e3: real^3`] (GEN_ALL VEC_DIV_MOV)));;
234 e (SUBST_ALL_TAC (ISPEC `u:real^3 ` VECTOR_MUL_LID));;
235 e (FIRST_X_ASSUM SUBST_ALL_TAC);;
236 e (ABBREV_TAC ` azzz = azim (vec 0) u v w `);;
237 e (ABBREV_TAC `arrr = arcV (vec 0) w (u:real^3)`);;
238 e (ABBREV_TAC ` diii = dist( vec 0, (w:real^3))`);;
239
240
241 e (SIMP_TAC[VECTOR_ADD_LID]);;
242 e (DISCH_TAC);;
243 e (ABBREV_TAC `no_u = norm (u:real^3)`);;
244 e (ASM_REWRITE_TAC[]);;
245 e (UNDISCH_TAC ` (v:real^3) - (e3 dot v ) %e3
246 = v' `);;
247 e (ABBREV_TAC ` era = e3 dot (v:real^3) `);;
248 e (REWRITE_TAC[VECTOR_ARITH` a - b = (x:real^N) <=>
249 a = x + b `]);;
250 e (SIMP_TAC[CROSS_RADD; CROSS_RMUL; CROSS_LMUL;
251 CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID]);;
252 e (REWRITE_TAC[VECTOR_ARITH` a = b + (c:real^N) <=>
253 a - c = b `]);;
254 e (DISCH_THEN SUBST_ALL_TAC);;
255 e (UNDISCH_TAC ` &1 / norm v' % (v':real^3) = e1 `);;
256 e (UNDISCH_TAC `~((v':real^3) = vec 0 ) `);;
257 e (SIMP_TAC[GSYM NORM_EQ_0; VEC_DIV_MOV; VECTOR_MUL_LID]);;
258 e (ABBREV_TAC `nov' = norm (v':real^3) `);;
259 e (SIMP_TAC[CROSS_RMUL]);;
260 e (STRIP_TAC);;
261 e (STRIP_TAC);;
262 e (ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; DOT_RADD; DOT_RMUL;
263 DOT_LMUL]);;
264 e (UNDISCH_TAC `orthonormal e1 e2 e3 `);;
265 e (REWRITE_TAC[orthonormal]);;
266 e (SIMP_TAC[DOT_SYM; REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RID]);;
267 e (DISCH_TAC);;
268 e (REWRITE_TAC[REAL_ARITH`(a * b * c ) * (d * e ) * &1
269 = (a * c * d * e ) * b `; re_eqvl]);;
270 e (EXISTS_TAC ` &1 / ( diii * sin arrr * no_u * nov') `);;
271 e (SUBGOAL_THEN ` &0 < diii * sin arrr * no_u * nov' `
272 ASSUME_TAC);;
273 e (MATCH_MP_TAC (
274 MESON[REAL_LT_MUL]` &0 < a /\ &0 < b /\ &0 < c /\ &0 < d
275 ==> &0 < b * a * c * d `));;
276 e (CONJ_TAC);;
277 e (EXPAND_TAC "arrr");;
278 e (UNDISCH_TAC `~ collinear {vec 0, u, (w:real^3)}`);;
279 e (SIMP_TAC[ARC_SYM; NOT_COLL_IM_SIN_LT]);;
280
281
282
283 e (UNDISCH_TAC `~(no_u = &0) `);;
284 e (UNDISCH_TAC ` ~(nov' = &0)`);;
285 e (UNDISCH_TAC `~ collinear {vec 0, u, (w:real^3)}`);;
286 e (NHANH NOT_COLLINEAR_IMP_2_UNEQUAL);;
287 e (STRIP_TAC);;
288 e (FIRST_X_ASSUM MP_TAC);;
289 e (SIMP_TAC[DIST_NZ]);;
290 e (EXPAND_TAC "diii");;
291 e (EXPAND_TAC "no_u");;
292 e (EXPAND_TAC "nov'");;
293 e (DISCH_TAC);;
294 e (PHA THEN CONV_TAC NORM_ARITH);;
295
296
297
298 e (CONJ_TAC);;
299 e (MATCH_MP_TAC REAL_LT_DIV);;
300 e (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
301
302
303 e (FIRST_X_ASSUM MP_TAC);;
304 e (NHANH REAL_POS_NZ);;
305 e (SIMP_TAC[REAL_MUL_ASSOC; NOT_0_INVERTABLE; REAL_MUL_LID]);;