text_formalization/trigonometry/trigonometry.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Trigonometry                                               *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11
  12 (* summary of the trig chapter *)
  13
  14
  15
  16
  17 (*
  18
  19 Known issues:
  20
  21 -- Flypaper defines sin and cos by their power series. HOL Light defines them
  22 through complex analysis.
  23
  24 -- NUHSVLM: 5 points in R3 ==> cayleyR = 0, moved to collect_geom2.ml. Slow to run.
  25      I will keep it out of the daily build.
  26
  27 -- Some results (marked LEG) may have been formalized but not imported from legacy directory.
  28 Lemmas in Elementary Geometry.  Now in leg/ directory.
  29
  30 -- some minor results that haven't been done or located are marked UNKNOWN  below
  31
  32 -- polar_cycle deprecated 2011-08-01.
  33
  34 *)
  35
  36
  37 module type Trigonometry_type = sig
  38
  39 end;;
  40
  41 flyspeck_needs "general/sphere.hl";;
  42 flyspeck_needs "leg/enclosed_def.hl";;
  43 flyspeck_needs "leg/collect_geom.hl";;
  44 flyspeck_needs "trigonometry/trig1.hl";;
  45 flyspeck_needs "trigonometry/trig2.hl";;
  46
  47
  48 module Trigonometry (* : Trigonometry_type *)  = struct
  49
  50 (*
  51 let LIST_MK_CONJ b = match b with
  52    [] -> TRUTH
  53   |b::bs as a-> let g = itlist (curry mk_conj) (map concl bs) (concl b) in prove(g,REWRITE_TAC a);;
  54 *)
  55   let LIST_MK_CONJ (b:thm list) = b;;
  56
  57 let UNKNOWN = REWRITE_RULE[TRUTH] (new_definition `unknown = T`);;
  58
  59  let elimin  = REWRITE_RULE[IN];;
  60
  61 let FOYTTIX1 = cos;;
  62 let FOYTTIX2 = sin;;
  63 let FOYTTIX=LIST_MK_CONJ [FOYTTIX1;FOYTTIX2];;
  64
  65 let YIXJNJQ1 = SIN_0;;
  66 let YIXJNJQ2 = COS_0;;
  67 let YIXJNJQ = LIST_MK_CONJ [YIXJNJQ1;YIXJNJQ2];;
  68
  69 let WPMXVYZ = SIN_CIRCLE;;
  70
  71 let WNYVJPE1 = SIN_ADD;;
  72 let WNYVJPE2 = COS_ADD;;
  73 let WNYVJPE = LIST_MK_CONJ [WNYVJPE1;WNYVJPE2];;
  74
  75 let KGLLRQT1 = COS_NEG;;
  76 let KGLLRQT2 = SIN_NEG;;
  77 let KGLLRQT = LIST_MK_CONJ [KGLLRQT1;KGLLRQT2];;
  78
  79 (* cos(pi/2) = 0 *)
  80 let CFXEKKP1 =  COS_PI2;;
  81 let CFXEKKP2 =  COS_POS_PI2;;
  82
  83 (* This is combined between two lemmas *)
  84 let ZSKECZV = COS_POS_PI_LE;;
  85
  86 (* Lemma label{lemma:sin-pi2} *)
  87 let CPIREMF1 = SIN_PI2;;
  88 let CPIREMF2 = SIN_POS_PI_LE;;
  89 let CPIREMF = LIST_MK_CONJ [CPIREMF1;CPIREMF2];;
  90
  91 (* Lemma label{lemma:cos-sin} *)
  92 let SCEZKRH1 = GSYM COS_SIN;;
  93 let SCEZKRH2 = GSYM SIN_COS;;
  94
  95 let SCEZKRH = LIST_MK_CONJ [SCEZKRH1;SCEZKRH2];;
  96
  97 let WIBGJRR = SIN_POS_PI_LE;;
  98
  99 let LLOYXRK1 = prove(`!x. cos(pi/ &2 + x) = -- (sin x)`,
 100    REWRITE_TAC[REAL_ARITH `x + y = x - (-- y)`;GSYM SIN_COS;SIN_NEG]);;
 101 let LLOYXRK2 = prove(`!x. sin(pi/ &2 + x) = cos x`,
 102    REWRITE_TAC[REAL_ARITH `x + y = x - (-- y)`;GSYM COS_SIN;COS_NEG]);;
 103 let LLOYXRK3 = SIN_PERIODIC_PI;;
 104 let LLOYXRK4 = COS_PERIODIC_PI;;
 105 let LLOYXRK5 = SIN_PERIODIC;;
 106 let LLOYXRK6 = COS_PERIODIC;;
 107 let LLOYXRK = LIST_MK_CONJ [LLOYXRK1;LLOYXRK2;LLOYXRK3;LLOYXRK4;LLOYXRK5;LLOYXRK6];;
 108
 109 (* sin non-negative *)
 110 let WIBGJRR = SIN_POS_PI_LE;;
 111
 112 (* definition label{def:tan} *)
 113  let BIRXGXP = tan ;;
 114
 115 (* Lemma label{lemma:tan-add} *)
 116 let KWYPRWZ = TAN_ADD;;
 117
 118 (* Lemma label{lemma:tan-pi4} *)
 119 let KSQDZSF = TAN_PI4;;
 120
 121 (* tan increasing and one-to-one *)
 122 let UTNKIAC = TAN_MONO_LT;;
 123
 124 let RIQVMHH1 = atn;;
 125 let RIQVMHH2 =  ATN_BOUNDS ;;
 126 let RIQVMHH=LIST_MK_CONJ [RIQVMHH1;RIQVMHH2];;
 127
 128
 129 let EWITKLU  = ATN_TAN ;;
 130
 131 let YTXYLRB = ATN_1 ;;
 132
 133 let OKENMAM= HAS_REAL_DERIVATIVE_ATN;;
 134
 135
 136 let LQCXGZX = ATN_MONO_LT_EQ ;;
 137
 138 (* atan2 *)
 139 let GYKGARD = Sphere.atn2;;
 140 let QZTBJMH1 = acs;;
 141 let QZTBJMH2 = COS_ACS;;
 142 let QZTBJMH3 = ACS_COS;;
 143 let QZTBJMH = LIST_MK_CONJ [ QZTBJMH1; QZTBJMH2; QZTBJMH3];;
 144 let FMGMALU = SIN_ACS;;
 145 let OUIJTWY = Trigonometry2.acs_atn2 ;;
 146 (* let asn = asn;; *)
 147
 148
 149 (* VECTOR GEOMETRY *)
 150
 151 let KRZJIAD = (`:real^N`,`v$i`,`vec 0`);;
 152
 153 let WHIAXYD1 =  [`(x:real^3) + (y:real^3)`;`(x:real^3) - (x:real^3)`;
 154   `-- (x:real^3)`;`t % (x:real^3)`];;
 155 let WHIAXYD2 = VECTOR_ADD_ASSOC;;
 156 let WHIAXYD3 = VECTOR_ADD_SYM;;
 157 let WHIAXYD = ( WHIAXYD1, WHIAXYD2, WHIAXYD3);;
 158
 159
 160 let VFPCZBI =  [`(x:real^3) dot (y:real^3)`];;
 161
 162 let XHVXJVB = vector_norm;;
 163
 164
 165 (*CAUCHY SCHWARZ Lemma label{} *)
 166 let JJKJALK = NORM_CAUCHY_SCHWARZ ;;
 167
 168
 169 (*TRIANGLE INEQ  Lemma label{} *)
 170 let OIPLPTM1 = NORM_TRIANGLE ;;
 171 let OIPLPTM2 = NORM_TRIANGLE_EQ ;;
 172 let OIPLPTM = LIST_MK_CONJ [OIPLPTM1;OIPLPTM2];;
 173
 174 (* AFFINE GEOMETRY *)
 175
 176 let KVLZSAQ1 = AFFINE;;
 177 let KVLZSAQ2 = Sphere.aff;;  (* deprecated *)
 178 let KVLZSAQ = LIST_MK_CONJ [KVLZSAQ1;KVLZSAQ2];;
 179
 180 (* see also affsign;; lin_combo;; *)
 181
 182 let BYFLKYM1 = Sphere.aff;;
 183 let BYFLKYM2 = Sphere.aff_ge_def;;
 184 let BYFLKYM3 = Sphere.aff_gt_def;;
 185 let BYFLKYM4 = Sphere.aff_lt_def;;
 186 let BYFLKYM5 = Sphere.aff_le_def;;
 187 let BYFLKYM = LIST_MK_CONJ [BYFLKYM1;BYFLKYM2;BYFLKYM3;BYFLKYM4;BYFLKYM5];;
 188
 189 let OWECYNV1 = convex;;
 190 let OWECYNV2 = `(hull) convex`;;
 191 let OWECYNV = (OWECYNV1,OWECYNV2);;
 192
 193 let GDCZMLO = CONVEX_HULL_AFF_GE;;
 194
 195 let UIVNNRR1 = prove(
 196   `!V. (aff_ge V EMPTY = aff_gt V EMPTY)`,
 197   REWRITE_TAC[aff_ge_def;aff_gt_def;affsign]  THEN
 198   STRIP_TAC THEN
 199   ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
 200   REWRITE_TAC[affsign;elimin NOT_IN_EMPTY]
 201 );;
 202
 203 let UIVNNRR2 = AFF_GT_EQ_AFFINE_HULL;;
 204 let UIVNNRR = LIST_MK_CONJ [UIVNNRR1;UIVNNRR2];;
 205
 206 let LLOUBAX = cone ;;
 207 let SWKFLBJ1 = Sphere.line ;;
 208 let SWKFLBJ2 = collinear ;;
 209 let parallel = define `parallel (v:real^N) w = collinear {(vec 0),v,w}`;;
 210 let SWKFLBJ3 = parallel;;
 211 let  SWKFLBJ = LIST_MK_CONJ [ SWKFLBJ1; SWKFLBJ2; SWKFLBJ3];;
 212
 213 let JLWZFBH1 = plane ;;
 214 let JLWZFBH2 = Sphere.closed_half_plane;;
 215 let JLWZFBH3 = Sphere.open_half_plane;;
 216 let  JLWZFBH4  = coplanar ;;
 217 let JLWZFBH = LIST_MK_CONJ [JLWZFBH1;JLWZFBH2;JLWZFBH3;JLWZFBH4];;
 218
 219 let OAUVFPS1 = Sphere.closed_half_space ;;
 220 let OAUVFPS2 = Sphere.open_half_space ;;
 221 let OAUVFPS = LIST_MK_CONJ [OAUVFPS1;OAUVFPS2];;
 222
 223 let AVWKGNB = delta_x;;
 224
 225 let LBEVAKV = Collect_geom.DELTA_POS_4POINTS;;
 226 let CTCZHMR = LIST_MK_CONJ [LBEVAKV;Collect_geom.POLFLZY];; (* Delta pos LEG [line 2690;line 3010], *)
 227
 228
 229 let KZVHHBG = LIST_MK_CONJ [Collect_geom.LTCTBAN;Collect_geom.GJWYYPS;Collect_geom.GDLRUZB];;
 230
 231 let NUHSVLM = UNKNOWN;; (* " implemented in collect_geom2.hl" ;;  *)
 232
 233 (* CayleyR results: lines from legacy/collect_geom.ml LEG:
 234 2337/LTCTBAN: ups is leading coeff of quadratic cayleyR
 235 2725/GJWYYPS: discriminant of cayleyR
 236 2894/GDLRUZB: disc(cayleyR)=0 <=> one of tetra are coplanar
 237 3010/NUHSVLM: 5 points in R3 ==> cayleyR = 0
 238
 239 RPFVZDI:  enclosed function defined
 240 *)
 241
 242 let RPFVZDI = Enclosed.enclosed;; (* "implemented in enclosed_def.hl ";; *)
 243
 244
 245 let WZYUXVC = arcV ;;
 246
 247 let ACNBFRL = UNKNOWN ;; (* arcV atn2 *)
 248
 249 let PQQDENV = Trigonometry1.ACS_ARCLENGTH;;
 250
 251 let HQTBPCM1 = LAW_OF_COSINES ;;
 252 let HQTBPCM2 = Trigonometry1.DIST_LAW_OF_COS ;;
 253 let HQTBPCM = LIST_MK_CONJ [HQTBPCM1;HQTBPCM2];;
 254
 255
 256 let OBPIOXD = Sphere.ups_x;; (* upsilon def *)
 257 let QRAAWFS = LIST_MK_CONJ [Trigonometry2.UPS_X_POS;Collect_geom.FHFMKIY];;
 258 let IHIQXLM = Trigonometry1.UPS_X_SQUARES;; (* upsilon factors *)
 259
 260 let UKBAHKV = Trigonometry1.VECTOR_LAW_OF_SINES ;; (* slightly different from book *)
 261
 262 let GVWTZKY = UNKNOWN;; (* arc, atn2 *)
 263
 264
 265 (* cross product something *)
 266 let FCUAGA = cross;;
 267 let KVVWPNA = NORM_CROSS ;; (* norm cross and ups, combine with UKBAHKV *)
 268
 269 (* Lemma label{} *)
 270 (* cross product order and distribution with dot product *)
 271 let BKMUSOX1 = CROSS_SKEW ;;
 272 let BKMUSOX2 = CROSS_TRIPLE ;;
 273 let  BKMUSOX = LIST_MK_CONJ [ BKMUSOX1; BKMUSOX2];;
 274
 275 (* Definition label{def:dih} *)
 276 let dihV = dihV ;;
 277
 278 let RLXWSTK = Trigonometry2.RLXWSTK;;
 279
 280 let NLVWBBW = Trigonometry2.NLVWBBW;;
 281
 282 let OJEKOJF = Trigonometry2.OJEKOJF;;
 283
 284 let JLPSDHF = Euler_main_theorem.EULER_TRIANGLE;; (* euler_triangle ;; *)
 285
 286
 287 let KEITDWB = Trigonometry2.ARCV_INEQUALTY ;;
 288 let FGNMPAV = Trigonometry2.FGNMPAV ;;
 289
 290 let FEVNANL = LIST_MK_CONJ [Trigonometry1.atn2_spec;Trigonometry1.ATAN2_EXISTS];;
 291
 292 let AXBTGQX = orthonormal;;  (* much more has been proved about orthonormal vectors *)
 293
 294 let QAUQIEC = UNKNOWN;; (* "not found, adapted orthonormization ";; *)
 295
 296 let EYFCXPP = [Trigonometry2.EYFCXPP;(* see also CYLINDER_CORDINATE *)
 297                Trigonometry2.CYLINDER_CORDINATE];;
 298
 299 let azim = azim ;;
 300
 301 let QQZKTXU = Trigonometry2.QQZKTXU;;
 302 let JBDNJJB = Trigonometry2.JBDNJJB;;
 303
 304 (* zenith angle *)
 305
 306 let QAFHJNM =Trigonometry2.QAFHJNM;;
 307 let XPHCPNY = SPHERICAL_COORDINATES ;;
 308
 309 (* Cycle *)
 310
 311 (* DEPRECATED 2011-08-01. let TNZQDCX = Sphere.polar_cycle;; *)
 312
 313 let PDPFQUK = Trigonometry2.PDPFQUK;;
 314 let ISRTTNZ = Trigonometry2.ISRTTNZ;;
 315 let KFKHLWK = Trigonometry2.cyclic_set;;
 316 let YESEEWW = Sphere.azim_cycle;;
 317 let NLOFMTR = UNKNOWN;; (* "not found, of doubtful use";; *)
 318 let YVREJIS =  Trigonometry2.YVREJIS;;
 319 let ULEKUUB = UNKNOWN;; (* "not found, fan version given as Topology.ULEKUUB";; *)
 320
 321 (* spherical triangle inequality *)
 322
 323 let KEITDWB = Trigonometry2.KEITDWB;;
 324 let FGNMPAV = Trigonometry2.FGNMPAV;;
 325
 326
 327 end;;
 328