my_cosine.mlw_Pgm_WP_my_cosine.v 5.41 KB
Newer Older
Claude Marche's avatar
Claude Marche committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
(* Beware! Only edit allowed sections below    *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Require Import Rbasic_fun.
Require Import R_sqrt.
Require Import Rtrigo.
Require Import AltSeries.
Definition unit  := unit.

Parameter ignore: forall (a:Type), a  -> unit.
Implicit Arguments ignore.

Parameter arrow : forall (a:Type) (b:Type), Type.

Parameter ref : forall (a:Type), Type.

Parameter prefix_ex: forall (a:Type), (ref a)  -> a.
Implicit Arguments prefix_ex.

Parameter label : Type.

Parameter at1: forall (a:Type), a -> label  -> a.
Implicit Arguments at1.

Parameter old: forall (a:Type), a  -> a.
Implicit Arguments old.

Parameter exn : Type.

Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x <  y)%Z.

Axiom Refl : forall (x:R), (x <= x)%R.

Axiom Trans : forall (x:R) (y:R) (z:R), (x <= y)%R -> ((y <= z)%R ->
  (x <= z)%R).

Axiom Antisymm : forall (x:R) (y:R), (x <= y)%R -> ((y <= x)%R -> (x = y)).

Axiom Total : forall (x:R) (y:R), (x <= y)%R \/ (y <= x)%R.

Axiom Abs_le : forall (x:R) (y:R), ((Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\
  (x <= y)%R).

Axiom Abs_pos : forall (x:R), ((0)%R <= (Rabs x))%R.

Axiom Sqrt_positive : forall (x:R), ((0)%R <= x)%R -> ((0)%R <= (sqrt x))%R.

Axiom Sqrt_square : forall (x:R), ((0)%R <= x)%R ->
  (((sqrt x) * (sqrt x))%R = x).

Axiom Square_sqrt : forall (x:R), ((0)%R <= x)%R -> ((sqrt (x * x)%R) = x).

Axiom Pythagorean_identity : forall (x:R),
  ((((cos x) * (cos x))%R + ((sin x) * (sin x))%R)%R = (1)%R).

Axiom Cos_le_one : forall (x:R), ((Rabs (cos x)) <= (1)%R)%R.

Axiom Sin_le_one : forall (x:R), ((Rabs (sin x)) <= (1)%R)%R.

Axiom Cos_0 : ((cos (0)%R) = (1)%R).

Axiom Sin_0 : ((sin (0)%R) = (0)%R).

Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R <  PI)%R /\
  (PI <  (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.

Axiom Cos_pi : ((cos PI) = (-(1)%R)%R).

Axiom Sin_pi : ((sin PI) = (0)%R).

Axiom Cos_pi2 : ((cos ((05 / 10)%R * PI)%R) = (0)%R).

Axiom Sin_pi2 : ((sin ((05 / 10)%R * PI)%R) = (1)%R).

Axiom Cos_plus_pi : forall (x:R), ((cos (x + PI)%R) = (-(cos x))%R).

Axiom Sin_plus_pi : forall (x:R), ((sin (x + PI)%R) = (-(sin x))%R).

Axiom Cos_plus_pi2 : forall (x:R),
  ((cos (x + ((05 / 10)%R * PI)%R)%R) = (-(sin x))%R).

Axiom Sin_plus_pi2 : forall (x:R),
  ((sin (x + ((05 / 10)%R * PI)%R)%R) = (cos x)).

Axiom Cos_neg : forall (x:R), ((cos (-x)%R) = (cos x)).

Axiom Sin_neg : forall (x:R), ((sin (-x)%R) = (-(sin x))%R).

Axiom Cos_sum : forall (x:R) (y:R),
  ((cos (x + y)%R) = (((cos x) * (cos y))%R - ((sin x) * (sin y))%R)%R).

Axiom Sin_sum : forall (x:R) (y:R),
  ((sin (x + y)%R) = (((sin x) * (cos y))%R + ((cos x) * (sin y))%R)%R).

Parameter atan: R  -> R.

Axiom Tan_atan : forall (x:R), ((tan (atan x)) = x).

Inductive mode  :=
  | nearestTiesToEven : mode 
  | toZero : mode 
  | up : mode 
  | down : mode 
  | nearTiesToAway : mode .

Parameter single : Type.

Axiom Zero : ((IZR 0%Z) = (0)%R).

Axiom One : ((IZR 1%Z) = (1)%R).

Axiom Add : forall (x:Z) (y:Z), ((IZR (x + y)%Z) = ((IZR x) + (IZR y))%R).

Axiom Sub : forall (x:Z) (y:Z), ((IZR (x - y)%Z) = ((IZR x) - (IZR y))%R).

Axiom Mul : forall (x:Z) (y:Z), ((IZR (x * y)%Z) = ((IZR x) * (IZR y))%R).

Axiom Neg : forall (x:Z) (y:Z), ((IZR (-x)%Z) = (-(IZR x))%R).

Parameter round: mode -> R  -> R.

Parameter round_logic: mode -> R  -> single.

Parameter value: single  -> R.

Parameter exact: single  -> R.

Parameter model: single  -> R.

Definition round_error(x:single): R := (Rabs ((value x) - (exact x))%R).

Definition total_error(x:single): R := (Rabs ((value x) - (model x))%R).

Definition no_overflow(m:mode) (x:R): Prop := ((Rabs (round m
  x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.

Axiom Bounded_real_no_overflow : forall (m:mode) (x:R),
  ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
  (no_overflow m x).

Axiom Round_monotonic : forall (m:mode) (x:R) (y:R), (x <= y)%R -> ((round m
  x) <= (round m y))%R.

Axiom Exact_rounding_for_integers : forall (m:mode) (i:Z),
  (((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) -> ((round m
  (IZR i)) = (IZR i)).

Axiom Round_down_le : forall (x:R), ((round (down ) x) <= x)%R.

Axiom Round_up_ge : forall (x:R), (x <= (round (up ) x))%R.

Axiom Round_down_neg : forall (x:R), ((round (down ) (-x)%R) = (-(round (up )
  x))%R).

Axiom Round_up_neg : forall (x:R), ((round (up ) (-x)%R) = (-(round (down )
  x))%R).

Theorem WP_my_cosine : forall (x:single),
  ((Rabs (value x)) <= (1 / 32)%R)%R ->
  ((Rabs (((1)%R - (((value x) * (value x))%R * (05 / 10)%R)%R)%R - (cos (value x)))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x Hx.
Require Import Interval_tactic.
interval with (i_bisect_diff (value x)).
Qed.
(* DO NOT EDIT BELOW *)