BitVec n → Vector Bool n

Stream: Is there code for X?

[Ka Wing Li]

Is there a function for converting a bit vector to a list of bools?

[Ka Wing Li]

The closest thing I can find is

def BitVec.toVector : BitVec n → Vector Bool n := λ bv ↦ bv.toNat.bits.toArray.toVector

But it will not work as docs#Nat.bits will not have leading zeros.

[Ka Wing Li]

I am not sure if I am missing something trivial from mathlib.

[Matt Diamond]

I think you should be able to get what you need by using docs#List.ofFn along with either docs#BitVec.getLsb or docs#BitVec.getMsb (depending on the ordering you'd like)

[Matt Diamond]

you know, something like fun bv => List.ofFn bv.getLsb or whatnot

[Ka Wing Li]

Yes, I am trying the function. The tricky part is now the dependent type.

[Matt Diamond]

what trouble are you running into?

[Ka Wing Li]

Classic trouble of dependent type

Type mismatch
  (List.ofFn bv.getMsb).toArray.toVector
has type
  Vector Bool (List.ofFn bv.getMsb).toArray.size
but is expected to have type
  Vector Bool n

[Matt Diamond]

oh, I didn't realize you wanted a vector, you said list (realizing now I should've read the post title more carefully)

[Matt Diamond]

just use Vector.ofFn then

[Ka Wing Li]

Nice!

[Ka Wing Li]

Thanks!

[Matt Diamond]

no problem!

[Ka Wing Li]

I guess there is also an inverse function as well?

[Ka Wing Li]

I am looking up relevant APIs.

[Matt Diamond]

yes, it looks like you can use docs#BitVec.ofFnLE (little endian) or docs#BitVec.ofFnBE (big endian) along with docs#Vector.get to go in the other direction

[Matt Diamond]

these lemmas should be useful for proving that these transformations are inverse to each other:

https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/BitVec/Lemmas.html

along with docs#Vector.get_ofFn