Negation Normal Form

This page describes the design of a tactic for putting a sequent in Negation Normal Form, as requested by Feature Request #3137893.

Objective

A predicate is in Negation Normal Form when negation occurs only on atomic expression. To compute such a normal form, the following rewrite rules (which are already implemented in Rodin) are used:

SIMP_NOT_NOT: $\lnot\, \lnot\, P \;\;\defi\;\; P$

DISTRI_NOT_AND: $\lnot\,(P \land Q) \;\;\defi\;\; \lnot\, P \lor \lnot\, Q$

DISTRI_NOT_OR: $\lnot\,(P \lor Q) \;\;\defi\;\; \lnot\, P \land \lnot\, Q$

DERIV_NOT_IMP: $\lnot\,(P \limp Q) \;\;\defi\;\; P \land \lnot\, Q$

DERIV_NOT_FORALL: $\lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P$

DERIV_NOT_EXISTS: $\lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P$

However, no rule has been defined for the case where the inner predicate is an equivalence, such as $\lnot (P \leqv Q)$, which is equivalent to both $\lnot P \leqv Q$ and $P \leqv\lnot Q$. Currently, the tactic will not do anything for such predicates.

Analysis

For equivalence predicate, as the tactic is to be designed for interactive use, we prefer to keep the equivalence predicate (rather than translate it to e.g., double implication). However, it is not clear how to decide which sub-predicate should get the negation. Some cases seem obvious. For instance, if one of the child is itself a negation, it seems a good idea to push the negation to this child (where both negations will cancel each other). Similarly, if one child is atomic, pushing the negation to this child seems also a good candidate.

However, in the general case, it is not easy to decide to which child the negation shall be pushed downto. For instance, consider predicate

$\lnot(A \leqv (\lnot B \land\lnot C))$

If we push negation to the left-hand child, we obtain the equivalent predicate

$\lnot A \leqv (\lnot B \land\lnot C)$

But, if we push it to the right-hand child, we get the normal form

$A \leqv (B \or C)$

which is highly preferable, as it is simpler to read.

It is not yet clear whether there is a good criterion for deciding which child to go for.

Implementation

The tactic shall apply to all visible hypotheses and the goal of a sequent. It should apply repeatedly the above rewrite rules until all these predicates are in Negation Normal Form.

However, care should be taken when organising the applications of these rules. They should be applied following a pre-order traversal of the predicate, to avoid undoing and redoing several times the same operations. This can be easily shown in the following example.

When rewrite rules are applied in the right order, the following rewrites are performed

$\lnot(A \land \lnot (B \lor C))$

$\lnot A \lor \lnot\lnot (B \lor C)$

$\lnot A \lor (B \lor C)$

However, if another order is used, one could get a much longer rewriting chain, such as

$\lnot(A \land \lnot (B \lor C))$

$\lnot(A \land (\lnot B \land \lnot C))$

$\lnot A \lor \lnot(\lnot B \land \lnot C)$

$\lnot A \lor (\lnot\lnot B \lor \lnot\lnot C)$

$\lnot A \lor (B \lor \lnot\lnot C)$

$\lnot A \lor (B \lor C)$