§ Less than versus Less than or equals over Z
- If we have a theorem whose hypotheses and goal are of the form
a <= b - 1 for
a, b integers, is it always safe to replace these with
a < b? Shockingly, no!
- Consider the theorem:
(a <= n - 1) => (2a <= 2n - 2).
- When we lose the information to
. < ., it becomes
(a < n) => (2a < 2n - 1).
- But this can't be proved, because the best we can do is
(a < n) => 2a < 2n!
- The key reason is that even though
(a < n) <-> (a <= n - 1) is an equivalence, we can't always rewrite with an equivalence under an inequality!
- Said differently,
a <= n - 1 is equivalent to
a < n, but once we start performing algebra on these, we start seeing the difference.
- This came up in the context of delinearization. I was trying to prove that if
i < N and
j < M, then
iM + j < NM.
- This proof, while state in terms of
<, actually needs us to go through
i <= (N - !), so
iM <= NM - M, so
iM + j <= (NM - M) + (M - 1), which means
iM + j <= M - 1, or
iM < M.