catalin-hritcu / rippling Goto Github PK

Inductive proof automation for Coq
by Sean Wilson

This package contains an inductive proof automation plugin for Coq. This automation
includes a rippling tactic, generalisation heuristics and a counterexample finder tool.
This file explains how to compile the code and run the demo file (see theory/demo.v),
which includes many examples of theorems that can be automated. See here for documentation
about how the automation works:
http://homepages.inf.ed.ac.uk/s0091720/

These tactics are still in development. The code and the installation process should
hopefully be simplified in the future.

Note that this code has only been tested under Linux so far.