Rodin Handbook


3.4.5 How to Use the Provers Effectively

It is very hard, in general, to predict whether a certain automatic prover can or cannot discharge a given proof obligation within a given amount of time. (This is also the case for many other automatic first order theorem provers.) Therefore applying the 11 configurations in a trial and error fashion is often frustrating.

The following guidelines may be useful:

  • Add PP restricted, P0, and ML to the auto-tactic. If the auto-tactic runs out of memory, remove PP.

  • If the model is small, add PP after lasso and P1 to the auto-tactic.

  • Whenever you think that the current proof obligation should be discharged automatically, invoke the auto-tactic ( \includegraphics[height=2ex]{img/icons/rodin/auto_prover.png} ) instead of some particular automatic prover.

  • If the auto-tactic fails, it is usually best to simplify the proof obligation in some way. The most important ways of simplifying the proof obligation are:

    • Remove unnecessary hypotheses; add required hypotheses that have been missing.

    • Create a case distinction

    • Instantiate quantifiers.

    • Apply ae (abstract expression) to replace complicated expressions with fresh variables.

  • You can also apply one of the automatic provers. They may be more successful than the auto-tactic because they have a longer timeout.

    • The configurations that act on more than the selected hypotheses (unrestricted P1, PP and ML) become useless when the model grows.

  • When everything fails, try to solve the proof obligation manually by clicking on the red symbols.

    • You may discover that some assumption was missing.

    • You may complete the proof.

    • If you observe that a valid proof obligation cannot be proved manually, please send a bug report (4.2.9).