explicit bitvectors

Stream: Is there code for X?

[Jeremy Avigad]

Suppose I want to write a definition of the form

def foo (b0 b1 b2 b3 : Bool) : BitVec 4 := ...

and prove

example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 0 = b0 := ...
example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 1 = b1 := ...
example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 2 = b2 := ...
example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 3 = b3 := ...

What's the easiest way to define foo and prove those properties? When bitvectors were represented by lists of booleans, we could take the definition to be { val := [b0, b1, b2, b3] } and then the proofs were all rfl.

[Mario Carneiro]

there should hopefully be a definition such that the proof is by simp [foo] at least

[Kim Morrison]

Yes, I can give you

def foo (b0 b1 b2 b3 : Bool) : BitVec 4 := ofBoolList [b0, b1, b2, b3]

example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 0 = b0 := by simp [foo]
example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 1 = b1 := by simp [foo]
example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 2 = b2 := by simp [foo]
example (b0 b1 b2 b2 : Bool) : (foo b0 b1 b2 b3).getMsb 3 = b3 := by simp [foo]

[Kim Morrison]

There's one or two easy sorries, but I could have a PR up shortly.

[Mario Carneiro]

although I think it's weird that getMsb would have this effect in this case, I would expect b0 to be the lsb

[Mario Carneiro]

I think BE needs to be in the name of ofBoolList there

[Kim Morrison]

Sure.

[Kim Morrison]

Should there be the pair ofBoolListLE and ofBoolListBE?

[Jeremy Avigad]

In the meantime, I got these working:

import Std.Data.BitVec.Lemmas
import Mathlib.Data.Fin.Basic
import Mathlib.Algebra.Order.Sub.Defs

namespace BitVec

variable {n : ℕ}

theorem getMsb_cons_zero (b : Bool) (v : BitVec n) : getMsb (cons b v) 0 = b := by
  simp [getMsb, cons, ofBool]
  cases b <;> simp

theorem getMsb_cons_succ (b : Bool) (v : BitVec n) (i : Nat) : getMsb (cons b v) (i + 1) = getMsb v i := by
  by_cases h : i < n
  . have : n - (i + 1) < n := Nat.sub_lt_of_pos_le (Nat.succ_pos _) h
    have : n - 1 - i = n - (i + 1) := by rw [add_comm, ←tsub_tsub]
    simp [*, getMsb, cons]
  . simp [*, getMsb, cons]

end BitVec

I think that will serve my purposes, but I'll be happy to see a nicer solution.

[Kim Morrison]

@Jeremy Avigad, you may be using an old Std: BitVec is all in the Lean repository now.

[Kim Morrison]

Also, you need to start using omega. I just also needed to prove getMsb_cons_succ, but just wrote:

@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
  simp [cons, cond_eq_if]
  omega

:-)

[Kim Morrison]

@Jeremy Avigad, would you check if lean#3721 covers what you need?

[Jeremy Avigad]

Thank you, @Scott Morrison . I appreciate the help.

ofBoolListBE and getMsb_ofBoolListBE solved the problem I asked about. In terms of recapturing functionality I had with previous versions of BitVec, I needed to convert to and from a Fin n → Bool representation, which I managed to do with this:

def ofFnBE (f : Fin n → Bool) : BitVec n :=
  ofBoolListBE (List.ofFn f) |>.cast (by rw [List.length_ofFn])

theorem getMsb_ofFnBE (f : Fin n → Bool) (i : Fin n) :
    getMsb (ofFnBE f) i = f i := by
  have : ↑i < List.length (List.ofFn f) := by rw [List.length_ofFn]; exact i.2
  simp [ofFnBE, getMsb_cast, List.getD_eq_get, this]

theorem ofFnBE_getMsb : (ofFnBE fun i : Fin n => getMsb b i) = b := by
  apply eq_of_getMsb_eq; intro i; rw [getMsb_ofFnBE]

I had a surprisingly hard time proving that toNat is injective, but I managed it with this:

theorem toNat_inj {n : ℕ} {b1 b2 : BitVec n} (h : b1.toNat = b2.toNat) : b1 = b2 := by
  rcases b1 with ⟨b1, h1⟩; rcases b2 with ⟨b2, h2⟩; cases h; rfl

[Kim Morrison]

These look good. Would you like to PR them?

[Eric Wieser]

Isn't _inj usually reserved for the Iff lemma?

[Jeremy Avigad]

Scott Morrison said:

Would you like to PR them?

Yes, I'll try to do this soon. (I am swamped.)