Evaluating Real numbers to decimal representation

Require Import Reals.
(* Euler's formula in Horner's form *)
Definition pi := (nat_rect _ 0 (fun n p => 2 + p * INR n / (2 * INR n + 1)))%R.   

What is the easiest way to evaluate pi 100 and print the first 15 decimals?

From Coq Require Import Reals.
From Interval Require Import Tactic.
Definition pi := (nat_rect _ 0 (fun n p => 2 + p * IZR (Z_of_nat n) / (2 * IZR (Z_of_nat n) + 1)))%R.
Goal True.
let v := eval simpl in (pi 100) in
interval_intro v.

gives

H : (8961703559183965 / 2251799813685248 <=
     2 + (2 + (2 + (2 + (2 + (2 + (2 + (2 +  (2 +
             (2 + (2 + (...) * 89 / (... + 1)) * 90 / (2 * 90 + 1)) * 91 / (2 * 91 + 1)) *
            92 / (2 * 92 + 1)) * 93 / (2 * 93 + 1)) * 94 / (2 * 94 + 1)) * 95 /
         (2 * 95 + 1)) * 96 / (2 * 96 + 1)) * 97 / (2 * 97 + 1)) * 98 / 
      (2 * 98 + 1)) * 99 / (2 * 99 + 1) <= 8961703559183979 / 2251799813685248)%R

Now, you need to use some other tool to convert the bounds to decimal, which gives you 3.979795852508501 <= ... <= 3.979795852508507, hence your fifteen digits.

I had to change INR to IZR in your definition of pi, otherwise Coq kind of dies while displaying H, but in theory it should also work with INR for smaller values of n.

If you do not want to use an external tool to get the decimal digits, you can use a slightly more complicated formula:

let v := eval simpl in (IZR (Raux.Zfloor (pi 100 * powerRZ 10 14))) in
interval_intro v with (i_prec 90).

Thanks!

How utterly embarrassing to compute pi to 3.97…

Require Import Reals.
Open Scope R.
From Interval Require Import Tactic. (* 'interval' tactic *)

Require Import List. Import ListNotations.
Definition Dec := fold_right (fun a b => a + b/10) 0.

Definition pi m := (nat_rect _ 0 (fun n p => 2 + p * IZR (Z_of_nat (m-n)) / (2 * IZR (Z_of_nat (m-n)) + 1)) m)%R.

Definition x := Dec [3;1;4;1;5;9;2;6;5;3;5;8;9;7;9].
Definition eps := 1/100000000000000.

Goal x < pi 100 < x + eps.
  split; unfold x, eps, pi; simpl; interval.
Qed.

Goal True.

  let X := (eval simpl in (pi 20)) in
  let x := (eval unfold pi in X) in
  let y := (eval simpl     in x) in
  interval_intro y with (i_prec 100) as EQ;
    replace y with X in * by reflexivity.

(*
  EQ : 995610223197390062935504709050 / 316912650057057350374175801344 <= 
       pi 20 <= 995610223197390062935504709052 / 316912650057057350374175801344
  ============================
  True
 *)


1 Like

One can use the exact real numbers from math-classes/corn. I can try to give more instructions later when I find the time.
https://math-classes.github.io/

@VincentSe may also be interested

1 Like