update proofs for gcd and gcd_bezout

examples/programs/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v

@@ -20,7 +20,7 @@ Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z).
 
 Axiom divides_refl : forall (n:Z), (divides n n).
 
-Axiom divides_1 : forall (n:Z), (divides 1%Z n).
+Axiom divides_1_n : forall (n:Z), (divides 1%Z n).
 
 Axiom divides_0 : forall (n:Z), (divides n 0%Z).
 
@@ -56,8 +56,8 @@ Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z).
 
 Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z).
 
-Axiom divides1 : forall (x:Z), (divides x 1%Z) -> ((x = 1%Z) \/
-  (x = (-1%Z)%Z)).
+Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/
+  (n = (-1%Z)%Z)).
 
 Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b
   a) -> ((a = b) \/ (a = (-b)%Z))).
@@ -83,33 +83,11 @@ Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
 
 Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x).
 
-Axiom mod_divides : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
+Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
   (((Zmod a b) = 0%Z) -> (divides b a)).
 
-Axiom divides_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) ->
-  ((Zmod a b) = 0%Z)).
-
-Parameter gcd: Z -> Z  -> Z.
-
-
-Axiom gcd_nonneg : forall (a:Z) (b:Z), (0%Z <= (gcd a b))%Z.
-
-Axiom gcd_def1 : forall (a:Z) (b:Z), (divides (gcd a b) a).
-
-Axiom gcd_def2 : forall (a:Z) (b:Z), (divides (gcd a b) b).
-
-Axiom gcd_def3 : forall (a:Z) (b:Z) (x:Z), (divides x a) -> ((divides x b) ->
-  (divides x (gcd a b))).
-
-Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((gcd (gcd x y) z) = (gcd x (gcd y
-  z))).
-
-Axiom Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)).
-
-Axiom gcd_0 : forall (a:Z), ((gcd a 0%Z) = a).
-
-Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a
-  (b - (q * a)%Z)%Z)).
+Axiom divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
+  ((divides b a) -> ((Zmod a b) = 0%Z)).
 
 Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
   (x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
@@ -151,16 +129,84 @@ Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z <  x)%Z /\ ((0%Z <= y)%Z /\
 Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z <  x)%Z /\ ((0%Z <= y)%Z /\
   (0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
 
+Axiom mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
+  (((ZOmod a b) = 0%Z) -> (divides b a)).
+
+Axiom divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b
+  a) -> ((ZOmod a b) = 0%Z)).
+
+Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
+
+Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z).
+
+Axiom even_or_odd : forall (n:Z), (even n) \/ (odd n).
+
+Axiom even_not_odd : forall (n:Z), (even n) -> ~ (odd n).
+
+Axiom odd_not_even : forall (n:Z), (odd n) -> ~ (even n).
+
+Axiom even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z).
+
+Axiom odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z).
+
+Axiom even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z).
+
+Axiom odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z).
+
+Axiom even_2k : forall (k:Z), (even (2%Z * k)%Z).
+
+Axiom odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z).
+
+Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a).
+
+Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a).
+
+Parameter gcd: Z -> Z  -> Z.
+
+
+Axiom gcd_nonneg : forall (a:Z) (b:Z), (0%Z <= (gcd a b))%Z.
+
+Axiom gcd_def1 : forall (a:Z) (b:Z), (divides (gcd a b) a).
+
+Axiom gcd_def2 : forall (a:Z) (b:Z), (divides (gcd a b) b).
+
+Axiom gcd_def3 : forall (a:Z) (b:Z) (x:Z), (divides x a) -> ((divides x b) ->
+  (divides x (gcd a b))).
+
+Axiom gcd_unique : forall (a:Z) (b:Z) (d:Z), (0%Z <= d)%Z -> ((divides d
+  a) -> ((divides d b) -> ((forall (x:Z), (divides x a) -> ((divides x b) ->
+  (divides x d))) -> (d = (gcd a b))))).
+
+Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((gcd (gcd x y) z) = (gcd x (gcd y
+  z))).
+
+Axiom Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)).
+
+Axiom gcd_0_pos : forall (a:Z), (0%Z <= a)%Z -> ((gcd a 0%Z) = a).
+
+Axiom gcd_0_neg : forall (a:Z), (a <  0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z).
+
+Axiom gcd_opp : forall (a:Z) (b:Z), ((gcd a b) = (gcd (-a)%Z b)).
+
+Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a
+  (b - (q * a)%Z)%Z)).
+
 Axiom Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a
   (ZOmod a b)) = (gcd a b)).
 
 Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a
   (Zmod a b)) = (gcd a b)).
 
+Axiom gcd_mult : forall (a:Z) (b:Z) (c:Z), (0%Z <= c)%Z -> ((gcd (c * a)%Z
+  (c * b)%Z) = (c * (gcd a b))%Z).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
 Theorem WP_parameter_gcd : forall (u:Z), forall (v:Z), ((0%Z <= u)%Z /\
-  (0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> ((((0%Z <= v)%Z /\
-  ((ZOmod u v) <  v)%Z) /\ ((0%Z <= v)%Z /\ (0%Z <= (ZOmod u v))%Z)) ->
-  ((gcd v (ZOmod u v)) = (gcd u v)))).
+  (0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> (((0%Z <= v)%Z /\
+  ((ZOmod u v) <  v)%Z) /\ ((0%Z <= v)%Z /\ (0%Z <= (ZOmod u v))%Z))).
 (* YOU MAY EDIT THE PROOF BELOW *)
 intuition.
 symmetry.

examples/programs/gcd/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/gcd/why3session.xml">
+ <prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
+ <prover id="coq" name="Coq" version="8.3pl2"/>
+ <prover id="cvc3" name="CVC3" version="2.2"/>
+ <prover id="eprover" name="Eprover" version="0.8 Steinthal"/>
+ <prover id="gappa" name="Gappa" version="0.15.0"/>
+ <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="yices" name="Yices" version="1.0.27"/>
+ <prover id="z3" name="Z3" version="2.19"/>
  <file name="../gcd.mlw" verified="true" expanded="true">
   <theory name="WP EuclideanAlgorithm" verified="true" expanded="true">
-   <goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="a484c5193a5cd03b14a4f295d1e1f03e" proved="true" expanded="true">
+   <goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="766d5a2cc24a5fd8ece90420c2f75c1f" proved="true" expanded="true" shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0FF">
     <transf name="split_goal" proved="true" expanded="true">
-     <goal name="WP_parameter gcd.1" expl="normal postcondition" sum="5a586460df7b95622e77fbef9bf3b5c9" proved="true" expanded="true">
-      <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
-      </proof>
+     <goal name="WP_parameter gcd.1" expl="normal postcondition" sum="4465e9890b7776b88f461cfd07f6534a" proved="true" expanded="true" shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0FF">
       <proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
-      </proof>
-      <proof prover="simplify" timelimit="2" edited="" obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="z3" timelimit="2" edited="" obsolete="false">
-       <result status="valid" time="0.04"/>
-      </proof>
      </goal>
-     <goal name="WP_parameter gcd.2" expl="precondition" sum="b712e1e03f97fab825d3144c19e74e4b" proved="true" expanded="true">
-      <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
-      </proof>
-      <proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
+     <goal name="WP_parameter gcd.2" expl="precondition" sum="4f12dd81ef67923c17562cf06453d85e" proved="true" expanded="true" shape="ainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
+      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
        <result status="valid" time="0.06"/>
       </proof>
-      <proof prover="simplify" timelimit="2" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
-      </proof>
-      <proof prover="z3" timelimit="2" edited="" obsolete="false">
-       <result status="valid" time="0.04"/>
-      </proof>
      </goal>
-     <goal name="WP_parameter gcd.3" expl="normal postcondition" sum="c6bdc24bc2e3c5380662a3fe96194dd7" proved="true" expanded="true">
+     <goal name="WP_parameter gcd.3" expl="normal postcondition" sum="9d5b42228b6e27b8f3654513a09c01d0" proved="true" expanded="true" shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
       <proof prover="coq" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v" obsolete="false">
-       <result status="valid" time="0.68"/>
+       <result status="valid" time="0.62"/>
       </proof>
      </goal>
     </transf>

examples/programs/gcd_bezout/gcd_bezout_WP_M_WP_parameter_gcd_1.v → examples/programs/gcd_bezout/gcd_bezout_WP_GcdBezout_WP_parameter_gcd_1.v

@@ -62,7 +62,7 @@ Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z).
 
 Axiom divides_refl : forall (n:Z), (divides n n).
 
-Axiom divides_1 : forall (n:Z), (divides 1%Z n).
+Axiom divides_1_n : forall (n:Z), (divides 1%Z n).
 
 Axiom divides_0 : forall (n:Z), (divides n 0%Z).
 
@@ -98,8 +98,8 @@ Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z).
 
 Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z).
 
-Axiom divides1 : forall (x:Z), (divides x 1%Z) -> ((x = 1%Z) \/
-  (x = (-1%Z)%Z)).
+Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/
+  (n = (-1%Z)%Z)).
 
 Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b
   a) -> ((a = b) \/ (a = (-b)%Z))).
@@ -123,11 +123,43 @@ Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
 
 Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x).
 
-Axiom mod_divides : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
+Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
   (((Zmod a b) = 0%Z) -> (divides b a)).
 
-Axiom divides_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) ->
-  ((Zmod a b) = 0%Z)).
+Axiom divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
+  ((divides b a) -> ((Zmod a b) = 0%Z)).
+
+Axiom mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
+  (((ZOmod a b) = 0%Z) -> (divides b a)).
+
+Axiom divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b
+  a) -> ((ZOmod a b) = 0%Z)).
+
+Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
+
+Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z).
+
+Axiom even_or_odd : forall (n:Z), (even n) \/ (odd n).
+
+Axiom even_not_odd : forall (n:Z), (even n) -> ~ (odd n).
+
+Axiom odd_not_even : forall (n:Z), (odd n) -> ~ (even n).
+
+Axiom even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z).
+
+Axiom odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z).
+
+Axiom even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z).
+
+Axiom odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z).
+
+Axiom even_2k : forall (k:Z), (even (2%Z * k)%Z).
+
+Axiom odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z).
+
+Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a).
+
+Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a).
 
 Parameter gcd: Z -> Z  -> Z.
 
@@ -141,12 +173,20 @@ Axiom gcd_def2 : forall (a:Z) (b:Z), (divides (gcd a b) b).
 Axiom gcd_def3 : forall (a:Z) (b:Z) (x:Z), (divides x a) -> ((divides x b) ->
   (divides x (gcd a b))).
 
+Axiom gcd_unique : forall (a:Z) (b:Z) (d:Z), (0%Z <= d)%Z -> ((divides d
+  a) -> ((divides d b) -> ((forall (x:Z), (divides x a) -> ((divides x b) ->
+  (divides x d))) -> (d = (gcd a b))))).
+
 Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((gcd (gcd x y) z) = (gcd x (gcd y
   z))).
 
 Axiom Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)).
 
-Axiom gcd_0 : forall (a:Z), ((gcd a 0%Z) = a).
+Axiom gcd_0_pos : forall (a:Z), (0%Z <= a)%Z -> ((gcd a 0%Z) = a).
+
+Axiom gcd_0_neg : forall (a:Z), (a <  0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z).
+
+Axiom gcd_opp : forall (a:Z) (b:Z), ((gcd a b) = (gcd (-a)%Z b)).
 
 Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a
   (b - (q * a)%Z)%Z)).
@@ -157,6 +197,9 @@ Axiom Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a
 Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a
   (Zmod a b)) = (gcd a b)).
 
+Axiom gcd_mult : forall (a:Z) (b:Z) (c:Z), (0%Z <= c)%Z -> ((gcd (c * a)%Z
+  (c * b)%Z) = (c * (gcd a b))%Z).
+
 Inductive ref (a:Type) :=
   | mk_ref : a -> ref a.
 Implicit Arguments mk_ref.
@@ -167,6 +210,10 @@ Definition contents (a:Type)(u:(ref a)): a :=
   end.
 Implicit Arguments contents.
 
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
 Theorem WP_parameter_gcd : forall (x:Z), forall (y:Z), ((0%Z <= x)%Z /\
   (0%Z <= y)%Z) -> forall (d:Z), forall (c:Z), forall (b:Z), forall (a:Z),
   forall (y1:Z), forall (x1:Z), ((0%Z <= x1)%Z /\ ((0%Z <= y1)%Z /\ (((gcd x1