Heiko Becker (Nov 03 2021 at 10:47): 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
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
Heiko Becker (Nov 03 2021 at 10:53):I did not run into this before. Thanks a lot for the pointer!
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
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 )
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
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