feat: Nat.shiftRight_bitwise_distrib

[tydeu]

This PR adds Nat theorems for distributing >>> over bitwise operations, paralleling those of BitVec.

This enables closing goals like the following using simp:

example (n : Nat) : (n <<< 2 ||| 3) >>> 2 = n := by simp [Nat.shiftRight_or_distrib]

It might be nice for these theorems to be simp lemmas, but they are not currently in order to be consistent with the existing BitVec and div_two theorems.

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-6334 build against this PR was cancelled. (2024-12-08 08:06:46) View Log
• ✅ Mathlib branch lean-pr-testing-6334 has successfully built against this PR. (2024-12-10 04:59:55) View Log

[tobiasgrosser]

It might be nice for these theorems to be simp lemmas, but they are not currently in order to be consistent with the existing BitVec and div_two theorems.

Can you expand on this? This PR adds:

theorem shiftRight_and_distrib {a b : Nat} : (a &&& b) >>> i = a >>> i &&& b >>> i :=
  shiftRight_bitwise_distrib

while the BitVev library has

 theorem ushiftRight_and_distrib (x y : BitVec w) (n : Nat) :
    (x &&& y) >>> n = (x >>> n) &&& (y >>> n) := by
  ext
  simp

This seem to be consistent among data types. What would be needed to make these simp lemmas? AFAIU neither direction is strictly more canonical. Do you have specific improvements in mind? I would be happy to explore these in the BitVec library.

[tydeu]

@tobiasgrosser

What would be needed to make these simp lemmas? AFAIU neither direction is strictly more canonical. Do you have specific improvements in mind? I would be happy to explore these in the BitVec library.

My thesis is that distributing shiftRight (and factoring out shiftLeft) is the natural direction because both reduce the number of bits considered by the bitwise operations. This reduces complexity and increases the chance the rest can be simp'ed away. I think the example in the PR description is a good demonstration of the kind of expression that it would be great to be able to simp by default:

example (n : Nat) : (n <<< 2 ||| 3) >>> 2 = n := by simp

Nonetheless, there are cases were distributing shiftRight can be bad. If the subterm can already simplified due to the presence of literals or a hypothesis, distributing can impair this. For instance:

example (n : Nat) : (1 &&& 3) >>> n = 1 >>> n := by simp 

Distributing first here would create the term (1 >>> n &&& 3 >>> n) which can no longer be simp'ed. Luckily, this is not a problem if distribution is a bottom-up simplification lemma (i.e., @[simp ↑], the default), as simp will apply potential simplifications to the subterm before distributing (and then simplifying again).

Weighing thees pros and cons lead me to believe the making the shiftRight distribution lemmas @[simp] would be preferable. However, I am not an expert in this area and there could be cases I have not considered where this poses a problem, hence my initial reservation.

[kim-em]

Otherwise, LGTM.