theory real.Trigonometry: replaced the insanely too precise bounds

for pi by the best possible bounds in double-precision IEEE-754
floating-point numbers

lib/coq/bv/BV_Gen.v

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 (* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
@@ -1845,3 +1856,4 @@ Lemma Extensionality : forall (x:t) (y:t), (eq_sub x y 0%Z size) -> (x = y).
   intros x y.
   apply Extensionality_aux.
 Qed.
+

lib/coq/bv/Pow2int.v

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 (* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.

lib/coq/real/Trigonometry.v

@@ -73,13 +73,16 @@ Qed.
 (* pi is replaced with Reals.Rtrigo1.PI by the coq driver *)
 
 (* Why3 goal *)
-Lemma Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < Reals.Rtrigo1.PI)%R /\
-  (Reals.Rtrigo1.PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
+Lemma Pi_double_precision_bounds : ((7074237752028440 / 2251799813685248)%R < Reals.Rtrigo1.PI)%R /\
+  (Reals.Rtrigo1.PI < (7074237752028441 / 2251799813685248)%R)%R.
 Proof.
 replace PI with (4 * (PI / 4))%R by field.
 rewrite <- atan_1.
 admit. (* to avoid a dependency on CoqInterval *)
-(* split ; interval with (i_prec 680). *)
+(*
+Require Import Interval_tactic.
+split ; interval with (i_prec 55). 
+*)
 Qed.
 
 (* Why3 goal *)

lib/isabelle/Why3_Real.thy

@@ -336,13 +336,13 @@ why3_vc Sin_le_one by auto
 
 why3_vc Cos_plus_pi by auto
 
-why3_vc Pi_interval
+why3_vc Pi_double_precision_bounds
 proof -
-  have "3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 < pi"
-    by (approximation 670)
+  have "7074237752028440 / 2251799813685248 < pi"
+    by (approximation 57)
   then show ?C1 by simp
-  have "pi < 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197"
-    by (approximation 670)
+  have "pi < 7074237752028441 / 2251799813685248"
+    by (approximation 55)
   then show ?C2 by simp
 qed
 

theories/real.why

@@ -308,10 +308,14 @@ theory Trigonometry
 
   constant pi : real
 
+  axiom Pi_double_precision_bounds:
+    0x1.921fb54442d18p+1 < pi < 0x1.921fb54442d19p+1
+(*
   axiom Pi_interval:
    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
    < pi <
    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+*)
 
   axiom Cos_pi: cos pi = -1.0
   axiom Sin_pi: sin pi = 0.0