Adding Reasoners(How to extend Rodin Tutorial)

<prev: Generating the proof obligations

^up: How to extend Rodin Tutorial (Index)

Principles

Rodin support several provers. Some are embedded such as NewPP, or the sequent prover which will talk about here, and some are added by external plug-ins (as the Atelier B provers : ML, PP, P0, etc).

Contributing to Rodin sequent prover is done by adding tactics. These tactics which often involve a set of reasoners, apply on proof tree nodes. The reasoners apply on the sequent of a given proof tree node. A reasoner is (and has to be) quite "rough" : it shall take a given sequent and produce a proof rule that will (if possible) apply on this given sequent, whereas a tactic could be smarter. Indeed, a tactic can involve several reasoners, thus apply them in loops, and combine them, or even call other tactics. A tactic can be either automatic (auto tactic and/or post tactic) or manual (using providers in the UI that paint their applications in red on formulas) in case of interactive proof.

A reasoner encapsulates a kind of "proof step", also called "proof rule". The sequent prover provides a set of tactics applying proof rules (and even other tactics!). These rules are either rewriting rules (see rewriting rule list) or inference rules (see inference rule list). It is actually a really critical piece of code, that developers should understand at first sight, and be convinced about its correctness. If one codes a wrong reasoner, one breaks the whole soundness of proofs done within Rodin! As they are written in pure java, and accorded to the previous considerations, they have to be the simpliest and most readable as possible. Finally, it is needed to write tests that cover all the possible cases of application of one given reasoner (this will not be detailed in this tutorial).

In this part

In this part we will see how to contribute to the sequent prover of Rodin by encapsulating a new proof rule within a reasoner and add a tactic to the sequent prover of Rodin that will encapsulate this reasoner. The rule, coded within the reasoner, that we want to apply is the following:

$\frac{ \textbf{H},\; a = b \;\; \vdash \;\; \textbf{G}} {\textbf{H},\; a \leq b,\;b \leq a\;\vdash \;\; \textbf{G}}$

DBL_INEQ

Let's call this rule DBL_INEQ. By reading this rule, we see it is goal agnostic. This means that the rule will be applied if the prover sequent under consideration contains the hypotheses $a \leq b,\;b \leq a$, whatever the goal of this sequent. We will say that $a \leq b,\;b \leq a$ are the "Needed hypotheses".

Moreover, $\textbf{H}$ is the set of selected hypotheses from the input sequent, and $a \leq b,\;b \leq a\;\vdash \;\textbf{G}$ is the antecedent of the rule (i.e. a child node to be proved).

Step1

• Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.
• Create a new class for the reasoner, called DoubleInequalityReasoner.

Step2

Implement the body of the reasoner :

• the reasoner shall "implements IVersionedReasoner" thus getVersion() shall return a static integer giving the current version of our reasoner. 0 might not be a wrong choice for our first try. getReasonerID() shall return a unique ID that we will further use when registering our reasoner extension point in our plugin. Create here something like :

private static final String REASONER_ID = "org.eventb.doubleInequality.dblIneq";

You should now have something close to this :

public class DoubleInequalityReasoner implements IVersionedReasoner {

	private static final int VERSION = 0;
	private static final String REASONER_ID = "org.eventb.doubleInequality.dblIneq";

	@Override
	public String getReasonerID() {
		return REASONER_ID;
	}

	@Override
	public int getVersion() {
		return VERSION;
	}

	@Override
	public IReasonerOutput apply(IProverSequent seq, IReasonerInput input,
			IProofMonitor pm) {

       }

Step3 / Exercise

Implement the method public IReasonerOutput apply(IProverSequent seq, IReasonerInput input, IProofMonitor pm). This method is where one shall create the proof rule to be applied from the input sequent seq and with the given input if needed. Here is the list of tasks you have to perform in this apply() method :

• get and check the input predicate a <= b
• check the presence of the other hypothesis b <= a
• make the new hypothesis a=b
• make the antecedent
• make the proof rule to return

Step4

Here we see together the solution proposed for the implementation of the apply() method of our reasoner:

<prev: Generating the proof obligations

^up: How to extend Rodin Tutorial (Index)