## Stream: Coq users

### Topic: Proof with BinNat and xor

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