aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Abstract.v4
-rw-r--r--test-suite/success/Omega.v29
-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/RemoteUnivs.v31
-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
12 files changed, 100 insertions, 72 deletions
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..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.
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/RemoteUnivs.v b/test-suite/success/RemoteUnivs.v
new file mode 100644
index 0000000000..5ab4937dda
--- /dev/null
+++ b/test-suite/success/RemoteUnivs.v
@@ -0,0 +1,31 @@
+
+
+Goal Type * Type.
+Proof.
+ split.
+ par: exact Type.
+Qed.
+
+Goal Type.
+Proof.
+ exact Type.
+Qed.
+
+(* (* coqide test, note the delegated proofs seem to get an empty dirpath?
+ or I got confused because I had lemma foo in file foo
+ *)
+Definition U := Type.
+
+Lemma foo : U.
+Proof.
+ exact Type.
+Qed.
+
+
+Lemma foo1 : Type.
+Proof.
+ exact (U:Type).
+Qed.
+
+Print foo.
+*)
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-05-05 06:31:23 +0000