tests de Romega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8832 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 392 insertions, 0 deletions

diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
new file mode 100644
index 000000000..20340c989
--- /dev/null
+++ b/test-suite/success/Omega0.v
@@ -0,0 +1,133 @@
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(* Pierre L: examples gathered while debugging romega. *)
+
+Lemma test_romega_1 : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_1b : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros z z1 z2.
+omega.
+Qed.
+
+Lemma test_romega_2 : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_2b : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros a b c.
+omega.
+Qed.
+
+Lemma test_romega_3 : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_3b : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros a b h hl hr ha hb.
+omega.
+Qed.
+
+
+Lemma test_romega_4 : forall hr ha, 
+ ha = 0 ->
+ (ha = 0 -> hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+omega.
+Qed.
+
+Lemma test_romega_5 : forall hr ha, 
+ ha = 0 ->
+ (~ha = 0 \/ hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+omega.
+Qed.
+
+Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros z.
+omega.
+Qed.
+
+Lemma test_romega_7 : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_7b : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+omega.
+Qed.
+
+(* Magaud #240 *)
+
+Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros x y.
+omega.
+Qed.
+
+
+
+
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
new file mode 100644
index 000000000..04b666edd
--- /dev/null
+++ b/test-suite/success/ROmega.v
@@ -0,0 +1,98 @@
+
+Require Import ZArith ROmega.
+
+(* Submitted by Xavier Urbain 18 Jan 2002 *)
+
+Lemma lem1 :
+ forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
+Proof.
+intros x y.
+ (*romega.*)
+Admitted.
+
+(* Proposed by Pierre Crégut *)
+
+Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
+intro.
+ romega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre *)
+
+Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
+Proof.
+intros.
+ (*romega.*)
+Admitted.
+
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* internal variable and a section variable (June 2001) *)
+
+Section A.
+Variable x y : Z.
+Hypothesis H : (x > y)%Z.
+Lemma lem4 : (x > y)%Z.
+ romega.
+Qed.
+End A.
+
+(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* May 2002 *)
+
+Section B.
+Variable R1 R2 S1 S2 H S : Z.
+Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z.
+Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z.
+Hypothesis K : (R1 >= 0)%Z -> R2 = R1.
+Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
+Hypothesis M : (H <= 2 * S)%Z.
+Hypothesis N : (S < H)%Z.
+Lemma lem5 : (H > 0)%Z.
+ romega.
+Qed.
+End B.
+
+(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+Lemma lem6 :
+ forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
+intros.
+ romega.
+Qed.
+
+(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
+Require Import Omega.
+Section C.
+Parameter g : forall m : nat, m <> 0 -> Prop.
+Parameter f : forall (m : nat) (H : m <> 0), g m H.
+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.
+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.
+
+(* 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.
+
+(* 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))).
+Proof.
+Intros; Omega.
+Qed.
+*)
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
new file mode 100644
index 000000000..2cb66fef1
--- /dev/null
+++ b/test-suite/success/ROmega0.v
@@ -0,0 +1,133 @@
+Require Import ZArith ROmega.
+Open Scope Z_scope.
+
+(* Pierre L: examples gathered while debugging romega. *)
+
+Lemma test_romega_1 : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_1b : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros z z1 z2.
+(* romega. *) 
+Admitted.
+
+Lemma test_romega_2 : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_2b : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros a b c.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_3 : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_3b : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros a b h hl hr ha hb.
+romega.
+Qed.
+
+
+Lemma test_romega_4 : forall hr ha, 
+ ha = 0 ->
+ (ha = 0 -> hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+romega.
+Qed.
+
+Lemma test_romega_5 : forall hr ha, 
+ ha = 0 ->
+ (~ha = 0 \/ hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+romega.
+Qed.
+
+Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros z.
+(*romega. *)
+Admitted.
+
+Lemma test_romega_7 : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_7b : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+(* Magaud #240 *)
+
+Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros x y.
+romega.
+Qed.
+
+
+
+
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
new file mode 100644
index 000000000..9d47c9f65
--- /dev/null
+++ b/test-suite/success/ROmega2.v
@@ -0,0 +1,28 @@
+Require Import ZArith ROmega.
+
+(* Submitted by Yegor Bryukhov (#922) *)
+
+Open Scope Z_scope.
+
+Lemma Test46 : 
+forall v1 v2 v3 v4 v5 : Z,
+((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
+9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
+((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 ->
+0 > 6 * v1 ->
+(0 * v3) + (6 * v2) <> 2 ->
+(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) ->
+7 * v3 > 5 * v5 ->
+0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) ->
+7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) ->
+0 * v3 > 7 * v1 ->
+9 * v2 < 9 * v5 ->
+(2 * v3) + (8 * v1) <= 5 * v4 ->
+5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) ->
+0 * v5 <= 9 * v2 ->
+((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
+-> False.
+intros.
+(*romega.*)
+Admitted.
+