GitHub - stepchowfun/proofs: A selection of formal proofs in Coq.
source link: https://github.com/stepchowfun/proofs
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Proofs
This is my personal repository of formally verified mathematics, including results from category theory, type theory, domain theory, etc. The proofs are verified using the Coq proof assistant.
If you want to set up your own repository of formally verified mathematics, you can simply fork this repository and replace the contents of the proofs directory with your own proofs. Setting up a Coq project from scratch is not particularly straightforward, so this scaffolding can save you time.
If you are new to Coq, the repository contains a tutorial here. I recommend Software Foundations and Certified Programming with Dependent Types for further learning.
Instructions
Make sure you have the dependencies listed below. Then you can run make in this directory to verify all the proofs. If you change anything, run make again to to incrementally verify the affected proofs. You can run the linters with make lint. The build artifacts can be removed with make clean.
To write proofs, you'll want to use an IDE that supports interactive theorem proving. My general recommendation is VsCoq, which is a plugin for Visual Studio Code. However, you may find the built-in CoqIDE easier if you're new to interactive theorem proving, since it has buttons you can click on to step through your proofs.
Dependencies
You'll need the following:
- Coq >= 8.15.0
- Make sure to update your
PATHto include the location of the Coq binaries (coqc,coqdep, etc.).
- Make sure to update your
- GNU Make >= 3.79.1
- You also need these common Unix tools:
echo,find, andrm. If you havemake, you probably already have those other programs too.
- You also need these common Unix tools:
- Ruby >= 2.6.8
- This is only needed by
make lint.
- This is only needed by
Recommend
-
28
This is an appendix to Freek Wiedijk's webpage on the "top 100" mathematical theorems , to keep track of the statements of the theorems that are fo...
-
41
我第一次听说 Coq 是在本科的时候。从那以后我就一直很想学 Coq，但是并不知道怎么开始。大部分的 Coq 教程都是在讲逻辑，我觉得并不是很有趣。 上个学期我选了
-
39
Advent of Code 2018 in Coq This repository contains solutions for the Advent of Code 2018 ( https://adventofcode.com/2018 ). Some of them are formally verified. T...
-
20
Announcements SkySkimmer
-
26
I haven’t written anything here in a while, which is mostly due to my paper about syntactic metaprogramming. It is close to being finished, but the remaining edits terrify me right now, so I thought I’d write my thoughts a...
-
4
coq/Logic.v at 6b10edbe056f38d784258b6bf3ea4b8dc472e472 · coq/coq · GitHubPermalink 568 lines (439 sloc)...
-
11
Tagref Tagref helps you maintain cross-references in your code. You can use it to help keep things in sync, document assumptions, manage invariants, etc. Airbnb uses it for their front-end monorepo. You should use it too! Wha...
-
5
Typical: data interchange with algebraic data types Typical is a data serialization framework. You define data types in a file called a schema, th...
-
3
EasyCrypt: Computer-Aided Cryptographic Proofs EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based c...
-
4
Breadcrumbs/069-coq-roadmap.md...
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK