Joining an Array of `BitVec` into a larger `BitVec`

Stream: lean4

[dxo]

I'm trying to write a function that iterates onver a Subarray of BitVec and appends them all together. I think I have something that should in principle work, but fails to typecheck because (I think) lean4 is unable to convince itself of the equality of syntactically different expressions in various BitVec indicies. Is there a way to help it along / is there a better way to write this?

def joinBytes (bytes : Subarray (BitVec b)) : BitVec (bytes.size * b) :=
  let rec go {m : Nat} (n : Fin (bytes.size + 1)) (res : BitVec m) : BitVec (m + (n * b))
    := if n = (0 : Nat)
       /-
       application type mismatch
         ite (n = ↑0) res
       argument
         res
       has type
         BitVec m : Type
       but is expected to have type
         BitVec (m + ↑n * b) : Type
       -/
       then res
       else go (n - 1) (BitVec.append res (bytes[bytes.size - n]'(by sorry)))
  /-
  type mismatch
    go (Fin.last (Subarray.size bytes)) nil
  has type
    BitVec (0 + ↑(Fin.last (Subarray.size bytes)) * b) : Type
  but is expected to have type
    BitVec (Subarray.size bytes * b) : Type
  -/
  go (Fin.last bytes.size) BitVec.nil

[dxo]

ah, I have discovered the ▸ operator! this seems to be exactly what I need

[Timo Carlin-Burns]

I think you want docs#BitVec.cast instead. Eq.rec (which that operator is notation for) tends to block reduction and be hard to prove equalities about, so we often use type-specific versions

[dxo]

oh, nice tip thanks!

[dxo]

that cleaned things up a bit

[dxo]

I managed to get everything working with ▸, but I'm still struggling with the proof of safe indexing

[Eric Wieser]

I think we have a version of this in mathlib called docs#finPiFinEquiv

[Eric Wieser]

(though to use it you need to pull the sum through the exponent via a cast)

[dxo]

Finally have a version that type checks:

def joinBytes (bytes : Subarray (BitVec b)) : BitVec (bytes.size * b) :=
  BitVec.cast (by simp) $ go bytes.size (by rfl) BitVec.nil
  where
    go {m : ℕ} (n : Nat) (thm : n <= bytes.size) (res : BitVec m) : BitVec (m + (n * b))
    := match n with
    | 0 => BitVec.cast (by simp) res
    | Nat.succ x
      => let n := Nat.succ x
         have add_thm : m + b + (x * b) = m + Nat.succ x * b := by
           simp [Nat.succ_mul, Nat.add_assoc]
           simp [Nat.add_comm]
         have idx_thm : bytes.size - n < bytes.size := by
           have npos : 0 < n := by simp
           have szpos : 0 < bytes.size := Nat.lt_of_lt_of_le npos thm
           apply Nat.sub_lt
           apply szpos
           assumption
         let next := BitVec.append res (bytes[bytes.size - n]'(idx_thm))
         BitVec.cast add_thm $ go x (Nat.le_of_succ_le thm) next

[dxo]

Eric Wieser said:

I think we have a version of this in mathlib called docs#finPiFinEquiv

Interesting! Thank you. I got rid of the Fin in the end, it was kinda too much to think about :grinning:. Maybe I'll try again now I have a working version with nats and evidence passing.

Eric Wieser said:

(though to use it you need to pull the sum through the exponent via a cast)

I don't understand this sentance at all I'm afraid :sweat_smile:

[dxo]

Figured out a much cleaner version based on a dependent fold:

import Mathlib.Data.Vector
open Vector
open Nat

def dfoldr {α : Type}
           : {sz : ℕ}
           → (tp : ℕ → Type)
           → (step : (idx : ℕ) → α → tp idx → tp (idx + 1))
           → (init : tp 0)
           → Vector α sz
           → tp sz
| 0, _, _, base, Vector.nil => base
| n + 1, p, step, base, v => step n (head v) (dfoldr p step base (tail v))


def joinBytes (bytes : Vector (BitVec b) sz) : BitVec (sz * b) :=
  have cast_thm {i} : b + i * b = (i + 1) * b := by rw [add_comm, mul_comm, ←mul_succ, mul_comm]
  dfoldr
    (λ i => BitVec (i * b))
    (λ i val acc => BitVec.cast cast_thm (BitVec.append val acc))
    (BitVec.cast (by simp) BitVec.nil)
    bytes

[dxo]

I couldn't find dfoldr or something like it anywhere in Init / Std / Mathlib.Am I missing it somewhere? joinBytes was so much easier to write once I understood how to define dfoldr.

[Kim Morrison]

@dxo, I have a PR about this at https://github.com/leanprover/lean4/pull/3727. It's currently a bit abandoned, but if you wanted to review it / suggest changes, etc, perhaps we can resume progress on it.