Update testsuite to Coq 8.4.

24c33a54 · Guillaume Melquiond · 38cee140 · 24c33a54 · 24c33a54 · 24c33a54
Commit 24c33a54 authored Aug 20, 2013 by Guillaume Melquiond
71 changed files
--- a/examples/alphaBeta/why3session.xml
+++ b/examples/alphaBeta/why3session.xml
@@ -16,7 +16,7 @@
 <prover
  id="3"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="4"
  name="Z3"
@@ -54,7 +54,7 @@
     edited="alphaBeta_TwoPlayerGame_Test_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="1.07"/>
    </proof>
    <proof
     prover="4"
@@ -88,7 +88,7 @@
     edited="alphaBeta_TwoPlayerGame_minmax_bound_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.80"/>
+     <result status="valid" time="1.58"/>
    </proof>
   </goal>
   <goal

--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
@@ -16,7 +16,7 @@
 <prover
  id="3"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="4"
  name="Z3"
@@ -165,7 +165,7 @@
     edited="double_TestDouble_exp_one_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.61"/>
+     <result status="valid" time="1.21"/>
    </proof>
   </goal>
   <goal
@@ -198,7 +198,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="2.91"/>
+     <result status="valid" time="3.36"/>
    </proof>
   </goal>
   <goal

--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
@@ -20,7 +20,7 @@
 <prover
  id="4"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="5"
  name="Gappa"
@@ -468,7 +468,7 @@
     edited="double_of_int_DoubleOfInt_exp_const_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.16"/>
+     <result status="valid" time="1.75"/>
    </proof>
   </goal>
   <goal
@@ -567,7 +567,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.14"/>
+     <result status="valid" time="0.27"/>
    </proof>
    <proof
     prover="3"
@@ -583,7 +583,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.28"/>
+     <result status="valid" time="1.01"/>
    </proof>
    <proof
     prover="7"
@@ -888,7 +888,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="8.87"/>
+     <result status="valid" time="7.52"/>
    </proof>
    <proof
     prover="3"
@@ -1004,7 +1004,7 @@
     edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="2.94"/>
+     <result status="valid" time="3.71"/>
    </proof>
   </goal>
   <goal
@@ -1022,7 +1022,7 @@
     edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="4.19"/>
+     <result status="valid" time="5.21"/>
    </proof>
   </goal>
   <goal
@@ -1089,7 +1089,7 @@
     edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="3.48"/>
+     <result status="valid" time="4.72"/>
    </proof>
   </goal>
   <goal
@@ -1107,7 +1107,7 @@
     edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.87"/>
+     <result status="valid" time="1.44"/>
    </proof>
   </goal>
   <goal
@@ -1207,7 +1207,7 @@
     edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="5.76"/>
+     <result status="valid" time="6.78"/>
    </proof>
   </goal>
   <goal
@@ -1314,7 +1314,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="140.04"/>
+     <result status="valid" time="125.06"/>
    </proof>
    <proof
     prover="3"
@@ -1373,7 +1373,7 @@
     edited="double_of_int_DoubleOfInt_lemma2_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="3.97"/>
+     <result status="valid" time="5.30"/>
    </proof>
   </goal>
   <goal
@@ -1556,7 +1556,7 @@
     edited="double_of_int_DoubleOfInt_lemma3_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="2.62"/>
+     <result status="valid" time="3.16"/>
    </proof>
   </goal>
   <goal
@@ -1745,7 +1745,7 @@
     edited="double_of_int_DoubleOfInt_var_value0_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.88"/>
+     <result status="valid" time="2.62"/>
    </proof>
   </goal>
   <goal

--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
@@ -12,7 +12,7 @@
 <prover
  id="2"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="3"
  name="Z3"
@@ -427,7 +427,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.21"/>
+     <result status="valid" time="1.53"/>
    </proof>
    <proof
     prover="4"
@@ -486,7 +486,7 @@
     edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.20"/>
+     <result status="valid" time="1.90"/>
    </proof>
   </goal>
  </theory>

--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
@@ -16,7 +16,7 @@
 <prover
  id="3"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="4"
  name="Gappa"
@@ -103,7 +103,7 @@
     edited="power2_Pow2int_Power_sum_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.77"/>
+     <result status="valid" time="1.23"/>
    </proof>
   </goal>
   <goal
@@ -121,7 +121,7 @@
     edited="power2_Pow2int_pow2pos_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.59"/>
+     <result status="valid" time="1.18"/>
    </proof>
   </goal>
   <goal
@@ -3311,7 +3311,7 @@
     edited="power2_Pow2int_Mod_pow2_gen_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.20"/>
+     <result status="valid" time="1.80"/>
    </proof>
   </goal>
  </theory>
@@ -3589,7 +3589,7 @@
     edited="power2_Pow2real_Power_non_null_aux_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.58"/>
+     <result status="valid" time="1.21"/>
    </proof>
   </goal>
   <goal
@@ -3607,7 +3607,7 @@
     edited="power2_Pow2real_Power_neg_aux_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.74"/>
+     <result status="valid" time="1.36"/>
    </proof>
   </goal>
   <goal
@@ -3625,7 +3625,7 @@
     edited="power2_Pow2real_Power_non_null_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.67"/>
+     <result status="valid" time="1.29"/>
    </proof>
   </goal>
   <goal
@@ -3668,7 +3668,7 @@
     edited="power2_Pow2real_Power_sum_aux_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.72"/>
+     <result status="valid" time="1.38"/>
    </proof>
   </goal>
   <goal
@@ -3686,7 +3686,7 @@
     edited="power2_Pow2real_Power_sum_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.83"/>
+     <result status="valid" time="1.27"/>
    </proof>
   </goal>
   <goal
@@ -3704,7 +3704,7 @@
     edited="power2_Pow2real_Pow2_int_real_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.59"/>
+     <result status="valid" time="1.20"/>
    </proof>
   </goal>
  </theory>

--- a/examples/bresenham/why3session.xml
+++ b/examples/bresenham/why3session.xml
@@ -12,7 +12,7 @@
 <prover
  id="2"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="3"
  name="Z3"
@@ -42,7 +42,7 @@
     edited="bresenham_M_closest_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="3.38"/>
+     <result status="valid" time="4.20"/>
    </proof>
   </goal>
   <goal

--- a/examples/bts/12934/why3session.xml
+++ b/examples/bts/12934/why3session.xml
@@ -4,7 +4,7 @@
 <prover
  id="0"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <file
  name="../12934.why"
  verified="true"
@@ -30,7 +30,7 @@
     edited="12934_BTS12934_t_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.43"/>
+     <result status="valid" time="1.01"/>
    </proof>
   </goal>
  </theory>

--- a/examples/bts/13849/why3session.xml
+++ b/examples/bts/13849/why3session.xml
@@ -4,7 +4,7 @@
 <prover
  id="0"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <file
  name="../13849.why"
  verified="true"
@@ -30,7 +30,7 @@
     edited="13849_T_x_2.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.43"/>
+     <result status="valid" time="0.99"/>
    </proof>
   </goal>
  </theory>

--- a/examples/bts/13854/why3session.xml
+++ b/examples/bts/13854/why3session.xml
@@ -4,7 +4,7 @@
 <prover
  id="0"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <file
  name="../13854.why"
  verified="true"
@@ -30,7 +30,7 @@
     edited="13854_T_g_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.42"/>
+     <result status="valid" time="0.95"/>
    </proof>
   </goal>
   <goal
@@ -48,7 +48,7 @@
     edited="13854_T_x_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.43"/>
+     <result status="valid" time="0.96"/>
    </proof>
   </goal>
  </theory>

--- a/examples/counting_sort/why3session.xml
+++ b/examples/counting_sort/why3session.xml
@@ -20,7 +20,7 @@
 <prover
  id="4"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="5"
  name="Z3"
@@ -58,7 +58,7 @@
     edited="counting_sort_WP_Spec_eqlt_2.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.64"/>
+     <result status="valid" time="2.78"/>
    </proof>
   </goal>
  </theory>
@@ -860,7 +860,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="unknown" time="1.44"/>
+       <result status="unknown" time="1.83"/>
      </proof>
     </goal>
     <goal
@@ -1172,7 +1172,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.13"/>
+       <result status="valid" time="0.01"/>
      </proof>
     </goal>
     <goal
@@ -1476,7 +1476,7 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.33"/>
+         <result status="valid" time="0.10"/>
        </proof>
       </goal>
      </transf>
@@ -2850,7 +2850,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="2.39"/>
+       <result status="valid" time="2.77"/>
      </proof>
      <proof
       prover="7"
@@ -2898,7 +2898,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="timeout" time="5.96"/>
+       <result status="timeout" time="4.96"/>
      </proof>
      <proof
       prover="7"

--- a/examples/decrease1/why3session.xml
+++ b/examples/decrease1/why3session.xml
@@ -20,7 +20,7 @@
 <prover
  id="4"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="5"
  name="Z3"
@@ -58,7 +58,7 @@
     edited="decrease1_Decrease1_decrease1_induction_2.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.56"/>
+     <result status="valid" time="1.24"/>
    </proof>
   </goal>
   <goal

--- a/examples/dfa_example/why3session.xml
+++ b/examples/dfa_example/why3session.xml
@@ -12,7 +12,7 @@
 <prover
  id="2"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <file
  name="../dfa_example.mlw"
  verified="false"
@@ -38,7 +38,7 @@
     edited="dfa_example_DfaExample_nil_notin_r1_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.48"/>
+     <result status="valid" time="1.01"/>
    </proof>
   </goal>
   <goal

--- a/examples/dijkstra/why3session.xml
+++ b/examples/dijkstra/why3session.xml
@@ -20,7 +20,7 @@
 <prover
  id="4"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="5"
  name="Z3"
@@ -147,7 +147,7 @@
     edited="dijkstra_DijkstraShortestPath_Length_nonneg_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.48"/>
+     <result status="valid" time="1.07"/>
    </proof>
   </goal>
   <goal
@@ -182,7 +182,7 @@
     edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.73"/>
+     <result status="valid" time="1.34"/>
    </proof>
   </goal>
   <goal
@@ -217,7 +217,7 @@
     edited="dijkstra_DijkstraShortestPath_Completeness_lemma_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.61"/>
+     <result status="valid" time="1.30"/>
    </proof>
   </goal>
   <goal
@@ -1034,7 +1034,7 @@
       edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"
       obsolete="false"
       archived="false">
-       <result status="valid" time="2.28"/>
+       <result status="valid" time="3.11"/>
      </proof>
     </goal>
     <goal

--- a/examples/edit_distance/why3session.xml
+++ b/examples/edit_distance/why3session.xml
@@ -12,7 +12,7 @@
 <prover
  id="2"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.4pl2"/>
 <prover
  id="3"
  name="Z3"
@@ -46,7 +46,7 @@
     edited="edit_distance_Word_first_last_explicit_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="1.03"/>
    </proof>
   </goal>
   <goal
@@ -64,7 +64,7 @@
     edited="edit_distance_Word_first_last_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="1.06"/>
    </proof>
   </goal>
   <goal
@@ -82,7 +82,7 @@
     edited="edit_distance_Word_key_lemma_right_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.54"/>
+     <result status="valid" time="1.27"/>
    </proof>
   </goal>
   <goal
@@ -100,7 +100,7 @@
     edited="edit_distance_Word_dist_symetry_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.50"/>
+     <result status="valid" time="1.07"/>
    </proof>
   </goal>
   <goal
@@ -135,7 +135,7 @@
     edited="edit_distance_Word_dist_concat_left_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.50"/>
+     <result status="valid" time="1.05"/>
    </proof>
   </goal>
   <goal
@@ -170,7 +170,7 @@
     edited="edit_distance_Word_min_dist_equal_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.55"/>
+     <result status="valid" time="1.13"/>
    </proof>
   </goal>
   <goal
@@ -188,7 +188,7 @@
     edited="edit_distance_Word_min_dist_diff_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.54"/>
+     <result status="valid" time="1.13"/>
    </proof>
   </goal>
   <goal
@@ -206,7 +206,7 @@
     edited="edit_distance_Word_min_dist_eps_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="1.07"/>
    </proof>
   </goal>
   <goal
@@ -224,7 +224,7 @@
     edited="edit_distance_Word_min_dist_eps_length_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.53"/>
+     <result status="valid" time="1.08"/>
    </proof>
   </goal>
  </theory>
@@ -249,7 +249,7 @@
     edited="edit_distance_WP_EditDistance_suffix_length_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.56"/>
+     <result status="valid" time="1.16"/>
    </proof>
   </goal>
   <goal
@@ -1141,7 +1141,7 @@
       edited="edit_distance_EditDistance_WP_parameter_distance_1.v"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.96"/>
+       <result status="valid" time="1.59"/>
      </proof>
     </goal>
     <goal
@@ -1322,7 +1322,7 @@
       edited="edit_distance_WP_EditDistance_WP_parameter_distance_2.v"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.71"/>
+       <result status="valid" time="1.34"/>
      </proof>
     </goal>
     <goal
@@ -1443,7 +1443,7 @@
       edited="edit_distance_WP_EditDistance_WP_parameter_distance_1.v"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.93"/>
+       <result status="valid" time="1.44"/>
      </proof>
     </goal>
     <goal

--- a/examples/euler001/euler001_DivModHints_mod_succ_1_1.v
+++ b/examples/euler001/euler001_DivModHints_mod_succ_1_1.v
-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq 8.4 driver *)
 (* Beware! Only edit allowed sections below    *)
-Require Import ZArith.
-Require Import Rbase.
+Require Import BuiltIn.
 Require Import ZOdiv.
-Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
-  (x <= y)%Z).
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.

-Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <  y)%Z /\
-  ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ (r <  y)%Z))) ->
-  ((r = (ZOmod x y)) /\ (q = (ZOdiv x y))).
+Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
+  ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
+  (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).

-(* YOU MAY EDIT THE CONTEXT BELOW *)
 Open Scope Z_scope.
-(* DO NOT EDIT BELOW *)

-Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+(* Why3 goal *)
+Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
  ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
  ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)).
-(* YOU MAY EDIT THE PROOF BELOW *)
+(* Why3 intros x y (h1,h2) h3. *)
 intros x y (Hx,Hy) H.
 assert (h: y>0) by omega.
 generalize (ZO_div_mod_eq x y); intro h1.
 generalize (ZO_div_mod_eq (x+1) y); intro h2.
-assert (h3:x = y * ((x + 1) / y) + ((x + 1) mod y - 1)) by omega.
-generalize (mod_div_unique x y ((x + 1) / y) ((x + 1) mod y - 1)).
+assert (h3:x = y * (ZOdiv (x + 1) y) + (ZOmod (x + 1) y - 1)) by omega.
+generalize (mod_div_unique x y (ZOdiv (x + 1) y) (ZOmod (x + 1) y - 1)).
 intuition.
-destruct H1; auto with zarith.
+destruct H1 ; auto with zarith.
 rewrite h3 at 1.
 ring.
-assert (0 <= (x + 1) mod y < y).
-  apply ZOmod_lt_pos_pos; omega.
+assert (0 <= ZOmod (x + 1) y < y).
+  apply Zquot.Zrem_lt_pos_pos; omega.
 omega.
 Qed.
-(* DO NOT EDIT BELOW *)


--- a/examples/euler001/euler001_DivModHints_mod_succ_2_1.v
+++ b/examples/euler001/euler001_DivModHints_mod_succ_2_1.v
-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq 8.4 driver *)
 (* Beware! Only edit allowed sections below    *)
-Require Import ZArith.
-Require Import Rbase.
+Require Import BuiltIn.
 Require Import ZOdiv.
-Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%