SYNTAXP-EXAMPLES

examples pertaining to syntaxp hypotheses 
Major Section:  SYNTAXP

See syntaxp for a basic discussion of the use of syntaxp to control rewriting.

A common syntactic restriction is 

(SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE)))
or, equivalently, 
(SYNTAXP (QUOTEP X)).
A rule with such a hypothesis can be applied only if x is bound to a specific constant. Thus, if x is 23 (which is actually represented internally as (quote 23)), the test evaluates to t; but if x prints as (+ 11 12) then the test evaluates to nil (because (car x) is the symbol binary-+). We see the use of this restriction in the rule 
(implies (and (syntaxp (quotep c))
              (syntaxp (quotep d)))
         (equal (+ c d x)
                (+ (+ c d) x))).
If c and d are constants, then the executable-counterpart of binary-+ will evaluate the sum of c and d. For instance, under the influence of this rule 
(+ 11 12 foo)
rewrites to 
(+ (+ 11 12) foo)
which in turn rewrites to (+ 23 foo). Without the syntactic restriction, this rule would loop with the built-in rules ASSOCIATIVITY-OF-+ or COMMUTATIVITY-OF-+.

We here recommend that the reader try the affects of entering expressions such as the following at the top level ACL2 prompt. 

(+ 11 23)
(+ '11 23)
(+ '11 '23)
(+ ''11 ''23)
:trans (+ 11 23)
:trans (+ '11 23)
:trans (+ ''11 23)
:trans (+ c d x)
:trans (+ (+ c d) x)
We also recommend that the reader verify our claim above about looping by trying the affect of each of the following rules individually. 
(defthm good
   (implies (and (syntaxp (quotep c))
                 (syntaxp (quotep d)))
            (equal (+ c d x)
                   (+ (+ c d) x))))

(defthm bad
   (implies (and (acl2-numberp c)
                 (acl2-numberp d))
            (equal (+ c d x)
                   (+ (+ c d) x))))
on (the false) theorems: 
(thm
  (equal (+ 11 12 x) y))

(thm
  (implies (and (acl2-numberp c)
                (acl2-numberp d)
                (acl2-numberp x))
           (equal (+ c d x) y))).
One can use :brr, perhaps in conjunction with cw-gstack, to investigate any looping.

Here is a simple example showing the value of rule good above. Without good, the thm form below fails. 

(defstub foo (x) t)

(thm (equal (foo (+ 3 4 x)) (foo (+ 7 x))))

The next three examples further explore the use of quote in syntaxp hypotheses.

We continue the examples of syntaxp hypotheses with a rule from community book books/finite-set-theory/set-theory.lisp. We will not discuss here the meaning of this rule, but it is necessary to point out that (ur-elementp nil) is true in this book. 

(defthm scons-nil
  (implies (and (syntaxp (not (equal a ''nil)))
                (ur-elementp a))
           (= (scons e a)
              (scons e nil)))).
Here also, syntaxp is used to prevent looping. Without the restriction, (scons e nil) would be rewritten to itself since (ur-elementp nil) is true.
Question: Why the use of two quotes in ''nil?
Hints: Nil is a constant just as 23 is. Try :trans (cons a nil), :trans (cons 'a 'nil), and :trans (cons ''a ''nil). Also, don't forget that the arguments to a function are evaluated before the function is applied.

The next two rules move negative constants to the other side of an inequality. 

(defthm |(< (+ (- c) x) y)|
  (implies (and (syntaxp (quotep c))
                (syntaxp (< (cadr c) 0))
                (acl2-numberp y))
           (equal (< (+ c x) y)
                  (< (fix x) (+ (- c) y)))))

(defthm |(< y (+ (- c) x))|
  (implies (and (syntaxp (quotep c))
                (syntaxp (< (cadr c) 0))
                (acl2-numberp y))
           (equal (< y (+ c x))
                  (< (+ (- c) y) (fix x)))))
Questions: What would happen if (< (cadr c) '0) were used? What about (< (cadr c) ''0)?

One can also use syntaxp to restrict the application of a rule to a particular set of variable bindings as in the following taken from community book books/ihs/quotient-remainder-lemmas.lisp. 

(encapsulate ()

  (local
   (defthm floor-+-crock
     (implies
      (and (real/rationalp x)
           (real/rationalp y)
           (real/rationalp z)
           (syntaxp (and (eq x 'x) (eq y 'y) (eq z 'z))))
      (equal (floor (+ x y) z)
             (floor (+ (+ (mod x z) (mod y z))
                       (* (+ (floor x z) (floor y z)) z)) z)))))

  (defthm floor-+
    (implies
     (and (force (real/rationalp x))
          (force (real/rationalp y))
          (force (real/rationalp z))
          (force (not (equal z 0))))
     (equal (floor (+ x y) z)
            (+ (floor (+ (mod x z) (mod y z)) z)
               (+ (floor x z) (floor y z))))))

  )
We recommend the use of :brr to investigate the use of floor-+-crock.

Another useful restriction is defined by 

(defun rewriting-goal-literal (x mfc state)

  ;; Are we rewriting a top-level goal literal, rather than rewriting
  ;; to establish a hypothesis from a rewrite (or other) rule?

  (declare (ignore x state))
  (null (access metafunction-context mfc :ancestors))).
We use this restriction in the rule 
(defthm |(< (* x y) 0)|
    (implies (and (syntaxp (rewriting-goal-literal x mfc state))
                  (rationalp x)
                  (rationalp y))
             (equal (< (* x y) 0)
                    (cond ((equal x 0)
                           nil)
                          ((equal y 0)
                           nil)
                          ((< x 0)
                           (< 0 y))
                          ((< 0 x)
                           (< y 0))))))
which has been found to be useful, but which also leads to excessive thrashing in the linear arithmetic package if used indiscriminately.

See extended-metafunctions for information on the use of mfc and metafunction-context.