## Stream: Is there code for X?

### Topic: Pi

#### Kevin Lacker (Oct 06 2020 at 20:49):

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

docs#real.pi

#### Johan Commelin (Oct 06 2020 at 20:50):

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 (Oct 06 2020 at 20:51):

@Kevin Lacker Do you know git grep?

#### Kevin Lacker (Oct 06 2020 at 20:59):

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

#### Adam Topaz (Oct 06 2020 at 20:59):

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

#### Johan Commelin (Oct 06 2020 at 20:59):

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

#### Kevin Lacker (Oct 06 2020 at 20:59):

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

#### Kevin Lacker (Oct 06 2020 at 21:00):

yeah i didn't realize that would be a lemma

#### Kevin Lacker (Oct 06 2020 at 21:00):

it sure is though

#### Kevin Lacker (Oct 06 2020 at 21:00):

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

so i tried!

#### Adam Topaz (Oct 06 2020 at 21:01):

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 (Oct 06 2020 at 21:01):

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

#### Kenny Lau (Oct 06 2020 at 21:02):

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

#### Johan Commelin (Oct 06 2020 at 21:03):

Never heard of that before (-;

#### Kenny Lau (Oct 06 2020 at 21:06):

and maybe something about circumference over diameter

#### Kevin Lacker (Oct 06 2020 at 21:06):

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

#### Kevin Lacker (Oct 06 2020 at 21:07):

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 (Oct 06 2020 at 21:07):

Right. We're waiting for Riemannian manifolds :)

#### Heather Macbeth (Oct 06 2020 at 21:12):

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 (Oct 06 2020 at 21:13):

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

#### Johan Commelin (Oct 06 2020 at 21:13):

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

#### Heather Macbeth (Oct 06 2020 at 21:17):

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 (Oct 06 2020 at 21:19):

yes, let's hope that it will!

#### Kevin Lacker (Oct 06 2020 at 21:21):

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

#### Kevin Lacker (Oct 06 2020 at 21:22):

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

#### Heather Macbeth (Oct 06 2020 at 21:22):

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 (Oct 06 2020 at 21:22):

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

#### Heather Macbeth (Oct 06 2020 at 21:23):

docs#real.cos_inj_of_nonneg_of_le_pi

#### Heather Macbeth (Oct 06 2020 at 21:26):

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

#### Kevin Lacker (Oct 06 2020 at 21:26):

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

#### Kevin Lacker (Oct 06 2020 at 21:28):

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

#### Julian Berman (Oct 06 2020 at 21:30):

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 (Oct 06 2020 at 21:31):

@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 (Oct 06 2020 at 21:34):

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

#### Heather Macbeth (Oct 06 2020 at 21:34):

It could even be a simp-lemma.

#### Kevin Lacker (Oct 06 2020 at 21:35):

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

#### Kyle Miller (Oct 06 2020 at 22:00):

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

Last updated: May 07 2021 at 22:14 UTC