Zulip Chat Archive

Stream: general

Topic: hole? golf!


view this post on Zulip Johan Commelin (Apr 21 2020 at 12:10):

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

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 12:14):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:16):

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 _ _)

view this post on Zulip Kenny Lau (Apr 21 2020 at 12:16):

yay my proof is shorter

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:18):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 12:19):

looks like you have no imports?

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:19):

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

view this post on Zulip Reid Barton (Apr 21 2020 at 12:21):

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 _ _)

view this post on Zulip Bhavik Mehta (Apr 21 2020 at 12:21):

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)

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:22):

night owl

view this post on Zulip Johan Commelin (Apr 21 2020 at 12:22):

name checks out

view this post on Zulip Kenny Lau (Apr 21 2020 at 12:22):

cheater

view this post on Zulip Reid Barton (Apr 21 2020 at 12:24):

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

theorem modeq_iff_dvd_of_le (a  b) : a  b [MOD n]  n  b - a

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:24):

I like the statement golfing

view this post on Zulip Reid Barton (Apr 21 2020 at 12:25):

removed an extraneous space to make it shorter

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:26):

I would skip the of_le in the name

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:26):

unless you want another version when it's not of_le

view this post on Zulip Kenny Lau (Apr 21 2020 at 12:27):

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

view this post on Zulip Reid Barton (Apr 21 2020 at 12:27):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:28):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 12:29):

Oh I see this is for nats

view this post on Zulip Reid Barton (Apr 21 2020 at 12:29):

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


Last updated: May 16 2021 at 21:11 UTC