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 semi-interactive development of machine-checked proofs.
OCaml Coq TeX C Shell CSS
Pull request Compare This branch is 16 commits ahead, 9836 commits behind coq:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
bootstrap
checker
config
dev
doc
grammar
ide
interp
intf
kernel
lib
library
man
parsing
plugins
pretyping
printing
proofs
tactics
test-suite
theories
tools
toplevel
.dir-locals.el
.gitignore
.mailmap
.merlin
CHANGES
COMPATIBILITY
COPYRIGHT
CREDITS
INSTALL
INSTALL.doc
INSTALL.ide
INSTALL.macosx
LICENSE
Makefile
Makefile.build
Makefile.common
Makefile.doc
README
README.doc
README.win
TODO
_tags
build
configure
configure.ml
coq-win32.itarget
coq.itarget
install.sh
myocamlbuild.ml

README

               	         THE IRRELEVANT COQ SYSTEM
            	         =========================

Take Coq.

Add in its syntax (up to kernel/extensions.ml) :
 - Irr : Type(0)
 - iPrf : Irr -> Prop
 - iJMeq : forall {A B: Type}, A -> B -> Irr
 - iSubst : forall {A: Type} (a: A) (b: A)
    (eq: iPrf (iJMeq a b)) (P : A -> Type) (p : P a), P b

Make it typecheck them (kernel/extension_behavior.ml +
kernel/typeops.ml).

Add in its conversion test (kernel/reduction.ml:ccnv) :
G |- p == q : forall (x_1: T_1) ... (x_n: T_n), iPrf A

Add in the reduction machine (kernel/closure.ml) :
      G |- a == b : A
____________________________
G |- isubst a b eq P p ==> p


Of course, Coq reduction machine and conversion test are not typed so
you have cheated by
 - carrying and updating a typing environment that destructs all the performance
 - declaring references "nasty_infer" & "nasty_conv" in kernel/closure.ml
that you set to the latter-defined functions afterward.

Of course, it is completely incomplete and will do "pattern matching
failure" if you try to use cbv reduction machines.

Of course, it is full of bugs such as the one that makes NMake_gen.v
kill your computer if you keep "reflexivity" instead of "exact
eq_refl" at some point. I personnaly stop the massacre after 30Go of
swap!

But at least, you will obtain a playground thus this one ... Sandbox
is open at theories/Irr/Irr.v.