examples/my_cosine/my_cosine_M_VC_my_cosine_1.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import BuiltIn.
   4 Require Reals.Rbasic_fun.
   5 Require Reals.R_sqrt.
   6 Require Reals.Rtrigo_def.
   7 Require Reals.Rtrigo1.
   8 Require Reals.Ratan.
   9 Require BuiltIn.
  10 Require int.Int.
  11 Require real.Real.
  12 Require real.RealInfix.
  13 Require real.Abs.
  14 Require real.FromInt.
  15 Require real.Square.
  16 Require real.Trigonometry.
  17 Require floating_point.Rounding.
  18 Require floating_point.SingleFormat.
  19 Require floating_point.Single.
  20
  21 Require Import Interval.Tactic.
  22
  23 (* Why3 goal *)
  24 Theorem my_cosine'vc :
  25   forall (x:floating_point.SingleFormat.single),
  26   ((Reals.Rbasic_fun.Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R ->
  27   ((Reals.Rbasic_fun.Rabs
  28     ((1%R -
  29       (((floating_point.Single.value x) * (floating_point.Single.value x))%R
  30        * (1 / 2)%R)%R)%R
  31      - (Reals.Rtrigo_def.cos (floating_point.Single.value x)))%R)
  32    <= (1 / 16777216)%R)%R.
  33 (* Why3 intros x h1. *)
  34 Proof.
  35 intros x h1.
  36 interval with (i_bisect (Single.value x), i_autodiff (Single.value x)).
  37 Qed.