simp [h] cannot use h : ¬ v = 0 on BitVec, because the goal's 0 becomes 0#w before h is tried #16260

Description

simp normalises a bit-vector literal in the goal from OfNat.ofNat 0 to 0#w through the BitVec.isValue dsimproc and BitVec.ofNat_eq_ofNat. A hypothesis passed as a simp argument is turned into a rewrite rule as written, so its left side keeps OfNat.ofNat 0. The rule no longer matches, the linter reports the argument as unused, and the goal is left open:

example (v : BitVec 32) (zero : ¬ v = 0) : ¬ v = 0 := by
  simp [zero]
-- unsolved goals
-- zero : ¬v = 0
-- ⊢ ¬v = 0#32
-- warning: This simp argument is unused: zero

set_option trace.Meta.Tactic.simp true shows zero:1000, failed to unify v = 0 with v = 0#32. The literal change itself does not appear in trace.Meta.Tactic.simp.rewrite.

The same happens through a definition:

def copied (values : List (BitVec 32)) : List (BitVec 32) := values.takeWhile (· ≠ 0)

example (v : BitVec 32) (rest : List (BitVec 32)) (zero : ¬ v = 0) :
    copied (v :: rest) = v :: copied rest := by
  simp [copied, List.takeWhile_cons, zero]   -- leaves ⊢ ¬v = 0#32

Expected behavior

simp [zero] closes both goals. They already close with simp -bitVecOfNat [zero], or after attribute [-simp] BitVec.isValue BitVec.ofNat_eq_ofNat.

One possible fix: normalise bit-vector literals in the left side of rules built from simp arguments the same way the goal is normalised.

Notes

• Downstream libraries cannot work around this by default: attribute [-simp] does not carry into importing modules, and bitVecOfNat is a per-call config.
• Making a library's own tactics emit the OfNat form instead makes later default simp calls convert every literal back. One measured proof's bv_omega preprocessing went from 994k to 1785k heartbeats.

Versions

Lean (version 4.35.0), Windows x86_64. Not checked on a nightly.