Commit 58a3586a authored by MARCHE Claude's avatar MARCHE Claude

update sessions after reinstall interval Coq tactic

parent da5b5d18
......@@ -3,133 +3,103 @@
<why3session
name="check-builtin/euclideandivision/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
id="2"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../euclideandivision.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="Test"
locfile="check-builtin/euclideandivision/../euclideandivision.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="G1"
sum="d2dce08bdba69fa50b6d8e7f01ac57fd"
locfile="check-builtin/euclideandivision/../euclideandivision.why"
loclnum="3" loccnumb="12" loccnume="14"
sum="85185e8acfb5f01cfd7b9fdca8a0be5d"
proved="true"
expanded="true"
shape="ainfix =amodc10c3c1">
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="timeout" time="10.31"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.03"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
sum="b4113a75f73aadcf47bc7eacfdd461bc"
locfile="check-builtin/euclideandivision/../euclideandivision.why"
loclnum="4" loccnumb="12" loccnume="14"
sum="8306a15d0f870a7c07cf5231a430fc7c"
proved="true"
expanded="true"
shape="ainfix =adivc10c3c3">
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="timeout" time="10.11"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="9.99"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
......@@ -6,46 +6,16 @@ Require Import Rbasic_fun.
Require Import R_sqrt.
Require Import Rtrigo.
Require Import AltSeries. (* for def of pi *)
Axiom assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = (0)%R)) ->
((Rdiv (x * y)%R z)%R = (x * (Rdiv y z)%R)%R).
Axiom assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = (0)%R)) /\
~ (z = (0)%R)) -> ((Rdiv (Rdiv x y)%R z)%R = (Rdiv x (y * z)%R)%R).
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).
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require int.Int.
Require real.Square.
Require floating_point.Rounding.
Require floating_point.Single.
Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%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),
((Rtrigo_def.cos (x + PI)%R) = (-(Rtrigo_def.cos x))%R).
......@@ -69,81 +39,17 @@ Axiom Cos_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).
Parameter atan: R -> R.
Parameter atan: R -> R.
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 *)
Require Import Interval_tactic.
(* DO NOT EDIT BELOW *)
Theorem MethodError : forall (x:R), ((Rabs x) <= (1 / 32)%R)%R ->
((Rabs (((1)%R - ((05 / 10)%R * (x * x)%R)%R)%R - (Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
((Rabs ((1%R - ((05 / 10)%R * (x * x)%R)%R)%R - (Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
interval with (i_bisect_diff x).
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="./my_cosine/why3session.xml">
name="my_cosine/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
id="1"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
id="2"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../my_cosine.why"
verified="true"
expanded="true">
<theory
name="CosineSingle"
locfile="my_cosine/../my_cosine.why"
loclnum="1" loccnumb="7" loccnume="19"
verified="true"
expanded="true">
<goal
name="MethodError"
locfile="my_cosine/../my_cosine.why"
loclnum="13" loccnumb="6" loccnume="17"
sum="5952f9383dbffe78b1fa14037bc54de0"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<proof
prover="coq"
timelimit="2"
prover="1"
timelimit="10"
edited="my_cosine_CosineSingle_MethodError_1.v"
obsolete="false">
<result status="valid" time="3.90"/>
obsolete="false"
archived="false">
<result status="valid" time="3.73"/>
</proof>
</goal>
<goal
name="TotalErrorFullyExpanded"
locfile="my_cosine/../my_cosine.why"
loclnum="20" loccnumb="6" loccnume="29"
sum="25f5a9c908fe4d1265b4f0f95504caa8"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
<proof
prover="gappa"
prover="2"
timelimit="2"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="TotalErrorExpanded"
locfile="my_cosine/../my_cosine.why"
loclnum="31" loccnumb="6" loccnume="24"
sum="847de2c0fab20f50a5c8c20a22a7efcf"
proved="true"
expanded="true"
shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof
prover="alt-ergo"
prover="0"
timelimit="2"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.86"/>
</proof>
</goal>
<goal
name="TotalError"
locfile="my_cosine/../my_cosine.why"
loclnum="51" loccnumb="6" loccnume="16"
sum="5af50be8fb318e8a3b66da558f5685c7"
proved="true"
expanded="true"
shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="3.04"/>
</proof>
</goal>
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="fill/why3session.xml">
name="examples/programs/fill/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.93.1"/>
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Z3"
version="2.19"/>
<prover
id="4"
name="Z3"
version="3.2"/>
<file
name="../fill.mlw"
verified="true"
expanded="true">
<theory
name="WP Fill"
locfile="fill/../fill.mlw"
loclnum="2" loccnumb="7" loccnume="11"
locfile="examples/programs/fill/../fill.mlw"
loclnum="4" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter fill"
locfile="fill/../fill.mlw"
loclnum="14" loccnumb="10" loccnume="14"
locfile="examples/programs/fill/../fill.mlw"
loclnum="16" loccnumb="10" loccnume="14"
expl="parameter fill"
sum="a7f6d0a4fd8b99196978e39ff255fcf5"
proved="true"
......@@ -28,11 +44,40 @@
<label
name="expl:parameter fill">
</label>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="unknown" time="0.18"/>
</proof>
<proof
prover="1"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false">
<result status="valid" time="0.15"/>
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="2"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
<proof
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
</proof>
</goal>
</theory>
......
......@@ -3,146 +3,133 @@
<why3session
name="programs/gcd/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
id="2"
name="Coq"
version="8.3pl3"/>
<prover
id="z3-2"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../gcd.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="WP EuclideanAlgorithm"
locfile="programs/gcd/../gcd.mlw"
loclnum="4" loccnumb="7" loccnume="25"
verified="true"
expanded="true">
<goal
name="WP_parameter gcd"
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="parameter gcd"
sum="b28ef6fde19dc9f3f079ce585be1c6eb"
sum="99b02a65fe607568247eecce3b17a059"
proved="true"
expanded="true"
shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0FF">
<label
name="expl:parameter gcd">
</label>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter gcd.1"
locfile="programs/gcd/../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="normal postcondition"
sum="9e6b1eaa8e540fb56b8b062bfc4c8651"
sum="d27f34a8e592811f5fa2bb4bad56e1cf"
proved="true"
expanded="true"
shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0FF">
<label
name="expl:parameter gcd">
</label>
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof