The ppsimpl tactics

OVERVIEW:

The "ppsimpl" tactic aims at preprocessing and simplifying quantifier-free formulae. The tactic is "compiled" based on type classes instances defined by the user. It is extensible and use the principle of proof by reflection. The tactics performs two transformations.

- The first transformation consists in defining type injections and providing compliant operators.

Currently, the nat and positive types are mapped into Z and boolean is mapped to Prop.

- The second transformation consists in replacing functions by their specification.

Example include Z.div, Z.mod, Z.max, Z.sqrt.

In terms of functionality, ppsimpl is similar to zify.

DOWNLOAD:

website repository

INSTALL:

The tactic is known to work with Coq 8.4pl2 & Ocaml 4.01.0 This is pure Coq except for a OCaml plugin declaring "Existing Instance" as a tactic construct. To compile the tactic, run

make

To install, run

make install

ppsimpl is placed in coq/user-contrib/PP

USE:

Require Import PP.Ppform.

The tactic is named ppsimpl

EXAMPLES:

Examples can be found in file examples/PpsimplEx.v

ADDING INSTANCES:

More type-class instances can be added to FOInstance.v If the compilation fails, check that: - All the operators are indeed declared - All the proofs of instances are terminated with Defined.