proofs's Introduction

Proofs

This is my personal repository of formally verified mathematics, including results from category theory, type theory, domain theory, etc., and some original research. All 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 incrementally verify the affected proofs. 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.17.1
- Make sure to update your PATH to include the location of the Coq binaries (coqc, coqdep, etc.).
GNU Make >= 3.79.1
- You also need these common Unix tools: cp, find, and rm. If you have make, you probably already have those other programs too.

proofs's People

Contributors

Stargazers

Watchers

proofs's Issues

coq 8.19.1 can't find `Coq.Arith.Gt` on Arch

Thought you might like to know. FWIW, just commenting-out the "Require" line causes Coq to fail on the proof t_local_closure_monotonic (attempt to save an incomplete proof).

└──5026:mgh@bree[0,0,4]: make
rm -f \
          .CoqMakefile.d \
          .lia.cache \
          CoqMakefile \
          CoqMakefile.conf \
          _CoqProjectFull
cp _CoqProject _CoqProjectFull
find proofs -type f -name '*.v' >> _CoqProjectFull
coq_makefile -f _CoqProjectFull -o CoqMakefile || (rm -f \
            .CoqMakefile.d \
            .lia.cache \
            CoqMakefile \
            CoqMakefile.conf \
            _CoqProjectFull; \
          exit 1)
make -f CoqMakefile || (rm -f \
            .CoqMakefile.d \
            .lia.cache \
            CoqMakefile \
            CoqMakefile.conf \
            _CoqProjectFull; \
          exit 1)
make[1]: Entering directory '/home/mgh/code/projects/stephan-boyer-proofs'
COQDEP VFILES
Warning: in file proofs/system_f/local_closure.v, library
         Coq.Arith.Gt is required and has not been found in the loadpath!
         [module-not-found,filesystem,default]
Warning: in file proofs/system_f/opening.v, library
         Coq.Arith.Le is required and has not been found in the loadpath!
         [module-not-found,filesystem,default]
COQC proofs/system_f/local_closure.v
File "./proofs/system_f/local_closure.v", line 9, characters 0-28:
Error: Cannot find a physical path bound to logical path Coq.Arith.Gt.

make[2]: *** [CoqMakefile:848: proofs/system_f/local_closure.vo] Error 1
make[2]: *** [proofs/system_f/local_closure.vo] Deleting file 'proofs/system_f/local_closure.glob'
make[1]: *** [CoqMakefile:417: all] Error 2
make[1]: Leaving directory '/home/mgh/code/projects/stephan-boyer-proofs'
make: *** [Makefile:8: verify] Error 1
┌┤ ...stephan-boyer-proofs (Thu Mar 28 07:30:03) 1 usr(s), up 17:30, load 0.67/32, avail. mem 40/62G
│ [M]
└──5027:mgh@bree[2,0,4]: uname -a
Linux bree 6.8.1-arch1-1 #1 SMP PREEMPT_DYNAMIC Sat, 16 Mar 2024 17:15:35 +0000 x86_64 GNU/Linux
┌┤ ...stephan-boyer-proofs (Thu Mar 28 07:30:04) 1 usr(s), up 17:30, load 0.67/32, avail. mem 40/62G
│ [M]
└──5028:mgh@bree[0,0,4]: coqc --version
The Coq Proof Assistant, version 8.19.1
compiled with OCaml 5.1.0
┌┤ ...stephan-boyer-proofs (Thu Mar 28 07:30:08) 1 usr(s), up 17:30, load 0.66/32, avail. mem 40/62G
│ [M]
└──5029:mgh@bree[0,0,4]: make --version
GNU Make 4.4.1

Monotone can be increasing or decreasing

https://github.com/stepchowfun/coq-fun/blob/fc90af9f7a122afd74241ed8414f81926a3b3b00/coq/Kleene.v#L74

Update 2 (removed the strictly) : the code cited here takes only care of increasing monotone function and neglect the decreasing one

https://en.wikipedia.org/wiki/Monotonic_function

Recommend Projects

stepchowfun / proofs Goto Github PK

proofs's Introduction

Proofs

Instructions

Dependencies

proofs's People

Contributors

Stargazers

Watchers

Forkers

proofs's Issues

coq 8.19.1 can't find `Coq.Arith.Gt` on Arch

Monotone can be increasing or decreasing

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent