diff options
Diffstat (limited to 'test-suite')
32 files changed, 417 insertions, 160 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f5ec80bcfc..93ce519350 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -127,14 +127,14 @@ clean: $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ - \) -print0 | xargs -0 rm -f + \) -exec rm -f {} + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' $(HIDE)find unit-tests \( \ -name '*.cmx' -o -name '*.cmi' -o -name '*.o' -o -name '*.test' \ - \) -print0 | xargs -0 rm -f + \) -exec rm -f {} + distclean: clean $(SHOW) 'RM <**/*.aux>' - $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f + $(HIDE)find . -name '*.aux' -exec rm -f {} + ####################################################################### # Per-subsystem targets @@ -196,10 +196,7 @@ PRINT_LOGS:=APPVEYOR endif #APPVEYOR report: summary.log - $(HIDE)bash save-logs.sh - $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi - $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi + $(HIDE)bash report.sh ####################################################################### # Regression (and progression) tests diff --git a/test-suite/bugs/2428.v b/test-suite/bugs/closed/2428.v index a4f587a58d..b398a76d91 100644 --- a/test-suite/bugs/2428.v +++ b/test-suite/bugs/closed/2428.v @@ -5,6 +5,6 @@ Definition myFact := forall x, P x. Hint Extern 1 (P _) => progress (unfold myFact in *). Lemma test : (True -> myFact) -> P 3. -Proof. +Proof. intros. debug eauto. Qed. diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v index c401420e94..791889b24b 100644 --- a/test-suite/bugs/closed/2670.v +++ b/test-suite/bugs/closed/2670.v @@ -15,6 +15,14 @@ Proof. refine (match e return _ with refl_equal => _ end). reflexivity. Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as a in _ = b return _ with refl_equal => _ end). + reflexivity. + Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as z in _ = y return _ with refl_equal => _ end). + reflexivity. + Undo 2. (* Next line similarly has a dependent and a non dependent solution *) refine (match e with refl_equal => _ end). reflexivity. diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/closed/4623.v index 7ecfd98b67..7ecfd98b67 100644 --- a/test-suite/bugs/4623.v +++ b/test-suite/bugs/closed/4623.v diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/closed/4624.v index f5ce981cd0..f5ce981cd0 100644 --- a/test-suite/bugs/4624.v +++ b/test-suite/bugs/closed/4624.v diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v index 1507fa4bf0..bd9bac37ef 100644 --- a/test-suite/bugs/closed/4717.v +++ b/test-suite/bugs/closed/4717.v @@ -19,8 +19,6 @@ Proof. omega. Qed. -Require Import ZArith ROmega. - Open Scope Z_scope. Definition Z' := Z. @@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m, Proof. intros. omega. - Undo. - romega. Qed. diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/closed/7333.v index fba5b9029d..fba5b9029d 100644 --- a/test-suite/bugs/7333.v +++ b/test-suite/bugs/closed/7333.v diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v new file mode 100644 index 0000000000..229df93773 --- /dev/null +++ b/test-suite/bugs/closed/7754.v @@ -0,0 +1,21 @@ + +Set Universe Polymorphism. + +Module OK. + + Inductive one@{i j} : Type@{i} := + with two : Type@{j} := . + Check one@{Set Type} : Set. + Fail Check two@{Set Type} : Set. + +End OK. + +Module Bad. + + Fail Inductive one := + with two@{i +} : Type@{i} := . + + Fail Inductive one@{i +} := + with two@{i +} := . + +End Bad. diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v new file mode 100644 index 0000000000..c4b29a6354 --- /dev/null +++ b/test-suite/bugs/closed/8215.v @@ -0,0 +1,14 @@ +(* Check that instances for local definitions in evars have compatible body *) +Goal False. +Proof. + pose (n := 1). + evar (m:nat). + subst n. + pose (n := 0). + Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *) + clearbody n. + Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *) + clear n. + pose (n := 0+1). + Check ?m. (* Should be ok *) +Abort. diff --git a/test-suite/bugs/closed/8432.v b/test-suite/bugs/closed/8432.v new file mode 100644 index 0000000000..844ee12668 --- /dev/null +++ b/test-suite/bugs/closed/8432.v @@ -0,0 +1,39 @@ +Require Import Program.Tactics. + +Obligation Tactic := idtac. +Set Universe Polymorphism. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Inductive Empty : Type :=. +Inductive Unit : Type := tt. +Definition not (A : Type) := A -> Empty. + + Lemma nat_path_O_S (n : nat) (H : paths O (S n)) : Empty. + Proof. refine ( + match H in paths _ i return + match i with + | O => Unit + | S _ => Empty + end + with + | idpath _ => tt + end + ). Defined. + Lemma symmetry {A} (x y : A) (p : paths x y) : paths y x. + Proof. + destruct p. apply idpath. + Defined. + Lemma nat_path_S_O (n : nat) (H : paths (S n) O) : Empty. + Proof. eapply nat_path_O_S. exact (symmetry _ _ H). Defined. +Set Printing Universes. +Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) := +match n as n return not (paths (S n) 0) with +| 0 => nat_path_S_O _ +| S n' => let dummy := succ_not_zero n' in _ +end. +Next Obligation. + intros f _ n dummy H. exact (nat_path_S_O _ H). + Show Universes. +Defined. diff --git a/test-suite/bugs/closed/8532.v b/test-suite/bugs/closed/8532.v new file mode 100644 index 0000000000..00aa66e701 --- /dev/null +++ b/test-suite/bugs/closed/8532.v @@ -0,0 +1,8 @@ +(* Checking Print Assumptions relatively to a bound module *) + +Module Type Typ. + Parameter Inline(10) t : Type. +End Typ. +Module Terms_mod (SetVars : Typ). +Print Assumptions SetVars.t. +End Terms_mod. diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh new file mode 100755 index 0000000000..e066ac039b --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/poly-capture-global-univs/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs + +if make; then + >&2 echo 'Should have failed!' + exit 1 +fi diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore new file mode 100644 index 0000000000..f5a6d22b8e --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/.gitignore @@ -0,0 +1 @@ +/Makefile* diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject new file mode 100644 index 0000000000..70ec246062 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Evil +-I src + +src/evil.ml4 +src/evilImpl.ml +src/evilImpl.mli +src/evil_plugin.mlpack +theories/evil.v + diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 new file mode 100644 index 0000000000..565e979aaa --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 @@ -0,0 +1,9 @@ + +open Stdarg +open EvilImpl + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] +END diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml new file mode 100644 index 0000000000..6d8ce7c5d7 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -0,0 +1,22 @@ +open Names + +let evil t f = + let open Univ in + let open Entries in + let open Decl_kinds in + let open Constr in + let k = IsDefinition Definition in + let u = Level.var 0 in + let tu = mkType (Universe.make u) in + let te = Declare.definition_entry + ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu + in + let tc = Declare.declare_constant t (DefinitionEntry te, k) in + let tc = mkConst tc in + + let fe = Declare.definition_entry + ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~types:(Term.mkArrow tc tu) + (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) + in + ignore (Declare.declare_constant f (DefinitionEntry fe, k)) diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli new file mode 100644 index 0000000000..97c7e3dadd --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli @@ -0,0 +1,2 @@ + +val evil : Names.Id.t -> Names.Id.t -> unit diff --git a/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack new file mode 100644 index 0000000000..0093328a40 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack @@ -0,0 +1,2 @@ +EvilImpl +Evil diff --git a/test-suite/misc/poly-capture-global-univs/theories/evil.v b/test-suite/misc/poly-capture-global-univs/theories/evil.v new file mode 100644 index 0000000000..7fd98c2773 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/theories/evil.v @@ -0,0 +1,13 @@ + +Declare ML Module "evil_plugin". + +Evil T f. (* <- if this doesn't fail then the rest goes through *) + +Definition g : Type -> Set := f. + +Require Import Hurkens. + +Lemma absurd : False. +Proof. + exact (TypeNeqSmallType.paradox (g Type) eq_refl). +Qed. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index b60b1ee863..94b86fc222 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -125,13 +125,15 @@ s : nat fun _ : nat => 9 : nat -> nat -fun (x : nat) (p : x = x) => match p with - | ONE => ONE - end = p +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| ONE => ONE +end = p : forall x : nat, x = x -> Prop -fun (x : nat) (p : x = x) => match p with - | 1 => 1 - end = p +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| 1 => 1 +end = p : forall x : nat, x = x -> Prop bar 0 : nat diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v deleted file mode 100644 index 2c373d5052..0000000000 --- a/test-suite/output/Quote.v +++ /dev/null @@ -1,36 +0,0 @@ -Require Import Quote. - -Parameter A B : Prop. - -Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula - | f_const : Prop -> formula. - -Fixpoint interp_f (vm: - varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - | f_const c => c - end. - -Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B). -intro H. -match goal with - | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H) -end. -match goal with - |- ?g => quote interp_f [ A ] in g using (fun x => idtac x) -end. -quote interp_f. -Show. -simpl; quote interp_f [ A ]. -Show. -Admitted. diff --git a/test-suite/report.sh b/test-suite/report.sh new file mode 100755 index 0000000000..05f39b4b02 --- /dev/null +++ b/test-suite/report.sh @@ -0,0 +1,55 @@ +#!/usr/bin/env bash + +# save failed logs to logs/, then print failure information +# returns failure code if any failed logs exist + +# save step + +SAVEDIR="logs" + +# reset for local builds +rm -rf "$SAVEDIR" +mkdir "$SAVEDIR" + +# keep this synced with test-suite/Makefile +FAILMARK="==========> FAILURE <==========" + +FAILED=$(mktemp /tmp/coq-check-XXXXXX) +find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" + +rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" +cp summary.log "$SAVEDIR"/ + +# cleanup +rm "$FAILED" + +# print info +if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then + find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do + if [ -n "$TRAVIS" ]; then + # ${foo////.} replaces every / by . in $foo + printf 'travis_fold:start:coq.logs.%s\n' "${file////.}"; + else printf '%s\n' "$file" + fi + + cat "$file" + + if [ -n "$TRAVIS" ]; then + # ${foo////.} replaces every / by . in $foo + printf 'travis_fold:end:coq.logs.%s\n' "${file////.}"; + else printf '\n' + fi + done +fi + +if grep -q -F 'Error!' summary.log ; then + echo FAILURES; + grep -F 'Error!' summary.log; + if [ -z "$TRAVIS" ] && [ -z "$PRINT_LOGS" ]; then + echo 'To print details of failed tests, rerun with environment variable PRINT_LOGS=1' + echo 'eg "make report PRINT_LOGS=1" from the test suite directory"' + echo 'See README.md in the test suite directory for more information.' + fi + false +else echo NO FAILURES; +fi diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh deleted file mode 100755 index 9b8fff09f8..0000000000 --- a/test-suite/save-logs.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -SAVEDIR="logs" - -# reset for local builds -rm -rf "$SAVEDIR" -mkdir "$SAVEDIR" - -# keep this synced with test-suite/Makefile -FAILMARK="==========> FAILURE <==========" - -FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" - -rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" -cp summary.log "$SAVEDIR"/ - -# cleanup -rm "$FAILED" diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 0df3d5685d..a97afa7ff0 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -1,5 +1,7 @@ - -Require Import ZArith ROmega. +(* This file used to test the `romega` tactics. + In Coq 8.9 (end of 2018), these tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) +Require Import ZArith Lia. (* Submitted by Xavier Urbain 18 Jan 2002 *) @@ -7,14 +9,14 @@ Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. -romega. +lia. Qed. (* Proposed by Pierre Crégut *) Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. intro. - romega. + lia. Qed. (* Proposed by Jean-Christophe Filliâtre *) @@ -22,7 +24,7 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. -romega. +lia. Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) @@ -32,7 +34,7 @@ Section A. Variable x y : Z. Hypothesis H : (x > y)%Z. Lemma lem4 : (x > y)%Z. - romega. + lia. Qed. End A. @@ -48,7 +50,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1. Hypothesis M : (H <= 2 * S)%Z. Hypothesis N : (S < H)%Z. Lemma lem5 : (H > 0)%Z. - romega. + lia. Qed. End B. @@ -56,11 +58,10 @@ End B. Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. - romega. + lia. Qed. (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) -Require Import Omega. Section C. Parameter g : forall m : nat, m <> 0 -> Prop. Parameter f : forall (m : nat) (H : m <> 0), g m H. @@ -68,23 +69,21 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - romega with nat. + lia. Qed. End C. (* Problem of dependencies *) -Require Import Omega. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. intros. -romega with nat. +lia. Qed. (* Bug that what caused by the use of intro_using in Omega *) -Require Import Omega. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. intros. -romega with nat. +lia. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) @@ -92,5 +91,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; romega with nat. +intros; lia. Qed. diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 3ddf6a40fb..7f69422ab3 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -1,25 +1,27 @@ -Require Import ZArith ROmega. +Require Import ZArith Lia. Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) +(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) -Lemma test_romega_0 : +Lemma test_lia_0 : forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_0b : +Lemma test_lia_0b : forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. -romega. +lia. Qed. -Lemma test_romega_1 : +Lemma test_lia_1 : forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> @@ -29,10 +31,10 @@ Lemma test_romega_1 : z >= 0. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_1b : +Lemma test_lia_1b : forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> @@ -42,24 +44,24 @@ Lemma test_romega_1b : z >= 0. Proof. intros z z1 z2. -romega. +lia. Qed. -Lemma test_romega_2 : forall a b c:Z, +Lemma test_lia_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_2b : forall a b c:Z, +Lemma test_lia_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. -romega. +lia. Qed. -Lemma test_romega_3 : forall a b h hl hr ha hb, +Lemma test_lia_3 : forall a b h hl hr ha hb, 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> @@ -70,10 +72,10 @@ Lemma test_romega_3 : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_3b : forall a b h hl hr ha hb, +Lemma test_lia_3b : forall a b h hl hr ha hb, 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> @@ -84,79 +86,79 @@ 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. -romega. +lia. Qed. -Lemma test_romega_4 : forall hr ha, +Lemma test_lia_4 : forall hr ha, ha = 0 -> (ha = 0 -> hr =0) -> hr = 0. Proof. intros hr ha. -romega. +lia. Qed. -Lemma test_romega_5 : forall hr ha, +Lemma test_lia_5 : forall hr ha, ha = 0 -> (~ha = 0 \/ hr =0) -> hr = 0. Proof. intros hr ha. -romega. +lia. Qed. -Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False. +Lemma test_lia_6 : forall z, z>=0 -> 0>z+2 -> False. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False. +Lemma test_lia_6b : forall z, z>=0 -> 0>z+2 -> False. Proof. intros z. -romega. +lia. Qed. -Lemma test_romega_7 : forall z, +Lemma test_lia_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_7b : forall z, +Lemma test_lia_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -romega. +lia. Qed. (* Magaud BZ#240 *) -Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. +Lemma test_lia_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. +Lemma test_lia_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. intros x y. -romega. +lia. Qed. (* Besson BZ#1298 *) -Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. +Lemma test_lia9 : forall z z':Z, z<>z' -> z'=z -> False. Proof. intros. -romega. +lia. Qed. (* Letouzey, May 2017 *) -Lemma test_romega10 : forall x a a' b b', +Lemma test_lia10 : forall x a a' b b', a' <= b -> a <= b' -> b < b' -> @@ -164,5 +166,5 @@ Lemma test_romega10 : forall x a a' b b', a <= x < b' <-> a <= x < b \/ a' <= x < b'. Proof. intros. - romega. + lia. Qed. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 43eda67ea3..e3b090699d 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -1,4 +1,6 @@ -Require Import ZArith ROmega. +(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) +Require Import ZArith Lia. (* Submitted by Yegor Bryukhov (BZ#922) *) @@ -13,7 +15,7 @@ forall v1 v2 v5 : Z, 0 < v2 -> 4*v2 <> 5*v1. intros. -romega. +lia. Qed. @@ -37,5 +39,5 @@ forall v1 v2 v3 v4 v5 : Z, ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9)) -> False. intros. -romega. +lia. Qed. diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v index fd4ff260b5..ef9cb17b4b 100644 --- a/test-suite/success/ROmega3.v +++ b/test-suite/success/ROmega3.v @@ -1,10 +1,14 @@ -Require Import ZArith ROmega. +Require Import ZArith Lia. Local Open Scope Z_scope. (** Benchmark provided by Chantal Keller, that romega used to solve far too slowly (compared to omega or lia). *) +(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) + + Parameter v4 : Z. Parameter v3 : Z. Parameter o4 : Z. @@ -27,5 +31,5 @@ Lemma lemma_5833 : (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. Proof. -Timeout 1 romega. (* should take a few milliseconds, not seconds *) +Timeout 1 lia. (* should take a few milliseconds, not seconds *) Timeout 1 Qed. (* ditto *) diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v index 58ae5b8fb8..a724592749 100644 --- a/test-suite/success/ROmega4.v +++ b/test-suite/success/ROmega4.v @@ -3,12 +3,12 @@ See also #148 for the corresponding improvement in Omega. *) -Require Import ZArith ROmega. +Require Import ZArith Lia. Open Scope Z. Goal let x := 3 in x = 3. intros. -romega. +lia. Qed. (** Example seen in #4132 @@ -22,5 +22,5 @@ Lemma foo (H : - zxy' <= zxy) (H' : zxy' <= x') : - b <= zxy. Proof. -romega. +lia. Qed. diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v index fa659273e1..6ca32f450f 100644 --- a/test-suite/success/ROmegaPre.v +++ b/test-suite/success/ROmegaPre.v @@ -1,127 +1,123 @@ -Require Import ZArith Nnat ROmega. +Require Import ZArith Nnat Lia. Open Scope Z_scope. (** Test of the zify preprocessor for (R)Omega *) +(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) (* More details in file PreOmega.v - - (r)omega with Z : starts with zify_op - (r)omega with nat : starts with zify_nat - (r)omega with positive : starts with zify_positive - (r)omega with N : starts with uses zify_N - (r)omega with * : starts zify (a saturation of the others) *) (* zify_op *) Goal forall a:Z, Z.max a a = a. intros. -romega with *. +lia. Qed. Goal forall a b:Z, Z.max a b = Z.max b a. intros. -romega with *. +lia. Qed. Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. -romega with *. +lia. Qed. Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. -romega with *. +lia. Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. -intuition; subst; romega. (* pure multiplication: omega alone can't do it *) +intuition; subst; lia. (* pure multiplication: omega alone can't do it *) Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. intros. -romega with *. +lia. Qed. Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. -romega with *. +lia. Qed. (* zify_nat *) Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. intros. -romega with *. +lia. Qed. Goal forall m:nat, (m<1)%nat -> (m=0)%nat. intros. -romega with *. +lia. Qed. Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. intros. -romega with *. +lia. Qed. (* 2000 instead of 200: works, but quite slow *) Goal forall m: nat, (m*m>=0)%nat. intros. -romega with *. +lia. Qed. (* zify_positive *) Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. intros. -romega with *. +lia. Qed. Goal forall m:positive, (m<2)%positive -> (m=1)%positive. intros. -romega with *. +lia. Qed. Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. intros. -romega with *. +lia. Qed. Goal forall m: positive, (m*m>=1)%positive. intros. -romega with *. +lia. Qed. (* zify_N *) Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. intros. -romega with *. +lia. Qed. Goal forall m:N, (m<1)%N -> (m=0)%N. intros. -romega with *. +lia. Qed. Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. intros. -romega with *. +lia. Qed. Goal forall m:N, (m*m>=0)%N. intros. -romega with *. +lia. Qed. (* mix of datatypes *) Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. -romega with *. +lia. Qed. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v new file mode 100644 index 0000000000..1c6e2d81d8 --- /dev/null +++ b/test-suite/success/Template.v @@ -0,0 +1,48 @@ +Set Printing Universes. + +Module AutoYes. + Inductive Box (A:Type) : Type := box : A -> Box A. + + About Box. + + (* This checks that Box is template poly, see module No for how it fails *) + Universe i j. Constraint i < j. + Definition j_lebox (A:Type@{j}) := Box A. + Definition box_lti A := Box A : Type@{i}. + +End AutoYes. + +Module AutoNo. + Unset Auto Template Polymorphism. + Inductive Box (A:Type) : Type := box : A -> Box A. + + About Box. + + Universe i j. Constraint i < j. + Definition j_lebox (A:Type@{j}) := Box A. + Fail Definition box_lti A := Box A : Type@{i}. + +End AutoNo. + +Module Yes. + #[template] + Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A. + + About Box. + + Universe i j. Constraint i < j. + Definition j_lebox (A:Type@{j}) := Box A. + Definition box_lti A := Box A : Type@{i}. + +End Yes. + +Module No. + #[notemplate] + Inductive Box (A:Type) : Type := box : A -> Box A. + + About Box. + + Universe i j. Constraint i < j. + Definition j_lebox (A:Type@{j}) := Box A. + Fail Definition box_lti A := Box A : Type@{i}. +End No. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index b287b5facf..e1df9ba84a 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -559,3 +559,26 @@ split. - (* clear b:True *) match goal with H:_ |- _ => clear H end. (* use a:0=0 *) match goal with H:_ |- _ => exact H end. Qed. + +(* Test choice of most dependent solution *) +Goal forall n, n = 0 -> exists p, p = n /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. (* Compatibility tells [?p:=n] rather than [?p:=0] *) +exact H. (* this checks that the goal is [n=0], not [0=0] *) +Qed. + +(* Check insensitivity to alphabetic order of names*) +(* In both cases, the last name is conventionally chosen *) +(* Before 8.9, the name coming first in alphabetic order *) +(* was chosen. *) +Goal forall m n, m = n -> n = 0 -> exists p, p = n /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. +exact H0. +Qed. + +Goal forall n m, n = m -> m = 0 -> exists p, p = m /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. +exact H0. +Qed. diff --git a/test-suite/vio/numeral.v b/test-suite/vio/numeral.v new file mode 100644 index 0000000000..f28355bb29 --- /dev/null +++ b/test-suite/vio/numeral.v @@ -0,0 +1,21 @@ +Lemma foo : True. +Proof. +Check 0 : nat. +Check 0 : nat. +exact I. +Qed. + +Lemma bar : True. +Proof. +pose (0 : nat). +exact I. +Qed. + +Require Import Coq.Strings.Ascii. +Open Scope char_scope. + +Lemma baz : True. +Proof. +pose "s". +exact I. +Qed. |