3.4.3 Proof Tactics

Tactics provide an easier way to construct and manage proof search and manipulation. They provide calls to the underlying reasoners or other tactics to modify proofs.

A list of all proof tactics is maintained in the Rodin Wiki.¹ This list is very comprehensive — be sure to check it out!

Tactics can be applied as follows:

Automatic

Rodin can automatically apply a number of tactics after each manual proof step.

Proof tree

Pruning the proof tree is a tactic that can be applied from the proof tree through the context menu. Other tactics may be available there.

In sequents

Some sequents have elements that are highlighted in red. Clicking on these elements brings up a menu with all applicable tactics so that they can be applied manually.

It may be useful to consider the following categories of tactics:

3.4.3.1 Basic Tactics

Basic tactics are tactics that change the proof tree only at the point of application.

• Prune - This tactic is a direct application of the pruning facility providing by the proof tree. The tactic is successful if the input node is not pending.

• Rule Application Tactics - Tactics of this class provide a wrapper around a proof rule (3.4.2). The tactic is successful if the proof rule is successfully applied to the input node.

• Reasoner Application Tactics - Tactics of this class provide a wrapper around a reasoner (3.4.6). The tactic is successful if the reasoner is successfully applied to the input node.

3.4.3.2 Tactical Tactics

Tactical tactics are constructed from existing tactics. They indicate different strategic or heuristic decisions.

• Apply on All Pending - A tactic to apply a specific sub-tactic to all pending nodes at the point of application. The tactic is successful if the sub-tactic is successful on one of the pending nodes.

• Repeating - A tactic that repeats a specific sub-tactic at the point of application until it fails. The tactic is successful if a sub-tactic is successful at least once.

• Composing Sequential - A tactic to compose a list of sub-tactics that can be applied to the point of application. The tactic is successful if one of the sub-tactics is successful.

More complex proof strategy can be constructed by combining the above tactical tactics.