# Define-sk-implies-handling

Explanation of the :implies :smart option for define-sk.

By default, the define-sk macro handles calls of
implies in its function's body in a ``smart'' way. Below we explain what
problem this special handling is meant to help with and the way it works.

Note: you can disable this behavior via :implies :dumb.

### Sketch of the problem

Consider a quantified function definition like:

(defun-sk all-greaterp (min list)
(declare (xargs :guard (and (integerp min)
(integer-listp list))
:verify-guards nil))
(forall (elem)
(implies (member elem list)
(< min elem))))

Unfortunately, the above produces a lousy -necc theorem that isn't
really the rule you usually want:

(defthm all-greaterp-necc
(implies (not (implies (member elem list)
(< min elem)))
(not (all-greaterp min list))))

We can get a better rule by adding the :rewrite :direct option to the
defun-sk. After we do that, we get a better rule:

(defthm all-greaterp-necc
(implies (all-greaterp min list)
(implies (member elem list)
(< min elem))))

So that's great. The problem comes in when we try to verify the guards of
all-greaterp. For that, we need to know that elem is a number when
we call (< min elem). This is obviously true since elem is a member
of list, an integer list—except wait, implies is a real
function, so when we call (< min elem), we haven't yet established that
elem is in list.

To fix this, we might try to rewrite our function to get rid of the
implies. For instance, we might write:

(defun-sk all-greaterp (min list)
(declare (xargs :guard (and (integerp min)
(integer-listp list))
:verify-guards nil))
(forall (elem)
(if (member elem list)
(< min elem)
t))
:rewrite :direct)

But now we run into a different problem: the -necc theorem now ends up
looking like this:

(defthm all-greaterp-necc
(implies (all-greaterp min list)
(if (member elem list)
(< min elem)
t)))

But this isn't a valid rewrite rule
because of the if in the conclusion!

In short: for guard verification we generally want to use something like
if or impliez instead of
implies, but to get good rewrite rules we need to use implies.

### Solution

To try to help with this, define-sk does something special with
implies forms inside the body. In particular, when we submit:

(define-sk all-greaterp ((min integerp) (list integer-listp))
(forall (elem)
(implies (member elem list)
(< min elem))))

The implies terms in the resulting defun for all-greaterp
will automatically get expanded into if terms. That is, the real defun that we submit will look something like this:

(defun all-greaterp (min list)
(declare ...)
(let ((elem (all-greaterp-witness min list)))
(if (member elem list)
(< min elem)
t)))

This will generally help to make guard verification more straightforward
because you'll be able to assume the hyps hold during the conclusion. But note
that this rewriting of implies is done only in the function's body, not in
the -necc theorem where it would ruin the rewrite rule.

Is this safe? There's of course no logical difference between implies
and impliez, but there certainly is a big difference in the execution, viz
evaluation order. Fortunately, this difference will not matter for what we are
trying to do: we're only changing implies to if in code that follows
a call of the -witness function. This code can never be reached in real
execution, because calling the -witness function will cause an error. So:
logically we aren't changing anything, and this term is never executed anyway,
so execution differences don't matter.