Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib

Rename _plus/_minus into _add/_sub to be consistent with Coq's current convention for numbers.

Following the discussion at iris!821 (merged)

assigned to @robbertkrebbers

Just to be super sure, do you have a link demonstrating that this is indeed Coq's convention now?

Let's see what the Coq folks say. https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/plus.20versus.20add

I get the impression from that thread that add/mul are indeed the way to go. That is also consistent with our choice for Qp, see !188 (merged)

Okay, then LGTM. Feel free to land whenever you have time to fix all the dependencies.

While we're at it, it seems we sometimes use Nat_ and sometimes nat_. For example:

Global Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
Lemma Nat_lt_succ_succ n : n < S (S n).
Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).

The Nat_ seems to imitate the Nat. lemmas in Coq, but nat_ is more like the standard std++ style.

Considering Coq's fantastic module system, we could also dump all our own Nat lemmas in a module Nat. Then there will be multiple Nat modules (one in the stdlib, and one in std++'s numbers), but as long as the lemmas are disjoint, that works just fine.

Would we use modules for all number types them?

I wouldn't mind doing some experimentation with modules. We should just test it carefully before merging.

mentioned in merge request iris!821 (merged)

added 18 commits

• 33fc8e62...02fd8ca3 - 16 commits from branch master
• dc815d28 - Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current...
• bb414ed6 - Modules for `Pos` and `Nat`.

Compare with previous version

I have done an experiment for nat and positive. See last commit in this MR. I did not update the sed script.

Feedback is welcome.

I am happy to continue this experiment for other number types and evaluate the impact on Iris and some other developments (I expect the sed script can port all of them trivially).

added 1 commit

• e548e71b - Same for Z and coercions between Z/N/Pos/nat.

Compare with previous version

Done the same for Z.

Now Qc and Qp remain. For Qp it should be more of the same.

Qc is weird since (1) the Coq stdlib does not does a module for it, (2) the Coq stdlib still uses plus/mult/etc for it, and (3) in std++ Qc is mostly used as an implementation detail of Qp.

added 1 commit

• e81d12ea - Same for `Qp`.

Compare with previous version

Would be good if you could try porting Iris, to ensure it works there.

If Qc is an implementation detail we should probably not pollute the global namespace with its lemmas...

I ported Iris, it was trivial: iris@e1f9c08b

added 4 commits

• 6ac287a0 - Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current...
• e7374676 - Modules for `Pos` and `Nat`.
• 0f60c18e - Same for Z and coercions between Z/N/Pos/nat.
• 8758522a - Same for `Qp`.

Compare with previous version

changed title from Rename {-_-}plus{-/_-}minus{- into _add/_sub-} to be consistent with Coq's current... to Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib

added 16 commits

• 8758522a...809dee91 - 10 commits from branch master
• aa8376e2 - Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current...
• b42404a3 - Modules for `Pos` and `Nat`.
• 1ac5e9d6 - Same for Z and coercions between Z/N/Pos/nat.
• 05ae1a51 - Same for `Qp`.
• 9377a916 - Export `Nat` and friends in our `Nat`.
• 5eb4810f - CHANGELOG.

Compare with previous version

added 2 commits

• 2d1a821e - Export `Nat` and friends in our `Nat`.
• 394f401f - CHANGELOG.

Compare with previous version