There's quite a mix of the use of the name `plus`

(and `mult`

, `minus`

, etc) versus `add`

(and `mul`

, `sub`

, etc) in the Coq standard library.

It seems the convention to use `add`

(and friends) has been introduced in the Numbers API, but the primitive definitions for nat still use `plus`

. Similarly, for Q and Qc only the name `plus`

seems to be used.

Does anyone know the history of this discrepancy? And what's the consensus for new lemmas, should they use `plus`

or `add`

?

I think `Nat.add`

is the new non-deprecated way to access `nat`

's addition

and this is consistent across `Z.add`

and `Q.add`

I think the person to ask on the history of `Nat.add`

vs. `Nat.plus`

is @Olivier Laurent

I don't really know about the details of the history but the ongoing work on stdlib pushes towards the use of `Nat.add`

(after importing `PeanoNat`

or `Arith`

to get associated lemmas). And similarly for `Nat.mul`

and `Nat.sub`

.

Good to now that add/mul is the new way to go. Then I guess std++ and Iris should follow suit, see https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/404

Karl Palmskog said:

and this is consistent across

`Z.add`

and`Q.add`

Are you sure it's consistent for `Q`

? Looks like there's still `Qplus`

(and no module `Q`

). https://github.com/coq/coq/blob/master/theories/QArith/QArith_base.v#L246

OK, I may have been thinking only about `Z`

I always thought of plus as the symbol and add as its operation. At least in British English, it is common to say "plus sign" and addition or summation for the operation, though the former is the binary one.

Olivier Laurent said:

I don't really know about the details of the history

I randomly stumbled upon this is the changelog for Coq 8.4: *It provides with unified notations (e.g. systematic use of add and mul for denoting the addition and multiplication operators)*. So I guess there was a move towards `add`

, but that never was completed?

Last updated: Jan 29 2023 at 03:28 UTC