Coq8.18

.github/workflows/docker-action.yml

@@ -18,11 +18,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

.github/workflows/replay-why3.yml

@@ -18,7 +18,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
-          custom_image: 'coqorg/coq:8.13'
+          custom_image: 'coqorg/coq:8.18'
           custom_script: |
             {{before_install}}
             startGroup "Build bertrand dependencies"

README.md

@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/bertrand/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/bertrand/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/bertrand/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/bertrand/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -37,7 +37,7 @@ an application of the postulate to compute partitions.
 - Coq-community maintainer(s):
   - Laurent Théry ([**@thery**](https://github.com/thery))
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
-- Compatible Coq versions: Coq 8.12 or later
+- Compatible Coq versions: Coq 8.18 or later
 - Additional dependencies: none
 - Coq namespace: `Bertrand`
 - Related publication(s):
@@ -101,15 +101,15 @@ let part30 = part 15;;
 ## Replaying the WhyML program correctness proof
 
 To replay the proof of correctness for the WhyML program for computing primes,
-first make sure the following packages are installed (in addition to Coq 8.13.2
+first make sure the following packages are installed (in addition to Coq 8.18.0
 and the proof of Bertrand's postulate):
 
-- [Alt-Ergo 2.4.1](https://alt-ergo.ocamlpro.com)
+- [Alt-Ergo 2.5.4](https://alt-ergo.ocamlpro.com)
 - [Why3 1.4.1](http://why3.lri.fr) and its Coq library
 
 These packages can be installed via OPAM using the following command:
 ```
-opam install alt-ergo.2.4.1 why3.1.4.1 why3-coq.1.4.1
+opam install alt-ergo.2.5.4 why3.1.7.2 why3-coq.1.7.2
 ```
 Then, the proof can be replayed by running
 ```

coq-bertrand.opam

@@ -19,7 +19,7 @@ an application of the postulate to compute partitions."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.12" & < "8.18~") | (= "dev")}
+  "coq" {(>= "8.18" & < "8.20~") | (= "dev")}
 ]
 
 tags: [

coq-knuth-prime-whyml.opam

@@ -18,10 +18,10 @@ build: [
   [make "why"]
 ]
 depends: [
-  "coq" {= "8.13.2"}
-  "why3" {= "1.4.1"}
-  "why3-coq" {= "1.4.1"}
-  "alt-ergo" {= "2.4.1"}
+  "coq" {= "8.18.0"}
+  "why3" {= "1.7.2"}
+  "why3-coq" {= "1.7.2"}
+  "alt-ergo" {= "2.5.4"}
   "coq-bertrand" {= version}
 ]
 

meta.yml

@@ -31,16 +31,13 @@ license:
   identifier: LGPL-2.1-or-later
 
 supported_coq_versions:
-  text: Coq 8.12 or later
-  opam: '{(>= "8.12" & < "8.18~") | (= "dev")}'
+  text: Coq 8.18 or later
+  opam: '{(>= "8.18" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: 'dev'
-- version: '8.16'
-- version: '8.15'
-- version: '8.14'
-- version: '8.13'
-- version: '8.12'
+- version: '8.19'
+- version: '8.18'
 
 tested_coq_nix_versions:
 - coq_version: 'master'
@@ -95,15 +92,15 @@ documentation: |
   ## Replaying the WhyML program correctness proof
 
   To replay the proof of correctness for the WhyML program for computing primes,
-  first make sure the following packages are installed (in addition to Coq 8.13.2
+  first make sure the following packages are installed (in addition to Coq 8.18.0
   and the proof of Bertrand's postulate):
 
-  - [Alt-Ergo 2.4.1](https://alt-ergo.ocamlpro.com)
+  - [Alt-Ergo 2.5.4](https://alt-ergo.ocamlpro.com)
   - [Why3 1.4.1](http://why3.lri.fr) and its Coq library
 
   These packages can be installed via OPAM using the following command:
   ```
-  opam install alt-ergo.2.4.1 why3.1.4.1 why3-coq.1.4.1
+  opam install alt-ergo.2.5.4 why3.1.7.2 why3-coq.1.7.2
   ```
   Then, the proof can be replayed by running
   ```

theories/Partition.v

@@ -19,7 +19,7 @@
                                          Laurent.Thery@inria.fr (2002)
   *********************************************************************)
 
-From Coq Require Import Div2 Even Wf_nat Arith ArithRing List.
+From Coq Require Import Wf_nat Arith ArithRing List.
 From Bertrand Require Import Bertrand.
 
 (*** All these theorems are in coq 8.16 *)

why/Knuth/Knuth_Knuth_h_5.v → why/Knuth/Knuth_Knuth_h_6.v

@@ -53,16 +53,20 @@ Parameter mixfix_lblsmnrb:
   forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z -> a ->
   array a.
 
+Axiom mixfix_lblsmnrb'spec'0 :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (a1:array a) (i:Numbers.BinNums.Z) (v:a),
+  ((length (mixfix_lblsmnrb a1 i v)) = (length a1)).
+
 Axiom mixfix_lblsmnrb'spec :
   forall {a:Type} {a_WT:WhyType a},
   forall (a1:array a) (i:Numbers.BinNums.Z) (v:a),
-  ((length (mixfix_lblsmnrb a1 i v)) = (length a1)) /\
   ((elts (mixfix_lblsmnrb a1 i v)) = (map.Map.set (elts a1) i v)).
 
 Parameter make:
   forall {a:Type} {a_WT:WhyType a}, Numbers.BinNums.Z -> a -> array a.
 
-Axiom make'spec :
+Axiom make_spec :
   forall {a:Type} {a_WT:WhyType a},
   forall (n:Numbers.BinNums.Z) (v:a), (0%Z <= n)%Z ->
   (forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < n)%Z ->
@@ -167,9 +171,20 @@ Axiom H11 : (0%Z <= j1)%Z.
 
 Axiom H12 : (j1 < i)%Z.
 
-Axiom H13 : ~ ((b1 = Init.Datatypes.true) /\ ((mixfix_lbrb a2 j1) <= s)%Z).
+Parameter o: Init.Datatypes.bool.
+
+Parameter o1: Numbers.BinNums.Z.
+
+Axiom H13 :
+  ((b1 = Init.Datatypes.true) ->
+   (o1 = (mixfix_lbrb a2 j1)) /\
+   ((o1 <= s)%Z -> (o = Init.Datatypes.true)) /\
+   (~ (o1 <= s)%Z -> (o = Init.Datatypes.false))) /\
+  (~ (b1 = Init.Datatypes.true) -> (o = Init.Datatypes.false)).
+
+Axiom H14 : ~ (o = Init.Datatypes.true).
 
-Axiom H14 : ~ (b1 = Init.Datatypes.true).
+Axiom H15 : ~ (b1 = Init.Datatypes.true).
 
 Parameter m1: Numbers.BinNums.Z.
 
@@ -193,3 +208,6 @@ assert (H5 : x = Z.to_nat n1); try lia.
 apply H1; try lia.
 exists (Z.to_nat y); lia.
 Qed.
+
+
+