coq-community / bertrand Goto Github PK
View Code? Open in Web Editor NEWCoq proof of Bertrand's postulate on existence of primes [maintainer=@thery]
License: GNU Lesser General Public License v2.1
Coq proof of Bertrand's postulate on existence of primes [maintainer=@thery]
License: GNU Lesser General Public License v2.1
Hi @Zimmi48: I updated "bertrand" to 8.9 and 8.10 and pushed corresponding tags v8.9.0 and v8.10.0.
I did not create/update an opam package for compilation with 8.9 and 8.10. There is an opam template in the archive which I could use, but I lost track of whom is supposed to be in charge of it (the opam file says it is @palmskog but the header of the repository says it is @herbelin).
The first part of this project, the proof of Bertrand's postulate, is a generic result about primes, and could be useful to a larger audience. One way to accomplish this is to have the proof transferred into the CoqPrime project, which is in the Coq Platform and has regular releases compatible with the latest released version of Coq. However, this may require reorganization and adaptation to CoqPrime idioms.
After a tentative transfer, the project here could focus fully on providing verified programs that use Bertrand's postulate (on top of CoqPrime), both using the Why toolchain and using other means. Such programs and proofs are likely to have a much smaller audience, but are still very valuable to the community.
The Why program (Knuth.mlw
) is unfortunately out of date with respect to recent releases of the Why toolchain; there is a modern Why program version available that is, however, "less verified" than the program here. One way to solve this, and verify fully down to assembly level, would be to convert Knuth.mlw
to C and use VST, bringing the program, its semantics, and the proof all fully into Coq. Such a conversion is not easy, so I will simply leave it here as a cool idea.
My testing while setting up CI for this repository shows that this project is not currently compatible with Coq 8.8 and above (see https://travis-ci.com/Zimmi48/bertrand/builds/78357211).
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.