		Search-engine friendly clone of the ACL2 documentation.

Define-sk

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.