4
$\begingroup$

In Lean we make definitions and formulate theorems about the things we have defined. Seemingly, to each definition there exists several simple theorems. Let's go to MeasureTheory/Function/SimpleFunc.lean because I think it's a decent example and because I've been mucking around here recently. In this file we define a structure SimpleFunc and then we start giving easy theorems about it: coe_injective, ext, finite_range, measurableSet_fiber, apply_mk, etc. When you write a file like this, how do you go about adding these small theorems? It would make sense that they're just added as we realize we need them, but also that experienced coders just carry a mental checklist with them generated by their goal in context. How should I think about this?

Note: This question may apply beyond the scope of "easy theorems", and any more-general commentary is certainly appreciated by me.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ This is a very good question that can apply to outside of Lean. Maybe a tag called "library-design"? $\endgroup$
    – Trebor ♦
    Commented Sep 25, 2023 at 1:46
  • 3
    $\begingroup$ Computer scientists are ahead of the game by several decades, they call it software engineering. $\endgroup$
    – Andrej Bauer
    Commented Sep 25, 2023 at 6:22

2 Answers 2

Reset to default
1
$\begingroup$

This is what we call an API for the new concept, and it is indeed the first thing we do after having written the definition. Of course we try to guess what will be needed to use our definition, but as you guessed in practice it is done in several steps. After some experience one becomes quite good in guessing a lot of small theorems, for example what happens for x = 0 (if there is an x...) and stuff like that.

I would say it mostly experience, but the real question you need to ask is: "how am I going to prove my non stupid result? What will I need?" and write all the basics you think will be needed.

For example, for SimpleFunc, I would prove that a constant function is simple, that the sum/product/difference... of simple functions is a simple function and so on.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Indeed, your example is the first thing a mathematician would do, which indicates two sides of the story. The first: How to build a rich mathematical theory/how, as a mathematician, to recognize the small things we take for granted (e.g., I haven't proved something is linear modulo "recognition" and mathematical "experience" for years). The second: Language knowledge/knowledge of language-specific new concept APIs. Do you approach a new concept API mathematically, i.e., digging in a book to realize your object as other objects, e.g., a simple function as a function, or with codebase knowledge? $\endgroup$
    – Alex Byard
    Commented Sep 26, 2023 at 18:54
  • $\begingroup$ Perhaps the mental divide is between keeping track of things we recognize but don't necessarily prove mathematically (i.e., xyz function is linear) by way of "experience" and keeping track of things we know but never think about (i.e., that a "simple function" is a "function" is contained in the language we use to describe "simple function"). $\endgroup$
    – Alex Byard
    Commented Sep 26, 2023 at 18:59
1
$\begingroup$

A general strategy I have is to consider how my new notion will be interacting with the ones I already have lying around. And then for each such interaction that generates a theorem that is 1) interesting 2) not too hard to prove, I go and prove it. Here, for instance, you already have the notions of constant functions around, and there an interesting theorem that constant functions are simple, so you can go and prove that.

You'll likely miss some such simple theorems, but as you go on and try to prove more interesting theorems about your new notions, they will generate interactions you missed, and new easy theorem, so you can come back and add these. Linked with this is a second important pragma: you should in most cases put lemmas in the earliest place where they can be stated and proven. In other words, if in a complicated proof you need a very elementary lemma that seems to be missing, you should add this lemma not where you need it, but much earlier. That way, you or others can more easily discover and re-use it, because it is not lost in a file which does not really have to do with it.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Along the lines of your second important pragma: Why do we put definitions before their self-titled namespaces? Is it that opening a namespace comes along with a bunch of variables and stuff inside that we don't necessarily want mingling with other things? $\endgroup$
    – Alex Byard
    Commented Sep 26, 2023 at 19:04
  • $\begingroup$ This is a more mathlib-specific choice, so I'm not sure what to say here. If I had to guess, I would say this is because having say SimpleFunc.SimpleFunc or something like this is silly, you want the simpler SimpleFunc. Note, though, that other conventions for namespaces/modules exist. For instance, a standard in the OCaml world is to locally call the main definition of a module t, so that once qualified you get SimpleFunc.t. But I guess this is less beginner-friendly, especially for people coming from non-CS background. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Sep 27, 2023 at 8:31
  • 1
    $\begingroup$ I think I actually like this standard. This way importing a file brings you all the main structures and typeclasses you want. You can use them however you want, but if you want to work with their theorems you either have to consider their scope and open the namespace or call them using SimpleFunc.Theorem, which clearly shows that it's a theorem pertaining to SimpleFunc. Not bad. $\endgroup$
    – Alex Byard
    Commented Sep 27, 2023 at 15:57

Not the answer you're looking for? Browse other questions tagged or ask your own question.