Zulip Chat Archive

Stream: new members

Topic: Pythagorean triples


Paul van Wamelen (May 24 2020 at 20:51):

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 (May 24 2020 at 21:15):

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

Yury G. Kudryashov (May 24 2020 at 23:39):

Do you prove rational parametrization of the circle?

Jalex Stark (May 25 2020 at 00:48):

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 (May 25 2020 at 00:51):

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

Paul van Wamelen (May 25 2020 at 01:55):

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

Yury G. Kudryashov (May 25 2020 at 03:10):

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 (May 25 2020 at 03:20):

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 (May 25 2020 at 09:13):

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

Paul van Wamelen (Jun 21 2020 at 19:14):

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 (Jun 21 2020 at 19:19):

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 (Jun 21 2020 at 19:21):

All the haves are poor form also, right?

Yakov Pechersky (Jun 21 2020 at 19:33):

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

Paul van Wamelen (Jun 21 2020 at 19:44):

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

Paul van Wamelen (Jun 21 2020 at 19:45):

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 (Jun 21 2020 at 20:13):

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 (Jun 21 2020 at 20:15):

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 (Jun 21 2020 at 20:15):

(why aren't those simp lemmas?)

Paul van Wamelen (Jun 21 2020 at 20:29):

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


Last updated: Dec 20 2023 at 11:08 UTC