coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Anounce: pi-agm 1.0.0
- Date: Thu, 1 Sep 2016 14:11:13 +0200
I am happy to announce the release of a formally verified algorithm to compute pi using
arithmetic geometric means.
This algorithm is available on the opam coq archive in the reposity 'released' under the name coq-pi-agm.
Version 1.0.0 works only with coq-8.4 and coquelicot-2.0.1. Updates to newer versions of Coq and
libraries will be made available as soon as possible.
Once you have installed this package, you can compute arbitrarily precise approximations of PI using the function rounding_big.hpi, as stated by theorems rounding_big.hpi_Z and rounding.integer_pi. In particular, the value million_digit_pi and the theorem pi_osix describe the required parameters to compute one million decimals of PI. Beware that fully computing this value may take up to 10 hours (but computing 1000 decimals only takes a second).
The source archive is available at
http://www.inria.fr/sophia/members/Yves.Bertot/proofs/pi_agm_1_0_0.tar.gz
Its compilation requires coq-8.4 (tested with coq-8.4.6) and coquelicot-2.0.1.
Yves
- [Coq-Club] Anounce: pi-agm 1.0.0, Yves Bertot, 09/01/2016
Archive powered by MHonArc 2.6.18.