feat: add Std.Trichotomous

[linesthatinterlace]

This PR adds Std.Tricho r, a typeclass for relations which identifies them as trichotomous. This is preferred to Std.Antisymm (¬ r · ·) in all cases (which it is equivalent to).

[linesthatinterlace]

See discussion in https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Std.20Trichotomous/with/546933901

[leanprover-community-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 e71d0abc7ddb2c9da37e91b88fd2be2a903601c7 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-24 16:55:35)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e71d0abc7ddb2c9da37e91b88fd2be2a903601c7 --onto 97d63db52cd2fc3353f8a75f48209de0011f1bd3. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-27 11:10:38)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e71d0abc7ddb2c9da37e91b88fd2be2a903601c7 --onto 106b0fa661d96fd1fa6ff96e2ee5f55f23f307f2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-30 14:48:12)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-04 12:13:09)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e71d0abc7ddb2c9da37e91b88fd2be2a903601c7 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-24 16:55:36)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-04 12:13:10)

[datokrat]

!bench

[leanprover-radar]

Benchmark results for 6cc5bd3 against e71d0ab are in! @datokrat

[leanprover-bot]

Here are the benchmark results for commit 6cc5bd3.
There were significant changes against commit e71d0ab:

  Benchmark              Metric                    Change
  ================================================================
- iterators (compiled)   wall-clock                  5.6% (39.7 σ)
- stdlib                 grind dsimp                 5.3% (25.5 σ)
- stdlib                 process pre-definitions     1.3% (24.3 σ)
- stdlib                 task-clock                  1.0% (40.2 σ)

[linesthatinterlace]

I will address your comments when I can (I have some work things which may take a little time). Bit worried about the performance hit here but maybe restoring those instances will fix that.

[datokrat]

Yes, I find it quite amazing how hard it can be to predict the performance impact of small changes to the typeclass hierarchy. In this case, I'm especially confused by the iterators (compiled) entry: This benchmark does not do any instance synthesis at all. It just runs a compiled program.

Radar (our new speedcenter that is still under development) luckily confirms that at least the specific iterators (compiled) slowdown was a fluke: https://radar.lean-lang.org/repos/lean4/commits/6cc5bd3f9efa1c0f09209fa36923c8b2cac17d7c?parent=e71d0abc7ddb2c9da37e91b88fd2be2a903601c7&s=iterators+

[datokrat]

Note: I slightly edited the PR description to match our changelog convention (removing the -- at the top and removing the newline before the second sentence so that "This is preferred to..." is still visible in the changelog. I did not change anything about the wording.

[linesthatinterlace]

Other than that one question about restoring instances (where I am concerned that taking a divergent approach with Total/Asymm and Antisymm/Trichotomous could lead to confusion down the line) I have acted on your comments, so (accepting that we still have that one question to resolve) I am going to pass this back.

[linesthatinterlace]

Right - apologies for the delay. This is ready for review again I believe.

[datokrat]

Right - apologies for the delay. This is ready for review again I believe.

No problem at all (and my review was also a bit delayed).

[linesthatinterlace]

Right, should be all done.

[linesthatinterlace]

awaiting-review