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.
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
Require Import PP.Ppform.
The tactic is named ppsimpl
Examples can be found in file examples/PpsimplEx.v
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.