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
andQ.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: Oct 13 2024 at 01:02 UTC