aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/.csdp.cachebin89077 -> 165200 bytes
-rw-r--r--test-suite/Makefile41
-rw-r--r--test-suite/bugs/closed/bug_4132.v2
-rw-r--r--test-suite/bugs/closed/bug_5197.v44
-rw-r--r--test-suite/bugs/closed/bug_8553.v (renamed from test-suite/bugs/closed/8553.v)0
-rw-r--r--test-suite/bugs/closed/bug_8672.v (renamed from test-suite/bugs/closed/8672.v)0
-rw-r--r--test-suite/dune73
-rw-r--r--test-suite/micromega/example.v151
-rw-r--r--test-suite/micromega/example_nia.v503
-rw-r--r--test-suite/micromega/non_lin_ci.v278
-rw-r--r--test-suite/micromega/rexample.v29
-rw-r--r--test-suite/micromega/square.v10
-rwxr-xr-xtest-suite/misc/universes/build_all_stdlib.sh4
-rw-r--r--test-suite/misc/universes/dune8
-rw-r--r--test-suite/output/MExtraction.v6
-rw-r--r--test-suite/output/PrintModule.out4
-rw-r--r--test-suite/output/PrintModule.v12
-rw-r--r--test-suite/success/btauto.v9
-rw-r--r--test-suite/success/univers.v2
19 files changed, 1112 insertions, 64 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95f..b85258505b 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
Binary files differ
diff --git a/test-suite/Makefile b/test-suite/Makefile
index e35393b5e8..928a77cb8e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -43,8 +43,8 @@ coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
coqdoc := $(BIN)coqdoc
coqtopbyte := $(BIN)coqtop.byte
-coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
-coqtopcompile := $(coqtop) -compile
+coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source
+coqtopcompile := $(coqtop) -async-proofs-cache force -compile
coqdep := $(BIN)coqdep -coqlib $(LIB)
VERBOSE?=
@@ -122,7 +122,7 @@ run: $(SUBSYSTEMS)
bugs: $(BUGS)
clean:
- rm -f trace .lia.cache output/MExtraction.out
+ rm -f trace .nia.cache .lia.cache output/MExtraction.out
$(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
$(HIDE)find . \( \
-name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
@@ -213,7 +213,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...still active"; \
@@ -235,7 +235,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -250,11 +250,22 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
# Unit tests
#######################################################################
-OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
-SYSMOD:=-package num,str,unix,dynlink,threads
+# An alternative is ifeq ($(OS),Windows_NT) using make's own variable.
+ifeq ($(ARCH),win32)
+ export FINDLIB_SEP=";"
+else
+ export FINDLIB_SEP=":"
+endif
+
+# COQLIBINSTALL is quoted in config/make thus we must unquote it,
+# otherwise the directory name will include the quotes, see
+# see for example https://stackoverflow.com/questions/10424645/how-to-convert-a-quoted-string-to-a-normal-one-in-makefile
-COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS))
-COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX))
+ifeq ($(LOCAL),true)
+ export OCAMLPATH := $(shell echo $(COQLIBINSTALL)$(FINDLIB_SEP)$$OCAMLPATH)
+endif
+
+OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
# ML files from unit-test framework, not containing tests
UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml)
@@ -278,10 +289,8 @@ unit-tests: $(UNIT_LOGFILES)
# Build executable, run it to generate log file
unit-tests/%.ml.log: unit-tests/%.ml
$(SHOW) 'TEST $<'
- $(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \
- $(SYSMOD) -package camlp5.gramlib,oUnit \
- -I unit-tests/src $(COQSRCDIRS) $(COQCMXS) \
- $(UNIT_CMXS) $< -o $<.test;
+ $(HIDE)$(OCAMLOPT) -linkall -linkpkg -package coq.toplevel,oUnit \
+ -I unit-tests/src $(UNIT_CMXS) $< -o $<.test;
$(HIDE)./$<.test
#######################################################################
@@ -309,7 +318,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v
$(HIDE){ \
opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
echo $(call log_intro,$<); \
- $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+ $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -341,7 +350,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -482,7 +491,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_success); \
echo " $<...still wished"; \
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 806ffb771f..67ecc3087f 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -26,6 +26,6 @@ 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,
- this might have triggered "Failure(occurence 2)" in the past,
+ 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_5197.v b/test-suite/bugs/closed/bug_5197.v
new file mode 100644
index 0000000000..b67e93d677
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -0,0 +1,44 @@
+Set Universe Polymorphism.
+Set Primitive Projections.
+Unset Printing Primitive Projection Compatibility.
+Axiom Ω : Type.
+
+Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack {
+ elt : forall ω, A ω;
+ prp : forall ω, Aᴿ ω elt;
+}.
+
+Record TYPE := mkTYPE {
+ wit : Ω -> Type;
+ rel : Ω -> (forall ω : Ω, wit ω) -> Type;
+}.
+
+Definition El (A : TYPE) : Type := Pack A.(wit) A.(rel).
+
+Definition Typeᶠ : TYPE := {|
+ wit := fun _ => Type;
+ rel := fun _ A => (forall ω : Ω, A ω) -> Type;
+ |}.
+Set Printing Universes.
+Fail Definition Typeᵇ : El Typeᶠ :=
+ mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+
+Definition Typeᵇ : El Typeᶠ :=
+ mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+
+(** Bidirectional typechecking helps here *)
+Require Import Program.Tactics.
+Program Definition progTypeᵇ : El Typeᶠ :=
+ mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+
+(**
+The command has indeed failed with message:
+Error: Conversion test raised an anomaly
+**)
+
+Definition Typeᵇ' : El Typeᶠ.
+Proof.
+unshelve refine (mkPack _ _ _ _).
++ refine (fun _ => Type).
++ simpl. refine (fun _ A => (forall ω, A ω) -> Type).
+Defined.
diff --git a/test-suite/bugs/closed/8553.v b/test-suite/bugs/closed/bug_8553.v
index 4a1afabe89..4a1afabe89 100644
--- a/test-suite/bugs/closed/8553.v
+++ b/test-suite/bugs/closed/bug_8553.v
diff --git a/test-suite/bugs/closed/8672.v b/test-suite/bugs/closed/bug_8672.v
index 66cd6dfa8c..66cd6dfa8c 100644
--- a/test-suite/bugs/closed/8672.v
+++ b/test-suite/bugs/closed/bug_8672.v
diff --git a/test-suite/dune b/test-suite/dune
new file mode 100644
index 0000000000..c5fa0bb14a
--- /dev/null
+++ b/test-suite/dune
@@ -0,0 +1,73 @@
+(rule
+ (targets summary.log)
+ (deps
+ ; File that should be promoted.
+ misc/universes/all_stdlib.v
+ ; Dependencies of the legacy makefile
+ ../Makefile.common
+ ../config/Makefile
+ ; Stuff for the compat script test
+ ../dev/header.ml
+ ../dev/tools/update-compat.py
+ ../doc/stdlib/index-list.html.template
+ (package coq)
+ ; For fake_ide
+ (package coqide-server)
+ (source_tree .))
+ ; Finer-grained dependencies look like this
+ ; ../tools/CoqMakefile.in
+ ; ../theories/Init/Prelude.vo
+ ; ../theories/Arith/Arith.vo
+ ; ../theories/Arith/Compare.vo
+ ; ../theories/PArith/PArith.vo
+ ; ../theories/QArith/QArith.vo
+ ; ../theories/QArith/Qcanon.vo
+ ; ../theories/ZArith/ZArith.vo
+ ; ../theories/ZArith/Zwf.vo
+ ; ../theories/Sets/Ensembles.vo
+ ; ../theories/Numbers/Natural/Peano/NPeano.vo
+ ; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo
+ ; ../theories/FSets/FMaps.vo
+ ; ../theories/FSets/FSets.vo
+ ; ../theories/MSets/MSets.vo
+ ; ../theories/Compat/Coq87.vo
+ ; ../theories/Compat/Coq88.vo
+ ; ../theories/Relations/Relations.vo
+ ; ../theories/Unicode/Utf8.vo
+ ; ../theories/Program/Program.vo
+ ; ../theories/Classes/EquivDec.vo
+ ; ../theories/Classes/DecidableClass.vo
+ ; ../theories/Classes/SetoidClass.vo
+ ; ../theories/Classes/RelationClasses.vo
+ ; ../theories/Logic/Classical.vo
+ ; ../theories/Logic/Hurkens.vo
+ ; ../theories/Logic/ClassicalFacts.vo
+ ; ../theories/Reals/Reals.vo
+ ; ../theories/Lists/Streams.vo
+ ; ../plugins/micromega/Lia.vo
+ ; ../plugins/micromega/Lqa.vo
+ ; ../plugins/micromega/Psatz.vo
+ ; ../plugins/micromega/MExtraction.vo
+ ; ../plugins/nsatz/Nsatz.vo
+ ; ../plugins/omega/Omega.vo
+ ; ../plugins/ssr/ssrbool.vo
+ ; ../plugins/derive/Derive.vo
+ ; ../plugins/funind/Recdef.vo
+ ; ../plugins/extraction/Extraction.vo
+ ; ../plugins/extraction/ExtrOcamlNatInt.vo
+ ; coqtop
+ ; coqtop.opt
+ ; coqidetop.opt
+ ; coqqueryworker.opt
+ ; coqtacticworker.opt
+ ; coqproofworker.opt
+ ; coqc
+ ; coqchk
+ ; coqdoc
+ ; %{bin:coq_makefile}
+ ; %{bin:fake_ide}
+ (action
+ (progn
+ ; XXX: we will allow to set the NJOBS variable in a future Dune
+ ; version, either by using an env var or by letting Dune set `-j`
+ (run make -j 2 BIN= PRINT_LOGS=1))))
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 25e4a09fa0..d70bb809c6 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -12,25 +12,48 @@ Open Scope Z_scope.
Require Import ZMicromega.
Require Import VarMap.
-(* false in Q : x=1/2 and n=1 *)
-
Lemma not_so_easy : forall x n : Z,
2*x + 1 <= 2 *n -> x <= n-1.
Proof.
intros.
- lia.
+ psatz Z 2.
Qed.
+
(* From Laurent Théry *)
-Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+ intros.
+ psatz Z 2.
+Qed.
+
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+ intros.
+ psatz Z 2.
+Qed.
+
+Goal forall (x y : Z), 2*x = 0 -> x * y = 0.
Proof.
intros.
psatz Z 2.
Qed.
+Goal forall (x y: Z), - x*x >= 0 -> x * y = 0.
+Proof.
+ intros.
+ psatz Z 4.
+Qed.
+
+Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Proof.
+ intros.
+ psatz Z 2.
+Qed.
+
Lemma Zdiscr: forall a b c x,
a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
Proof.
@@ -42,11 +65,9 @@ Lemma plus_minus : forall x y,
0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y.
Proof.
intros.
- lia.
+ psatz Z 1.
Qed.
-
-
Lemma mplus_minus : forall x y,
x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
Proof.
@@ -95,7 +116,7 @@ Proof.
generalize (H8 _ _ _ (conj H5 H4)).
generalize (H10 _ _ _ (conj H5 H4)).
generalize rho_ge.
- psatz Z 2.
+ zify; intuition subst ; psatz Z 2.
Qed.
(* Rule of signs *)
@@ -118,18 +139,12 @@ Proof.
intros; psatz Z 2.
Qed.
-Lemma sign_zer_pos: forall x y,
+Lemma sign_zero_pos: forall x y,
x = 0 -> y > 0 -> x*y = 0.
Proof.
intros; psatz Z 2.
Qed.
-Lemma sign_zero_zero: forall x y,
- x = 0 -> y = 0 -> x*y = 0.
-Proof.
- intros; psatz Z 2.
-Qed.
-
Lemma sign_zero_neg: forall x y,
x = 0 -> y < 0 -> x*y = 0.
Proof.
@@ -157,12 +172,6 @@ Qed.
(* Other (simple) examples *)
-Lemma binomial : forall x y, (x+y)^2 = x^2 + 2*x*y + y^2.
-Proof.
- intros.
- lia.
-Qed.
-
Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
Proof.
intros.
@@ -170,13 +179,6 @@ Proof.
Qed.
-Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
-Proof.
- intros.
- psatz Z 2.
-Qed.
-
-
Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 -> False.
Proof.
intros ; psatz Z 2.
@@ -229,8 +231,6 @@ Proof.
intros; psatz Z 3.
Qed.
-
-
Lemma hol_light7 : forall x y z,
0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
-> x * y + x * z + y * z >= 3 * x * y * z.
@@ -251,6 +251,7 @@ Proof.
intros; psatz Z 2.
Qed.
+
Lemma hol_light10 : forall x y,
x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
Proof.
@@ -275,6 +276,7 @@ Proof.
unfold e ; intros ; psatz Z 2.
Qed.
+
Lemma hol_light14 : forall x y z,
2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
-> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
@@ -300,6 +302,7 @@ Proof.
intros ; psatz Z 3.
Qed.
+
Lemma hol_light18 : forall x y,
0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
Proof.
@@ -310,18 +313,12 @@ Qed.
(* Some examples over integers and natural numbers. *)
(* ------------------------------------------------------------------------- *)
-Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
-Proof.
- intros ; lia.
-Qed.
-
Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
Proof.
intros.
psatz Z 2.
Qed.
-
Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 ->
((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
-> (x1 + y1 = x2 + y2).
@@ -336,11 +333,89 @@ Proof.
psatz Z 1.
Qed.
-
-
Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
Proof.
intros.
generalize (motzkin' x y).
psatz Z 8.
Qed.
+
+(** Other tests *)
+
+Goal forall x y z n,
+ y >= z /\ y = n \/ ~ y >= z /\ z = n ->
+ x >= y /\
+ (x >= z /\ (x >= n /\ x = x \/ ~ x >= n /\ x = n) \/
+ ~ x >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)) \/
+ ~ x >= y /\
+ (y >= z /\ (x >= n /\ y = x \/ ~ x >= n /\ y = n) \/
+ ~ y >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)).
+Proof.
+ intros.
+ psatz Z 2.
+Qed.
+
+(** Incompeteness: require manual case split *)
+Goal forall (z0 z z1 z2 z3 z5 :Z)
+(H8 : 0 <= z2)
+(H5 : z5 > 0)
+(H0 : z0 > 0)
+(H9 : z2 < z0)
+(H1 : z0 * z5 > 0)
+(H10 : 0 <= z1 * z0 + z0 * z5 - 1 - z0 * z5 * z)
+(H11 : z1 * z0 + z0 * z5 - 1 - z0 * z5 * z < z0 * z5)
+(H6 : 0 <= z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3)
+(H7 : z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3 < z0 * z5)
+(C : z > z3), False.
+Proof.
+ intros.
+ assert (z1 - z5 * z3 - 1 < 0) by psatz Z 3.
+ psatz Z 3.
+Qed.
+
+Goal forall
+ (d sz x n : Z)
+ (GE : sz * x - sz * d >=1 )
+ (R : sz + d * sz - sz * x >= 1),
+ False.
+Proof.
+ intros.
+ assert (x - d >= 1) by psatz Z 3.
+ psatz Z 3.
+Qed.
+
+
+Goal forall x6 x8 x9 x10 x11 x12 x13 x14,
+ x6 >= 0 ->
+ -x6 + x8 + x9 + -x10 >= 1 ->
+ x8 >= 0 ->
+ x11 >= 0 ->
+ -x11 + x12 + x13 + -x14 >= 1 ->
+ x6 + -4*x8 + -2*x9 + 3*x10 + x11 + -4*x12 + -2*x13 + 3*x14 >= -5 ->
+ x10 >= 0 ->
+ x14 >= 0 ->
+ x12 >= 0 ->
+ x8 + -x10 + x12 + -x14 >= 1 ->
+ False.
+Proof.
+ intros.
+ psatz Z 1.
+Qed.
+
+Goal forall x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12,
+x2 + -1*x4 >= 0 ->
+-2*x2 + x4 >= -1 ->
+x1 + x3 + x4 + -1*x7 + -1*x11 >= 1 ->
+-1*x2 + x8 + x10 >= 0 ->
+-2*x3 + -2*x4 + x5 + 2*x6 + x9 >= -1 ->
+-2*x1 + 3*x3 + x4 + -1*x7 + -1*x11 >= 0 ->
+-2*x1 + x3 + x4 + -1*x8 + -1*x10 + 2*x12 >= 0 ->
+-2*x2 + x3 + x4 + -1*x7 + -1*x11 + 2*x12 >= 0 ->
+-2*x2 + x3 + 3*x4 + -1*x8 + -1*x10 >= 0 ->
+2*x2 + -1*x3 + -1*x4 + x5 + 2*x6 + -2*x8 + x9 + -2*x10 >= 0 ->
+x1 + -2*x3 + x7 + x11 + -2*x12 >= 0 ->
+ False.
+Proof.
+ intros.
+ psatz Z 1.
+Qed.
diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v
new file mode 100644
index 0000000000..8de631aa6a
--- /dev/null
+++ b/test-suite/micromega/example_nia.v
@@ -0,0 +1,503 @@
+(************************************************************************)
+(* *)
+(* Micromega: A reflexive tactic using the Positivstellensatz *)
+(* *)
+(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
+(* *)
+(************************************************************************)
+
+Require Import ZArith.
+Require Import Psatz.
+Open Scope Z_scope.
+Require Import ZMicromega.
+Require Import VarMap.
+
+(* false in Q : x=1/2 and n=1 *)
+
+Lemma int_not_rat : forall x, 2 * x = 1 -> False.
+Proof.
+ intros.
+ lia.
+Qed.
+
+
+Lemma not_so_easy : forall x n : Z,
+ 2*x + 1 <= 2 *n -> x <= n-1.
+Proof.
+ intros.
+ lia.
+Qed.
+
+Goal forall a1 da na b1 db nb,
+ a1 * da = na ->
+ b1 * db = nb ->
+ a1 * b1 * da * db = na * nb.
+Proof.
+ intros.
+ nia.
+Qed.
+
+(* From Laurent Théry *)
+
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+Goal forall (x y : Z), 2*x = 0 -> x * y = 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+
+Goal forall (x y: Z), - x*x >= 0 -> x * y = 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+
+Lemma Zdiscr: forall a b c x,
+ a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
+Proof.
+ intros.
+ Fail nia. (* Incompletness *)
+Abort.
+
+
+Lemma plus_minus : forall x y,
+ 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y.
+Proof.
+ intros.
+ lia.
+Qed.
+
+
+Lemma mplus_minus : forall x y,
+ x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma pol3: forall x y, 0 <= x + y ->
+ x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+
+(* Motivating example from: Expressiveness + Automation + Soundness:
+ Towards COmbining SMT Solvers and Interactive Proof Assistants *)
+Parameter rho : Z.
+Parameter rho_ge : rho >= 0.
+Parameter correct : Z -> Z -> Prop.
+
+
+Definition rbound1 (C:Z -> Z -> Z) : Prop :=
+ forall p s t, correct p t /\ s <= t -> C p t - C p s <= (1-rho)*(t-s).
+
+Definition rbound2 (C:Z -> Z -> Z) : Prop :=
+ forall p s t, correct p t /\ s <= t -> (1-rho)*(t-s) <= C p t - C p s.
+
+
+Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t /\ correct q t /\
+ rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D ->
+ Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s).
+Proof.
+ intros.
+ generalize (Z.abs_eq (C p t - D q t)).
+ generalize (Z.abs_neq (C p t - D q t)).
+ generalize (Z.abs_eq (C p s -D q s)).
+ generalize (Z.abs_neq (C p s - D q s)).
+ unfold rbound2 in H.
+ unfold rbound1 in H.
+ intuition.
+ generalize (H6 _ _ _ (conj H H4)).
+ generalize (H7 _ _ _ (conj H H4)).
+ generalize (H8 _ _ _ (conj H H4)).
+ generalize (H10 _ _ _ (conj H H4)).
+ generalize (H6 _ _ _ (conj H5 H4)).
+ generalize (H7 _ _ _ (conj H5 H4)).
+ generalize (H8 _ _ _ (conj H5 H4)).
+ generalize (H10 _ _ _ (conj H5 H4)).
+ generalize rho_ge.
+ nia.
+Qed.
+
+(* Rule of signs *)
+
+Lemma sign_pos_pos: forall x y,
+ x > 0 -> y > 0 -> x*y > 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_pos_zero: forall x y,
+ x > 0 -> y = 0 -> x*y = 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_pos_neg: forall x y,
+ x > 0 -> y < 0 -> x*y < 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_zero_pos: forall x y,
+ x = 0 -> y > 0 -> x*y = 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_zero_zero: forall x y,
+ x = 0 -> y = 0 -> x*y = 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_zero_neg: forall x y,
+ x = 0 -> y < 0 -> x*y = 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_neg_pos: forall x y,
+ x < 0 -> y > 0 -> x*y < 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_neg_zero: forall x y,
+ x < 0 -> y = 0 -> x*y = 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma sign_neg_neg: forall x y,
+ x < 0 -> y < 0 -> x*y > 0.
+Proof.
+ intros; nia.
+Qed.
+
+
+(* Other (simple) examples *)
+
+Lemma binomial : forall x y, (x+y)^2 = x^2 + 2*x*y + y^2.
+Proof.
+ intros.
+ lia.
+Qed.
+
+Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+
+Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
+Proof.
+ intros.
+ nia.
+Qed.
+
+
+Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 -> False.
+Proof.
+ intros. nia.
+Qed.
+
+(* Found in Parrilo's talk *)
+(* BUG?: certificate with **very** big coefficients *)
+Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
+Proof.
+ intros.
+ nia.
+Qed.
+
+(* from hol_light/Examples/sos.ml *)
+
+Lemma hol_light1 : forall a1 a2 b1 b2,
+ a1 >= 0 -> a2 >= 0 ->
+ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) ->
+ (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+Lemma hol_light2 : forall x a,
+ 3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma hol_light3 : forall b a c x,
+ b ^ 2 < 4 * a * c -> (a * x ^2 + b * x + c = 0) -> False.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+
+Lemma hol_light4 : forall a c b x,
+ a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+Lemma hol_light5 : forall x y,
+ 0 <= x /\ x <= 1 /\ 0 <= y /\ y <= 1
+ -> x ^ 2 + y ^ 2 < 1 \/
+ (x - 1) ^ 2 + y ^ 2 < 1 \/
+ x ^ 2 + (y - 1) ^ 2 < 1 \/
+ (x - 1) ^ 2 + (y - 1) ^ 2 < 1.
+Proof.
+intros; nia.
+Qed.
+
+Lemma hol_light7 : forall x y z,
+ 0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
+ -> x * y + x * z + y * z >= 3 * x * y * z.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+Lemma hol_light8 : forall x y z,
+ x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+Lemma hol_light9 : forall w x y z,
+ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
+ -> (w + x + y + z) ^ 2 <= 4.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+
+Lemma hol_light10 : forall x y,
+ x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
+Proof.
+ intros.
+ nia.
+Qed.
+
+
+Lemma hol_light11 : forall x y,
+ x > 1 /\ y > 1 -> x * y > x + y - 1.
+Proof.
+ intros ; nia.
+Qed.
+
+Lemma hol_light12: forall x y z,
+ 2 <= x /\ x <= 125841 / 50000 /\
+ 2 <= y /\ y <= 125841 / 50000 /\
+ 2 <= z /\ z <= 125841 / 50000
+ -> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= 0.
+Proof.
+ intros x y z ; set (e:= (125841 / 50000)).
+ compute in e.
+ unfold e ; intros ; nia.
+Qed.
+
+
+Lemma hol_light14 : forall x y z,
+ 2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
+ -> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
+Proof.
+ intros ; nia.
+Qed.
+
+
+(* ------------------------------------------------------------------------- *)
+(* Inequality from sci.math (see "Leon-Sotelo, por favor"). *)
+(* ------------------------------------------------------------------------- *)
+
+Lemma hol_light16 : forall x y,
+ 0 <= x /\ 0 <= y /\ (x * y = 1)
+ -> x + y <= x ^ 2 + y ^ 2.
+Proof.
+ intros ; nia.
+Qed.
+
+Lemma hol_light17 : forall x y,
+ 0 <= x /\ 0 <= y /\ (x * y = 1)
+ -> x * y * (x + y) <= x ^ 2 + y ^ 2.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+
+Lemma hol_light18 : forall x y,
+ 0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+(* ------------------------------------------------------------------------- *)
+(* Some examples over integers and natural numbers. *)
+(* ------------------------------------------------------------------------- *)
+
+Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
+Proof.
+ intros ; lia.
+Qed.
+
+Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
+Proof.
+ intros.
+ nia.
+Qed.
+
+Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 ->
+ ((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
+ -> (x1 + y1 = x2 + y2).
+Proof.
+ intros.
+ nia.
+Qed.
+
+Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+
+Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
+Proof.
+ intros.
+ Fail generalize (motzkin' x y).
+ Fail nia.
+Abort.
+
+(** Other tests *)
+
+Goal forall x y z n,
+ y >= z /\ y = n \/ ~ y >= z /\ z = n ->
+ x >= y /\
+ (x >= z /\ (x >= n /\ x = x \/ ~ x >= n /\ x = n) \/
+ ~ x >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)) \/
+ ~ x >= y /\
+ (y >= z /\ (x >= n /\ y = x \/ ~ x >= n /\ y = n) \/
+ ~ y >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)).
+Proof.
+ intros.
+ lia.
+Qed.
+
+(** Incompeteness: require manual case split *)
+Goal forall (z0 z z1 z2 z3 z5 :Z)
+(H8 : 0 <= z2)
+(H5 : z5 > 0)
+(H0 : z0 > 0)
+(H9 : z2 < z0)
+(H1 : z0 * z5 > 0)
+(H10 : 0 <= z1 * z0 + z0 * z5 - 1 - z0 * z5 * z)
+(H11 : z1 * z0 + z0 * z5 - 1 - z0 * z5 * z < z0 * z5)
+(H6 : 0 <= z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3)
+(H7 : z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3 < z0 * z5)
+(C : z > z3), False.
+Proof.
+ intros.
+ assert (z1 - z5 * z3 - 1 < 0) by nia.
+ nia.
+Qed.
+
+
+Goal forall
+ (d sz x n : Z)
+ (GE : sz * x - sz * d >=1 )
+ (R : sz + d * sz - sz * x >= 1),
+ False.
+Proof.
+ intros.
+ assert (x - d >= 1) by nia.
+ nia.
+Qed.
+
+
+Goal forall x6 x8 x9 x10 x11 x12 x13 x14,
+ x6 >= 0 ->
+ -x6 + x8 + x9 + -x10 >= 1 ->
+ x8 >= 0 ->
+ x11 >= 0 ->
+ -x11 + x12 + x13 + -x14 >= 1 ->
+ x6 + -4*x8 + -2*x9 + 3*x10 + x11 + -4*x12 + -2*x13 + 3*x14 >= -5 ->
+ x10 >= 0 ->
+ x14 >= 0 ->
+ x12 >= 0 ->
+ x8 + -x10 + x12 + -x14 >= 1 ->
+ False.
+Proof.
+ intros.
+ lia.
+Qed.
+
+Goal forall x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12,
+x2 + -1*x4 >= 0 ->
+-2*x2 + x4 >= -1 ->
+x1 + x3 + x4 + -1*x7 + -1*x11 >= 1 ->
+-1*x2 + x8 + x10 >= 0 ->
+-2*x3 + -2*x4 + x5 + 2*x6 + x9 >= -1 ->
+-2*x1 + 3*x3 + x4 + -1*x7 + -1*x11 >= 0 ->
+-2*x1 + x3 + x4 + -1*x8 + -1*x10 + 2*x12 >= 0 ->
+-2*x2 + x3 + x4 + -1*x7 + -1*x11 + 2*x12 >= 0 ->
+-2*x2 + x3 + 3*x4 + -1*x8 + -1*x10 >= 0 ->
+2*x2 + -1*x3 + -1*x4 + x5 + 2*x6 + -2*x8 + x9 + -2*x10 >= 0 ->
+x1 + -2*x3 + x7 + x11 + -2*x12 >= 0 ->
+ False.
+Proof.
+ intros.
+ lia.
+Qed.
+
+(** Needs some cutting plane *)
+Goal
+ forall (m : Z)
+ (M : Z)
+ (x : Z)
+ (i : Z)
+ (e1 : Z)
+ (e2 : Z)
+ (e5 : Z)
+ (e6 : Z)
+ (H2 : e5 >= M)
+ (H11 : i < m)
+ (H5 : 0 <= i)
+ (H15 : m < 4294967296)
+ (H7 : 0 <= x)
+ (H26 : e5 < 4294967296)
+ (H21 : x + i = 4294967296 * e6 + e5)
+ (H9 : x + m = 4294967296 * e2 + e1)
+ (H12 : x < e1)
+ (H13 : e1 < M),
+ False.
+Proof.
+ intros.
+ lia.
+Qed.
diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v
new file mode 100644
index 0000000000..ec39209230
--- /dev/null
+++ b/test-suite/micromega/non_lin_ci.v
@@ -0,0 +1,278 @@
+Require Import ZArith.
+Require Import Lia Psatz.
+Open Scope Z_scope.
+
+
+
+
+(* From fiat-crypto Generalized.v *)
+
+
+Goal forall (x1 : Z) (x2 : Z) (x3 : Z) (x4 : Z) (x5 : Z) (x6 : Z) (x7 : Z) (x8 : Z) (x9 : Z) (x10 : Z) (x11 : Z) (x12 : Z) (x13 : Z) (x14 : Z) (x15 : Z) (x16 : Z) (x17 : Z) (x18 : Z)
+(H0 : -1 + -x1^2 + x3*x5 + x1^2*x2 + -x2*x3*x4 >= 0)
+(H1 : -1 + x4 >= 0)
+(H2 : -1 + x6 >= 0)
+(H3 : -1 + -x4 + x1 >= 0)
+(H4 : x3 + -x7 = 0)
+(H5 : x8 >= 0)
+(H6 : -1 + x4 >= 0)
+(H7 : x9 >= 0)
+(H8 : -x8 + x10 >= 0)
+(H9 : -1 + x1^2 + -x9 >= 0)
+(H10 : x4 + -x11 >= 0)
+(H11 : -x3 + x1*x12 + -x12*x13 >= 0)
+(H12 : -1 + -x9 + x1*x4 >= 0)
+(H13 : -1 + x4 + -x13 >= 0)
+(H14 : x13 >= 0)
+(H15 : -1 + x5 >= 0)
+(H16 : -1 + x1 + -x2 >= 0)
+(H17 : x1^2 + -x13 + -x3*x4 = 0)
+(H18 : -1 + x12 + -x14 >= 0)
+(H19 : x14 >= 0)
+(H20 : x1 + -x14 + -x5*x12 = 0)
+(H21 : -1 + x4 + -x15 >= 0)
+(H22 : x15 >= 0)
+(H23 : x9 + -x15 + -x2*x4 = 0)
+(H24 : -x9 + x16 + x4*x17 = 0)
+(H25 : x17 + -x18 = 0)
+, False
+.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+Goal
+ forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13
+ __x14 __x15 __x16 : Z)
+ (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2)
+ (H7 : 0 <= __x8)
+ (H12 : 0 <= __x14)
+ (H0 : __x8 = __x15 * __x11 + __x9)
+ (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16)
+ (H17 : __x16 <= 0)
+ (H15 : 0 <= __x9)
+ (H18 : __x9 < __x15)
+ (H16 : 0 <= __x12)
+ (H19 : __x12 < (__x10 * __x15 + __x14) * __x10)
+ , False.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+
+(* From fiat-crypto Toplevel1.v *)
+
+
+Goal forall
+ (x1 x2 x3 x4 x5 x7 : Z)
+ (H0 : x1 + x2 - x3 = 0) (* substitute x1, nothing happens *)
+ (H1 : 2 * x2 - x4 - 1 >= 0)
+ (H2 : - x2 + x4 >= 0)
+ (H3 : 2 * x2 - x5 - 1 >= 0)
+ (H5 : x2 - 4 >= 0)
+ (H7 : - x2 * x7 + x4 * x5 >= 0)
+ (H6 : x2 * x7 + x2 - x4 * x5 - 1 >= 0)
+ (H9 : x7 - x2 ^ 2 >= 0), (* x2^2 is *visibly* positive *)
+ False.
+Proof.
+ intros.
+ nia.
+Qed.
+
+Goal forall
+ (x1 x2 x3 x4 x5 x7 : Z)
+ (H0 : x2 + x1 - x3 = 0) (* substitute x2= x3 -x1 ... *)
+ (H1 : 2 * x2 - x4 - 1 >= 0)
+ (H2 : - x2 + x4 >= 0)
+ (H3 : 2 * x2 - x5 - 1 >= 0)
+ (H5 : x2 - 4 >= 0)
+ (H7 : - x2 * x7 + x4 * x5 >= 0)
+ (H6 : x2 * x7 + x2 - x4 * x5 - 1 >= 0)
+ (H9 : x7 - x2 ^ 2 >= 0), (* (x3 - x1)^2 is not visibly positive *)
+ False.
+Proof.
+ intros.
+ nia.
+Qed.
+
+(* From bedrock2 FlatToRisc.v *)
+
+(* Variant of the following - omega fails (bad linearisation?)*)
+Goal forall
+ (PXLEN XLEN r : Z)
+ (q q0 r0 a : Z)
+ (H3 : 4 * a = 4 * PXLEN * q0 + (4 * q + r))
+ (H6 : 0 <= 4 * q + r)
+ (H7 : 4 * q + r < 4 * PXLEN)
+ (H8 : r <= 3)
+ (H4 : r >= 1),
+ False.
+Proof.
+ intros.
+ Time lia.
+Qed.
+
+Goal forall
+ (PXLEN XLEN r : Z)
+ (q q0 r0 a : Z)
+ (H3 : 4 * a = 4 * PXLEN * q0 + (4 * q + r))
+ (H6 : 0 <= 4 * q + r)
+ (H7 : 4 * q + r < 4 * PXLEN)
+ (H8 : r <= 3)
+ (H4 : r >= 1),
+ False.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+
+(** Very slow *)
+Goal forall
+ (XLEN r : Z)
+ (H : 4 < 2 ^ XLEN)
+ (H0 : 8 <= XLEN)
+ (q q0 r0 a : Z)
+ (H3 : 4 * a = 4 * 2 ^ (XLEN - 2) * q0 + r0)
+ (H5 : r0 = 4 * q + r)
+ (H6 : 0 <= r0)
+ (H7 : r0 < 4 * 2 ^ (XLEN - 2))
+ (H2 : 0 <= r)
+ (H8 : r < 4)
+ (H4 : r > 0)
+ (H9 : 0 < 2 ^ (XLEN - 2)),
+ False.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+Goal forall
+ (XLEN r : Z)
+ (R : r > 0 \/ r < 0)
+ (H : 4 < 2 ^ XLEN)
+ (H0 : 8 <= XLEN)
+ (H1 : ~ (0 <= XLEN - 2) \/ 0 < 2 ^ (XLEN - 2))
+ (q q0 r0 a : Z)
+ (H2 : 0 <= r0 < 4 * 2 ^ (XLEN - 2))
+ (H3 : 4 * a = 4 * 2 ^ (XLEN - 2) * q0 + r0)
+ (H4 : 0 <= r < 4)
+ (H5 : r0 = 4 * q + r),
+ False.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+Goal forall
+ (XLEN r : Z)
+ (R : r > 0 \/ r < 0)
+ (H : 4 < 2 ^ XLEN)
+ (H0 : 8 <= XLEN)
+ (H1 : ~ (0 <= XLEN - 2) \/ 0 < 2 ^ (XLEN - 2))
+ (q q0 r0 a : Z)
+ (H2 : 0 <= r0 < 4 * 2 ^ (XLEN - 2))
+ (H3 : 4 * a = 4 * 2 ^ (XLEN - 2) * q0 + r0)
+ (H4 : 0 <= r < 4)
+ (H5 : r0 = 4 * q + r),
+ False.
+Proof.
+ intros.
+ intuition idtac.
+ Time all:nia.
+Qed.
+
+
+
+Goal forall
+ (XLEN a q q0 z : Z)
+ (HR : 4 * a - 4 * z * q0 - 4 * q > 0)
+ (H0 : 8 <= XLEN)
+ (H1 : 0 < z)
+ (H : 0 <= 4 * a - 4 * z * q0 - 4 * q)
+ (H3 : 4 * a - 4 * z * q0 - 4 * q < 4)
+ (H4 : 4 * a - 4 * z * q0 < 4 * z),
+ False.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+
+
+(* From fiat-crypto Modulo.v *)
+
+Goal forall (b : Z)
+ (H : 0 <> b)
+ (c r q1 q2 r2 : Z)
+ (H2 : r2 < c)
+ (q0 : Z)
+ (H7 : r < b)
+ (H5 : 0 <= r)
+ (H6 : r < b)
+ (H12 : 0 < c)
+ (H13 : 0 <> c)
+ (H0 : 0 <> c * b)
+ (H1 : 0 <= r2)
+ (H14 : 0 <= q0)
+ (H9 : c * q1 + q0 = c * q2 + r2)
+ (H4 : 0 <= b * q0 + - r)
+ (H10 : b * q0 + - r < c * b),
+ q1 = q2.
+Proof.
+ intros.
+ Fail nia.
+Abort.
+
+
+(* From Sozeau's plugin Equations *)
+
+
+Goal forall x p2 p1 m,
+ x <> 0%Z ->
+ (Z.abs (x * p2 ) > Z.abs (Z.abs p1 + Z.abs m))%Z ->
+ (Z.abs (x * (p1 + x * p2 )) > Z.abs m)%Z.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+
+Goal forall z z0 z1 m
+ (Heqz0 : z0 = ((1 + z) * z1)%Z)
+ (H0 : (0 <= m)%Z)
+ (H3 : z = m)
+ (H1 : (0 <= z0)%Z)
+ (H4 : z1 = z0)
+ (H2 : (z1 > 0)%Z),
+ (z1 > z)%Z.
+Proof.
+ intros.
+ Time nia.
+Qed.
+
+
+
+
+(* Known issues.
+
+ - Found proof may violate Proof using ...
+ There may be a compliant proof but lia has no way to know.
+ Proofs could be optimised to minimise the number of hypotheses,
+ but this seems to costly.
+Section S.
+ Variable z z0 z1 z2 : Z.
+ Variable H2 : 0 <= z2.
+ Variable H3 : z2 < z1.
+ Variable H4 : 0 <= z0.
+ Variable H5 : z0 < z1.
+ Variable H6 : z = - z2.
+
+ Goal -z1 -z2 >= 0 -> False.
+ Proof using H2 H3 H6.
+ intros.
+ lia.
+ Qed.
+*)
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index bd52270100..52dc9ed2e0 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -72,6 +72,14 @@ Proof.
psatz R 3.
Qed.
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+Proof.
+ intros.
+ nra.
+Qed.
+
+
+
Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 ) *x^2*y^2) >= 0.
Proof.
intros ; psatz R 2.
@@ -86,3 +94,24 @@ Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
Proof.
lra.
Qed.
+
+(* From L. Théry *)
+
+Goal forall (x y : R), x = 0 -> x * y = 0.
+Proof.
+ intros.
+ nra.
+Qed.
+
+Goal forall (x y : R), 2*x = 0 -> x * y = 0.
+Proof.
+ intros.
+ nra.
+Qed.
+
+
+Goal forall (x y: R), - x*x >= 0 -> x * y = 0.
+Proof.
+ intros.
+ nra.
+Qed.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index d163dfbcd2..7266b662fa 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,21 +11,21 @@ Open Scope Z_scope.
Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2.
Proof.
- intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
+ intros ; case (Zabs_dec x) ; intros ; nia.
Qed.
Hint Resolve Z.abs_nonneg Zabs_square.
Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
Proof.
-intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
+ intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
/\ Z.abs p^2 = p^2) by auto.
assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
- (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
+ (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia).
generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
intros n IHn p [Hn [Hp Heq]].
-assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z 2).
-assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z 2.
+assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; nia).
+assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by nia.
apply (IHn (2*p-n) Hzwf (n-p) Hdecr).
Qed.
diff --git a/test-suite/misc/universes/build_all_stdlib.sh b/test-suite/misc/universes/build_all_stdlib.sh
new file mode 100755
index 0000000000..2d2e6f863b
--- /dev/null
+++ b/test-suite/misc/universes/build_all_stdlib.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+echo "Require $(find ../../../theories ../../../plugins -type f -name "*.v" | \
+ sed 's/^.*\/theories\///' | sed 's/^.*\/plugins\///' | sed 's/\.v$//' | sed 's/\//./g') ."
diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune
new file mode 100644
index 0000000000..58bba300d2
--- /dev/null
+++ b/test-suite/misc/universes/dune
@@ -0,0 +1,8 @@
+(rule
+ (targets all_stdlib.v)
+ (deps
+ (source_tree ../../../theories)
+ (source_tree ../../../plugins))
+ (action
+ (with-outputs-to all_stdlib.v
+ (run ./build_all_stdlib.sh))))
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 352e422cf7..36992e4dda 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -7,6 +7,6 @@ Require Import QMicromega.
Require Import RMicromega.
Recursive Extraction
- List.map RingMicromega.simpl_cone (*map_cone indexes*)
- denorm Qpower vm_add
- n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+ List.map simpl_cone (*map_cone indexes*)
+ denorm Qpower vm_add
+ normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index 751d5fcc48..1a9bc068c5 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -1,5 +1,9 @@
Module N : S with Definition T := nat := M
+Module N : S with Definition T := M
+
Module N : S with Module T := K := M
+Module N : S with Module T := M
+
Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 5f30f7cda6..54ef305be4 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -1,3 +1,5 @@
+(* Bug #2169 *)
+
Module FOO.
Module M.
@@ -12,6 +14,10 @@ Module N : S with Definition T := nat := M.
Print Module N.
+Set Short Module Printing.
+Print Module N.
+Unset Short Module Printing.
+
End FOO.
Module BAR.
@@ -31,8 +37,14 @@ Module N : S with Module T := K := M.
Print Module N.
+Set Short Module Printing.
+Print Module N.
+Unset Short Module Printing.
+
End BAR.
+(* Bug #4661 *)
+
Module QUX.
Module Type Test.
diff --git a/test-suite/success/btauto.v b/test-suite/success/btauto.v
new file mode 100644
index 0000000000..d2512b5cbb
--- /dev/null
+++ b/test-suite/success/btauto.v
@@ -0,0 +1,9 @@
+Require Import Btauto.
+
+Open Scope bool_scope.
+
+Lemma test_orb a b : (if a || b then negb (negb b && negb a) else negb a && negb b) = true.
+Proof. btauto. Qed.
+
+Lemma test_xorb a : xorb a a = false.
+Proof. btauto. Qed.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 2863404590..28426b5700 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,7 +60,7 @@ Qed.
Record U : Type := { A:=Type; a:A }.
-(** Check assignement of sorts to inductives and records. *)
+(** Check assignment of sorts to inductives and records. *)
Variable sh : list nat.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 17:05:00 +0000