4 files changed, 269 insertions, 19 deletions

diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 2d29a8356b..ecbf04e412 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -10,14 +10,14 @@ intros x y.
  omega.
 Qed.
 
-(* Proposed by Pierre Crégut *)
+(* Proposed by Pierre Crégut *)
 
 Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
 intro.
  omega.
 Qed.
 
-(* Proposed by Jean-Christophe Filliâtre *)
+(* Proposed by Jean-Christophe Filliâtre *)
 
 Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
@@ -25,7 +25,7 @@ intros.
  omega.
 Qed.
 
-(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
 (* internal variable and a section variable (June 2001) *)
 
 Section A.
@@ -87,10 +87,8 @@ Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
 (* Submitted by Hubert Thierry (bug #743) *)
-(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
-Require Omega.
-Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
+Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
 Proof.
-Intros; Omega.
+intros; omega with *.
 Qed.
-*)
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
new file mode 100644
index 0000000000..bb800b7a01
--- /dev/null
+++ b/test-suite/success/OmegaPre.v
@@ -0,0 +1,127 @@
+Require Import ZArith Nnat Omega.
+Open Scope Z_scope.
+
+(** Test of the zify preprocessor for (R)Omega *)
+
+(* More details in file PreOmega.v
+ 
+   (r)omega with Z        : starts with zify_op
+   (r)omega with nat      : starts with zify_nat
+   (r)omega with positive : starts with zify_positive
+   (r)omega with N        : starts with uses zify_N
+   (r)omega with *        : starts zify (a saturation of the others)
+*)
+
+(* zify_op *)
+
+Goal forall a:Z, Zmax a a = a.
+intros.
+omega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b = Zmax b a.
+intros.
+omega with *.
+Qed.
+
+Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+intros.
+omega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+intros.
+omega with *.
+Qed.
+
+Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+intros.
+zify.
+intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
+Qed.
+
+Goal forall a:Z, Zabs a = a -> a >= 0.
+intros.
+omega with *.
+Qed.
+
+Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+intros.
+omega with *.
+Qed.
+
+(* zify_nat *)
+
+Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
+intros.
+omega with *.
+Qed.
+
+Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
+intros.
+omega with *.
+Qed.
+(* 2000 instead of 200: works, but quite slow *)
+
+Goal forall m: nat, (m*m>=0)%nat.
+intros.
+omega with *.
+Qed.
+
+(* zify_positive *)
+
+Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
+intros.
+omega with *.
+Qed.
+
+Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
+intros.
+omega with *.
+Qed.
+
+Goal forall m: positive, (m*m>=1)%positive.
+intros.
+omega with *.
+Qed.
+
+(* zify_N *)
+
+Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:N, (m<1)%N -> (m=0)%N.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:N, (m*m>=0)%N.
+intros.
+omega with *.
+Qed.
+
+(* mix of datatypes *)
+
+Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+intros.
+omega with *.
+Qed.
+
+
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index ff1f57df32..0c37c59aca 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -68,31 +68,29 @@ Variable n : nat.
 Variable ap_n : n <> 0.
 Let delta := f n ap_n.
 Lemma lem7 : n = n.
- (*romega. ---> ROMEGA CANT DEAL WITH NAT*)
-Admitted.
+ romega with nat.
+Qed.
 End C.
 
 (* Problem of dependencies *)
 Require Import Omega.
 Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
 intros.
-(* romega. ---> ROMEGA CANT DEAL WITH NAT*)
-Admitted.
+romega with nat.
+Qed.
 
 (* Bug that what caused by the use of intro_using in Omega *)
 Require Import Omega.
 Lemma lem9 :
  forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
 intros.
-(* romega. ---> ROMEGA CANT DEAL WITH NAT*) 
-Admitted.
+romega with nat.
+Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
 (* Submitted by Hubert Thierry (bug #743) *)
-(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
-Require Omega.
-Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
+Lemma lem10 : forall n m : nat, le n (plus n (mult n m)).
 Proof.
-Intros; Omega.
+intros; romega with nat.
 Qed.
-*)
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
new file mode 100644
index 0000000000..550edca507
--- /dev/null
+++ b/test-suite/success/ROmegaPre.v
@@ -0,0 +1,127 @@
+Require Import ZArith Nnat ROmega.
+Open Scope Z_scope.
+
+(** Test of the zify preprocessor for (R)Omega *)
+
+(* More details in file PreOmega.v
+ 
+   (r)omega with Z        : starts with zify_op
+   (r)omega with nat      : starts with zify_nat
+   (r)omega with positive : starts with zify_positive
+   (r)omega with N        : starts with uses zify_N
+   (r)omega with *        : starts zify (a saturation of the others)
+*)
+
+(* zify_op *)
+
+Goal forall a:Z, Zmax a a = a.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b = Zmax b a.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+intros.
+romega with *.
+Qed.
+
+Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+intros.
+zify.
+intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
+Qed.
+
+Goal forall a:Z, Zabs a = a -> a >= 0.
+intros.
+romega with *.
+Qed.
+
+Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+intros.
+romega with *.
+Qed.
+
+(* zify_nat *)
+
+Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
+intros.
+romega with *.
+Qed.
+(* 2000 instead of 200: works, but quite slow *)
+
+Goal forall m: nat, (m*m>=0)%nat.
+intros.
+romega with *.
+Qed.
+
+(* zify_positive *)
+
+Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: positive, (m*m>=1)%positive.
+intros.
+romega with *.
+Qed.
+
+(* zify_N *)
+
+Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m<1)%N -> (m=0)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m*m>=0)%N.
+intros.
+romega with *.
+Qed.
+
+(* mix of datatypes *)
+
+Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+intros.
+romega with *.
+Qed.
+
+