Naming conventions

[maximedenes]

@CohenCyril and I will extend https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#statements-of-lemmas-theorems-and-definitions

These conventions will be used in stdlib2.

Their description should be moved to the stdlib2 repository, and missing/unclear conventions can be discussed here.

[andres-erbsen]

"push" lemmas have often been named like mul_cos : cos(a)*cos(b) = (cos(a+b) + cos(a-b))/2, add_0_r, not_not_decidable. I find that naming scheme very intuitive and helpful, often allowing to skip a Search command. This scheme is also used quite widely in the current Coq library. I can see that the math-comp style is much more concise, but I am worried that this brevity might become an obstacle to new users. What are the other reasons for switching to that style?

[maximedenes]

Sorry, what do you mean by "push"?

A few remarks:

• we are not "switching", this is a clean-slate project. Maybe the name is misleading, but it is just to emphasize that the point is to get integrated as the standard library once stabilized.
• we are choosing the math-comp naming conventions mainly because it is documented and has been tested on a large scale. But if you have an alternative style satisfying these criteria, I can have a look at it.
• IMHO the right way to address concerns of beginners would be to have a "student" mode where Coq simplifies a bit the model it exposes (no implicit arguments, fewer tactics, etc). But this is out of scope for this project.

[herbelin]

I'd be interested in seeing a synthesis of all naming conventions we have around.

There is one here (to be eventually turned into a PDF).

If I remember correctly, @silene also had a proposal which he mentioned when we talked about naming conventions at a WG last year.

[maximedenes]

By the way, I don't think that there is a unique satisfactory naming convention. So, some arbitrary choice will be made at some point. We have so many technical points to solve that I don't expect to spend much time on naming conventions, although I will read all these documents to stay informed.

[herbelin]

I don't think that there is a unique satisfactory naming convention

I agree, and my conclusion about that was that the (challenging and interesting) way to address this heterogeneity of style is to turn naming conventions into languages of naming. But let's address things in order and start indeed by collecting the technical points to solve.

[andres-erbsen]

By "push" lemmas I mean the rules for commuting one operation from outside of other operations to inputs of these operations. Here are some push lemmas for Z.pow from the current standard library, named mostly as I described with the addition of _l and _r to distinguish two conceptually different inputs of Z.pow:

Z.pow_1_r: forall a : Z, (a ^ 1)%Z = a
Z.pow_0_l: forall a : Z, (0 < a)%Z -> (0 ^ a)%Z = 0%Z
Z.pow_0_r: forall n : Z, (n ^ 0)%Z = 1%Z
Z.pow_0_l': forall a : Z, a <> 0%Z -> (0 ^ a)%Z = 0%Z
Z.pow_opp_even: forall a b : Z, Z.Even b -> ((- a) ^ b)%Z = (a ^ b)%Z
Z.pow_2_r: forall a : Z, (a ^ 2)%Z = (a * a)%Z
Z.pow_opp_odd: forall a b : Z, Z.Odd b -> ((- a) ^ b)%Z = (- a ^ b)%Z
Z.pow_mul_l: forall a b c : Z, ((a * b) ^ c)%Z = (a ^ c * b ^ c)%Z
Z.pow_1_l: forall a : Z, (0 <= a)%Z -> (1 ^ a)%Z = 1%Z
Z.pow_succ_r: forall n m : Z, (0 <= m)%Z -> (n ^ Z.succ m)%Z = (n * n ^ m)%Z
Z.pow_twice_r: forall a b : Z, (a ^ (2 * b))%Z = (a ^ b * a ^ b)%Z
Z.pow_mul_r: forall a b c : Z, (0 <= b)%Z -> (0 <= c)%Z -> (a ^ (b * c))%Z = ((a ^ b) ^ c)%Z
Z.pow_add_r: forall a b c : Z, (0 <= b)%Z -> (0 <= c)%Z -> (a ^ (b + c))%Z = (a ^ b * a ^ c)%Z
Z.pow_sub_r: forall a b c : Z, a <> 0%Z -> (0 <= c <= b)%Z -> (a ^ (b - c))%Z = (a ^ b / a ^ c)%Z
Z.pow_div_l:
  forall a b c : Z, b <> 0%Z -> (0 <= c)%Z -> (a mod b)%Z = 0%Z -> ((a / b) ^ c)%Z = (a ^ c / b ^ c)%Z

I can't think of other naming conventions that I have clear opinions about, but this one has been very helpful in cases it is applicable. I don't particularly care that it is the only naming convention allowed for these lemmas, but I would find it unfortunate if names/aliases of this style were barred from inclusion in stdlib2. For more examples of this pattern, please see https://github.com/mit-plv/fiat-crypto/blob/4ecdd6ca43af688e5cd36ec9ab2496c4e192477d/src/Util/ZUtil/Hints/PullPush.v and https://github.com/mit-plv/fiat-crypto/search?q=push&unscoped_q=push

[silene]

@silene also had a proposal which he mentioned when we talked about naming conventions at a WG last year.

It was not so much a proposal than a description of the naming convention that we used in Coquelicot and in Flocq 3 and how it fared. The driving motivation was that the name of a theorem you need to apply to the current goal should be inferrable from the statement of the goal. I recall here the main principles for those who did not follow that WG:

1. If the conclusion of a theorem statement starts with a named predicate, its name also starts with it.
2. If the theorem is specific to some applied term, then the function name follows (unless it is not discriminating).
3. Similarly, if the term is a universally quantified variable but it has to satisfy a given predicate, then the name of this predicate follows (unless it is not discriminating).
4. If the predicate is an infix operator (e.g. order relation), rule 1 above is ignored and the operator is put into infix position.
5. If, due to an infix operator, the first part of a name would be an integer, the converse infix operator is used, just for naming.
6. Redundancies are avoided, unless discriminating.
7. If the theorem is a rewriting rule, equality is not mentioned in the name. So the name mostly reflects the left-hand side.
8. Right-hand sides of rewriting rules are either simpler than left-hand sides or more expanded. So the name mostly reflects the complicated term.
9. If the name is still not unique at this point, discriminating parts of the hypotheses are used.

Here are a few examples (premises are skipped unless relevant):

• generic_format_round: generic_format (round rnd x) (rules 1, 2)
• generic_round_generic: generic_format fexp1 x -> generic_format fexp1 (round fexp2 rnd x) (rules 1, 2, 3, 6)
• FLT_format_generic: generic_format beta FLT_exp x -> FLT_format x (rules 1, 3, 6)
• bpow_le: e1 <= e2 -> bpow e1 <= bpow e2 (rules 2, 4)
• lt_bpow: bpow e1 < bpow e2 -> e1 < e2 (rules 4, 9)
• mag_le_bpow: Rabs x < bpow e -> mag x <= e (rules 2, 4, 9)
• bpow_gt_0: 0 < bpow e (rules 2, 4, 5)
• mag_bpow: mag (bpow e) = e + 1 (rules 7 and 8)

That said, our approach is obviously flawed, since some theorems do not follow the above naming conventions.

To conclude, here are the main differences with MathComp's naming convention (and why we did not want to follow it):

• We never start a theorem name by one of its hypotheses.
• We never name a rewriting theorem using the description of its right-hand side.
• If the head symbol of the goal is a named predicate, we always start the theorem name with it.

[herbelin]

A concrete case about naming is given in coq/coq#8815, which, among others, adds the following NArith lemma:

Lemma succ_double_le n m : n <= m -> succ_double n <= succ_double m.

Coquelicot/Flocq would say succ_double_le.

If I understood correctly, MathComp rules would say le_succ_double (this policy is effectively used, e.g. for binary functions, in ssrnat.ltn_mul and ssrnum.ler_add, though there are exceptions, e.g. binomial.fact_smonotone, or falgebra.expvS).

Stdlib1 has many variants for such a lemma, such as BinNat.succ_double_lt, Ndec.Nleb_double_plus_one_mono, or, for other unary operators, e.g. for succ: BinPos.succ_lt_mono or Zorder.Zsucc_lt_compat; for Zpower: Zpow_facts.Zpower_le_monotone (a Frenchism); for pow: Rfunctions.Power_monotonic. The naming proposal in dev/doc/naming-conventions.tex would be quite verbose and say succ_double_lt_compat or double_plus_one_lt_compat.

So, maybe succ_double_le is indeed a good compromise (relatively short, as well as non-ambiguous, once we have learned the convention which distinguishes succ_double_le : n <= m -> succ_double n <= succ_double m and le_succ_double : succ_double n <= succ_double m -> n <= m)?

Any opinion in the context of stdlib2?

[vbgl]

About this particular example, I doubt that these lemmas should be in the standard library. Instead, a unique and more general (n.×2+1 ≤ m.×2+1) = (m ≤ n) seems also more convenient to use.

[herbelin]

About this particular example, I doubt that these lemmas should be in the standard library. Instead, a unique and more general (n.×2+1 ≤ m.×2+1) = (m ≤ n) seems also more convenient to use.

Good questions! Can you detail your vision? What should be the extent of a "standard library"? What should be the place of decidable relations? Can you give examples?