Zulip Chat Archive

Stream: general

Topic: autogenerating `*_hom` and `sub*`


Yury G. Kudryashov (Apr 07 2020 at 19:28):

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 (Apr 07 2020 at 19:37):

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

Yury G. Kudryashov (Apr 07 2020 at 19:38):

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

Yury G. Kudryashov (Apr 07 2020 at 19:39):

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

Yury G. Kudryashov (Apr 07 2020 at 19:43):

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 (Apr 07 2020 at 19:43):

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 (Apr 07 2020 at 19:44):

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

Yury G. Kudryashov (Apr 07 2020 at 19:46):

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

Chris Hughes (Apr 07 2020 at 19:48):

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 (Apr 07 2020 at 19:51):

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

Patrick Massot (Apr 07 2020 at 19:52):

Wouldn't the generated stuff be autonomous after generation?

Yury G. Kudryashov (Apr 07 2020 at 19:53):

It would, so we can git add it.

Yury G. Kudryashov (Apr 07 2020 at 19:55):

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

Patrick Massot (Apr 07 2020 at 19:57):

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

Patrick Massot (Apr 07 2020 at 19:57):

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

Yury G. Kudryashov (Apr 07 2020 at 20:03):

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 (Apr 07 2020 at 20:04):

I see.

Patrick Massot (Apr 07 2020 at 20:04):

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

Yury G. Kudryashov (Apr 07 2020 at 20:05):

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

Scott Morrison (Apr 07 2020 at 23:20):

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 (Apr 07 2020 at 23:21):

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

Yury G. Kudryashov (Apr 07 2020 at 23:24):

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

Yury G. Kudryashov (Apr 07 2020 at 23:31):

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

Yury G. Kudryashov (Apr 08 2020 at 00:52):

@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 (Apr 08 2020 at 00:54):

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

Scott Morrison (Apr 08 2020 at 00:54):

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

Scott Morrison (Apr 08 2020 at 00:55):

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

Scott Morrison (Apr 08 2020 at 00:55):

A theorem prover with usable metaprogramming.

Scott Morrison (Apr 08 2020 at 00:55):

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

Scott Morrison (Apr 08 2020 at 00:56):

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

Scott Morrison (Apr 08 2020 at 00:56):

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

Scott Morrison (Apr 08 2020 at 00:59):

We are hitting a bottleneck here.

Scott Morrison (Apr 08 2020 at 00:59):

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

Scott Morrison (Apr 08 2020 at 01:00):

(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 (Apr 08 2020 at 01:49):

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

Yury G. Kudryashov (Apr 21 2020 at 23:36):

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 (Apr 21 2020 at 23:52):

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.


Last updated: Dec 20 2023 at 11:08 UTC