diff options
Diffstat (limited to 'test-suite')
30 files changed, 323 insertions, 106 deletions
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/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/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 7326f137c2..8a00cd3fe5 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,25 +1,25 @@ The command has indeed failed with message: -The user-defined tactic "Top.foo" was not fully applied: +The user-defined tactic "foo" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There are missing arguments for variables y and _, an argument was provided for variable x. The command has indeed failed with message: -The user-defined tactic "Top.baz" was not fully applied: +The user-defined tactic "baz" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.qux" was not fully applied: +The user-defined tactic "qux" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.mydo" was not fully applied: +The user-defined tactic "mydo" was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: @@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.rec" was not fully applied: +The user-defined tactic "rec" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v new file mode 100644 index 0000000000..422bb95fdf --- /dev/null +++ b/test-suite/ssr/ssrpattern.v @@ -0,0 +1,7 @@ +Require Import ssrmatching. + +Goal forall n, match n with 0 => 0 | _ => 0 end = 0. +Proof. + intro n. + ssrpattern (match _ with 0 => _ | S n' => _ end). +Abort. 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/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/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v index 83fb3d0c8e..241d4eb200 100644 --- a/test-suite/success/attribute-syntax.v +++ b/test-suite/success/attribute-syntax.v @@ -1,4 +1,4 @@ -From Coq Require Program. +From Coq Require Program.Wf. Section Scope. @@ -21,3 +21,13 @@ Fixpoint f (n: nat) {wf lt n} : nat := _. #[deprecated(since="8.9.0")] Ltac foo := foo. + +Module M. + #[local] #[polymorphic] Definition zed := Type. + + #[local, polymorphic] Definition kats := Type. +End M. +Check M.zed@{_}. +Fail Check zed. +Check M.kats@{_}. +Fail Check kats. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 4404ff3f16..448febed25 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -377,3 +377,30 @@ f y true. Abort. End LtacNames. + +(* Test binding of the name of existential variables in Ltac *) + +Module EvarNames. + +Ltac pick x := eexists ?[x]. +Goal exists y, y = 0. +pick foo. +[foo]:exact 0. +auto. +Qed. + +Ltac goal x := refine ?[x]. + +Goal forall n, n + 0 = n. +Proof. + induction n; [ goal Base | goal Rec ]. + [Base]: { + easy. + } + [Rec]: { + simpl. + now f_equal. + } +Qed. + +End EvarNames. 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. |