100/heron.ml

   1 (* ========================================================================= *)
   2 (* Heron's formula for the area of a triangle.                               *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/measure.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Eliminate square roots from formula by the usual method.                  *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let SQRT_ELIM_TAC =
  14   let sqrt_tm = `sqrt:real->real` in
  15   let is_sqrt tm = is_comb tm & rator tm = sqrt_tm in
  16   fun (asl,w) ->
  17     let stms = setify(find_terms is_sqrt w) in
  18     let gvs = map (genvar o type_of) stms in
  19     (MAP_EVERY (MP_TAC o C SPEC SQRT_POW_2 o rand) stms THEN
  20      EVERY (map2 (fun s v -> SPEC_TAC(s,v)) stms gvs)) (asl,w);;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* Main result.                                                              *)
  24 (* ------------------------------------------------------------------------- *)
  25
  26 let HERON = prove
  27  (`!A B C:real^2.
  28         let a = dist(C,B)
  29         and b = dist(A,C)
  30         and c = dist(B,A) in
  31         let s = (a + b + c) / &2 in
  32         measure(convex hull {A,B,C}) = sqrt(s * (s - a) * (s - b) * (s - c))`,
  33   REPEAT GEN_TAC THEN REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
  34   REWRITE_TAC[MEASURE_TRIANGLE] THEN
  35   CONV_TAC SYM_CONV THEN MATCH_MP_TAC SQRT_UNIQUE THEN
  36   SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS; REAL_POS] THEN
  37   REWRITE_TAC[REAL_POW_DIV; REAL_POW2_ABS] THEN
  38   REWRITE_TAC[dist; vector_norm] THEN
  39   REWRITE_TAC[dot; SUM_2; DIMINDEX_2] THEN
  40   SIMP_TAC[VECTOR_SUB_COMPONENT; ARITH; DIMINDEX_2] THEN
  41   SQRT_ELIM_TAC THEN SIMP_TAC[REAL_LE_SQUARE; REAL_LE_ADD] THEN
  42   CONV_TAC REAL_RING);;