RFC: adding dot notations #8556

Stream: general

[Anne Baanen]

I was getting annoyed that working with definitions such as irreducible, prime and associated, I had to write quite verbose terms like dvd_symm_of_irreducible (irreducible_of_prime (prime_of_factor _ hp)) (irreducible_of_prime (prime_of_factor _ hq)) hdvd, where a lot of redundancy can be eliminated with dot notation: (prime_of_factor _ hp).irreducible.dvd_symm (prime_of_factor _ hq).irreducible hdvd. So I made PR #8556, which changes the spelling of many of the lemmas in algebra/associated.lean to make usage of dot notation easier.

Since this would affect a lot of files, I want to see what everyone thinks before fully putting my efforts behind the PR.

[Yaël Dillies]

Did you consider using alias to make aliases similar to eg lt_of_le_of_lt and has_le.le.trans_lt?

[Eric Wieser]

That would certainly be a way to reduce your workload, but I think in this case having the dot notations alone is fine if you're willing to purge all uses of the old spellings.

[Anne Baanen]

I did, but I feel like the new names are strictly better, since they are shorter (turning _ or _of_ into .) but otherwise the same.

[Anne Baanen]

(OK, dvd_iff_dvd_of_rel_right did become associated.dvd_iff_dvd_right which is slightly longer, but I believe the rel in the original name was a mistake.)

[Yaël Dillies]

Okay well then as a dot notation partisan I back up that change!

[Yaël Dillies]

But do not forget to make some of them protected :wink:

[Filippo A. E. Nuccio]

BTW: Is there a comprehensive guide to the use of dot notation? Given its ubiquity, isn't it something which would deserve to appear in the left column of https://leanprover-community.github.io/mathlib_docs/ ?

[Eric Wieser]

Or perhaps in #naming

[Yaël Dillies]

I totally agree. in general, there are many things I could see added to the website, like a glossary, a sortable list of files (similar to the contributors page)...

[Filippo A. E. Nuccio]

But isn't the dot notation somewhat deeper than just a naming convention? The fact that I can write P.irreducible to apply prime.irreducible to a prime P is not (well?) documented, right?

[Eric Wieser]

The things in the left column of mathlib_docs tend to be related to library design choices. What you're describing are language features, which probably belong in the parts of the lean reference manual that were never written.

[Yaël Dillies]

Ah I thought Filippo was more talking about what kind of things mathlib uses dot notation for.

[Eric Wieser]

Right, that's the viewpoint that suggests #naming is a good place to me

[Filippo A. E. Nuccio]

Well, indeed what I had in mind was more the "language feature" as Eric calls it, and if this has never been documented then my point is not very sound. If it is a matter of what should/should not have dot notation, I agree that #naming is the right place.

[Anne Baanen]

Eric Wieser said:

Right, that's the viewpoint that suggests #naming is a good place to me

I think we should indeed expand this section of #naming:

It is useful to use dot notation even for types which are not inductive types. For instance, we use:

    le.trans
    lt.trans_le
    le.trans_lt

[Yaël Dillies]

Eh! This is a lie. These lemmas have a prepended has_le or has_lt namespace.

[Anne Baanen]

Perhaps:

Introduce dot notation when it is practical to do so, namely when a parameter has a name as its head symbol. Following this convention, ∀ {x}, foo x → bar x ∨ baz x should be called foo.bar_or_baz rather than bar_or_baz_of_foo. Examples in mathlib:

has_le.le.trans -- in addition to `le_trans`
has_lt.lt.trans_le -- in addition to `lt_of_lt_of_le`
has_le.le.trans_lt -- in addition to `lt_of_le_of_lt`
prime.irreducible -- instead of `irreducible_of_prime`

[Yaël Dillies]

You can even talk about cases where the head symbol isn't the one that's dot notated. I'm still very unclear about when it works.

[Eric Wieser]

Right, if (x : foo y z) (which has foo as the head symbol) but foo y z unfolds to bar z y, then x.baz will still find bar.foo

[Yaël Dillies]

It seems to work so long as you totally apply the function (not leaving any →). If you partially apply it, sometimes it works, sometimes it doesn't.

[Eric Wieser]

Yaël Dillies, don't confuse head symbol with first argument

[Yaël Dillies]

Ah, uh, yeah that's probably the problem.

[Yaël Dillies]

Mind adding an explanation of that too? :grinning:

[Eric Wieser]

docs#tactic.whnf I think might does not mention what head symbols are, but is relevant nonetheless.

[Anne Baanen]

Thinking about it a bit more, it's not really the most accurate description that "a parameter has a name as its head". I want to definitely include things like associated x y, definitely excluding things like associated x y ∨ associated y z (sincee the head symbol is or, which is not descriptive enough), and potentially allowing associated x (2 * y) (where the head symbol does not fully describe the situation, but is recognizable enough).

[Eric Wieser]

"a parameter has a name as its head" is a reasonably accurate description of when dot notation works, but perhaps not of when it is a good choice

[Yakov Pechersky]

I understand dot notation as just accessing into the term's namespace. So if you have something called my_term.my_lemma and a term h : my_term, then h.my_lemma will work. This is why l : list R and then l.foldr works, even though list.foldr (f : α → β → β) (b : β) : list α → β.

[Anne Baanen]

Indeed! So coming at it from a namespace-based viewpoint sounds like it would be clearer:

Prefer namespacing over longer un-namespaced names, when we can use dot notation. Following this convention, ∀ {x}, foo x → bar x ∨ baz x should be called foo.bar_or_baz rather than bar_or_baz_of_foo. Examples in mathlib:

[Mario Carneiro]

s/so that/when/