Computing hexadecimal digits of Π with the Plouffe formula.

Plouffe formula is an efficient way of computing the nth digit of Π in hexadecimal. Its Coq formalisation is composed of two files:

The proof of the formula Plouffe.html, Plouffe.v

The proof of the program CPlouffe.html CPlouffe.v

It requires ssreflect and coquelicot to compile. We can have a tar file or an opam package.

Once compiled, you can get the one millionth decimal (in Hexadecimal) of Π in Coq with the command :

Require Import CPlouffe.

Compute digit 1000000.
     = "2"%string
     : string

or the one billionth decimal :

Compute digit 1000000000.
     = "F"%string
     : string

The computation is performed in fixed size (the default is 40 bits). If it is not enough the program returns ? as a digit. Increasing the size will solve the problem.

Laurence Rideau & Laurent Théry