I am looking into moving some lemmas about `N`

and `positive`

into the standard library, but the proofs I have use `Z`

(often through `lia`

). Refactoring to fit the definition dependency order may be feasible, but it looks like a good bit of of busywork, and in mathematics more generally there are definitely cases where the "best" proofs of lemmas about more primitive concepts use elaborate theories built on top of these concepts. However, currently `NArith`

cannot depend on `Z`

.

- Is there a precedent for how lemmas about N are proven using Z and presented to stdlib users? Or any analogous case
- What do you all think about internally renaming NArith to NArith_base and making NArith export Z-dependent lemmas too?

I don't really like it a priori, anything breaking modularity seems wrong to me (but I don't really have a say in this).

What are these new lemmas you want to add?

Are they missing in `PArith`

and `Arith`

as well?

Is there a module in `Numbers`

which could achieve some sort of generality?

A simple example is proving that `land`

and do not increase the value passed to them (`<=`

). The closest thing in the standard library is `log2_land`

which is proven using the abstract interfaces, but the manual proof there works by appealing to properties of log that aren't helpful in this case. With zify and lia, each of the Pos and N proofs is a oneliner. Earlier when adding other bitwise properties for Z only, I just created `Zbitwise`

outside the abstraction tower, perhaps unwisely, but again doing the same proofs without lia looks challenging.

More generally, I have the experience that stdlib is much less complete for Pos and N even for lemmas that are available for Z (about gcd, div, mod, etc). Maybe there is another reason for this, but the I don't think the current strict dependency order is helping. Basically what I wonder whether we would benefit from doing the opposite: using Z (and even Q) for most of the development, and later deriving N and Pos versions of theorems that also hold there.

If a general "Numbers"-like proof is not possible or too difficult, why not indeed transferring proofs in Z to N and pos. WIth namespaces (hopefully acting this year), that would be quite transparent user side. (Only my 2p though.)

IMHO we should have a base level of number theorems on top of which one can build "lia" and then have an advanced level which can use lia. I don't think it is a good idea to have a dependency hierarchy where no N lemma can depend on any Z lemma.

I agree. In addition to lia, there is also the ring tactic which uses N and Z (meaning `Coq.Arith.Arith`

depends on ZArith and which is why there is `Coq.Arith.Arith_base`

without that dependency). The initial proposal of @Andres Erbsen to extract some NArith_base (as pointed by @Michael Soegtrop it would just as well make sense to extract some ZArith_base) would certainly be a great progress. My understanding is that currently things are highly mixed up. When I tried to split this in packages that one could compile separatly, I managed to extract PArith but pretty much gave up on NArith/ZArith/ring/micromega due to the level of entanglement (FWIW, here is the dependency graph I ended up with: https://github.com/proux01/stdlib#compilation).

I guess the difficulties in splitting this up are historic - one used what is there in a certain point in time, so that we should have a lot of time induced dependencies. A nice design would come up with other dependencies, but then one has to redo a lot of proofs to adjust the dependencies. Unfortunately I don't think such dependencies are sufficiently canonical to emerge from themselves.

Last updated: Oct 13 2024 at 01:02 UTC