如何证明 Coq 中的整数除法不等式

Question

我需要证明：256 * (x / 256) <= 256 * x / 256，或更一般地说forall a b c : N, c > 0 -> a * (b / c) <= a * b / c。这是真的，因为要么 b 可以被 c 整除并且它们相等，要么不相等，首先乘法可以扩大数字并导致更高的精度。但是，我在标准库中找不到任何可以证明这一点的定理，而且我知道的任何自动策略（auto、intuition、easy、zify 和 omega）都不起作用。如果有帮助，我也知道x < 256 * 256，但是检查所有 65536 个案例并不是一个很好的证明......

Answer 1

在我的具体情况下，我能够像这样解决它：

rewrite (N.mul_comm 256 x).

这会将右侧切换到256 * (x / 256) <= x * 256 / 256。

rewrite (N.div_mul x 256).

这将右侧减少到256 * (x / 256) <= x。

rewrite (N.mul_div_le x 256).

这样自动化策略就足够了。