List of Bools to Nat

Stream: Is there code for X?

[Isabel Dahlgren]

I've converted a Nat to a list of Bools, via docs#Nat.Bits. Now I'm looking for a way to recover the Nat from the list of Bools. I'm aware of docs#Nat.ofDigits, but it takes a list of Nats rather than Bools. There's also docs#BitVec.toNat for BitVecs, but I don't want to recast my list of Bools. Any suggestions?

[Richard Kiss]

Isabel Dahlgren said:

I've converted a Nat to a list of Bools, via docs#Nat.Bits. Now I'm looking for a way to recover the Nat from the list of Bools. I'm aware of docs#Nat.ofDigits, but it takes a list of Nats rather than Bools. There's also docs#BitVec.toNat for BitVecs, but I don't want to recast my list of Bools. Any suggestions?

There's a problem with this idea, and that's that any non-zero Nat converted to a list of bools always starts with a true. So a list of bools that starts with a false can't be represented. That's probably why you can't find the inverse.

There's a trick where you treat the most-significant bit as a marker only, ignoring its true/false meaning, so a binary int that starts with 10 now maps to a list of bools that starts with false, and so now the mapping is invertible. It's a useful enough trick that it should probably have a name (if it doesn't already) and be a standardized trick. But I don't know if its well-known.

[Yaël Dillies]

The broader context is that we have some finite (group) G and want to broadcast over a channel (interpreted as a sequence of Bool, namely List Bool) an element of G. So we find some k such that 2 ^ (k - 1) < card G ≤ 2 ^ k and send over k bits of information (where the identification G ≃ Fin (card G) is arbitrary, eg docs#Fintype.equivFin).

[Yaël Dillies]

I think docs#BitVec would be better here, but it seems the API is quite underdeveloped :sad:

[Yaël Dillies]

The relevant items here are trivial-strategy and trivial-strategy-valid

[Mario Carneiro]

@Richard Kiss said:

There's a trick where you treat the most-significant bit as a marker only, ignoring its true/false meaning, so a binary int that starts with 10 now maps to a list of bools that starts with false, and so now the mapping is invertible. It's a useful enough trick that it should probably have a name (if it doesn't already) and be a standardized trick. But I don't know if its well-known.

The trouble with that is that it sets up a bijection between lists of bools and positive nats. There are a few variations on that bijection in mathlib

[Kim Morrison]

Yaël Dillies said:

I think docs#BitVec would be better here, but it seems the API is quite underdeveloped :sad:

Requests welcome.