BitVec simp automation

Stream: lean4

[James Gallicchio]

I am working on a project with bit vectors that are n+2-wide. I end up needing to prove the below bitvec goal, and I'm wondering if there is a less wordy way to prove it:

theorem Nat.lt_pow_of_exp_le {x base exp exp' : Nat}
  (base_pos : base > 0) (x_lt : x < base^exp') (exp_le : exp' ≤ exp) : x < base^exp := by
  apply Nat.lt_of_lt_of_le x_lt
  exact Nat.pow_le_pow_of_le_right base_pos exp_le

example (n : Nat) : 0#(n+2) ≠ 3#(n+2) := by
  simp only [bv_toNat]
  rw [Nat.mod_eq_of_lt (by apply Nat.lt_pow_of_exp_le (exp' := 2) <;> simp)]
  rw [Nat.mod_eq_of_lt (by apply Nat.lt_pow_of_exp_le (exp' := 2) <;> simp)]
  decide

example (n : Nat) (h : n ≥ 2) : 0#n ≠ 3#n := by
  simp only [bv_toNat]
  rw [Nat.mod_eq_of_lt (by apply Nat.lt_pow_of_exp_le (exp' := 2) <;> simp [h])]
  rw [Nat.mod_eq_of_lt (by apply Nat.lt_pow_of_exp_le (exp' := 2) <;> simp [h])]
  decide

My project needs the first example but I'm also curious if there is a cleaner proof for the second example.

[James Gallicchio]

I do understand why the automation doesn't handle this case, but simultaneously I think my use case is quite reasonable. I could see others wanting to prove, for example, facts about bitvecs where n \mem [8,16,32,64] based on the fact that n >= 8.

[James Gallicchio]

I have golfed myself with a more specific lemma:

theorem BitVec.ofNat_eq_of_width_ge (minWidth : Nat) (hwidth : n ≥ minWidth) (hi : i < 2^minWidth)
  : BitVec.ofNat n i = ⟨i, Nat.lt_of_lt_of_le hi (Nat.pow_le_pow_right (by decide) hwidth)⟩ := by
  simp only [bv_toNat]
  rw [Nat.mod_eq_of_lt]
  exact Nat.lt_of_lt_of_le hi (Nat.pow_le_pow_right (by decide) hwidth)

example (n : Nat) : 0#(n+2) ≠ 3#(n+2) := by
  simp [BitVec.ofNat_eq_of_width_ge (minWidth := 2)]

example (n : Nat) (h : n ≥ 2) : 0#n ≠ 3#n := by
  simp [h, BitVec.ofNat_eq_of_width_ge (minWidth := 2)]

[James Gallicchio]

Another category of goals I'm unsure how to prove:

example (n : Nat) : (3#(n+2))[0] = true := sorry
example (n : Nat) : (3#(n+2))[1] = true := sorry
example (n : Nat) (h : k >= 2) : (3#(n+2))[k] := sorry

[Kim Morrison]

How about

example (n : Nat) : 0#(n+2) ≠ 3#(n+2) := by
  simp only [bv_toNat]
  intro h
  replace h := congrArg (· % 4) h
  simp [Nat.pow_add] at h

[Kim Morrison]

And for the later ones:

example (n : Nat) : (3#(n+2))[0] = true := by
  simp [BitVec.getElem_eq_testBit_toNat]
example (n : Nat) : (3#(n+2))[1] = true := by
  simp [BitVec.getElem_eq_testBit_toNat]
  decide
example (n : Nat) (h : k >= 2) (h') : (3#(n+2))[k] = false :=
  match k, h with
  | k + 2, h => by
    simp [BitVec.getElem_eq_testBit_toNat]
    intro h'
    simp [Nat.testBit, Nat.add_comm k 2, Nat.shiftRight_add]

[Kim Morrison]

getElem_eq_testBit_toNat should be added to the bv_toNat simp set, probably many others.

[Kim Morrison]

Anyone interested in doing a survey of things that should be added to bv_toNat?

[James Gallicchio]

Kim Morrison|110087 said:

How about

example (n : Nat) : 0#(n+2) ≠ 3#(n+2) := by
  simp only [bv_toNat]
  intro h
  replace h := congrArg (· % 4) h
  simp [Nat.pow_add] at h

This is a cool proof, and not a route I expected! (I think the key lemma is Nat.mod_mul_left_mod in that simp?)

I am still a bit unsatisfied that the goal is not simp-able. If these were little-endian lists of bits, then list congruence lemmas would reduce this. Maybe there needs to be a second simp set for pushing bitvecs towards a list like normal form?

[Kim Morrison]

Yes, we're definitely missing API for converting to List Bool and to Vector Bool n.

[James Gallicchio]

I'm gonna post some more example goals for whoever in the future fills out that API. Thanks again for the help

[James Gallicchio]

example {a b : BitVec n} {i : Fin n} : a = b ^^^ (1 <<< i.val) → a[i] ≠ b[i] := sorry
example {a b : BitVec n} {i : Fin n} : a = b ^^^ (1 <<< i.val) → ∀ i' ≠ i, a[i'] = b[i'] := sorry

[Kim Morrison]

The first one is

attribute [bv_toNat] getElem_eq_testBit_toNat

example {a b : BitVec n} {i : Fin n} : a = b ^^^ (1 <<< i.val) → a[i] ≠ b[i] := by
  rintro rfl
  simp [bv_toNat]

[Kim Morrison]

Ugly, but:

example {a b : BitVec n} {i : Fin n} : a = b ^^^ (1 <<< i.val) → ∀ i' ≠ i, a[i'] = b[i'] := by
  rcases i with ⟨i, w⟩
  rintro rfl ⟨i', w'⟩ h
  simp at h
  simp [bv_toNat]
  have : (decide (i ≤ i') && Nat.testBit 1 (i' - i)) = false := by
    by_cases p : i ≤ i'
    · have q : i' - i = i' - i - 1 + 1 := by omega
      rw [q]
      simp [p, Nat.testBit_succ]
    · simp [p]
  simp_all

[Kim Morrison]

I'll put these aside somewhere as "good examples of automation we want".

[James Gallicchio]

slightly different question within "simp automation for bitvec": have we settled on a simp normal form for BitVec.getLsbD?

• There's a lemma BitVec.getLsbD_eq_getElem, which is not marked simp
• The ext lemma for BitVec is eq_of_getLsbD_eq
• A major lemma is getLsb_ofBoolListLE, and an equivalent getElem_ofBoolListLE is not defined yet. Weirdly, getElem_ofBoolListBE is defined, which subtracts the index from the length.

[James Gallicchio]

maybe I should check v4.17.0-rc1 to see what bitvec lemmas were added

[Henrik Böving]

getLsbD is its own simp normal form, the eq_getElem lemma does not always apply. There is work underway to provide getElem and getLsbD lemmas for basically all operations on BitVec and that goal is quite close

[James Gallicchio]

Ok. In that case, can we consider making the default ext lemma be getElem rather than getLsbD? At the moment I am doing lots of ext; simp [BitVec.getLsbD_eq_getElem, *] because getElem has cleaner lemmas.

[Henrik Böving]

that could be worth a consideration, I guess we could have an RFC about it as it would require at least some proof refactoring I would assume

[James Gallicchio]

Yeah. I'm not sure how to best refactor @[ext] lemmas, and I don't know who else is using BitVec aside from bv_decide and my project :big_smile: I'll wait to see if Kim and others have thoughts. Let me know if you need someone to write an RFC

[Henrik Böving]

BitVec is one of the more heavily used basic libraries right now. There is AWS projects that have used it (e.g. LNSym), there is academic groups like Tobias Grosser's team at Cambridge, the Lean SAIL project etc.

[Kim Morrison]

Yes, I agree that changing the default ext lemma would be preferable, as it results in a better proof obligation (the bound witness is already installed where you want to use it!) It would be disruptive to existing proofs. But it is not too late, and indeed the sooner we do it, the better.

I'd want to make sure @Tobias Grosser et al have a chance to express concerns, so an RFC would be great.

[James Gallicchio]

https://github.com/leanprover/lean4/issues/7045 :salute:

[Tobias Grosser]

Hi @James Gallicchio, I am in favor (assuming the patches don't expose any trouble).

[Tobias Grosser]

Let me give some historical context. In earlier variants of the BitVec library, we did not had the nice getElem interface. AFAIU @Kim Morrison started to push towards getElem and he added the initial interface definitions. At this point, large parts of the BitVec library already used the current ext lemma and most theorems for getExt were missing.

[Tobias Grosser]

Over the last month we added these theorems.

[Tobias Grosser]

In fact, we were aiming to complete the following table:

Screenshot 2025-02-12 at 05.11.15.png

[Tobias Grosser]

Which was very blue at the beginning.

[Tobias Grosser]

And now looks already quite reasonable.

[Tobias Grosser]

As you see, the getElem row is meanwhile complete.

[Tobias Grosser]

Which means, I can probably rebase an old PR # feat: make getLsbD_eq_getElem a simp lemma #5498.

[Tobias Grosser]

And it should look a lot better.

[James Gallicchio]

awesome. is someone in FRO able to make the @[ext] change in time for v4.17?

[Tobias Grosser]

I can rebase the above PR today. If this PR goes through, I would be happy with the @[ext] change.

[Tobias Grosser]

And feel it would be rather trivial.

[Tobias Grosser]

On the other side, I remember one issue. Let me rebase the PR and see where we are standing.

[Tobias Grosser]

The remaining issue was that in some cases we ended up with a mix of getElem and non-get-elem variants, which led to inconsistencies that I could not resolve automatically. Give me 20' and I get back with the actual PR.

[Markus Himmel]

James Gallicchio said:

awesome. is someone in FRO able to make the @[ext] change in time for v4.17?

Since 4.17.0-rc1 is already out, changes merged today will not make it into the 4.17 release. Only fixes for ciritical issues discovered in 4.17.0-rc1 would make it into a 4.17.0-rc2, and if no such issues are found, 4.17.0 will be identical to 4.17.0-rc1.

[Tobias Grosser]

https://github.com/leanprover/lean4/pull/5498 is updated.

[Tobias Grosser]

This took a bit longer than 20', but I would hope the CI will be green.

[Tobias Grosser]

This is a first pass aimed at getting the proofs through. I would like to go over them carefully to polish the proofs and also to get a better feeling of what the diff looks like.

[Tobias Grosser]

The overall diff does look quite reasonable already, with only a handful of proofs requiring some more thoughts. The getElem API being now complete (with the exception of 1-2 cases) made the change reasonably easy.

[Tobias Grosser]

I now have a busy work-day, but I will do another round of polishing latest tomorrow morning.

[Tobias Grosser]

OK, https://github.com/leanprover/lean4/pull/5498 is ready for review.

[Tobias Grosser]

@Kim Morrison, @James Gallicchio, feedback is much appreciated.

[Kim Morrison]

'd. Thanks for this, this is a nice improvement.

[Tobias Grosser]

Thank you for your fast and careful review.

[James Gallicchio]

This is low priority-- but I just noticed the RHS in BitVec.getElem_cons is not in terms of getElem. Instead we can match the new getElem_append:

@[simp] theorem BitVec.getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if is_msb : i = n then b else x[i]'(by omega) := by
  split
  · simp [cons, getElem_append, *]
  · have : i < n := by omega
    simp [cons, getElem_append, *]

I apologize for not catching this during review :frowning:

[Tobias Grosser]

Thank you for pointing this out. As the big merge has now happened I will review the getElem functions to ensure their rhs actually uses getElem.

[Tobias Grosser]

https://github.com/leanprover/lean4/pull/7187

[Tobias Grosser]

Sorry for the delay.

[Tobias Grosser]

I have one minor question, maybe someone has an idea.

[Tobias Grosser]

This is now resolved.