Merging bitwise and bitwise'

Stream: new members

[Harun Khan]

I'm trying to merge bitwise and bitwise' as mentioned here. Particularly I'm trying to prove

lemma bitwise_eq_bitwise' (f: Bool → Bool → Bool ) : bitwise f = bitwise' f := by sorry

but all of the useful lemmas in the library have this assumption f false false = false. So so far I proved (without any sorries) that

lemma bitwise_eq_bitwise'1 (f: Bool → Bool → Bool ) (h: f false false = false):
bitwise f = bitwise' f := by sorry

Is the more general bitwise_eq_bitwise' true too? How can I check?

[Bolton Bailey]

The reason the f false false = false hypothesis is necessary is because if f false false = true, then the high-order 0 bits would then map to ones, and you would get a natural number with an infinite number of one bits, which shouldn't be possible.

You might be able to check by running an #eval statement with an f that does have f false false = true and see how these functions are defined in this case.

[Bolton Bailey]

Checking this out, I couldn't find any inputs on which they behave differently, it seems like they just perform as if f were changed to return false on false false. Perhaps this theorem could be proved and then the condition in bitwise_eq_bitwise' could be removed.

[Eric Wieser]

I think docs4#Nat.bitwise'_zero_right does not need its side condition?

[Eric Wieser]

This looks like a pretty good confirmation that the statement you want is true:

import Mathlib.Data.Fintype.Pi
import Mathlib.Data.Nat.Bitwise

#eval ∀ m, m ≤ 10 → ∀ n, n ≤ 10 → ∀ f : Bool → Bool → Bool, Nat.bitwise f m n = Nat.bitwise' f m n
-- outputs `true`

[Kevin Buzzard]

Bolton Bailey said:

The reason the f false false = false hypothesis is necessary is because if f false false = true, then the high-order 0 bits would then map to ones, and you would get a natural number with an infinite number of one bits, which shouldn't be possible.

You might be able to check by running an #eval statement with an f that does have f false false = true and see how these functions are defined in this case.

I looked a bit at this and it seems to me that both algorithms simply stop at the point where both numbers have become 000000..., as opposed to applying f ad infinitum, so this shouldn't affect things.

[Eric Wieser]

I think @Bolton Bailey is explaining why that hypothesis appears in some lemmas. Indeed, it's unecessary in this one

[Eric Wieser]

But the natural way to prove this one is to use the other lemmas!

[Alex Keizer]

Looking at this a bit more, it seems bitwise (and bitwise') behaves somewhat strangely for functions where f false false = true.

import Mathlib.Data.Nat.Bitwise

def f : Bool → Bool → Bool :=
  fun _ _ => true

#eval Nat.bitwise f 100 0 -- 100

I would have expected that to apply f to each pair of bits up-to the most significant bit in either of its inputs, returning 127.

The implementation of bitwise starts like so

if n = 0 then
    if f false true then m else 0
  else if m = 0 then
    if f true false then n else 0
  else
--  ...

So the implementation assumes that if, say, m = 0 and f true false = true, that the result of aplying f to each bit of n together with 0 is simply n; which is true only if indeed f false false = false.