The PhoX Proof Assistant

Hot news

• Version 0.89: adapted to recent OCaml 4.XX. Remark: not yet adapted to recent ProofGeneral Emacs mode.
• Version 0.85: more bugs fixed, lots of improvement, first experimental version of proof by contextual menu (needs a very recent cvs version of Proof General.
• Version 0.83: more bugs fixed and started to clean the software for more natural names and behavior for commands.
• Version 0.82: more bugs fixed and most of the tutorials translated to english.
• A Windows version is available. See its specific installation instructions.
• New version (version 0.8): better tutorials and documentation.
• Version 0.8 tested successfully under MAC OS X (thanks to Laurent Chéno).
• Coming later (version 0.9): a much more powerful module system.

Contents

PhoX overview

The major design goal of this program was to make as easy as possible the formalization of mathematical proofs on machine. This is quite a hard goal to reach. For instance, if you consider knots theory, you will have great problems to translate your graphical proofs !

However, I have put a lot of work to make it possible to formalize a lot of mathematics quite easily. Here are a list of the features offered by this program (quite a few of them are unique!):

• Proofs are developed in a natural deduction style, but the left rules and cut rule of sequent calculus are also available (offering a maximum freedom).
• Automatic theorem proving is provided to help you finish the easy cases. This is quite useful but there are still a little place for improvement here (coming soon).
• Equational reasoning is provided in two forms: rewriting (you can rewrite a goal or an hypothesis using one or more equations) and automatic (when 2 or 3 equations are needed, and sometimes more, an automatic equational reasoning algorithm can discover for you that two expressions are equal). Moreover, conditional equations are supported (the conditions necessary to apply a given equation may be proven automatically or left to you).
• The rules (sometimes called tactics) can be extended by the user. After defining a predicate, you can prove some new theorems and add them as introduction or elimination rules. You can also control the way the automatic reasoning uses your new rules.
• After finishing a proof, a proof tree is constructed and checked (by a small piece of code). This means that the correctness of your proof is independent from the correctness of the tactics you used (including the automatic reasoning).
• A module system is provided. For instance, you can prove results about groups using the usual axioms on groups and then reuse your results on other groups. In future version, the module system will allow quantifications on modules ...
• The syntax is extensible. This makes your PhoX source files more readable.
• The program can assist you to extract a LaTeX article from your formalization. Formulas from the current context during a proof can be translated into a LaTeX version. You can customized the way these formulas are produced. This means that you can write normal articles because the text is not automatically generated !
• We recommend you use Proof General as an interface using the Xemacs editor. You can have a look at a screen shot.

Documentation

• You can browse the reference manual and the user's manual of the library .
• Otherwise, you may downlad a ps or dvi version of the presious manuals, see the distribution section
• Computer Assisted Teaching in Mathematics is an article describing a teaching experiment using PhoX. This paper constitutes a very good introduction to PhoX, with one detailed example and a short index of the main commands. It is also available in french
• The distribution comes with various kinds of tutorials (in french only). Some of them are intended to learn PhoX, others are intended to learn Mathematics.
• For bug report, send me a mail at the address christophe@raffalli.eu with a precise description of the problem.

Examples

Here is a very simple proof development: a proof of the existence of the quotient and remaining of the euclidain division. You can browse

• The PhoX source enriched with LaTeX comments
• A resulting LaTeX article

The team

All people working on PhoX were member of the Laboratory of Mathematic of the Savoy University or the Logic Team of Paris VII university. Although some part of the code where written while C. Raffalli was at L.F.C.S. in Edinburgh or at Chalmers university.

Christophe Raffalli

Christophe.Raffalli@univ-savoie.fr
Author of most of the implementation.

Philippe Curmin

curmin@logique.jussieu.fr
P. Curmin is working on a marking algorithm to optimise extracted programs. This work should be useful in future versions.

Pascal Manoury

eleph@logique.jussieu.fr
P. Manoury may port in the future the ProPre system within PhoX. This should allow a lot of totality proofs to be automatized (proof that a given equational definition of a function always terminates)

Paul Roziere

roziere@logique.jussieu.fr
P. Roziere formalized quite a few proofs in the system and is responsible for most of the emacs mode.

PhoX distribution (0.89)

• use opam install phox, need ocaml <= 4.08.1 because it uses camlp4 (suggest --unlock-base)
• Source are on github
• You will need Objective Caml (version 3.08 to 4.08.1) to use and install the Unix version.
• You can also browse the manuals:
• Reference manual
• Users manual of the library