lemma := theorem?

Stream: lean4

[Kevin Buzzard]

Can I have lemma back? Is it an easy task to write a macro which defines a keyword lemma to mean theorem?

[Yakov Pechersky]

Daniel Selsam said:

Yakov Pechersky FYI declVal is exposed now on master so

macro "lemma" n:declId sig:declSig val:declVal : command => `(theorem $n $sig $val)

should work.

[Kevin Buzzard]

@[simp] lemma doesn't work :-( The error is

expected 'abbrev', 'axiom', 'class', 'constant', 'def', 'example', 'inductive', 'instance', 'structure' or 'theorem'

[Sebastian Ullrich]

macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
@[simp] lemma foo : True = True := rfl

[Kevin Buzzard]

Thanks Sebastian! Right now all this macro stuff looks like complete gobble-de-gook to me -- I look forward to the day when it all starts making sense.

[Kevin Buzzard]

I can't really understand how people can just appear from nowhere on this stream (I'm not talking about you, I'm talking about others) writing macro stuff when there's no documentation

[Daniel Fabian]

@Kevin Buzzard There's really an elegance and simplicity to the code base of lean4 that makes is quite possible to understand. But it is complex too, so it takes time to build up the intuition.

[Daniel Selsam]

@Kevin Buzzard I'll share a quick explanation of this one in case it helps. The parser for theorem is defined as:

def «theorem» := parser! "theorem " >> declId >> declSig >> declVal

and so it is tempting to define lemma similarly, i.e. as a macro that takes the same arguments as theorem and just replaces the name "lemma" with "theorem":

macro "lemma" n:declId sig:declSig val:declVal : command => `(theorem $n $sig $val)

However, the theorem parser is not actually considered at the top-level when parsing commands. Instead, it gets called by the declaration parser:

@[builtinCommandParser] def declaration := leading_parser
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)

The declModifiers false part is what allows for first parsing e.g. @[simp]. As you can see, the list of declaration commands «abbrev», «def», ... is hardcoded in the declaration parser (presumably for performance reasons) and so it cannot easily be extended. Also, as the error message you saw indicates, the lemma macro is not expanded when the macro does not match the full command. Aside: I am not sure what the rules are in general for when macros are expanded besides at the top-level.

So, Sebastian's solution is to basically mimic the "upwards closure" of the theorem parser, i.e. the path from the theorem parser to the actual top-level command parser, declaration, that calls it. Then whenever the theorem parser would have worked, the same command but with lemma will trigger the macro, and the result will trigger the original declaration parser.

[Kevin Buzzard]

Thank you!

[Kevin Buzzard]

I feel like there is a really nice "introduction to parsers" which could be written using Lean 4, explaining what a parser actually is and using Lean 4 to demonstrate them.

[Marc Huisinga]

Kevin Buzzard said:

I can't really understand how people can just appear from nowhere on this stream (I'm not talking about you, I'm talking about others) writing macro stuff when there's no documentation

The Lean 4 code itself has some examples that you can imitate and then play around with to see how it works. That's at least what I did to write the lean4-cli configuration macro.

[Kevin Buzzard]

I think you're all vastly overestimating how much I know about what a parser even is, but thanks anyway :-) Just to give you some idea of where I'm coming from, although I often read the non-meta mathlib source code (i.e. the maths), it is extremely rare that I ever look at the core Lean 3 code base. I'm about as far from a computer scientist as it's possible to be in this game. I am already lost at "DSL" in that README. I am not looking for more hints! I'm just saying that what I need to get going is something far more basic.

[Andrew Ashworth]

Probably everybody in this chat thread has taken a compilers course, so it definitely can feel intimidating. I feel like that's where most people pick up this sort of thing. It took about six weeks in an upper undergraduate course and many hours of homework exercises until I really had a handle on basic scanning and parsing. My college's compilers course used Engineering a Compiler 2nd Ed; but textbooks cost money. I've read online that https://craftinginterpreters.com/ is quite good, you might try the chapters on scanning and parsing there. It's much more applications-focused - it'll skip a lot of theory that you might not be interested in.

[Scott Morrison]

I'll join the thread just so Kevin doesn't feel alone in not having taken a compilers course. :-) A large fraction of the mathlib contributors / user base is in the same boat (and hopefully only more so in the future). Eventually it would be great if we have a layer of documentation that caters to this group, too! (Of course, this can probably only be usefully written by people who haven't taken a compilers course.)

[Ryan Lahfa]

the Lean Tactic Game? :> <:

[Scott Morrison]

Even just tutorials like Rob's great metaprogramming tutorial for LFTCM2020. I think this was pitched at a level where mathematicians without prior PL experience, but who had used Lean a bit, could start to interact with Lean's metaprogramming facilities.

[Mario Carneiro]

I'm hoping for a reference manual version first, which can be re-packaged (by anyone) for a lay audience

[Ryan Lahfa]

Scott Morrison said:

Even just tutorials like Rob's great metaprogramming tutorial for LFTCM2020. I think this was pitched at a level where mathematicians without prior PL experience, but who had used Lean a bit, could start to interact with Lean's metaprogramming facilities.

For anyone who might be interested into it (I didn't know about it!), I think this is the series of video on this tutorial: https://www.youtube.com/playlist?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2

[Bryan Gin-ge Chen]

There is a link to Rob's videos on our community resources page here. Maybe that page isn't easy to find though.

[François G. Dorais]

This is a blast-from-the-past but I think the recent "Typed Macros" update broke this:

macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)

[Sebastian Ullrich]

Thanks, fixed https://github.com/leanprover/lean4/commit/c64ac02ffc5a1e496557a009e42f129306a0c031