Skip to content

feat: generalize LE, LT and the Std order-predicate classes to Sort u - #14737

Draft
sgraf812 wants to merge 6 commits into
masterfrom
sg/le-level-collapse
Draft

feat: generalize LE, LT and the Std order-predicate classes to Sort u#14737
sgraf812 wants to merge 6 commits into
masterfrom
sg/le-level-collapse

Conversation

@sgraf812

@sgraf812 sgraf812 commented Aug 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR generalizes the carriers of LE, LT, GE.ge, GT.gt, DecidableLE, DecidableLT, Std.IsPreorder, Std.IsPartialOrder, Std.IsLinearOrder, Std.IsLinearPreorder and Std.LawfulOrderLT from Type u to Sort u, so that propositions can carry order structure. It is the prerequisite for stating the order on Lean.Order fixpoint carriers in terms of Std.IsPartialOrder.

The library fallout is binder-level only. Metaprograms that build LE and LT applications pass the carrier's own universe where they used to pass its predecessor. Grind's order module works on Sort-carried goals, taking the argument LE takes as its per-carrier universe and recovering a Type level by decLevel where the Grind.Ring-constrained lemmas, which stay Type-fixed, need one.

Mathlib needs an adaptation of seven files, mostly Qq pattern universes and one notation elaborator.

@sgraf812 sgraf812 added the changelog-library Library label Aug 10, 2026
@sgraf812

sgraf812 commented Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Aug 10, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 2b77fd4 against 8d96b70 are in. No significant results found. @sgraf812

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run build differ between commits.
  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +7.4G (+0.06%)

Small changes (5🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.RingId//instructions: +141.7M (+1.69%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.StructId//instructions: +120.0M (+0.67%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Internalize//instructions: +66.1M (+0.52%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Proof//instructions: +160.3M (+4.20%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.StructId//instructions: +371.3M (+11.34%) (reduced significance based on *//lines)

@sgraf812 sgraf812 added needs-update-stage0 stage 0 should be updated after merging this PR awaiting-mathlib We should not merge this until we have a successful Mathlib build labels Aug 10, 2026
@sgraf812

sgraf812 commented Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Aug 10, 2026

Copy link
Copy Markdown

Benchmark results for 2b77fd4 against 8d96b70 are in. (These commits have already been benchmarked in a previous command.) No significant results found. @sgraf812

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run build differ between commits.
  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +7.4G (+0.06%)

Small changes (5🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.RingId//instructions: +141.7M (+1.69%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.StructId//instructions: +120.0M (+0.67%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Internalize//instructions: +66.1M (+0.52%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Proof//instructions: +160.3M (+4.20%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.StructId//instructions: +371.3M (+11.34%) (reduced significance based on *//lines)

@sgraf812
sgraf812 force-pushed the sg/le-level-collapse branch from 2b77fd4 to dde890c Compare August 10, 2026 16:53
@sgraf812

sgraf812 commented Aug 10, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Aug 10, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for dde890c against 3fc29d3 are in. No significant results found. @sgraf812

  • 🟥 build//instructions: +2.2G (+0.02%)

Small changes (5🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.RingId//instructions: +139.8M (+1.69%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.StructId//instructions: +137.1M (+0.77%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Internalize//instructions: +63.0M (+0.50%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Proof//instructions: +163.3M (+4.32%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.StructId//instructions: +364.8M (+11.28%) (reduced significance based on *//lines)

@github-actions github-actions Bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Aug 11, 2026
@sgraf812 sgraf812 added the release-ci Enable all CI checks for a PR, like is done for releases label Aug 11, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 11, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 11, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1d2dde6d64cb3da989bab118f4d386eb55237fe5 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-11 05:42:15)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 42a250c81d82d0fc39015b71319e4af7f2b91b5d --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-11 09:14:48)
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 42a250c81d82d0fc39015b71319e4af7f2b91b5d --onto 3fc29d37a70f8fd904ebab848557c12383543008. (2026-08-11 13:24:48)

@leanprover-bot

leanprover-bot commented Aug 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1d2dde6d64cb3da989bab118f4d386eb55237fe5 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-11 05:42:17)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 42a250c81d82d0fc39015b71319e4af7f2b91b5d --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-11 09:14:50)

@sgraf812
refactor: prepare metaprograms for generalizing LE and LT to `Sor…
e0ebf08 
…t u`

This PR makes every metaprogram that constructs an application of `LE`, `LT`, `Std.IsPreorder`, `Std.IsPartialOrder`, `Std.IsLinearOrder`, `Std.IsLinearPreorder` or `Std.LawfulOrderLT` derive the universe argument from the declared form of `LE`, so that generalizing these classes from `Type u` to `Sort u` needs no further compiler changes once this change is the stage0 compiler.

`Lean.leCarrierIsSort` classifies the declared form of `LE` once per process. Every affected site branches on it, with the else branch carrying the present code unchanged; the branch and its else are removed once the generalization lands. Pure helpers such as `Lean.Expr.mkNatLE` take the universe argument as a parameter, with the branch at their callers; the `Grind.CommRing.*_norm0` helpers likewise take the ring structure's universe argument, which coincides with the order structure's until the generalization. Grind's per-carrier order structure caches the universe argument `LE` takes at the carrier, so its downstream instantiation sites are unchanged; the `_k` helper lemmas whose `[Ring α]` constraint binds their carrier as a `Type` are constructed directly in the two ord-ring prefix builders.
@sgraf812
chore: trigger stage0 update
5fa671a
@sgraf812
chore: update stage0
0f19d72
@sgraf812
feat: generalize LE, LT and the Std order-predicate classes to …
9465533 
…`Sort u`

This PR generalizes the carriers of `LE`, `LT`, `GE.ge`, `GT.gt`, `DecidableLE`, `DecidableLT`, `Std.IsPreorder`, `Std.IsPartialOrder`, `Std.IsLinearOrder`, `Std.IsLinearPreorder` and `Std.LawfulOrderLT` from `Type u` to `Sort u`, so that propositions and proof-indexed function types can carry order structure. This is the prerequisite for stating the order on `Lean.Order` fixpoint carriers in terms of `Std.IsPartialOrder`.

The compiler needs no changes: since the previous stage0 update its `LE`/`LT` construction sites branch on the declared form of `LE`.
@sgraf812
fix: adjust the library to the Sort u order classes
dd07446
@sgraf812
sgraf812 force-pushed the sg/le-level-collapse branch from 35e2374 to f8b5216 Compare August 11, 2026 07:14
@sgraf812 sgraf812 added force-mathlib-ci and removed release-ci Enable all CI checks for a PR, like is done for releases awaiting-mathlib We should not merge this until we have a successful Mathlib build labels Aug 11, 2026
@sgraf812
refactor: remove the LE generalization scaffolding
88d74fd 
This PR removes the `leCarrierIsSort` classification and the branches it selected, keeping the code for the `Sort u` form of `LE` throughout, and returns the universe argument of the `Expr` comparison builders and the `Nat` simproc helpers to a fixed level. `Lean.OrderLevel` is deleted.
@sgraf812
sgraf812 force-pushed the sg/le-level-collapse branch from f8b5216 to 88d74fd Compare August 11, 2026 12:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner
@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-library Library changes-stage0 Contains stage0 changes, merge manually using rebase force-mathlib-ci needs-update-stage0 stage 0 should be updated after merging this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@sgraf812 @leanprover-radar @leanprover-bot