Commit 33918667 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix testsuite breakage due to floating-point theories for Coq and Gappa provers.

parent 20f53fc1
...@@ -187,7 +187,7 @@ theory floating_point.Rounding ...@@ -187,7 +187,7 @@ theory floating_point.Rounding
syntax function ToZero "zr" syntax function ToZero "zr"
syntax function Up "up" syntax function Up "up"
syntax function Down "dn" syntax function Down "dn"
syntax function NearTiesToAway "na" syntax function NearestTiesToAway "na"
end end
......
...@@ -6,58 +6,34 @@ Require Import Rbasic_fun. ...@@ -6,58 +6,34 @@ Require Import Rbasic_fun.
Require Import R_sqrt. Require Import R_sqrt.
Require Import Rtrigo. Require Import Rtrigo.
Require Import AltSeries. (* for def of pi *) Require Import AltSeries. (* for def of pi *)
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require real.Square.
Require floating_point.Rounding.
Require floating_point.Single.
Definition unit := unit. Definition unit := unit.
Parameter mark : Type. Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> mark -> a. Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1. Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a. Parameter old: forall (a:Type), a -> a.
Implicit Arguments old. Implicit Arguments old.
Axiom assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = (0)%R)) -> Definition implb(x:bool) (y:bool): bool := match (x,
((Rdiv (x * y)%R z)%R = (x * (Rdiv y z)%R)%R). y) with
| (true, false) => false
Axiom assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = (0)%R)) /\ | (_, _) => true
~ (z = (0)%R)) -> ((Rdiv (Rdiv x y)%R z)%R = (Rdiv x (y * z)%R)%R). end.
Axiom assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = (0)%R)) /\
~ (z = (0)%R)) -> ((Rdiv x (Rdiv y z)%R)%R = (Rdiv (x * z)%R y)%R).
Axiom Abs_le : forall (x:R) (y:R), ((Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\
(x <= y)%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 -> ((Rsqr (sqrt x)) = x).
Axiom Square_sqrt : forall (x:R), ((0)%R <= x)%R -> ((sqrt (x * x)%R) = x).
Axiom Pythagorean_identity : forall (x:R),
(((Rsqr (Rtrigo_def.cos x)) + (Rsqr (Rtrigo_def.sin x)))%R = (1)%R).
Axiom Cos_le_one : forall (x:R), ((Rabs (Rtrigo_def.cos x)) <= (1)%R)%R.
Axiom Sin_le_one : forall (x:R), ((Rabs (Rtrigo_def.sin x)) <= (1)%R)%R.
Axiom Cos_0 : ((Rtrigo_def.cos (0)%R) = (1)%R).
Axiom Sin_0 : ((Rtrigo_def.sin (0)%R) = (0)%R).
Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\ Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
(PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R. (PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
Axiom Cos_pi : ((Rtrigo_def.cos PI) = (-(1)%R)%R).
Axiom Sin_pi : ((Rtrigo_def.sin PI) = (0)%R).
Axiom Cos_pi2 : ((Rtrigo_def.cos ((05 / 10)%R * PI)%R) = (0)%R).
Axiom Sin_pi2 : ((Rtrigo_def.sin ((05 / 10)%R * PI)%R) = (1)%R).
Axiom Cos_plus_pi : forall (x:R), Axiom Cos_plus_pi : forall (x:R),
((Rtrigo_def.cos (x + PI)%R) = (-(Rtrigo_def.cos x))%R). ((Rtrigo_def.cos (x + PI)%R) = (-(Rtrigo_def.cos x))%R).
...@@ -81,87 +57,23 @@ Axiom Cos_sum : forall (x:R) (y:R), ...@@ -81,87 +57,23 @@ Axiom Cos_sum : forall (x:R) (y:R),
Axiom Sin_sum : forall (x:R) (y:R), Axiom Sin_sum : forall (x:R) (y:R),
((Rtrigo_def.sin (x + y)%R) = (((Rtrigo_def.sin x) * (Rtrigo_def.cos y))%R + ((Rtrigo_def.cos x) * (Rtrigo_def.sin y))%R)%R). ((Rtrigo_def.sin (x + y)%R) = (((Rtrigo_def.sin x) * (Rtrigo_def.cos y))%R + ((Rtrigo_def.cos x) * (Rtrigo_def.sin y))%R)%R).
Parameter atan: R -> R. Parameter atan: R -> R.
Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x). Axiom Tan_atan : forall (x:R), ((Rtrigo.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), ((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).
(* YOU MAY EDIT THE CONTEXT BELOW *) (* YOU MAY EDIT THE CONTEXT BELOW *)
Require Import Interval_tactic. Require Import Interval_tactic.
(* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *)
Theorem WP_parameter_my_cosine : forall (x:single), Theorem WP_parameter_my_cosine : forall (x:floating_point.Single.single),
((Rabs (value x)) <= (1 / 32)%R)%R -> ((Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R ->
((Rabs (((1)%R - (((value x) * (value x))%R * (05 / 10)%R)%R)%R - (Rtrigo_def.cos (value x)))%R) <= (1 / 16777216)%R)%R. ((Rabs ((1%R - (((floating_point.Single.value x) * (floating_point.Single.value x))%R * (05 / 10)%R)%R)%R - (Rtrigo_def.cos (floating_point.Single.value x)))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *) (* YOU MAY EDIT THE PROOF BELOW *)
intros x H. intros x H.
interval with (i_bisect_diff (value x)). interval with (i_bisect_diff (Single.value x)).
Qed. Qed.
(* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment