diff --git a/.travis.yml b/.travis.yml index e35ed21..85aa5b8 100644 --- a/.travis.yml +++ b/.travis.yml @@ -47,21 +47,27 @@ jobs: # Test supported versions of Coq via Nix - env: - - COQ=8.8 + - COQ=https://github.com/coq/coq-on-cachix/tarball/master <<: *NIX - env: - - COQ=8.9 + - COQ=8.12 + <<: *NIX + - env: + - COQ=8.11 <<: *NIX - env: - COQ=8.10 <<: *NIX - env: - - COQ=8.11 + - COQ=8.9 + <<: *NIX + - env: + - COQ=8.8 <<: *NIX # Test supported versions of Coq via OPAM - env: - - COQ_IMAGE=coqorg/coq:8.11 + - COQ_IMAGE=coqorg/coq:dev - PACKAGE=coq-bertrand.dev - NJOBS=2 <<: *OPAM diff --git a/Knuth_why.v b/Knuth_why.v index 7ba8a47..1a5c0a8 100644 --- a/Knuth_why.v +++ b/Knuth_why.v @@ -17,6 +17,7 @@ Require Import Zwf. Require Import Bertrand. Require Import WhyArrays. Require Import Knuth_def. +Require Import Lia. Arguments well_founded [A]. (*Why*) Parameter n : Z. @@ -394,7 +395,7 @@ split. intros k (H2, H3); replace k with (m1 + 1)%Z; auto with zarith. red in |- *; intros (H4, H5); Contradict H5. replace (Z.abs_nat (m1 + 1)) with (S (Z.abs_nat m1)). -apply prime_not_prime_S; auto with zarith. +apply prime_not_prime_S. case (prime_2_or_more (Z.abs_nat (access a1 (i1 - 1)))). case Pre7; intros H5 (H6, (H7, (H8, (H9, H10)))); case (H9 (i1 - 1)%Z); auto with zarith. @@ -439,7 +440,7 @@ unfold lexZ, pairZ in |- *; apply left_lex; auto with zarith. split; auto with zarith. split; auto with zarith. apply prime_def1. -apply le_lt_trans with (Z.abs_nat (access a1 (i1 - 1))); auto with zarith. +apply le_lt_trans with (Z.abs_nat (access a1 (i1 - 1))). apply le_Zle_inv. simpl in |- *; rewrite inj_abs; auto with zarith. apply lt_Zlt_inv. @@ -474,14 +475,14 @@ apply Z.lt_le_trans with (1 := H7); auto with zarith. case (Zle_lt_or_eq j2 (i1 - 1)); auto with zarith; intros H8. apply Zlt_le_weak; intuition. rewrite H8; auto with zarith. -apply Z.le_lt_trans with s1; auto with zarith. +apply Z.le_lt_trans with s1. replace (Z_of_nat p) with (Z_of_nat (Misc.sqr (p * p))). rewrite Post5; unfold sqr in |- *. apply Znat.inj_le; auto with arith; apply sqr_mono; auto with arith. rewrite sqr_mult2; auto. case Post12; intros (H10, H11) [(H12, H13)| (H12, H13)]; try discriminate; auto with zarith. -omega. +lia. (* b2 = false *) intros j2 Post12. split. case Post12; intros (H1, H2) [(H3, H4)| (H3, H4)]; try discriminate. @@ -496,15 +497,15 @@ intros x (H5, (H6, H7)). case (Zle_or_lt (2 * access a1 (i1 - 1)) (m1 + 2)); auto. intros H8; absurd (Zprime (Z_of_nat x)); auto with zarith. case Pre7; intros (H9, H9') (H10, (H11, (H12, H13))). -apply H12; split; auto with zarith. +apply H12; split. rewrite <- (inj_abs (access a1 (i1 - 1))); auto with zarith. case (Zle_lt_or_eq (Z_of_nat x) m1); auto with zarith. -case (Zle_lt_or_eq (Z_of_nat x) (m1 + 1)); auto with zarith. +case (Zle_lt_or_eq (Z_of_nat x) (m1 + 1)); [|auto with zarith|]. apply Zlt_succ_le. -apply Z.lt_le_trans with (2 * access a1 (i1 - 1))%Z; auto with zarith. -rewrite <- (inj_abs (2 * access a1 (i1 - 1))); auto with zarith. +apply Z.lt_le_trans with (2 * access a1 (i1 - 1))%Z; [|auto with zarith]. +rewrite <- (inj_abs (2 * access a1 (i1 - 1))); [|auto with zarith]. rewrite absolu_comp_mult. -replace (Z.abs_nat 2) with 2; auto with zarith. +replace (Z.abs_nat 2) with 2; [|auto with zarith]. apply Znat.inj_lt; auto. intros H14; absurd (Zprime (Z_of_nat x)). rewrite H14. @@ -573,7 +574,7 @@ rewrite H11; rewrite <- absolu_comp_mult. replace (2 * x + 1 + 1)%Z with ((x + 1) * 2)%Z; auto with zarith. intuition. rewrite H; unfold lexZ, pairZ in |- *; apply right_lex; auto with zarith. -unfold Zwf in |- *; omega. +unfold Zwf in |- *; lia. Qed. (* Why obligation from file "Knuth.mlw", characters 481-1499 *) diff --git a/README.md b/README.md index 8cb33e2..1daec11 100644 --- a/README.md +++ b/README.md @@ -35,7 +35,7 @@ application using Bertrand's postulate. - Coq-community maintainer(s): - Hugo Herbelin ([**@herbelin**](https://github.com/herbelin)) - License: [GNU Lesser General Public License v2.1 or later](LICENSE) -- Compatible Coq versions: Coq 8.8 to 8.11 +- Compatible Coq versions: Coq 8.8 or later - Additional dependencies: none - Coq namespace: `Bertrand` - Related publication(s): diff --git a/coq-bertrand.opam b/coq-bertrand.opam index 017e002..6a7ff41 100644 --- a/coq-bertrand.opam +++ b/coq-bertrand.opam @@ -18,7 +18,7 @@ application using Bertrand's postulate. build: [make "-j%{jobs}%" ] install: [make "install"] depends: [ - "coq" {>= "8.8" & < "8.12~"} + "coq" {(>= "8.8" & < "8.13~") | (= "dev")} ] tags: [ diff --git a/meta.yml b/meta.yml index d9fc475..7f1316e 100644 --- a/meta.yml +++ b/meta.yml @@ -32,17 +32,19 @@ license: identifier: LGPL-2.1-or-later supported_coq_versions: - text: Coq 8.8 to 8.11 - opam: '{>= "8.8" & < "8.12~"}' + text: Coq 8.8 or later + opam: '{(>= "8.8" & < "8.13~") | (= "dev")}' tested_coq_nix_versions: -- version_or_url: "8.8" -- version_or_url: "8.9" -- version_or_url: "8.10" +- version_or_url: https://github.com/coq/coq-on-cachix/tarball/master +- version_or_url: "8.12" - version_or_url: "8.11" +- version_or_url: "8.10" +- version_or_url: "8.9" +- version_or_url: "8.8" tested_coq_opam_versions: -- version: "8.11" +- version: "dev" namespace: Bertrand diff --git a/why/WhyArrays.v b/why/WhyArrays.v index c6b0b0a..dc57ac1 100644 --- a/why/WhyArrays.v +++ b/why/WhyArrays.v @@ -33,6 +33,7 @@ (* $Id$ *) Require Export ZArith. +Require Import Lia. (**************************************) (* Functional arrays, for use in Why. *) @@ -126,11 +127,11 @@ Ltac AccessStore i j H := [ intro H; rewrite H; rewrite store_def_1; WhyArrays | intro H; rewrite store_def_2; [ idtac | idtac | idtac | exact H ] ]. -Ltac AccessSame := rewrite store_def_1; WhyArrays; try omega. +Ltac AccessSame := rewrite store_def_1; WhyArrays; try lia. -Ltac AccessOther := rewrite store_def_2; WhyArrays; try omega. +Ltac AccessOther := rewrite store_def_2; WhyArrays; try lia. -Ltac ArraySubst t := subst t; simpl in |- *; WhyArrays; try omega. +Ltac ArraySubst t := subst t; simpl in |- *; WhyArrays; try lia. (* Syntax and pretty-print for arrays *) @@ -140,4 +141,4 @@ Ltac ArraySubst t := subst t; simpl in |- *; WhyArrays; try omega. Syntax constr level 0 : array_access [ << (access ($VAR $t) $c) >> ] -> [ "#" $t "[" $c:L "]" ]. -***) \ No newline at end of file +***)