(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Trigonometry *)
(* Author: Thomas C. Hales *)
(* Date: 2010-02-09 *)
(* ========================================================================== *)
(* summary of the trig chapter *)
(*
Known issues:
-- Flypaper defines sin and cos by their power series. HOL Light defines them
through complex analysis.
-- NUHSVLM: 5 points in R3 ==> cayleyR = 0, moved to collect_geom2.ml. Slow to run.
I will keep it out of the daily build.
-- Some results (marked LEG) may have been formalized but not imported from legacy directory.
Lemmas in Elementary Geometry. Now in leg/ directory.
-- some minor results that haven't been done or located are marked UNKNOWN below
-- polar_cycle deprecated 2011-08-01.
*)
module type Trigonometry_type = sig
end;;
flyspeck_needs "general/sphere.hl";;
flyspeck_needs "leg/enclosed_def.hl";;
flyspeck_needs "leg/collect_geom.hl";;
flyspeck_needs "trigonometry/trig1.hl";;
flyspeck_needs "trigonometry/trig2.hl";;
module Trigonometry (* : Trigonometry_type *) = struct
(*
let LIST_MK_CONJ b = match b with
[] -> TRUTH
|b::bs as a-> let g = itlist (curry mk_conj) (map concl bs) (concl b) in prove(g,REWRITE_TAC a);;
*)
let LIST_MK_CONJ (b:thm list) = b;;
let UNKNOWN = REWRITE_RULE[TRUTH] (new_definition `unknown = T`);;
let elimin = REWRITE_RULE[IN];;
let FOYTTIX1 = cos;;
let FOYTTIX2 = sin;;
let FOYTTIX=LIST_MK_CONJ [FOYTTIX1;FOYTTIX2];;
let YIXJNJQ1 = SIN_0;;
let YIXJNJQ2 = COS_0;;
let YIXJNJQ = LIST_MK_CONJ [YIXJNJQ1;YIXJNJQ2];;
let WPMXVYZ = SIN_CIRCLE;;
let WNYVJPE1 = SIN_ADD;;
let WNYVJPE2 = COS_ADD;;
let WNYVJPE = LIST_MK_CONJ [WNYVJPE1;WNYVJPE2];;
let KGLLRQT1 = COS_NEG;;
let KGLLRQT2 = SIN_NEG;;
let KGLLRQT = LIST_MK_CONJ [KGLLRQT1;KGLLRQT2];;
(* cos(pi/2) = 0 *)
let CFXEKKP1 = COS_PI2;;
let CFXEKKP2 = COS_POS_PI2;;
(* This is combined between two lemmas *)
let ZSKECZV = COS_POS_PI_LE;;
(* Lemma label{lemma:sin-pi2} *)
let CPIREMF1 = SIN_PI2;;
let CPIREMF2 = SIN_POS_PI_LE;;
let CPIREMF = LIST_MK_CONJ [CPIREMF1;CPIREMF2];;
(* Lemma label{lemma:cos-sin} *)
let SCEZKRH1 = GSYM COS_SIN;;
let SCEZKRH2 = GSYM SIN_COS;;
let SCEZKRH = LIST_MK_CONJ [SCEZKRH1;SCEZKRH2];;
let WIBGJRR = SIN_POS_PI_LE;;
let LLOYXRK3 = SIN_PERIODIC_PI;;
let LLOYXRK4 = COS_PERIODIC_PI;;
let LLOYXRK5 = SIN_PERIODIC;;
let LLOYXRK6 = COS_PERIODIC;;
let LLOYXRK = LIST_MK_CONJ [LLOYXRK1;LLOYXRK2;LLOYXRK3;LLOYXRK4;LLOYXRK5;LLOYXRK6];;
(* sin non-negative *)
let WIBGJRR = SIN_POS_PI_LE;;
(* definition label{def:tan} *)
let BIRXGXP = tan ;;
(* Lemma label{lemma:tan-add} *)
let KWYPRWZ = TAN_ADD;;
(* Lemma label{lemma:tan-pi4} *)
let KSQDZSF = TAN_PI4;;
(* tan increasing and one-to-one *)
let UTNKIAC = TAN_MONO_LT;;
let RIQVMHH1 = atn;;
let RIQVMHH2 = ATN_BOUNDS ;;
let RIQVMHH=LIST_MK_CONJ [RIQVMHH1;RIQVMHH2];;
let EWITKLU = ATN_TAN ;;
let YTXYLRB = ATN_1 ;;
let OKENMAM= HAS_REAL_DERIVATIVE_ATN;;
let LQCXGZX = ATN_MONO_LT_EQ ;;
(* atan2 *)
let GYKGARD = Sphere.atn2;;
let QZTBJMH1 = acs;;
let QZTBJMH2 = COS_ACS;;
let QZTBJMH3 = ACS_COS;;
let QZTBJMH = LIST_MK_CONJ [ QZTBJMH1; QZTBJMH2; QZTBJMH3];;
let FMGMALU = SIN_ACS;;
let OUIJTWY = Trigonometry2.acs_atn2 ;;
(* let asn = asn;; *)
(* VECTOR GEOMETRY *)
let KRZJIAD = (`:real^N`,`v$i`,`vec 0`);;
let WHIAXYD1 = [`(x:real^3) + (y:real^3)`;`(x:real^3) - (x:real^3)`;
`-- (x:real^3)`;`t % (x:real^3)`];;
let WHIAXYD2 = VECTOR_ADD_ASSOC;;
let WHIAXYD3 = VECTOR_ADD_SYM;;
let WHIAXYD = ( WHIAXYD1, WHIAXYD2, WHIAXYD3);;
let VFPCZBI = [`(x:real^3) dot (y:real^3)`];;
let XHVXJVB = vector_norm;;
(*CAUCHY SCHWARZ Lemma label{} *)
let JJKJALK = NORM_CAUCHY_SCHWARZ ;;
(*TRIANGLE INEQ Lemma label{} *)
let OIPLPTM1 = NORM_TRIANGLE ;;
let OIPLPTM2 = NORM_TRIANGLE_EQ ;;
let OIPLPTM = LIST_MK_CONJ [OIPLPTM1;OIPLPTM2];;
(* AFFINE GEOMETRY *)
let KVLZSAQ1 = AFFINE;;
let KVLZSAQ2 = Sphere.aff;; (* deprecated *)
let KVLZSAQ = LIST_MK_CONJ [KVLZSAQ1;KVLZSAQ2];;
(* see also affsign;; lin_combo;; *)
let BYFLKYM1 = Sphere.aff;;
let BYFLKYM2 = Sphere.aff_ge_def;;
let BYFLKYM3 = Sphere.aff_gt_def;;
let BYFLKYM4 = Sphere.aff_lt_def;;
let BYFLKYM5 = Sphere.aff_le_def;;
let BYFLKYM = LIST_MK_CONJ [BYFLKYM1;BYFLKYM2;BYFLKYM3;BYFLKYM4;BYFLKYM5];;
let OWECYNV1 = convex;;
let OWECYNV2 = `(hull) convex`;;
let OWECYNV = (OWECYNV1,OWECYNV2);;
let GDCZMLO = CONVEX_HULL_AFF_GE;;
let UIVNNRR2 = AFF_GT_EQ_AFFINE_HULL;;
let UIVNNRR = LIST_MK_CONJ [UIVNNRR1;UIVNNRR2];;
let LLOUBAX = cone ;;
let SWKFLBJ1 = Sphere.line ;;
let SWKFLBJ2 = collinear ;;
let SWKFLBJ3 = parallel;;
let SWKFLBJ = LIST_MK_CONJ [ SWKFLBJ1; SWKFLBJ2; SWKFLBJ3];;
let JLWZFBH1 = plane ;;
let JLWZFBH2 = Sphere.closed_half_plane;;
let JLWZFBH3 = Sphere.open_half_plane;;
let JLWZFBH4 = coplanar ;;
let JLWZFBH = LIST_MK_CONJ [JLWZFBH1;JLWZFBH2;JLWZFBH3;JLWZFBH4];;
let OAUVFPS1 = Sphere.closed_half_space ;;
let OAUVFPS2 = Sphere.open_half_space ;;
let OAUVFPS = LIST_MK_CONJ [OAUVFPS1;OAUVFPS2];;
let AVWKGNB = delta_x;;
let LBEVAKV = Collect_geom.DELTA_POS_4POINTS;;
let CTCZHMR = LIST_MK_CONJ [LBEVAKV;Collect_geom.POLFLZY];; (* Delta pos LEG [line 2690;line 3010], *)
let KZVHHBG = LIST_MK_CONJ [Collect_geom.LTCTBAN;Collect_geom.GJWYYPS;Collect_geom.GDLRUZB];;
let NUHSVLM = UNKNOWN;; (* " implemented in collect_geom2.hl" ;; *)
(* CayleyR results: lines from legacy/collect_geom.ml LEG:
2337/LTCTBAN: ups is leading coeff of quadratic cayleyR
2725/GJWYYPS: discriminant of cayleyR
2894/GDLRUZB: disc(cayleyR)=0 <=> one of tetra are coplanar
3010/NUHSVLM: 5 points in R3 ==> cayleyR = 0
RPFVZDI: enclosed function defined
*)
let RPFVZDI = Enclosed.enclosed;; (* "implemented in enclosed_def.hl ";; *)
let WZYUXVC = arcV ;;
let ACNBFRL = UNKNOWN ;; (* arcV atn2 *)
let PQQDENV = Trigonometry1.ACS_ARCLENGTH;;
let HQTBPCM1 = LAW_OF_COSINES ;;
let HQTBPCM2 = Trigonometry1.DIST_LAW_OF_COS ;;
let HQTBPCM = LIST_MK_CONJ [HQTBPCM1;HQTBPCM2];;
let OBPIOXD = Sphere.ups_x;; (* upsilon def *)
let QRAAWFS = LIST_MK_CONJ [Trigonometry2.UPS_X_POS;Collect_geom.FHFMKIY];;
let IHIQXLM = Trigonometry1.UPS_X_SQUARES;; (* upsilon factors *)
let UKBAHKV = Trigonometry1.VECTOR_LAW_OF_SINES ;; (* slightly different from book *)
let GVWTZKY = UNKNOWN;; (* arc, atn2 *)
(* cross product something *)
let FCUAGA = cross;;
let KVVWPNA = NORM_CROSS ;; (* norm cross and ups, combine with UKBAHKV *)
(* Lemma label{} *)
(* cross product order and distribution with dot product *)
let BKMUSOX1 = CROSS_SKEW ;;
let BKMUSOX2 = CROSS_TRIPLE ;;
let BKMUSOX = LIST_MK_CONJ [ BKMUSOX1; BKMUSOX2];;
(* Definition label{def:dih} *)
let dihV = dihV ;;
let RLXWSTK = Trigonometry2.RLXWSTK;;
let NLVWBBW = Trigonometry2.NLVWBBW;;
let OJEKOJF = Trigonometry2.OJEKOJF;;
let JLPSDHF = Euler_main_theorem.EULER_TRIANGLE;; (* euler_triangle ;; *)
let KEITDWB = Trigonometry2.ARCV_INEQUALTY ;;
let FGNMPAV = Trigonometry2.FGNMPAV ;;
let FEVNANL = LIST_MK_CONJ [Trigonometry1.atn2_spec;Trigonometry1.ATAN2_EXISTS];;
let AXBTGQX = orthonormal;; (* much more has been proved about orthonormal vectors *)
let QAUQIEC = UNKNOWN;; (* "not found, adapted orthonormization ";; *)
let EYFCXPP = [Trigonometry2.EYFCXPP;(* see also CYLINDER_CORDINATE *)
Trigonometry2.CYLINDER_CORDINATE];;
let azim = azim ;;
let QQZKTXU = Trigonometry2.QQZKTXU;;
let JBDNJJB = Trigonometry2.JBDNJJB;;
(* zenith angle *)
let QAFHJNM =Trigonometry2.QAFHJNM;;
let XPHCPNY = SPHERICAL_COORDINATES ;;
(* Cycle *)
(* DEPRECATED 2011-08-01. let TNZQDCX = Sphere.polar_cycle;; *)
let PDPFQUK = Trigonometry2.PDPFQUK;;
let ISRTTNZ = Trigonometry2.ISRTTNZ;;
let KFKHLWK = Trigonometry2.cyclic_set;;
let YESEEWW = Sphere.azim_cycle;;
let NLOFMTR = UNKNOWN;; (* "not found, of doubtful use";; *)
let YVREJIS = Trigonometry2.YVREJIS;;
let ULEKUUB = UNKNOWN;; (* "not found, fan version given as Topology.ULEKUUB";; *)
(* spherical triangle inequality *)
let KEITDWB = Trigonometry2.KEITDWB;;
let FGNMPAV = Trigonometry2.FGNMPAV;;
end;;