ssrcoq
small scale reflection library for Coq (theories)
Install
- All systems
-
curl cmd.cat/ssrcoq.sh
- Debian
-
apt-get install libssreflect-coq - Ubuntu
-
apt-get install libssreflect-coq - Kali Linux
-
apt-get install libssreflect-coq - Windows (WSL2)
-
sudo apt-get updatesudo apt-get install libssreflect-coq - Raspbian
-
apt-get install libssreflect-coq - Dockerfile
- dockerfile.run/ssrcoq
libssreflect-coq
small scale reflection library for Coq (theories)
The name Ssreflect stands for "small scale reflection", a style of proof that evolved from the computer-checked proof of the Four Colour Theorem and which leverages the higher-order nature of Coq's underlying logic to provide effective automation for many small, clerical proof steps. This is often accomplished by restating ("reflecting") problems in a more concrete form, hence the name. For example, in the Ssreflect library, arithmetic comparison is not an abstract predicate, but a function computing a boolean. The Ssreflect distribution comprises two parts: * A new tactic language, which promotes more structured, concise and robust proof scripts, and is in fact independent from the "reflection" proof style. It is implemented as a linkable extension to the Coq system. * A set of Coq libraries that provide core "reflection-oriented" theories for basic combinatorics (roughly: arithmetic, lists, and finite sets). This package installs the full Ssreflect distribution.