=== SyDRec : Systematic Development of Recursive programs ===

DESCRIPTION

This plugin for Coq provides tools to construct and derive programs in
the BMF style.

The module SyDRec.Morphisms provides the 'Catamorphism' command, which
generate a catamorphism function and a fusion theorem according to an
arbitrary inductive type definition. A similar command 'Paramorphism'
is also provided.

The module SyDRec.Constructive provides the 'beta' tactic as well as
other tools for constructive proofs (mostly extending the type sig to
n-ary propositions).

REQUIREMENTS

This module is known to be compatible with Coq 8.4. Other versions
have not been tested, and the module is almost certainly NOT
compatible with versions 8.2 or earlier.

TO INSTALL

from the top directory:

make
make install (may require super-user privileges)
make clean

TO USE

In coq, load the modules with:

Require SyDRec.Constructive.
Require SyDRec.Morphisms.

CATAMORPHISM AND PARAMORPHISM COMMANDS

To use the Catamorphism command:

Catamorphism foo.

where foo is a reference to an inductive type. This command generates
two definitions 'cata_foo' and 'cata_foo_fusion', which correspond to
the catamorphism function (generalized fold) over type foo and its
fusion theorem.

The use of the paramorphism command is similar.

BETA TACTIC

beta

This tactic performs beta-expansion. It applies to a goal of the form
{f x = e} and yields the goal {f = (fun x0 => e0)} where {e0} is {e[x :=
x0]} This tactic is mostly useful when f is an existential variable. It
can be used to solve higher-order equations.

Error messages:

1. The goal does not have the required form: f x = e

OTHER TOOLS AND TACTICS

Other tools and tactics are documented in the file Constructive.v as
well as the examples provided.