Proof Contextual Information

The aim of this page is to define a way for provers (tactics, reasoners) to handle cases where their behaviour shall depend on the context of the proof obligation. Usually, as was the case until the Rule-Based Prover appeared, prover behaviours were only determined by a sequent and optionally a user input. Several features of the platform now require extra information:

• project specific tactic profiles need the project of the PO
• mathematical extension rules need the theory where the rule is defined
• rule-based prover needs to know whether the rules in a proof are still valid (reusable)

The last point concerns the rule-based prover as a separate plug-in as well as its equivalent in mathematical extensions. The requirement stated here is that, after a project clean, proof states must reflect the possibility to replay corresponding proofs. If a given rule has been used in a proof, and then this rule has been changed or removed, the proof status must be considered broken.

Reasoners are Context-Free

The concept of a reasoner is that of a purely mathematical processing unit. Hence it shall remain unaware of notions like project, proof obligation, or merely proof … The only notion a reasoner deals with is that of sequent, along with an optional specific input.

Handling Context with Tactics

Thus, contextual informations have to be handled in tactics. They take a proof tree node as parameter, so all information should be available from this starting point. After fetching and processing these data, a tactic can specify the intended behaviour of the called reasoner(s) via reasoner input(s). For instance, when a rule-based prover tactic knows which theory is being proved and which rules are applicable, these rules can be encapsulated in the reasoner input passed to the reasoner. The reasoner then only applies the given rules, regardless of any external notion.

Similarly, when the user profile metatactic knows which project it is applied to, it can call the project-specific profile metatactic.

Handling Rule Validity with Reasoners

For reasoners to remain sound in whatever context at whatever time, it is their own duty to verify the validity of this input. Thus, if tactics pass rules through their input, and these rules are liable to become invalid (changed or removed), a reasoner must verify their validity before applying them. This could be achieved with a global registry of currently valid rules, updated during deployments.

The problem of updating proof states after a clean can be solved by these very reasoners, if they visibly bear their particularity (of not always being reusable). They could implement a special interface, say IIrregularReasoner with a method isReusable(IReasonerInput input). This method would be called when checking proof reusability at proof status update time.

In the Origin was the Proof Attempt

There is currently already a contextual information available to tactics from a proof tree node, which is the proof attempt given as origin to the proof tree. This information is put into the proof tree in every situation where a tactic could be called on the proof tree. It can then be asserted that the origin of a proof tree received by a tactic is the corresponding proof attempt.

The following is a code snippet showing how to fetch a handle to the PO sequent from a proof tree node:

	public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {
		final Object origin = ptNode.getProofTree().getOrigin();
		if (!(origin instanceof IProofAttempt)) {
			return "tactic unapplicable without contextual information";
		}
		final IProofAttempt pa = (IProofAttempt) origin;
		final String poName = pa.getName();
		final IProofComponent pc = pa.getComponent();
		final IPORoot poRoot = pc.getPORoot();
		final IPOSequent sequent = poRoot.getSequent(poName);
		// ...
	}