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!

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 `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: Jun 16 2024 at 03:41 UTC