Timothy Mou (Feb 21 2023 at 04:01): Timothy Mou (Feb 21 2023 at 04:01):I'm trying to prove the following goal:
Goal forall A B,
(B > 0%N) ->
N.testbit A (N.log2 B) = true ->
(N.lxor A B < A)%N.
I would explain why this is true like this: for k > N.log2 B, the k'th bit of N.lxor A B is equal to the k'th bit of A.
Since B is positive, the N.log2 B' th bits of A and B are both 1, so the k'th bit of N.lxor A B is 0. Therefore A and N.lxor A B agree up to N.log2 B'th bit, at which point N.lxor A B becomes smaller than A.
N.log2_lt_cancel seems close to what I want, except I want to show a < b if they agree up to a point, then a has a 0 bit while b has a 1 bit.
I would appreciate any help or any theorems I may have missed. Thanks!
Paolo Giarrusso (Feb 21 2023 at 05:36):N.bit_log2, N.bits_above_log2 and N.lxor_spec should allow proving your first step, describing the bits of B and of N.lxor A B. Relating N.testbit and < sounds more painful and will probably require intermediate steps or proving auxiliary theorems; maybe N.testbit_spec could help there (or maybe details of its proof, since there's an explicit construction of witnesses).
Timothy Mou (Feb 21 2023 at 22:08):Thanks for the suggestions! I ended up proving it with the following approach: if N.log2 A is greater than N.log2 B, that means we can subtract off 2^n from both A and N.lxor A B, decreasing the index of the highest one bit. We show that subtracting 2^n does not affect any other bits by relating it to N.ldiff.
We can continue until the highest one bit is N.log2 B, at which point we can use N.log2_lt_cancel to finish it off. It ended up being quite messy and involved some liberal usage of lia.
I think another approach would be to use N.testbit_spec, using the fact that we can write N.lxor A B as l + h*2^(n+1) and A as l' + 2^n + h'*2^(n+1). Then we should be able to show that h = h' and then subtract it off from both sides. Then since the RHS has a 2^n, it is larger than the LHS.
Last updated: Oct 04 2023 at 21:01 UTC