diff options
Diffstat (limited to 'test-suite')
23 files changed, 728 insertions, 105 deletions
diff --git a/test-suite/bugs/closed/bug_12365.v b/test-suite/bugs/closed/bug_12365.v new file mode 100644 index 0000000000..a8e2bb459d --- /dev/null +++ b/test-suite/bugs/closed/bug_12365.v @@ -0,0 +1,8 @@ +Parameter a b : nat. +Parameter p : a = b. + +Goal exists (_ : True) (_ : exists x, x = b), True. +Proof. + exists I, (ex_intro _ a p). + exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_12390.v b/test-suite/bugs/closed/bug_12390.v new file mode 100644 index 0000000000..a8fda29a6f --- /dev/null +++ b/test-suite/bugs/closed/bug_12390.v @@ -0,0 +1,3 @@ +Fail Inductive foo : forall P, P := . +Fail Inductive bar : nat := . +Fail Inductive baz : _ := . diff --git a/test-suite/bugs/closed/bug_12418.v b/test-suite/bugs/closed/bug_12418.v new file mode 100644 index 0000000000..cf11ea627b --- /dev/null +++ b/test-suite/bugs/closed/bug_12418.v @@ -0,0 +1,29 @@ +(* The second "match" below used to raise an anomaly *) + +Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := + { ret : forall {t : Type@{d}}, t -> m t }. + +Record state {S : Type} (t : Type) : Type := mkState { runState : t }. + +Global Declare Instance Monad_state : forall S, Monad (@state S). + +Class Cava := { + constant : bool -> unit; + constant_vec : unit; +}. + +Axiom F : forall {A : Type}, (bool -> A) -> Datatypes.unit. + +Fail Instance T : Cava := { + + constant b := match b with + | true => ret tt + | false => ret tt + end; + + constant_vec := @F _ (fun b => match b with + | true => tt + | false => tt + end); + +}. diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v new file mode 100644 index 0000000000..0d034a65eb --- /dev/null +++ b/test-suite/bugs/closed/bug_12483.v @@ -0,0 +1,10 @@ +Require Import Floats. + +Goal False. +Proof. +cut (false = true). +{ intro H; discriminate H. } +change false with (1 <= 0)%float. +rewrite leb_spec. +Fail reflexivity. +Abort. diff --git a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v index f3bc1767da..94ee23f38e 100644 --- a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v +++ b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v @@ -4,92 +4,143 @@ Require Import QArith Qabs. Require Import ConstructiveCauchyRealsMult. +Require Import Lqa. +Require Import Lia. Local Open Scope CReal_scope. -Definition approx_sqrt_Q (q : Q) (n : positive) : Q +(* We would need a shift instruction on positives to do this properly *) + +Definition CReal_sqrt_Q_seq (q : Q) (n : Z) : Q := let (k,j) := q in match k with | Z0 => 0 - | Z.pos i => Z.pos (Pos.sqrt (i*j*n*n)) # (j*n) + | Z.pos i => match n with + | Z0 + | Z.pos _ => Z.pos (Pos.sqrt (i*j)) # (j) + | Z.neg n' => Z.pos (Pos.sqrt (i*j*2^(2*n'))) # (j*2^n') + end | Z.neg i => 0 (* unused *) end. -(* Approximation of the square root from below, - improves the convergence modulus. *) -Lemma approx_sqrt_Q_le_below : forall (q : Q) (n : positive), - Qle 0 q -> Qle (approx_sqrt_Q q n * approx_sqrt_Q q n) q. +Local Lemma Pos_pow_twice_r a b : (a^(2*b) = a^b * a^b)%positive. Proof. - intros. destruct q as [k j]. unfold approx_sqrt_Q. - destruct k as [|i|i]. apply Z.le_refl. - pose proof (Pos.sqrt_spec (i * j * n * n)). simpl in H0. - destruct H0 as [H0 _]. - unfold Qle, Qmult, Qnum, Qden. - rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. - apply Pos2Z.pos_le_pos. rewrite (Pos.mul_comm i (j * n * (j * n))). - rewrite <- (Pos.mul_comm j), <- (Pos.mul_assoc j), <- (Pos.mul_assoc j). - apply Pos.mul_le_mono_l. - apply (Pos.le_trans _ _ _ H0). - rewrite <- (Pos.mul_comm n), <- (Pos.mul_assoc n). - apply Pos.mul_le_mono_l. - rewrite (Pos.mul_comm i j), <- Pos.mul_assoc, <- Pos.mul_assoc. - apply Pos.mul_le_mono_l. rewrite Pos.mul_comm. apply Pos.le_refl. - exfalso. unfold Qle, Z.le in H; simpl in H. exact (H eq_refl). + apply Pos2Z.inj. + rewrite Pos2Z.inj_mul. + do 2 rewrite Pos2Z.inj_pow. + rewrite Pos2Z.inj_mul. + apply Z.pow_twice_r. Qed. -Require Import Lia. - -Lemma approx_sqrt_Q_le_below_lia : forall (q : Q) (n : positive), - (0 <= q)%Q -> (approx_sqrt_Q q n * approx_sqrt_Q q n <= q)%Q. +(* Approximation of the square root from below, + improves the convergence modulus. *) +Lemma CReal_sqrt_Q_le_below : forall (q : Q) (n : Z), + (0<=q)%Q -> (CReal_sqrt_Q_seq q n * CReal_sqrt_Q_seq q n <= q)%Q. Proof. - intros. destruct q as [k j]. unfold approx_sqrt_Q. + intros q n Hqpos. destruct q as [k j]. unfold CReal_sqrt_Q_seq. destruct k as [|i|i]. - apply Z.le_refl. - - unfold Qle, Qmult, Qnum, Qden. - pose proof (Pos.sqrt_spec (i * j * n * n)) as Hsqrt; simpl in Hsqrt. - destruct Hsqrt as [Hsqrt _]; apply (Pos.mul_le_mono_l j) in Hsqrt. - lia. - - unfold Qle, Qnum, Qden in H; lia. + - destruct n as [|n|n]. + + pose proof (Pos.sqrt_spec (i * j)) as H. simpl in H. + destruct H as [H _]. + unfold Qle, Qmult, Qnum, Qden. + rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. + apply Pos2Z.pos_le_pos. rewrite (Pos.mul_assoc i j j). + apply Pos.mul_le_mono_r; exact H. + + pose proof (Pos.sqrt_spec (i * j)) as H. simpl in H. + destruct H as [H _]. + unfold Qle, Qmult, Qnum, Qden. + rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. + apply Pos2Z.pos_le_pos. rewrite (Pos.mul_assoc i j j). + apply Pos.mul_le_mono_r; exact H. + + pose proof (Pos.sqrt_spec (i * j * 2^(2*n))) as H. simpl in H. + destruct H as [H _]. + unfold Qle, Qmult, Qnum, Qden. + rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. + apply Pos2Z.pos_le_pos. rewrite (Pos.mul_comm j (2^n)) at 2. + do 3 rewrite Pos.mul_assoc. + apply Pos.mul_le_mono_r. + simpl. + rewrite Pos_pow_twice_r in H at 3. + rewrite Pos.mul_assoc in H. + exact H. + - exact Hqpos. Qed. -Print Assumptions approx_sqrt_Q_le_below_lia. - -Lemma approx_sqrt_Q_lt_above : forall (q : Q) (n : positive), - Qle 0 q -> Qlt q ((approx_sqrt_Q q n + (1#n)) * (approx_sqrt_Q q n + (1#n))). +Lemma CReal_sqrt_Q_lt_above : forall (q : Q) (n : Z), + (0 <= q)%Q -> (q < ((CReal_sqrt_Q_seq q n + 2^n) * (CReal_sqrt_Q_seq q n + 2^n)))%Q. Proof. - intros. destruct q as [k j]. unfold approx_sqrt_Q. - destruct k as [|i|i]. reflexivity. - 2: exfalso; unfold Qle, Z.le in H; simpl in H; exact (H eq_refl). - pose proof (Pos.sqrt_spec (i * j * n * n)). simpl in H0. - destruct H0 as [_ H0]. - apply (Qlt_le_trans - _ (((Z.pos ((Pos.sqrt (i * j * n * n)) + 1) # j * n)) - * ((Z.pos ((Pos.sqrt (i * j * n * n)) + 1) # j * n)))). - unfold Qlt, Qmult, Qnum, Qden. - rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. - apply Pos2Z.pos_lt_pos. - rewrite Pos.mul_comm, <- Pos.mul_assoc, <- Pos.mul_assoc, Pos.mul_comm. - apply Pos.mul_lt_mono_r. rewrite Pplus_one_succ_r in H0. - refine (Pos.le_lt_trans _ _ _ _ H0). rewrite Pos.mul_comm. - apply Pos.mul_le_mono_r. - rewrite <- Pos.mul_assoc, (Pos.mul_comm i), <- Pos.mul_assoc. - apply Pos.mul_le_mono_l. rewrite Pos.mul_comm. apply Pos.le_refl. - setoid_replace (1#n)%Q with (Z.pos j#j*n)%Q. 2: reflexivity. - rewrite Qinv_plus_distr. - unfold Qle, Qmult, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. - discriminate. apply Z.mul_le_mono_nonneg. - discriminate. 2: discriminate. - rewrite Pos2Z.inj_add. apply Z.add_le_mono_l. - apply Pos2Z.pos_le_pos. destruct j; discriminate. - rewrite Pos2Z.inj_add. apply Z.add_le_mono_l. - apply Pos2Z.pos_le_pos. destruct j; discriminate. + intros. destruct q as [k j]. unfold CReal_sqrt_Q_seq. + destruct k as [|i|i]. + - ring_simplify. + setoid_rewrite <- Qpower.Qpower_mult. + setoid_rewrite QExtra.Qzero_eq. + pose proof QExtra.Qpower_pos_lt 2 (n*2)%Z ltac:(lra). + lra. + - destruct n as [|n|n]. + + pose proof (Pos.sqrt_spec (i * j)). simpl in H0. + destruct H0 as [_ H0]. + change (2^0)%Q with 1%Q. + unfold Qlt, Qplus, Qmult, Qnum, Qden. + rewrite Pos.mul_1_r, Z.mul_1_r, Z.mul_1_l. + repeat rewrite <- Pos2Z.inj_add, <- Pos2Z.inj_mul. + apply Pos2Z.pos_lt_pos. + rewrite Pos.mul_assoc. + apply Pos.mul_lt_mono_r. + apply (Pos.lt_le_trans _ _ _ H0). + apply Pos.mul_le_mono; lia. + + pose proof (Pos.sqrt_spec (i * j)). simpl in H0. + destruct H0 as [_ H0]. + rewrite QExtra.Qpower_decomp'. + unfold Qlt, Qplus, Qmult, Qnum, Qden. + rewrite PosExtra.Pos_pow_1_r. + rewrite Pos.mul_1_r, Z.mul_1_r. + rewrite <- Pos2Z.inj_pow; do 2 rewrite <- Pos2Z.inj_mul; rewrite <- Pos2Z.inj_add. + apply Pos2Z.pos_lt_pos. + rewrite Pos.mul_assoc. + apply Pos.mul_lt_mono_r. + apply (Pos.lt_le_trans _ _ _ H0). + apply Pos.mul_le_mono; + pose proof Pos.le_1_l (2 ^ n * j)%positive; lia. + + pose proof (Pos.sqrt_spec (i * j * 2 ^ (2 * n))). simpl in H0. + destruct H0 as [_ H0]. + rewrite <- Pos2Z.opp_pos, Qpower.Qpower_opp. + rewrite QExtra.Qpower_decomp'. + rewrite <- Pos2Z.inj_pow, PosExtra.Pos_pow_1_r, <- QExtra.Qinv_swap_pos. + unfold Qlt, Qplus, Qmult, Qnum, Qden. + repeat rewrite Pos2Z.inj_mul. + ring_simplify. + replace (Z.pos i * Z.pos j ^ 2 * Z.pos (2 ^ n) ^ 4)%Z + with ((Z.pos i * Z.pos j * Z.pos (2 ^ n) ^ 2) * (Z.pos j * Z.pos (2 ^ n) ^ 2))%Z by ring. + replace ( + Z.pos j ^ 3 * Z.pos (2 ^ n) ^ 2 + + 2 * Z.pos j ^ 2 * Z.pos (2 ^ n) ^ 2 * Z.pos (Pos.sqrt (i * j * 2 ^ (2 * n))) + + Z.pos j * Z.pos (2 ^ n) ^ 2 * Z.pos (Pos.sqrt (i * j * 2 ^ (2 * n))) ^ 2)%Z + with ( + (Z.pos j + Z.pos (Pos.sqrt (i * j * 2 ^ (2 * n))))^2 * + (Z.pos j * Z.pos (2 ^ n) ^ 2))%Z by ring. + repeat rewrite Pos2Z.inj_pow. + rewrite <- Z.pow_mul_r by lia. + repeat rewrite <- Pos2Z.inj_mul. + repeat rewrite <- Pos2Z.inj_pow. + repeat rewrite <- Pos2Z.inj_mul. + repeat rewrite <- Pos2Z.inj_add. + apply Pos2Z.pos_lt_pos. + rewrite (Pos.mul_comm n 2); change (2*n)%positive with (n~0)%positive. + apply Pos.mul_lt_mono_r. + apply (Pos.lt_le_trans _ _ _ H0). + apply Pos.mul_le_mono; + pose proof Pos.le_1_l (2 ^ n * j)%positive; lia. + - exfalso; unfold Qle, Z.le in H; simpl in H; exact (H eq_refl). Qed. -Lemma approx_sqrt_Q_pos : forall (q : Q) (n : positive), - Qle 0 q -> Qle 0 (approx_sqrt_Q q n). +Lemma CReal_sqrt_Q_pos : forall (q : Q) (n : Z), + (0 <= (CReal_sqrt_Q_seq q n))%Q. Proof. - intros. unfold approx_sqrt_Q. destruct q, Qnum. - apply Qle_refl. discriminate. apply Qle_refl. + intros. unfold CReal_sqrt_Q_seq. destruct q, Qnum. + - apply Qle_refl. + - destruct n as [|n|n]; discriminate. + - apply Qle_refl. Qed. Lemma Qsqrt_lt : forall q r :Q, @@ -104,46 +155,95 @@ Proof. - exfalso. rewrite q0 in H0. exact (Qlt_irrefl _ H0). Qed. -Lemma approx_sqrt_Q_cauchy : - forall q:Q, QCauchySeq (approx_sqrt_Q q). +Lemma CReal_sqrt_Q_cauchy : + forall q:Q, QCauchySeq (CReal_sqrt_Q_seq q). Proof. intro q. destruct q as [k j]. destruct k. - - intros n a b H H0. reflexivity. - - assert (forall n a b, Pos.le n b -> - (approx_sqrt_Q (Z.pos p # j) a - approx_sqrt_Q (Z.pos p # j) b - < 1 # n)%Q). - { intros. rewrite <- (Qplus_lt_r _ _ (approx_sqrt_Q (Z.pos p # j) b)). + - intros n a b H H0. + change (Qabs _) with 0%Q. + apply QExtra.Qpower_pos_lt; reflexivity. + - assert (forall n a b, (b<=n)%Z -> + (CReal_sqrt_Q_seq (Z.pos p # j) a - CReal_sqrt_Q_seq (Z.pos p # j) b + < 2^n)%Q). + { intros. + pose proof QExtra.Qpower_pos_lt 2 n eq_refl as Hpow. + rewrite <- (Qplus_lt_r _ _ (CReal_sqrt_Q_seq (Z.pos p # j) b)). ring_simplify. apply Qsqrt_lt. - apply (Qle_trans _ (0+(1#n))). rewrite Qplus_0_l. discriminate. - apply Qplus_le_l. apply approx_sqrt_Q_pos. discriminate. + { apply (Qle_trans _ (0+2^n)). lra. + apply Qplus_le_l. apply CReal_sqrt_Q_pos. } apply (Qle_lt_trans _ (Z.pos p # j)). - apply approx_sqrt_Q_le_below. discriminate. - apply (Qlt_le_trans _ ((approx_sqrt_Q (Z.pos p # j) b + (1 # b)) * - (approx_sqrt_Q (Z.pos p # j) b + (1 # b)))). - apply approx_sqrt_Q_lt_above. discriminate. - apply (Qle_trans _ ((approx_sqrt_Q (Z.pos p # j) b + (1 # n)) * - (approx_sqrt_Q (Z.pos p # j) b + (1 # b)))). - apply Qmult_le_r. - apply (Qlt_le_trans _ (0+(1#b))). rewrite Qplus_0_l. reflexivity. - apply Qplus_le_l. apply approx_sqrt_Q_pos. discriminate. - apply Qplus_le_r. unfold Qle; simpl. - apply Pos2Z.pos_le_pos, H. - apply Qmult_le_l. - apply (Qlt_le_trans _ (0+(1#n))). rewrite Qplus_0_l. reflexivity. - apply Qplus_le_l. apply approx_sqrt_Q_pos. discriminate. - apply Qplus_le_r. unfold Qle; simpl. - apply Pos2Z.pos_le_pos, H. } + { apply CReal_sqrt_Q_le_below. discriminate. } + apply (Qlt_le_trans _ ((CReal_sqrt_Q_seq (Z.pos p # j) b + (2^b)) * + (CReal_sqrt_Q_seq (Z.pos p # j) b + (2^b)))). + { apply CReal_sqrt_Q_lt_above. discriminate. } + apply (Qle_trans _ ((CReal_sqrt_Q_seq (Z.pos p # j) b + (2^n)) * + (CReal_sqrt_Q_seq (Z.pos p # j) b + (2^b)))). + { apply Qmult_le_r. + - apply (Qlt_le_trans _ (0+(2^b))). + + rewrite Qplus_0_l. apply QExtra.Qpower_pos_lt. reflexivity. + + apply Qplus_le_l. apply CReal_sqrt_Q_pos. + - apply Qplus_le_r. apply QExtra.Qpower_le_compat. + exact H. discriminate. } + apply QExtra.Qmult_le_compat_nonneg. + - split. + + pose proof CReal_sqrt_Q_pos (Z.pos p # j) b. + lra. + + apply Qle_refl. + - split. + + pose proof CReal_sqrt_Q_pos (Z.pos p # j) b. + pose proof QExtra.Qpower_pos_lt 2 b eq_refl as Hpowb. + lra. + + apply Qplus_le_r. + apply QExtra.Qpower_le_compat. + exact H. discriminate. + } intros n a b H0 H1. apply Qabs_case. intros. apply H, H1. intros. - setoid_replace (- (approx_sqrt_Q (Z.pos p # j) a - approx_sqrt_Q (Z.pos p # j) b))%Q - with (approx_sqrt_Q (Z.pos p # j) b - approx_sqrt_Q (Z.pos p # j) a)%Q. + setoid_replace (- (CReal_sqrt_Q_seq (Z.pos p # j) a - CReal_sqrt_Q_seq (Z.pos p # j) b))%Q + with (CReal_sqrt_Q_seq (Z.pos p # j) b - CReal_sqrt_Q_seq (Z.pos p # j) a)%Q. 2: ring. apply H, H0. - - intros n a b H H0. reflexivity. + - intros n a b H H0. + change (Qabs _) with 0%Q. + apply QExtra.Qpower_pos_lt; reflexivity. Qed. -Definition CReal_sqrt_Q (q : Q) : CReal - := exist _ (approx_sqrt_Q q) (approx_sqrt_Q_cauchy q). +Definition CReal_sqrt_Q_scale (q : Q) : Z + := ((QExtra.Qbound_lt_ZExp2 q + 1)/2)%Z. + +Lemma CReal_sqrt_Q_bound : forall (q : Q), + QBound (CReal_sqrt_Q_seq q) (CReal_sqrt_Q_scale q). +Proof. + intros q k. + unfold CReal_sqrt_Q_scale. + rewrite Qabs_pos. + 2: apply CReal_sqrt_Q_pos. + apply Qsqrt_lt. + 1: apply Qpower.Qpower_pos; discriminate. + destruct (Qlt_le_dec q 0) as [Hq|Hq]. + - destruct q as [[|n|n] d]. + + discriminate Hq. + + discriminate Hq. + + reflexivity. + - apply (Qle_lt_trans _ _ _ (CReal_sqrt_Q_le_below _ _ Hq)). + rewrite <- Qpower.Qpower_plus. + 2: discriminate. + rewrite Z.add_diag, Z.mul_comm. + pose proof Zdiv.Zmod_eq (QExtra.Qbound_lt_ZExp2 q + 1) 2 eq_refl as Hmod. + assert (forall a b c : Z, c=b-a -> a=b-c)%Z as H by (intros a b c H'; rewrite H'; ring). + apply H in Hmod; rewrite Hmod; clear H Hmod. + apply (Qlt_le_trans _ _ _ (QExtra.Qbound_lt_ZExp2_spec q)). + apply QExtra.Qpower_le_compat. 2: discriminate. + pose proof Z.mod_pos_bound (QExtra.Qbound_lt_ZExp2 q + 1)%Z 2%Z eq_refl. + lia. +Qed. +Definition CReal_sqrt_Q (q : Q) : CReal := +{| + seq := CReal_sqrt_Q_seq q; + scale := CReal_sqrt_Q_scale q; + cauchy := CReal_sqrt_Q_cauchy q; + bound := CReal_sqrt_Q_bound q +|}. -Time Eval vm_compute in (proj1_sig (CReal_sqrt_Q 2) (10 ^ 400)%positive). +Time Eval vm_compute in (seq (CReal_sqrt_Q 2) (-1000)%Z). diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh new file mode 100755 index 0000000000..4a50759bdb --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log + +diff -u time-of-build-both.log.expected time-of-build-both.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in new file mode 100644 index 0000000000..1031cb85c5 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in @@ -0,0 +1,58 @@ +./src/Rewriter/PerfTesting/Specific/make.py primes.txt +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq +COQ_MAKEFILE -f _CoqProject > Makefile.coq +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +COQDEP VFILES +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +COQC src/UnsaturatedSolinasHeuristics/Tests.v +Finished transaction in 25.269 secs (24.869u,0.051s) (successful) +src/UnsaturatedSolinasHeuristics/Tests.vo (real: 26.27, user: 25.97, sys: 0.27, mem: 566428 ko) +DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256 +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions +DIFF Crypto.Fancy.Montgomery256.montred256 +DIFF Crypto.Fancy.Barrett256.Prod.MulMod +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions +DIFF Crypto.Fancy.Barrett256.barrett_red256 +DIFF Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs +cp -f AUTHORS fiat-rust/AUTHORS +cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS +cp -f LICENSE fiat-rust/LICENSE diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in new file mode 100644 index 0000000000..b78039b589 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in @@ -0,0 +1,40 @@ +./src/Rewriter/PerfTesting/Specific/make.py primes.txt +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq +COQ_MAKEFILE -f _CoqProject > Makefile.coq +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256 +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions +DIFF Crypto.Fancy.Montgomery256.montred256 +DIFF Crypto.Fancy.Barrett256.Prod.MulMod +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions +DIFF Crypto.Fancy.Barrett256.barrett_red256 +cp -f AUTHORS fiat-rust/AUTHORS +cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS +cp -f LICENSE fiat-rust/LICENSE diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected new file mode 100644 index 0000000000..6a232623bf --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected @@ -0,0 +1,5 @@ + After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) +------------------------------------------------------------------------------------------------------------------------------------------- +0m25.96s | 566428 ko | Total Time / Peak Mem | 0m00.00s | 0 ko || +0m25.96s || 566428 ko | N/A | ∞ +------------------------------------------------------------------------------------------------------------------------------------------- +0m25.97s | 566428 ko | UnsaturatedSolinasHeuristics/Tests.vo | N/A | N/A || +0m25.96s || 566428 ko | ∞ | ∞ diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index 8935759705..123b272a69 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -12,3 +12,4 @@ export COQLIB ./003-non-utf8/run.sh ./004-per-file-fuzz/run.sh ./005-correct-diff-sorting-order-mem/run.sh +./006-zero-before/run.sh diff --git a/test-suite/interactive/ParalITP_fail_on_qed.v b/test-suite/interactive/ParalITP_fail_on_qed.v new file mode 100644 index 0000000000..37692ed254 --- /dev/null +++ b/test-suite/interactive/ParalITP_fail_on_qed.v @@ -0,0 +1,54 @@ +(* Some boilerplate *) +Fixpoint fib n := match n with + | O => 1 + | S m => match m with + | O => 1 + | S o => fib o + fib m end end. + +Ltac sleep n := + try (cut (fib n = S (fib n)); reflexivity). + +(* Tune that depending on your PC *) +Let time := 10. + + +(* Beginning of demo *) + +Section Demo. + +Variable i : True. + +Lemma a (n : nat) : nat. +Proof using. + revert n. + fix f 1. + apply f. +Qed. + +Lemma b : True. +Proof using i. + sleep time. + idtac. + sleep time. + (* Here we use "a" *) + exact I. +Qed. + +Lemma work_here : True /\ True. +Proof using i. +(* Jump directly here, Coq reacts immediately *) +split. + exact b. (* We can use the lemmas above *) +exact I. +Qed. + +End Demo. + +From Coq Require Import Program.Tactics. +Obligation Tactic := idtac. +Program Definition foo : nat -> nat * nat := + fix f (n : nat) := (0,_). + +Next Obligation. +intros f n; apply (f n). +Qed. diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v new file mode 100644 index 0000000000..8fd7398638 --- /dev/null +++ b/test-suite/micromega/zify.v @@ -0,0 +1,229 @@ +Require Import BinNums BinInt ZifyInst Zify. + +Definition pos := positive. + +Goal forall (x : pos), x = x. +Proof. + intros. + zify_op. + apply (@eq_refl Z). +Qed. + +Goal (1 <= Pos.to_nat 1)%nat. +Proof. + zify_op. + apply Z.le_refl. +Qed. + +Goal forall (x : positive), not (x = x) -> False. +Proof. + intros. zify_op. + apply H. + apply (@eq_refl Z). +Qed. + +Goal (0 <= 0)%nat. +Proof. + intros. + zify_op. + apply Z.le_refl. +Qed. + + +Lemma N : forall x, (0 <= Z.of_nat x)%Z. +Proof. + intros. + zify. exact cstr. +Defined. + +Lemma N_eq : N = +fun x : nat => let cstr : (0 <= Z.of_nat x)%Z := Znat.Nat2Z.is_nonneg x in cstr. +Proof. + reflexivity. +Qed. + +Goal (Z.of_nat 1 * 0 = 0)%Z. +Proof. + intros. + zify. + match goal with + | |- (1 * 0 = 0)%Z => reflexivity + end. +Qed. + +Lemma C : forall p, + Z.pos p~1 = Z.pos p~1. +Proof. + intros. + zify_op. + reflexivity. +Defined. + +Lemma C_eq : C = fun p : positive => +let cstr : (0 < Z.pos p)%Z := Pos2Z.pos_is_pos p in eq_refl. +Proof. +reflexivity. +Qed. + + +Goal forall p, + (Z.pos p~1 = 2 * Z.pos p + 1)%Z. +Proof. + intros. + zify_op. + reflexivity. +Qed. + +Goal forall z, + (2 * z = 2 * z)%Z. +Proof. + intros. + zify_op. + reflexivity. +Qed. + +Goal (-1= Z.opp 1)%Z. +Proof. + intros. + zify_op. + reflexivity. +Qed. + +Require Import Lia. + +Goal forall n n3, +S n + n3 >= 0 + n. +Proof. + intros. + lia. +Qed. + +Open Scope Z_scope. + +Goal forall p, + False -> + (Pos.to_nat p) = 0%nat. +Proof. + intros. + zify_op. + match goal with + | H : False |- Z.pos p = Z0 => tauto + end. +Qed. + +Goal forall + fibonacci + (p : positive) + (n : nat) + (b : Z) + (H : 0%nat = (S (Pos.to_nat p) - n)%nat) + (H0 : 0 < Z.pos p < b) + (H1 : Z.pos p < fibonacci (S n)), + Z.abs (Z.pos p) < Z.of_nat n. +Proof. + intros. + lia. +Qed. + + + +Section S. + Variable digits : positive. + Hypothesis digits_ne_1 : digits <> 1%positive. + + Lemma spec_more_than_1_digit : (1 < Z.pos digits)%Z. + Proof. lia. Qed. + + Let digits_gt_1 := spec_more_than_1_digit. + + Goal True. + Proof. + intros. + zify. + exact I. + Qed. + +End S. + + +Record Bla : Type := + mk + { + T : Type; + zero : T + }. + +Definition znat := mk nat 0%nat. + +Require Import ZifyClasses. +Require Import ZifyInst. + +Instance Zero : CstOp (@zero znat : nat) := Op_O. +Add CstOp Zero. + + +Goal @zero znat = 0%nat. + zify. + reflexivity. +Qed. + +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. + intros. + zify_op. + apply Z.add_comm. +Qed. + +Goal forall (x y : nat) (F : forall (P: le x y) , nat) (P : le x y), + (F P + 1 = 1 + F P)%nat. +Proof. + intros. + zify_op. + apply Z.add_comm. +Qed. + +Require Import Bool. + +Goal true && false = false. +Proof. + lia. +Qed. + +Goal forall p, p || true = true. +Proof. + lia. +Qed. + +Goal forall x y, Z.eqb x y = true -> x = y. +Proof. + intros. + lia. +Qed. + +Goal forall x, Z.leb x x = true. +Proof. + intros. + lia. +Qed. + +Goal forall x, Z.gtb x x = false. +Proof. + intros. + lia. +Qed. + +Require Import ZifyBool. + +Goal forall x y : nat, Nat.eqb x 1 = true -> + Nat.eqb y 0 = true -> + Nat.eqb (x + y) 1 = true. +Proof. + intros x y. + lia. +Qed. + +Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0. +Proof. + intros. lia. +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 4c0ee1b5bd..767b3c1922 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -23,11 +23,11 @@ Module Pair (X: PO) (Y: PO) <: PO. Hint Unfold le. Lemma le_refl : forall p : T, le p p. - info auto. + auto. Qed. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. - unfold le; intuition; info eauto. + unfold le; intuition; eauto. Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. @@ -39,9 +39,9 @@ Module Pair (X: PO) (Y: PO) <: PO. enough (t0 = t2) as ->. reflexivity. - info auto. + auto. - info auto. + auto. Qed. End Pair. @@ -53,5 +53,5 @@ Require Nat. Module NN := Pair Nat Nat. Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. - info auto with arith. + auto with arith. Qed. diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v index e63ab1cd48..709ac305e4 100644 --- a/test-suite/output/ErrorLocation_12152_1.v +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -1,3 +1,4 @@ (* Reported in #12152 *) Goal True. intro H; auto. +Abort. diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v index 5df6bec939..29e4c910d8 100644 --- a/test-suite/output/ErrorLocation_12152_2.v +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -1,3 +1,4 @@ (* Reported in #12152 *) Goal True. intros H; auto. +Abort. diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v index 347424b2fc..59c0e1dfc5 100644 --- a/test-suite/output/ErrorLocation_12255.v +++ b/test-suite/output/ErrorLocation_12255.v @@ -2,3 +2,4 @@ Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. Definition i := O. Goal False. can_unfold (i>0). +Abort. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 22268daa83..8d590a797c 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -58,7 +58,7 @@ Recursive Extraction Tauto.abst_form ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add + denorm QArith_base.Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. (* Local Variables: *) diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out index 8d67a4a4b7..010e217efb 100644 --- a/test-suite/output/SuggestProofUsing.out +++ b/test-suite/output/SuggestProofUsing.out @@ -1,7 +1,11 @@ -The proof of nat should start with one of the following commands: +The proof of Nat should start with one of the following commands: Proof using . Proof using Type*. Proof using Type. The proof of foo should start with one of the following commands: Proof using A B. Proof using All. +The proof of sec_exactproof should start with one of the following commands: +Proof using . +Proof using Type*. +Proof using Type. diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v index 00b6f8e183..69bf8d194a 100644 --- a/test-suite/output/SuggestProofUsing.v +++ b/test-suite/output/SuggestProofUsing.v @@ -1,10 +1,22 @@ +Require Program.Tactics. + Set Suggest Proof Using. +Lemma nosec : nat. Proof. exact 0. Qed. + +Lemma nosec_exactproof : bool. Proof false. + +Program Definition nosec_program : nat := _. +Next Obligation. exact 1. Qed. + +Lemma nosec_abstract : nat. +Proof. abstract exact 3. Defined. + Section Sec. Variables A B : Type. (* Some normal lemma. *) - Lemma nat : Set. + Lemma Nat : Set. Proof. exact nat. Qed. @@ -28,4 +40,15 @@ Section Sec. exact A. Defined. + (* No suggest, is this OK? There's nowhere to put it anyway. *) + Program Definition program : nat := _. + Next Obligation. exact 1. Qed. + + (* Must not suggest *) + Lemma sec_abstract : nat. + Proof. abstract exact 3. Defined. + + (* Suggests even though there's nowhere to put it, bug? *) + Lemma sec_exactproof : bool. Proof true. + End Sec. diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v index 92917cdfc7..7b295dd1cb 100644 --- a/test-suite/output/auto.v +++ b/test-suite/output/auto.v @@ -1,4 +1,4 @@ -(* testing info/debug auto/eauto *) +(* testing info_*/debug auto/eauto *) Goal False \/ (True -> True). info_auto. diff --git a/test-suite/output/bug12442.out b/test-suite/output/bug12442.out new file mode 100644 index 0000000000..644ef6cd7c --- /dev/null +++ b/test-suite/output/bug12442.out @@ -0,0 +1,6 @@ +The command has indeed failed with message: +No product even after head-reduction. +The command has indeed failed with message: +Not an inductive product. +The command has indeed failed with message: +Not an inductive product. diff --git a/test-suite/output/bug12442.v b/test-suite/output/bug12442.v new file mode 100644 index 0000000000..481989a4e9 --- /dev/null +++ b/test-suite/output/bug12442.v @@ -0,0 +1,10 @@ +Parameter A B : Prop. +Axiom P : inhabited (A -> B). + +Goal A -> True. +Proof. + Fail intros ?%P ?. + Fail intros []%P. + intro a. + Fail apply P in a as []. +Abort. diff --git a/test-suite/ssr/rewrtite_err_msg.v b/test-suite/ssr/rewrtite_err_msg.v new file mode 100644 index 0000000000..2bbbff433c --- /dev/null +++ b/test-suite/ssr/rewrtite_err_msg.v @@ -0,0 +1,30 @@ +Require Import ssreflect ssrbool. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Axiom finGroupType : Type. +Axiom group : finGroupType -> Type. +Axiom abelian : forall gT : finGroupType, group gT -> Prop. +Arguments abelian {_} _. +Axiom carrier : finGroupType -> Type. +Coercion carrier : finGroupType >-> Sortclass. +Axiom mem : forall gT : finGroupType, gT -> group gT -> Prop. +Arguments mem {_} _ _. +Axiom mul : forall gT : finGroupType, gT -> gT -> gT. +Arguments mul {_} _ _. +Definition centralised gT (G : group gT) (x : gT) := forall y, mul x y = mul y x. +Arguments centralised {gT} _. +Axiom b : bool. + +Axiom centsP : forall (gT : finGroupType) (A B : group gT), + reflect (forall a, mem a A -> centralised B a) b. +Arguments centsP {_ _ _}. + +Lemma commute_abelian (gT : finGroupType) (G : group gT) + (G_abelian : abelian G) (g g' : gT) (gG : mem g G) (g'G : mem g' G) : + mul g g' = mul g' g. +Proof. +Fail rewrite (centsP _). (* fails but without an anomaly *) +Abort. |