More Archimedean lemmas by pi8027 · Pull Request #1510 · math-comp/math-comp

pi8027 · 2025-12-04T11:15:27Z

Motivation for this change

This PR adds some lemmas for archiNumDomainType and archiRealDomainType using to_real (also to_nneg) suggested by @CohenCyril (cf. #1377 (comment)).

Most of these lemmas for floor and ceil generalize existing lemmas requiring the Num.real condition on a variable. Since the names of these lemmas have the prefix real_, the names of their general versions replace it with to_real_ for the moment. Similarly, some of the new lemmas for truncn have the prefix to_nneg_. (We probably need to think a bit more about the naming convention here.)

In the end, I didn't find floorP, ceilP, and truncnP stated using spec datatypes very useful (cf. #1377 (comment)). I keep their statements as comments for the moment.

I suggest extensively testing the new lemmas in MCA before merging this PR.

(Eventually) Fix #1377

Dependencies

Cleanup archimedean.v #1526

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.

Automatic note to reviewers

Read this Checklist.

pi8027 · 2025-12-04T11:36:58Z

MCA still uses Num.floor/Num.ceil/Num.truncn with Num.normr or absz in a few places. If Num.truncn does not subsume them, we should try to use Num.bound. It's defined in archimedean.v but currently lacks lemmas.

Definition bound (x : R) := (truncn `|x|).+1.

pi8027 · 2026-02-25T10:30:27Z

Rebased. I will take a fresh look at the PR and fix the naming issue this afternoon.

pi8027 · 2026-02-25T14:53:46Z

+(* TODO1: rename to real_eq_floor? *)
+(* TODO2: add a general version using to_real, and derive (to_)real_floor_itvP from it *)
 Lemma real_floor_eq x n : x \is real_num ->
  (floor x == n) = (n%:~R <= x < (n + 1)%:~R).
+Proof. by move=> ?; apply/eqP/real_floor_itvP. Qed.
+
+(* TODO: rename? *)
+Lemma floor_def x n : n%:~R <= x < (n + 1)%:~R -> floor x = n.


Any opinion on the renaming of these lemmas? I think real_floor_eq should be called something like real_eq_floor or real_eq_floor_itv, cf., meet_idPl and eq_meetl.

IMO, floor_def is almost the definition of floor, but only for the case where x \is real_num.

Maybe just floor_eq

and floor_default: x \isn't real_num -> floor x = 0

@CohenCyril Am I right that your suggestion was to rename (real_)floor_eq to (real_)eq_floor and then rename floor_def to floor_eq? (We can do the latter renaming only after releasing MC 2.7.)

And I prefer to add floor_default in a subsequent PR.

pi8027 · 2026-02-27T23:31:42Z

@CohenCyril @affeldt-aist @proux01 @hoheinzollern While this PR is far from ready, I think I have done almost everything I can. Since this PR addresses the issue you reported (#1377) or implements the solution you proposed (#1377 (comment)), your input is necessary at this point.

pi8027

I made some progress. I isolated the renaming of existing lemmas into the first commit. We can consider merging it first.

pi8027

I think this PR is ready for another round of review. Currently, the first commit does all the renamings of existing lemmas, and the second commit does the other changes. Perhaps the former part can be merged quickly. (If it is the case, I will split the PR.)

pi8027 · 2026-04-24T10:53:59Z

@CohenCyril @affeldt-aist @proux01 @hoheinzollern This PR is waiting for review.

proux01 · 2026-04-28T09:35:10Z

I'll do it but this may take me a bit of time to get to it.

pi8027 · 2026-06-03T10:45:29Z

@affeldt-aist FYI, this PR breaks infotheo. However, I won't fix it.

hoheinzollern · 2026-06-03T10:25:29Z

 Lemma ceilNfloor x : ceil x = - floor (- x).
 Proof. exact: ceil_subproof. Qed.

-Lemma truncEfloor x : truncn x = if floor x is Posz n then n else 0.


Shouldn't you write:

if 0 <= x then `|floor x|%N else 0%N;

like in truncn_subproof

hoheinzollern · 2026-06-03T10:28:22Z

 Lemma truncn_floor x : truncn x = if 0 <= x then `|floor x|%N else 0%N.
+Proof. exact: truncn_subproof. Qed.
+
+Lemma truncEfloor x : truncn x = if floor x is Posz n then n else 0.


Same as above?

Note that this lemma already exists in the master branch. I moved the lemma, but the statement is unchanged. Changing it would require deprecation.

And, since this PR has been open for 6 months, I would rather do the suggested change in another PR.

hoheinzollern

Apart from the open comments, the PR looks good to me.

hoheinzollern · 2026-06-04T11:26:49Z

Of course, it needed rebase (now done) and docs.

pi8027 · 2026-06-04T13:44:09Z

I added changelog entries.

@CohenCyril @proux01 Could you double-check and merge this PR after the release of MC 2.6? It targets MC 2.7, and I won't change it to 2.6. (I'm against to merge any PR in a rush before a release.)

pi8027 commented Dec 4, 2025

View reviewed changes

Comment thread algebra/archimedean.v Outdated

pi8027 mentioned this pull request Jan 2, 2026

lemmas from MathComp-Analysis' unstable.v #1515

Merged

4 tasks

pi8027 requested a review from affeldt-aist January 2, 2026 15:14

pi8027 force-pushed the archimedan-lemmas branch from f0fac3a to 24c11d8 Compare January 26, 2026 17:41

pi8027 mentioned this pull request Jan 26, 2026

Cleanup archimedean.v #1526

Merged

2 tasks

pi8027 force-pushed the archimedan-lemmas branch from 24c11d8 to 934a425 Compare January 27, 2026 13:53

pi8027 force-pushed the archimedan-lemmas branch from 934a425 to 2188e06 Compare February 25, 2026 10:29

pi8027 force-pushed the archimedan-lemmas branch from 2188e06 to 84df4f1 Compare February 25, 2026 14:21

pi8027 commented Feb 25, 2026

View reviewed changes

Comment thread algebra/archimedean.v Outdated

pi8027 requested review from CohenCyril and proux01 February 25, 2026 22:25

pi8027 force-pushed the archimedan-lemmas branch from 84df4f1 to 16f0e30 Compare February 26, 2026 10:30

pi8027 added this to the 2.7.0 milestone Feb 26, 2026

pi8027 mentioned this pull request Feb 26, 2026

Use Num.bound math-comp/analysis#1862

Merged

1 task

pi8027 requested a review from hoheinzollern February 27, 2026 23:31

pi8027 force-pushed the archimedan-lemmas branch from 16f0e30 to 8bc40dc Compare March 12, 2026 14:57

pi8027 force-pushed the archimedan-lemmas branch 2 times, most recently from 2401b4f to 5677272 Compare March 25, 2026 16:18

CohenCyril reviewed Apr 1, 2026

View reviewed changes

Comment thread algebra/archimedean.v Outdated

CohenCyril self-requested a review April 1, 2026 11:46

pi8027 force-pushed the archimedan-lemmas branch from 5677272 to 56f1f2e Compare April 8, 2026 16:32

pi8027 changed the title ~~More Archimedan lemmas~~ More Archimedean lemmas Apr 9, 2026

pi8027 force-pushed the archimedan-lemmas branch from 56f1f2e to 35d1b4f Compare April 9, 2026 12:33

pi8027 commented Apr 9, 2026

View reviewed changes

Comment thread algebra/archimedean.v

Comment thread algebra/archimedean.v Outdated

Comment thread algebra/archimedean.v Outdated

pi8027 force-pushed the archimedan-lemmas branch 2 times, most recently from 5c2589f to fc46e67 Compare April 13, 2026 15:08

pi8027 force-pushed the archimedan-lemmas branch from fc46e67 to b2f972b Compare April 15, 2026 14:49

pi8027 commented Apr 15, 2026

View reviewed changes

Comment thread algebra/archimedean.v

pi8027 force-pushed the archimedan-lemmas branch from b2f972b to 9195dc8 Compare April 17, 2026 11:49

pi8027 force-pushed the archimedan-lemmas branch from 9195dc8 to d105851 Compare May 6, 2026 15:33

pi8027 force-pushed the archimedan-lemmas branch 2 times, most recently from 200e30b to b504f5d Compare May 27, 2026 14:41

pi8027 marked this pull request as ready for review May 27, 2026 14:42

pi8027 force-pushed the archimedan-lemmas branch from b504f5d to 78b9a84 Compare May 28, 2026 10:38

hoheinzollern reviewed Jun 3, 2026

View reviewed changes

hoheinzollern approved these changes Jun 3, 2026

View reviewed changes

t6s mentioned this pull request Jun 4, 2026

fix for mathcomp PR 1510 affeldt-aist/infotheo#224

Merged

pi8027 added 2 commits June 4, 2026 13:06

Rename archimedean lemmas

b97bc0a

Add new archimedean lemmas

da358b3

pi8027 force-pushed the archimedan-lemmas branch from 9c0f9d7 to da358b3 Compare June 4, 2026 11:06

Add changelog entries

0403b5a

Conversation

pi8027 commented Dec 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Dependencies

Minimal TODO list

Automatic note to reviewers

Uh oh!

Uh oh!

pi8027 commented Dec 4, 2025

Uh oh!

pi8027 commented Feb 25, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

pi8027 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

pi8027 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

pi8027 commented Apr 24, 2026

Uh oh!

proux01 commented Apr 28, 2026

Uh oh!

pi8027 commented Jun 3, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

hoheinzollern left a comment

Choose a reason for hiding this comment

Uh oh!

hoheinzollern commented Jun 4, 2026

Uh oh!

pi8027 commented Jun 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

pi8027 commented Dec 4, 2025 •

edited

Loading

pi8027 commented Feb 27, 2026 •

edited

Loading