chore: introduce BitVec.setWidth to unify zeroExtend and truncate

[tobiasgrosser]

We always simplify to setWidth to minimize the API surface.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 078e9b6d778932430adf9ecbbf02e1025e922ce1 --onto 5eea8355baa64e6fda4e3874a0f45649d4c27633. (2024-09-16 07:05:01)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-09-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-09-16 09:04:36)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7952a7f74d6ff6ac44816cfce487f7bbc72ec04d --onto 5eea8355baa64e6fda4e3874a0f45649d4c27633. (2024-09-16 09:49:24)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 45af92fcd1846d7ec61125ab0fbd939f38ca68fe --onto 5eea8355baa64e6fda4e3874a0f45649d4c27633. (2024-09-16 10:17:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 45af92fcd1846d7ec61125ab0fbd939f38ca68fe --onto c25d2066471c7726b64d7f3eea8b5cce9910f33d. (2024-09-16 11:47:17)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 445c8f2ee02ec75cdd8b2811bd56f4fb16adb655 --onto c25d2066471c7726b64d7f3eea8b5cce9910f33d. (2024-09-16 13:25:20)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6a06a620f59da610afe875bacefedbd68788e52 --onto 445c8f2ee02ec75cdd8b2811bd56f4fb16adb655. (2024-09-18 05:59:34)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 77cd700fa877033316046f463f4c1b455b4498d2 --onto 445c8f2ee02ec75cdd8b2811bd56f4fb16adb655. (2024-09-18 07:14:41)

[tobiasgrosser]

This works, but for some reason, the simprocs for setWidth and family do not fire.

[tobiasgrosser]

This works, but for some reason, the simprocs for setWidth and family do not fire.

It required a stage-0 update. Now everything works.

[kim-em]

@alexkeizer, @bollu, @TwoFX, any thoughts on this?

I like this (indeed, suggested it!) as we've been accumulating inconsistently duplicated API for zeroExtend and truncate. After this change, we will just be simplifying both of those abbreviations to setWidth, and having a single verification API.

Moreover, we can further (I think, but we'll experiment in a later PR) replace cast (h : w = v) with setWidth v.

[alexkeizer]

I like it! I've also been a bit bothered with the API duplication, picking a more neutrally named simp normal form makes a lot of sense

[alexkeizer]

Moreover, we can further (I think, but we'll experiment in a later PR) replace cast (h : w = v) with setWidth v.

I do have my reservation about this, won't it lose information? For example, could the following still work with such a redefinition?

example {w v : Nat} {x : BitVec w} (h : w = v) : 
    (x.cast h).cast h.symm = x := by
  simp