Reasoning about bitwise xor

Stream: general

[Markus Himmel]

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]

Is this useful for diagram chasing?!

[Markus Himmel]

It's useful for addition of Grundy numbers.

[Patrick Massot]

And what is a grungy number?

[Markus Himmel]

See here for example.

[Simon Hudon]

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]

Ah! The assumption makes that impossible, my mistake

[Simon Hudon]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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