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.

[Patrick Massot]

Some news from Verbose Lean: I ported the help tactic from the French Lean 3 version, and created a widget prototype. Unfortunately those are two areas where separating syntax from actual code is a lot harder. After playing with a couple of ideas, I decided to go with massive code duplication for now. The code is still at https://github.com/PatrickMassot/verbose-lean4, although I may overwrite the Lean 3 repo at some point. Remember the context: this is a teaching library for people who want to teach pen and paper proof writing using Lean. It is not meant to replace ordinary usage of Lean. Using natural language as an input is slightly harder than normal Lean syntax. The widget is meant for people who have not enough teaching hours to teach syntax. Demo:
verbose_widget_test_en.gif

[Kim Morrison]

Very nice!

[Kim Morrison]

It will be great to have non-verbose versions of this! :-) More hints in the infoview, and more point and click construction of tactics!

[Patrick Massot]

All the infrastructure is already there!

[Patrick Massot]

There is not even a single line of javascript code in Verbose Lean. It is all built using @Wojciech Nawrocki's widget writing in Lean technology.

[Marc Masdeu]

I have been thinking about this option as well: after writing a Catalan translation of most of Patrick's code (I'm struggling to keep his pace!) I wanted to do a "Native" version, which incorporates some of the niceties (I would love to be able to do intro x ≥ y when the goal is ∀ x y, x ≥ y → P x y) and the help and point-and-click, but does not require so much typing and is closer to the actual Lean tactics. Maybe instead of Native it could be called TrainingWheels ?

[Patrick Massot]

About point and click, we know @Jovan Gerbscheid is doing something in this direction so we would at least need some coordination if we do something for Mathlib.

[Patrick Massot]

Your example of intro x ≥ y is actually not supported by Verbose Lean. It only does the case where the right-hand side is already there (and not necessarily a single variable, it could be Fix n ≥ max N N'). I could add support for intro x ≥ y introducing two variables, but I never needed it in more than a couple of exercise on increasing/decreasing functions.

[Sergey Cherkis]

Why is it that the fist example compiles fine while the second does not?

Example "example 1"
  Given: (P Q R S : Prop)
  Assume: (h:True)
  Conclusion: True ↔ True
Proof:
Let's first prove that True → True
sorry
Let's now prove that True → True
sorry
QED


Example "example 2"
  Given: (P Q R S : Prop)
  Assume: (h : True)
  Conclusion: ((P ∨ Q) → R) ↔ ((P → R) ∧ (Q → R))
Proof:
Let's first prove that ((P ∨ Q ⇒ R) → (P ⇒ R) ∧ (Q ⇒ R))
sorry
Let's now prove that ((P ⇒ R) ∧ (Q ⇒ R) → P ∨ Q ⇒ R)
sorry
QED

Also, is there a convention that allows to skip Assume:?

[Aaron Liu]

I would guess it is your use of ⇒

[Sergey Cherkis]

@Aaron Liu Do you mean Let's first prove that (P ∨ Q ⇒ R) ⇒ (P ⇒ R) ∧ (Q ⇒ R) ? Alas, that does not change the response. Still, Lean4 tells me "This is not what needs to be proven."

[Jovan Gerbscheid]

What about just using →?

[Aaron Liu]

I mean you should do something like

Example "example 2"
  Given: (P Q R S : Prop)
  Assume: (h : True)
  Conclusion: ((P ∨ Q) → R) ↔ ((P → R) ∧ (Q → R))
Proof:
Let's first prove that ((P ∨ Q → R) → (P → R) ∧ (Q → R))
sorry
Let's now prove that ((P → R) ∧ (Q → R) → P ∨ Q → R)
sorry
QED

[Kevin Buzzard]

The point is that in the first example you use → everywhere and it works, and in the second example you use ⇒ in lots of places and it doesn't work, so the conjecture is that you should be using → everywhere.

[Patrick Massot]

That has nothing to do with mixing notations (that Lean happily deals with). It has to do with missing parentheses and with logical connective precedence. So it has nothing to do with Verbose Lean.

[Patrick Massot]

Note that help will tell you the correct thing to do here.

[Sergey Cherkis]

First, these are the suggestions of Verbose:
Screenshot 2025-03-06 at 1.19.24 PM.png

Let's prove that (P ∨ Q ⇒ R) → (P ⇒ R) ∧ (Q ⇒ R)
Let's prove that (P ⇒ R) ∧ (Q ⇒ R) → P ∨ Q ⇒ R

which I tried augmenting to Let's first prove that and Let's now prove that

Second, changing to \r, following advice above (thank you @Aaron Liu and @Kevin Buzzard !) , appears to have fixed the problem.
Ex. 1 works fine, but Ex. 2 does not. Why?

Example "Ex. 1"
  Given: (P Q R S : Prop)
  Assume: (h : True)
  Conclusion: ((P ∨ Q) → R) ↔ ((P → R) ∧ (Q → R))
Proof:
Let's first prove that ((P ∨ Q) ⇒ R) ⇒ (P ⇒ R) ∧ (Q ⇒ R)
sorry
Let's now prove that (P → R) ∧ (Q → R) → P ∨ Q → R
sorry
QED

Example "Ex. 2"
  Given: (P Q R S : Prop)
  Assume: (h : True)
  Conclusion: ((P ∨ Q) → R) ↔ ((P → R) ∧ (Q → R))
Proof:
Let's first prove that (P ∨ Q → R) ⇒ (P ⇒ R) ∧ (Q → R)
sorry
Let's now prove that (P ⇒ R) ∧ (Q ⇒ R) ⇒ P ∨ Q ⇒ R
sorry
QED

[Sergey Cherkis]

Patrick Massot said:

Note that help will tell you the correct thing to do here.

Yes, though help gives valid suggestion, in this case, for some reason, Lean fails to accept the suggested step for me.

[Sergey Cherkis]

I think I see the light. \r and \=> appear to have different precedence!
(P → R) ∧ (Q → R) → P ∨ Q → R is NOT the same as
(P ⇒ R) ∧ (Q ⇒ R) ⇒ P ∨ Q ⇒ R.
But, rather, it is the same as
((P ⇒ R) ∧ (Q ⇒ R)) ⇒ (P ∨ Q) ⇒ R

[Patrick Massot]

Ok, so there are two completely different things. First there was indeed a typo in a help handler. This is now fixed. Then there is a completely incomprehensible delaboration issue. I will need to ask Kyle to take a look, but he is very busy right now.