New Proof Rules

This document describes the set of newly added reasoners for improving the usability of the prover within Rodin Platform. The work has been done originally by Stephan Merkli, Michael Schaufelberger and David Simmen as their project for an object oriented programming course at ETH Zürich.

Remove Membership for Range

This is submitted as feature request 1942487 at sourceforge.

1942487

The request is about the following rewriting rule:

$E \in a \upto b  ~~~\mathrel{\widehat{=}}~~~ a \leq E ~\land~ E \leq b$

The rule has been implemented so that it can be applied both automatically and interactively.

• Automatically: The rule can be chosen from the Preferences of the Sequent Prover to be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is carried out to all sub-formulas of the form $E \in a \upto b$.

• Interactively: The $\in$ symbol is redden in the formular (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.

Automatic Rule for Overriding

This is submitted as feature request 1936295 at sourceforge.

1936295

The request is about the following rewriting rule:

$p \ovl \ldots \ovl \emptyset \ovl \ldots q  ~~~\mathrel{\widehat{=}}~~~ p \ovl \ldots \ovl q$

(i.e. removing $\emptyset$ for overriding $\ovl$ operator)

The rule is added so that it can be applied automatically. User can choose the rule from the Preferences of the Sequent Prover, so that it can be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is carried out to all sub-formulas of the form that match the left-hand side of the rule.

Automatically Apply De Morgan's Laws

This is submitted as feature request 1935674 at sourceforge.

1935674

The request is about the following rewriting rules (De Morgan's Laws):

$\begin{array}{c}
		 \neg ( P \land \ldots \land Q )  ~~~\mathrel{\widehat{=}}~~~  \neg P \lor \ldots \lor \neg Q \\
		 \neg (P \lor \ldots \lor Q)  ~~~\mathrel{\widehat{=}}~~~  \neg P \land \ldots \land \neg Q \\
		 \neg (\forall x \qdot P)  ~~~\mathrel{\widehat{=}}~~~  \exists x \qdot \neg P \\
		 \neg (\exists x \qdot P)  ~~~\mathrel{\widehat{=}}~~~  \forall x \qdot \neg P
	 \end{array}$ 

Currently, these rewriting rules can be invoked manualy during interactive proofs. The rules is added so that user can choose from the Preferences of the Sequent Prover, so that they can be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is recursively carried out to all sub-formulas of the form that match the left-hand side of the one of the rule.

Automatically Rewrite $\dom(f) = S$

This is submitted as feature request 1866809 at sourceforge.

1866809

The request is about rewriting automatically $\dom(f) \mathrel{\widehat{=}} S$ for selected hypotheses and goal if there is a hypothesis that $f$ is a total function from $S$, e.g.

$\begin{array}{l}
		f \in S \trel T \\
		f \in S \tfun T \\
		f \in S \tinj T \\
		f \in S \tbij T
	\end{array}$

The rule is added so that it can be applied automatically. User can choose the rule from the Preferences of the Sequent Prover, so that it can be run as a part of the Automatic Prover or as a part of the Post-Tactic.

Interactively Rewrite $B \subset A$

This is submitted as feature request 1834715 at sourceforge.

1834715

The request is about providing support for interactively proving $B \subset A$ according to the following rewriting rules.

$B \subset A   ~~~\mathrel{\widehat{=}}~~~ B \subseteq A ~\land~ B \neq A$

The rule has been implemented so that it can be applied both automatically and interactively.

• Automatically: The rule can be chosen from the Preferences of the Sequent Prover to be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is carried out to all sub-formulas of the form $B \subset A$.

• Interactively: The $\subset$ symbol is redden in the formular (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.