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]);;