aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile11
-rw-r--r--test-suite/bugs/closed/bug_11866.v43
-rw-r--r--test-suite/bugs/closed/bug_12806.v9
-rw-r--r--test-suite/bugs/closed/bug_14131.v19
-rw-r--r--test-suite/ltac2/std_tactics.v29
-rw-r--r--test-suite/micromega/bug_11089.v13
-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
-rw-r--r--test-suite/micromega/zify.v7
-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
18 files changed, 316 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 2a2f62e23f..f06439a863 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -517,6 +517,17 @@ approve-output: output output-coqtop output-coqchk
echo "Updated $${f%.real}!"; \
done
+approve-coqdoc: coqdoc
+ $(HIDE)(cd coqdoc; \
+ for f in *.html.out; do \
+ cp "Coqdoc.$${f%.out}" "$$f"; \
+ echo "Updated $$f!"; \
+ done; \
+ for f in *.tex.out; do \
+ cat "Coqdoc.$${f%.out}" | grep -v "^%%" > "$$f"; \
+ echo "Updated $$f!"; \
+ done)
+
# the expected output for the MExtraction test is
# /plugins/micromega/micromega.ml except with additional newline
output/MExtraction.out: ../plugins/micromega/micromega.ml
diff --git a/test-suite/bugs/closed/bug_11866.v b/test-suite/bugs/closed/bug_11866.v
new file mode 100644
index 0000000000..5a47f3833e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11866.v
@@ -0,0 +1,43 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Notation "ex0" x(tactic(0)) := ().
+Ltac2 Notation "ex1" x(tactic(1)) := ().
+Ltac2 Notation "ex2" x(tactic(2)) := ().
+Ltac2 Notation "ex3" x(tactic(3)) := ().
+Ltac2 Notation "ex4" x(tactic(4)) := ().
+Ltac2 Notation "ex5" x(tactic(5)) := ().
+Ltac2 Notation "ex6" x(tactic(6)) := ().
+
+Ltac2 Notation ":::0" x(tactic) "+0" y(tactic) : 0 := ().
+Ltac2 Notation ":::1" x(tactic) "+1" y(tactic) : 1 := ().
+Ltac2 Notation ":::2" x(tactic) "+2" y(tactic) : 2 := ().
+Ltac2 Notation ":::3" x(tactic) "+3" y(tactic) : 3 := ().
+Ltac2 Notation ":::4" x(tactic) "+4" y(tactic) : 4 := ().
+Ltac2 Notation ":::5" x(tactic) "+5" y(tactic) : 5 := ().
+Ltac2 Notation ":::6" x(tactic) "+6" y(tactic) : 6 := ().
+Fail Ltac2 Notation ":::7" x(tactic) "+7" y(tactic) : 7 := ().
+Goal True.
+ ex0 :::0 0 +0 0.
+ ex1 :::0 0 +0 0.
+ (*ex2 :::0 0 +0 0.*) (* fails with an anomaly, cf COQBUG(https://github.com/coq/coq/issues/12807) *)
+ (*ex3 :::0 0 +0 0.*)
+ ex4 :::0 0 +0 0.
+ ex5 :::0 0 +0 0.
+ ex6 :::0 0 +0 0.
+
+ ex0 :::1 0 +1 0.
+ ex1 :::1 0 +1 0.
+ (*ex2 :::1 0 +1 0.*)
+ (*ex3 :::1 0 +1 0.*)
+ ex4 :::1 0 +1 0.
+ ex5 :::1 0 +1 0.
+ ex6 :::1 0 +1 0.
+
+ ex0 :::6 0 +6 0.
+ ex1 :::6 0 +6 0.
+ (*ex2 :::6 0 +6 0.*)
+ (*ex3 :::6 0 +6 0.*)
+ ex4 :::6 0 +6 0.
+ ex5 :::6 0 +6 0.
+ ex6 :::6 0 +6 0.
+Abort.
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/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v
new file mode 100644
index 0000000000..611464458e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14131.v
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Unset Elimination Schemes.
+
+Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
+ JMeq_refl : JMeq x x.
+
+Set Elimination Schemes.
+
+Register JMeq as core.JMeq.type.
+
+Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
+ P x -> forall y, JMeq x y -> P y.
+
+Register JMeq_ind as core.JMeq.ind.
+
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
+ P x -> forall y, JMeq y x -> P y.
+Proof. intros. try rewrite H0.
+Abort.
diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v
new file mode 100644
index 0000000000..39b620a6ac
--- /dev/null
+++ b/test-suite/ltac2/std_tactics.v
@@ -0,0 +1,29 @@
+Require Import Ltac2.Ltac2.
+
+Axiom f: nat -> nat.
+Definition g := f.
+
+Axiom Foo1: nat -> Prop.
+Axiom Foo2: nat -> Prop.
+Axiom Impl: forall n: nat, Foo1 (f n) -> Foo2 (f n).
+
+Create HintDb foo discriminated.
+#[export] Hint Constants Opaque : foo.
+#[export] Hint Resolve Impl : foo.
+
+Goal forall x, Foo1 (f x) -> Foo2 (g x).
+Proof.
+ auto with foo.
+ #[export] Hint Transparent g : foo.
+ auto with foo.
+Qed.
+
+Goal forall (x: nat), exists y, f x = g y.
+Proof.
+ intros.
+ eexists.
+ unify f g.
+ lazy_match! goal with
+ | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs
+ end.
+Abort.
diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v
new file mode 100644
index 0000000000..e62b5b8d9e
--- /dev/null
+++ b/test-suite/micromega/bug_11089.v
@@ -0,0 +1,13 @@
+Require Import Lia.
+Unset Lia Cache.
+Definition t := nat.
+Goal forall (n : t), n = n.
+Proof.
+ intros.
+ lia.
+Qed.
+Goal let t' := nat in forall (n : t'), n = n.
+Proof.
+ intros.
+ lia.
+Qed.
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/micromega/zify.v b/test-suite/micromega/zify.v
index a12623c3c0..2ea320047d 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -167,6 +167,12 @@ Goal @zero znat = 0%nat.
reflexivity.
Qed.
+Require Import ZifyBool.
+Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
+ { TUOp := id; TUOpInj := fun _ => eq_refl }.
+Add Zify UnOp Op_bool_inj.
+
+
Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y),
(F P + 1 = 1 + F P)%positive.
Proof.
@@ -228,6 +234,7 @@ Proof.
intros. lia.
Qed.
+
Ltac Zify.zify_pre_hook ::= unfold is_true in *.
Goal forall x y : nat, is_true (Nat.eqb x 1) ->
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-01-31 11:05:51 +0000