Rework of PR #281: Archimedean structures on top of num/real domain/field/closedField

[pi8027]

Motivation for this change

This PR renames the archiFieldType structure to archiRealFieldType and introduces 5 new Archimedean ring/field structures. These structures are currently defined in ssrnum.v, but will be relocated to a new file archimedean.v in a future release. We also generalize truncation (truncC), floor (floorC), the subset of natural integers (Cnat, Qnat, and Znat), and the subset of integers (Cint and Qint) to Archimedean rings, which are now Num.trunc, Num.floor, Num.nat, and Num.int respectively.

Closes #281

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
• added corresponding documentation in the headers
• merge dependency: Drop support for Coq 8.10 #686

CI overlays

• Fix w.r.t. math-comp/math-comp#682 coq-community/fourcolor#27
• Fix w.r.t. math-comp/math-comp#682 odd-order#28

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

[pi8027]

Currently, classfun.v is broken since it uses Cint, but importing ssrint adds the infix ^ notation which collides with that of group_scope.

It seems that group notations and ring notations are mixed almost everywhere in classfun.v. So there is no other solution than adding %g whenever required. If a scope declaration for arguments of coercion to Funclass works, this situation probably becomes better. But this does not work in the current implementation of Coq (see coq/coq#5527 (comment)):

Arguments fun_of_cfun [gT] [B] _ _%g.

[pi8027]

I guess Qint and Qnat should be deprecated and superseded by Cint and Cnat respectively. Right? @CohenCyril

[CohenCyril]

I guess Qint and Qnat should be deprecated and superseded by Cint and Cnat respectively. Right? @CohenCyril

Yes! And Cint and Cnat should both be renamed Num.int and Num.nat.

[CohenCyril]

I guess Qint and Qnat should be deprecated and superseded by Cint and Cnat respectively. Right? @CohenCyril

Yes! And Cint and Cnat should both be renamed Num.int and Num.nat.

And they should be in the mixin, so as to make the computations for ssrint and rat faster!

[pi8027]

Yes! And Cint and Cnat should both be renamed Num.int and Num.nat.

And they should be in the mixin, so as to make the computations for ssrint and rat faster!

Make sense. Allowing the use of Cint without importing ssrint would also be nice to get a better fix for classfun and inertia. But reimplementing Cint theory in the absence of ssrint would require some more work.

[pi8027]

@CohenCyril Could you confirm this is what you mean?

(* Module ArchiNumDomain. *)
Record mixin_of (R : numDomainType) := Mixin {
  trunc : R -> nat;
  is_nat : pred R;
  is_int : pred R;
  _ : forall x, 0 <= x -> (trunc x)%:R <= x < (trunc x).+1%:R;
  _ : forall x, is_nat x = ((trunc x)%:R == x);
  _ : forall x, is_int x = is_nat x || is_nat (- x);
}.

[CohenCyril]

@CohenCyril Could you confirm this is what you mean?

(* Module ArchiNumDomain. *)
Record mixin_of (R : numDomainType) := Mixin {
  trunc : R -> nat;
  is_nat : pred R;
  is_int : pred R;
  _ : forall x, 0 <= x -> (trunc x)%:R <= x < (trunc x).+1%:R;
  _ : forall x, is_nat x = ((trunc x)%:R == x);
  _ : forall x, is_int x = is_nat x || is_nat (- x);
}.

Yes roughly, except the truncation has no reason to be only for non negative numbers, I would prefer the function in the mixin to be more general, knowing that there could be a factory providing opaque trunc, is_nat, and is_int from a nat upper bound.

I had planned to wait for HB to make this kind of changes... I am a bit surprised you are willing to go through so much work while we intend to trivialize all of this...

[pi8027]

Yes roughly, except the truncation has no reason to be only for non negative numbers, I would prefer the function in the mixin to be more general, knowing that there could be a factory providing opaque trunc, is_nat, and is_int from a nat upper bound.

The problem is that we have to relocate the basic part of ssrint (int and intmul at least?) to ssrnum (or ssralg?) in order to generalize the truncation to the negative case. Since the above mixin has been proved equivalent to Num.archimedean_axiom, we can provide such a factory.

I had planned to wait for HB to make this kind of changes... I am a bit surprised you are willing to go through so much work while we intend to trivialize all of this...

Reworking an existing branch is easier to do now rather than later. Also, IMO actual difficulties appear in places other than the definitions of structures, as in the breakage of classfun.v.

[pi8027]

Cnat, Cint, truncC, and floorC have been renamed to Num.nat, Num.int, Num.trunc, and floorR respectively. I guess we have to relocate ssrint.int (or make the dependency from ssrint to ssrnum opposite) to rename floorR to Num.floor anyway.

[pi8027]

Almost done except that floorR is still not a part of the Archimedean mixin and defined in ssrint. I'm not sure what to do about this point.

[pi8027]

Here is a summary of possible solutions:

1. Keeping the dependency relation of libraries as is, placing truncR, Rnat, and Rint in ssrnum, and placing floorR in ssrint (the current situation):
   • Pros: This solution works.
   • Cons: floorR cannot be located in ssrnum.Num (we can declare another Num module in ssrint to work around this, but it seems troublesome). The floorR functions of int and rat cannot be as straightforward/efficient as we expect. The archiNumDomainType theory has to be separated into two parts (one in ssrnum and another in ssrint).
2. Keeping the dependency relation of libraries as is, but relocating int and intmul from ssrint to ssrnum or before to include floorR and related lemmas in ssrnum:
   I think this solution does not work, because statements and proofs of some lemmas about floorR require, e.g., canonical ringType and orderType instances of int. So we have to relocate a significant part of ssrint anyway.
3. Changing the dependency relation of libraries to make ssrnum requiring ssrint:
   This solution may work. But the canonical numDomainType of int has to be defined in ssrnum or later, and then some lemmas about int cannot be stated in ssrint, e.g., abszE which requires the norm function.
4. Adding another library that requires both ssrnum and ssrint, and relocating the Archimedean structures and related lemmas to it:
   I think this is the best solution among these, but requires at least two steps of transition.

[CohenCyril]

Yet another solution: dispatching the contents of ssrint between ssralg and ssrnum.

[pi8027]

@CohenCyril That is what I meant in solution 3 IIUC.

[CohenCyril]

@CohenCyril That is what I meant in solution 3 IIUC.

Indeed. It was not clear to me whether you were suggesting to remove the file ssrint, which is what I suggest here.

[CohenCyril]

Anyway, I like solution 4... it makes a lot of sense to me. How would you envision the transitiom though? Having files with new names required by files with old names?

[pi8027]

Indeed. It was not clear to me whether you were suggesting to remove the file ssrint, which is what I suggest here.

I did not suggest removing ssrint.v. So they are actually different. But, anyway...

Anyway, I like solution 4... it makes a lot of sense to me. How would you envision the transitiom though? Having files with new names required by files with old names?

In the first step, we try to relocate definitions and lemmas about the Archimedean structures as much as possible, to a new file, say archimedean.v. Since we have to deprecate Znat and related lemmas in ssrint, we cannot relocate some of them. So we declare them as Local ones in ssrnum or ssrint, provide deprecation aliases if needed, and also provide non-deprecated aliases in archimedean.v. I think this trick is also applicable to definitions of structures. In the second step, we remove deprecation aliases and relocate everything that depends on archiNumDomainType to archimedean.v.

[pi8027]

BTW, why CI disappeared from the checklist here?

[CohenCyril]

BTW, why CI disappeared from the checklist here?

no idea, that's very strange

[CohenCyril]

@pi8027

BTW, why CI disappeared from the checklist here?

This is now fixed (cf #706 (comment)). In principle, if you rebased this PR for example, github would show the status of the CI. Although I believe with the ongoing stuff on HB it would not make sense to rebase it. Just so you know

[proux01]

@pi8027 @CohenCyril now that 2.0 is out, I rebased this and CI is green. I'd like to merge by the end of the week if there is no more comments (I'll open an issue to remember the above points about Rnat_sum_eq1 and Rnat_prod_eq1).

[proux01]

The remaining comments will be addressed in #1030 depending on this.

[proux01]

No more comments apparently so I'll merge on Friday.

[CohenCyril]

Just a few remarks befor we merge.

[CohenCyril]

The R in Rnat and Rint does not respect any existing convention. It should either be documented or renamed.
I am in favor of naming them nat_num and int_num inside this file, and then nat and int directly so that they can be used through Num.nat and Num.int later on.

[proux01]

Done, I thus renamed "Rnat" in lemma names to "nat" or "natr". This yields a few conflicts with "natr" already used for %:R which I solved using a few "nat_num". This is not perfect but I think it's acceptable.

Also note that we already had Rpos, Rneg and Rreal which should probably be deprecated/renamed pos_num, neg_num and real_num in a separate PR.

[CohenCyril]

Done, I thus renamed "Rnat" in lemma names to "nat" or "natr". This yields a few conflicts with "natr" already used for %:R which I solved using a few "nat_num". This is not perfect but I think it's acceptable.

I'm not sure having natr for lemmas about nat_num is desirable...

Also note that we already had Rpos, Rneg and Rreal which should probably be deprecated/renamed pos_num, neg_num and real_num in a separate PR.

Sure we should also deal with Rpos, Rneg and Rreal