How to get familiar enough with Mathlib to use it

Stream: new members

[Keefer Rowan]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Patrick Massot]

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)

[Kevin Buzzard]

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.

[Keefer Rowan]

I'll start working on it.

[Johan Commelin]

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”?

[Kevin Buzzard]

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.

[Patrick Massot]

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

[ROCKY KAMEN-RUBIO]

“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.

[Filippo A. E. Nuccio]

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

[Anne Baanen]

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

[Anne Baanen]

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

[Johan Commelin]

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

[Reid Barton]

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?

[Anne Baanen]

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.

[Patrick Massot]

This is tricky, unfolding more stuff could make library_search slower

[Anne Baanen]

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

[Reid Barton]

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

[Scott Morrison]

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

[Anne Baanen]

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

[Anne Baanen]

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

[Scott Morrison]

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

[Anne Baanen]

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?

[Anne Baanen]

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