Alternative take on #153: fix `le` in future versions of Coq

This should provide compatibility for https://github.com/coq/coq/pull/12162

Other changes:

• Use Arith instead of NPeano, since the latter is deprecated. While it may also be possible to import NPeano, numbers export PArith NArith ZArith, so it seemed logical to also export Arith.
• Add test to check for correct version of le.

Which symbols does this now also put into the already extremely polluted global namespace of every std++-using application?

Probably a lot, but we already got these via numbers, prelude, list, and pretty much and other file but base.

Do we? Arith is not exported anywhere.

We used to export NPeano in numbers, according to https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.Natural.Peano.NPeano.html it's deprecated and Arith should be used instead.

Sounds more like PeanoNat should be used.

Arith exports at least all these things: https://coq.inria.fr/distrib/current/stdlib/Coq.Arith.Arith_base.html

Since we export PArith NArith ZArith QArith in numbers, it seemed logical to also export Arith.

That said, I really don't understand how the files for numbers in the stdlib work, it's such a spaghetti of kludges put on top of each other.

Oh you mean because these are all "on the same level" in https://coq.inria.fr/distrib/current/stdlib/index.html ? Hm, I can see that.

However, we actually just import QArith. Makes me wonder if we should try to turn some of the others into imports, too...

So yeah I think I prefer this over !153 (closed) -- could you make this an MR? I'l run the test on the reverse dependencies.

However, we actually just import QArith. Makes me wonder if we should try to turn some of the others into imports, too...

That's because we generally use Qp, and QArith is mostly a means to define Qp.

Yeah, you just claimed above that we exported it, hence my response.

Don't we need to re-export Arith here to give it precedence over the others?

(But please don't push here now while the reverse dependency tests are running.)

So why does nothing here shadow things from Arith? Would it be better to add Arith to the end just to be sure its names take precedence?

Makes sense. Can you push to this branch and rerun the CI?

Maybe tomorrow I have more time, right now I shouldn't start coding Coq stuff.^^

I pushed. If you can rerun the CI for the reverse deps sometimes, that'd be great.

That's just a shell command, that's easy. ;)

CI again came back all-clean.

Great. Shall we merge this MR then?

I ran this through CI and our reverse deps are all fine.

added 1 commit

• 8e38d217 - Also import `Arith` in numbers to make sure it shadows (just to be sure).

Compare with previous version

Code looks good, but

• should this be in the changelog?
• can we have a comment explaining why the exports are the way they are?

Regarding the "spaghetti of kludges put on top of each other" of arith files in stdlib, I am also a bit lost.

Concerning Arith (I did not dig into other *Arith), what I understand is that Arith gathers PeanoNat with obsolete files. Using PeanoNat and properties named Nat.* is apparently the safest way to go. It apparently misses very few useful statements from my own experience. I just tried on std++: replacing Arith with PeanoNat works. Only one occurrence in numbers.v:

@@ -1,9 +1,9 @@
 (** This file collects some trivial facts on the Coq types [nat] and [N] for
 natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
-From Coq Require Export EqdepFacts PArith NArith ZArith Arith.
+From Coq Require Export EqdepFacts PArith NArith ZArith PeanoNat.
 From Coq Require Import QArith Qcanon.
 From stdpp Require Export base decidable option.
 Set Default Proof Using "Type".
 Local Open Scope nat_scope.

I don't know for projects using std++.

For the current MR: apparently Arith is not good at masking Bool.le. From what I have been able to see, only Peano (which contains the primary definition of le) does the job. Note also that it has to be called after any import of Bool (which is in particular coming with Program.Syntax through BVector). What seems to work is to add:

From Coq Require Export Peano.

at the end of Requires in base.v:

@@ -1,15 +1,16 @@
 (** This file collects type class interfaces, notations, and general theorems
 that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Arith.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+From Coq Require Export Peano.
 
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See
 also strings.v and
 https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and

(tested both on master and master + PR#12162)

@olaure01

For the current MR: apparently Arith is not good at masking Bool.le.

So you are saying, the MR as-is does not build with your Coq change?

Yes: building stdpp + !156 (closed) against coq + coq/coq#12162 gives the same errors as building std++ master against coq + coq/coq#12162.

mentioned in merge request !159 (merged)

mentioned in commit ef839489

Closing in favor of !159 (merged).

closed