autogenerating `*_hom` and `sub*`

Stream: general

[Yury G. Kudryashov]

I think it would be nice to have some basic theory about *_hom (id, comp, comp_id, id_comp, comp_assoc, cancellation properties, maybe prod and/or pi) and substructures (complete_lattice, sub*.val, subtype_mk or cod_restrict, of_le, restrict) autogenerated, because this way we can guarantee that we use same API. Unfortunately, we can't use category_theory for *_hom lemmas because we want comp to be defined for Types in different universes. In a one-universe world, I'd say "define a concrete category ASAP, then use category theory notation and theorems".

I see three main options:

1. Leave it as is, and try to sync API manually.
2. Use Lean metaprogramming.
3. Use external templates (e.g., python+jinja2).

Pros and cons as I see them:

1. pros: easy to read and write code; cons: hard to sync;
2. pros: can use a lot of information; cons: hard to write; defs, statements & proofs are not readable without knowledge of metaprogramming;
3. pros: easy to write templates; generated code is readable by a user who doesn't know template language or lean metaprogramming;
   cons: extra dependency, can't use internal information about a structure.

[Kevin Buzzard]

4. abolish polymorphism because it's not necessary in classical mathematics

[Yury G. Kudryashov]

Last time I asked @Mario Carneiro explained that in some cases he really wants to have universe polymorphism.

[Yury G. Kudryashov]

But category theory doesn't give us automation for prod/pi/sub* anyway.

[Yury G. Kudryashov]

So without some kind of code generation we'll have to deal with the fact that, e.g., submodules use different names than subgroups, some facts are here for subalgebras but not for submonoids, and adding subsemirings is a lot of work.

[Chris Hughes]

This has something to do with varieties. https://en.m.wikipedia.org/wiki/Variety_(universal_algebra) I think this stuff can probably be pushed a long way, to give colimits and limits and adjoints of the canonical functors between these categories. I'd love to see how far this could be pushed. That's quite a big project though.

[Yury G. Kudryashov]

I'm not sure that we can use varieties to actually generate definitions and lemmas.

[Yury G. Kudryashov]

I mean, if we want to have nice structures, then we'll need some tactic to transfer statements anyway.

[Chris Hughes]

Yes. You might be able to prove things in a great generality, and write automation to generate the special cases. Not sure if that's a good way of doing it, particularly if you're just going for homs and subobjects.

[Yury G. Kudryashov]

I'd go with "generate using Python" because it gives readable definitions and proofs but this adds an extra dependency.

[Patrick Massot]

Wouldn't the generated stuff be autonomous after generation?

[Yury G. Kudryashov]

It would, so we can git add it.

[Yury G. Kudryashov]

And CI can easily check that generated code agrees with the actual lean file.

[Patrick Massot]

I don't understand why you need to CI anything here.

[Patrick Massot]

Isn't the goal to write Lean file, and then be happy with them?

[Yury G. Kudryashov]

I want to have synced theories for different algebraic structures. If someone wants to modify it, the proper way is to adjust the template, then regenerate. Or add a lemma/def outside of the "generated" section/file.

[Patrick Massot]

I see.

[Patrick Massot]

But it still wouldn't make it harder to use mathlib without a sane python installation.

[Yury G. Kudryashov]

If we git add generated files, then using mathlib and contributing to any other file will not be harder.

[Scott Morrison]

I'm pretty wary about templating Lean files using python. My experience of previous projects that generated source code from a program written in another language was that the generated files quickly degenerated into non-human-usable disasters.

[Scott Morrison]

I'd prefer to explore using Lean meta-programming more.

[Yury G. Kudryashov]

Then we'll have a hard to read file right away.

[Yury G. Kudryashov]

I can't be sure about others but for me it's hard to read Lean meta-programs.

[Yury G. Kudryashov]

@Scott Morrison What do you think about the following? I'll try to write some jinja template. If it will lead to an unreadable file, we trash it.

[Scott Morrison]

Obviously I can't say no to trying. :-) But I just feel we should eat our own dog food here!

[Scott Morrison]

If the meta programming is too hard / too unreadable, we should do a better job.

[Scott Morrison]

This question right here is meant to be _what Lean is for_.

[Scott Morrison]

A theorem prover with usable metaprogramming.

[Scott Morrison]

It feels like once we add outside templating we've admitted defeat. :-)

[Scott Morrison]

Admittedly, I am very sympathetic to the problem at hand.

[Scott Morrison]

I have been meaning to automate the construction of colimits / free objects for a long time, but the metaprogramming intimidates me!

[Scott Morrison]

We are hitting a bottleneck here.

[Scott Morrison]

Availability of metaprogramming resources has been outstripped by availability of mathematical resources...

[Scott Morrison]

(I can see Leo is on zulip right now, I feel embarrassed saying "what Lean is for", even if I know he doesn't read the main channels. :-)

[Yury G. Kudryashov]

You've convinced me to try lean metaprogramming. Be prepared to answer lots of stupid questions.

[Yury G. Kudryashov]

OK, first stupid question: is it possible to autogenerate, e.g., has_coe_to_fun for a monoid_hom without loosing readability?

[Yury G. Kudryashov]

With jinja templates the template will be slightly less readable but it'll generate exactly the same code as the one we have in algebra/group/hom.lean.