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. 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
• ✅ Mathlib branch lean-pr-testing-6914 has successfully built against this PR. (2025-02-10 10:35:58) View Log
• 🟡 Mathlib branch lean-pr-testing-6914 build against this PR was cancelled. (2025-02-10 11:48:34) View Log
• ✅ Mathlib branch lean-pr-testing-6914 has successfully built against this PR. (2025-02-10 13:09:18) View Log
• 🟡 Mathlib branch lean-pr-testing-6914 build against this PR was cancelled. (2025-02-10 14:05:56) View Log
• ✅ Mathlib branch lean-pr-testing-6914 has successfully built against this PR. (2025-02-10 15:25:46) View Log
• ✅ Mathlib branch lean-pr-testing-6914 has successfully built against this PR. (2025-02-10 16:31:51) View Log
• 💥 Mathlib branch lean-pr-testing-6914 build failed against this PR. (2025-02-10 17:42:34) View Log
• 💥 Mathlib branch lean-pr-testing-6914 build failed against this PR. (2025-02-11 12:02:34) View Log
• 💥 Mathlib branch lean-pr-testing-6914 build failed against this PR. (2025-02-11 13:33:22) View Log
• 💥 Mathlib branch lean-pr-testing-6914 build failed against this PR. (2025-02-11 15:01:31) View Log