Commit e73db6d3 authored by MARCHE Claude's avatar MARCHE Claude

euler001 in regression tests

parent 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/euler001/why3session.xml">
<file name="../euler001.mlw" verified="false" expanded="true">
<theory name="SumMultiple" verified="false" expanded="true">
<goal name="div_minus1_1" sum="f5f3412d9b58086a6e9b482e89262ec3" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.40"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.22"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.06"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.38"/>
</proof>
</goal>
<goal name="div_minus1_2" sum="58b4c2b7cc926f7281ef2d9806046849" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.30"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.24"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.04"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>
<goal name="mod_15" sum="e2d678bf333354c7d41e3255a00ce78b" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.13"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.44"/>
</proof>
</goal>
<goal name="Closed_formula_0" sum="bedb2551f46c9bf80e4fd6d1cddcc221" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Closed_formula_n_1" sum="07cd7a1e0916a0fd5db441ad655752d4" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.17"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="Closed_formula_n_2" sum="9f118f99f106bbd45be20274179078b5" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>
<goal name="Closed_formula" sum="6a9095ec398278b6e7fa407e16f64039" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</theory>
<theory name="Euler001" verified="true" expanded="false">
<goal name="WP_parameter solve" expl="normal postcondition" sum="c41d9ff50a1fcc7bd5f7a82e94c058f3" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.68"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.16"/>
</proof>
</goal>
</theory>
</file>
</why3session>
(* 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 *)
Require Import Interval_tactic.
intros x Pre.
interval with (i_bisect_diff (value x)).
Qed.
(* DO NOT EDIT BELOW *)
(* 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. (* for def of pi *)
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 *)
Require Import Interval_tactic.
intros x Pre.
interval with (i_bisect_diff (value x)).
Qed.
(* 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