100/pythagoras.ml

   1 (* ========================================================================= *)
   2 (* A "proof" of Pythagoras's theorem. Of course something similar is         *)
   3 (* implicit in the definition of "norm", but maybe this is still nontrivial. *)
   4 (* ========================================================================= *)
   5
   6 needs "Multivariate/misc.ml";;
   7 needs "Multivariate/vectors.ml";;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Direct vector proof (could replace 2 by N and the proof still runs).      *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let PYTHAGORAS = prove
  14  (`!A B C:real^2.
  15         orthogonal (A - B) (C - B)
  16         ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,
  17   REWRITE_TAC[NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
  18   CONV_TAC REAL_RING);;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* A more explicit and laborious "componentwise" specifically for 2-vectors. *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 let PYTHAGORAS = prove
  25  (`!A B C:real^2.
  26         orthogonal (A - B) (C - B)
  27         ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,
  28   SIMP_TAC[NORM_POW_2; orthogonal; dot; SUM_2; DIMINDEX_2;
  29            VECTOR_SUB_COMPONENT; ARITH] THEN
  30   CONV_TAC REAL_RING);;