diff options
Diffstat (limited to 'test-suite/success/Omega.v')
| -rw-r--r-- | test-suite/success/Omega.v | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 5e0f90d59b..a530c34297 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,5 +1,4 @@ - -Require Import Omega. +Require Import Lia ZArith. (* Submitted by Xavier Urbain 18 Jan 2002 *) @@ -7,14 +6,14 @@ Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. - omega. + lia. Qed. (* Proposed by Pierre Crégut *) Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. intro. - omega. + lia. Qed. (* Proposed by Jean-Christophe Filliâtre *) @@ -22,7 +21,7 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. - omega. + lia. Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) @@ -32,7 +31,7 @@ Section A. Variable x y : Z. Hypothesis H : (x > y)%Z. Lemma lem4 : (x > y)%Z. - omega. + lia. Qed. End A. @@ -48,7 +47,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1. Hypothesis M : (H <= 2 * S)%Z. Hypothesis N : (S < H)%Z. Lemma lem5 : (H > 0)%Z. - omega. + lia. Qed. End B. @@ -56,11 +55,11 @@ End B. Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. - omega. + lia. Qed. (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) -Require Import Omega. +Require Import Lia. Section C. Parameter g : forall m : nat, m <> 0 -> Prop. Parameter f : forall (m : nat) (H : m <> 0), g m H. @@ -68,21 +67,21 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - omega. + lia. Qed. End C. (* Problem of dependencies *) -Require Import Omega. +Require Import Lia. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. -intros; omega. +intros; lia. Qed. (* Bug that what caused by the use of intro_using in Omega *) -Require Import Omega. +Require Import Lia. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. -intros; omega. +intros; lia. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) @@ -90,5 +89,5 @@ Qed. (* 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; zify; omega. +intros; lia. Qed. |