Split `order.v` by pi8027 · Pull Request #1580 · math-comp/math-comp

pi8027 · 2026-04-20T10:22:27Z

Motivation for this change

Since order.v is 8k lines long and the largest file in MathComp, this PR splits it into smaller pieces. This is the result:

$ wc order/*.v
     1      3     22 order/all_order.v
  1659  10520  65624 order/complemented_lattice_instances.v
   637   3769  23625 order/complemented_lattice.v
   820   6133  34117 order/lattice_instances.v
  2148  14386  85315 order/lattice.v
   125    643   4642 order/order_instances.v
   177   1529  12929 order/order.v
   842   5291  29276 order/porder.v
  1911  13834  75124 order/preorder.v
  2047  13860  80854 order/total_order_instances.v
  1228   8636  45177 order/total_order.v
 11595  78604 456705 total

This PR also reduces the compilation time of MC in several scenarios: #1580 (comment)

Closes #1508

Minimal TODO list

added changelog entries with doc/changelog/make-entry.sh

added corresponding documentation in the headers
tried to abide by the contribution guide
this PR contains an optimum number of meaningful commits

See this Checklist for details.

TODO list

They are more or less sorted by importance/urgency. Less important ones can be done in separate PRs. See #1580 (comment) for details.

Overlays

Dependencies

Automatic note to reviewers

Read this Checklist.

proux01 · 2026-04-23T16:19:51Z

Maybe the instances can go in three files? (the last one requiring the tow other independent ones)

pi8027 · 2026-04-27T22:38:06Z

I added a long TODO list to the PR description above. It would be great if I could discharge some of them, since I won't be able to address all of them. Here I elaborate on them:

TODOs for this PR

Name conflicts of `ltEprod` and `lt_pair`

In the current master branch, they are spread across preorder.v and order.v. So, we didn't notice the name conflicts.

math-comp/order/preorder.v

Lines 2723 to 2724 in 77e80d5

    
           Lemma ltEprod x y : 
        
             (x < y) = (x.1 < y.1) && (x.2 <= y.2) || (x.1 <= y.1) && (x.2 < y.2).

math-comp/order/order.v

Line 6244 in 33421d3

Lemma ltEprod x y : (x < y) = [&& x != y, x.1 <= y.1 & x.2 <= y.2].

math-comp/order/preorder.v

Lines 2734 to 2736 in 77e80d5

    
           Lemma lt_pair (x1 y1 : T1) (x2 y2 : T2) : 
        
             ((x1, x2) < (y1, y2) :> T1 * T2) 
        
             = (x1 < y1) && (x2 <= y2) || (x1 <= y1) && (x2 < y2).

math-comp/order/order.v

Lines 6247 to 6248 in 33421d3

    
           Lemma lt_pair (x1 y1 : T1) (x2 y2 : T2) : ((x1, x2) < (y1, y2) :> T1 * T2) = 
        
             [&& (x1 != y1) || (x2 != y2), x1 <= y1 & x2 <= y2].

[DONE] PR overlays

[DONE] Propagate the changes to the rest of MathComp

As of now, we often need only total_order(_instances) in MathComp. Requiring only a part of the order package may reduce the time spent on Require Import. We should also stop using Order.LTheory, Order.TTheory, and Order.CTheory.

[DONE] Compare the compilation time before/after this PR

Reducing compilation time is part of the motivation of this PR. So, we need to confirm that it actually reduces the compilation time. We need to do it in several scenarios: make -j 1, make -j 8, package-wise build, etc.

TODOs for MathComp 2.7

I would like to address the following items in the same milestone as this PR, so that users don't need to adapt their proof script to this series of changes several times.

[DONE] Move the lexicographic order instances on tuples from `order_instances.v` to `total_order_instances.v`

See #1580 (comment).

Decide what we do with the order instances on `sub_type`

See #1583. #1584 removed the [POrder of T by <:] and [Order of T by <:] notations. This PR removes the DeprecatedSubOrder module, but keeps the two order instances on sub_type. We need to decide wether we try to eventuall remove the instances on sub_type or not.

Move `interval.v` and `orderedzmod.v` to `order/`

We should also re-export them from order.v. The latter relocation is currently blocked. See #1560.

Completing the subtype hierarchy with semilattices and split `lattices.v`

This is actually two items, but closely related. Adding more subtype structures would increase the size of lattices.v. We will see whether it is reasonable to further split lattices.v only after that.

TODOs with no milestone

Extend `lattice.v` with modular lattices

See #613 and #653.

pi8027 · 2026-05-06T13:12:40Z

@affeldt-aist Do you mind reviewing the header documentation and the changelog entries?

affeldt-aist · 2026-05-06T14:31:37Z

It is difficult for me to act on this before Saturday. I will try to do that tomorrow evening JST.

pi8027 · 2026-05-06T14:41:56Z

No hurry since I aim to merge this shortly after the release, not before.

pi8027 · 2026-05-20T09:51:52Z

If a part of the reviews arrives before the 27th, I should be able to make some progress during the MathComp sharing day.

pi8027 · 2026-05-28T10:30:06Z

It is difficult for me to act on this before Saturday. I will try to do that tomorrow evening JST.

@affeldt-aist Any news?

affeldt-aist · 2026-05-28T10:45:24Z

It is difficult for me to act on this before Saturday. I will try to do that tomorrow evening JST.

@affeldt-aist Any news?

No, I'm sorry, I can't find time. :-(

pi8027 · 2026-05-28T13:16:07Z

@hoheinzollern @t6s By any chance, are you able to review the documentation part of this PR?

t6s · 2026-05-28T14:52:22Z

@hoheinzollern @t6s By any chance, are you able to review the documentation part of this PR?

sure. I'll see it in a few days

t6s

Looked through the changelog and header docs, and they look mostly good.
It seems 04-removed/1580-split-order.md needs to be updated. Please check.
I have also suggested two minor corrections.

…attice.v

t6s · 2026-06-03T01:27:10Z

I am satisfied by the current state of the documentation!

hoheinzollern · 2026-06-05T07:42:49Z

Since this is a huge PR and it's hard to check that everything is preserved, I built a mapping showing where HB instances, lemmas and notations went:

hoheinzollern · 2026-06-05T07:56:17Z

Comments about the mapping:

ltgtP and leP are dropped, though they are specializations of comparable_ltgtP and comparable_leP respectively. @pi8027 does this come at no loss of ergonomics?
andKb, orKb are dropped as they are already present in Corelib
le_def (4288), meet_eql, joinUKI, lcmnn, le_def (5530), andbE, orbE, setKUC, setKIC are all helpers to build HB instances, which are preserved, the lemmas are safe to drop (le_def is still available as a mixin field in preorder.v, so only the local helpers are lost)

pi8027 · 2026-06-08T10:26:56Z

ltgtP and leP are dropped, though they are specializations of comparable_ltgtP and comparable_leP respectively. @pi8027 does this come at no loss of ergonomics?

If you are talking about these, they are in an HB.builders section and not exposed to users.

math-comp/order/order.v

Lines 4179 to 4186 in 1054971

    
           Fact ltgtP x y : 
        
             compare x y (min y x) (min x y) (max y x) (max x y) 
        
                         (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). 
        
           Proof. exact: comparable_ltgtP. Qed. 
        
           Fact leP x y : le_xor_gt x y 
        
             (min y x) (min x y) (max y x) (max x y) (x <= y) (y < x). 
        
           Proof. exact: comparable_leP. Qed.

The ltgtP and leP lemmas exposed to users are definitely preserved. See total_order.v. (By the way, they are Definition but not Lemma.)

andKb, orKb are dropped as they are already present in Corelib

They are internal lemmas for building lattice instances on bool.

math-comp/order/order.v

Lines 5612 to 5616 in 1054971

    
           Fact orKb b a : a && (a || b) = a. 
        
           Proof. by rewrite orbC orKb. Qed. 
        
           Fact andKb y x : x || x && y = x. 
        
           Proof. by rewrite andbC andKb. Qed.

le_def (4288), meet_eql, joinUKI, lcmnn, le_def (5530), andbE, orbE, setKUC, setKIC are all helpers to build HB instances, which are preserved, the lemmas are safe to drop (le_def is still available as a mixin field in preorder.v, so only the local helpers are lost)

Idem.

pi8027 added the kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...) label Apr 20, 2026

pi8027 added this to the 2.7.0 milestone Apr 20, 2026

pi8027 force-pushed the split-order branch 3 times, most recently from 39efbf5 to 20cd9f1 Compare April 22, 2026 23:36

pi8027 mentioned this pull request Apr 23, 2026

DeprecatedSubOrder module in order.v #1583

Closed

pi8027 force-pushed the split-order branch 6 times, most recently from 03938d9 to 2cc96da Compare April 23, 2026 15:57

This comment was marked as outdated.

Sign in to view

pi8027 force-pushed the split-order branch from 2cc96da to 3ec644d Compare April 23, 2026 18:09

This comment was marked as outdated.

Sign in to view

pi8027 force-pushed the split-order branch 3 times, most recently from 8ce164a to d0ee04c Compare April 27, 2026 21:49

pi8027 marked this pull request as ready for review April 27, 2026 23:28

pi8027 mentioned this pull request Apr 28, 2026

Remove [POrder of T by <:] and [Order of T by <:] #1584

Merged

4 tasks

pi8027 force-pushed the split-order branch 2 times, most recently from cafd341 to 0233f5b Compare April 28, 2026 13:30

pi8027 mentioned this pull request Apr 28, 2026

Adapt to math-comp/math-comp#1580 imdea-software/fcsl-pcm#60

Merged

aleksnanevski pushed a commit to imdea-software/fcsl-pcm that referenced this pull request Apr 28, 2026

Adapt to math-comp/math-comp#1580 (#60)

4f55ee2

pi8027 mentioned this pull request Apr 29, 2026

Replace Fact and #[local] Lemma (for internal lemmas) with Let #1569

Open

pi8027 force-pushed the split-order branch 2 times, most recently from f735b88 to dfe2e9f Compare April 30, 2026 11:00

pi8027 force-pushed the split-order branch from 65622e9 to bf5227a Compare May 6, 2026 16:08

pi8027 force-pushed the split-order branch from bf5227a to 13e0fda Compare May 15, 2026 15:14

pi8027 force-pushed the split-order branch 2 times, most recently from 0195e5b to 120d40e Compare May 28, 2026 10:20

pi8027 requested review from hoheinzollern and t6s and removed request for affeldt-aist May 28, 2026 10:58

t6s reviewed Jun 1, 2026

View reviewed changes

Comment thread order/lattice.v Outdated

Comment thread order/order.v Outdated

Comment thread doc/changelog/04-removed/1580-split-order.md Outdated

Comment thread doc/changelog/04-removed/1580-split-order.md Outdated

pi8027 added 9 commits June 2, 2026 13:06

Gather the general documentation about the order package

2f01467

Isolate the order structure instances to order_instances.v

4dcb637

Reorder the contents of preorder.v

248f0d7

Isolate partial order structures and theory to porder.v

a199baa

Split order.v into three: lattice.v, total_order.v and complemented_l…

c0ed9c4

…attice.v

Split order_instances.v into 4 files

4c8fd7a

Documentation

99b23d7

Propagation

0d7f795

Changelog

6115ed1

pi8027 force-pushed the split-order branch from 120d40e to 6115ed1 Compare June 2, 2026 11:10

Uh oh!

Conversation

pi8027 commented Apr 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Minimal TODO list

TODO list

Overlays

Dependencies

Automatic note to reviewers

Uh oh!

This comment was marked as outdated.

proux01 commented Apr 23, 2026

Uh oh!

This comment was marked as outdated.

This comment was marked as outdated.

pi8027 commented Apr 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

TODOs for this PR

Name conflicts of ltEprod and lt_pair

[DONE] PR overlays

[DONE] Propagate the changes to the rest of MathComp

[DONE] Compare the compilation time before/after this PR

TODOs for MathComp 2.7

[DONE] Move the lexicographic order instances on tuples from order_instances.v to total_order_instances.v

Decide what we do with the order instances on sub_type

Move interval.v and orderedzmod.v to order/

Completing the subtype hierarchy with semilattices and split lattices.v

TODOs with no milestone

Extend lattice.v with modular lattices

Uh oh!

pi8027 commented May 6, 2026

Uh oh!

affeldt-aist commented May 6, 2026

Uh oh!

pi8027 commented May 6, 2026

Uh oh!

pi8027 commented May 20, 2026

Uh oh!

pi8027 commented May 28, 2026

Uh oh!

affeldt-aist commented May 28, 2026

Uh oh!

pi8027 commented May 28, 2026

Uh oh!

t6s commented May 28, 2026

Uh oh!

t6s left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

t6s commented Jun 3, 2026

Uh oh!

hoheinzollern commented Jun 5, 2026

Uh oh!

hoheinzollern commented Jun 5, 2026

Uh oh!

pi8027 commented Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

pi8027 commented Apr 20, 2026 •

edited

Loading

pi8027 commented Apr 27, 2026 •

edited

Loading

Name conflicts of `ltEprod` and `lt_pair`

[DONE] Move the lexicographic order instances on tuples from `order_instances.v` to `total_order_instances.v`

Decide what we do with the order instances on `sub_type`

Move `interval.v` and `orderedzmod.v` to `order/`

Completing the subtype hierarchy with semilattices and split `lattices.v`

Extend `lattice.v` with modular lattices

pi8027 commented Jun 8, 2026 •

edited

Loading