scratch
§ Less than Versus Less than or Equals over Z
created 2022-09-28 · last edited 2023-04-02
- 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.
❦