Almost Full

Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination.

Meta

• Author(s):
  • Dimitrios Vytiniotis (initial)
  • Thierry Coquand (initial)
  • David Wahlstedt (initial)
• Coq-community maintainer(s):
  • Karl Palmskog (@palmskog)
• License: MIT License
• Compatible Coq versions: 8.11 or later
• Additional dependencies: none
• Coq namespace: AlmostFull
• Related publication(s):
  • Stop When You Are Almost-Full doi:10.1007/978-3-642-32347-8_17

Building and installation instructions

The easiest way to install the latest released version of Almost Full is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-almost-full

To instead build and install manually, do:

git clone https://github.com/coq-community/almost-full.git
cd almost-full
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

Included files:

• AlmostFull.v: Basic setup, connections to well-founded relations
• AFConstructions.v: Almost-full relation constructions and type-based combinators
• AlmostFullInduction.v: Various induction principles
• AFExamples.v: Examples
• Terminator.v: Deriving the Terminator proof rule