Finding Theorems

Stream: new members

[Alex Zhang]

When I am writing a Lean project and if I want to use some lemma/theorem "L" to prove a new one, how do I know whether "L" has already existed in mathlib?

[Kevin Buzzard]

How can you use it if it doesn't exist? I'm a bit confused by this question.

[Alex Zhang]

"in mathlib" I mean, I edited the question. Sorry for any confusion.

[Kevin Buzzard]

Oh so "L" is a mathematical theorem, not a formalised one? You can search for it in the docs or ask in #Is there code for X?

[Kevin Buzzard]

If I'm hacking on mathlib then I often just use the search functionality of VS Code.

[Alex Zhang]

Yeah, I do mean a math theorem or a commonly used lemma (such as if x is real, then x^2>=0).

[Kevin Buzzard]

For something as simple as that, I would guess the name of the lemma.

[Kevin Buzzard]

import data.real.basic

#check pow_two_nonneg -- works

[Eric Rodriguez]

other options include library_search, suggest, using simp and seeing what lemmas it uses withsqueeze_simp

[Alex Zhang]

Many thanks! I am just taking that simple lemma as an example.

[Kevin Buzzard]

The naming conventions are here.

[Kevin Buzzard]

Alex Zhang said:

Many thanks! I am just taking that simple lemma as an example.

Different examples require different techniques -- your question is very broad.

[Alex Zhang]

Eric, could you please explain how to use squeeze_simp maybe with a #mwe?

[Kevin Buzzard]

This is the variant of your question where the theorem you want is actually your goal in a formalisation effort. You suspect the result is in the library, and then you discover that simp solves the goal, you can replace it with squeeze_simp and see what actually happened.

[Anne Baanen]

For example:

example : 4 * 0 = 0 := by squeeze_simp
-- Try this: simp only [mul_zero]

example : 4 * 0 = 0 := mul_zero _