Zulip Chat Archive

Stream: general

Topic: Reasoning about bitwise xor


Markus Himmel (Aug 27 2020 at 20:24):

I'm currently stuck at this sorry about nat.lxor and I'd like to ask whether anyone has an idea how to tackle it. The pen-and-paper proof is as follows. By our hypothesis, v is not zero. Let i be the position of the most significant 1-bit of v. Then at least one of a, b or c has a 1 at position i. Wlog, assume this is a. Then a xor v does not have a 1 at position i, but for every j > i, a xor v has a 1 at position j iff a does, so a xor v < a.

Does anyone have an idea how to approach these bitwise arguments? I tried both nat.digits and nat.test_bit and friends, but both seem very painful for this purpose.

Patrick Massot (Aug 27 2020 at 20:25):

Is this useful for diagram chasing?!

Markus Himmel (Aug 27 2020 at 20:26):

It's useful for addition of Grundy numbers.

Patrick Massot (Aug 27 2020 at 20:26):

And what is a grungy number?

Markus Himmel (Aug 27 2020 at 20:27):

See here for example.

Simon Hudon (Aug 27 2020 at 20:49):

Is it true if a = 0, b = 0 and c = 0? Then there is no most significant 1-bit for any of the values

Simon Hudon (Aug 27 2020 at 20:50):

Ah! The assumption makes that impossible, my mistake

Simon Hudon (Aug 27 2020 at 20:51):

I was thinking, maybe you can use a decomposition: 0 < a -> exists p k, a = 2^k + p /\ p < 2^k. Then, k gives you a handle on the most significant 1-bit

Simon Hudon (Aug 27 2020 at 21:01):

If you have a = 2^ka + pa and b = 2^kb + pb, you have three cases to consider when decomposing the xor:

xor a b = xor pa pb if ka = kb
          2^kb + xor a pb if ka < kb
          2^ka + xor pa b if ka > kb

Mario Carneiro (Aug 27 2020 at 21:37):

I don't like theorems that have let in their statements. In this case I think it would be best to just inline the let and introduce it in the body if you need it

Mario Carneiro (Aug 27 2020 at 21:38):

Also, the first disjunct is impossible - once you expand it you get lxor a (lxor a (lxor b c)) = lxor b c, which is greater than a by hypothesis

Mario Carneiro (Aug 27 2020 at 21:39):

in fact the other two disjuncts also simplify once you expand the let

Mario Carneiro (Aug 27 2020 at 21:39):

you should prove associativity of lxor for any bitwise so that you can conclude associativity of band and bor too

Mario Carneiro (Aug 27 2020 at 21:41):

In general, a good strategy for all sorts of bitwise properties is to apply test_bit extensionality, simp with test_bit, then conclude using a boolean theorem

Bhavik Mehta (Aug 27 2020 at 21:47):

I don't know if this is helpful but it might suggest alternative approaches: I developed properties of the colex ordering here - if you view naturals as the finite set of positions where the bit is on (ie under the map taking a A : finset ℕ to A.sum (pow 2)) then the ordering on naturals is the same as colex ordering, and lxor corresponds to symmetric difference of sets, so it could be helpful to use some of the ordering properties I put there

Mario Carneiro (Aug 27 2020 at 21:47):

I would suggest this version of the statement:

lemma tri' {a b c : } (h₁ : a  lxor b c) (h₂ : b  lxor a c) : lxor a b  c :=

Mario Carneiro (Aug 27 2020 at 21:55):

Your wlog in the proof sketch doesn't make any sense because a,b,c are not symmetric in the statement, only b and c

Markus Himmel (Aug 28 2020 at 05:51):

Mario Carneiro said:

Your wlog in the proof sketch doesn't make any sense because a,b,c are not symmetric in the statement, only b and c

The proof sketch only uses the more general assumption nat.lxor a (nat.lxor b c) ≠ 0, which is symmetric.

Mario Carneiro (Aug 28 2020 at 06:06):

It is possible to formalize your argument directly, but there are some lemmas to prove about bitwise stuff

Mario Carneiro (Aug 28 2020 at 06:07):

I think it might be easier though to make use of the fact that (\forall i, test_bit i a -> test_bit i b) -> a <= b

Mario Carneiro (Aug 28 2020 at 06:11):

In this case, I think you want to construct the number x which matches a up to position i, and is 1 at position i and 0 at all lower bits. Then a xor v \sub x-1 and x <= a, which does the latter part of your proof sketch

Mario Carneiro (Aug 28 2020 at 06:14):

The lemma for the first part of your sketch is that if v != 0 then there exists i such that 2^i <= v < 2^(i+1), which may already exist, plus the proof that test_bit i v = 1 for such a number, which should not be hard to prove if you unfold the definition in terms of right shift (which is the same as integer division by 2^i)

Markus Himmel (Aug 28 2020 at 11:47):

Thanks, I was able to work it out using your ideas. I PRed the resulting lemmas about test_bit, lxor and friends in #3964.


Last updated: Dec 20 2023 at 11:08 UTC