Verbose Lean

Stream: Lean for teaching

[Patrick Massot]

After a lot of demands, I finally took a day to translate my verbose Lean teaching tactics into (very fake) English. I'm sorry some people have been waiting for this for nearly one year. The result can be found at https://github.com/PatrickMassot/lean-verbose. I didn't spend time figuring out the best translation, for lack of time and English language fluency. I'm sure people will soon suggest nice improvements. Please keep in mind this is a hack that will probably be very easy to improve in Lean 4 (see the README for information about the price to pay for abusing the Lean 3 parser). And I guess even the Lean 4 won't be able to compete with actual controlled natural language dedicated parsers, but @Sebastian Ullrich should feel very free to prove me wrong.

[Patrick Massot]

For the impatient people: you can have a look at sample.lean but beware that GitHub syntax highlighting is completely wrong and misleading here.

[Patrick Massot]

Unfortunately I currently don't have a solution better than using a custom version of the VSCode syntax highlighting if you want proper highlighting as in my essay.

[Patrick Massot]

Maybe I should warn Sebastian to get a glass of Whisky ready before opening https://github.com/PatrickMassot/lean-verbose/blob/master/src/parsers.lean, just in case.

[Sebastian Ullrich]

Looks perfectly reasonable to me

[Sebastian Ullrich]

But maybe that's the whiskey talking

[Patrick Massot]

Is there any hope to avoid the long list of new tokens from the beginning of that file in Lean 4?

[Sebastian Ullrich]

Any tokens used in parsers are registered automatically in Lean 4

[Patrick Massot]

I have completed a first Lean 4 version of my Lean verbose library. You can find it at https://github.com/PatrickMassot/verbose-lean4. This time the French and English versions are hosted in the same repository and share their backend so hopefully the English version will stay up to date. But I haven't yet ported the help tactic that was only in the French Lean 3 version. The Lean 4 version is far from being thoroughly tested but interested people can already play with it. The examples file from starts with:

import Verbose.English.ExampleLib

Exercise "Continuity implies sequential continuity"
  Given: (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
  Assume: (hu : u converges to x₀) (hf : f is continuous at x₀)
  Conclusion: (f ∘ u) converges to f x₀
Proof:
  Let's prove that ∀ ε > 0, ∃ N, ∀ n ≥ N, |f (u n) - f x₀| ≤ ε
  Fix ε > 0
  By hf applied to ε using ε_pos we get δ such that
    (δ_pos : δ > 0) (Hf : ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε)
  By hu applied to δ using δ_pos we get N such that Hu : ∀ n ≥ N, |u n - x₀| ≤ δ
  Let's prove that N works : ∀ n ≥ N, |f (u n) - f x₀| ≤ ε
  Fix n ≥ N
  By Hf applied to u n it suffices to prove |u n - x₀| ≤ δ
  We conclude by Hu applied to n using n_ge
QED

For people not familiar with Lean verbose, let me emphasize the above snippet is actual game content, not a cinematic. And it is properly highlighted in VSCode (unless you switch off semantic highlighting).

[Patrick Massot]

An important consequence of the new code layout is that adding support for more languages would be very easy, with essentially no meta-programming knowledge required.

[David Thrane Christiansen]

This is really fun!

[Floris van Doorn]

Very nice! It looks really good.

The phrases We discuss using h / We discuss depending on P sound very weird to me.
I would suggest We do case analysis using h or We do cases on h.

[Patrick Massot]

Every suggestion about English phrasing is very welcome. There are lots of things that sound much better in French but I don't know how to improve in English. My plan was to ask local people in Pittsburgh who teach math but know no Lean. In particular I'm afraid that "We do cases on h" is Lean-inspired. Would normal people say that?

[Patrick Massot]

Another remark about this library: it can be useful even if you don't focus on teaching proofs on paper. Tactics can be used with a different syntax. Some are simply wrappers around standard tactics. But others do actual extra work. For instance By foo we get bar baz will first try rcases foo with ⟨bar, baz⟩ but if that fail then it tries to apply lemmas tagged with anonymous_split_lemma. This how you can see things like

  By hN applied to n using (n_ge : n ≥ N) we get hN' : |u n - l| ≤ l / 2
  By hN' we get (h₁ : -(l/2) ≤ u n - l) (h₂ : u n - l ≤ l / 2)

[Patrick Massot]

Which of course can also be written as

By hN applied to n using (n_ge : n ≥ N) we get (h₁ : -(l/2) ≤ u n - l) (h₂ : u n - l ≤ l / 2)

[Johan Commelin]

My non-native ears like We do case analysis using h.

[Adam Topaz]

How bout "Let's do a case analysis on h"?

[Johan Commelin]

"Let's do a case distinction on P", when P is a Prop. But when h has type P \or Q, would you write "case analysis on h", or "using h"?

[Adam Topaz]

I would say "on".

[Adam Topaz]

But either one works, I guess...

[Kyle Miller]

"We proceed by cases" is common wording, but usually you figure out what the cases are by reading the cases. In a wordy text, I could imagine "We proceed by cases on whether P is true or Q is true", so that supports "on"

[Adam Topaz]

"Let's split h into cases."

[Adam Topaz]

Anyway there are of course hundreds of permutations that could sound valid, but I guess Patrick has to make a choice at the end of the day.

[Kyle Miller]

And let's not split on those cases here :smile:

[Patrick Massot]

I'm sure I understand what is the conclusion here. Indeed a big part of the issue is to distinguish rcases h with h1|h2 from by_cases h : P (which is of course the abbreviation of rcases Classical.em P with h|h. One could argue that real math doesn't see any distinction and we should use the same tactic, but somehow my Lean-induced distorsion fights back.

[Scott Morrison]

"We case bash on h"

[Andrés Goens]

Adam Topaz said:

Anyway there are of course hundreds of permutations that could sound valid, but I guess Patrick has to make a choice at the end of the day.

or does he? He could just have multiple valid syntax rules that all delaborate to the same thing, ight? Or is having a very rigid syntax an explicit design goal of verbose Lean?

[Arthur Paulino]

Also, new syntaxes are additive in Lean, so people can add variants of their liking

Btw, this looks awesome

[Patrick Massot]

Adding variants of syntax is very easy. There are already a couple of variations allowed. The danger with adding many more variations is that users could start thinking this is completely free form and get very frustrated when things don't work. Having lots of close variations doing different things also complicates having good error messages. Anyway, Lean Verbose is a library, you can use it as you like, you don't need me to add syntax. That being said, the current version is still pretty far from having everything that I plan. There should be a first feature-full version before Christmas.

[Johan Commelin]

I think this is one of the problems with Naproche that new users struggle with a lot: tiny variations mean different things. Filler words that we usually regard as synonymous in mathematical english have slightly different meanings withing the formal language, and if you don't realize this, you're lost.

[Marc Masdeu]

After years of learning lean I had become quite content with the looks of it, but yesterday I demoed a Catalan port of this to a new-to-Lean audience and they were very amazed at how much nicer it looks. I confirm also that one needs very little knowledge of metaprogramming to add a new language. @Patrick Massot are you interested in PRs?

[Kevin Buzzard]

My impression with general audience talks is that the audience love it if they see something new; some of your audience may have seen Lean code or a video of a Lean talk or whatever, but then you show them lean being used in a different "mode" that wasn't in the video, and this is exciting.

[Patrick Massot]

Yes, I'm interested in PRs adding new languages, as long as you promise to try to maintain the new language. I plan to work more on this project before Christmas so there will be some instability in the beginning, but then it should be more stable.