diff options
Diffstat (limited to 'test-suite/success/Omega0.v')
| -rw-r--r-- | test-suite/success/Omega0.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index 6fd936935c..6ce7264b7a 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -1,4 +1,4 @@ -Require Import ZArith Omega. +Require Import ZArith Lia. Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) @@ -8,7 +8,7 @@ Lemma test_romega_0 : 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. -omega. +lia. Qed. Lemma test_romega_0b : @@ -16,7 +16,7 @@ Lemma test_romega_0b : 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. -omega. +lia. Qed. Lemma test_romega_1 : @@ -29,7 +29,7 @@ Lemma test_romega_1 : z >= 0. Proof. intros. -omega. +lia. Qed. Lemma test_romega_1b : @@ -42,21 +42,21 @@ Lemma test_romega_1b : z >= 0. Proof. intros z z1 z2. -omega. +lia. Qed. Lemma test_romega_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. -omega. +lia. 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. +lia. Qed. Lemma test_romega_3 : forall a b h hl hr ha hb, @@ -70,7 +70,7 @@ Lemma test_romega_3 : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros. -omega. +lia. Qed. Lemma test_romega_3b : forall a b h hl hr ha hb, @@ -84,7 +84,7 @@ Lemma test_romega_3b : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros a b h hl hr ha hb. -omega. +lia. Qed. @@ -94,7 +94,7 @@ Lemma test_romega_4 : forall hr ha, hr = 0. Proof. intros hr ha. -omega. +lia. Qed. Lemma test_romega_5 : forall hr ha, @@ -103,45 +103,45 @@ Lemma test_romega_5 : forall hr ha, hr = 0. Proof. intros hr ha. -omega. +lia. Qed. Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False. Proof. intros. -omega. +lia. Qed. Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False. Proof. intros z. -omega. +lia. Qed. Lemma test_romega_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -omega. +lia. Qed. Lemma test_romega_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -omega. +lia. Qed. (* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros. -omega. +lia. Qed. Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros x y. -omega. +lia. Qed. |