Rodin User’s Handbook v.2.8: Proof Rules

3.4.2 Proof Rules

In its pure mathematical form, a proof rule is a tool to perform a formal proof and is denoted by:

$\frac{\quad A\quad }{C}$

where $A$ is a (possibly empty) list of sequents (the antecedents of the proof rule) and $C$ is a sequent (the consequent of the rule). We interpret the above proof rule as follows: The combination of the proofs of each sequent of $A$ prove the sequent $C$ .

$\includegraphics[width=7mm]{img/pencil_64.png}$
Example: Consider the following proof rule:

$\frac{ E_1 }{ E_1 \lor E_2 }$

This says that if $E_1$ is valid, then the statement $E_1 \lor E_2$ must be valid as well. Thus, we can replace the sequent by the consequent.

3.4.2.1 Proof Rule Representation in Rodin

In Rodin, the representation for proof rules is more structured not only to reduce the space required to store the rule but, more importantly, to support proof reuse. A proof rule in Rodin contains the following:

used goal: A used goal predicate.
used hypotheses: The set of used hypotheses.
antecedents: A list of antecedents (to be explained later).
reasoner: The reasoner used to generate this proof rule (see Section 3.4.6).
reasoner input: The input for the reasoner to generate this proof rule (reasoners are explained in Section 3.4.6).

Each antecedent of the proof rule contains the following information:

new goal: A new goal predicate.
added hypotheses: The set of added hypotheses.

With this representation, a proof rule in Rodin corresponding to a proof schema as follows:

$\begin{array}{c} H, H_ u, H_{A_0} \vdash G_{A_0} ~ ~ ~ \ldots ~ ~ ~ H, H_ u, H_{A_ n-1} \vdash G_{A_ n-1} \\ \hline H, H_ u \vdash G_ u \end{array}$

Where:

$H_ u$ is the set of used hypotheses
$G_ u$ is the used goal
$H_{A_ i}$ is the set of added hypotheses corresponding to the ith antecedent.
$G_{A_ i}$ is the new goal corresponding to the ith antecedent.
$H$ is the meta-variable that can be instantiated.

3.4.2.2 Applying Proof Rules

Given a proof rule of the form mentioned above, the following describes how to apply this rule to an input sequent. If the process is successful, a list of output sequences is produced.

The rule is not applicable if the goal of the sequent is not exactly the same as the used goal or if any of the used hypotheses are not contained in the set of hypotheses of the input sequent.
If the rule is applicable, the antecedent sequents are returned. The goal of each antecedent sequent is the new goal. The hypotheses of each antecedent sequent are the union of the old hypotheses and added hypotheses of the corresponding antecedent.

$\includegraphics[width=7mm]{img/info_64.png}$
The user interface for proving is explained in Section 3.1.7. The practical application of proof rules is explained in Section 2.9.6.

Rodin Handbook

3.4.2 Proof Rules

3.4.2.1 Proof Rule Representation in Rodin

3.4.2.2 Applying Proof Rules