Pairs of bitvectors

Stream: Is there code for X?

[Jakob von Raumer]

Is there code in any repo about intrepreting pairs/vectors/lists of bitvectors as a big bitvector by appending? With lemmas saying that the "high" bitvector is 0 if the value is low enough etc.

[Jakob von Raumer]

@Tobias Grosser @Henrik Böving

[Kim Morrison]

Certainly appending pairs of BitVectors is supported, just as v ++ w, and there is a fairly complete set of lemmas about this.

I have an abandoned PR at lean#3727 that defined

protected def flattenList {n : Nat} (xs : List (BitVec n)) : BitVec (n * xs.length) :=

but it needed work.

I would suggest just starting over on this, and:

1. Now that the Vector API is fairly complete, just do it for Vector n (BitVec m) directly.
2. Writing the function with signature Vector.flatMapBitVec (v : Vector n \a) (f : \a \to BitVec m) : BitVec (n * m) first is probably best, and then defining Vector.flattenBitVec in terms of that.
3. Probably it is best to define variants for both little-endian and big-endian conventions.

[Jakob von Raumer]

I'll take up on this, including some analysis of the .toNat of flattened vectors and about carries of multiplication etc

[Jakob von Raumer]

@Kim Morrison Any comment on lean#7754? Will add the BE versions of the type equivalence if the approach seems reasonable. I think with the lemmas about getElem we don't even need specific lemmas for the arithmetic operations

[Siddharth Bhat]

@Jakob von Raumer I left another round of review on the new APIs!