Zulip Chat Archive

Stream: Is there code for X?

Topic: Pi


view this post on Zulip Kevin Lacker (Oct 06 2020 at 20:49):

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

view this post on Zulip Adam Topaz (Oct 06 2020 at 20:50):

docs#real.pi

view this post on Zulip 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 [

view this post on Zulip Johan Commelin (Oct 06 2020 at 20:51):

@Kevin Lacker Do you know git grep?

view this post on Zulip Kevin Lacker (Oct 06 2020 at 20:59):

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

view this post on Zulip Adam Topaz (Oct 06 2020 at 20:59):

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

view this post on Zulip Johan Commelin (Oct 06 2020 at 20:59):

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

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:00):

yeah i didn't realize that would be a lemma

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:00):

it sure is though

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:00):

so i tried!

view this post on Zulip 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 ;)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 06 2020 at 21:02):

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

view this post on Zulip Johan Commelin (Oct 06 2020 at 21:03):

Never heard of that before (-;

view this post on Zulip Kenny Lau (Oct 06 2020 at 21:06):

and maybe something about circumference over diameter

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 21:07):

Right. We're waiting for Riemannian manifolds :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 06 2020 at 21:13):

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

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Oct 06 2020 at 21:19):

yes, let's hope that it will!

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:21):

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

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:22):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 21:23):

docs#real.cos_inj_of_nonneg_of_le_pi

view this post on Zulip Heather Macbeth (Oct 06 2020 at 21:24):

docs#real.cos_add_pi

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 21:28):

There sure are! docs#real.cos_add

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:28):

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

view this post on Zulip 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))

view this post on Zulip 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\cos(x) = a implies {yR:cos(y)=a}={2nπ±x:nZ}\{y \in \mathbb{R}:\cos(y)=a\}=\{2n\pi\pm x:n\in\mathbb{Z}\} would be very useful.

view this post on Zulip Heather Macbeth (Oct 06 2020 at 21:34):

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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 21:34):

It could even be a simp-lemma.

view this post on Zulip Kevin Lacker (Oct 06 2020 at 21:35):

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

view this post on Zulip 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