perf: add ShareCommon.shareCommon'

[leodemoura]

A more restrictive but efficient max sharing primitive.

Motivation: Some software verification proofs may contain significant redundancy that can be eliminated using hash-consing (also known as shareCommon). For example, theorem sha512_block_armv8_test_4_sym took a few seconds at addPreDefinitions and one second at fixLevelParams on a MacBook Pro (with M1 Pro). The proof term initially had over 16 million subterms, but the redundancy was indirectly and inefficiently eliminated using Core.transform at addPreDefinitions. I tried to use shareCommon method to fix the performance issue, but it was too inefficient. This PR introduces a new shareCommon' method that, although less flexible (e.g., it uses only a local cache and hash-consing table), is much more efficient. The new procedure minimizes the number of RC operations and optimizes the caching strategy. It is 20 times faster than the old shareCommon procedure for theorem sha512_block_armv8_test_4_sym.

[leodemoura]

!bench

[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 b73fe04710437daf1140cc8d06bef3e0f503fd33 --onto 7aec6c9ae7a54935ada0df0b4cc1efafc2291007. (2024-07-17 00:17:50)

[leanprover-bot]

Here are the benchmark results for commit 8558fd6.
There were significant changes against commit b73fe04:

  Benchmark                  Metric                Change
  ==================================================================
+ stdlib                     add pre-definitions    -4.4%  (-38.6 σ)
+ stdlib                     dsimp                 -11.1% (-665.6 σ)
+ stdlib                     fix level params      -14.4% (-127.0 σ)
- tests/bench/ interpreted   instructions            1.1% (1268.3 σ)