Stream: math-comp users

Topic: Proofs about pi


view this post on Zulip Heiko Becker (Nov 03 2021 at 10:47):

Hi all,
I am not a math-comp user per se, as I mainly do proofs in HOL4, but I am currently trying to find out how different ITP systems have formalized pi, and proven properties of it.
I already found the definition and proofs for Pi from CCorn (https://github.com/coq-community/corn/blob/master/transc/Pi.v) but for math-comp I am struggling to search through the official documentation. Searching for pi in the definition index (https://math-comp.github.io/htmldoc_1_13_0/index_definition_P.html) I could not find any definition that looked like the mathematical constant pi.

Thanks in advance for any replies,

Heiko

view this post on Zulip Karl Palmskog (Nov 03 2021 at 10:50):

have you seen this? http://www-sop.inria.fr/marelle/distant-decimals-pi/

references https://github.com/thery/Plouffe which builds with latest Coq

view this post on Zulip Heiko Becker (Nov 03 2021 at 10:53):

I did not run into this before. Thanks a lot for the pointer!

view this post on Zulip Karl Palmskog (Nov 03 2021 at 10:55):

also, proof of transcendence for pi: https://arxiv.org/abs/1512.02791

I think the latest code for this is here: https://github.com/Sobernard/Lindemann

view this post on Zulip Karl Palmskog (Nov 03 2021 at 10:57):

would be nice to get the Lindemann repo maintained and working with latest Coq/MathComp (cc: @Yves Bertot )

view this post on Zulip Karl Palmskog (Nov 03 2021 at 11:59):

I think most of everyone is using the Pi definition from Stdlib as a spec: https://github.com/coq/coq/blob/master/theories/Reals/Rtrigo1.v#L227

view this post on Zulip Pierre Roux (Nov 03 2021 at 12:26):

There is also an interval enclosure computing function in CoqInterval https://gitlab.inria.fr/coqinterval/interval/-/blob/master/src/Interval/Float_full.v#L41


Last updated: Jan 29 2023 at 18:03 UTC