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
Since B is positive, the
N.log2 B' th bits of
B are both 1, so the k'th bit of
N.lxor A B is 0. Therefore
N.lxor A B agree up to
N.log2 B'th bit, at which point
N.lxor A B becomes smaller than
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!
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).
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
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
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
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
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