Division by Remainder

Stream: new members

[Will Midwood]

Hi all,
I'm trying to construct my first theorem in lean:
For all integers a & b with b > 0, There exists integers p & r such that a = b*q + r and 0 ≤ r < b
Currently, I have got:

theorem div_by_rem (a b : ℤ) (hb : 0 < b) : ∃ (q r : ℤ), (a = b*q + r)∧(0 ≤ r)∧(r<b) :=
begin
    sorry,
end

I'm just wanting some confirmation that this is indeed the right construction.And if so, can this be proven using induction?
Thanks <3, and apologies if this is the wrong place for this!

[Damiano Testa]

Depending on how much of mathlib you want to use, most of the work is already done for you. In particular, so much is already done, that in the proof below, I did not need to explicitly use induction!

import data.int.basic

theorem div_by_rem (a b : ℤ) (hb : 0 < b) : ∃ (q r : ℤ), (a = b*q + r)∧(0 ≤ r)∧(r<b) :=
⟨a / b, a % b, ⟨(a.div_add_mod b).symm, a.mod_nonneg hb.ne', a.mod_lt_of_pos hb⟩⟩

In any case, this is the right place to ask these questions!

[Damiano Testa]

(By the way, I compressed the proof on purpose, in case you wanted to take a peak and then regretted it. There are more educational ways of rewriting the hidden proof above.)

[Kevin Buzzard]

Yes, the theorem is correct as stated. I would not embark upon a Lean proof unless you know a mathematical proof first. Damiano's spoilered one-line proof uses the fact that the result is already in the library. If you want to prove it yourself by induction on a then you need a principle of induction appropriate for integers; you could start like this:

theorem div_by_rem (a b : ℤ) (hb : 0 < b) : ∃ (q r : ℤ), (a = b*q + r)∧(0 ≤ r)∧(r<b) :=
begin
  apply int.induction_on a,
  ...
end

[Kyle Miller]

There's also docs#int.div_mod_unique which is essentially the statement, though leaving it to you to know about a / b and a % b.

import data.int.basic

theorem div_by_rem (a b : ℤ) (hb : 0 < b) : ∃ (q r : ℤ), a = b * q + r ∧ 0 ≤ r ∧ r < b :=
begin
  refine ⟨a / b, a % b, _⟩,
  rw [eq_comm, add_comm, ← int.div_mod_unique hb],
  exact ⟨rfl, rfl⟩,
end

[Kyle Miller]

In any case, take the existence of Damiano's and my spoilers as being proof that you have the correct construction!

[Will Midwood]

Thank you everyone! I want to prove this theorem without the already existing math-lib statement, hence the induction question :). I will leave this issue open incase I have any issues writing my proof. Thanks again!

[Damiano Testa]

A suggestion. As part of the induction, you will have to prove the result when a is a natural number. Begin by proving just this result, since most of the content is there anyway.

[Damiano Testa]

If you do that, then you can prove the full result using this partial one, and the final proof will be simpler.

[Kevin Buzzard]

I agree that doing nat would be a good warm-up (and there you can just usual nat induction). I'm not so sure that going from nat to int (i.e. using the nat result to deduce the int one) will be any easier than doing int directly by induction (but I am open to being proved wrong!)

[Damiano Testa]

Kevin, you are probably right: most of the time is spent dealing with the top or the bottom of the interval [0, b) and they get swapped by the minus sign: I cannot see a way of making substantial use of the nat case in the -nat case, other than that to a human they look very similar proofs!

[Will Midwood]

Hi there, still attempting this proof. I have a very good idea on how to complete the proof, but can't seem to continue past this goal:

a b : ℤ,
hb : 0 < b,
d : ℕ,
qd rd : ℤ,
hr : ↑d = b * qd + rd,
hm : 0 ≤ rd,
hl : rd < b
⊢ rd + 1 = b ∨ rd + 1 < b

I feel like this is obvious and/or the definition of rd < b, but don't know what proofs or tactics I could use. Thanks in advance for any help

[Kyle Miller]

You should be able to use docs#eq_or_lt_of_le along with docs#int.add_one_le_iff

[Kyle Miller]

like apply eq_or_lt_of_le, rw int.add_one_le_iff, exact hl (I definitely did not test this)

[Will Midwood]

Thank you @Kyle Miller ! Very helpful

[Kevin Buzzard]

PS it's neither obvious nor the definition of <. It's not obvious because the result is not true for eg the real numbers, so you must be using some non-formal fact about the integers. And it's not true by definition because who are you to decide what the internal definition of the fundamental structures on the naturals are? This is a question for the person who implements <, not the user. But you can trust that the implementor will have made an API for <, to ensure that for all the different definitions of < (and there are many), the theorem which would be true by definition if that were the definition will be in the library anyway. Asking what the definition of something like < is, is not the right question. It's like asking whether lean's reals are Cauchy sequences or Dedekind cuts -- this is not a mathematical question so it shouldn't matter. The important thing is knowing that the API is there. The theorems Kyle mentions break up your goal into a sequence of natural statements which one would expect to be in the library. The knack is to figure out what to expect.