chore: redefine Nat.bit and csimp lemma for Nat.bit

[FR-vdash-bot]

---

split from #13649

[github-actions]

PR summary 8185f68ded

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ bit_eq_bitImpl

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kim-em]

Could you please explain why you want to do this? I've never seen a @[csimp] lemma proved by rfl, which makes me a bit skeptical.

Could you include some form of benchmark showing the csimp lemma has a meaningful effect?

[FR-vdash-bot]

def bit (b : Bool) (n : Nat) : Nat :=
  cond b (2 * n + 1) (2 * n)

def bitImpl (b : Bool) (n : Nat) : Nat :=
  cond b (n <<< 1 + 1) (n <<< 1)

def run_bit (n : Nat) (x : Nat) : IO Unit := do
  let mut t := 0
  for _ in [0 : n] do
    t := bit false x

def run_bitImpl (n : Nat) (x : Nat) : IO Unit := do
  let mut t := 0
  for _ in [0 : n] do
    t := bitImpl false x

def n := 10^4
def x := 11^1000000

#eval timeit "bit" (run_bit n x) -- bit 620ms
#eval timeit "bitImpl" (run_bitImpl n x) -- bitImpl 433ms

[kbuzzard]

Although I'm by no means an expert here (and never use #eval in my own Lean work) I am by default suspicious of adding csimp lemmas which show only marginal improvement and in such niche cases. Are there any places in the library where the speedup is by e.g. a factor of 2 or more? Is it possible to give a lake exe benchmark which shows improvement? Are there other users who can see advantages here? e.g. @TwoFX or @girving ? Otherwise I am inclined to close as too niche. We've seen something get 30% better in one extreme case. How do we know, for example, that things don't get 30% slower for more reasonable values of n and x? We don't really have enough evidence to merge this change, in my opinion, but I'm open to changing my mind if more evidence is accumulated. With no more evidence I'm minded to close as "too risky to fiddle with".

[girving]

I don’t have a strong take here, but it does seem marginal. For one thing the code is branching, but my guess is that there’s some other even faster version.

[TwoFX]

@FR-vdash-bot, could you say a bit more about why you want this? Do you have a performance-critical compiled application that calls Nat.bit a lot?