feat(Data/Nat): faster computation of Nat.log

[b-mehta]

Give an alternate definition Nat.logC for Nat.log which computes more efficiently (roughly speaking, this should have logarithmic time in the output, while Nat.log has linear time in its output).
Prove that these two give the same output, and use csimp to ensure evaluation of Nat.log uses Nat.logC instead.

---

[github-actions]

PR summary 5e2f2d7089

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ logC
+ logTR
+ log_eq_logC

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).

[eric-wieser]

@kim-em, what's the SOTA for committing benchmarks / performance tests like these? It would be great to have a test file that computes a big logarithm, and even better if we can assert it is "quick".

[b-mehta]

Now that I read it again, the point of this was that Nat.logTR times out on this computation whereas Nat.logC doesn't, and Nat.log hits stack limit at something like Nat.log 2 (2 ^ 11000).
I wouldn't mind removing these lines either, it's largely to save a future person's time if they think "I wonder if tail-recursion would be better than this weird doubling algorithm"

[eric-wieser]

My comment really was "let's add a test somewhere of something that didn't work before your change"

[kim-em]

I'm inclined to just create tests/nat/log.lean, if these are meant to be regression tests.

If they are documentation, they should be code blocks inside a module doc next to the definition.

[b-mehta]

I don't have a strong preference here. What's the distinction between having a code block as a module doc as opposed to a code block in the definition docstring?

[jcommelin]

Do you mean in particular that these aren't meant as regression tests?

[eric-wieser]

I'm inclined to just create tests/nat/log.lean, if these are meant to be regression tests.

We should add this file, with an invocation that took >20s before and now takes <1s.

[urkud]

Optional (I didn't test if it results in the same IR):

Suggested change

	if h : 1 < b then let (_, e) := step b h; e else 0 where
	if h : 1 < b then (step b h).2 else 0 where

[jcommelin]

bors d+

[jcommelin]

Do you mean in particular that these aren't meant as regression tests?

[mathlib-bors]

✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[b-mehta]

bors merge

[mathlib-bors]

Canceled.

[mattrobball]

Can you also update the PR description with the changes and their reason (for the people who grep the git log)? Thanks.

[b-mehta]

Updated.