Description

The SSREFLECT package is an extension module for the Coq proof assistant developed at INRIA. It implements a set of proof tactics designed to support the extensive use of small-scale reflection in formal proofs—using the internal computation of the formal system to automate reliably and efficiently the trivial operations that tend to clutter formal proofs. Many of the new features supported by SSREFLECT should actually be of interest to most advanced users of Coq; they include support for better layout and control flow in proof scripts, as well as for maintaining and enforcing precise dataflow. SSREFLECT also provides unified facilities for precise induction loading and intensive rewriting. The reflection-specific features are comparatively modest: a short theory file and a "view" feature that enables switching seemlessly between the new computational style and the traditional deductive style of proof. For better results, the SSREFLECT package should be compiled and statically linked with the standard Coq system. Finally, the package is fully backward compatible; Coq proofs that do not use the new features should compile unchanged with the extended system.