The PhoX Proof Assistant

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.
• 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 and uses math symbols represented by unicode characters. 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 ! This feature will likely be replaced by a generation of web page.

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

Christophe Raffalli

christophe@raffalli.eu
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.

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, before we used proof general.

PhoX distribution and documentation (0.90)

• You can try and use PhoX online
• Source are on github
• You will need Objective Caml (version 4.14 or 5.xx) to use and install the Unix version.
• You can also browse the manuals:
• Reference manual
• Users manual of the library

Changes

• Version 0.90 (2024): adapted to OCaml 5.XX + web version.
• Version 0.89 (2017): adapted to 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 1.0 or probably never): a much more powerful module system. The idea is to add a form of record with subtyping to have first class module in the logique. This also requires quantification over sort in formulas.