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:21:00Z


-Lemma floor_def x m : m%:~R <= x < (m + 1)%:~R -> floor x = m.
+Lemma to_real_floor_idP x n :
+  reflect (floor x = n) (n%:~R <= to_real x < (n + 1)%:~R).


@affeldt-aist @proux01 @hoheinzollern To answer your question (#1377 (comment)), floor_def and real_floor_itv are more or less the converses of each other. This lemma to_real_floor_idP (also real_floor_idP and floor_idP below) reformulates them using reflect.
However, real_floor_idP below does not nicely subsume floor_def, because the assumption x \is Num.real is deduced from n%:~R <= x in the proof of the latter.

(Now I think floor_idP is not the right name... floor_itvP?)

floor_itvP sounds good

I renamed it to (to_real_)floor_itvP.

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 · 2026-04-09T12:35:50Z

+#[deprecated(since="mathcomp 2.7.0", use=real_floor_gez)]
+Notation real_floor_ge_int := real_floor_gez (only parsing).
+#[deprecated(since="mathcomp 2.7.0", use=real_floor_ltz)]
+Notation real_floor_lt_int := real_floor_ltz (only parsing).
+#[deprecated(since="mathcomp 2.7.0", use=real_ceil_lez)]
+Notation real_ceil_le_int := real_ceil_lez (only parsing).
+#[deprecated(since="mathcomp 2.7.0", use=real_ceil_gtz)]
+Notation real_ceil_gt_int := real_ceil_gtz (only parsing).


Following Cyril's suggestion during the meeting, I replaced _int with z in these names.

pi8027 · 2026-04-09T12:36:21Z

+Notation truncn_ge_nat := truncn_gen (only parsing).
+#[deprecated(since="mathcomp 2.7.0", use=truncn_gtn)]
+Notation truncn_gt_nat := truncn_gtn (only parsing).
+#[deprecated(since="mathcomp 2.7.0", use=truncn_ltn)]
+Notation truncn_lt_nat := truncn_ltn (only parsing).
+#[deprecated(since="mathcomp 2.7.0", use=real_truncn_len)]
+Notation real_truncn_le_nat := real_truncn_len (only parsing).


Similarly, I replaced _nat with n here.

Shouldn't the suffixes _gen and _len by _geq and _leq like in ssrnat.v?

I was hesitating between the two. To be honest, I don't know. @CohenCyril

For example, the way I would read truncn_len is: truncn x is less than or equal to n, for some x and natural number n. I'm unsure if we can read it in the same way if we replace n with q.

That being said, I think _gen and _len are confusing. What about _ge(q)_n and _le(q)_n?

After thinking about it twice, I decided to use _leq and _geq.

pi8027 · 2026-04-09T12:38:13Z


 (* Factories *)

+HB.factory Record NumDomain_hasFloorCeilTruncn R & Num.NumDomain R := {


This was the mixin of the Archimedean structures before this PR, and this should be deprecated and eventually removed. What is the right suffix (like _truncn_abs_floor) for this one?

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-15T14:51:11Z

-Lemma truncnD :
-  {in nat_num & nneg_num, {morph truncn : x y / x + y >-> (x + y)%N}}.


I renamed this to truncnDnr to introduce truncnDrn. I'm unsure if they are the right name since this r has to be non-negative.

Looking at CONTRIBUTING.md and num_theory/, the shorthand for nneg_num seems to be wp (weak positive ?). So they should probably be called truncnDn(_)wp and truncnDwp(_)n. Any opinion?

Another option is to use D as an infix symbol like M in rMn: truncn_nDwp and truncn_wpDn. But, we need to rename similar lemmas for floor and ceil too.

We can also postpone introducing truncnDrn to address this naming issue later.

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 commented Dec 4, 2025

View reviewed changes

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

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

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

pi8027 added 2 commits May 6, 2026 17:32

Rename archimedean lemmas

ed9f26a

Add new archimedean lemmas

d105851

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


		(* Factories *)

		HB.factory Record NumDomain_hasFloorCeilTruncn R & Num.NumDomain R := {

		Lemma truncnD :
		{in nat_num & nneg_num, {morph truncn : x y / x + y >-> (x + y)%N}}.

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!

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!

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!

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!

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

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!

pi8027 left a comment

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!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pi8027 commented Apr 24, 2026

Uh oh!

proux01 commented Apr 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

pi8027 commented Dec 4, 2025 •

edited

Loading

pi8027 commented Feb 27, 2026 •

edited

Loading

pi8027 Apr 9, 2026 •

edited

Loading

pi8027 Apr 16, 2026 •

edited

Loading