aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_12806.v9
-rw-r--r--test-suite/micromega/bug_11656.v11
-rw-r--r--test-suite/micromega/bug_12184.v8
-rw-r--r--test-suite/micromega/bug_14054.v46
-rw-r--r--test-suite/micromega/example.v6
-rw-r--r--test-suite/micromega/example_nia.v35
-rwxr-xr-xtest-suite/misc/vio_checking.sh32
-rw-r--r--test-suite/misc/vio_checking.v9
-rw-r--r--test-suite/misc/vio_checking_bad.v4
-rw-r--r--test-suite/success/Omega.v1
-rw-r--r--test-suite/success/RemoteUnivs.v31
-rw-r--r--test-suite/vio/univ_constraints_statements_body.v7
12 files changed, 194 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/bug_12806.v b/test-suite/bugs/closed/bug_12806.v
new file mode 100644
index 0000000000..ee221d33a6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12806.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Declare Scope my_scope.
+Delimit Scope my_scope with my_scope.
+
+Notation "###" := tt : my_scope.
+
+Ltac2 Notation "bar" c(open_constr(my_scope)) := c.
+Ltac2 Eval bar ###.
diff --git a/test-suite/micromega/bug_11656.v b/test-suite/micromega/bug_11656.v
new file mode 100644
index 0000000000..19846ad50a
--- /dev/null
+++ b/test-suite/micromega/bug_11656.v
@@ -0,0 +1,11 @@
+Require Import Lia.
+Require Import NArith.
+Open Scope N_scope.
+
+Goal forall (a b c: N),
+ a <> 0 ->
+ c <> 0 ->
+ a * ((b + 1) * c) <> 0.
+Proof.
+ intros. nia.
+Qed.
diff --git a/test-suite/micromega/bug_12184.v b/test-suite/micromega/bug_12184.v
new file mode 100644
index 0000000000..d329a3fa7f
--- /dev/null
+++ b/test-suite/micromega/bug_12184.v
@@ -0,0 +1,8 @@
+Require Import Lia.
+Require Import ZArith.
+
+Goal forall p : positive, (0 < Z.pos (2^p)%positive)%Z.
+Proof.
+ intros p.
+ lia.
+Qed.
diff --git a/test-suite/micromega/bug_14054.v b/test-suite/micromega/bug_14054.v
new file mode 100644
index 0000000000..d97e13375f
--- /dev/null
+++ b/test-suite/micromega/bug_14054.v
@@ -0,0 +1,46 @@
+(* bug 13242 *)
+
+Require Import Lia.
+Fail Add Zify InjTyp id.
+
+(* bug 14054 *)
+
+Require Import Coq.ZArith.ZArith. Open Scope Z_scope.
+Require Coq.Init.Byte .
+Require Import Coq.micromega.ZifyClasses Coq.micromega.Lia.
+
+Notation byte := Coq.Init.Byte.byte.
+
+Module byte.
+ Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).
+End byte.
+
+Section WithA.
+ Context (A: Type).
+ Fixpoint tuple(n: nat): Type :=
+ match n with
+ | O => unit
+ | S m => A * tuple m
+ end.
+End WithA.
+
+Module LittleEndian.
+ Fixpoint combine (n : nat) : forall (bs : tuple byte n), Z :=
+ match n with
+ | O => fun _ => 0
+ | S n => fun bs => Z.lor (byte.unsigned (fst bs))
+ (Z.shiftl (combine n (snd bs)) 8)
+ end.
+ Lemma combine_bound: forall {n: nat} (t: tuple byte n),
+ 0 <= LittleEndian.combine n t < 2 ^ (8 * Z.of_nat n).
+ Admitted.
+End LittleEndian.
+
+Instance InjByteTuple{n: nat}: InjTyp (tuple byte n) Z := {|
+ inj := LittleEndian.combine n;
+ pred x := 0 <= x < 2 ^ (8 * Z.of_nat n);
+ cstr := @LittleEndian.combine_bound n;
+|}.
+Fail Add Zify InjTyp InjByteTuple.
+Fail Add Zify UnOp InjByteTuple.
+Fail Add Zify UnOp X.
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index d70bb809c6..d22e2b7c8c 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -12,6 +12,12 @@ Open Scope Z_scope.
Require Import ZMicromega.
Require Import VarMap.
+Lemma power_pos : forall x y, 0 <= x \/ False -> x^ y >= 0.
+Proof.
+ intros.
+ lia.
+Qed.
+
Lemma not_so_easy : forall x n : Z,
2*x + 1 <= 2 *n -> x <= n-1.
Proof.
diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v
index 485c24f0c9..e79b76b810 100644
--- a/test-suite/micromega/example_nia.v
+++ b/test-suite/micromega/example_nia.v
@@ -7,10 +7,16 @@
(************************************************************************)
Require Import ZArith.
-Require Import Psatz.
Open Scope Z_scope.
-Require Import ZMicromega.
+Require Import ZMicromega Lia.
Require Import VarMap.
+Unset Nia Cache.
+
+Goal forall (x y: Z), 0 < (1+y^2)^(x^2).
+Proof. nia. Qed.
+
+Goal forall (x y: Z), 0 <= (y^2)^x.
+Proof. nia. Qed.
(* false in Q : x=1/2 and n=1 *)
@@ -347,8 +353,8 @@ Lemma hol_light17 : forall x y,
-> x * y * (x + y) <= x ^ 2 + y ^ 2.
Proof.
intros.
- Fail nia.
-Abort.
+ nia.
+Qed.
Lemma hol_light18 : forall x y,
@@ -507,3 +513,24 @@ Proof.
intros.
lia.
Qed.
+
+Lemma mult : forall x x0 x1 x2 n n0 n1 n2,
+ 0 <= x -> 0 <= x0 -> 0 <= x1 -> 0 <= x2 ->
+ 0 <= n -> 0 <= n0 -> 0 <= n1 -> 0 <= n2 ->
+ (n1 * x <= n2 * x1) ->
+ (n * x0 <= n0 * x2) ->
+ (n1 * n * (x * x0) > n2 * n0 * (x1 * x2)) -> False.
+Proof.
+ intros.
+ nia.
+Qed.
+
+
+Lemma mult_nat : forall x x0 x1 x2 n n0 n1 n2,
+ (n1 * x <= n2 * x1)%nat ->
+ (n * x0 <= n0 * x2)%nat ->
+ (n1 * n * (x * x0) > n2 * n0 * (x1 * x2))%nat -> False.
+Proof.
+ intros.
+ nia.
+Qed.
diff --git a/test-suite/misc/vio_checking.sh b/test-suite/misc/vio_checking.sh
new file mode 100755
index 0000000000..ffa909e93b
--- /dev/null
+++ b/test-suite/misc/vio_checking.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -ex
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc
+
+rm -f vio_checking{,bad}.{vo,vio}
+
+coqc -vio vio_checking.v
+coqc -vio vio_checking_bad.v
+
+coqc -schedule-vio-checking 2 vio_checking.vio
+
+if coqc -schedule-vio-checking 2 vio_checking_bad.vio; then
+ echo 'vio-checking on vio_checking_bad.vio should have failed!'
+ exit 1
+fi
+if coqc -schedule-vio-checking 2 vio_checking.vio vio_checking_bad.vio; then
+ echo 'vio-checking on vio_checking vio_checking_bad.vio should have failed!'
+ exit 1
+fi
+
+coqc -vio2vo vio_checking.vio
+coqchk -silent vio_checking.vo
+
+if coqc -vio2vo vio_checking_bad.vio; then
+ echo 'vio2vo on vio_checking_bad.vio should have failed!'
+ exit 1
+fi
diff --git a/test-suite/misc/vio_checking.v b/test-suite/misc/vio_checking.v
new file mode 100644
index 0000000000..8dd5e47383
--- /dev/null
+++ b/test-suite/misc/vio_checking.v
@@ -0,0 +1,9 @@
+
+Lemma foo : Type.
+Proof. exact Type. Qed.
+
+Lemma foo1 : Type.
+Proof. exact Type. Qed.
+
+Lemma foo2 : Type.
+Proof. exact foo1. Qed.
diff --git a/test-suite/misc/vio_checking_bad.v b/test-suite/misc/vio_checking_bad.v
new file mode 100644
index 0000000000..f32d06f34a
--- /dev/null
+++ b/test-suite/misc/vio_checking_bad.v
@@ -0,0 +1,4 @@
+(* a file to check that vio-checking is not a noop *)
+
+Lemma foo : Type.
+Proof. match goal with |- ?G => exact G end. Qed.
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index bbdf9762a3..a530c34297 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -1,4 +1,3 @@
-
Require Import Lia ZArith.
(* Submitted by Xavier Urbain 18 Jan 2002 *)
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/vio/univ_constraints_statements_body.v b/test-suite/vio/univ_constraints_statements_body.v
new file mode 100644
index 0000000000..6302adefc2
--- /dev/null
+++ b/test-suite/vio/univ_constraints_statements_body.v
@@ -0,0 +1,7 @@
+Definition T := Type.
+Definition T1 : T := Type.
+
+Lemma x : True.
+Proof.
+exact (let a : T := Type in I).
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:21:01 +0000