Small contribution

Stream: new members

[Harry Pacitti]

Hi everyone,
I'm a beginner Lean user and want to start contributing. I've been working on Pythagorean Triples and proved that for a primitive triple (a, b, c), exactly one of a or b is divisible by 3. I was wondering if the proof would be worth contributing? If so, would it be worth showing exactly one of a or b is divisible by four? Only the case involving 2 is in the library.

import number_theory.pythagorean_triples
import tactic.ring

lemma sq_ne_two_fin_zmod_three (z : zmod 3) : z * z ≠ 2 :=
begin
  change fin 3 at z,
  fin_cases z; norm_num [fin.ext_iff, fin.coe_bit0, fin.coe_bit1],
end

lemma int.sq_ne_two_mod_three (z : ℤ) : (z * z) % 3 ≠ 2 :=
suffices ¬ (z * z) % (3 : ℕ) = 2 % (3 : ℕ), by norm_num at this,
begin
  rw ← zmod.int_coe_eq_int_coe_iff',
  simpa using sq_ne_two_fin_zmod_three _,
end

variables {x y z : ℤ}

lemma mod_three_eq_zero_or_one_or_two (n : ℤ) : n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2 :=
have h : n % 3 < 3 := abs_of_nonneg (show 0 ≤ (3 : ℤ), from dec_trivial) ▸ int.mod_lt _ dec_trivial,
have h₁ : 0 ≤ n % 3 := int.mod_nonneg _ dec_trivial,
match (n % 3), h, h₁ with
| (0:ℕ) := λ _ _, or.inl rfl
| (1 : ℕ) := λ _ _, or.inr (or.inl rfl)
| (2 : ℕ) := λ _ _, or.inr (or.inr rfl)
| (k + 3 : ℕ) := λ h _, absurd h dec_trivial
| -[1+ a] := λ _ h₁, absurd h₁ dec_trivial
end

variables (h : pythagorean_triple x y z)

include h

lemma exact_one_div_three (hc : int.gcd x y = 1) :
  (x % 3 = 0 ∧ y % 3 = 1) ∨ (x % 3 = 0 ∧ y % 3 = 2) ∨ (x % 3 = 1 ∧ y % 3 = 0) ∨ (x % 3 = 2 ∧ y % 3 = 0) :=
begin
  rcases mod_three_eq_zero_or_one_or_two x with hx | hx | hx ;
    rcases mod_three_eq_zero_or_one_or_two y with hy | hy | hy,
  {-- x % 3 = 0, y % 3 = 0
  exfalso,
  apply nat.not_coprime_of_dvd_of_dvd (dec_trivial : 1 < 3) _ _ hc,
  {apply int.dvd_nat_abs_of_of_nat_dvd, apply int.dvd_of_mod_eq_zero hx },
  {apply int.dvd_nat_abs_of_of_nat_dvd, apply int.dvd_of_mod_eq_zero hy}},
  {left, exact ⟨ hx, hy ⟩}, --x % 3 = 0, y % 3 = 1
  {right,left, exact ⟨ hx, hy ⟩}, --x % 3 = 0, y % 3 = 2
  {right, right, left, exact ⟨ hx, hy ⟩}, --x % 3 = 1, y % 3 = 1
  {-- x % 3 = 1, y % 3 = 1
    exfalso,
    obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0* 3 + 1 ∧ y = y0 * 3 + 1,
    { cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hx) with x0 hx2,
      cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hy) with y0 hy2,
      rw sub_eq_iff_eq_add at hx2 hy2, exact ⟨x0, y0, hx2, hy2⟩ },
    apply int.sq_ne_two_mod_three z,
    rw show z * z = 3 * (3 * x0 * x0 + 2 * x0 + 2 * y0 + 3 * y0 * y0 ) + 2, by { rw ← h.eq, ring },
    rw [int.add_mod, int.mul_mod_right, zero_add, int.mod_mod], norm_num,},
  {--x % 3 = 1, y % 3 = 2
    exfalso,
    obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0* 3 + 1 ∧ y = y0 * 3 + 2,
    { cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hx) with x0 hx2,
      cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hy) with y0 hy2,
      rw sub_eq_iff_eq_add at hx2 hy2, exact ⟨x0, y0, hx2, hy2⟩ },
    apply int.sq_ne_two_mod_three z,
     rw show z * z = 3 * (3 * x0 * x0 + 2 * x0 + 4 * y0 + 3 * y0 * y0 ) + 5, by { rw ← h.eq, ring },
    rw [int.add_mod, int.mul_mod_right, zero_add, int.mod_mod], norm_num,},
  {right ,right ,right ,exact ⟨hx, hy⟩ },
  {--x % 3 = 2, y % 3 = 1
    exfalso,
    obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0* 3 + 2 ∧ y = y0 * 3 + 1,
    { cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hx) with x0 hx2,
      cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hy) with y0 hy2,
      rw sub_eq_iff_eq_add at hx2 hy2, exact ⟨x0, y0, hx2, hy2⟩ },
    apply int.sq_ne_two_mod_three z,
     rw show z * z = 3 * (3 * x0 * x0 + 4 * x0 + 2 * y0 + 3 * y0 * y0 ) + 5, by { rw ← h.eq, ring },
    rw [int.add_mod, int.mul_mod_right, zero_add, int.mod_mod],
    norm_num,},
  {--x % 3 = 2, y % 3 = 1
    exfalso,
    obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0* 3 + 2 ∧ y = y0 * 3 + 2,
    { cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hx) with x0 hx2,
      cases exists_eq_mul_left_of_dvd (int.dvd_sub_of_mod_eq hy) with y0 hy2,
      rw sub_eq_iff_eq_add at hx2 hy2, exact ⟨x0, y0, hx2, hy2⟩ },
    apply int.sq_ne_two_mod_three z,
     rw show z * z = 3 * (3 * x0 * x0 + 4 * x0 + 4 * y0 + 3 * y0 * y0 ) + 8, by { rw ← h.eq, ring },
    rw [int.add_mod, int.mul_mod_right, zero_add, int.mod_mod],
    norm_num,},
end

[Eric Wieser]

Which lemma is the one already in the library?

[Harry Pacitti]

Eric Wieser said:

Which lemma is the one already in the library?

I've put the lemma I meant below from number_theory.pythagorean_triples

even_odd_of_coprime

[Eric Wieser]

docs#even_odd_of_coprime?

[Harry Pacitti]

Eric Wieser said:

docs#pythagorean_triple.even_odd_of_coprime

Yes, that's the one.

[Eric Wieser]

Is it true more generally as n \dvd x ↔ ¬(n \dvd y) for nonsquare n?

[Eric Wieser]

To answer your original question though, this statement looks like a great first (or subsequent) contribution to me. I suspect reviewers can shorten the proof a little, but that's all part of the contribution process.

[Damiano Testa]

Also, consider that dec_trivial can get you quite far. This means that you need to do less work:

def my_pyt {R : Type*} [semiring R] (x y z : R) : Prop := x * x + y * y = z * z

variables {R S : Type*} [semiring R] [semiring S] {x y z : R} (f : R →+* S)

lemma pyt_map (h : my_pyt x y z) : my_pyt (f x) (f y) (f z) :=
by simpa only [map_add, map_mul] using congr_arg ⇑f h
end my

lemma int.my_pyt_iff {x y z : ℤ} : my_pyt x y z ↔ pythagorean_triple x y z := iff.rfl

variables {x y z : zmod 3}

lemma eq_zero_or_of_pyt (h : my_pyt x y z) :
  (x = 0 ∨ y = 0) ∨ (x = 0 ∧ y = 1) ∨ (x = 0 ∧ y = 2) ∨ (x = 1 ∧ y = 0) ∨ (x = 2 ∧ y = 0) :=
begin
  unfold my_pyt at h,
  dec_trivial!,
end