feat: add BitVec.intMin

[tobiasgrosser]

We keep the library interface for intMin minimal and make it an abbrev for twoPow. To ensure a uniform library interface, we also turn intMax into an abbrev for allOnes.

To improve proof automation, we introduce a simp-set boolToPropSimps plus corresponding lemmas that turn our intMin_toLsb proof into a simple simp; omega proof. This simp set is not yet active, but should become so after a stage-0 update.

This PR also pulls in some mathlib theorems on testBit and Nat and establishes facts about 2 ^ w that are needed here and which are generally useful for bitvector reasoning.

The following theorem is not generalized to arbitrary x instead of 2, as this would require a condition to be added for x > 1 which would have to be passed to simp each time this theorem should fire:

protected theorem two_pow_pred_mod_two_pow (h : 0 < w) :
    2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1)

Mathlib reports only errors for theorems that this PR moves into lean.

error: ././././Mathlib/Data/Nat/Bitwise.lean:250:8: 'Nat.testBit_two_pow_self' has already been declared
error: ././././Mathlib/Data/Nat/Bitwise.lean:254:8: 'Nat.testBit_two_pow_of_ne' has already been declared
error: ././././Mathlib/Data/Nat/Bitwise.lean:265:8: 'Nat.testBit_two_pow' has already been declared

[tobiasgrosser]

Draft, as I am still polishing the order of the various theorems within the files. Any feedback is obviously already welcome.

[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 efbecf272dc2c12610efd825e8672cee380b4c24 --onto b486c6748b153bda628575635baa28aeeb38b8c5. (2024-08-20 05:49:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea97aac83b276bd582471d4d6b5899bac67298fd --onto 2bc87298d9fc5b1a63dd8c10c15e970d5df93fdf. (2024-08-24 20:49:17)
• 💥 Mathlib branch lean-pr-testing-5098 build failed against this PR. (2024-08-26 11:22:13) View Log
• 💥 Mathlib branch lean-pr-testing-5098 build failed against this PR. (2024-08-26 13:36:56) View Log
• 💥 Mathlib branch lean-pr-testing-5098 build failed against this PR. (2024-08-26 14:11:15) View Log
• 💥 Mathlib branch lean-pr-testing-5098 build failed against this PR. (2024-08-26 14:40:56) View Log
• 💥 Mathlib branch lean-pr-testing-5098 build failed against this PR. (2024-08-26 15:56:56) View Log
• 💥 Mathlib branch lean-pr-testing-5098 build failed against this PR. (2024-08-26 16:48:38) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c45a6a93f98b004d2e10574d25ee5898bdf0ee34 --onto 9305049f1ef7309842806c2a994a2020bb32a71f. (2024-08-27 01:20:50)

[AtticusKuhn]

looks good to me.

[tobiasgrosser]

This is now ready-for-review from my side.

[tobiasgrosser]

awaiting-review

[AnotherAlexHere]

Looks good to me.

[kim-em]

As we are modifying simp lemmas for Nat, I would like to see Mathlib tested against this. If you rebase this PR onto nightly-with-mathlib, you should hopefully get a builds-mathlib or breaks-mathlib label within an hour.

[tobiasgrosser]

The comments are adressed, except for finding the correct imports for the new simp set. I will await advice from @bollu.

[tobiasgrosser]

The simp-set is also defined, so the remaining issue is a lonely build failure in the nix build, which I am not sure how to debug or if it is even introduced by this PR.

[tobiasgrosser]

It seems that the intMax definition was incorrect. I corrected it, but I haven't polished the proofs yet.

[kim-em]

Remaining steps to activating boolToPropSimps:

• Move BoolToPropSimps.lean to src/Init/Data/.
• add import Init.Data.BoolToPropSimps to src/Init/Data.lean
• commit that
• make -j32 -C build/release update-stage0
• git commit -m "chore: update stage0"
  (it's essential the commit message is exactly that)
• now uncomment the @[boolToPropSimps] attributes, and hopefully you can use simp only [boolToPropSimps].

(If you give me write access on your repo I'm happy to do these steps, too.)

[tobiasgrosser]

Remaining steps to activating boolToPropSimps:

• Move BoolToPropSimps.lean to src/Init/Data/.
• add import Init.Data.BoolToPropSimps to src/Init/Data.lean
• commit that
• make -j32 -C build/release update-stage0
• git commit -m "chore: update stage0"
  (it's essential the commit message is exactly that)
• now uncomment the @[boolToPropSimps] attributes, and hopefully you can use simp only [boolToPropSimps].

(If you give me write access on your repo I'm happy to do these steps, too.)

Cool. I gave you write access. I guess it's easier if you push this through.