Using properties of arithmetic operations on [nat] in standard library

Using Coq
1

The standard library seems to contain various approaches to arithmetic operations on nat.
This includes files mentioned to be “mostly OBSOLETE now”.
Depending on which files/modules are imported, the available properties/lemmas seem to be different.
What is the current recommended way to use arithmetic operations on nat? what should be imported? is there a natural place where one can find (a list of) the available properties? if not, would it be interesting to create such an interface file?

Thanks.

1 Like
2

For a more consistent and carefully structured version of arithmetic on nat, I recommend ssrnat.v in MathComp’s ssreflect package, (coq-mathcomp-ssreflect on OPAM). See the comments at the top of the file for documentation of the key operations.

The only crux of using this library is that the lia decision procedure cannot be applied directly most of the time. However, this can be solved by using the ppsimpl package (coq-ppsimpl on OPAM).

One example:

Require Import Lia.
From PP Require Import Ppsimplmathcomp.
From mathcomp Require Import all_ssreflect.
(*...*)
have Ht: (size trace <= n.+2) by ppsimpl; lia.