Good "style"

Stream: new members

[Logan Murphy]

So I'm making a small group theory project from scratch (taking some pointers from mathlib when needed), and I have been wondering about what constitutes good style when it comes to writing definitions and lemmas. I often see people saying things in the chat like "this needs a better API" , which I assume means giving more definitions and lemmas so that proofs can be shorter.

Basically, my question is, how should I think about whether or not I'm building enough of an API? (This project is just for fun, I'm not planning on making any PRs based on it or anything)

Is there some sort of precept like "you should never need to do more than X rewrites" or "most of your proofs should be in term mode" that can guide me ?

[Logan Murphy]

And merry Christmas everyone :)

[Mario Carneiro]

there is no restriction on how hard the API theorems should be

[Mario Carneiro]

but they are usually one-liners

[Mario Carneiro]

the usual principle I use is to make sure that I have theorems that relate the new thing to all the old things

[Mario Carneiro]

generally it's only about adding more lemmas to work with the definitions, not adding more definitions (which are the reason for the lemmas)

[Logan Murphy]

Right. My approach to proving nontrivial theorems has basically been

1. Write a proof in tactic mode because it's easy
2. Refactor the tactic script into a series of have/obtain's that are basically just function applications
3. Figure out which of those might be useful to have their own lemmas

This usually lets me turn most 10-20 line tactic proofs into one or two lines, but I'd be interested in hearing what other people use as their guiding principles

[Mario Carneiro]

I don't know how useful this is, but I try to prove every obvious lemma about the new thing. I just keep going until I can't think of anything off hand

[Logan Murphy]

That makes sense

[Mario Carneiro]

That "proof compression" a useful skill of it's own, but you should be careful that the lemmas you extract from a theorem are suitably general

[Reid Barton]

I usually like to go in the reverse order--write the proof of a "real theorem" the way I want it to go but split out the steps as lemmas, and don't even prove the lemmas until I'm done with the main theorem

[Reid Barton]

of course you have to be 100% sure the lemmas are actually true then

[Reid Barton]

Sometimes you can even defer actually defining your definitions until after you see how they get used in practice.

[Julian Berman]

It's interesting that a couple of times I've seen it, it seems that folks do mean "good API" in a very programming-like sense -- i.e. layered theorems/definitions, encapsulation of some layers of abstraction such that you don't have to touch implementation details of layers below them, composability so that you can assemble new theorems by reusing theorems "one level down" in abstraction without either needing to reimplement chunks of them...

[Kevin Buzzard]

When I made a basic API for group theory in some sense the biggest design decision I felt I made was what the definition of a group should be. I went with just three axioms (associativity, left identity and left inverse) and then it's hard work proving right identity and right inverse, then the trick is to prove the Knuth-Bendix rewrite rules for groups and then check by doing various examples that simp solves the word problem for free groups.

[Kevin Buzzard]

@Logan Murphy I will be covering this material in lecture two of my course next term -- and subgroups too