Proving Tips

Theorem provers internally use search procedures (sophisticated and specialized, but search procedures) that try to find a path from an initial state (the objective to prove) to a (set of) final state(s). In our case, states are sequents with hypotheses to use and goals to prove. Transitions between states are triggered by inference rules that rewrite sequents. In some cases, from a state there may be a single transition to a possible previous state. In other cases an inference may give rise to several states that in turn become goals to prove (e.g., if there is a disjunction on the left). And, last, there may be states where different independent inference rules can be applied, and therefore selecting one of them is necessary, and if one of them does not work to prove a hypothesis, backtracking to try another inference rule may be needed.

Some states are final: sequents whose goal is an axiom, whose goal is among the hypotheses, or whose hypotheses are inconsistent. The objective of the theorem prover is to reach a final state(s) starting from the initial sequent to prove, using inference rules to go from state to state.

Search procedures waste time if useless paths are taken. In our case this may happen, for example, if there are unnecessary hypotheses, as the theorem prover may try to apply inference rules that are not required to discharge a proof . Also, if a necessary hypothesis is absent, then any path taken is useless.

This process may not prove a goal for several reasons. In some cases (e.g., propositional problems), it is possible to exhaust all possible inference rules and traverse all possible states and therefore a failure to prove indicates an impossibility to prove (Rodin flags this with a “Failed” warning on the bottom left of the window). In the case of first-order sequents, it may also be the case that a necessary hypothesis is dropped and the rest of the hypotheses are not enough to prove the goal at hand. Very often, the theorem prover gives up after some predefined amount of time with a “Timeout” result. This does not mean that the sequent cannot be proved, but that no proof has been found after some amount of time.

Some high-level tactics can help provers do their job: (a) avoid unnecessary hypotheses; (b) make sure necessary hypotheses are there; (c) simplify the proof.

Check the Proving Perspective section of the Rodin Handbook to learn more about what Rodin provides to help discharge proof obligations, including an explanation of the elements in the proving perspective and more information on how to interact with the prover.

Search tree and hypotheses

In the Proving Perspective, Rodin keeps on the left of the window a tab with the current search tree. You can click on any point in it and see what is the goal and the active hypotheses. After selecting a point in the search tree, it is also possible to cut to that node by clicking on the scissors in the proving toolbar (or right-clicking on the node and selecting Prune). Then the search process moves to that state and the goal and hypotheses at that point become current.

When you enter the Proving perspective, chances are that the internal theorem prover has made some attempts to prove / simplify the proof. What the prover has attempted is shown in the search tree on the left and the current goal is probably not the initial goal that was required by the proof obligation.

The Goal tab contains the goal to be proved. The button Search Hypotheses makes all the available hypotheses appear in panel on the right. These are used by the PP button. The Selected Hypotheses section collects the subset of the current hypotheses that are used by P0 to try to prove the goal. This is so because in some cases the set of selected hypotheses may be too large and it is better to use only a meaningful subset of the existing hypotheses or apply to them transformations. Hypotheses can be selected in the Search Hypotheses panel and added to the Selected Hypotheses and hypotheses can be removed from the selected hypotheses.

Warning: Do not use the “NewPP theorem prover. It is unsound and may give wrong results.

The Lasso button selects a subset of the existing hypotheses using a heuristic that takes into account which symbols are there in common with the current goal; it works reasonably well, at least as a first approach. But it may err either including unnecessary hypotheses or the opposite.

You can right-click on any symbol in red in the panels of the Proving perspective. Rewriting options will appear.

Simple proof strategies

  • When you enter the Proving perspective, click P0. If you’re lucky, it may be enough. “P0” starts the external prover with the hypothesis that appear in the Selected hypotheses window. Hypotheses can be added or removed from that window.
  • Otherwise, use Lasso to bring to the selected hypotheses additional hypotheses, then click P0. Lasso is not guaranteed to select all the relevant hypothesis. Review them and check whether there is any hypothesis that ought to be necessary and is not in the Selected hypotheses window.
  • If it does not work, try PP in the current goal. PP uses the Atelier B prover using all available hypotheses. That can make the space of the search for a proof too large, due to the many possibilities of applying inference rules. It often times out, but it is worth trying if other possibilities don’t work. In general, it is better to restrict the hypotheses to use to attempt a proof.
  • If it does not work, you can cut / prune to the initial node of the search tree to select the goal and hypotheses required by the proof obligation and use there PP or Lasso + P0.
  • If you have pruned to a node up in the search tree, you can rerun the automatic theorem provers by clicking on the green robot head (“Run Auto Provers”).
  • To add hypotheses to the selected hypotheses: click on the “Search Hypothesis” button in the proof control tab, select those to be added to the selected hypotheses and click on the green icon with a white “+” .
  • Changes in invariants, axioms, guards, and actions invalidate proofs assisted by hand. However, Rodin can attempt to redo the proofs. In the panel with the machine name, right-click on the machine (or context, in its case) and select “Proof replay on undischarged POs”. With some luck, the previous proof strategies will continue to be applicable.

Avoiding unnecessary hypotheses

  • Make sure that, among comparable hypotheses, only the most specific ones (the strongest hypotheses) are used, and remove the others from the Selected Hypotheses. For example, if we have a > 1 and a ∈ ℕ, keep the former, as it implies the latter.
  • Remove hypotheses not necessary to prove the goal. This is delicate, as sometimes a hypothesis does not look necessary, but is indirectly required. Also, if the goal can only be proved showing inconsistency in the hypotheses, removing hypotheses may make the inconsistency disappear. To remove hypotheses: select those to be removed, click on the red icon with a white “-“.

Ensuring that the necessary hypotheses are there

It is not easy to decide beforehand when a hypothesis is necessary, but some general rules may help.

  • Bounds for variables are in general helpful, as they make the hypotheses stronger. Add them to the selected hypotheses. Use the strictest possible bounds available, in concordance with (a).
  • Make sure the selected hypotheses set is “closed”, i.e., it does not refer to any symbol that is not defined in the set. I.e., if you have r ∈ p..q, make sure there are selected hypotheses that make it explicit what are the ranges of p and q. Note: this is sometimes not needed, as the bounds / types of some symbols may sometimes be inferred, but I recommend not to trust that this is so.
  • When the prover is stuck, examine the goal, and try to decide whether it is something that must happen (i.e., a valid property) or not.
    • If it does, try to determine what is missing to prove it, and whether that missing condition is or not true.
    • If it is, try to find hypotheses that provide it. If none seems to be available, it may be necessary to work on some strategy combining several hypothesis and simplifications to derive that condition. The CUT inference rule may help, but this has to be done by hand: think of a formula that is necessary to prove the goal and that can be deduced from the rest of the hypotheses, add it to the selected hypotheses writing it in the Proof Control window and clicking on the ah (add hypothesis) button. A subtree to prove that hypothesis will be open and another one where that hypothesis is added to the sequent will appear as well.
    • If it is a condition that should be true, but no hypotheses support it, perhaps there are missing hypotheses: the axioms are not complete, there are missing invariants, or the guards of the event need to be stronger. In the last case, be careful when adding / strengthening guards: you may compromise completeness.
  • If the goal describes something that cannot take place, your only chance to prove it is to make the hypotheses inconsistent. That needs the right hypotheses because an “unsatisfiable kernel” is needed. If one formula involved in making the hypotheses inconsistent is missing, inconsistency cannot be proved.

Simplifying proofs

This helps in two directions. On the one hand, sometimes the right rule to use needs a step that is difficult or impossible to guess for the prover. On the other hand, every time we simplify a proof (in the right direction), we are actually buying time against the timeout of the prover.

  • If you have a disjunction among the hypotheses, you may want to tell Rodin to split the proof into two branches. If the disjunction symbol is in red, just click on it. Two simpler branches will be generated and will appear in the left pane.
  • Similarly if you have a conjunction in the goal. You need to prove separately each formula and can tell Rodin to create a branch for each.
  • Quantifiers: for some proofs, the variables in the quantifiers need to be instantiated using the right values / variables to use the resulting formula. That needs you to decide what are the right bindings and do the instantiation: enter values / variable names in the boxes, click on the quantifier.
  • Distinction by cases: a proof can often be simplified by splitting the hypotheses in several cases. If we have a ≥ 0, we can study what happens if a = 0 and what happens if a > 0. You can add a = 0 ∨ a > 0 in the Proof Control and add it as hypotheses. You can then remove a ≥ 0 from the hypotheses.
  • Rodin has a general approach to deal with distinction by cases: if a formula F is written in the proof control window, pressing “dc” makes Rodin add the formula F ∨ ¬F in the hypotheses (since F ∨ ¬F ≡ ⊤ , no information is added / removed) and will create two branches, one with F and another one with ¬F. Sequents can be simplified by judiciously choosing F. In the example mentioned above: if we have a ≥ 0 and we enter F ≡ a = 0, we will create two sequents with hypotheses a ≥ 0, a = 0 (which simplifies to a = 0) and a ≥ 0, a ≠ 0 (which simplifies to a > 0).
  • Interval membership: x ∈ a..b can be simplified (by clicking on ∈, when it is in red) into x ≥ a ∧ x ≤ b. This is especially useful in the goals because a different branch can be generated for each component of the conjunction.
  • Domain membership: if we simplify the domain in x ∈ dom(f) by clicking on the dom keyword, it will be converted into something similar to x ∈ a..b which can then be converted into x ≥ a ∧ x ≤ b.
  • Clicking on the membership symbol when the set is a function domain / range transforms it into ∃ y ⋅ x ↦ y ∈ f. This is useful when we need to access both components of a tuple in the function.
  • Propagate variable instantiation: when a variable in the hypotheses is given a definite value, such as a = 0, you can propagate this value to wherever the variable appears.