diff --git a/examples/gcd.mlw b/examples/gcd.mlw
index b7209d5702fe707cfa15108972244b7de2c47223..2f37aa0f33fc28c417a84f05f653a205ab8b5f1d 100644
--- a/examples/gcd.mlw
+++ b/examples/gcd.mlw
@@ -56,6 +56,8 @@ module BinaryGcd
lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1
lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2
+ use number.Coprime
+
lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u ->
gcd (2 * u) (2 * v) = 2 * gcd u v
lemma gcd_even_odd: forall u v: int. 0 <= v -> 0 <= u ->
@@ -64,9 +66,11 @@ module BinaryGcd
even u -> odd v -> gcd u v = gcd (div u 2) v
lemma odd_odd_div2: forall u v: int. 0 <= v -> 0 <= u ->
div ((2*u+1) - (2*v+1)) 2 = u - v
- lemma gcd_odd_odd: forall u v: int. 0 <= v -> 0 <= u ->
+ lemma gcd_odd_odd_aux: forall u v: int. 0 <= v <= u ->
+ gcd (2 * u + 1) (2 * v + 1) = gcd ((2*u+1) - 1*(2*v+1)) (2 * v + 1)
+ lemma gcd_odd_odd: forall u v: int. 0 <= v <= u ->
gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1)
- lemma gcd_odd_odd2: forall u v: int. 0 <= v -> 0 <= u ->
+ lemma gcd_odd_odd2: forall u v: int. 0 <= v <= u ->
odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v
let rec binary_gcd (u v: int) : int
diff --git a/examples/gcd/gcd_BinaryGcd_gcd_even_odd_2.v b/examples/gcd/gcd_BinaryGcd_gcd_even_odd_2.v
new file mode 100644
index 0000000000000000000000000000000000000000..a1366ed8174817cad66fac6a1ddba12524fa0e64
--- /dev/null
+++ b/examples/gcd/gcd_BinaryGcd_gcd_even_odd_2.v
@@ -0,0 +1,58 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.EuclideanDivision.
+Require int.ComputerDivision.
+Require number.Parity.
+Require number.Divisibility.
+Require number.Gcd.
+Require number.Prime.
+Require number.Coprime.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
+(* Why3 assumption *)
+Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
+
+(* Why3 assumption *)
+Inductive lex: (Z* Z)%type -> (Z* Z)%type -> Prop :=
+ | Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1,
+ y1) (x2, y2))
+ | Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
+ y2)).
+
+Axiom even1 : forall (n:Z), (0%Z <= n)%Z -> ((number.Parity.even n) <->
+ (n = (2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z)).
+
+Axiom odd1 : forall (n:Z), (0%Z <= n)%Z -> ((~ (number.Parity.even n)) <->
+ (n = ((2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z + 1%Z)%Z)).
+
+Axiom div_nonneg : forall (n:Z), (0%Z <= n)%Z ->
+ (0%Z <= (ZArith.BinInt.Z.quot n 2%Z))%Z.
+
+Axiom gcd_even_even : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z ->
+ ((number.Gcd.gcd (2%Z * u)%Z (2%Z * v)%Z) = (2%Z * (number.Gcd.gcd u
+ v))%Z)).
+
+(* Why3 goal *)
+Theorem gcd_even_odd : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z ->
+ ((number.Gcd.gcd (2%Z * u)%Z ((2%Z * v)%Z + 1%Z)%Z) = (number.Gcd.gcd u
+ ((2%Z * v)%Z + 1%Z)%Z))).
+(* Why3 intros u v h1 h2. *)
+intros u v h1 h2.
+rewrite Gcd.Comm.
+rewrite number.Coprime.gcd_coprime.
+now rewrite Gcd.Comm.
+unfold Coprime.coprime.
+rewrite <- Gcd.Gcd_computer_mod; auto with zarith.
+rewrite ComputerDivision.Mod_mult; auto with zarith.
+Qed.
+
diff --git a/examples/gcd/why3session.xml b/examples/gcd/why3session.xml
index 732d2ee631c19eeffefb5ffd7d6564094db2a120..e6469aa17d06bbb12a0ec7ea90168273df2ba582 100644
--- a/examples/gcd/why3session.xml
+++ b/examples/gcd/why3session.xml
@@ -36,10 +36,14 @@
+
@@ -411,17 +415,26 @@
+
+
+
@@ -437,13 +450,13 @@
+
+
+
+
+
+ loclnum="71" loccnumb="8" loccnume="19"
+ sum="7d0f42fe2077e24ed0584c4a42509617"
+ proved="true"
+ expanded="false"
+ shape="ainfix =agcdainfix +ainfix *c2V0c1ainfix +ainfix *c2V1c1agcdainfix -V0V1ainfix +ainfix *c2V1c1Iainfix <=V1V0Aainfix <=c0V1F">
+
+
+
+
+
+
+
+
+
+ shape="ainfix =agcdV0V1agcdadivainfix -V0V1c2V1IaoddV1IaoddV0Iainfix <=V1V0Aainfix <=c0V1F">
@@ -495,9 +549,9 @@
@@ -523,9 +577,9 @@
@@ -551,9 +605,9 @@
@@ -579,9 +633,9 @@
@@ -607,9 +661,9 @@
@@ -623,21 +677,13 @@
archived="false">
-
-
-
@@ -663,9 +709,9 @@
@@ -685,15 +731,15 @@
memlimit="1000"
obsolete="false"
archived="false">
-
+
@@ -711,9 +757,9 @@
@@ -739,9 +785,9 @@
@@ -761,15 +807,15 @@
memlimit="1000"
obsolete="false"
archived="false">
-
+
@@ -789,15 +835,15 @@
memlimit="1000"
obsolete="false"
archived="false">
-
+
@@ -823,9 +869,9 @@
@@ -845,15 +891,15 @@
memlimit="1000"
obsolete="false"
archived="false">
-
+
@@ -879,9 +925,9 @@
@@ -909,15 +955,15 @@
memlimit="1000"
obsolete="false"
archived="false">
-
+
@@ -937,7 +983,7 @@
memlimit="1000"
obsolete="false"
archived="false">
-
+
diff --git a/examples/list_rev.mlw b/examples/in_progress/list_rev.mlw
similarity index 100%
rename from examples/list_rev.mlw
rename to examples/in_progress/list_rev.mlw
diff --git a/examples/list_rev/list_rev_M2_frame_list_1.v b/examples/in_progress/list_rev/list_rev_M2_frame_list_1.v
similarity index 100%
rename from examples/list_rev/list_rev_M2_frame_list_1.v
rename to examples/in_progress/list_rev/list_rev_M2_frame_list_1.v
diff --git a/examples/list_rev/list_rev_M2_frame_list_ft_1.v b/examples/in_progress/list_rev/list_rev_M2_frame_list_ft_1.v
similarity index 100%
rename from examples/list_rev/list_rev_M2_frame_list_ft_1.v
rename to examples/in_progress/list_rev/list_rev_M2_frame_list_ft_1.v
diff --git a/examples/list_rev/list_rev_M2_frame_model_1.v b/examples/in_progress/list_rev/list_rev_M2_frame_model_1.v
similarity index 100%
rename from examples/list_rev/list_rev_M2_frame_model_1.v
rename to examples/in_progress/list_rev/list_rev_M2_frame_model_1.v
diff --git a/examples/list_rev/why3session.xml b/examples/in_progress/list_rev/why3session.xml
similarity index 100%
rename from examples/list_rev/why3session.xml
rename to examples/in_progress/list_rev/why3session.xml
diff --git a/examples/tests-provers/alt-ergo-models.mlw b/examples/tests/alt-ergo-models.mlw
similarity index 100%
rename from examples/tests-provers/alt-ergo-models.mlw
rename to examples/tests/alt-ergo-models.mlw
diff --git a/examples/tests-provers/alt-ergo-models.why b/examples/tests/alt-ergo-models.why
similarity index 100%
rename from examples/tests-provers/alt-ergo-models.why
rename to examples/tests/alt-ergo-models.why
diff --git a/examples/tests-provers/alt-ergo-models/why3session.xml b/examples/tests/alt-ergo-models/why3session.xml
similarity index 100%
rename from examples/tests-provers/alt-ergo-models/why3session.xml
rename to examples/tests/alt-ergo-models/why3session.xml
diff --git a/lib/coq/number/Coprime.v b/lib/coq/number/Coprime.v
index f7b159078b087d2005538d52806061c3cbd0d174..a2e1c6e1049a675f8a8b54727a3ab7bb92968037 100644
--- a/lib/coq/number/Coprime.v
+++ b/lib/coq/number/Coprime.v
@@ -67,3 +67,21 @@ apply Znumtheory.prime_mult; auto.
now rewrite <- Prime.prime_is_Zprime.
Qed.
+(* Why3 goal *)
+Lemma gcd_coprime : forall (a:Z) (b:Z) (c:Z), (coprime a b) ->
+ ((number.Gcd.gcd a (b * c)%Z) = (number.Gcd.gcd a c)).
+intros a b c h1.
+apply Z.gcd_unique.
+- apply Z.gcd_nonneg.
+- apply Gcd.gcd_def1.
+- apply Divisibility.divides_multl.
+ apply Gcd.gcd_def2.
+- intros q h2 h3.
+ apply Gcd.gcd_def3.
+ trivial.
+ apply Gauss with b; split; auto.
+ rewrite coprime_is_Zrel_prime.
+ rewrite coprime_is_Zrel_prime in h1.
+ now apply Znumtheory.rel_prime_div with (2:=h2).
+Qed.
+
diff --git a/theories/number.why b/theories/number.why
index e270074e66c2c71949c6fee29792c80ce18ffabb..99466e95dcb70a465597b0ca0d3d3640aab22295 100644
--- a/theories/number.why
+++ b/theories/number.why
@@ -118,7 +118,6 @@ theory Gcd
clone algebra.AC with type t = int, function op = gcd,
lemma Comm.Comm, lemma Assoc
- (*** FIXME: Alt-Ergo proves gcd_0_pos even without gcd_unique *)
lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a
lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a
@@ -196,5 +195,7 @@ theory Coprime
forall p a b:int.
prime p /\ divides p (a*b) -> divides p a \/ divides p b
+ lemma gcd_coprime:
+ forall a b c. coprime a b -> gcd a (b*c) = gcd a c
end