Zulip Chat Archive

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