feat: BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT

[bollu]

We add a new definition BitVec.twoPow w i to represent (1#w <<< i).
This expression is used to test bits when building the multiplication bitblaster.

Patch 1/?, being peeled from opencompl#6.

[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 366f3ac272b6a12b19cabd8573652fc138804bdf --onto ea46bf2839ad1c98d3a0c3e5caad8a81f812934c. (2024-06-10 12:15:02)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bd3b466f2f4f6d9ff10c65fbf68f758ecaa071c3 --onto bedcbfcfeed429428c3e7f008b6984fc8c2b2b76. (2024-06-13 10:18:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bd3b466f2f4f6d9ff10c65fbf68f758ecaa071c3 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-17 14:22:18)

[kim-em]

Mostly happy, but:

Convince me that this needs a name, and shouldn't just be written out as its definition in all the statements.

The proofs are less trivial than I expected (they are fine), and I think this justifies giving a name, but I just want to push back a little so we don't accumulate named entities needlessly!

[bollu]

@semorrison That's somewhat of a hard ask :) I abstracted it precisely because dealing with the raw definitions was unwieldy.

I've been mulling over this a little, and I wonder what the 'correct' approach is. The crux is that I want to break a bitvector into the bitwise-or of different 1 <<< i's, and having a name for this 1 <<< i object makes things easy because:

1. It conceptually isolates the core idea of each induction.
2. It makes naming lemmas easier, as they now talk about twoPow.

---

I wonder what you recommend in such a situation. I also wonder how mathlib handles such scenarios!

[kim-em]

No, I think your justification is satisfactory! Let's get the minor suggestions sorted out, and I can merge.

[bollu]

I've fixed all nits now.

[bollu]

awaiting-review