Zulip Chat Archive

Stream: new members

Topic: How to get familiar enough with Mathlib to use it


view this post on Zulip Keefer Rowan (May 25 2020 at 13:13):

I have been learning Lean for a few weeks now; I started with the natural numbers game, then Theorem Proving in Lean, and have since written around 3000 lines of Lean formalizing basic topological facts and the necessary set theory/function theory/logic for them. But I really failed to use libraries for this (failing even to use Lean's core library); if I needed a basic logic fact for a rw, I just proved it. Similarly for sets, functions, etc. After spending about 1000 lines giving a definition of finite (bijection with {0,1,...,n}) and showing the subsets of finite sets are finite and union of finite is finite, I thought I might want to start using facts from libraries and going about more doing "proper math". So I saw that no one has formalized basic facts about Hilbert spaces, and I thought I try my hand at that. But then I realized I'd need a working knowledge of (parts of) the libraries on real and complex numbers, metric space topology, linear algebra, normed spaces, etc. This seems totally impossible to get, so I would appreciate any advice on how to start familiarizing myself with the libraries enough to start building on them.

view this post on Zulip Patrick Massot (May 25 2020 at 13:15):

We currently don't have a better answering than reading the #docs . There are projects to improve on this, but time is scarce.

view this post on Zulip Patrick Massot (May 25 2020 at 13:16):

But see also https://leanprover-community.github.io/mathlib-overview.html

view this post on Zulip Kevin Buzzard (May 25 2020 at 13:21):

I'm pretty sure that when I started formalising undergraduate level mathematics I had no working knowledge of the libraries, and proved a bunch of things myself. The point which I had not understood back then, and do understand now, is the "library philosophy". Is this obscure result in the library? No. Can its proof be broken up into a small number of simple steps, each of which is natural? Yes. Are each of the simple steps in the library? Probably, and I can look for them by abstracting what I'm after and trying library_search, or just reading the library files and getting a feel for the kind of theorems which are proved.

I found finding my own proofs a lot of fun, even crappy proofs which were inefficient, because I would get a buzz and some confidence out of finding my own proof of something. But if you want to do Hilbert spaces then you should just start, and think clearly, and expect that standard natural results are already proved. I formalised basic 1st year undergrad stuff for 3000 lines like you, and then I started on schemes despite the fact that I was woefully underprepared in some sense, and I asked a lot of questions here, and we got there in the end. People will help you if you are asking questions about Hilbert spaces, there are plenty of people here that would love to see Hilbert spaces in mathlib and these people are going to be happy to help.

view this post on Zulip Patrick Massot (May 25 2020 at 13:24):

It still feels pretty pointless to start on Hilbert spaces without having a look at https://leanprover-community.github.io/mathlib_docs/linear_algebra/sesquilinear_form.html and https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/banach.html

view this post on Zulip Patrick Massot (May 25 2020 at 13:28):

And, as soon as definitions are there, also look at https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/complemented.html and https://leanprover-community.github.io/mathlib_docs/analysis/convex/basic.html (working towards projection lemmas)

view this post on Zulip Kevin Buzzard (May 25 2020 at 13:32):

But then I realized I'd need a working knowledge of (parts of) the libraries on real and complex numbers, metric space topology, linear algebra, normed spaces, etc. This seems totally impossible to get

This isn't totally impossible to get at all. The library files are not scary. Skip the definitions because you know what they are supposed to say -- instead, read the docstrings. Skip the proofs because you can look them up in a book; they are not written to be human-readable anyway. Look at the theorem statements. Make sure you understand them -- they are what you will need. Learn the various ways of searching for them (e.g. the ctrl-space trick, learning naming conventions, library_search). Don't be scared by the library files. If you find one without a docstring and you really can't get your head around it, mention it here and someone might write one. Start where Patrick suggests. Mathlib is not scary -- people who think it's scary are just reading it wrong.

view this post on Zulip Keefer Rowan (May 25 2020 at 13:34):

I'll start working on it.

view this post on Zulip Johan Commelin (May 25 2020 at 16:54):

Kevin Buzzard said:

But then I realized I'd need a working knowledge of (parts of) the libraries on real and complex numbers, metric space topology, linear algebra, normed spaces, etc. This seems totally impossible to get

This isn't totally impossible to get at all. The library files are not scary. Skip the definitions because you know what they are supposed to say -- instead, read the docstrings. Skip the proofs because you can look them up in a book; they are not written to be human-readable anyway. Look at the theorem statements. Make sure you understand them -- they are what you will need. Learn the various ways of searching for them (e.g. the ctrl-space trick, learning naming conventions, library_search). Don't be scared by the library files. If you find one without a docstring and you really can't get your head around it, mention it here and someone might write one. Start where Patrick suggests. Mathlib is not scary -- people who think it's scary are just reading it wrong.

@Kevin Buzzard should this become a blogpost “How to learn the library”?

view this post on Zulip Kevin Buzzard (May 25 2020 at 16:54):

Perhaps when I've finished my marking :-) But I'll definitely consider it! I had no idea what was going on when I first tried to read the library.

view this post on Zulip Patrick Massot (May 25 2020 at 17:20):

I also hope that the new mathlib overview will be helpful when it will exist.

view this post on Zulip ROCKY KAMEN-RUBIO (May 26 2020 at 05:21):

“Suggest” and “library_search” have been very useful to me. Sometimes they work better if you open a new goal state for the specific theorem you want.

view this post on Zulip Filippo A. E. Nuccio (May 26 2020 at 10:54):

I had the same feeling yesterday, when had to prove (to complete Kevin's homework) that the norm of a complex number is non-negative. I realised that someone must have proved that the square of a real is always non-negative, but after much time spent around I ended up with a trick (and I copy-paste here in case someone is willing to give me an opinion on how poor it is..):
lemma norm_sq_nonneg (z : ℂ) : 0 ≤ norm_sq z := begin rw norm_sq, have h: ∀ a : ℝ, 0 ≤ a*a , intro, cases le_total 0 a with posa nega, apply mul_nonneg posa posa, apply mul_nonneg_of_nonpos_of_nonpos nega nega, apply add_nonneg, all_goals {apply h}, end

So I also believe that a tutorial on how to properly search and browse the library would be great!

Added: I have eventually realized that in his solutions, Kevin complains that CS told him that "reals were almost entirely developed" but that he quite disagrees...

view this post on Zulip Anne Baanen (May 26 2020 at 11:04):

For what it's worth, this lemma is included as mul_self_nonneg : ∀ a, a * a ≥ 0 in algebra/ordered_ring.lean, but library_search or suggest don't seem to find it...

view this post on Zulip Anne Baanen (May 26 2020 at 11:10):

As I suspected, it's fixed when we switch the in the type of mul_self_nonneg to . Let me make a PR...

view this post on Zulip Johan Commelin (May 26 2020 at 11:19):

You don't even have to PR core, and wait for a new version of Lean... [/self-indulgence]

view this post on Zulip Reid Barton (May 26 2020 at 11:27):

Hmm, I don't see why that would matter to library_search--isn't it perfectly happy to give correct but conceptually nonsensical proofs that rely on unfolding semireducible things?

view this post on Zulip Anne Baanen (May 26 2020 at 11:45):

I believe the problem arises because library_search only unfolds the goal, not all the lemmas in scope. So to solve a goal a * a ≥ 0, it unfolds it to 0 ≤ a * a and looks for lemmas that return something with . The head symbol for this lemma is which doesn't get unfolded further and we get a mismatch.

view this post on Zulip Patrick Massot (May 26 2020 at 11:46):

This is tricky, unfolding more stuff could make library_search slower

view this post on Zulip Anne Baanen (May 26 2020 at 11:49):

Ah, it's a bit more nuanced. It's because the function head_symbol, used to compute the head symbol of the goal, contains a special case to map > to < and to , while match_head_symbol, used to find the lemmas with this head symbol, doesn't perform this mapping

view this post on Zulip Reid Barton (May 26 2020 at 11:52):

Oh, I didn't realize it used any kind of symbol matching, I thought it just tried to apply everything

view this post on Zulip Scott Morrison (May 26 2020 at 12:16):

It's pretty lame: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/suggest.lean#L61

view this post on Zulip Anne Baanen (May 26 2020 at 12:19):

How about using one function normalize_synonym that we apply to the goal and to the lemmas? I believe it's sufficient to map > to <, to and not to false to preserve the current behaviour

view this post on Zulip Anne Baanen (May 26 2020 at 12:21):

meta def normalize_synonym : name  name
| `gt := `has_lt.lt
| `ge := `has_le.le
| `not := `false
| n   := n

/-- compute the head symbol of an expression, but normalise synonyms -/
-- We may want to tweak this further?
meta def head_symbol : expr  name
| (expr.pi _ _ _ t) := head_symbol t
| (expr.app f _) := head_symbol f
| (expr.const n _) := normalize_synonym n
| _ := `_

-- snip --

/-- Determine if, and in which way, a given expression matches the specified head symbol. -/
meta def match_head_symbol (hs : name) : expr  option head_symbol_match
| (expr.pi _ _ _ t) := match_head_symbol t
| `(%%a  %%b)      := if `iff = hs then some ex else
                       match (match_head_symbol a, match_head_symbol b) with
                       | (some ex, some ex) :=
                           some both
                       | (some ex, _) := some mpr
                       | (_, some ex) := some mp
                       | _ := none
                       end
| (expr.app f _)    := match_head_symbol f
| (expr.const n _)  := if hs = normalize_synonym n then some ex else none
| _ := if hs = `_ then some ex else none

view this post on Zulip Scott Morrison (May 26 2020 at 13:28):

@Anne Baanen, did you try this out (e.g. run the tests file)? I'm certainly game to change this.

view this post on Zulip Anne Baanen (May 26 2020 at 13:34):

I just finished testing it, and I'm happy enough with the results. I didn't notice any changes in running time, but I haven't checked whether there are any benchmarks. Apart from > versus <, the change also improves on ¬ versus false:

lemma lemma_with_false_in_head (a b : ) (h1 : a < b) (h2 : P a) : false := sorry

set_option trace.silence_library_search false
example (a b : ) (h1 : a < b) (h2 : P a) : false := by library_search
-- Try this: `exact lemma_with_false_in_head a b h1 h2`

example (a b : ) (h1 : a < b) : ¬ (P a) := by library_search
-- Try this: `exact lemma_with_false_in_head a b h1`

example (a b : ) (h1 : a < b) : ¬ (P a) := by library_search
-- Try this: `exact lemma_with_false_in_head a b h1`

example (a b : ) (h2 : P a) : ¬ (a < b) := by library_search
-- fails - do we want this to work too?

view this post on Zulip Anne Baanen (May 26 2020 at 13:52):

I've made a PR out of the changes: https://github.com/leanprover-community/mathlib/pull/2829


Last updated: May 10 2021 at 00:31 UTC