# Library Fermat4.Pythagorean

Require Export Tactics.

Definition nnl_triple (a b c : Z) := ~(a = 0) ~(b = 0) ~(c = 0).

Definition pos_triple (a b c : Z) := (a 0) (b 0) (c 0).

Definition is_pytha (a b c : Z) := (pos_triple a b c) a × a + b × b = c × c.

Definition in_ucirc (x y : R) := (x × x + y × y = 1)%R.
Definition D_r (r x y : R) := (y = r × (x + 1))%R.

Lemma pytha_ucirc1 : a b c : Z,
(c > 0) (is_pytha a b c) (in_ucirc (frac a c) (frac b c)).
Proof.
intros; unfold in_ucirc; unfold frac; field_simplify_eq.
unfold is_pytha in H0; elim H0; intros.
repeat rewrite pow_IZR. rewrite <- plus_IZR. simpl Z_of_nat.
ring_simplify [(sym_eq H2)] (c^2);trivial.
discrR; auto with zarith.
Save.

Lemma pytha_ucirc2 : a b c : Z, (a 0) (b 0) (c > 0)
(in_ucirc (frac a c) (frac b c)) (is_pytha a b c).
Proof.
unfold in_ucirc; unfold frac; unfold is_pytha; intros; split.
unfold pos_triple; auto with zarith.
apply eq_IZR; apply (Rmult_eq_reg_l (/ (IZR c × IZR c))).
pattern (IZR c × IZR c)%R at 2; rewrite <- mult_IZR;rewrite Rinv_l.
rewrite Rinv_mult_distr.
rewrite <- H0; rewrite plus_IZR; repeat rewrite mult_IZR; field.
discrR; auto with zarith.
discrR; auto with zarith.
discrR; auto with zarith.
rewrite mult_IZR; split_Rmult; discrR; auto with zarith.
apply Rinv_neq_0_compat; split_Rmult; discrR; auto with zarith.
Save.

Definition interCDr (r x y : R) := (in_ucirc x y) (D_r r x y).

Definition p1 := (-1,0)%R.
Definition p2 (r : R) :=
let den := (1 + r × r)%R in
((1 - r × r) / den, 2 × r / den)%R.

Definition eqp (p1 p2 : R × R) := (fst p1) = (fst p2) (snd p1)= (snd p2).

Lemma ordp : p1 p2 : R × R, (eqp p1 p2) ~(eqp p1 p2).
Proof.
intros p3 p4. unfold eqp; elim p3; elim p4; intros; simpl.
elim (Req_dec a a0); elim (Req_dec b b0); intuition.
Save.

Lemma interCDr_sol : r x y : R,
(interCDr r x y) (eqp (x,y) p1) (eqp (x,y) (p2 r)).
Proof.
unfold interCDr;unfold in_ucirc;unfold D_r;unfold eqp, p1, p2;simpl.
intros;elim H;intros;rewrite H1 in H0.
cut (((1 + r × r) × Rsqr x + 2 × r × r × x + (r × r - 1)) = 0)%R.
intro;cut ((1 + r × r) 0)%R.
intro;cut (Delta_is_pos (mknonzeroreal (1 + r × r) H3) (2 × r × r)
(r × r - 1))%R.
intro;generalize (Rsqr_sol_eq_0_0 (mknonzeroreal (1 + r × r) H3) (2 × r × r)
(r × r - 1) x H4 H2)%R.
unfold sol_x1, sol_x2;unfold Delta;unfold Rsqr;simpl.
cut ((2 × r × r × (2 × r × r) - 4 × (1 + r × r) × (r × r - 1))%R = 4%R).
intro;rewrite H5;rewrite sqrt_square.
induction 1;[right|left].
split;[rewrite H6;field;assumption
|rewrite H1;rewrite H6;field;assumption].
split;[rewrite H6;field;assumption
|rewrite H1;rewrite H6;field;assumption].
unfold Rle;left;prove_sup.
ring.
unfold Delta_is_pos;unfold Delta;unfold Rsqr;simpl;
ring_simplify (2 × r × r × (2 × r × r) - 4 × (1 + r × r) × (r × r - 1))%R;
unfold Rle;left;prove_sup.
apply Rgt_not_eq;unfold Rgt;rewrite Rplus_comm;apply Rle_lt_0_plus_1;
fold (Rsqr r);elim (Req_dec r 0);intro;
[rewrite H3;rewrite Rsqr_0;unfold Rle;right;auto
|unfold Rle;left;apply Rsqr_pos_lt;assumption].
pattern 1%R at 4;rewrite <- H0;unfold Rsqr;ring.
Save.

Lemma rat_coo1 : x y : R, (in_ucirc x y)
( r : R, (is_rat r) (interCDr r x y)) (is_ratp (x,y)).
Proof.
unfold in_ucirc, is_ratp, is_rat.
unfold frac; intros; elim H; intros; elim H1; intros; elim H2; intros;
elim H3; intro; elim x1;intros; elim H5; intros;
elim (interCDr_sol x0 x y H4); unfold eqp, p1, p2; simpl; intro; elim H8;
intros; rewrite H9; rewrite H10.
split.
(-1,1); split; [ auto with zarith | simpl; field; discrR ].
(0,1); split; [ auto with zarith | simpl; field; discrR ].
split.
(b × b - a × a, a × a + b × b); split.
auto with zarith.
rewrite H7; rewrite <- Z_R_minus; rewrite plus_IZR; repeat rewrite mult_IZR;
field; split;discrR; auto with zarith reals.
(2 × a × b × b, (a × a + b × b) × b); split.
apply not_IZR_0; rewrite mult_IZR; split_Rmult; discrR; auto with zarith.
rewrite H7; repeat rewrite mult_IZR; rewrite plus_IZR;
repeat rewrite mult_IZR; simpl; field; split; discrR;
auto with zarith reals.
Save.

Lemma rat_coo2 : x y : R, (in_ucirc x y) (is_ratp (x,y))
r : R, (is_rat r) (interCDr r x y).
Proof.
unfold in_ucirc, is_ratp, is_rat, interCDr.
unfold frac, in_ucirc, D_r; intros.
elim (Req_dec x (-1)%R); intro.
1%R; split.
(1,1); split; [ auto with zarith | field; discrR ].
elim H; intros; split.
assumption.
rewrite H0; rewrite H0 in H1; ring_simplify (1 × (-1 + 1))%R;
cut ((1 + y × y) = 1)%R;
[ intro; apply Rsqr_0_uniq; unfold Rsqr;
apply (Rplus_0_r_uniq 1 (y × y) H3)%R
| pattern 1%R at 2; rewrite <- H1; ring ].
(y / (x + 1))%R; cut ((x + 1) 0)%R;
[ intro; split
| rewrite <- (Ropp_involutive 1); fold (x - -1)%R; apply Rminus_eq_contra;
assumption ].
elim H; intros; elim H3; intros; elim H4; intro; elim x0; intros; elim H6;
intros; elim H5; intro; elim x1; intros; elim H9; intros; rewrite H8;
rewrite H11.
cut (a + b 0);
[ intro
| apply not_IZR_0;
cut (((IZR a / IZR b + 1) × IZR b)%R = (IZR a + IZR b)%R);
[ intro; rewrite plus_IZR; rewrite <- H12; split_Rmult;
[ rewrite <- H8; assumption
| discrR; assumption ]
| field; discrR; assumption ] ].
(a0 × b, b0 × (a + b)); split.
apply not_IZR_0; rewrite mult_IZR; rewrite plus_IZR; split_Rmult; discrR;
assumption.
repeat rewrite mult_IZR; rewrite plus_IZR; field; discrR; try assumption.
repeat split; discrR; try assumption; fold (IZR a / IZR b)%R;
rewrite <- H8; assumption.
split; [ elim H; intros; assumption | field; assumption ].
Save.

Definition is_posp (c : R × R) := (fst c 0)%R (snd c 0)%R.

Definition is_ucp (c : R × R) :=
(in_ucirc (fst c) (snd c)) (is_ratp c) (is_posp c).

Definition ucp (p q : Z) :=
let pr := (IZR p) in
let qr := (IZR q) in
let den := (pr × pr + qr × qr)%R in
((qr × qr - pr × pr) / den, (2 × pr × qr) / den)%R.

Definition cond_pqb (p q : Z) := p 0 q > 0 p q (rel_prime p q).

Definition in_ucp_setb (x y : R) :=
p : Z, q : Z,
x = (fst (ucp p q)) y = (snd (ucp p q)) (cond_pqb p q).

Lemma rat_pos_coo1 : x y : R, (is_ucp (x,y))
r : R, (is_rat r) (r 0)%R (r 1)%R x = (fst (p2 r))
y = (snd (p2 r)).
Proof.
intros; unfold is_ucp in H; elim H; intros; elim H1; intros;
elim (rat_coo2 x y (conj H0 H2)); intros; elim H4; intros.
elim (interCDr_sol x0 x y).
unfold eqp; simpl; intro; elim H7; intros; elim H3; simpl; intros;
rewrite H8 in H10; elimtype False; generalize (Rge_le (-1) 0 H10)%R;
fold (¬ (0 -1)%R); apply Rlt_not_le; prove_sup.
cut (0 < / (1 + x0 × x0))%R;
[ intro
| apply Rinv_0_lt_compat; rewrite <- (Rplus_0_r 0)%R;
apply Rplus_lt_le_compat;
[ prove_sup
| fold (Rsqr x0); elim (Req_dec x0 0); intro;
[ rewrite H7; rewrite Rsqr_0; unfold Rle; right; auto
| unfold Rle; left; apply Rsqr_pos_lt; assumption ] ] ].
unfold eqp; simpl; intro; elim H8; intros; elim H3; simpl; rewrite H9;
rewrite H10; intros; x0; split.
assumption.
split.
generalize (Rge_le (2 × x0 / (1 + x0 × x0)) 0 H12); intro;
rewrite Rmult_comm in H13;
rewrite <- (Rmult_0_l (2 / (1 + x0 × x0))) in H13;
cut (0 < 2 / (1 + x0 × x0))%R;
[ intro; rewrite Rmult_comm in H13; unfold Rdiv in H13;
rewrite (Rmult_assoc x0 2) in H13;
rewrite (Rmult_comm x0 (2 × / (1 + x0 × x0)))%R in H13;
generalize (Rmult_le_reg_l (2 / (1 + x0 × x0)) 0 x0 H14 H13); intro;
apply Rle_ge; assumption
| unfold Rdiv; prove_sup; assumption ].
split.
generalize (Rge_le ((1 - x0 × x0) / (1 + x0 × x0)) 0 H11); intro;
unfold Rdiv in H13; rewrite Rmult_comm in H13;
rewrite <- (Rmult_0_r (/ (1 + x0 × x0)))%R in H13;
generalize (Rmult_le_reg_l (/ (1 + x0 × x0)) 0 (1 - x0 × x0) H7 H13)%R;
intro; generalize (Rplus_le_compat_r (x0 × x0) 0 (1 - x0 × x0) H14)%R;
intro; rewrite Rplus_0_l in H15; unfold Rminus in H15;
rewrite Rplus_assoc in H15; rewrite Rplus_opp_l in H15;
rewrite Rplus_0_r in H15; rewrite <- (Rmult_1_r 1) in H15;
fold (Rsqr x0) in H15; fold (Rsqr 1) in H15;
apply (Rsqr_incr_0_var x0 1 H15); unfold Rle; left; prove_sup.
auto.
assumption.
Save.

Lemma rat_pos_coo2 : x y : R, (is_ucp (x,y)) (in_ucp_setb x y).
Proof.
intros; elim (rat_pos_coo1 x y H); simpl; intros; elim H0; intros; elim H2;
intros; elim H4; intros; elim H6; intros; elim (relp_rat x0 H1 H3 H5);
intro; elim x1; unfold frac; intros; elim H9; intros; elim H11; intros;
elim H13; intros; elim H15; intros; unfold in_ucp_setb; simpl;
unfold cond_pqb; a; b; rewrite H7; rewrite H8; rewrite H17.
cut (b 0); auto with zarith; intro.
split.
field; split; discrR; auto with zarith reals.
split.
field; split; discrR; auto with zarith reals.
tauto.
Save.

Definition cond_pq (p q : Z) := cond_pqb p q (distinct_parity p q).

Definition in_ucp_set (x y : R) :=
p : Z, q : Z,
(x = (fst (ucp p q)) y = (snd (ucp p q))
x = (snd (ucp p q)) y = (fst (ucp p q))) (cond_pq p q).

Lemma nrat_pos_coo1 : x y : R, (in_ucp_set x y) (in_ucp_setb x y).
Proof.
unfold in_ucp_set, in_ucp_setb, cond_pq, cond_pqb; simpl; intros; elim_hyps.
x0; x1; intuition.
(x1 - x0); (x0 + x1); rewrite plus_IZR; rewrite <- Z_R_minus;
rewrite H; rewrite H5.
replace
((IZR x1 - IZR x0) × (IZR x1 - IZR x0) +
(IZR x0 + IZR x1) × (IZR x0 + IZR x1))%R with
(2 × (IZR x0 × IZR x0 + IZR x1 × IZR x1))%R by ring.
split;[idtac|split]; try (field; neq_0;apply sqr_sum; auto with zarith).
do 3 try split; auto with zarith.
generalize (prop1 _ _ H4 H1); auto with zarith.
Save.

Lemma nrat_pos_coo2 : x y : R, (in_ucp_setb x y) (in_ucp_set x y).
Proof.
unfold in_ucp_setb, in_ucp_set, cond_pq, cond_pqb, distinct_parity; simpl;
intros; elim_hyps.
elim (relp_parity x0 x1 H4); intro.
x0; x1; intuition.
unfold both_odd in H5; elim_hyps; generalize (Zodd_def1 _ H5); clear H5;
intro; generalize (Zodd_def1 _ H6); clear H6; intro; elim_hyps.
(x2 - x3); (x2 + x3 + 1); split;
[ right; rewrite H; rewrite H0; rewrite H5; rewrite H6; atomic_IZR; simpl;
split; field; split; neq_0; apply sqr_sum; auto with zarith
| rewrite H5 in H1; rewrite H6 in H2; rewrite H5 in H3; rewrite H6 in H3;
do 4 try split; auto with zarith ].
apply rel_prime_sym; apply relp_sum; ring_simplify (x2 + x3 + 1 + (x2 - x3));
ring_simplify (x2 + x3 + 1 - (x2 - x3)); generalize H5; clear H5;
ring_simplify (2 × x3 + 1);
intro; generalize H6; clear H6; ring_simplify (2 × x2 + 1); intro;
rewrite <- H5; rewrite <- H6; auto with zarith.
elim (Zeven_odd_dec x2); intro; elim (Zeven_odd_dec x3); intro; Zparity_hyps;
rewrite H7; rewrite H8;
[ left; split; [ apply Zeven_def2; (x4 - x5)
| apply Zodd_def2; (x4 + x5) ]
| right; split; [ apply Zodd_def2; (x5 - x4 - 1)
| apply Zeven_def2; (x5 + x4 + 1) ]
| right; split; [ apply Zodd_def2; (x4 - x5)
| apply Zeven_def2; (x4 + x5 + 1) ]
| left; split; [ apply Zeven_def2; (x4 - x5)
| apply Zodd_def2; (x4 + x5 + 1) ] ]; ring.
Save.

Definition pytha_set (a b c : Z) :=
p : Z, q : Z, m : Z,
(a = m × (q × q - p × p) b = 2 × m × (p × q)
a = 2 × m × (p × q) b = m × (q × q - p × p))
c = m × (p × p + q × q) m 0 (cond_pq p q).

Lemma relp_frac : a b c d : Z,
(b 0) (d 0) (frac a b) = (frac c d) (rel_prime c d)
m : Z, m 0 b = m × d.
Proof.
unfold frac; intros.
cut (c × b = a × d).
intro; cut (d | c × b);
[ intro; cut (rel_prime d c);
try (intro; generalize (Gauss d c b H4 H5); intro; destruct H6 as (q,H6);
q; intuition; rewrite H7 in H6); auto with zarith
| apply (Zdivide_intro _ _ a H3) ].
generalize (Rmult_eq_compat_l (IZR b × IZR d) _ _ H1); clear H1; intro;
replace (IZR b × IZR d × (IZR a / IZR b))%R
with ((IZR a) × (IZR d))%R in H1;
[ replace (IZR b × IZR d × (IZR c / IZR d))%R
with ((IZR c) × (IZR b))%R in H1;
[ repeat rewrite <- mult_IZR in H1; generalize (eq_IZR _ _ H1); auto
| field; discrR; assumption ]
| field; discrR; assumption ].
Save.

Lemma pytha_thm1 : a b c : Z, (is_pytha a b c) (pytha_set a b c).
Proof.
do 3 intro; elim (Z_gt_dec c 0); [ idtac
| unfold is_pytha, pytha_set, pos_triple, cond_pq, cond_pqb ]; intros.
generalize (pytha_ucirc1 _ _ _ a0 H); intro;
cut (is_ucp (frac a c, frac b c));
[ clear H0; intro; generalize (rat_pos_coo2 _ _ H0); clear H0; intro;
generalize (nrat_pos_coo2 _ _ H0); clear H0; intro;
unfold in_ucp_set, cond_pq, cond_pqb in H0;
unfold pytha_set, cond_pq, cond_pqb; simpl in H0; elim_hyps;
generalize (relp_pq1 _ _ H1 H4 H5 H2); intro;
generalize (Zgt_lt _ _ a0); intro; generalize (Zlt_not_eq _ _ H8);
clear H8; intro; generalize (sym_not_eq H8); clear H8; intro;
generalize (Zgt_lt _ _ H3); intro; generalize (Zlt_not_eq _ _ H9);
clear H9; intro; generalize (sym_not_eq H9); clear H9; intro;
(cut (x × x + x0 × x0 0); [ intro | auto with zarith ];
(cut ((IZR x0 × IZR x0 - IZR x × IZR x) /
(IZR x × IZR x + IZR x0 × IZR x0) =
frac (x0 × x0 - x × x) (x × x + x0 × x0))%R;
[ intro | head_IZR; auto ];
(cut (2 × IZR x × IZR x0 / (IZR x × IZR x + IZR x0 × IZR x0) =
frac (2 × x × x0) (x × x + x0 × x0))%R;
[ intro | head_IZR; auto ])))
| idtac ].
rewrite H11 in H0; clear H11; rewrite H12 in H6; clear H12;
generalize (relp_frac _ _ _ _ H8 H10 H0 H7); intro; elim_hyps;
rewrite H12 in H0; rewrite H12 in H6; x; x0; x1;
generalize (frac_eq _ _ _ _ H11 H10 H0); clear H0; intro;
generalize (frac_eq _ _ _ _ H11 H10 H6); clear H6; intro;
rewrite H0; rewrite H6; rewrite H12; intuition; (left; split; ring) ||
(cut (x1 × (x × x + x0 × x0) > 0);
[ intro; rewrite Zmult_comm in H13; cut (x × x + x0 × x0 > 0);
try (intro; generalize (Zmult_gt_0_reg_l _ _ H14 H13));
auto with zarith
| rewrite <- H12; assumption ]).
rewrite H11 in H6; clear H11; rewrite H12 in H0; clear H12;
generalize (relp_frac _ _ _ _ H8 H10 H6 H7); intro; elim_hyps;
rewrite H12 in H0; rewrite H12 in H6; x; x0; x1;
generalize (frac_eq _ _ _ _ H11 H10 H0); clear H0; intro;
generalize (frac_eq _ _ _ _ H11 H10 H6); clear H6; intro;
rewrite H0; rewrite H6; rewrite H12; intuition; (right; split; ring) ||
(cut (x1 × (x × x + x0 × x0) > 0);
[ intro; rewrite Zmult_comm in H13; cut (x × x + x0 × x0 > 0);
try (intro; generalize (Zmult_gt_0_reg_l _ _ H14 H13));
auto with zarith
| rewrite <- H12; assumption ]).
unfold is_ucp, is_ratp, is_posp; simpl; intuition; unfold is_rat;
unfold is_pytha, pos_triple in H; elim_hyps; generalize (Zgt_lt _ _ a0);
intro; generalize (IZR_lt _ _ H4); intro; simpl in H5;
fold (IZR c > 0)%R in H5;
[ (a, c); intuition | (b, c); intuition
| unfold frac; generalize (IZR_ge _ _ H); clear H; intro; simpl in H
| unfold frac; generalize (IZR_ge _ _ H2); clear H2; intro; simpl in H2 ];
auto with reals.
elim_hyps; cut (c = 0);
[ intro; 0; 1; 0; rewrite H3; simpl; intuition;
(left; rewrite H3 in H0; simpl in H0; progress auto with zarith)
|| (compute; auto with zarith)
| auto with zarith ].
Save.

Lemma pytha_thm2 : a b c : Z, (pytha_set a b c) (is_pytha a b c).
Proof.
unfold pytha_set, is_pytha, cond_pq, cond_pqb, pos_triple; intros; elim_hyps;
rewrite H; rewrite H7; rewrite H0; split; ring || (intuition; apply Zle_ge;
generalize (Zge_le _ _ H2); clear H2; intro; generalize (Zgt_lt _ _ H4);
clear H4; intro; generalize (Zlt_le_weak _ _ H4); intro;
repeat apply Zmult_le_0_compat; auto with zarith).
Save.

Definition pytha_set_even (a b c : Z) :=
p : Z, q : Z, m : Z,
a = m × (q × q - p × p) b = 2 × m × (p × q)
c = m × (p × p + q × q) m 0 (cond_pq p q).

Lemma pytha_thm3 : a b c : Z,
is_pytha a b c Zodd a pytha_set_even a b c.
Proof.
intros; elim (pytha_thm1 _ _ _ H); clear H; intros;
unfold cond_pq, cond_pqb in H; elim_hyps;
unfold pytha_set_even, cond_pq, cond_pqb; x; x0; x1;
try solve [ intuition ].
elimtype False; rewrite <- Zmult_assoc in H;
generalize (Zeven_def2 _ (ex_intro (fun xa = 2 × x) (x1 × (x × x0)) H));
intro; generalize (Zeven_not_Zodd _ H9); auto.
Save.