rename `GRing.exp` to `pown` #1503

affeldt-aist · 2025-11-27T04:36:03Z

Motivation for this change

as decided during the regular meeting

Minimal TODO list

added changelog entries ~~with doc/changelog/make-entry.sh~~

added corresponding documentation in the headers
tried to abide by the contribution guide
this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

pi8027

While I'm not providing an exhaustive review, I think many lemmas are poorly named. In many of them, pownr should be changed to powrn because of the order of the parameters of pown.

What about expn in ssrnat.v and exprz in intmul.v? (The latter is indeed not a power function, but do we really want GRing.pown to be a "power function" while we call exprz "exponentiation"?)

pi8027 · 2025-11-27T11:27:15Z

algebra/ssralg.v

-Lemma expr2 x : x ^+ 2 = x * x. Proof. by []. Qed.
+Lemma pownr0 x : x ^+ 0 = 1. Proof. by []. Qed.
+Lemma pownr1 x : x ^+ 1 = x. Proof. by []. Qed.
+Lemma pownr2 x : x ^+ 2 = x * x. Proof. by []. Qed.


I think that these lemmas should be called powr0n, powr1n, and powr2n, because these 0, 1, and 2 are nat. (See mulr0n, mulr1n, and mulr2n in nmodule.v.)

pi8027 · 2025-11-27T11:28:03Z

algebra/ssralg.v

+Lemma pownr2 x : x ^+ 2 = x * x. Proof. by []. Qed.

-Lemma exprS x n : x ^+ n.+1 = x * x ^+ n.
+Lemma pownrS x n : x ^+ n.+1 = x * x ^+ n.


~~powrSn~~ powrS, like mulrS

pi8027 · 2025-11-27T11:28:32Z

algebra/ssralg.v


-Lemma expr0n n : 0 ^+ n = (n == 0%N)%:R :> R.
-Proof. by case: n => // n; rewrite exprS mul0r. Qed.
+Lemma pown0n n : 0 ^+ n = (n == 0%N)%:R :> R.


pow0rn, like mul0rn

Also, the names pown0n and pown1n (below) look ambiguous because they do not contain r; that is, these names do not indicate that these lemmas are for ring-like structures.

pi8027 · 2025-11-27T11:28:49Z

algebra/ssralg.v


-Lemma expr1n n : 1 ^+ n = 1 :> R.
-Proof. by elim: n => // n IHn; rewrite exprS mul1r. Qed.
+Lemma pown1n n : 1 ^+ n = 1 :> R.


pi8027 · 2025-11-27T11:31:09Z

algebra/ssralg.v


-Lemma exprD x m n : x ^+ (m + n) = x ^+ m * x ^+ n.
-Proof. by elim: m => [|m IHm]; rewrite ?mul1r // !exprS -mulrA -IHm. Qed.
+Lemma pownrD x m n : x ^+ (m + n) = x ^+ m * x ^+ n.


powrDn? But I'm not so sure. (The additive counterpart is mulrnDr, but it makes sense only because natmul is both left- and right-distributive.)

pi8027 · 2025-11-27T11:32:48Z

algebra/ssralg.v


-Lemma exprSr x n : x ^+ n.+1 = x ^+ n * x.
-Proof. by rewrite -addn1 exprD expr1. Qed.
+Lemma pownrSr x n : x ^+ n.+1 = x ^+ n * x.


powrSr, like mulrSr?

pi8027 · 2025-11-27T11:33:48Z

algebra/ssralg.v

 Qed.

-Lemma exprMn_n x m n : (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.
+Lemma pownMn_n x m n : (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.


powrMn_n?

pi8027 · 2025-11-27T11:34:00Z

algebra/ssralg.v

 Qed.

-Lemma exprM x m n : x ^+ (m * n) = x ^+ m ^+ n.
+Lemma pownrM x m n : x ^+ (m * n) = x ^+ m ^+ n.


affeldt-aist · 2025-11-27T12:09:18Z

Thanks for the comments.

For the naming, I have indeed taken a conservative approach, essentially using pown as a substitute for exp and I refrained from removing too quickly the n in pown despite simplifications suggested by positional notations because maybe we do not want to use the shortest notation now in case a power function appears soon in MathComp.

As for ssrnat and ssrint, I thought of doing it later (even in another PR) because the review of this PR will answer several questions about naming that will tell us what to do about ssrnat and ssrint and also because we might want to get ssralg.v asap since it is the target of current, orthogonal revisions.

pi8027 · 2025-11-27T12:20:54Z

I refrained from removing too quickly the n in pown despite simplifications suggested by positional notations because maybe we do not want to use the shortest notation now in case a power function appears soon in MathComp.

The names I suggested do not remove n but move n, except for powrS and powrSr where S already means the successor of nat. So there is no ambiguity here.

As for ssrnat and ssrint, I thought of doing it later (even in another PR) because the review of this PR will answer several questions about naming that will tell us what to do about ssrnat and ssrint and also because we might want to get ssralg.v asap since it is the target of current, orthogonal revisions.

I consider this transitional state a major naming inconsistency, and thus, I prefer to make these changes in a single PR. At the very least, we need to have a rough idea of how we will converge.

pi8027 · 2025-11-27T12:24:21Z

IIRC, the motivation of this change is a name conflict with an exp function of type R -> R -> R in MCA. ~~What about renaming GRing.exp (resp. exprz) to GRing.natexp (resp. intexp)?~~ I revised my proposal below.

pi8027 · 2025-11-27T12:58:36Z

@affeldt-aist Is this the meeting you're referring to? It doesn't even say we decided to rename GRing.exp to pown: https://github.com/math-comp/math-comp/wiki/Minutes-2024-09-04

affeldt-aist · 2025-11-27T13:00:13Z

@affeldt-aist Is this the meeting you're referring to? It doesn't even say we decided to rename GRing.exp to pown: https://github.com/math-comp/math-comp/wiki/Minutes-2024-09-04

https://github.com/math-comp/math-comp/wiki/Minutes-2025-09-17

pi8027 · 2025-11-27T13:29:32Z

IMO, the following definitions should ideally follow the same naming pattern, with no ambiguity/naming conflict:

Algebra.natmul in nmodule.v (= GRing.natmul in ssralg.v),
natexp in monoid.v (= expgn in fingroup.v),
GRing.exp in ssralg.v, and
intmul and exprz in ssrint.v.

One solution I can think of is to make the following renaming:

Algebra.natmul -> Algebra.mulrn,
natexp -> expgn (expgn in fingroup.v should disappear),
GRing.natmul -> GRing.mulrn,
GRing.exp -> GRing.exprn,
intmul -> mulrz, and
exprz stays as is.

Although GRing and r in GRing.mulrn and GRing.exprn are redundant, we probably shouldn't shorten them to GRing.muln and GRing.expn, since it introduces naming conflicts with muln and expn of ssrnat.v inside the GRing module.

What do you think?

pi8027 · 2025-11-27T13:37:02Z

I also argue that renaming GRing.exp to GRing.pown is a bad idea, while GRing.pow*r*n might be acceptable, because we may eventually want to rename expn to pown.

affeldt-aist · 2025-11-27T14:58:22Z

What do you think?

I'll address all your comments but I am a bit skeptical about enlarging the scope of this PR to other naming issues because it could take a long time to complete.

pi8027 · 2025-11-27T15:07:09Z

I agree that my proposal goes beyond what we usually do in a single PR. I think that renaming GRing.exp to GRing.exprn (optionally natexp to expgz) and some lemmas is already good enough, if we agree to converge towards my proposal eventually. At least, such a change does not seem to introduce a new naming inconsistency, which is my concern regarding GRing.pown.

pi8027 · 2025-11-27T15:26:48Z

I suggest waiting for some input from others before starting any implementation work. @Tragicus @CohenCyril @proux01

CohenCyril · 2025-11-28T08:00:41Z

I think I would prefer the n to be used as in the GRing.natmul conventions. e.g. powr0n : x ^+ 0 = 1

CohenCyril · 2025-11-28T08:17:48Z

@pi8027 thanks for questioning the renaming, however please do not target this PR or @affeldt-aist who kindly volunteered to experiment with the change we decided during the above mentioned meeting.
Your thoughts on the topic are necessary to converge, and to me this implementation of the change raised many unforeseen inconveniences, but I do not think any next action should be taken before reaching another consensus during a mathcomp meeting.

affeldt-aist · 2025-11-28T08:24:57Z

by the way, on the MathComp-Analysis side, @jmmarulang has been working to extend powR (power function for real numbers) to poweR (the same for extended real numbers) and has generated many lemmas, maybe we can take a look at the status of their theories during a next meeting, we might learn something about which conventions would scale better (fyi: @hoheinzollern)

pi8027 · 2025-12-04T23:42:33Z

@CohenCyril Right. I didn't see the issues before reading the patch.

@affeldt-aist Just in case, let me write down the naming convention I suggest here, so that we can discuss it further at some point. This is based on my understanding of the naming convention for the lemmas about GRing.natmul and intmul.

As a rule of thumb, a lemma whose conclusion has the form ?r ^+ ?n = _ should be called exp<r><n> (or pow<r><n> if we decide to rename GRing.exp), where:

<r> is the abbreviation corresponding to ?r. For example:
- <r> is r if ?r is a variable,
- <r> is 1r if ?r is 1%R,
- <r> is Mr if ?r is (_ * _)%R, and
- <r> is rMn if ?r is (_ *+ _)%R.
<n> is the abbreviation corresponding to ?n. For example:
- <n> is n if ?n is a variable,
- <n> is 1n if ?n is 1%N,
- <n> is S if ?n is S _, and
- <n> is Dn if ?n is (_ + _)%N.

Note that we shouldn't use very short abbreviations like M and D (instead of Mr and Dn above), because these r and n represent the types of ?r and ?n to disambiguate with exp of other types, e.g., nat -> nat -> nat, R -> int -> R, and R -> R -> R. For example, expMn : ((_ * _) ^+ _)%R = _ is too ambiguous. When we need a separator between <r> and <n>, we put _, e.g., exprMn_n. On the other hand, when we have GRing.exp as a subterm of LHS like ?r and ?n above, its abbreviation is rXn or Xn.

As a result, the names of lemmas for exp (_ ^ _) of type R -> R -> R may need further disambiguation with GRing.exp. For example, a lemma whose LHS has the form _ ^ (_ *+ _) should probably be called expr_rMn rather than exprMn (which is already taken by ssralg.v).

Although it obviously doesn't cover everything, I hope it conveys my idea.

affeldt-aist added this to the 2.6.0 milestone Nov 27, 2025

affeldt-aist added the kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...) label Nov 27, 2025

rename GRing.exp to pown

e55cf5b

affeldt-aist force-pushed the expn_pown branch from d8e78f5 to e55cf5b Compare November 27, 2025 08:03

affeldt-aist requested review from CohenCyril and proux01 November 27, 2025 08:04

fix CI

40a1f5b

pi8027 requested changes Nov 27, 2025

View reviewed changes

fix

9493266

rename GRing.exp to pown #1503

Are you sure you want to change the base?

rename GRing.exp to pown #1503

Uh oh!

Conversation

affeldt-aist commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Minimal TODO list

Automatic note to reviewers

Uh oh!

pi8027 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pi8027 Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

affeldt-aist commented Nov 27, 2025

Uh oh!

pi8027 commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Nov 27, 2025

Uh oh!

affeldt-aist commented Nov 27, 2025

Uh oh!

pi8027 commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Nov 27, 2025

Uh oh!

affeldt-aist commented Nov 27, 2025

Uh oh!

pi8027 commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Nov 27, 2025

Uh oh!

CohenCyril commented Nov 28, 2025

Uh oh!

CohenCyril commented Nov 28, 2025

Uh oh!

affeldt-aist commented Nov 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Dec 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

rename `GRing.exp` to `pown` #1503

rename `GRing.exp` to `pown` #1503

affeldt-aist commented Nov 27, 2025 •

edited

Loading

pi8027 left a comment •

edited

Loading

pi8027 Nov 27, 2025 •

edited

Loading

pi8027 commented Nov 27, 2025 •

edited

Loading

pi8027 commented Nov 27, 2025 •

edited

Loading

pi8027 commented Nov 27, 2025 •

edited

Loading

pi8027 commented Nov 27, 2025 •

edited

Loading

affeldt-aist commented Nov 28, 2025 •

edited

Loading