(* ========================================================================= *)
(* A "proof" of Pythagoras's theorem. Of course something similar is         *)
(* implicit in the definition of "norm", but maybe this is still nontrivial. *)
(* ========================================================================= *)

needs "Multivariate/misc.ml";;
needs "Multivariate/vectors.ml";;

(* ------------------------------------------------------------------------- *)
(* Direct vector proof (could replace 2 by N and the proof still runs).      *)
(* ------------------------------------------------------------------------- *)

let PYTHAGORAS = 
prove
 (`!A B C:real^2.
        orthogonal (A - B) (C - B)
        ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,

  REWRITE_TAC[NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
  CONV_TAC REAL_RING);;
(* ------------------------------------------------------------------------- *)
(* A more explicit and laborious "componentwise" specifically for 2-vectors. *)
(* ------------------------------------------------------------------------- *)

let PYTHAGORAS = 
prove
 (`!A B C:real^2.
        orthogonal (A - B) (C - B)
        ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,

  SIMP_TAC[NORM_POW_2; orthogonal; dot; SUM_2; DIMINDEX_2;
           VECTOR_SUB_COMPONENT; ARITH] THEN
  CONV_TAC REAL_RING);;