Stream: Coq users

Topic: plus versus add


view this post on Zulip Robbert Krebbers (Aug 08 2022 at 14:41):

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?

view this post on Zulip Karl Palmskog (Aug 08 2022 at 16:11):

I think Nat.add is the new non-deprecated way to access nat's addition

view this post on Zulip Karl Palmskog (Aug 08 2022 at 16:11):

and this is consistent across Z.add and Q.add

view this post on Zulip Karl Palmskog (Aug 08 2022 at 16:13):

I think the person to ask on the history of Nat.add vs. Nat.plus is @Olivier Laurent

view this post on Zulip Olivier Laurent (Aug 08 2022 at 16:32):

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.

view this post on Zulip Robbert Krebbers (Aug 09 2022 at 07:45):

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

view this post on Zulip Robbert Krebbers (Aug 09 2022 at 07:48):

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

view this post on Zulip Karl Palmskog (Aug 09 2022 at 07:50):

OK, I may have been thinking only about Z

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:23):

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.

view this post on Zulip Meven Lennon-Bertrand (Aug 24 2022 at 13:31):

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