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,
have you seen this? http://www-sop.inria.fr/marelle/distant-decimals-pi/
references https://github.com/thery/Plouffe which builds with latest Coq
I did not run into this before. Thanks a lot for the pointer!
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
would be nice to get the Lindemann repo maintained and working with latest Coq/MathComp (cc: @Yves Bertot )
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
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: Feb 27 2024 at 22:02 UTC