eq.rec docs

Stream: general

[Reid Barton]

Anyone know why there are no docs generated for docs#eq.rec?

[Eric Wieser]

We don't generate docs for any "autogenerated" lemmas

[Reid Barton]

oh weird

[Reid Barton]

I guess there are a lot of them, but X.rec seems important no? I mean there are many occurrences of eq.rec in the statements of other lemmas

[Eric Wieser]

I guess the argument is that .rec is "obvious" from the inductive declaration

[Eric Wieser]

Maybe we should have a collapsed panel of "subdeclarations" inside inductive boxes which shows all the autogenerated definitions like rec, rec_on, cases, ...

[Floris van Doorn]

It would be nice if eq.rec redirects to eq in the same way as docs#eq.refl does. I don't think we need to change the entry of eq to include information about eq.rec though.

[Reid Barton]

Having something to link to for eq.rec is useful for explaining to users of other proof assistants (why this just came up now for me).

[Reid Barton]

Maybe we can have some mechanism whereby we manually indicate to the documentation generator that it should include documentation for indicated autogenerated definitions (e.g. eq.rec, eq.rec_on but not the recursors for every random inductive type)

[Eric Wieser]

Or maybe just for rec that actually appear in statement of other lemmas?

[Reid Barton]

That also sounds reasonable but I am not sure if the documentation generator has access to that information at an appropriate time

[Eric Wieser]

If the lean exporter just wrote out all definitions including autogenerated ones (rather than filtering them out), then the python script could filter them back out again, at the point when it has all the information

[Gabriel Ebner]

We could try to include the auto-generated declarations in the documentation, but collapse them by default. (Not sure how much space they take up. There's also various kinds of auto-generated declarations, equation lemmas, no_confusion, injectivity lemmas, sizeof, sunfold, expansion of general inductive types, ...).

[Yaël Dillies]

Equation lemmas are already included as part of the definition, and also they have the same name as the corresponding definition so I wouldn't include them.

[Eric Wieser]

and also they have the same name as the corresponding definition

That's not true, they are called foo.equations._eqn_1. rw and simp just know how to desugar foo into that name

[Alex J. Best]

We already handle these in doc_gen by putting an "Equations" section after the def, so the proposal is just to do the same with "Auxiliary declarations" too right

[Eric Wieser]

Yes, although the "auxiliary declarations" will likely need explicit arguments unlike the equations which mostly just reuse the arguments of the parent

[Eric Wieser]

I guess we'd add all of these?
https://github.com/leanprover-community/mathlib/blob/ca61dbffa497f43e2bdf6c4c6f446c112043ecd1/src/meta/expr.lean#L1086-L1088

[Gabriel Ebner]

I think it could be helpful to show them. I don't how many people know all the auto-generated definitions, nevermind how they are defined.

[Kyle Miller]

I like this idea to make the autogenerated definitions more documented. I remember it being frustrating while learning when I'd follow definitions and hit one of them. It was very unclear what they were or what they were for, and there's not much that helps direct you to the answer (save asking Zulip or thinking to check the right textbook).

Would it be a good idea to modify #print so that it directs you to how an automatically generated definition was created? I imagine #print eq.rec could at the least be like

protected eliminator eq.rec : Π {α : Sort u} {a : α} {motive : α → Sort l}, motive a → Π {ᾰ : α}, a = ᾰ → motive ᾰ

Generated for the inductive type eq.

and maybe even point you to where in the Lean source code it's generated.

[Kyle Miller]

(Relatedly, sometimes I feel like it would be nice to have provenance information for other automatically generated objects, like things created by to_additive. Could there be something like a "from" attribute that the docs could include and linkify?)

[Gabriel Ebner]

We already have "to" attributes, so it could be enough to just reverse that map.

[Junyan Xu]

There are also lemmas semi-auto-generated by @[simps], reassoc, elementwise etc. which can be lengthy. For example, I'd rather have this collapsed.

[Gabriel Ebner]

I think that also needs open category_theory topological_space opposite, which is another reasonable feature request.