Proof Certificates and Geometry

Examples

Altitudes, Bisections, Bisectors, Butterfly, Ceva, Chords, Desargues, Euler circle, Feuerbach, Isoceles, Medians, Minh, Pappus, Pascal circle, Pascal circle2, Ptolemy, Ptolemy95, Pythagore, Segments of chords, Simson, Thales, Threepoints

Definitions

Record point:Type := { X:R; Y:R}.

Definition collinear(A B C:point):=
  (X A - X B) * (Y C - Y B) - (Y A - Y B) * (X C - X B) = 0.

Definition parallel (A B C D:point):=
  ((X A) - (X B)) * ((Y C) - (Y D)) = ((Y A) - (Y B)) * ((X C) - (X D)).

Definition notparallel (A B C D:point)(x:R):=
  x* (((X A) - (X B)) * ((Y C) - (Y D)) - ((Y A) - (Y B)) * ((X C) - (X D))) = 1.

Definition orthogonal (A B C D:point):=
  ((X A) - (X B)) * ((X C) - (X D)) + ((Y A) - (Y B)) * ((Y C) - (Y D)) = 0.

Definition equal2(A B:point):=
  (X A) = (X B) /\ (Y A) = (Y B).

Definition equal3(A B:point):=
  ((X A) - (X B))^2 + ((Y A) - (Y B))^2 = 0.

Definition nequal2(A B:point):=
  (X A) <> (X B) \/ (Y A) <> (Y B).

Definition nequal3(A B:point):=
  not (((X A) - (X B))^2 + ((Y A) - (Y B))^2 = 0).

Definition middle(A B I:point):=
  2* (X I) = (X A) + (X B) /\ 2 * (Y I)= (Y A) + (Y B).

Definition distance2(A B:point):=
  ((X B) - (X A))^2 + ((Y B) - (Y A))^2.

Definition equaldistance(A B C D:point):=
  ((X B) - (X A))^2 + ((Y B) - (Y A))^2 = ((X D) - (X C))^2 + ((Y D) - (Y C))^2.

Definition determinant(A O B:point):=
  ((X A) - (X O)) * ((Y B) - (Y O)) - ((Y A) - (Y O)) * ((X B) - (X O)).

Definition scalarproduct(A O B:point):=
  ((X A) - (X O)) * ((X B) - (X O)) + ((Y A) - (Y O)) * ((Y B) - (Y O)).

Definition norm2(A O B:point):=
  (((X A) - (X O))^2 + ((Y A) - (Y O))^2) * (((X B) - (X O))^2 + ((Y B) - (Y O))^2).

Definition tripletangente(A B C D E F:point):=
  let s:= determinant A B C in
  let c:= scalarproduct A B C in
  let s3:= determinant D E F in
  let c3:= scalarproduct D E F in
  s^3 * c3 - 3 * s3 * s^2 * c - 3 * s * c^2 * c3 + s3 * c^3 = 0.

Definition equalangle(A B C D E F:point):=
  let s1:= determinant A B C in
  let c1:= scalarproduct A B C in
  let n1:= norm2 A B C in
  let s2:= determinant D E F in
  let c2:= scalarproduct D E F in
  let n2:= norm2 D E F in
  s1 * n2 = s2 * n1 /\ c1 * n2 = c2 * n1.

Definition equaltangente(A B C D E F:point):=
  let s1:= determinant A B C in
  let c1:= scalarproduct A B C in
  let s2:= determinant D E F in
  let c2:= scalarproduct D E F in
  s1 * c2 = s2 * c1.