feat: tree map data structures and operations

[datokrat]

This PR introduces ordered map data structures, namely DTreeMap, TreeMap, TreeSet and their .Raw variants, into the standard library. There are still some operations missing that the hash map has; all those operations were implemented that are necessary so that RBMap and RBTree can be replaced by TreeMap and TreeSet in the Lean repository itself (as part of a later PR). As of now, the operations are unverified, but the corresponding lemmas will follow in subsequent PRs. While the tree map has already been optimized, more micro-optimization will follow as soon as the new code generator is ready.

[datokrat]

!bench

[leanprover-bot]

Here are the benchmark results for commit 0581dd5.
The entire run failed.
Found no significant differences.

[datokrat]

!bench

[leanprover-bot]

Here are the benchmark results for commit 0581dd5.
The entire run failed.
Found no significant differences.

[datokrat]

!bench

[leanprover-bot]

Here are the benchmark results for commit 26013c5.
There were significant changes against commit c073da2:

  Benchmark                  Metric                 Change
  ====================================================================
+ bv_decide_mul              branches                -1.6%  (-129.2 σ)
+ bv_decide_mul              instructions            -1.5%   (-91.1 σ)
- ilean roundtrip            branches                 2.6%    (13.0 σ)
- ilean roundtrip            instructions             2.2%    (27.4 σ)
- import Lean                branches                 5.1%   (150.9 σ)
- import Lean                instructions             5.3%   (198.6 σ)
- import Lean                maxrss                   4.0%   (101.8 σ)
- lake build no-op           maxrss                   4.6%    (60.4 σ)
- lake config elab           instructions             1.0%    (39.2 σ)
- lake config elab           maxrss                   6.1%    (85.1 σ)
- lake config import         instructions             2.7%    (42.6 σ)
- lake config import         maxrss                   6.1%    (66.8 σ)
- lake config tree           instructions             2.6%    (73.9 σ)
- lake config tree           maxrss                   6.2%    (57.8 σ)
- lake env                   instructions             2.6%   (104.6 σ)
- lake env                   maxrss                   6.1%   (107.4 σ)
- language server startup    branches                 1.9%    (37.6 σ)
- language server startup    instructions             1.9%    (34.4 σ)
- language server startup    maxrss                   8.5%    (71.6 σ)
- libleanshared.so           binary size              8.1%
- reduceMatch                instructions             2.2%    (94.8 σ)
- reduceMatch                maxrss                   4.6%   (613.8 σ)
- simp_arith1                branches                 1.8%   (250.7 σ)
- simp_arith1                instructions             1.8%   (235.8 σ)
- simp_arith1                maxrss                   3.8%   (269.6 σ)
- stdlib                     dsimp                   45.6%  (4124.2 σ)
- stdlib                     fix level params         7.4%   (128.4 σ)
- stdlib                     instantiate metavars    96.8%    (18.1 σ)
- stdlib                     instructions             9.3% (15096.4 σ)
- stdlib                     share common exprs      11.1%    (19.2 σ)
- stdlib                     tactic execution        18.8%   (109.8 σ)
- stdlib                     task-clock               6.8%   (113.0 σ)
- stdlib                     type checking           11.5%    (42.9 σ)
- stdlib size                bytes .olean             4.8%
- stdlib size                lines                    2.2%
- stdlib size                lines C                  8.1%
- tests/bench/ interpreted   maxrss                   3.7%   (155.9 σ)
- tests/compiler             sum binary sizes         6.9%
- workspaceSymbols           instructions             7.6%  (2977.5 σ)
- workspaceSymbols           maxrss                   4.9%   (181.8 σ)

[datokrat]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6d015f8.
There were significant changes against commit c073da2:

  Benchmark                   Metric                 Change
  ====================================================================
- binarytrees                 task-clock               4.3%   (43.7 σ)
- bv_decide_inequality.lean   branches                 1.1%  (215.9 σ)
- bv_decide_realworld         branches                 1.6%  (263.8 σ)
- bv_decide_realworld         instructions             1.5%  (317.9 σ)
- ilean roundtrip             branches                 8.3%  (565.7 σ)
- ilean roundtrip             instructions             8.4%  (417.2 σ)
- import Lean                 branches                 5.4%  (100.8 σ)
- import Lean                 instructions             5.6%  (121.5 σ)
- import Lean                 maxrss                   3.6%  (140.0 σ)
- lake build clean            instructions             1.0%   (22.4 σ)
- lake build no-op            maxrss                   4.0%   (84.7 σ)
- lake config elab            instructions             1.9%   (95.7 σ)
- lake config elab            maxrss                   5.0%   (73.4 σ)
- lake config import          instructions             3.2%   (82.4 σ)
- lake config import          maxrss                   5.4%  (109.6 σ)
- lake config tree            instructions             3.1% (1378.4 σ)
- lake config tree            maxrss                   5.5%  (157.5 σ)
- lake env                    instructions             3.2%   (77.2 σ)
- lake env                    maxrss                   5.5%   (72.2 σ)
- lake startup                instructions             2.1%   (27.5 σ)
- language server startup     branches                 3.6%   (60.1 σ)
- language server startup     instructions             3.8%   (51.5 σ)
- language server startup     maxrss                   7.9%   (70.6 σ)
- libleanshared.so            binary size              1.8%
- reduceMatch                 instructions             2.3%  (129.0 σ)
- reduceMatch                 maxrss                   4.0%  (207.3 σ)
- simp_arith1                 branches                 2.2%   (89.2 σ)
- simp_arith1                 instructions             2.1%  (112.0 σ)
- simp_arith1                 maxrss                   3.3%  (116.2 σ)
- stdlib                      dsimp                   47.0%   (95.5 σ)
- stdlib                      instantiate metavars    99.6%   (17.1 σ)
- stdlib                      instructions             8.9% (1888.9 σ)
- stdlib                      share common exprs      11.8%   (28.0 σ)
- stdlib                      tactic execution        21.1%  (660.6 σ)
- stdlib                      task-clock               7.8%   (48.7 σ)
- stdlib                      type checking           14.3%   (98.6 σ)
- stdlib                      wall-clock               1.2%   (18.7 σ)
- stdlib size                 bytes .olean             3.5%
- stdlib size                 lines                    2.3%
- tests/bench/ interpreted    maxrss                   3.1%   (20.8 σ)
- tests/compiler              sum binary sizes         1.4%
- workspaceSymbols            instructions             7.4% (5461.4 σ)
- workspaceSymbols            maxrss                   4.3%   (78.2 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-6914 build against this PR was cancelled. (2025-02-06 13:41:41) View Log
• 💥 Mathlib branch lean-pr-testing-6914 build failed against this PR. (2025-02-06 14:20:28) View Log
• ✅ Mathlib branch lean-pr-testing-6914 has successfully built against this PR. (2025-02-06 16:13:23) View Log
• ✅ Mathlib branch lean-pr-testing-6914 has successfully built against this PR. (2025-02-07 12:43:30) View Log

[TwoFX]

Might want to tone down the "Detailed performance optimizations will follow as soon as the new code generator is ready." in the description a bit; that makes it sound like the current implementation is completely unoptimized, which is not the case.

[TwoFX]

You should probably add yourself to the list of authors on a majority of the files.