Zulip Chat Archive

Stream: new members

Topic: nat_add_div


Julian Külshammer (Jan 12 2021 at 12:00):

I tried to practice some induction in lean and in the process used division on nat (which I know from discussions here one should try to avoid). If one decides to use it anyway, I found the following lemma helpful:

import tactic

lemma add_div'' (a b c : ) (hca : c  a) (hba : c  b) :
(a+b)/c=a/c+b/c :=
begin
-- We can prove the statement by splitting into cases: Either c=0,
-- in which case the statement holds by definition or c>0, in which
-- case we have to work.
cases le_or_gt c 0 with hc hc,
{ rw nat.le_zero_iff at hc,
rw hc,
simp only [nat.div_zero]
},
-- As / is defined as the floor function on / on ℕ, we can multiply
-- by c to obtain the result provided that c ∣ (a+b) and c>0.
apply (nat.div_eq_iff_eq_mul_right _ _).mpr,
{
-- We show that (a+b)=c(a/c+b/c) using that c∣a and c∣b by assumption.
rw mul_add,
rw nat.mul_div_cancel',
rw nat.mul_div_cancel',
assumption,
assumption},
-- c>0 in this case.
assumption,
-- c ∣ (a+b) holds since c∣a and c∣b.
exact dvd_add hca hba
end

Is this somewhere in mathlib? The only thing I could find was the following in data/nat/modeq.lean and I didn't manage to use it.

lemma add_div {a b c : } (hc0 : 0 < c) : (a + b) / c = a / c + b / c +
  if c  a % c + b % c then 1 else 0

Johan Commelin (Jan 12 2021 at 12:12):

@Julian Külshammer it doesn't seem to be in mathlib, and I agree that it looks useful

Ruben Van de Velde (Jan 12 2021 at 12:15):

You could use add_div like this:

import tactic
import data.nat.modeq

lemma add_div'' (a b c : ) (hca : c  a) (hba : c  b) :
(a+b)/c=a/c+b/c :=
begin
-- We can prove the statement by splitting into cases: Either c=0,
-- in which case the statement holds by definition or c>0, in which
-- case we have to work.
cases le_or_gt c 0 with hc hc,
{ rw nat.le_zero_iff at hc,
  rw hc,
  simp only [nat.div_zero] },

rw [nat.add_div hc, if_neg, add_zero],
rw [nat.mod_eq_zero_of_dvd hca, nat.mod_eq_zero_of_dvd hba, add_zero],
exact hc.lt.not_le,
end

Eric Wieser (Jan 12 2021 at 12:29):

Golfed using docs#nat.add_div_eq_of_add_mod_lt

lemma nat.add_div_eq_of_dvd (a b c : ) (hca : c  a) (hba : c  b) :
  (a + b)/c = a/c + b/c :=
if h : c = 0 then by simp [h] else nat.add_div_eq_of_add_mod_lt begin
  rw [nat.mod_eq_zero_of_dvd hca, nat.mod_eq_zero_of_dvd hba, zero_add],
  exact nat.pos_of_ne_zero h,
end

Alex J. Best (Jan 12 2021 at 14:43):

Are both assumptions necessary, they are there in docs#int.add_div_of_dvd too, but it seems to me you only need c\|a or c\|b in both the nat and int versions?

Eric Wieser (Jan 12 2021 at 14:45):

No, they're not necessary, which is why docs#nat.add_div_eq_of_add_mod_lt exists

Eric Wieser (Jan 12 2021 at 14:46):

But I guess the fact we have the lemma for int is an argument in itself for having nat.add_div_of_dvd

Alex J. Best (Jan 12 2021 at 14:48):

Oh I agree we should have the lemma! But let's add the best version, and fix the old one too :smile:

Alex J. Best (Jan 12 2021 at 15:17):

import tactic
import data.nat.modeq

lemma nat.add_div_eq_of_dvd {a b c : } (hca : c  a) :
  (a + b)/c = a/c + b/c :=
if h : c = 0 then by simp [h] else nat.add_div_eq_of_add_mod_lt begin
  rw [nat.mod_eq_zero_of_dvd hca, zero_add],
  exact nat.mod_lt _ (pos_iff_ne_zero.mpr h),
end

Eric Wieser (Jan 12 2021 at 15:34):

Why hca over hcb?

Eric Wieser (Jan 12 2021 at 15:35):

I mean, I guess commutativity of addition lets you recover the other one

Julian Külshammer (Jan 12 2021 at 20:02):

@Johan Commelin @Eric Wieser @Alex J. Best Thanks a lot for your comments and improvements.

Julian Külshammer (Jan 14 2021 at 20:54):

@Alex J. Best For int there is also docs#int.add_mul_div_left, which is basically the same but formulated slightly differently.

Alex J. Best (Jan 14 2021 at 20:55):

Ah, thank you! I had some vague memory that this already existed, but it must have been that version indeed

Julian Külshammer (Jan 14 2021 at 20:58):

Should the nat version be added anyway? For consistency maybe formulated in the same way?

Johan Commelin (Jan 14 2021 at 21:08):

@Julian Külshammer if the nat version is missing, then yes, please add it (if you are planning a PR)

Julian Külshammer (Jan 14 2021 at 22:14):

I can give it a try. Can you (or someone else) give me permission to push to a branch?

Johan Commelin (Jan 14 2021 at 22:14):

@Julian Külshammer what's your github username?

Julian Külshammer (Jan 14 2021 at 22:15):

Julian-Kuelshammer

Johan Commelin (Jan 14 2021 at 22:16):

@Julian Külshammer invitation sent

Julian Külshammer (Jan 14 2021 at 22:18):

Thanks.

Julian Külshammer (Jan 16 2021 at 09:19):

The corresponding PR (my first to mathlib) just got merged. Thanks everyone for the comments and improvements.

Johan Commelin (Jan 16 2021 at 09:46):

Congrats!


Last updated: Dec 20 2023 at 11:08 UTC