aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_1362.v15
-rw-r--r--test-suite/bugs/closed/bug_1912.v4
-rw-r--r--test-suite/bugs/closed/bug_4132.v8
-rw-r--r--test-suite/bugs/closed/bug_4717.v8
-rw-r--r--test-suite/bugs/closed/bug_9512.v9
-rw-r--r--test-suite/bugs/opened/bug_1615.v11
-rw-r--r--test-suite/bugs/opened/bug_6602.v17
-rw-r--r--test-suite/interactive/ParalITP_smallproofs.v18
-rw-r--r--test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v33
-rw-r--r--test-suite/success/Abstract.v4
-rw-r--r--test-suite/success/Omega.v28
-rw-r--r--test-suite/success/Omega0.v34
-rw-r--r--test-suite/success/Omega2.v4
-rw-r--r--test-suite/success/OmegaPre.v43
-rw-r--r--test-suite/success/ProgramWf.v8
-rw-r--r--test-suite/success/ROmegaPre.v3
-rw-r--r--test-suite/success/fix.v8
-rw-r--r--test-suite/success/keyedrewrite.v2
-rw-r--r--test-suite/success/rewrite_iterated.v4
-rw-r--r--test-suite/success/search.v2
20 files changed, 109 insertions, 154 deletions
diff --git a/test-suite/bugs/closed/bug_1362.v b/test-suite/bugs/closed/bug_1362.v
index 6cafb9f0cd..18b8d743b3 100644
--- a/test-suite/bugs/closed/bug_1362.v
+++ b/test-suite/bugs/closed/bug_1362.v
@@ -1,26 +1,17 @@
(** Omega is now aware of the bodies of context variables
(of type Z or nat). *)
-Require Import ZArith Omega.
+Require Import ZArith Lia.
Open Scope Z.
Goal let x := 3 in x = 3.
intros.
-omega.
+lia.
Qed.
Open Scope nat.
Goal let x := 2 in x = 2.
intros.
-omega.
+lia.
Qed.
-
-(** NB: this could be disabled for compatibility reasons *)
-
-Unset Omega UseLocalDefs.
-
-Goal let x := 4 in x = 4.
-intros.
-Fail omega.
-Abort.
diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v
index 0228abbb9b..9f6c8177f6 100644
--- a/test-suite/bugs/closed/bug_1912.v
+++ b/test-suite/bugs/closed/bug_1912.v
@@ -1,6 +1,6 @@
-Require Import Omega.
+Require Import Lia ZArith.
Goal forall x, Z.succ (Z.pred x) = x.
intros x.
-omega.
+lia.
Qed.
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 67ecc3087f..2ebbb66758 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -1,5 +1,5 @@
-Require Import ZArith Omega.
+Require Import ZArith Lia.
Open Scope Z_scope.
(** bug 4132: omega was using "simpl" either on whole equations, or on
@@ -14,18 +14,18 @@ Lemma foo
(H : - zxy' <= zxy)
(H' : zxy' <= x') : - b <= zxy.
Proof.
-omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
Qed.
Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
this might have triggered "index out of bounds" in the past,
but I never managed to reproduce that in any version,
even before my fix. *)
Qed.
Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
this might have triggered "Failure(occurrence 2)" in the past,
but I never managed to reproduce that. *)
Qed.
diff --git a/test-suite/bugs/closed/bug_4717.v b/test-suite/bugs/closed/bug_4717.v
index bd9bac37ef..81bc70d076 100644
--- a/test-suite/bugs/closed/bug_4717.v
+++ b/test-suite/bugs/closed/bug_4717.v
@@ -1,6 +1,6 @@
(* Omega being smarter on recognizing nat and Z *)
-Require Import Omega.
+Require Import Lia ZArith.
Definition nat' := nat.
@@ -10,13 +10,13 @@ Theorem le_not_eq_lt : forall (n m:nat),
n < m.
Proof.
intros.
- omega.
+ lia.
Qed.
Goal forall (x n : nat'), x = x + n - n.
Proof.
intros.
- omega.
+ lia.
Qed.
Open Scope Z_scope.
@@ -29,5 +29,5 @@ Theorem Zle_not_eq_lt : forall n m,
n < m.
Proof.
intros.
- omega.
+ lia.
Qed.
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index bad9d64f65..f42e32cf25 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+Require Import Coq.ZArith.BinInt Coq.micromega.Lia.
Set Primitive Projections.
Record params := { width : Z }.
@@ -10,7 +10,6 @@ Set Printing All.
Lemma foo : width p = 0%Z -> width p = 0%Z.
intros.
- assert_succeeds (enough True; [omega|]).
assert_succeeds (enough True; [lia|]).
(* H : @eq Z (width p) Z0 *)
@@ -26,12 +25,6 @@ Lemma foo : width p = 0%Z -> width p = 0%Z.
(* @eq Z (width p) Z0 *)
assert_succeeds (enough True; [lia|]).
- (* Tactic failure: <tactic closure> fails. *)
- (* assert_succeeds (enough True; [omega|]). *)
- (* Tactic failure: <tactic closure> fails. *)
-
- (* omega. *)
- (* Error: Omega can't solve this system *)
lia.
(* Tactic failure: Cannot find witness. *)
diff --git a/test-suite/bugs/opened/bug_1615.v b/test-suite/bugs/opened/bug_1615.v
deleted file mode 100644
index c045335410..0000000000
--- a/test-suite/bugs/opened/bug_1615.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Require Import Omega.
-
-Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
-Proof.
- intros. omega.
-Qed.
-
-Lemma foo' : forall n m : nat, n <= n + n * m.
-Proof.
- intros. Fail omega.
-Abort.
diff --git a/test-suite/bugs/opened/bug_6602.v b/test-suite/bugs/opened/bug_6602.v
deleted file mode 100644
index 3690adf90a..0000000000
--- a/test-suite/bugs/opened/bug_6602.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Omega.
-
-Lemma test_nat:
- forall n, (5 + pred n <= 5 + n).
-Proof.
- intros.
- zify.
- omega.
-Qed.
-
-Lemma test_N:
- forall n, (5 + N.pred n <= 5 + n)%N.
-Proof.
- intros.
- zify.
- omega.
-Qed.
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index d2e6794c0b..1f4913b49d 100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
@@ -140,35 +140,35 @@ Qed.
Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0.
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n).
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
Proof.
- intros; omega.
+ intros; lia.
Qed.
Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
Proof.
- intros; omega.
+ intros; lia.
Qed.
Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n.
Proof.
intros.
- omega.
+ lia.
Qed.
@@ -1414,13 +1414,13 @@ Qed.
Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n.
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n.
Proof.
intros.
- omega.
+ lia.
Qed.
@@ -1501,7 +1501,7 @@ Proof.
[ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1));
[ idtac | apply f_equal with Z; auto with zarith ];
rewrite absolu_plus;
- [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega
+ [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; lia
| auto with zarith
| intro; discriminate ]
| rewrite <- H1; reflexivity ].
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 69ed621877..ae71ddfd1d 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -19,6 +19,7 @@
Require Export ZArith.
Require Export ZArithRing.
+Require Import Lia.
Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
@@ -140,35 +141,35 @@ Qed.
Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0.
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n).
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
Proof.
- intros; omega.
+ intros; lia.
Qed.
Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
Proof.
- intros; omega.
+ intros; lia.
Qed.
Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n.
Proof.
intros.
- omega.
+ lia.
Qed.
@@ -573,7 +574,7 @@ Qed.
-Hint Resolve Zmult_pos_pos Zmult_neg_neg Zmult_neg_pos Zmult_pos_neg: zarith.
+Local Hint Resolve Zmult_pos_pos Zmult_neg_neg Zmult_neg_pos Zmult_pos_neg: zarith.
Lemma Zle_reg_mult_l :
@@ -1158,7 +1159,7 @@ Proof.
intros [| p| p]; intros; [ Falsum | constructor | constructor ].
Qed.
-Hint Resolve square_pos: zarith.
+Local Hint Resolve square_pos: zarith.
(*###########################################################################*)
(** Properties of positive numbers, mapping between Z and nat *)
@@ -1414,13 +1415,13 @@ Qed.
Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n.
Proof.
intros.
- omega.
+ lia.
Qed.
Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n.
Proof.
intros.
- omega.
+ lia.
Qed.
@@ -1501,7 +1502,7 @@ Proof.
[ replace (Z.abs_nat x) with (Z.abs_nat (x - 1 + 1));
[ idtac | apply f_equal with Z; auto with zarith ];
rewrite absolu_plus;
- [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; omega
+ [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; lia
| auto with zarith
| intro; discriminate ]
| rewrite <- H1; reflexivity ].
@@ -1985,7 +1986,7 @@ Proof.
intros [| p| p] Hp; trivial.
Qed.
-Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8
+Local Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8
Zsgn_9 Zsgn_10 Zsgn_11 Zsgn_12 Zsgn_13 Zsgn_14 Zsgn_15 Zsgn_16 Zsgn_17
Zsgn_18 Zsgn_19 Zsgn_20 Zsgn_21 Zsgn_22 Zsgn_23 Zsgn_24 Zsgn_25 Zsgn_26
Zsgn_27: zarith.
@@ -2388,7 +2389,7 @@ Proof.
intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos.
Qed.
-Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9
+Local Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9
Zabs_10 Zabs_11 Zabs_12 Zabs_min Zabs_neg Zabs_mult Zabs_plus Zle_Zabs: zarith.
@@ -2949,7 +2950,7 @@ Proof.
ring.
Qed.
-Hint Resolve ZmaxSS Zle_max_r Zle_max_l Zmax_n_n: zarith.
+Local Hint Resolve ZmaxSS Zle_max_r Zle_max_l Zmax_n_n: zarith.
(*###########################################################################*)
(** Properties of Arity *)
@@ -3020,7 +3021,7 @@ Proof.
Flip.
Qed.
-Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith.
+Local Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith.
(*###########################################################################*)
(** Properties of Zpower *)
@@ -3038,4 +3039,4 @@ Proof.
ring.
Qed.
-Hint Resolve Zpower_1 Zpower_2: zarith.
+Local Hint Resolve Zpower_1 Zpower_2: zarith.
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index d52a853aae..24634bd321 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,6 +1,6 @@
(* Cf BZ#546 *)
-Require Import Omega.
+Require Import Lia.
Section S.
@@ -19,7 +19,7 @@ induction n.
replace (2 * S n0) with (2*n0 + 2) ; auto with arith.
apply DummyApp.
2:exact Dummy2.
- apply IHn0 ; abstract omega.
+ apply IHn0 ; abstract lia.
Defined.
End S.
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 5e0f90d59b..bbdf9762a3 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -1,5 +1,5 @@
-Require Import Omega.
+Require Import Lia ZArith.
(* Submitted by Xavier Urbain 18 Jan 2002 *)
@@ -7,14 +7,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 +22,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 +32,7 @@ Section A.
Variable x y : Z.
Hypothesis H : (x > y)%Z.
Lemma lem4 : (x > y)%Z.
- omega.
+ lia.
Qed.
End A.
@@ -48,7 +48,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 +56,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 +68,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 +90,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.
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.
diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v
index 4e726335c9..b2eef5bcd5 100644
--- a/test-suite/success/Omega2.v
+++ b/test-suite/success/Omega2.v
@@ -1,4 +1,4 @@
-Require Import ZArith Omega.
+Require Import ZArith Lia.
(* Submitted by Yegor Bryukhov (BZ#922) *)
@@ -23,6 +23,6 @@ forall v1 v2 v3 v4 v5 : Z,
((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
-> False.
intros.
-omega.
+lia.
Qed.
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index 0223255067..32bc99621a 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -1,4 +1,4 @@
-Require Import ZArith Nnat Omega.
+Require Import ZArith Nnat Lia.
Open Scope Z_scope.
(** Test of the zify preprocessor for (R)Omega *)
@@ -16,112 +16,111 @@ Open Scope Z_scope.
Goal forall a:Z, Z.max a a = a.
intros.
-zify; omega.
+lia.
Qed.
Goal forall a b:Z, Z.max a b = Z.max b a.
intros.
-zify; omega.
+lia.
Qed.
Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
intros.
-zify; omega.
+lia.
Qed.
Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
intros.
-zify; omega.
+lia.
Qed.
Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
intros.
-zify.
-intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *)
+intuition; subst; lia.
Qed.
Goal forall a:Z, Z.abs a = a -> a >= 0.
intros.
-zify; omega.
+lia.
Qed.
Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
intros.
-zify; omega.
+lia.
Qed.
(* zify_nat *)
Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
intros.
-zify; omega.
+lia.
Qed.
(* 2000 instead of 200: works, but quite slow *)
Goal forall m: nat, (m*m>=0)%nat.
intros.
-zify; omega.
+lia.
Qed.
(* zify_positive *)
Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m: positive, (m*m>=1)%positive.
intros.
-zify; omega.
+lia.
Qed.
(* zify_N *)
Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m:N, (m<1)%N -> (m=0)%N.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
intros.
-zify; omega.
+lia.
Qed.
Goal forall m:N, (m*m>=0)%N.
intros.
-zify; omega.
+lia.
Qed.
(* mix of datatypes *)
Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
intros.
-zify; omega.
+lia.
Qed.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 02adb012d9..ef8617cd9e 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -85,19 +85,19 @@ Time Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat)
error
end.
-Require Import Omega Setoid.
+Require Import Lia Setoid.
Next Obligation.
intros ; simpl in *. apply H.
- simpl in * ; omega.
+ simpl in * ; lia.
Qed.
Next Obligation. simpl in *; intros.
revert H0 ; clear_subset_proofs. intros.
- case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst.
+ case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by lia. subst.
revert H0 ; clear_subset_proofs ; tauto.
- apply H. simpl. omega.
+ apply H. simpl. lia.
Qed.
Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p})
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index 6ca32f450f..c0e86b00dd 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -32,8 +32,7 @@ Qed.
Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
intros.
-zify.
-intuition; subst; lia. (* pure multiplication: omega alone can't do it *)
+intuition; subst; lia.
Qed.
Goal forall a:Z, Z.abs a = a -> a >= 0.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index ff34840d83..b7d5276bc8 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -61,7 +61,7 @@ Qed.
(* Check mutually inductive statements *)
-Require Import ZArith_base Omega.
+Require Import ZArith_base Lia.
Open Scope Z_scope.
Inductive even: Z -> Prop :=
@@ -75,13 +75,13 @@ with odd_pos_even_pos : forall n, odd n -> n >= 1.
Proof.
intros.
destruct H.
- omega.
+ lia.
apply odd_pos_even_pos in H.
- omega.
+ lia.
intros.
destruct H.
apply even_pos_odd_pos in H.
- omega.
+ lia.
Qed.
CoInductive a : Prop := acons : b -> a
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index 5638a7d3eb..06847f4f96 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -23,7 +23,7 @@ Qed.
Print Equivalent Keys.
End foo.
-Require Import Arith List Omega.
+Require Import Arith List.
Definition G {A} (f : A -> A -> A) (x : A) := f x x.
diff --git a/test-suite/success/rewrite_iterated.v b/test-suite/success/rewrite_iterated.v
index 962dada35a..946011e393 100644
--- a/test-suite/success/rewrite_iterated.v
+++ b/test-suite/success/rewrite_iterated.v
@@ -1,8 +1,8 @@
-Require Import Arith Omega.
+Require Import Arith Lia.
Lemma test : forall p:nat, p<>0 -> p-1+1=p.
Proof.
- intros; omega.
+ intros; lia.
Qed.
(** Test of new syntax for rewrite : ! ? and so on... *)
diff --git a/test-suite/success/search.v b/test-suite/success/search.v
index 92de43e052..627e109d5f 100644
--- a/test-suite/success/search.v
+++ b/test-suite/success/search.v
@@ -32,4 +32,4 @@ Require Import ZArith.
Search Z.mul Z.add "distr".
Search "+"%Z "*"%Z "distr" -positive -Prop.
-Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
+Search (?x * _ + ?x * _)%Z outside Lia.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:13:38 +0000