100/ptolemy.ml

   1 (* ========================================================================= *)
   2 (* Ptolemy's theorem.                                                        *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/transcendentals.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Some 2-vector special cases.                                              *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let DOT_VECTOR = prove
  12  (`(vector [x1;y1] :real^2) dot (vector [x2;y2]) = x1 * x2 + y1 * y2`,
  13   REWRITE_TAC[dot; DIMINDEX_2; SUM_2; VECTOR_2]);;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Lemma about distance between points with polar coordinates.               *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let DIST_SEGMENT_LEMMA = prove
  20  (`!a1 a2. &0 <= a1 /\ a1 <= a2 /\ a2 <= &2 * pi /\ &0 <= radius
  21            ==> dist(centre + radius % vector [cos(a1);sin(a1)] :real^2,
  22                     centre + radius % vector [cos(a2);sin(a2)]) =
  23                &2 * radius *  sin((a2 - a1) / &2)`,
  24   REPEAT STRIP_TAC THEN REWRITE_TAC[dist; vector_norm] THEN
  25   MATCH_MP_TAC SQRT_UNIQUE THEN CONJ_TAC THENL
  26    [MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
  27     MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
  28     MATCH_MP_TAC SIN_POS_PI_LE THEN
  29     ASM_REAL_ARITH_TAC;
  30     ALL_TAC] THEN
  31   REWRITE_TAC[VECTOR_ARITH `(c + r % x) - (c + r % y) = r % (x - y)`] THEN
  32   REWRITE_TAC[VECTOR_ARITH `(r % x) dot (r % x) = (r pow 2) * (x dot x)`] THEN
  33   REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_VECTOR] THEN
  34   SUBST1_TAC(REAL_ARITH `a1 = &2 * a1 / &2`) THEN
  35   SUBST1_TAC(REAL_ARITH `a2 = &2 * a2 / &2`) THEN
  36   REWRITE_TAC[REAL_ARITH `(&2 * x - &2 * y) / &2 = x - y`] THEN
  37   REWRITE_TAC[SIN_SUB; SIN_DOUBLE; COS_DOUBLE] THEN
  38   MP_TAC(SPEC `a1 / &2` SIN_CIRCLE) THEN MP_TAC(SPEC `a2 / &2` SIN_CIRCLE) THEN
  39   CONV_TAC REAL_RING);;
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* Hence the overall theorem.                                                *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 let PTOLEMY = prove
  46  (`!A B C D:real^2 a b c d centre radius.
  47         A = centre + radius % vector [cos(a);sin(a)] /\
  48         B = centre + radius % vector [cos(b);sin(b)] /\
  49         C = centre + radius % vector [cos(c);sin(c)] /\
  50         D = centre + radius % vector [cos(d);sin(d)] /\
  51         &0 <= radius /\
  52         &0 <= a /\ a <= b /\ b <= c /\ c <= d /\ d <= &2 * pi
  53         ==> dist(A,C) * dist(B,D) =
  54             dist(A,B) * dist(C,D) + dist(A,D) * dist(B,C)`,
  55   REPEAT STRIP_TAC THEN
  56   REPEAT(FIRST_X_ASSUM(SUBST1_TAC o check (is_var o lhs o concl))) THEN
  57   REPEAT
  58    (W(fun (asl,w) ->
  59      let t = find_term
  60       (fun t -> can (PART_MATCH (lhs o rand) DIST_SEGMENT_LEMMA) t) w in
  61      MP_TAC (PART_MATCH (lhs o rand) DIST_SEGMENT_LEMMA t) THEN
  62      ANTS_TAC THENL
  63       [ASM_REAL_ARITH_TAC;
  64        DISCH_THEN SUBST1_TAC])) THEN
  65   REWRITE_TAC[REAL_ARITH `(x - y) / &2 = x / &2 - y / &2`] THEN
  66   MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE))
  67    [`a / &2`; `b / &2`; `c / &2`; `d / &2`] THEN
  68   REWRITE_TAC[SIN_SUB; SIN_ADD; COS_ADD; SIN_PI; COS_PI] THEN
  69   CONV_TAC REAL_RING);;