help with proof strategy to show a mod b is unique

Stream: new members

[rzeta0]

I've been struggling with an MoP exercise and specifically struggling with the Lean aspects.

So I thought I'd get some sleep, and start afresh at the overall proof strategy.

If the proof strategy is sensible, then I'll be justified in struggling with the Lean implementation,

I'd welcome thoughts on the following proof strategy:

---

Task:

Let  $a$ and $b$  be integers, with  $b>0$. Let $r$ and $s$  be integers, both in the range $0 \le r < b$,  and $0 \le s < b$ both congruent to $a$  modulo $b$. Show that they are equal.

Strategy:

1. Definitions tell us $a - r = b \cdot m$, and $a - s = b \cdot n$ for some integers $m, n$.

2. Algebra gives us $r-s = b \cdot (n - m)$, re-arranged to the more useful $\frac{r-s}{b}= n-m$.

3. We have 3 cases: $r-s < 0$, $r-s > 0$, $r-s = 0$. So this is a proof by cases.

4. Since, by definition, $r$ and $s$ are both less than $b$, then LHS $\frac{r-s}{b}$ has magnitude less than 1. The RHS $n-m$ must be an integer, and so the LHS $\frac{r-s}{b}$ can only be zero.

That is, two of the three cases have been ruled out, leaving only $r-s=0$.

---

I think the "upcasting" to show the fraction must have magnitude less than 1 might be a challenge for me.

[Dan Velleman]

Here's a strategy that avoids cases: Show that $-b < r - s < b$. Then, since you have $r - s = b \cdot (n - m)$, you can conclude $-b < b \cdot (n - m) < b$. Deduce from this that $-1 < n - m < 1$. But $n - m$ is an integer, so it must be 0.

There is a proof similar to this in Section 7.3 of of How To Prove It with Lean.

[rzeta0]

Thanks Dan - I will study this approach.

I was running into errors associated with division, so avoiding even division will be good too.

failed to synthesize instance
  HDiv ℤ ℤ ?m.163069

[Aaron Liu]

You should convert to Rat before introducing division, since dividing integers has rounding.

[Dan Velleman]

...Or avoid division altogether by looking for a theorem about canceling b from both sides of an inequality.

[Ruben Van de Velde]

There's lemmas like this, for example:
@loogle ?b * ?c < ?b

[loogle]

:search: lt_one_of_mul_lt_right, mul_lt_of_lt_one_right', and 4 more