coqlibraryundecidability
corn
coqlibraryundecidability  corn  

2  1  
105  108  
1.0%  0.0%  
4.7  4.3  
7 days ago  24 days ago  
Coq  Coq  
Mozilla Public License 2.0  GNU General Public License v3.0 only 
Stars  the number of stars that a project has on GitHub. Growth  month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
coqlibraryundecidability

Development Environment with guix shell for Coq Package
I want to run guix shell to create an environment with the dependencies required to build coqlibraryundecidability.

Math proof databases
There are two problems. The first is that there is no central repository. Sure, maybe if you're interested in undecidable results you might go here... But it's an island, and so is every other library. Worse yet, there's little inter mixing or combinable ways to use libraries. Unlike other programming languages, automated proof systems have so far been aimed at the technical aspects of a single person proving something, rather than the shareability of proofs.
corn

The Fundamental Theorem of Algebra in ACL2
> Or there are these high level systems for proving deep theorems. Is anyone trying to fill the gap?
There's ongoing work on computable real numbers for instance the CoRN library[1], so hope is on the horizon, for instance, a recent update to the Coq Interval package adds certified plotting, that is, the library guarantees that if a function passes through a pixel, that pixel is filled[2]. There's also the userfriendly Coquelicot[3] real analysis library up to basic differential equations (e.g. Bessel function).
> It'll rearrange an equation but I can't ask it "prove this is increasing"
For a taste, here's my proof that the cube function is increasing[4]. If I wanted to create a tactic that automatically proves a function is increasing, I would use properties of increasing functions[5] to recursively break it down into trivial subcases.
[0] https://github.com/siraben/math3100/blob/master/analysis.v
[1] https://github.com/coqcommunity/corn
[2] https://coq.discourse.group/t/interval42nowwithplotting...
[3] https://hal.inria.fr/hal00860648v1/document
[4] http://ix.io/3rxD
[5] https://www.math24.net/increasingdecreasingfunctions#hpro...
What are some alternatives?
CoqEquations  A function definition package for Coq
CompCert  The CompCert formallyverified C compiler
mathcomp  Mathematical Components
fourcolor  Formal proof of the Four Color Theorem [maintainer=@ybertot]
UniMath  This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
coq  Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semiinteractive development of machinechecked proofs.
verdiraft  An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
magmide  A dependentlytyped proof language intended to make provably correct bare metal code possible for working software engineers.