Add reg theorems for nat on multiplication

[HaoYang670]

Fixes / closes #17354

[proux01]

We already have

Lemma eqn_pmul2l m n1 n2 : 0 < m -> (m * n1 == m * n2) = (n1 == n2).
Lemma eqn_pmul2r m n1 n2 : 0 < m -> (n1 * m == n2 * m) = (n1 == n2).

why would you need a weaker version? (if the implication is really needed, one can use eqbLR or eqbRL)

[HaoYang670]

Hi @robbertkrebbers, do we still need these?

[proux01]

Ho, sorry it's about Coq stdlib here. I accidentally mixed up with MathComp, so please disregard my comment above.
I have no opinion about that part of the the stdlib since I'm not using it.

[robbertkrebbers]

Thanks for the PR.

I think it's important that Z and other number types are consistent. So we should either have this lemma for all Numbers instances, or none at all. Otherwise it's confusing.

If we want to have them for all, we should remove the specific versions for Z and the comment, see https://github.com/coq/coq/blob/master/theories/ZArith/BinInt.v#L1281

If we want to have them for none at all, we should deprecated the versions for Z and have a warning that says to use the <-> lemma instead.

[HaoYang670]

Hi @robbertkrebbers, should we define a type class for all number types?

[robbertkrebbers]

There is a module in Coq for all number types, and my suggestion is that the reg lemmas should be part of that module.

[HaoYang670]

Hi @robbertkrebbers, could I know which module it is?

[robbertkrebbers]

NZMulOrderProp I think, here's the abstract version of the biimplication that was mentioned in the issue: https://github.com/coq/coq/blob/master/theories/Numbers/NatInt/NZMulOrder.v#L100

[HaoYang670]

Move mul_reg_l and mul_reg_r from BigInt to NZMulOrder.

[proux01]

Note that if you (re)move lemmas, you need a deprecation (https://coq.inria.fr/distrib/current/refman/using/libraries/writing.html).

[robbertkrebbers]

Note that if you (re)move lemmas, you need a deprecation (https://coq.inria.fr/distrib/current/refman/using/libraries/writing.html).

Unless I am mistaken, you can still refer to the Z lemmas by Z.lem. It merely got moved to a different place and generalized from Z to all instances of Numbers.

[robbertkrebbers]

By the way, it appears there are plenty of more lemmas specific to Z in https://github.com/coq/coq/blob/master/theories/ZArith/BinInt.v#L1281 which should either be generalized to Numbers or be deprecated.

[HaoYang670]

Thank you, @proux01 @robbertkrebbers for your review!

Note that if you (re)move lemmas, you need a deprecation (https://coq.inria.fr/distrib/current/refman/using/libraries/writing.html).

Unless I am mistaken, you can still refer to the Z lemmas by Z.lem. It merely got moved to a different place and generalized from Z to all instances of Numbers.

I am not familiar with the module type in Coq. But actually, I can't refer Z.mul_reg_l or Z.mul_reg_r. I need to check if Z implements NZMulOrderProp.

By the way, it appears there are plenty of more lemmas specific to Z in https://github.com/coq/coq/blob/master/theories/ZArith/BinInt.v#L1281 which should either be generalized to Numbers or be deprecated.

Good point!. I filed #17606 to track it

[HaoYang670]

@coqbot run full ci

[Zimmi48]

Sorry, @HaoYang670, this coqbot command only works if you're a member of @coq/contributors. We should make coqbot provide feedback when it ignores it. Let me re-run it for you.

@coqbot run full CI

[SkySkimmer]

Not sure if CI failures are real, at least some of them are not so let's get a fresh run
@coqbot run full ci

@coq/stdlib-maintainers please take a decision on this PR instead of waiting another year

[andres-erbsen]

Let's merge if CI passes.