Pythagorean triples

Stream: new members

[Paul van Wamelen]

I have a proof of the formula for Pythagorean triples (Number 23 on the 100 Theorems list). I would like to PR this to mathlib. Where should it go though? In src\number_theory or archive\100-theorems-list?
I've made a PR for the first lemma needed in multiset. Hope I did it right! Feedback would be appreciated. I probably still have a lot of cleanup to do...

[Alex J. Best]

I would say in number theory rather than archive, this formula could be useful in other developments.

[Yury G. Kudryashov]

Do you prove rational parametrization of the circle?

[Jalex Stark]

Yury G. Kudryashov said:

Do you prove rational parametrization of the circle?

Is that the same as characterizing all pythagorean triples and then dividing so one side of the equation is 1?

[Kevin Buzzard]

Parametrising the circle is easier, it's less fiddly. You want to find all solutions to $x^2+y^2=1$ in rationals, and you use the fact that each solution $(a,b)$ lies on a unique line which also goes through $(1,0)$, so you just consider lines of the form $y=m(x-1)$ for a fixed $m$; this is two equations in the two unknowns $x$ and $y$ which simplify to one quadratic equation in $x$ and you know $x=1$ is a root, and you can read off the sum of the roots, so you get $a$ from this, and then $b$ by the linear equation. Now clear denominators to get the "classical" result.

[Paul van Wamelen]

This seems much simpler than going through the gaussian integers (which is what I did)...

[Yury G. Kudryashov]

As a free bonus you get the equivalence for any field with ∀ x, x^2+1 ≠ 0 (in particular, any linear ordered field).

[Yury G. Kudryashov]

Something like (with sorrys and a suboptimal proof):

variables {k : Type*} [field k]

def circle_equiv_gen (hk : ∀ x : k, 1 + x^2 ≠ 0) :
  k ≃ {p : k × k | p.1^2 + p.2^2 = 1 ∧ p.2 ≠ -1} :=
{ to_fun := λ x, ⟨⟨2 * x / (1 + x^2), (1 - x^2) / (1 + x^2)⟩,
    by { field_simp [hk x, div_pow], ring },
    by { simp only [ne.def, div_eq_iff (hk x), ← neg_mul_eq_neg_mul, one_mul, neg_add,
      sub_eq_add_neg, add_left_inj],
      rw [eq_neg_iff_add_eq_zero],
      convert hk 1,
      simp }⟩,
  inv_fun := λ p, p.1.1 / (p.1.2 + 1),
  left_inv := λ x, by { field_simp [hk x], sorry },
  right_inv := λ ⟨⟨x, y⟩, hxy, hy⟩, sorry
}

[Kevin Buzzard]

The parametrisation trick works for any smooth plane conic over any field, showing they're birational and hence isomorphic to $\mathbb{P}^1$.

[Paul van Wamelen]

I've now followed the suggestion to use the rational parametrization of the the circle to do pythagorean triples. It actually turns out to be VERY fiddly. There is a problem with divisibility by 2 when you want to go from x/z = (m^2-n^2)/(m^2+y^2) to x = m^2 - n^2. Anyway, that isn't my question. Should something like this:

lemma rat_id {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : nat.coprime a.nat_abs b.nat_abs)
  (h2 : nat.coprime c.nat_abs d.nat_abs) (h : (a : ℚ) / b = (c : ℚ) / d) :
  a = c ∧ b = d

go in data\rat\basic.lean? What should this be named, rat_id is probably not right.

[Paul van Wamelen]

I prove that by first proving (the even more poorly named):

import data.rat.basic
import data.int.gcd
import tactic

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
  a = ((a : ℚ) / b).num ∧ b = ((a : ℚ) / b).denom :=
begin
  have h2 : (a : ℚ) / b = rat.mk ((a : ℚ) / b).num ((a : ℚ) / b).denom, { rw rat.num_denom },
  rw ←rat.mk_eq_div at h2,
  have h3 : a * ((a : ℚ) / b).denom = ((a : ℚ) / b).num * b,
  { apply (rat.mk_eq _ _).1, rw h2,
    rw ←rat.mk_eq_div, exact (ne_of_lt hb0).symm,
    simp only [rat.denom_ne_zero, int.coe_nat_eq_zero, ne.def, not_false_iff] },
  have h4 : int.nat_abs b ∣ int.nat_abs (a * ((a : ℚ) / b).denom),
  { exact int.nat_abs_dvd_abs_iff.2 (dvd_of_mul_left_eq _ h3.symm) },
  have h5 : int.nat_abs b ∣ int.nat_abs a * ((a : ℚ) / b).denom, { rw int.nat_abs_mul at h4, exact h4 },
  have h6 : int.nat_abs b ∣ ((a : ℚ) / b).denom,
  { apply nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm h) h5 },
  have h7 : ((a : ℚ) / b).denom ∣ int.nat_abs ((a : ℚ) / b).num * int.nat_abs b,
  { rw ←int.nat_abs_mul,
    change int.nat_abs ((a : ℚ) / b).denom ∣ int.nat_abs (((a : ℚ) / b).num * b),
    apply int.nat_abs_dvd_abs_iff.2,
    apply dvd_of_mul_left_eq _ h3
  },
  have h8 : ((a : ℚ) / b).denom ∣ int.nat_abs b,
  { exact nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm ((a : ℚ) / b).cop) h7 },
  have h9 : ((a : ℚ) / b).denom = int.nat_abs b, { exact nat.dvd_antisymm h8 h6 },
  have h10 : (((a : ℚ) / b).denom : ℤ) = b,
  { rw [int.eq_nat_abs_of_zero_le (le_of_lt hb0)] {occs := occurrences.pos [2]}, rw h9 },
  apply and.intro _ h10.symm,
  rw h10 at h3,
  exact (domain.mul_left_inj (ne_of_lt hb0).symm).mp h3
end

This proof seems a bit long. Any suggestions for improving this?

[Paul van Wamelen]

All the haves are poor form also, right?

[Yakov Pechersky]

Shouldn't something like h10 : (((a : ℚ) / b).denom : ℤ) = b be a simp lemma as it is?

[Paul van Wamelen]

denom is the "canonical" denominator. That is, denom of (-2)/(-6) is 3.

[Paul van Wamelen]

This is slightly better:

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
  a = ((a : ℚ) / b).num ∧ b = ((a : ℚ) / b).denom :=
begin
  have h2 : (a : ℚ) / b = rat.mk ((a : ℚ) / b).num ((a : ℚ) / b).denom, { rw rat.num_denom },
  rw ←rat.mk_eq_div at h2,
  have h3 : a * ((a : ℚ) / b).denom = ((a : ℚ) / b).num * b,
  { apply (rat.mk_eq ((ne_of_lt hb0).symm) _).1,
    { rw h2, rw ←rat.mk_eq_div },
    { simp only [rat.denom_ne_zero, int.coe_nat_eq_zero, ne.def, not_false_iff] }},
  have h4 : int.nat_abs b ∣ ((a : ℚ) / b).denom,
  { apply nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm h),
    change b.nat_abs ∣ int.nat_abs a * int.nat_abs ((a : ℚ) / (b : ℚ)).denom,
    rw ←int.nat_abs_mul, exact int.nat_abs_dvd_abs_iff.2 (dvd_of_mul_left_eq _ h3.symm) },
  have h5 : ((a : ℚ) / b).denom ∣ int.nat_abs b,
  { apply nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm ((a : ℚ) / b).cop),
    rw ←int.nat_abs_mul,
    change int.nat_abs ((a : ℚ) / b).denom ∣ int.nat_abs (((a : ℚ) / b).num * b),
    apply int.nat_abs_dvd_abs_iff.2,
    apply dvd_of_mul_left_eq _ h3
  },
  have h6 : ((a : ℚ) / b).denom = int.nat_abs b, { exact nat.dvd_antisymm h5 h4 },
  have h7 : (((a : ℚ) / b).denom : ℤ) = b,
  { rw [int.eq_nat_abs_of_zero_le (le_of_lt hb0)] {occs := occurrences.pos [2]}, rw h6 },
  apply and.intro _ h7.symm,
  rw h7 at h3,
  exact (domain.mul_left_inj (ne_of_lt hb0).symm).mp h3
end

[Kenny Lau]

import data.rat.basic tactic

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
  (a / b : ℚ).num = a ∧ ((a / b : ℚ).denom : ℤ) = b :=
begin
  lift b to ℕ using le_of_lt hb0,
  norm_cast at hb0 h,
  rw [← rat.mk_eq_div, ← rat.mk_pnat_eq a b hb0, rat.mk_pnat_num, rat.mk_pnat_denom,
    pnat.mk_coe, h.gcd_eq_one, int.coe_nat_one, int.div_one, nat.div_one],
  split; refl
end

[Kenny Lau]

using simp:

import data.rat.basic tactic

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
  (a / b : ℚ).num = a ∧ ((a / b : ℚ).denom : ℤ) = b :=
begin
  lift b to ℕ using le_of_lt hb0,
  norm_cast at hb0 h,
  rw [← rat.mk_eq_div, ← rat.mk_pnat_eq a b hb0],
  split; simp [rat.mk_pnat_num, rat.mk_pnat_denom, h.gcd_eq_one]
end

[Kenny Lau]

(why aren't those simp lemmas?)

[Paul van Wamelen]

Ah, I missed rat.mk_pnat_num, and rat.mk_pnat_denom!