[doc] in_cons vs mem_head, explain in the wiki

[gares]

Hum, I guess one may expect to either have mem_cons and mem_head or in_cons and in_head or the four variants... Is there a rationale behind this naming?

[gares]

CC @benjgregoire

[CohenCyril]

Hi, the only reason I could think of is that the only two lemmas that start with "in_" instead of "mem_", namely in_nil and in_cons are actually conversion rules. The rest of them are not.

[amahboubi]

Lemmas with the prefix 'in_' are lemmas which state an equality between an infix syntax of the form
x \in foo with the corresponding applicative form. Proofs consist in unfolding the definition of membership and propagating the application gracefully if this membership predicate is itself defined as a conjunction, a disjunction,... For instance (in seq.v):
Lemma in_cons y s x : (x \in y :: s) = (x == y) || (x \in s).
or also (in finset.v):
Lemma in_set0 x : x \in set0 = false.
The user-defined inE rewrite rule typically gathers in_* lemmas, although not all in_* lemmas should land in inE.
By contrast, lemmas with the prefix 'mem_' have a hypothesis of the shape x \in foo, like (in finset.v):
Lemma mem_imset (D : pred aT) x : x \in D -> f x \in f @: D.
or (in seq.v):
Lemma mem_mask x m s : x \in mask m s -> x \in s.
Alternatively, they state equivalences between x \in foo and and another boolean statement, but not the latter structural one provided by the in_* lemma. Examples of such possibly non-trivial equivalences include (in prime.v):
Lemma mem_primes p n : (p \in primes n) = [&& prime p, n > 0 & p %| n].

Back to the initial question, as @CohenCyril pointed, mem_head is not strictly speaking not a structural in_* lemma. Although the proof is almost trivial, it still requires a small massage, to clean up the "or false" part featured by the bare expansion of the applicative form of the infix statement.

[amahboubi]

Now to be more user-friendly, I guess that we could decide to have 'mem_' aliases, at least when there is not a useful 'in_' form...

[amahboubi]

I sent my previous comment while still editing it sorry. I meant we could decide to have 'mem_aliases full stop.

[CohenCyril]

@ggonthier what do you think about this?

[ggonthier]

Well, in_head would be wrong, because the lemma is not about something being in the head of a sequence. It's the membership lemma for the head of a sequence, whence the name is appropriate.

[CohenCyril]

Sure, but what about all these lemmas which start with mem_ with left hand side x \in _ and could start with in_ instead...

[CohenCyril]

For example I understand mem_mask is expressing the hyphothesis is in the mask, but for mem_imset it's the conclusion...

[ggonthier]

mem_ is a non-committal prefix, since it can be read either as membership of or membership in. I 've used to as the default for all lemmas about membership, reserving the in_ prefix for components of inE or their special cases. The latter come in handy for the occasional right-to-left rewrite, or as explicit proof arguments (for in_setT). Note that using in_ more widely could create ambiguities with the infix _in_ used to signal variant of lemmas with a localised {in ..., ...} premise, such as eq_in_map, especially in seq where they are very common.

[CohenCyril]

OK, so what do you think about @amahboubi's suggestion to provide mem_ aliases for our users?

[ggonthier]

I suppose it's not unreasonable if there are user requests, but it does introduce some bloat, and undermines the reminder that one should consider using inE rather than in_ lemmas, unless there is a specific reason to do so (e.g., using in_setU to expand a union membership, when inE would expand some other \in in the goal).

[affeldt-aist]

What about putting in an FAQ page on the wiki the explanations by @amahboubi so that we can close this issue?

[pi8027]

@chdoc I suggest you to work on the draft of documentation in a wiki page good practices and integrate it to CONTRIBUTING.md later.

[CohenCyril]

Good practices has been integrated in CONTRIBUTING.md (the comment was outdate, this fixed now). So I suggest this documentation goes directly to CONTRIBUTING.md.