hole? golf!

Stream: general

[Johan Commelin]

Is this a hole in the library? What is the shortest proof?

lemma dvd_sub_mod (k : ℕ) : n ∣ (k - (k % n)) :=

[Kenny Lau]

lemma dvd_sub_mod (n k : ℕ) : n ∣ (k - (k % n)) :=
⟨k / n, nat.sub_eq_of_eq_add (nat.mod_add_div k n).symm⟩

[Mario Carneiro]

lemma dvd_sub_mod (n k : ℕ) : n ∣ k - k % n :=
⟨k / n, (nat.sub_eq_iff_eq_add (nat.mod_le _ _)).2 $
  (nat.mod_add_div _ _).symm.trans (add_comm _ _)⟩

[Kenny Lau]

yay my proof is shorter

[Mario Carneiro]

Damn you autocomplete
Screenshot-from-2020-04-21-05-17-09.png

[Kenny Lau]

looks like you have no imports?

[Mario Carneiro]

Oh, yes import data.nat.basic solves the problem

[Reid Barton]

The nat subtraction makes this annoying.

lemma dvd_sub_mod (n k : ℤ) : n ∣ (k - (k % n)) :=
int.modeq.modeq_iff_dvd.mp (int.modeq.mod_modeq _ _)

[Bhavik Mehta]

Mario Carneiro said:

Damn you autocomplete
Screenshot-from-2020-04-21-05-17-09.png

(entirely unrelated - which theme is this? I quite like it)

[Mario Carneiro]

night owl

[Johan Commelin]

name checks out

[Kenny Lau]

cheater

[Reid Barton]

maybe another hole is, in data.nat.modeq:

theorem modeq_iff_dvd_of_le (a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a

[Mario Carneiro]

I like the statement golfing

[Reid Barton]

removed an extraneous space to make it shorter

[Mario Carneiro]

I would skip the of_le in the name

[Mario Carneiro]

unless you want another version when it's not of_le

[Kenny Lau]

The nonunits make this annoying.

import ring_theory.euclidean_domain data.real.basic

lemma dvd_sub_mod (n k : ℝ) : n ∣ (k - (k % n)) :=
if H : n = 0 then by rw [H, euclidean_domain.mod_zero, sub_self]
else ⟨(k - k % n) / n, by rw mul_div_cancel' _ H⟩

[Reid Barton]

There's an existing theorem modeq_iff_dvd : a ≡ b [MOD n] ↔ (n:ℤ) ∣ b - a but maybe that should be the one with the altered name

[Mario Carneiro]

Yeah but that's in a different namespace, right?

[Mario Carneiro]

Oh I see this is for nats

[Reid Barton]

No this is for nats (MOD is for nat)--there's also theorem modeq_iff_dvd : a ≡ b [ZMOD n] ↔ (n:ℤ) ∣ b - a := in int.zmod