The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

Dear Guillaume,

 

first let me thank Guillaume and all other contributors for the great “Interval” library! I am currently working on verification of numerical C code and HW, and this library / tactics do a good part of the hard work in a very pleasant and efficient way.

 

There is one thing I don’t understand, though.: i_bisect_taylor and i_bisect work as expected, but I don’t understand what i_bisect_diff does. I would expect that the results of i_bisect_diff is similar to i_bisect_taylor x 1, since both should take 1^st derivative information into account – maybe in a slightly different way. But to my surprise i_bisect_diff gives in all cases I tried the same result as i_bisect, which is far away from i_bisect_taylor x 1. Below is a simple example, which also shows the error bounds I get. Could you please explain this behavior?

 

I have one more question: I guess my Coq skill is slightly rusted: how can I supply the term “t” to the tactic in the below example?

 

Best regards,

 

Michael

 

 

Require Import Reals.

Require Import Interval.Interval_tactic.

 

Open Scope R_scope.

 

Definition f   x :=sin (x).

Definition s1:= 4294967285/2^32.

Definition s3:= -715784163/2^32.

Definition fp3 x :=s1 * x + s3 * x^3.

 

Goal forall x, -1/32 <= x <= 1/32 -> True.

Proof.

  intros.

  pose (f(x)-fp3(x)) as t.

  unfold f,fp3,s1,s3 in t.

 

(* i_bisect_taylor 4th order = 1.77355302815385*10^-11 (sufficiently close to real deviation) *)

 

  Time interval_intro (Rabs (sin x - (4294967285 / 2 ^ 32 * x + -715784163 / 2 ^ 32 * x ^ 3)))

    upper with (i_prec 60, i_depth 5, i_bisect_taylor x 4, i_delay) as Ht4.

 

(* i_bisect_taylor 1st order = 5.713030931057944*10^-8 *)

 

  Time interval_intro (Rabs (sin x - (4294967285 / 2 ^ 32 * x + -715784163 / 2 ^ 32 * x ^ 3)))

    upper with (i_prec 60, i_depth 5, i_bisect_taylor x 1, i_delay) as Ht1.

 

(* i_bisect_diff = 0.003906250007731088 *)

 

  Time interval_intro (Rabs (sin x - (4294967285 / 2 ^ 32 * x + -715784163 / 2 ^ 32 * x ^ 3)))

    upper with (i_prec 60, i_depth 5, i_bisect_diff x, i_delay) as Hbd.

 

(* i_bisect = 0.003906250007731088 *)

 

  Time interval_intro (Rabs (sin x - (4294967285 / 2 ^ 32 * x + -715784163 / 2 ^ 32 * x ^ 3)))

    upper with (i_prec 60, i_depth 5, i_bisect x, i_delay) as Hb.

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928