Zulip Chat Archive

Stream: Lean for teaching

Topic: Verbose Lean

Patrick Massot (Dec 07 2021 at 21:20):

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 (Dec 07 2021 at 21:22):

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 (Dec 07 2021 at 21:23):

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 (Dec 07 2021 at 21:25):

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 (Dec 07 2021 at 21:40):

Looks perfectly reasonable to me

Sebastian Ullrich (Dec 07 2021 at 21:42):

But maybe that's the whiskey talking

Patrick Massot (Dec 07 2021 at 21:46):

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

Sebastian Ullrich (Dec 07 2021 at 21:51):

Any tokens used in parsers are registered automatically in Lean 4

Patrick Massot (Nov 20 2023 at 06:06):

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₀
  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

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 (Nov 20 2023 at 06:10):

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 (Nov 20 2023 at 11:27):

This is really fun!

Floris van Doorn (Nov 20 2023 at 11:27):

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 (Nov 20 2023 at 14:10):

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 (Nov 20 2023 at 14:14):

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 (Nov 20 2023 at 14:15):

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 (Nov 20 2023 at 16:28):

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

Adam Topaz (Nov 20 2023 at 17:23):

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

Johan Commelin (Nov 20 2023 at 17:32):

"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 (Nov 20 2023 at 17:38):

I would say "on".

Adam Topaz (Nov 20 2023 at 17:38):

But either one works, I guess...

Kyle Miller (Nov 20 2023 at 17:45):

"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 (Nov 20 2023 at 17:48):

"Let's split h into cases."

Adam Topaz (Nov 20 2023 at 17:49):

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 (Nov 20 2023 at 17:51):

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

Patrick Massot (Nov 20 2023 at 20:37):

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 (Nov 21 2023 at 00:17):

"We case bash on h"

Andrés Goens (Nov 23 2023 at 10:37):

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 (Nov 23 2023 at 11:33):

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

Btw, this looks awesome

Patrick Massot (Nov 23 2023 at 16:20):

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 (Nov 23 2023 at 16:25):

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 (Nov 29 2023 at 11:05):

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 (Nov 29 2023 at 12:20):

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 (Nov 29 2023 at 13:02):

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.

Last updated: Dec 20 2023 at 11:08 UTC