Alternative take on #153: import `Arith` in `base`.

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.