golf `nat.coprime` proof

Stream: Is there code for X?

[Heather Macbeth]

I wanted to remove the unnecessary consideration of prime factors from the following lemma, keeping the imports elementary.

lemma coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) :
  nat.coprime a n :=

Note that by definition a * b ≡ 1 [MOD n] means (a * b) % n = 1 % n and nat.coprime a n means a.gcd n = 1. So basically this is just the lemma that if N * k + 1 = a * b then a.gcd N = 1.

You can see my 14-line version on #16811, any golfing?

[Eric Rodriguez]

this works, using mostly your proof:

lemma coprime_of_mul_modeq_one : ∀ (b : ℕ) {a n : ℕ}, a * b ≡ 1 [MOD n] → coprime a n
| b a 0 h := (coprime_zero_right _).mpr (eq_one_of_mul_eq_one_right $ modeq_zero_iff.mp h)
| b a 1 h := coprime_one_right _
| b a (n+2) (h : _ = _) :=
begin
  rw [coprime_iff_gcd_eq_one, ←nat.dvd_one, ←nat.dvd_add_right $ (gcd_dvd_right a _).mul_right _],
  convert (gcd_dvd_left a _).mul_right b,
  simpa only [h, one_mod] using nat.div_add_mod (a * b) (n + 2),
end

it's a bit metavariably sadly, you can fill in the holes on the righthand of the first rw but it makes it a line longer

[Eric Rodriguez]

it'd be nice if there was also a definitional lemma for modeq so I don't have to do the horrendous (h : _ = _)

[Eric Rodriguez]

the equation compiler style is very underutilised I find

[Michael Stoll]

lemma coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : coprime a n :=
begin
  cases eq_or_ne (a * b) 0 with h₀ h₀,
  { rw [h₀] at h,
    exact (nat.eq_one_of_dvd_one (nat.modeq_zero_iff_dvd.mp h.symm)).substr (nat.coprime_one_right a), },
  have h₁ := nat.one_le_iff_ne_zero.mpr h₀,
  obtain ⟨k, hk⟩ := (nat.modeq_iff_dvd' h₁).mp h.symm,
  rw nat.sub_eq_iff_eq_add h₁ at hk,
  exact nat.eq_one_of_dvd_one ((nat.dvd_add_iff_right $ (nat.gcd_dvd_right a n).trans
    (dvd_mul_right n k)).mpr $ hk ▸ (nat.gcd_dvd_left a n).trans (dvd_mul_right a b)),
end

[Heather Macbeth]

Thank you both!

[Michael Stoll]

One can save another line by inlining h₁, but I assume this would be a bit less efficient...

[Alex J. Best]

import data.nat.modeq
.
lemma coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) :
  nat.coprime a n :=
begin
  by_contra hd,
  obtain ⟨p, hp, hpa, ⟨d, rfl⟩⟩ := nat.prime.not_coprime_iff_dvd.mp hd,
  exact nat.not_prime_one (nat.dvd_one.mp (nat.modeq_zero_iff_dvd.mp
    ((nat.modeq.of_modeq_mul_right d h).symm.trans
    (zero_mul b ▸ (nat.modeq_zero_iff_dvd.mpr hpa).mul_right b))) ▸ hp),
end

[Heather Macbeth]

But @Alex J. Best , I'm trying to avoid primes!

[Alex J. Best]

Oops! Thats what I get for diving straight into lean xD

[Heather Macbeth]

As I complain on #16811, nat.prime imports all kinds of rubbish ... complete boolean algebras, modules, ...

[Yaël Dillies]

Don't call my beautiful orders rubbish :rofl:

[Alex J. Best]

What about this? Instead of using a prime just using the gcd, maybe I'm just redoing the above now lol

import data.nat.modeq
.
lemma coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) :
  nat.coprime a n :=
begin
  obtain ⟨g, hh⟩ := nat.gcd_dvd_right a n,
  by_contra hd,
  exact (mt nat.coprime_iff_gcd_eq_one.mpr hd) (nat.dvd_one.mp (nat.modeq_zero_iff_dvd.mp
    ((nat.modeq.of_modeq_mul_right g (hh.subst h)).symm.trans
    (zero_mul b ▸ (nat.modeq_zero_iff_dvd.mpr (nat.gcd_dvd_left _ _)).mul_right b)))),
end

[Eric Rodriguez]

I do often wish we could do as Anne wanted and import specific lemmas and only their requirements, but that's for the computer scientists to figure out :)

[Vincent Beffara]

Eric Rodriguez said:

I do often wish we could do as Anne wanted and import specific lemmas and only their requirements, but that's for the computer scientists to figure out :)

One way to make this possible would be to split mathlib into many more files (though perhaps not one .lean file per lemma). It would also make parallel builds easier. I'm assuming that the reason the files in mathlib are so big is that doing otherwise would make build times a lot bigger?

[Kevin Buzzard]

Files have always been huge. I think data.multiset.basic was already thousands of lines long in 2017 when I joined. So it might be more cultural than anything else. Also, it's easier to just PR an addition to a file than to start reorganising things.

[Scott Morrison]

There's a balance: too many small files makes finding related material hard. But we almost certainly still err much too far on the side of large files, with too many imports that are only relevant for short sections.

[Anne Baanen]

I've been trying to be critical on the import structure during reviews, suggesting to create a new file rather than doing a heavy import. But there's still quite a bit of nontrivial dependencies coming with innocuous imports.

[Heather Macbeth]

I went with the following un-golfed version of @Alex J. Best's proof:

lemma coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : coprime a n :=
begin
  obtain ⟨g, hh⟩ := nat.gcd_dvd_right a n,
  rw [nat.coprime_iff_gcd_eq_one, ← nat.dvd_one, ← nat.modeq_zero_iff_dvd],
  calc 1 ≡ a * b [MOD a.gcd n] : nat.modeq.of_modeq_mul_right g (hh.subst h).symm
  ... ≡ 0 * b [MOD a.gcd n] : (nat.modeq_zero_iff_dvd.mpr (nat.gcd_dvd_left _ _)).mul_right b
  ... = 0 : by rw zero_mul,
end

[Alex J. Best]

That's actually way nicer, and the same line count :wink: