# Non-case-splitting-logic

Boolean connectives that avoid case splits.

Perhaps the most common reason that ACL2 proofs take a long time is
that they split into too many cases unnecessarily. The alternative Boolean
operators iff*, and*, or*, xor*, and if* can help to
avoid such case splits.

A small and abstract example: Suppose foo is a function that has the following shape:

(defun foo (...)
(cond (<exceptional-case1> ...)
(<exceptional-case2> ...)
...
(<exceptional-casen> ...)
(t ...))) ;; default case

And suppose that each of the N exceptional cases is a conjunction of M
subterms. How many cases will ACL2 typically split into in order to prove
something about foo?

The answer is on the order of M^N. You can get the exact number via the following recurrence:

(defun number-of-cases (n m)
(if (zp n)
1
(+ 1 (* m (number-of-cases (- n 1) m)))))

This is because for each conjunction (and a b c that may cause an
exceptional case, ACL2 considers the cases:

(not a)
(and a (not b))
(and a b (not c))
(and a b c)

In the first three cases, the conjunction is not true (this is where the
* m in the recurrence comes from), and in the last case it is true (this
is where the + 1 in the recurrence comes from).

This is where the alternative operators come in. If we replace the
conjunctions above with and* calls, then instead of splitting into
M^N cases, we split into N+1 cases! This usually works because when
we are in case K, we care that the conjuncts of <exceptional-casek> were
true, but usually not which of the conjuncts of <exceptional-case0>
through exceptional-casek-1 were untrue.

### Subtopics

- Or*
- Non-case-splitting version of OR.
- And*
- Non-case-splitting version of AND.
- Iff*
- Non-case-splitting version of IFF.
- Xor*
- Non-case-splitting version of XOR.