Tactic tutorial

Stream: lean4

[Jad Ghalayini]

I've recently been putting in some effort trying to learn how to write tactics in Lean 4, and realized that it would be extremely helpful to have a tutorial. I'd be happy to try my hand at writing one up and posting it, but was wondering what I could do to try to make it less likely to become obsolete; in particular, what features can I expect to be (mostly) stable? What should I include to make it as useful as possible?

[Henrik Böving]

There has been some discussion on a general meta programming tutorial in another recent thread here named "metaprogramming tutorial" so it definitely seems to be a popular subject, you can check that out if you want to look for some inspiration

[Arthur Paulino]

@Jad Ghalayini have you seen the current tactics writing tutorial for Lean 3?
https://leanprover-community.github.io/extras/tactic_writing.html

[Arthur Paulino]

I would not cover monadic programming nor do notation though. I think those would deserve a dedicated topic of their own in Lean 4. I would go straight to practical/minimal examples, building small blocks for more complex tactics

[Henrik Böving]

I'm btw still of the opinion that we might want to look into a general programming tutorial before before looking into the more complex topics like meta programming.

[Arthur Paulino]

I see a didactic order, but not necessarily an order of making because ppl's motivations can fade away

[František Silváši]

I think 'general programming' is something that most Lean 4 users are already quite apt at. OTOH Lean metaprogramming is fairly Lean-specific and I assume a 'tutorial' would benefit the current CS/programmer community more. That said, one could make the argument that Lean 4 is primarily used by mathematicians right now, but I have no idea about stats. In such case, introduction to 'functional programming' would likely be of more benefit, for you can't really do any of the Lean meta stuff without the basics first.

[James Gallicchio]

(Also worth noting that a general programming manual can be written by those of us who have no understanding of Lean meta-programming :joy:)

[Kevin Buzzard]

I think it's a sociological coincidence that lean 3 (not 4) is primarily used by mathematicians; I see far fewer mathematicians in the lean 4 stream (although of course they will come when the maths library is ported). I think that the lean 4 devs have a vision of lean 4 being adopted by a far wider community than the mathematics crowd.

[Xubai Wang]

Why not put them together first? Like what we do for Mathlib and Std. And they can be separated when the tutorial get too large.

[František Silváši]

Oh I thought this was a question of prioritization, as per Henrik's comment along the lines of 'let's do general before looking into more complex topics'. I simply wanted to point out that having a 'metaprogramming' tutorial without a general, more basic one, would not be useless at all.

[František Silváši]

And I managed to accidentally also drag the CS/math discussion into it, because I assumed that, e.g., Kevin's undergraduates, might not have experience in functional programming and for those, a metaprogramming thing without a general thing would indeed be useless.

[Xubai Wang]

František Silváši said:

a metaprogramming thing without a general thing would indeed be useless.

I agree with that.

[Xubai Wang]

But just as a suggestion, I think it's better to view tutorial as a community process: we do need an (evolving) to-do list for what to write, but not an exact plan of at what time for whom to write which. People can freely fork and contribute, without any predetermined prioritization, what they know and want to write.

[Xubai Wang]

I myself had tried writing one, but soon failed, both because I didn't know that to write then, and finding my actually not knowing a lot about what I want to write.

[Xubai Wang]

lean-samples may be a good place to start :wink:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/new.20lean4-samples.20repo
Although it's code sample based, we can use doc-gen and leanink to make it more like a tutorial

[Kevin Buzzard]

Many of my students are undergraduate mathematicians who have no need to learn either programming or metaprogramming; they spend their entire life within a begin/end block running tactics which other people have written. But (hence?) this is not about them. I think it's absolutely clear that there are people out there who don't know where to start and right now the answer they're given here is typically of the form "read the source code". I think that beginners with some programming background (eg undergraduates, who turned out to be important members of our community) be given a better place to start.

[Siddhartha Gadgil]

In many ways https://leanprover.github.io/theorem_proving_in_lean4/introduction.html is a very good starting point. Perhaps it will help the discussion if one thinks in what way it should be complemented.

In my personal experience, teaching courses with Agda and Idris (as Lean was not a programming language when I did this), this can be preceded by

• an introduction to functional programming in the weak sense, by which I mean
  - using recursion as the only form of looping, with no mutability.
  - higher-order functions, say for composition or dynamics, and the corresponding type theory (which is at the HOL level)
  - real-world is via #eval, so there is no need of Monads at this stage.
• refining this by clarifying total and partial function definitions.

After this one moves on to Dependent Type theory and Propositions as types, for which "Theorem Proving in Lean 4" is excellent.

[Alcides Fonseca]

I would be grateful for the tactic writing tutorial. I've managed with examples to write programs in Lean4. Tactics are another beast.

[Mac]

Siddhartha Gadgil said:

• an introduction to functional programming in the weak sense, by which I mean
  * using recursion as the only form of looping, with no mutability.

One thing that I think is significantly different about Lean from other functional programming languages is its superpowered do notation which allows one to write code in a manner very close to procedural/imperative languages lake Rust. As such, I think an easier on-ramp for non-functional programmers in Lean is to introduce them to purely imperative examples using IO and do so they can naturally transition their imperative programing skills to Lean. Only once they have gotten a handle on the API and syntax of Lean would I then suggest peeling back the sugar and teaching them the difficult pure functional concepts.

[Kevin Buzzard]

This is interesting because I teach mathematicians how to use lean purely within tactic mode for as long as possible, using mathlib's definitions of mathematical objects and asking them to fill in proofs, so they also don't really ever see any hint that it's a functional language (and indeed many of them have no idea what a functional language is)

[Kevin Buzzard]

I might add that the moment mathlib is ported to lean 4 I will be writing tutorials for mathematicians (emphasizing tactic mode)

[Pieter Cuijpers]

I've just started using Lean4, am getting comfortable writing tactic mode proofs, and looking for a tutorial to write my own tactics. So far, did not find much useful content. Either the lean3 examples are not working, or the videos are too high level.

Can anyone help me get started?

[Pieter Cuijpers]

First steps for me would be to program some recurring proof patterns as a tactic. Any examples to learn from perhaps?

[Henrik Böving]

There is https://github.com/arthurpaulino/lean4-metaprogramming-book/ Some of the API descriptions might be out of date but the general concepts remain the same

[Pieter Cuijpers]

Great! Let's see how far I get with that. Thnx