Proof Simplification

Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of this kind of needless data contained in proof files.

Useless data

As a reminder about the structure of proof trees, one can have a look at the Proof Manager page. The idea here is to remove unnecessary actions on hypotheses. These include:

• 'forward' on a hypothesis when the inferred predicate is never used afterwards
• 'hide' of an unused forward-generated hypothesis
• 'select' of an hypothesis that is never used afterwards

These actions are stored in antecedents. After removing unneeded actions of an antecedent, it may become empty and can thus be itself removed. These antecedents are stored in rules. After removing unneeded antecedents, the rule may become empty. But the rule is linked to the node it is applied to, so we cannot remove the rule without removing the corresponding proof tree node. Here, we have to distinguish 3 cases, depending on the number of children a proof tree node has:

• 0 child: it is a leaf of the proof tree, we cannot remove it without obtaining a pending node
• 2 or more children: it is a branching node, we cannot remove it because the children could not be 'plugged' anywhere else
• 1 child: if the rule is empty, the step is unnecessary and can be skipped, 'plugging' its only child node to its parent node

Automatic and manual simplification

In order to simplify a proof, it is necessary to determine for each of its nodes if some data is needless. But, when the proof is not complete, some data that is not yet used might become valuable in a further step. Thus, only discharged proofs are simplifiable.

The main goal is to reduce the size of the proof file, so the simplification should take place before the storage of the proof. But before the user saves its proof, he or she is modifying it, so the proof is unstable and undischarged. Therefore, the simplification has to take place at proof saving, when the proof is committed.

But when a project is imported, it may also contain proofs with useless data. So a new user action has been added to the contextual menu of proof obligations, event-B components and projects: "Simplify Proof(s)". It allows to manually trigger proof simplification.

Implementation approach

Since we have to determine for each node if the predicates it refers to are used in its subtree, it is necessary to gather informations about the subtree before processing a node. The approach consists in a depth-first postorder traversal of the closed proof tree, remembering in each branch which predicates are needed. It is then possible to simplify the nodes according to the above stated principles.