Contribution: MapleMode

A Maple Mode for Coq

Authors

Description

This contribution is an interface between Coq and Maple. In particular, this exports the functions simplify/factor/expand/normal giving the corresponding tactics Simplify/Factor/Expand/Normal. The manipulations carried out by these tactics are proved thanks to the tactic Field. These tactics can be also used as functions by means of the Eval ... In command.

Keywords

maple, simplification, field tactic

README

(* README *)

(************************)
(* A Maple Mode for Coq *)
(************************)

Requirements:
============

    This contribution requires Maple V Release 5 or higher versions. The
executable "maple" (exactly with this name) must be accessible (in your PATH).
Otherwise, you can specify another name as well as a path using the MAPLE
environment variable (this variable has priority over the executable "maple"
which may be in your PATH).

Compilation and use:
===================

    Just type "make" and load the module Maple with "Require Import Maple.".

Description:
===========

    This contribution is an interface between Coq and Maple. In particular,
this exports the functions simplify/factor/expand/normal of Maple giving the
corresponding tactics Simplify/Factor/Expand/Normal. These tactics are
described as follows:

    o simplify term_0 ... term_n

    This tactic simplifies the terms term_0 ... term_n (using the function
simplify of Maple) and replaces them in the conclusion of the current goal by
the resulting simplified terms. There must be a field theory (see the Reference
Manual) declared for the type of these terms.

    o factor term_0 ... term_n

    This tactic factorizes the terms term_0 ... term_n (using the function
factor of Maple) and replaces them in the conclusion of the current goal by
the resulting factorized terms. There must be a field theory (see the Reference
Manual) declared for the type of these terms.

    o expand term_0 ... term_n

    This tactic factorizes the terms term_0 ... term_n (using the function
factor of Maple) and replaces them in the conclusion of the current goal by
the resulting expanded terms. There must be a field theory (see the Reference
Manual) declared for the type of these terms.

    o normal term_0 ... term_n

    This tactic factorizes the terms term_0 ... term_n (using the function
factor of Maple) and replaces them in the conclusion of the current goal by
the resulting normalized terms (reduction to the same denominator +
simplification of common factors). There must be a field theory (see the
Reference Manual) declared for the type of these terms.

    These tactics can be also used as functions by means of the Eval ... In
command. This can be as a tactic expression or as a function over terms:

    Definition ident ... := Eval <Maple Tactic> in term.

Examples:
========

    For a complete set of examples, see the file Examples.v.

Maple documentation:
===================

    For a documentation of the corresponding Maple functions, just type:

    ?<function>

    under the Maple toplevel loop.

Extensions:
==========

    If you want to extend this Maple mode with other functions over
multivariate polynomials and if these functions accept only one argument (they
may take other arguments, but as optional arguments), you need to add new
TACTIC EXTEND commands and new declare_red_expr in the file maple.ml.

    If you need to add more complicated functions, please contact the authors.

Implementation notes:
====================

    The functions simplify/factor are not only exported from Maple as functions
for Coq. They are also used as tactics and this is only possible thanks to the
tactic Field. Indeed, given a term t, if t' is the simplified/factorized term,
we must prove that t=t' in order to replace t by t' in the conclusion of the
current goal. This is exactly done using the tactic Field and this explains why
there must be a field theory declared for the type of t.

Contacts:
========

    If you need further information, if you have some remarks or if you have
observed some bugs, please let us know sending us a mail at:

    delahaye@cs.chalmers.se
    mayero@cs.chalmers.se

Ported to Coq 8.x by Hugo Herbelin; support for extensions directly
from the Coq user side still to be done.

Available files