Towards a naming convention for the standard library?

[tahina-pro]

TR: Currently experimenting on FStar.Seq (proposed changes coming soon.)
I propose the following guidelines:

1. Prefix each lemma name with lemma_
   This convention seems to be in progress of being adopted. It totally makes sense in F* to clearly separate operators from their properties (compared to Coq, where a lemma is really an ordinary term which can very well appear in the definition of something that is more than just a proof term).
2. Names of lemmas about the interaction of two functions foo(bar(…))
   should be named lemma_foo_bar, with a suffix if there are several of them.
   Examples in FStar.Seq: lemma_of_list_length -> lemma_length_of_list; lemma_of_list -> lemma_index_of_list
3. Lemma names indexed by _1, _2, etc.
   should be avoided in favor of more expressive names, for instance:
   • foo_intro, foo_elim for “general principles” of foo in conclusion vs. foo in hypotheses (convention seems to be already adopted)
   • foobin_bar_left, foobin_bar_right for lemmas about interactions between a binary operator and another operator, i.e. pertaining to foobin(bar(…), …), foobin(…, bar(…)) respectively.
     Example in FStar.Seq: lemma_index_app1 -> lemma_index_append_left; lemma_index_app2 -> lemma_index_append_right
     Question: should we use shorter suffixes such as _l, _r (cf. Coq: plus_0_r)
   • get_set_same, get_set_other for interactions between getter and setter (cf. CompCert maps: gss, gso)
     Example in FStar.Seq: lemma_index_upd1 -> lemma_index_upd_same; lemma_index_upd2 -> lemma_index_upd_other
4. Ideally, names of operators should be fully spelled out.
   • At least, they should be spelled out in the same way in the operator name as in the lemma name. For instance, the name of any lemma about an operator called length should be based on length rather than len
     Example in FStar.Seq: lemma_len_slice -> lemma_length_slice
   • Exception: mem instead of member (see Coq/OCaml: List.mem).
   • Question: What about upd vs. update? Source?
5. Ideally, auxiliary lemmas named with _aux should be private
   I claim, to reduce the base of lemmas when translating to Z3/Lean.

[nikswamy]

Regarding 1:

This sounds quite reasonable, at first.

However, Lemma in F* is just an abbreviation for Pure unit. As such, it isn't particularly special. I see it really as quite similar to a Prop in Coq.

Generalizing this convention, should the effect of a function be reflected in that function's name? Ideally, a naming convention like the one you're hinting at below, if done correctly, should suffice without the lemma_ prefix, e.g. append_sums_lengths is clearly a proof of a property, even without the lemma_ prefix.

[nikswamy]

Regarding 5:

Good idea. We should add the private qualifier there. It's not used enough currently.

[s-zanella]

I concur with @nikswamy regarding 1., I'd prefer to avoid the lemma_ prefix.

Add to 3. other various prefixes and suffixes I've seen:
lemma_foo' -> foo_<explains difference with lemma foo>;
foo_; _foo;foo_lemma;
lemma_helper (used in a lemma named bar) -> bar_aux (and make it private).

6. If we're adopting the naming conventions of Coq, I'd say that we name similar lemmas the same way as in Coq's standard library. For instance map_lemma -> map_length (not length_map). There's the question of whether we want to adopt other conflicting styles (e.g. SSReflect's or LEAN's). For instance, in SSReflect, the lemma that says that 0 is the right identity of addition on naturals is called addn0, in Coq is plus_n_O, and in LEAN is add_zero.

7. Compound names: camelCase vs snake_case. Which to use? Should we use a different style for differentiating constructions: e.g. use camelCase for values but snake_case for lemmas (much more compact than using a lemma_ prefix), or perhaps use camelCase for values and lemmas, but use snake_case for values in Type(n). I think we are almost consistently using CamelCase for module names.

[tahina-pro]

@s-zanella
6. I am not sure about what you mean by "naming conventions of Coq", as you mention, because they have both map_length for a property about (length (map _ _)), and map_cons for a property about (map _ (cons _ _)). I am not claiming that explicit naming conventions do or do not exist in the Coq standard library, but I am trying to infer possible guideline proposals for the F* standard library from (what I claim to be) meaningful examples in the Coq or OCaml standard libraries. However:

• to which extent we would like to maintain some compatibility is a good question of yours.
• regarding Ssreflect and MathComp, you are right, there are such explicit naming conventions in Section 11.2 of Gonthier et al., A Small Scale Reflection Extension for the Coq system, Research Report RR-6455, INRIA, https://hal.inria.fr/inria-00258384

While we are not necessarily going to follow all of Ssreflect's guidelines (although I just figured out that my proposal about naming length_map was actually already part of Ssreflect's guidelines somehow), I hope that we will be able to make our own naming conventions for the F* standard library explicit.

[s-zanella]

It was a bit of stretch to say that map_length follows any naming conventions. I meant that we could just pick the same names for lemmas in Coq's standard library. I picked map_length as an example of how arbitrary these names sometimes are.

If we had to chose a system to be compatible with, LEAN is probably our best choice given that at some point we would like to use it to certify our proofs.