Pi

Stream: Is there code for X?

[Kevin Lacker]

Is pi defined somewhere, like good old' 3.14 etc pi

[Adam Topaz]

docs#real.pi

[Johan Commelin]

git grep "3.14"
src/analysis/special_functions/trigonometric.lean:/-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from
src/data/real/pi.lean:lemma pi_gt_314 : 3.14 < pi := by pi_lower_bound [99/70, 874/473, 1940/989, 1447/727]
src/data/real/pi.lean:lemma pi_gt_31415 : 3.1415 < pi := by pi_lower_bound [
src/data/real/pi.lean:lemma pi_lt_31416 : pi < 3.1416 := by pi_upper_bound [
src/data/real/pi.lean:  411278/205887, 438142/219137, 451504/225769, 265603/132804, 849938/424971]
src/data/real/pi.lean:lemma pi_gt_3141592 : 3.141592 < pi := by pi_lower_bound [
src/data/real/pi.lean:lemma pi_lt_3141593 : pi < 3.141593 := by pi_upper_bound [

[Johan Commelin]

@Kevin Lacker Do you know git grep?

[Kevin Lacker]

yeah, i grepped for pi but a bazillion other things came up

[Adam Topaz]

yeah, that's stuff related to pi types, I guess.

[Johan Commelin]

Aah, you should have grepped for good old' 3.14 etc

[Kevin Lacker]

i looked through the file that defined cosine too, hoping that it would be in there, or some trig equalities would be

[Kevin Lacker]

yeah i didn't realize that would be a lemma

[Kevin Lacker]

it sure is though

[Kevin Lacker]

and for the record, when I use docs search for "pi", "real.pi" isn't one of the top 20 results

[Kevin Lacker]

so i tried!

[Adam Topaz]

TBH, I only knew that the 3.14 pi existed because @Johan Commelin had a post about two_pi_I a few days ago ;)

[Heather Macbeth]

Which trig equalities are you after? Another good file is analysis/special_functions/trigonometric. docs#complex.cos_pi_div_two

[Kenny Lau]

Maybe we should add "Archimedes' constant" somewhere in the docstrings

[Johan Commelin]

Never heard of that before (-;

[Kenny Lau]

and maybe something about circumference over diameter

[Kevin Lacker]

ideally i would like some tactic that auto solves a formula like (cos x)^2 = 1/2

[Kevin Lacker]

i even grepped for "area", figuring the formula for the area of a circle should tell me what pi is. but there is no use of the word "area" in any lean file

[Heather Macbeth]

Right. We're waiting for Riemannian manifolds :)

[Heather Macbeth]

Kevin Lacker said:

ideally i would like some tactic that auto solves a formula like (cos x)^2 = 1/2

This depends what you want. Do you want it for a small set of nice trig values only? If so, docs#real.cos_pi_div_four for this one, and there are plenty more special values (and you can PR more!). Do you want it for a general RHS? We have docs#real.arccos if so.

[Johan Commelin]

No, I think Kevin wants to throw an equation at lean the way you can throw equations at wolframalpha

[Johan Commelin]

But we don't have anything that gets close to that.

[Heather Macbeth]

How does wolframalpha work? (Of course it's closed source, so one has to guess.) It is so helpful and friendly (especially the paid version), maybe interacting with Lean can be like that someday!

[Johan Commelin]

yes, let's hope that it will!

[Kevin Lacker]

well, in this case I literally want to solve (cos x)^2 = 1/2

[Kevin Lacker]

it should be (odd number) pi / 4 i think

[Heather Macbeth]

It'll be slightly messy, but use docs#real.cos_pi_div_four, the periodicity and reflective symmetry of cos, and its injectivity on certain intervals.

[Kevin Lacker]

i'm sure there's some sort of formula that reduces this... yea i'll look around

[Heather Macbeth]

docs#real.cos_inj_of_nonneg_of_le_pi

[Heather Macbeth]

docs#real.cos_add_pi

[Heather Macbeth]

And a possible model, the classification of solutions to cos x = 1: docs#real.cos_eq_one_iff

[Kevin Lacker]

how about the formula for cos (x + y) - is that somewhere? i'm looking, and i feel silly for not finding it, but there are just so many of tehse things

[Heather Macbeth]

There sure are! docs#real.cos_add

[Kevin Lacker]

arr, i even grepped the docs for "add" but those are on a different page

[Julian Berman]

Heather Macbeth said:

How does wolframalpha work? (Of course it's closed source, so one has to guess.) It is so helpful and friendly (especially the paid version), maybe interacting with Lean can be like that someday!

(FWIW if you want open source equivalents there's also how e.g. sympy does this in Python land) Which for this example gives...

>>> var("x")
>>> solveset(Eq(cos(x) ** 2, 1/2))
Union(ImageSet(Lambda(_n, 2*_n*pi + 5*pi/4), Integers), ImageSet(Lambda(_n, 2*_n*pi + 3*pi/4), Integers), ImageSet(Lambda(_n, 2*_n*pi + 7*pi/4), Integers), ImageSet(Lambda(_n, 2*_n*pi + pi/4), Integers))

[Heather Macbeth]

@Kevin Lacker If it doesn't yet exist, I think a lemma saying that $\cos(x) = a$ implies $\{y \in \mathbb{R}:\cos(y)=a\}=\{2n\pi\pm x:n\in\mathbb{Z}\}$ would be very useful.

[Heather Macbeth]

Or maybe, $\cos(x)=\cos(y)$ implies, $\exists n\in\mathbb{Z}, y= 2n\pi + x \lor y = 2n\pi - x$.

[Heather Macbeth]

It could even be a simp-lemma.

[Kevin Lacker]

yeah... i'll try this problem and see what trig lemmas end up seeming necessary

[Kyle Miller]

Heather Macbeth said:

How does wolframalpha work? (Of course it's closed source, so one has to guess.) It is so helpful and friendly (especially the paid version), maybe interacting with Lean can be like that someday!

I'm under the impression it's a big Mathematica program, so it would more or less call Solve or Reduce when you ask for it to solve something. It seems to also interpret the results it gets and automatically try other approaches, too.

Given Stephen Wolfram's recent blog post, it would be cool if he might divert some of his company's resources into generating Lean proofs for different calculations :smile:. I know Mathematica already has some basic support for formal proofs, so there's at least some interest there. (Related: https://robertylewis.com/leanmm/) Of course, depending on how it works, a downside might be lock-in into the non-free Mathematica platform...

(Aside: something I discovered a few years ago is WolframAlpha would time out with the query "10 random people." No errors -- it just seem to think hard about this very difficult problem for a few minutes (with a pro account) then give up. They seem to have fixed it in the last year, but it doesn't seem to be using a uniform distribution because it is completely biased towards famous people.)