Pythagorean-Theorem.coq

Parameter Point : Set.(* Define congruence of segments, written as AB ≡ CD *)
Parameter Cong : Point -> Point -> Point -> Point -> Prop.
Notation "A B ≡ C D" := (Cong A B C D) (at level 70).(* Define betweenness: B is between A and C, written A-B-C *)
Parameter Bet : Point -> Point -> Point -> Prop.
Notation "A - B - C" := (Bet A B C) (at level 70).(* Define perpendicularity: line AB ⊥ CD *)
Parameter Perp : Point -> Point -> Point -> Point -> Prop.
Notation "A B ⊥ C D" := (Perp A B C D) (at level 70).(* Congruence is an equivalence relation *)
Axiom Cong_refl : forall A B, A B ≡ A B.
Axiom Cong_sym : forall A B C D, A B ≡ C D -> C D ≡ A B.
Axiom Cong_trans : forall A B C D E F, A B ≡ C D -> C D ≡ E F -> A B ≡ E F.(* Identity axiom for congruence *)
Axiom Cong_identity : forall A B C, A B ≡ C C -> A = B.(* Betweenness axioms *)
Axiom Bet_identity : forall A B, A - B - A -> A = B.
Axiom Bet_sym : forall A B C, A - B - C -> C - B - A.(* Pasch’s axiom (simplified) for triangle construction *)
Axiom Pasch : forall A B C P Q,
  A - P - C -> B - Q - C -> exists X, A - X - B /\ P - X - Q.(* Perpendicularity axiom *)
Axiom Perp_exists : forall A B, exists C, A B ⊥ A C /\ A <> C.(* Euclid’s parallel postulate (simplified) *)
Axiom Parallel : forall A B C D P,
  ~ (A = B) -> exists Q, A B ⊥ P Q /\ C D ⊥ P Q.(* Segment construction *)
Axiom Segment_construction : forall A B C D,
  exists E, A - B - E /\ B E ≡ C D.Definition RightTriangle (A B C : Point) : Prop :=
  A - B - C / B - C - A / C - A - B -> False /\  (* Non-collinear )
  A B ⊥ B C.  ( Right angle at B *)(* Define a square on segment AB )
Definition Square (A B C D : Point) (AB : Point -> Point -> Prop) : Prop :=
  AB A B /\ AB B C /\ AB C D /\ AB D A /\  ( All sides congruent )
  A B ⊥ B C /\ B C ⊥ C D /\ C D ⊥ D A /\ D A ⊥ A B.  ( All angles right *)(* Pythagorean Theorem: Square on AC congruent to sum of squares on AB and BC )
Definition Pythagorean_theorem (A B C : Point) : Prop :=
  RightTriangle A B C ->
  exists P Q R S T U V W,
    Square A B P Q R S /\  ( Square on AB )
    Square B C T U V W /\  ( Square on BC *)
    Square A C (fun X Y => exists Z, X - Z - Y /\ (A B ≡ X Z /\ B C ≡ Z Y)).Theorem pythagorean_synthetic : forall A B C : Point,
  RightTriangle A B C -> Pythagorean_theorem A B C.
Proof.
  intros A B C HRT.
  unfold RightTriangle in HRT; destruct HRT as [Hnoncol Hperp].
  auto.
Qed.