3.1.7 The Proving Perspective

When proof obligations (POs) (3.2.7) are not discharged automatically, the user can attempt to discharge them interactively using the Proving Perspective. This page provides an overview of the Proving Perspective and its use. If the Proving Perspective is not visible as a tab on the top right-hand corner of the main interface, the user can switch to it via Window Open Perspective.

The Proving Perspective consists of a number of views: the Proof Tree, the Goal, the Selected Hypotheses, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views individually. Figure 3.28 shows an overview of the Proving Perspective.

Figure 3.28: Overview of the Proving Perspective

3.1.7.1 Loading a Proof

To work on an PO that has not yet been discharged, it is necessary to load the proof into the Proving Perspective. To do this, switch to the Proving Perspective. Select the project from the Event-B Explorer and select and expand the component (context or machine). Finally, select (double-click) the proof obligation of interest. A number of views will be updated with details of the corresponding proof.

Note that pressing the button on the top left hand side of the Event-B Explorer will remove all discharged proof obligations (POs) from the view.

3.1.7.2 The Proof Tree

The proof tree view provides a graphical representation of each individual proof step as seen in Figure 3.29.

Figure 3.29: The Proof Tree

The tree is made up of sequents. A line of the tree is shifted to the right when the corresponding node is a direct descendant of the node of the previous line. Each sequent is labeled with a comment which indicates which rule has been applied or which prover discharged the proof. By selecting a sequent in the proof tree, the hypotheses of the sequent are loaded to the Selected Hypotheses window, and the goal of the sequent is loaded to the Goal view.

3.1.7.2.1 Decoration

The symbol to the left of the leaf indicates the state of the sequent:

• indicates that this sequent is discharged.

• indicates that this sequent is not discharged.

• indicates that this sequent has been reviewed.

Internal nodes in the proof display the symbols with the colours inverted. Note that a “reviewed" sequent is one that is not yet discharged by the prover. Instead, it has been “seen" by the user who decided to postpone the proof. Marking sequents as “reviewed" is very convenient since the provers will ignore these leaves and focus on specific areas of interest. This allows the proof to be discharged interactively in a gradual fashion. In order to discharge a “reviewed" sequent, select it and prune the tree at that node: the node will become “brown" again (undischarged), and you can now try to discharge it.

3.1.7.2.2 Navigation within the Proof Tree

There are three buttons on the top of the proof tree view:

• allows you to see the goal of corresponding to each node.

• allows you to fully expand the proof tree.

• allows you to fully collapse the tree; only the root stays visible.

3.1.7.2.3 Manipulating the Proof Tree

3.1.7.2.3.1 Hiding

The button next to each node in the proof tree allows you to expand or collapse the subtree starting at that node.

3.1.7.2.3.2 Pruning

The proof tree can be pruned at a selected node. This means that the subtree of the selected node is removed from the proof tree. The selected node becomes a leaf and displays the symbol . The proof activity can then be resumed from this node. After selecting a node in the proof tree, pruning can be performed in two ways:

• by right-clicking and selecting Prune,

• by clicking on the button in the proof control view.

Note that after pruning, the post-tactic is not applied to the new current sequent. The post-tactic should be applied manually, if required, by clicking on the post-tactic button in the Proof Control view. This is especially useful when you want to redo a proof from the beginning. The proof tree can be pruned at its root node and then the proof can proceed again with invocation of internal or external provers or with an interactive proof.

Before pruning a particular node, the node (and its subtree) can be copied to the clipboard. If the new proof strategy subsequently fails, the copied version can be pasted back into the pruned node (explained further in the next section).

3.1.7.2.3.3 Copy/Paste

By selecting a node in the proof tree and then right-clicking with the mouse, you can copy the part of the proof tree starting at that sequent (including the node and its subtree). Pasting the node and subtree back in is done in a similar manner with a right mouse click on a proof node. This allows you to reuse a part of a proof tree in the same proof or even in another proof.

3.1.7.3 Goal and Selected Hypotheses

Each sequent in the proof tree have corresponding hypotheses and goals. A user will work with one selected sequent at a time by attempting various strategies in an effort to show that the goal is true. The Goal and Selected Hypotheses views provide information to the user about the currently selected sequent. Figure 3.30 shows an example.

Figure 3.30: Open proof obligation

A hypothesis can be removed from the list of selected hypotheses by selecting the check the box situated next to it (you can click on several boxes at once) and then by clicking on the button at the top of the selected hypotheses window.

Note that the deselected hypotheses are not lost. You can find them again using the Search Hypotheses button in the Proof Control view. Other buttons are used as follows:

• - Select all hypotheses.

• - Invert the selection.

• next to the goal - Proof by contradiction 1: The negation of the goal becomes a selected hypothesis and the goal becomes “".

• next to a selected hypothesis - Proof by contradiction 2: The negation of the hypothesis becomes the goal and the negated goal becomes a selected hypothesis.

A user wishing to attempt an interactive proof has a number of proof rules available, and these may either rewrite a hypothesis/goal or infer something from it. In the Goal and the Selected Hypotheses views, various operators may appear in red coloured font. The red font indicates that some interactive proof rule(s) are applicable and may be applied as a step in the proof attempt. When the mouse hovers over such an operator, a number of applicable rules may be displayed; the user may choose to apply one of the rules by clicking on it. Figure 3.31 shows an example.

Other proof rules can be applied when green buttons appear in the Goal and Selected Hypotheses views. Examples are proof by contradiction and conjunction introduction .

Figure 3.31: Applying a rule

To instantiate a quantifier, the user enters the desired expression in the yellow box behind the quantifier and clicks on the quantifier (the red ) as demonstrated in Figure 3.32.

Figure 3.32: Instantiating a quantifier

3.1.7.4 The Proof Control View

The Proof Control view contains the buttons with which you can perform an interactive proof. An overview of this proof can be seen in Figure 3.33.

Figure 3.33: The Proof Control View

The following buttons are available in the Proof Control view:

• invokes the new predicate prover. A drop-down list indicates alternative strategies.

• indicates that a node has been reviewed. In an attempt by the user to carry out sequents in a certain order, they might decide to postpone the task of discharging some sequents until a later stage. To do this, the sequent can be marked as reviewed by choosing the correct node and clicking on this button. This indicates that by visually checking the sequent, the user is convinced that they can discharge it later, but they do not want to do it right now.

• external provers can be invoked from the drop-down list to test sequents.

• begins a proof by cases. The proof is split into two branches. In the first branch, the predicate supplied by the user is added to the Selected Hypotheses, and the user attempts to discharge this branch. In the second branch, the predicate supplied by the user is negated and added to the Selected Hypotheses. The user then attempts to discharge this branch.

• adds a new hypothesis. The predicate in the editing area should be proved by the user. It is then added as a new selected hypothesis.

• adds an abstract expression. The expression in the editing area is given a fresh name.

• invokes the auto prover which attempts to discharge the goal. The auto-prover is applied automatically on all proof obligations after a the machine or context is saved. Using this button, you can invoke the auto-prover within an interactive proof.

• executes the post-tactics.

• loads the hidden hypotheses that contain identifiers in common with the goal and with the selected hypotheses into the Selected Hypotheses window

• backtracks from the current node (i.e., prunes its parent).

• prunes the proof tree from the node selected in the proof tree.

• finds hypotheses containing the character string in the editing area and displays them in the Search Hypothesis view.

• displays the Cache Hypotheses view. This view displays all hypotheses that are related to the current goal.

• loads the preceding undischarged proof obligation.

• loads the next undischarged proof obligation,

• displays information regarding the current proof obligation in the corresponding window. This information corresponds to the elements that directly took part in the generation of the proof obligation (events, invariant, etc.).

• moves to the next pending node of the current proof tree,

• loads the next reviewed node of the current proof tree.

You can also disable/enable post-tactics which allows you to decide if post-tactics should run after each interactive proof step. In addition, you can open the preferences for post-tactics. To do this, open the menu of the Proof Control view via the button in the upper right corner of the view.

3.1.7.4.1 The Smiley

The smiley can be one of three different colours:

1. red indicates that the proof tree contains one or more undischarged sequents

2. blue indicates that all undischarged sequents of the proof tree have been reviewed

3. green indicates that all sequents of the proof tree are discharged.

3.1.7.4.2 The Editing Area

The editing area allows the user to enter parameters for proof commands. For example, in order for the user to add a new hypothesis, the user should enter this hypothesis into the editing area and then should click on the button.

3.1.7.4.3 ML/PP and Hypotheses

3.1.7.4.3.1 ML

The (mono-lemma) prover appears in the drop-down list under the button (pp) as M0, M1, M2, M3, and ML. The different configuration (e.g., M0) refer to the proof force of the ML prover. All hypotheses are passed to ML.

3.1.7.4.3.2 PP

The (predicate prover) appears in the drop-down list under the button (pp) as P0, P1, PP.

• The prover uses all selected hypotheses in the Selected Hypotheses view.

• The prover performs a lasso operation on the selected hypotheses and the goal and uses the resulting hypotheses.

• The prover uses all hypotheses.

3.1.7.5 Auto Prover

The auto prover can be run by clicking the . This prover automatically applies all of the tactics that are predefined in the auto-tactic profile. Section 3.1.8.4 describes in detail how to configure the auto prover, and Section 3.4.3 gives an overview about what proof tactics are and which are available.

3.1.7.6 The Search Hypotheses View

By typing a string in the Proof Control view and pressing the Search Hypotheses ( ) button, all the hypotheses that have a character string in common with the one entered by the user in the editing area are shown in the Search Hypotheses view. For example, if we search for hypotheses containing the character string “cr”, then after pressing the Search Hypothesis ( ) button on the Proof Control view, we obtain the windows as shown in Figure 3.34.

Figure 3.34: The Search Hypotheses View

This view also integrates a “quick search” area (A), that allows us to search for hypotheses containing short character strings such as “cr", a search hypothesis button (B) that behaves the same as the button in the Proof Control view, a refresh button (C) that updates the window manually, and a drop down menu (D) to set up the preferences for the view.

By pressing return key or the button (B) (once a short string has been entered into the input area (A)), specific hypotheses can be found just as quickly as if we had used the Proof Control as described previously.

The drop down menu (D) allows some preferences about the searched hypotheses to be set.

After we have changed preferences for the search, we might need to manually “update” the view with the button (C). By selecting the “Consider hidden hypotheses in search" option, we can view all the hypotheses are not selected in the Selected Hypotheses window.

To move hypotheses to the Selected Hypotheses window, select the desired hypotheses (using the check boxes) and press the button. Adding these hypotheses to the selected hypotheses means that they will be visible to the prover. They can then be used during the next interactive proof phase.

To remove hypotheses from the Search Hypotheses window, use the button. This button also appears above the selected hypotheses and allows the user to remove any hypothesis from the Selected Hypotheses window.

The other button, situated to the left each hypotheses, is the button. Clicking on this will attempt a proof by contradiction. The effect is the same as if the hypothesis were in the Selected Hypotheses window.

3.1.7.7 The Cache Hypotheses View

This window allows the user to keep track of recently manipulated (i.e. used, removed, or selected) hypotheses for any PO. For example, when the user rewrites a hypothesis, the new hypothesis is selected, and the original hypothesis is deselected and put in the Cache Hypotheses window.

Operations similar to those in the Selected Hypotheses and Search Hypotheses views are also available for the cached hypotheses. It is possible to remove, select, and start a proof by contradiction ( ) in the Cache Hypotheses view as well. Interactive proof steps (e.g., rewriting) can also be carried out in the Cache Hypotheses view.

3.1.7.8 The Type Environment View

Figure 3.35: Type Environment View

This view 3.35 shows the type environment for the current node of the proof (free identifiers and their type). It is accessible through Window Show View Type Environment.

3.1.7.9 Proof Information View

This view displays information so that the user can relate a proof obligation to the model. For example, typical information for an event invariant preservation includes the event as well as the invariant in question. For instance, in Figure 3.36, the hyperlinks CreateToken and inv2 can be used to navigate to the containing machine.

Figure 3.36: Proof Information View

3.1.7.10 Rule Details View

This view displays the information relating to a given proof tree node onto which a rule was applied. This information can be viewed by right clicking on any node in the proof tree and selecting Show Details... (see Figure 3.37).

Figure 3.37: Open Rule Details View

By default, this view appears in the Fast View bar. If the window does not appear, click on the button in the Fast View bar to make this view visible. The Fast View bar is in the lower left corner of the Rodin workspace by default.

Figure 3.38 gives an overview of the Rule Details View.

Figure 3.38: Rule Details View

We will now quickly cover all of the information that is displayed in this view. In this figure, the contents of the rule hyp mp are displayed. Here an input has been used to instantiate an hypothesis. The input that was used to instantiate the rule is shown on the line below Rule: hyp mp instantiated with:, and the hypothesis that was used by this rule is shown on the line below Input Sequent:. Furthermore, it is possible to view the antecedents (i.e. child proof tree nodes) created by this rule in detail and the actions (selection, deselection, etc.) that have been performed on the hypotheses.

3.1.7.11 Auto-tactic and Post-tactic

The auto-tactic automatically applies a combination (i.e. ordered list) of rewrite tactics, inference tactics and external provers to newly generated proof obligations. However, they can also be invoked by the user by clicking on the button in the Proof Control view. Note that the automatic application of the auto-prover can be quickly toggled with the Prove Automatically menu item available from the Project menu (See Figure 3.39).

Figure 3.39: Toggle auto-prover via project menu

The post-tactic is also a combination of rewrite tactics, inference tactics and external provers and is applied automatically after each interactive proof step. However, it can also be invoked manually by clicking on the button in the Proof Control view.

Note that the post-tactic can be disabled quickly by clicking on the button (marked with an A) of the Proof Control view (right upper corner) and then by deselecting the box next to the Enable post-tactic option (B) as shown in Figure 3.40.

Figure 3.40: Proof Control view menu

3.1.7.11.1 Principles

The ordered list of rewrite tactics, inference tactics and external provers that should be applied is called a profile. There are two default profiles. One is for auto-tactics and one is for post-tactics. These default profiles cannot be edited, but they can be duplicated for further modification by the user. The user can edit a profile and select it to run as automatic or post tactic. The idea is to have a set of available tactic profiles to be used as needed. Moreover, these edited profiles are saved within projects if they are defined at the project level, and they can be imported or exported if they are defined at a workspace level. This makes it easy to share the profiles.

There are two ways to run the automatic or post tactics:

• Manually by clicking on the button or the button in the Proof Control view to launch the auto-tactic (with the selected auto-tactic profile) and the post-tactic (with the selected post-tactic profile) respectively.

• Automatically if such preference is activated. (Auto-tactic will then run after each proof step and post-tactic will run after each step and rebuild). Post-tactics and auto-tactics only need to be activated in order to run automatically.

The user can separately define tactic profiles and assign them to post and auto tactics. Section 3.1.8.4 describes in detail how to configure auto- and post-tactics.