Properties of floors, ceilings and modulus

Question

I'm trying to reduce one calculation in an iterative Successive Over-Relaxation procedure for a program I'm writing. The code that works does this calculation:

$$ s = \left\lfloor\frac{b + \left\lfloor\frac{2^{16}-1}{4}\right\rfloor}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor $$

Now, I think that the following two properties of floors/ceilings and modulus division hold up (or at least I couldn't find a contradicting set of inputs):

$$ \forall x\in\mathbb{N},y\in\mathbb{N}\left(\left\lfloor\frac{x-1}{y}\right\rfloor = \frac{x-y}{y} \leftrightarrow x\mod y = 0\right)\\ \forall x\in\mathbb{N},y\in\mathbb{N}\left(\left\lfloor\frac{x+y-1}{y}\right\rfloor=\left\lceil\frac{x}{y}\right\rceil\right) $$

So, according to the first property, because $2^{16}\mod4=0$, I can rewrite the above as:

$$ s=\left\lfloor\frac{b+\frac{2^{16}-4}{4}}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor = \left\lfloor\frac{b+\frac{2^{16}}{4}-1}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor $$

and since, again, $2^{16}\mod4=0$, it must be true that $\frac{2^{16}}{4}=\left\lfloor\frac{2^{16}}{4}\right\rfloor$, and so by the second property this can be re-written as:

$$ s=\left\lceil\frac{b}{\frac{2^{16}}{4}}\right\rceil = \left\lceil\frac{b}{2^{14}}\right\rceil $$

This usually gets me the right answer, but sometimes I get erroneous outputs, and I'm trying to eliminate this simplification of the original as the cause. Are those two properties really true? Or did I mess up in the actual simplification somewhere? Or is it actually fine and the flaw is probably elsewhere?

Bonus Question

Should those statements above be written as $\forall x\in\mathbb{N},y\in\mathbb{N}$ or $\forall(x,y)\in\mathbb{N}^2$? Or are those equivalent? I'll edit my question as appropriate/if needed according to any comments on the formatting.

Answer 1

$\newcommand{\fl}[1]{\left\lfloor #1 \right\rfloor}$ $\newcommand{\ce}[1]{\left\lceil #1 \right\rceil}$

The first claim is correct, if you assume that $x \geq y$.

Proof of 1: For ($\implies$), $\frac{x-y}{y}$ must be an integer, so $x$ is a multiple of $y$, in other words $x \equiv 0 \ (\textrm{mod}\ y)$. For ($\impliedby$), note that $x=ky$, so $\frac{x-y}{y}=k-1$, and $\left\lfloor \frac{x - 1}{y} \right\rfloor = \left\lfloor k - \frac{1}{y} \right\rfloor = k - 1$ whenever $y$ is positive.

The second claim is also true. Proof:

Case 1: $\fl{\frac{x}{y}} = \frac{x}{y} = \ce{\frac{x}{y}}$. Since $0 < \frac{1}{y} < 1, \fl{\frac{x}{y}} - 1 < \frac{x}{y} - \frac{1}{y} < \ce{\frac{x}{y}}$, and so $\fl{\frac{x}{y} - \frac{1}{y}} + 1 = \ce{\frac{x}{y}}$.

Case 2: $\frac{x}{y} - \frac{1}{y} < \fl{\frac{x}{y}}$: Note that $\fl{\frac{x}{y}} \leq \frac{x}{y}$. Together with the assumption, this implies that $\fl{\frac{x}{y}} = \frac{x}{y}$, reducing to case 1.

Case 3: $\fl{\frac{x}{y}} \leq \frac{x}{y} - \frac{1}{y} < \frac{x}{y} < \ce{\frac{x}{y}}$: The result is obvious.

So I don't know what's wrong with your simulation. It should work fine.

Answer 2

$$s=\left\lfloor\frac{b+16383}{16384}\right\rfloor=\left\lfloor\frac{b-1}{16384}\right\rfloor+1$$ makes a unit jump from $k$ to $k+1$ at every $16384 k+1$ (included) while

$$s'=\left\lceil\frac b{16384}\right\rceil$$ does it at $16384k$ (excluded).

You can't replace a floor by a ceiling, unless the arguments are fractions with a bounded denominator.