CODEWITHSUNDEEP
coqproof
Joald
Joald

Reputation: 1134

How to prove integer division inequality in Coq

I need to prove: 256 * (x / 256) <= 256 * x / 256, or more generally forall a b c : N, c > 0 -> a * (b / c) <= a * b / c. This is true since either b is divisible by c and they are equal or it's not and multiplying first can inflate the number and result in greater precision. However, I could not find any theorem in the standard library that proves this, and no automatic tactic I know (auto, intuition, easy, zify and omega) worked. If it helps, I also know that x < 256 * 256, but checking all 65536 cases is not a good proof...

Upvotes: 5

Views: 366

Answers (1)

Joald
Joald

Reputation: 1134

In my specific case I was able to solve it like this:

rewrite (N.mul_comm 256 x).

This switches around the right side to 256 * (x / 256) <= x * 256 / 256.

rewrite (N.div_mul x 256).

This reduced the right side to 256 * (x / 256) <= x.

rewrite (N.mul_div_le x 256).

After this automated tactics are sufficient.

Upvotes: 4

Related Questions