Add builtin simproc for HShift for Nat and UInt?

Stream: lean4

[Casavaca]

Sometimes simp would make no progress where you thought it would:

example (x : BitVec 32) (h : x = 5#32) :
  match (x >>> 1) with
  | 2#32 => True
  | _    => False := by
  rw [h]
  simp? -- simp only [BitVec.reduceHShiftRight, _example.match_1.eq_1]
        --            BitVec.reduceHShiftRight is built in

example (x : Nat) (h : x = 5) :
  match (x >>> 1)#32 with
  | 2#32 => True
  | _    => False := by
  rw [h]
  simp -- no progress

example (x : UInt8) (h : x = 5) :
  match (x >>> 1) with
  | 2 => True
  | _ => False := by
  rw [h]
  simp -- no progress

It turned out that BitVec.reduceHShiftRight is builtin_dsimproc. Should we add this for HShift of Nat and UInt?

[Kim Morrison]

Yes, this sounds reasonable.